Examples/multiwf.ml

   1 (* ========================================================================= *)
   2 (* Part 1: Background theories.                                              *)
   3 (* ========================================================================= *)
   4
   5 let EMPTY_IS_FINITE = prove
   6  (`!s. (s = EMPTY) ==> FINITE s`,
   7   SIMP_TAC[FINITE_RULES]);;
   8
   9 let SING_IS_FINITE = prove
  10  (`!s a. (s = {a}) ==> FINITE s`,
  11   SIMP_TAC[FINITE_INSERT; FINITE_RULES]);;
  12
  13 let UNION_NONZERO = prove
  14  (`{a | ~(f a + g a = 0)} = {a | ~(f a = 0)} UNION {a | ~(g a = 0)}`,
  15   REWRITE_TAC[ADD_EQ_0; EXTENSION; IN_UNION; IN_ELIM_THM; DE_MORGAN_THM]);;
  16
  17 (* ------------------------------------------------------------------------- *)
  18 (* Definition of type of finite multisets with a few basic operations.       *)
  19 (* ------------------------------------------------------------------------- *)
  20
  21 parse_as_infix("mmember",(11,"right"));;
  22 parse_as_infix("munion",(16,"right"));;
  23 parse_as_infix("mdiff",(18,"left"));;
  24
  25 let multiset_tybij_th = prove
  26  (`?f. FINITE {a:A | ~(f a = 0)}`,
  27   EXISTS_TAC `\a:A. 0` THEN
  28   SIMP_TAC[EMPTY_IS_FINITE; EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY]);;
  29
  30 let multiset_tybij = new_type_definition
  31   "multiset" ("multiset","multiplicity") multiset_tybij_th;;
  32
  33 let mempty = new_definition
  34   `mempty = multiset (\b. 0)`;;
  35
  36 let mmember = new_definition
  37   `a mmember M <=> ~(multiplicity M a = 0)`;;
  38
  39 let msing = new_definition
  40   `msing a = multiset (\b. if b = a then 1 else 0)`;;
  41
  42 let munion = new_definition
  43   `M munion N = multiset(\b. multiplicity M b + multiplicity N b)`;;
  44
  45 let mdiff = new_definition
  46   `M mdiff N = multiset(\b. multiplicity M b - multiplicity N b)`;;
  47
  48 (* ------------------------------------------------------------------------- *)
  49 (* Extensionality for multisets.                                             *)
  50 (* ------------------------------------------------------------------------- *)
  51
  52 let MEXTENSION = prove
  53  (`(M = N) = !a. multiplicity M a = multiplicity N a`,
  54   REWRITE_TAC[GSYM FUN_EQ_THM] THEN CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN
  55   MESON_TAC[multiset_tybij]);;
  56
  57 (* ------------------------------------------------------------------------- *)
  58 (* Basic properties of multisets.                                            *)
  59 (* ------------------------------------------------------------------------- *)
  60
  61 let MULTIPLICITY_MULTISET = prove
  62  (`FINITE {a | ~(f a = 0)} /\ (f a = y) ==> (multiplicity(multiset f) a = y)`,
  63   SIMP_TAC[multiset_tybij]);;
  64
  65 let MEMPTY = prove
  66  (`multiplicity mempty a = 0`,
  67   REWRITE_TAC[mempty] THEN MATCH_MP_TAC MULTIPLICITY_MULTISET THEN
  68   SIMP_TAC[EMPTY_IS_FINITE; EXTENSION; IN_ELIM_THM; NOT_IN_EMPTY]);;
  69
  70 let MSING = prove
  71  (`multiplicity (msing (a:A)) b = if b = a then 1 else 0`,
  72   REWRITE_TAC[msing] THEN MATCH_MP_TAC MULTIPLICITY_MULTISET THEN
  73   REWRITE_TAC[] THEN MATCH_MP_TAC SING_IS_FINITE THEN EXISTS_TAC `a:A` THEN
  74   REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_INSERT; NOT_IN_EMPTY] THEN
  75   GEN_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[ARITH_EQ]);;
  76
  77 let MUNION = prove
  78  (`multiplicity (M munion N) a = multiplicity M a + multiplicity N a`,
  79   REWRITE_TAC[munion] THEN MATCH_MP_TAC MULTIPLICITY_MULTISET THEN
  80   REWRITE_TAC[UNION_NONZERO; FINITE_UNION] THEN SIMP_TAC[multiset_tybij] THEN
  81   CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[multiset_tybij]);;
  82
  83 let MDIFF = prove
  84  (`multiplicity (M mdiff N) (a:A) = multiplicity M a - multiplicity N a`,
  85   REWRITE_TAC[mdiff] THEN MATCH_MP_TAC MULTIPLICITY_MULTISET THEN
  86   REWRITE_TAC[] THEN MATCH_MP_TAC FINITE_SUBSET THEN
  87   EXISTS_TAC `{a:A | ~(multiplicity M a = 0)}` THEN
  88   SIMP_TAC[SUBSET; IN_ELIM_THM; multiset_tybij] THEN
  89   CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[multiset_tybij] THEN
  90   ARITH_TAC);;
  91
  92 (* ------------------------------------------------------------------------- *)
  93 (* Some trivial properties of multisets that we use later.                   *)
  94 (* ------------------------------------------------------------------------- *)
  95
  96 let MUNION_MEMPTY = prove
  97  (`~(M munion (msing(a:A)) = mempty)`,
  98   REWRITE_TAC[MEXTENSION; MEMPTY; MSING; MUNION] THEN
  99   DISCH_THEN(MP_TAC o SPEC `a:A`) THEN
 100   REWRITE_TAC[ADD_EQ_0; ARITH_EQ]);;
 101
 102 let MMEMBER_MUNION = prove
 103  (`x mmember (M munion N) <=> x mmember M \/ x mmember N`,
 104   REWRITE_TAC[mmember; MUNION; ADD_EQ_0; DE_MORGAN_THM]);;
 105
 106 let MMEMBER_MSING = prove
 107  (`x mmember (msing a) <=> (x = a)`,
 108   REWRITE_TAC[mmember; MSING] THEN COND_CASES_TAC THEN REWRITE_TAC[ARITH_EQ]);;
 109
 110 let MUNION_EMPTY = prove
 111  (`M munion mempty = M`,
 112   REWRITE_TAC[MEXTENSION; MUNION; MEMPTY; ADD_CLAUSES]);;
 113
 114 let MUNION_ASSOC = prove
 115  (`M1 munion (M2 munion M3) = (M1 munion M2) munion M3`,
 116   REWRITE_TAC[MEXTENSION; MUNION; ADD_ASSOC]);;
 117
 118 let MUNION_AC = prove
 119  (`(M1 munion M2 = M2 munion M1) /\
 120    ((M1 munion M2) munion M3 = M1 munion M2 munion M3) /\
 121    (M1 munion M2 munion M3 = M2 munion M1 munion M3)`,
 122   REWRITE_TAC[MEXTENSION; MUNION; ADD_AC]);;
 123
 124 let MUNION_11 = prove
 125  (`(M1 munion N = M2 munion N) <=> (M1 = M2)`,
 126   REWRITE_TAC[MEXTENSION; MUNION; EQ_ADD_RCANCEL]);;
 127
 128 let MUNION_INUNION = prove
 129  (`a mmember (M munion (msing b)) /\ ~(b = a) ==> a mmember M`,
 130   REWRITE_TAC[mmember; MUNION; MSING; ADD_EQ_0] THEN
 131   COND_CASES_TAC THEN ASM_REWRITE_TAC[ARITH_EQ]);;
 132
 133 let MMEMBER_MDIFF = prove
 134  (`(a:A) mmember M ==> (M = (M mdiff (msing a)) munion (msing a))`,
 135   REWRITE_TAC[mmember; MEXTENSION; MUNION; MDIFF; MSING] THEN
 136   REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
 137   UNDISCH_TAC `~(multiplicity M (a:A) = 0)` THEN ARITH_TAC);;
 138
 139 (* ------------------------------------------------------------------------- *)
 140 (* Induction principle for multisets.                                        *)
 141 (* ------------------------------------------------------------------------- *)
 142
 143 let MULTISET_INDUCT_LEMMA1 = prove
 144  (`(!M. ({a | ~(multiplicity M a = 0)} SUBSET s) ==> P M) /\
 145    (!a:A M. P M ==> P (M munion (msing a)))
 146    ==> !n M. (multiplicity M a = n) /\
 147              {a:A | ~(multiplicity M a = 0)} SUBSET (a INSERT s)
 148              ==> P M`,
 149   STRIP_TAC THEN INDUCT_TAC THEN REPEAT STRIP_TAC THENL
 150    [FIRST_X_ASSUM MATCH_MP_TAC THEN
 151     UNDISCH_TAC `{a:A | ~(multiplicity M a = 0)} SUBSET (a INSERT s)` THEN
 152     REWRITE_TAC[SUBSET; IN_ELIM_THM; IN_INSERT] THEN ASM_MESON_TAC[];
 153     SUBGOAL_THEN `M = (M mdiff (msing(a:A))) munion (msing a)` SUBST1_TAC THENL
 154      [MATCH_MP_TAC MMEMBER_MDIFF THEN ASM_REWRITE_TAC[mmember; NOT_SUC];
 155       ALL_TAC] THEN
 156     MAP_EVERY (MATCH_MP_TAC o ASSUME)
 157      [`!a:A M. P M ==> P (M munion msing a)`;
 158       `!M. (multiplicity M a = n) /\
 159            {a:A | ~(multiplicity M a = 0)} SUBSET (a INSERT s)
 160            ==> P M`] THEN
 161     ASM_REWRITE_TAC[MDIFF; MSING; ARITH_RULE `SUC n - 1 = n`] THEN
 162     MATCH_MP_TAC SUBSET_TRANS THEN
 163     EXISTS_TAC `{a:A | ~(multiplicity M a = 0)}` THEN
 164     ASM_SIMP_TAC[SUBSET; IN_ELIM_THM; CONTRAPOS_THM; SUB_0]]);;
 165
 166 let MULTISET_INDUCT_LEMMA2 = prove
 167  (`P mempty /\
 168    (!a:A M. P M ==> P (M munion (msing a)))
 169    ==> !s. FINITE s ==> !M. {a:A | ~(multiplicity M a = 0)} SUBSET s ==> P M`,
 170   STRIP_TAC THEN MATCH_MP_TAC FINITE_INDUCT THEN CONJ_TAC THENL
 171    [REWRITE_TAC[SUBSET; IN_ELIM_THM; NOT_IN_EMPTY] THEN
 172     REPEAT STRIP_TAC THEN
 173     SUBGOAL_THEN `M:(A)multiset = mempty` (fun th -> ASM_REWRITE_TAC[th]) THEN
 174     ASM_REWRITE_TAC[MEXTENSION; MEMPTY]; X_GEN_TAC `a:A`] THEN
 175   REPEAT STRIP_TAC THEN MP_TAC MULTISET_INDUCT_LEMMA1 THEN
 176   ASM_REWRITE_TAC[] THEN DISCH_THEN MATCH_MP_TAC THEN
 177   ASM_REWRITE_TAC[GSYM EXISTS_REFL]);;
 178
 179 let MULTISET_INDUCT = prove
 180  (`P mempty /\
 181    (!a:A M. P M ==> P (M munion (msing a)))
 182    ==> !M. P M`,
 183   DISCH_THEN(MP_TAC o MATCH_MP MULTISET_INDUCT_LEMMA2) THEN
 184   REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
 185   REWRITE_TAC[IMP_IMP] THEN
 186   GEN_TAC THEN DISCH_THEN MATCH_MP_TAC THEN
 187   EXISTS_TAC `{a:A | ~(multiplicity M a = 0)}` THEN
 188   REWRITE_TAC[SUBSET_REFL; multiset_tybij] THEN
 189   CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[multiset_tybij]);;
 190
 191 (* ========================================================================= *)
 192 (* Part 2: Transcription of Tobias's paper.                                  *)
 193 (* ========================================================================= *)
 194
 195 parse_as_infix("<<",(12,"right"));;
 196
 197 (* ------------------------------------------------------------------------- *)
 198 (* Wellfounded part of a relation.                                           *)
 199 (* ------------------------------------------------------------------------- *)
 200
 201 let WFP_RULES,WFP_INDUCT,WFP_CASES = new_inductive_definition
 202   `!x. (!y. y << x ==> WFP(<<) y) ==> WFP(<<) x`;;
 203
 204 (* ------------------------------------------------------------------------- *)
 205 (* Wellfounded part induction.                                               *)
 206 (* ------------------------------------------------------------------------- *)
 207
 208 let WFP_PART_INDUCT = prove
 209  (`!P. (!x. x IN WFP(<<) /\ (!y. y << x ==> P(y)) ==> P(x))
 210        ==> !x:A. x IN WFP(<<) ==> P(x)`,
 211   GEN_TAC THEN REWRITE_TAC[IN] THEN STRIP_TAC THEN
 212   ONCE_REWRITE_TAC[TAUT `a ==> b <=> a ==> a /\ b`] THEN
 213   MATCH_MP_TAC WFP_INDUCT THEN ASM_MESON_TAC[WFP_RULES]);;
 214
 215 (* ------------------------------------------------------------------------- *)
 216 (* A relation is wellfounded iff WFP is the whole universe.                  *)
 217 (* ------------------------------------------------------------------------- *)
 218
 219 let WFP_WF = prove
 220  (`WF(<<) <=> (WFP(<<) = UNIV:A->bool)`,
 221   EQ_TAC THENL
 222    [REWRITE_TAC[WF_IND; EXTENSION; IN; UNIV] THEN MESON_TAC[WFP_RULES];
 223     DISCH_TAC THEN MP_TAC WFP_PART_INDUCT THEN
 224     ASM_REWRITE_TAC[IN; UNIV; WF_IND]]);;
 225
 226 (* ------------------------------------------------------------------------- *)
 227 (* The multiset order.                                                       *)
 228 (* ------------------------------------------------------------------------- *)
 229
 230 let morder = new_definition
 231   `morder(<<) N M <=> ?M0 a K. (M = M0 munion (msing a)) /\
 232                                (N = M0 munion K) /\
 233                                (!b. b mmember K ==> b << a)`;;
 234
 235 (* ------------------------------------------------------------------------- *)
 236 (* We separate off this part from the proof of LEMMA_2_1.                    *)
 237 (* ------------------------------------------------------------------------- *)
 238
 239 let LEMMA_2_0 = prove
 240  (`morder(<<) N (M0 munion (msing a))
 241    ==> (?M. morder(<<) M M0 /\ (N = M munion (msing a))) \/
 242        (?K. (N = M0 munion K) /\ (!b:A. b mmember K ==> b << a))`,
 243   GEN_REWRITE_TAC LAND_CONV [morder] THEN
 244   DISCH_THEN(EVERY_TCL (map X_CHOOSE_THEN
 245    [`M1:(A)multiset`; `b:A`; `K:(A)multiset`]) STRIP_ASSUME_TAC) THEN
 246   ASM_CASES_TAC `b:A = a` THENL
 247    [DISJ2_TAC THEN UNDISCH_THEN `b:A = a` SUBST_ALL_TAC THEN
 248     EXISTS_TAC `K:(A)multiset` THEN ASM_MESON_TAC[MUNION_11]; DISJ1_TAC] THEN
 249   SUBGOAL_THEN `?M2. M1 = M2 munion (msing(a:A))` STRIP_ASSUME_TAC THENL
 250    [EXISTS_TAC `M1 mdiff (msing(a:A))` THEN
 251     MAP_EVERY MATCH_MP_TAC [MMEMBER_MDIFF; MUNION_INUNION] THEN
 252     UNDISCH_TAC `M0 munion (msing a) = M1 munion (msing(b:A))` THEN
 253     ASM_REWRITE_TAC[MEXTENSION; MUNION; MSING; mmember] THEN
 254     DISCH_THEN(MP_TAC o SPEC `a:A`) THEN ASM_REWRITE_TAC[] THEN
 255     ARITH_TAC; ALL_TAC] THEN
 256   EXISTS_TAC `M2 munion K:(A)multiset` THEN ASM_REWRITE_TAC[MUNION_AC] THEN
 257   REWRITE_TAC[morder] THEN
 258   MAP_EVERY EXISTS_TAC [`M2:(A)multiset`; `b:A`; `K:(A)multiset`] THEN
 259   UNDISCH_TAC `M0 munion msing (a:A) = M1 munion msing b` THEN
 260   ASM_REWRITE_TAC[MUNION_AC] THEN MESON_TAC[MUNION_AC; MUNION_11]);;
 261
 262 (* ------------------------------------------------------------------------- *)
 263 (* The sequence of lemmas from Tobias's paper.                               *)
 264 (* ------------------------------------------------------------------------- *)
 265
 266 let LEMMA_2_1 = prove
 267  (`(!M b:A. b << a /\ M IN WFP(morder(<<))
 268             ==> (M munion (msing b)) IN WFP(morder(<<))) /\
 269    M0 IN WFP(morder(<<)) /\
 270    (!M. morder(<<) M M0 ==> (M munion (msing a)) IN WFP(morder(<<)))
 271    ==> (M0 munion (msing a)) IN WFP(morder(<<))`,
 272   STRIP_TAC THEN REWRITE_TAC[IN] THEN MATCH_MP_TAC WFP_RULES THEN
 273   X_GEN_TAC `N:(A)multiset` THEN
 274   DISCH_THEN(DISJ_CASES_THEN MP_TAC o MATCH_MP LEMMA_2_0) THENL
 275    [ASM_MESON_TAC[IN]; REWRITE_TAC[LEFT_IMP_EXISTS_THM]] THEN
 276   SPEC_TAC(`N:(A)multiset`,`N:(A)multiset`) THEN
 277   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN
 278   MATCH_MP_TAC MULTISET_INDUCT THEN REPEAT STRIP_TAC THEN
 279   RULE_ASSUM_TAC(REWRITE_RULE[MUNION_ASSOC; MMEMBER_MUNION; MMEMBER_MSING]) THEN
 280   ASM_MESON_TAC[IN; MUNION_EMPTY]);;
 281
 282 let LEMMA_2_2 = prove
 283  (`(!M b. b << a /\ M IN WFP(morder(<<))
 284           ==> (M munion (msing b)) IN WFP(morder(<<)))
 285    ==> !M. M IN WFP(morder(<<)) ==> (M munion (msing a)) IN WFP(morder(<<))`,
 286   STRIP_TAC THEN MATCH_MP_TAC WFP_PART_INDUCT THEN
 287   REPEAT STRIP_TAC THEN MATCH_MP_TAC LEMMA_2_1 THEN ASM_REWRITE_TAC[]);;
 288
 289 let LEMMA_2_3 = prove
 290  (`WF(<<)
 291    ==> !a M. M IN WFP(morder(<<)) ==> (M munion (msing a)) IN WFP(morder(<<))`,
 292   REWRITE_TAC[WF_IND] THEN DISCH_THEN MATCH_MP_TAC THEN MESON_TAC[LEMMA_2_2]);;
 293
 294 let LEMMA_2_4 = prove
 295  (`WF(<<) ==> !M. M IN WFP(morder(<<))`,
 296   DISCH_TAC THEN MATCH_MP_TAC MULTISET_INDUCT THEN CONJ_TAC THENL
 297    [REWRITE_TAC[IN] THEN MATCH_MP_TAC WFP_RULES THEN
 298     REWRITE_TAC[morder; MUNION_MEMPTY];
 299     ASM_SIMP_TAC[LEMMA_2_3]]);;
 300
 301 (* ------------------------------------------------------------------------- *)
 302 (* Hence the final result.                                                   *)
 303 (* ------------------------------------------------------------------------- *)
 304
 305 let MORDER_WF = prove
 306  (`WF(<<) ==> WF(morder(<<))`,
 307   SIMP_TAC[WFP_WF; EXTENSION; IN_UNIV; LEMMA_2_4]);;