TFL/examples/Subst/Unify.ML
 author nipkow Fri Feb 07 14:15:35 1997 +0100 (1997-02-07) changeset 2597 8b523426e1a4 parent 2113 21266526ac42 permissions -rw-r--r--
Modified proofs due to added triv_forall_equality.
 paulson@2113 ` 1` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 2` ``` * This file defines a nested unification algorithm, then proves that it ``` paulson@2113 ` 3` ``` * terminates, then proves 2 correctness theorems: that when the algorithm ``` paulson@2113 ` 4` ``` * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution. ``` paulson@2113 ` 5` ``` * Although the proofs may seem long, they are actually quite direct, in that ``` paulson@2113 ` 6` ``` * the correctness and termination properties are not mingled as much as in ``` paulson@2113 ` 7` ``` * previous proofs of this algorithm. ``` paulson@2113 ` 8` ``` * ``` paulson@2113 ` 9` ``` * Our approach for nested recursive functions is as follows: ``` paulson@2113 ` 10` ``` * ``` paulson@2113 ` 11` ``` * 0. Prove the wellfoundedness of the termination relation. ``` paulson@2113 ` 12` ``` * 1. Prove the non-nested termination conditions. ``` paulson@2113 ` 13` ``` * 2. Eliminate (0) and (1) from the recursion equations and the ``` paulson@2113 ` 14` ``` * induction theorem. ``` paulson@2113 ` 15` ``` * 3. Prove the nested termination conditions by using the induction ``` paulson@2113 ` 16` ``` * theorem from (2) and by using the recursion equations from (2). ``` paulson@2113 ` 17` ``` * These are constrained by the nested termination conditions, but ``` paulson@2113 ` 18` ``` * things work out magically (by wellfoundedness of the termination ``` paulson@2113 ` 19` ``` * relation). ``` paulson@2113 ` 20` ``` * 4. Eliminate the nested TCs from the results of (2). ``` paulson@2113 ` 21` ``` * 5. Prove further correctness properties using the results of (4). ``` paulson@2113 ` 22` ``` * ``` paulson@2113 ` 23` ``` * Deeper nestings require iteration of steps (3) and (4). ``` paulson@2113 ` 24` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 25` paulson@2113 ` 26` ```(* This is just a wrapper for the definition mechanism. *) ``` paulson@2113 ` 27` ```local fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[]))); ``` paulson@2113 ` 28` ```in ``` paulson@2113 ` 29` ```fun Rfunc thy R eqs = ``` paulson@2113 ` 30` ``` let val read = term_of o cread thy; ``` paulson@2113 ` 31` ``` in Tfl.Rfunction thy (read R) (read eqs) ``` paulson@2113 ` 32` ``` end ``` paulson@2113 ` 33` ```end; ``` paulson@2113 ` 34` paulson@2113 ` 35` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 36` ``` * The algorithm. ``` paulson@2113 ` 37` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 38` ```val {theory,induction,rules,tcs} = ``` paulson@2113 ` 39` ```Rfunc Unify.thy "R" ``` paulson@2113 ` 40` ``` "(Unify(Const m, Const n) = (if (m=n) then Subst[] else Fail)) & \ ``` paulson@2113 ` 41` ```\ (Unify(Const m, Comb M N) = Fail) & \ ``` paulson@2113 ` 42` ```\ (Unify(Const m, Var v) = Subst[(v,Const m)]) & \ ``` paulson@2113 ` 43` ```\ (Unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])) & \ ``` paulson@2113 ` 44` ```\ (Unify(Comb M N, Const x) = Fail) & \ ``` paulson@2113 ` 45` ```\ (Unify(Comb M N, Var v) = (if (Var v <: Comb M N) then Fail \ ``` paulson@2113 ` 46` ```\ else Subst[(v,Comb M N)])) & \ ``` paulson@2113 ` 47` ```\ (Unify(Comb M1 N1, Comb M2 N2) = \ ``` paulson@2113 ` 48` ```\ (case Unify(M1,M2) \ ``` paulson@2113 ` 49` ```\ of Fail => Fail \ ``` paulson@2113 ` 50` ```\ | Subst theta => (case Unify(N1 <| theta, N2 <| theta) \ ``` paulson@2113 ` 51` ```\ of Fail => Fail \ ``` paulson@2113 ` 52` ```\ | Subst sigma => Subst (theta <> sigma))))"; ``` paulson@2113 ` 53` paulson@2113 ` 54` ```open Unify; ``` paulson@2113 ` 55` paulson@2113 ` 56` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 57` ``` * A slightly augmented strip_tac. ``` paulson@2113 ` 58` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 59` ```fun my_strip_tac i = ``` paulson@2113 ` 60` ``` CHANGED (strip_tac i ``` paulson@2113 ` 61` ``` THEN REPEAT ((etac exE ORELSE' etac conjE) i) ``` paulson@2113 ` 62` ``` THEN TRY (hyp_subst_tac i)); ``` paulson@2113 ` 63` paulson@2113 ` 64` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 65` ``` * A slightly augmented fast_tac for sets. It handles the case where the ``` paulson@2113 ` 66` ``` * top connective is "=". ``` paulson@2113 ` 67` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 68` ```fun my_fast_set_tac i = (TRY(rtac set_ext i) THEN fast_tac set_cs i); ``` paulson@2113 ` 69` paulson@2113 ` 70` paulson@2113 ` 71` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 72` ``` * Wellfoundedness of proper subset on finite sets. ``` paulson@2113 ` 73` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 74` ```goalw Unify.thy [R0_def] "wf(R0)"; ``` paulson@2113 ` 75` ```by (rtac ((wf_subset RS mp) RS mp) 1); ``` paulson@2113 ` 76` ```by (rtac wf_measure 1); ``` paulson@2113 ` 77` ```by(simp_tac(!simpset addsimps[measure_def,inv_image_def,symmetric less_def])1); ``` paulson@2113 ` 78` ```by (my_strip_tac 1); ``` paulson@2113 ` 79` ```by (forward_tac[ssubset_card] 1); ``` paulson@2113 ` 80` ```by (fast_tac set_cs 1); ``` paulson@2113 ` 81` ```val wf_R0 = result(); ``` paulson@2113 ` 82` paulson@2113 ` 83` paulson@2113 ` 84` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 85` ``` * Tactic for selecting and working on the first projection of R. ``` paulson@2113 ` 86` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 87` ```fun R0_tac thms i = ``` paulson@2113 ` 88` ``` (simp_tac (!simpset addsimps (thms@[R_def,lex_prod_def, ``` paulson@2113 ` 89` ``` measure_def,inv_image_def,point_to_prod_def])) i THEN ``` paulson@2113 ` 90` ``` REPEAT (rtac exI i) THEN ``` paulson@2113 ` 91` ``` REPEAT ((rtac conjI THEN' rtac refl) i) THEN ``` paulson@2113 ` 92` ``` rtac disjI1 i THEN ``` paulson@2113 ` 93` ``` simp_tac (!simpset addsimps [R0_def,finite_vars_of]) i); ``` paulson@2113 ` 94` paulson@2113 ` 95` paulson@2113 ` 96` paulson@2113 ` 97` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 98` ``` * Tactic for selecting and working on the second projection of R. ``` paulson@2113 ` 99` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 100` ```fun R1_tac thms i = ``` paulson@2113 ` 101` ``` (simp_tac (!simpset addsimps (thms@[R_def,lex_prod_def, ``` paulson@2113 ` 102` ``` measure_def,inv_image_def,point_to_prod_def])) i THEN ``` paulson@2113 ` 103` ``` REPEAT (rtac exI i) THEN ``` paulson@2113 ` 104` ``` REPEAT ((rtac conjI THEN' rtac refl) i) THEN ``` paulson@2113 ` 105` ``` rtac disjI2 i THEN ``` paulson@2113 ` 106` ``` asm_simp_tac (!simpset addsimps [R1_def,rprod_def]) i); ``` paulson@2113 ` 107` paulson@2113 ` 108` paulson@2113 ` 109` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 110` ``` * The non-nested TC plus the wellfoundedness of R. ``` paulson@2113 ` 111` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 112` ```Tfl.tgoalw Unify.thy [] rules; ``` paulson@2113 ` 113` ```by (rtac conjI 1); ``` paulson@2113 ` 114` ```(* TC *) ``` paulson@2113 ` 115` ```by (my_strip_tac 1); ``` paulson@2113 ` 116` ```by (cut_facts_tac [monotone_vars_of] 1); ``` paulson@2113 ` 117` ```by (asm_full_simp_tac(!simpset addsimps [subseteq_iff_subset_eq]) 1); ``` paulson@2113 ` 118` ```by (etac disjE 1); ``` paulson@2113 ` 119` ```by (R0_tac[] 1); ``` paulson@2113 ` 120` ```by (R1_tac[] 1); ``` paulson@2113 ` 121` ```by (simp_tac ``` paulson@2113 ` 122` ``` (!simpset addsimps [measure_def,inv_image_def,less_eq,less_add_Suc1]) 1); ``` paulson@2113 ` 123` paulson@2113 ` 124` ```(* Wellfoundedness of R *) ``` paulson@2113 ` 125` ```by (simp_tac (!simpset addsimps [Unify.R_def,Unify.R1_def]) 1); ``` paulson@2113 ` 126` ```by (REPEAT (resolve_tac [wf_inv_image,wf_lex_prod,wf_R0, ``` paulson@2113 ` 127` ``` wf_rel_prod, wf_measure] 1)); ``` paulson@2113 ` 128` ```val tc0 = result(); ``` paulson@2113 ` 129` paulson@2113 ` 130` paulson@2113 ` 131` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 132` ``` * Eliminate tc0 from the recursion equations and the induction theorem. ``` paulson@2113 ` 133` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 134` ```val [tc,wfr] = Prim.Rules.CONJUNCTS tc0; ``` paulson@2113 ` 135` ```val rules1 = implies_intr_hyps rules; ``` paulson@2113 ` 136` ```val rules2 = wfr RS rules1; ``` paulson@2113 ` 137` paulson@2113 ` 138` ```val [a,b,c,d,e,f,g] = Prim.Rules.CONJUNCTS rules2; ``` paulson@2113 ` 139` ```val g' = tc RS (g RS mp); ``` paulson@2113 ` 140` ```val rules4 = standard (Prim.Rules.LIST_CONJ[a,b,c,d,e,f,g']); ``` paulson@2113 ` 141` paulson@2113 ` 142` ```val induction1 = implies_intr_hyps induction; ``` paulson@2113 ` 143` ```val induction2 = wfr RS induction1; ``` paulson@2113 ` 144` ```val induction3 = tc RS induction2; ``` paulson@2113 ` 145` paulson@2113 ` 146` ```val induction4 = standard ``` paulson@2113 ` 147` ``` (rewrite_rule[fst_conv RS eq_reflection, snd_conv RS eq_reflection] ``` paulson@2113 ` 148` ``` (induction3 RS (read_instantiate_sg (sign_of theory) ``` paulson@2113 ` 149` ``` [("x","%p. Phi (fst p) (snd p)")] spec))); ``` paulson@2113 ` 150` paulson@2113 ` 151` paulson@2113 ` 152` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 153` ``` * Some theorems about transitivity of WF combinators. Only the last ``` paulson@2113 ` 154` ``` * (transR) is used, in the proof of termination. The others are generic and ``` paulson@2113 ` 155` ``` * should maybe go somewhere. ``` paulson@2113 ` 156` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 157` ```goalw WF1.thy [trans_def,lex_prod_def,mem_Collect_eq RS eq_reflection] ``` paulson@2113 ` 158` ``` "trans R1 & trans R2 --> trans (R1 ** R2)"; ``` paulson@2113 ` 159` ```by (my_strip_tac 1); ``` paulson@2113 ` 160` ```by (res_inst_tac [("x","a")] exI 1); ``` paulson@2113 ` 161` ```by (res_inst_tac [("x","a'a")] exI 1); ``` paulson@2113 ` 162` ```by (res_inst_tac [("x","b")] exI 1); ``` paulson@2113 ` 163` ```by (res_inst_tac [("x","b'a")] exI 1); ``` paulson@2113 ` 164` ```by (REPEAT (rewrite_tac [Pair_eq RS eq_reflection] THEN my_strip_tac 1)); ``` paulson@2113 ` 165` ```by (Simp_tac 1); ``` paulson@2113 ` 166` ```by (REPEAT (etac disjE 1)); ``` paulson@2113 ` 167` ```by (rtac disjI1 1); ``` paulson@2113 ` 168` ```by (ALLGOALS (fast_tac set_cs)); ``` paulson@2113 ` 169` ```val trans_lex_prod = result() RS mp; ``` paulson@2113 ` 170` paulson@2113 ` 171` paulson@2113 ` 172` ```goalw WF1.thy [trans_def,rprod_def,mem_Collect_eq RS eq_reflection] ``` paulson@2113 ` 173` ``` "trans R1 & trans R2 --> trans (rprod R1 R2)"; ``` paulson@2113 ` 174` ```by (my_strip_tac 1); ``` paulson@2113 ` 175` ```by (res_inst_tac [("x","a")] exI 1); ``` paulson@2113 ` 176` ```by (res_inst_tac [("x","a'a")] exI 1); ``` paulson@2113 ` 177` ```by (res_inst_tac [("x","b")] exI 1); ``` paulson@2113 ` 178` ```by (res_inst_tac [("x","b'a")] exI 1); ``` paulson@2113 ` 179` ```by (REPEAT (rewrite_tac [Pair_eq RS eq_reflection] THEN my_strip_tac 1)); ``` paulson@2113 ` 180` ```by (Simp_tac 1); ``` paulson@2113 ` 181` ```by (fast_tac set_cs 1); ``` paulson@2113 ` 182` ```val trans_rprod = result() RS mp; ``` paulson@2113 ` 183` paulson@2113 ` 184` paulson@2113 ` 185` ```goalw Unify.thy [trans_def,inv_image_def,mem_Collect_eq RS eq_reflection] ``` paulson@2113 ` 186` ``` "trans r --> trans (inv_image r f)"; ``` paulson@2113 ` 187` ```by (rewrite_tac [fst_conv RS eq_reflection, snd_conv RS eq_reflection]); ``` paulson@2113 ` 188` ```by (fast_tac set_cs 1); ``` paulson@2113 ` 189` ```val trans_inv_image = result() RS mp; ``` paulson@2113 ` 190` paulson@2113 ` 191` ```goalw Unify.thy [R0_def, trans_def, mem_Collect_eq RS eq_reflection] ``` paulson@2113 ` 192` ``` "trans R0"; ``` paulson@2113 ` 193` ```by (rewrite_tac [fst_conv RS eq_reflection,snd_conv RS eq_reflection, ``` paulson@2113 ` 194` ``` ssubset_def, set_eq_subset RS eq_reflection]); ``` paulson@2113 ` 195` ```by (fast_tac set_cs 1); ``` paulson@2113 ` 196` ```val trans_R0 = result(); ``` paulson@2113 ` 197` paulson@2113 ` 198` ```goalw Unify.thy [R_def,R1_def,measure_def] "trans R"; ``` paulson@2113 ` 199` ```by (REPEAT (resolve_tac[trans_inv_image,trans_lex_prod,conjI, trans_R0, ``` paulson@2113 ` 200` ``` trans_rprod, trans_inv_image, trans_trancl] 1)); ``` paulson@2113 ` 201` ```val transR = result(); ``` paulson@2113 ` 202` paulson@2113 ` 203` paulson@2113 ` 204` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 205` ``` * The following lemma is used in the last step of the termination proof for ``` paulson@2113 ` 206` ``` * the nested call in Unify. Loosely, it says that R doesn't care so much ``` paulson@2113 ` 207` ``` * about term structure. ``` paulson@2113 ` 208` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 209` ```goalw Unify.thy [R_def,lex_prod_def, inv_image_def,point_to_prod_def] ``` paulson@2113 ` 210` ``` "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : R --> \ ``` paulson@2113 ` 211` ``` \ ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : R"; ``` paulson@2113 ` 212` ```by (Simp_tac 1); ``` paulson@2113 ` 213` ```by (rtac conjI 1); ``` paulson@2113 ` 214` ```by (strip_tac 1); ``` paulson@2113 ` 215` ```by (rtac disjI1 1); ``` paulson@2113 ` 216` ```by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \ ``` paulson@2113 ` 217` ``` \ (vars_of D Un vars_of E Un vars_of F)) = \ ``` paulson@2113 ` 218` ``` \ (vars_of A Un (vars_of B Un vars_of C) Un \ ``` paulson@2113 ` 219` ``` \ (vars_of D Un (vars_of E Un vars_of F)))" 1); ``` paulson@2113 ` 220` ```by (my_fast_set_tac 2); ``` paulson@2113 ` 221` ```by (Asm_simp_tac 1); ``` paulson@2113 ` 222` ```by (strip_tac 1); ``` paulson@2113 ` 223` ```by (rtac disjI2 1); ``` paulson@2113 ` 224` ```by (etac conjE 1); ``` paulson@2113 ` 225` ```by (Asm_simp_tac 1); ``` paulson@2113 ` 226` ```by (rtac conjI 1); ``` paulson@2113 ` 227` ```by (my_fast_set_tac 1); ``` paulson@2113 ` 228` ```by (asm_full_simp_tac (!simpset addsimps [R1_def, measure_def, rprod_def, ``` paulson@2113 ` 229` ``` less_eq, inv_image_def,add_assoc]) 1); ``` paulson@2113 ` 230` ```val Rassoc = result() RS mp; ``` paulson@2113 ` 231` paulson@2113 ` 232` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 233` ``` * Rewriting support. ``` paulson@2113 ` 234` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 235` paulson@2113 ` 236` ```val termin_ss = (!simpset addsimps (srange_iff::(subst_rews@al_rews))); ``` paulson@2113 ` 237` paulson@2113 ` 238` paulson@2113 ` 239` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 240` ``` * This lemma proves the nested termination condition for the base cases ``` paulson@2113 ` 241` ``` * 3, 4, and 6. It's a clumsy formulation (requiring two conjuncts, each with ``` paulson@2113 ` 242` ``` * exactly the same proof) of a more general theorem. ``` paulson@2113 ` 243` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 244` ```goal theory "(~(Var x <: M)) --> [(x, M)] = theta --> \ ``` paulson@2113 ` 245` ```\ (! N1 N2. (((N1 <| theta, N2 <| theta), (Comb M N1, Comb (Var x) N2)) : R) \ ``` paulson@2113 ` 246` ```\ & (((N1 <| theta, N2 <| theta), (Comb(Var x) N1, Comb M N2)) : R))"; ``` paulson@2113 ` 247` ```by (my_strip_tac 1); ``` paulson@2113 ` 248` ```by (case_tac "Var x = M" 1); ``` paulson@2113 ` 249` ```by (hyp_subst_tac 1); ``` paulson@2113 ` 250` ```by (case_tac "x:(vars_of N1 Un vars_of N2)" 1); ``` paulson@2113 ` 251` ```let val case1 = ``` paulson@2113 ` 252` ``` EVERY1[R1_tac[id_subst_lemma], rtac conjI, my_fast_set_tac, ``` paulson@2113 ` 253` ``` REPEAT o (rtac exI), REPEAT o (rtac conjI THEN' rtac refl), ``` paulson@2113 ` 254` ``` simp_tac (!simpset addsimps [measure_def,inv_image_def,less_eq])]; ``` paulson@2113 ` 255` ```in by (rtac conjI 1); ``` paulson@2113 ` 256` ``` by case1; ``` paulson@2113 ` 257` ``` by case1 ``` paulson@2113 ` 258` ```end; ``` paulson@2113 ` 259` paulson@2113 ` 260` ```let val case2 = ``` paulson@2113 ` 261` ``` EVERY1[R0_tac[id_subst_lemma], ``` paulson@2113 ` 262` ``` simp_tac (!simpset addsimps [ssubset_def,set_eq_subset]), ``` paulson@2113 ` 263` ``` fast_tac set_cs] ``` paulson@2113 ` 264` ```in by (rtac conjI 1); ``` paulson@2113 ` 265` ``` by case2; ``` paulson@2113 ` 266` ``` by case2 ``` paulson@2113 ` 267` ```end; ``` paulson@2113 ` 268` paulson@2113 ` 269` ```let val case3 = ``` paulson@2113 ` 270` ``` EVERY1 [R0_tac[], ``` paulson@2113 ` 271` ``` cut_inst_tac [("s2","[(x, M)]"), ("v2", "x"), ("t2","N1")] Var_elim] ``` paulson@2113 ` 272` ``` THEN ALLGOALS(asm_simp_tac(termin_ss addsimps [vars_iff_occseq])) ``` paulson@2113 ` 273` ``` THEN cut_inst_tac [("s2","[(x, M)]"),("v2", "x"), ("t2","N2")] Var_elim 1 ``` paulson@2113 ` 274` ``` THEN ALLGOALS(asm_simp_tac(termin_ss addsimps [vars_iff_occseq])) ``` paulson@2113 ` 275` ``` THEN EVERY1 [simp_tac (HOL_ss addsimps [ssubset_def]), ``` paulson@2113 ` 276` ``` rtac conjI, simp_tac (HOL_ss addsimps [subset_iff]), ``` paulson@2113 ` 277` ``` my_strip_tac, etac UnE, dtac Var_intro] ``` paulson@2113 ` 278` ``` THEN dtac Var_intro 2 ``` paulson@2113 ` 279` ``` THEN ALLGOALS (asm_full_simp_tac (termin_ss addsimps [set_eq_subset])) ``` paulson@2113 ` 280` ``` THEN TRYALL (fast_tac set_cs) ``` paulson@2113 ` 281` ```in ``` paulson@2113 ` 282` ``` by (rtac conjI 1); ``` paulson@2113 ` 283` ``` by case3; ``` paulson@2113 ` 284` ``` by case3 ``` paulson@2113 ` 285` ```end; ``` paulson@2113 ` 286` ```val var_elimR = result() RS mp RS mp RS spec RS spec; ``` paulson@2113 ` 287` paulson@2113 ` 288` paulson@2113 ` 289` ```val Some{nchotomy = subst_nchotomy,...} = assoc(!datatypes,"subst"); ``` paulson@2113 ` 290` paulson@2113 ` 291` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 292` ``` * Do a case analysis on something of type 'a subst. ``` paulson@2113 ` 293` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 294` paulson@2113 ` 295` ```fun Subst_case_tac theta = ``` paulson@2113 ` 296` ```(cut_inst_tac theta (standard (Prim.Rules.SPEC_ALL subst_nchotomy)) 1 ``` paulson@2113 ` 297` ``` THEN etac disjE 1 ``` paulson@2113 ` 298` ``` THEN rotate_tac ~1 1 ``` paulson@2113 ` 299` ``` THEN Asm_full_simp_tac 1 ``` paulson@2113 ` 300` ``` THEN etac exE 1 ``` paulson@2113 ` 301` ``` THEN rotate_tac ~1 1 ``` paulson@2113 ` 302` ``` THEN Asm_full_simp_tac 1); ``` paulson@2113 ` 303` paulson@2113 ` 304` paulson@2113 ` 305` ```goals_limit := 1; ``` paulson@2113 ` 306` paulson@2113 ` 307` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 308` ``` * The nested TC. Proved by recursion induction. ``` paulson@2113 ` 309` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 310` ```goalw_cterm [] ``` paulson@2113 ` 311` ``` (hd(tl(tl(map (cterm_of (sign_of theory) o USyntax.mk_prop) tcs)))); ``` paulson@2113 ` 312` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 313` ``` * The extracted TC needs the scope of its quantifiers adjusted, so our ``` paulson@2113 ` 314` ``` * first step is to restrict the scopes of N1 and N2. ``` paulson@2113 ` 315` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 316` ```by (subgoal_tac "!M1 M2 theta. \ ``` paulson@2113 ` 317` ``` \ Unify (M1, M2) = Subst theta --> \ ``` paulson@2113 ` 318` ``` \ (!N1 N2. ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R)" 1); ``` paulson@2113 ` 319` ```by (fast_tac HOL_cs 1); ``` paulson@2113 ` 320` ```by (rtac allI 1); ``` paulson@2113 ` 321` ```by (rtac allI 1); ``` paulson@2113 ` 322` ```(* Apply induction *) ``` paulson@2113 ` 323` ```by (res_inst_tac [("xa","M1"),("x","M2")] ``` paulson@2113 ` 324` ``` (standard (induction4 RS mp RS spec RS spec)) 1); ``` paulson@2113 ` 325` ```by (simp_tac (!simpset addsimps (rules4::(subst_rews@al_rews)) ``` paulson@2113 ` 326` ``` setloop (split_tac [expand_if])) 1); ``` paulson@2113 ` 327` ```(* 1 *) ``` paulson@2113 ` 328` ```by (rtac conjI 1); ``` paulson@2113 ` 329` ```by (my_strip_tac 1); ``` paulson@2113 ` 330` ```by (R1_tac[subst_Nil] 1); ``` paulson@2113 ` 331` ```by (REPEAT (rtac exI 1) THEN REPEAT ((rtac conjI THEN' rtac refl) 1)); ``` paulson@2113 ` 332` ```by (simp_tac (!simpset addsimps [measure_def,inv_image_def,less_eq]) 1); ``` paulson@2113 ` 333` paulson@2113 ` 334` ```(* 3 *) ``` paulson@2113 ` 335` ```by (rtac conjI 1); ``` paulson@2113 ` 336` ```by (my_strip_tac 1); ``` paulson@2113 ` 337` ```by (rtac (Prim.Rules.CONJUNCT1 var_elimR) 1); ``` paulson@2113 ` 338` ```by (Simp_tac 1); ``` paulson@2113 ` 339` ```by (rtac refl 1); ``` paulson@2113 ` 340` paulson@2113 ` 341` ```(* 4 *) ``` paulson@2113 ` 342` ```by (rtac conjI 1); ``` paulson@2113 ` 343` ```by (strip_tac 1); ``` paulson@2113 ` 344` ```by (rtac (Prim.Rules.CONJUNCT2 var_elimR) 1); ``` paulson@2113 ` 345` ```by (assume_tac 1); ``` paulson@2113 ` 346` ```by (rtac refl 1); ``` paulson@2113 ` 347` paulson@2113 ` 348` ```(* 6 *) ``` paulson@2113 ` 349` ```by (rtac conjI 1); ``` paulson@2113 ` 350` ```by (rewrite_tac [symmetric (occs_Comb RS eq_reflection)]); ``` paulson@2113 ` 351` ```by (my_strip_tac 1); ``` paulson@2113 ` 352` ```by (rtac (Prim.Rules.CONJUNCT1 var_elimR) 1); ``` paulson@2113 ` 353` ```by (Asm_simp_tac 1); ``` paulson@2113 ` 354` ```by (rtac refl 1); ``` paulson@2113 ` 355` paulson@2113 ` 356` ```(* 7 *) ``` paulson@2113 ` 357` ```by (REPEAT (rtac allI 1)); ``` paulson@2113 ` 358` ```by (rtac impI 1); ``` paulson@2113 ` 359` ```by (etac conjE 1); ``` paulson@2113 ` 360` ```by (Subst_case_tac [("v","Unify(M1, M2)")]); ``` nipkow@2597 ` 361` ```by (rename_tac "theta" 1); ``` paulson@2113 ` 362` paulson@2113 ` 363` ```by (Subst_case_tac [("v","Unify(N1 <| theta, N2 <| theta)")]); ``` nipkow@2597 ` 364` ```by (rename_tac "sigma" 1); ``` paulson@2113 ` 365` ```by (REPEAT (rtac allI 1)); ``` nipkow@2597 ` 366` ```by (rename_tac "P Q" 1); ``` paulson@2113 ` 367` ```by (simp_tac (HOL_ss addsimps [subst_comp]) 1); ``` paulson@2113 ` 368` ```by(rtac(rewrite_rule[trans_def] transR RS spec RS spec RS spec RS mp RS mp) 1); ``` paulson@2113 ` 369` ```by (fast_tac HOL_cs 1); ``` paulson@2113 ` 370` ```by (simp_tac (HOL_ss addsimps [symmetric (subst_Comb RS eq_reflection)]) 1); ``` paulson@2113 ` 371` ```by (subgoal_tac "((Comb N1 P <| theta, Comb N2 Q <| theta), \ ``` paulson@2113 ` 372` ``` \ (Comb M1 (Comb N1 P), Comb M2 (Comb N2 Q))) :R" 1); ``` paulson@2113 ` 373` ```by (asm_simp_tac HOL_ss 2); ``` paulson@2113 ` 374` paulson@2113 ` 375` ```by (rtac Rassoc 1); ``` paulson@2113 ` 376` ```by (assume_tac 1); ``` paulson@2113 ` 377` ```val Unify_TC2 = result(); ``` paulson@2113 ` 378` paulson@2113 ` 379` paulson@2113 ` 380` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 381` ``` * Now for elimination of nested TC from rules and induction. This step ``` paulson@2113 ` 382` ``` * would be easier if "rewrite_rule" used context. ``` paulson@2113 ` 383` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 384` ```goal theory ``` paulson@2113 ` 385` ``` "(Unify (Comb M1 N1, Comb M2 N2) = \ ``` paulson@2113 ` 386` ```\ (case Unify (M1, M2) of Fail => Fail \ ``` paulson@2113 ` 387` ```\ | Subst theta => \ ``` paulson@2113 ` 388` ```\ (case if ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R \ ``` paulson@2113 ` 389` ```\ then Unify (N1 <| theta, N2 <| theta) else @ z. True of \ ``` paulson@2113 ` 390` ```\ Fail => Fail | Subst sigma => Subst (theta <> sigma)))) \ ``` paulson@2113 ` 391` ```\ = \ ``` paulson@2113 ` 392` ```\ (Unify (Comb M1 N1, Comb M2 N2) = \ ``` paulson@2113 ` 393` ```\ (case Unify (M1, M2) \ ``` paulson@2113 ` 394` ```\ of Fail => Fail \ ``` paulson@2113 ` 395` ```\ | Subst theta => (case Unify (N1 <| theta, N2 <| theta) \ ``` paulson@2113 ` 396` ```\ of Fail => Fail \ ``` paulson@2113 ` 397` ```\ | Subst sigma => Subst (theta <> sigma))))"; ``` paulson@2113 ` 398` ```by (cut_inst_tac [("v","Unify(M1, M2)")] ``` paulson@2113 ` 399` ``` (standard (Prim.Rules.SPEC_ALL subst_nchotomy)) 1); ``` paulson@2113 ` 400` ```by (etac disjE 1); ``` paulson@2113 ` 401` ```by (Asm_simp_tac 1); ``` paulson@2113 ` 402` ```by (etac exE 1); ``` paulson@2113 ` 403` ```by (Asm_simp_tac 1); ``` paulson@2113 ` 404` ```by (cut_inst_tac ``` paulson@2113 ` 405` ``` [("x","list"), ("xb","N1"), ("xa","N2"),("xc","M2"), ("xd","M1")] ``` paulson@2113 ` 406` ``` (standard(Unify_TC2 RS spec RS spec RS spec RS spec RS spec)) 1); ``` paulson@2113 ` 407` ```by (Asm_full_simp_tac 1); ``` paulson@2113 ` 408` ```val Unify_rec_simpl = result() RS eq_reflection; ``` paulson@2113 ` 409` paulson@2113 ` 410` ```val Unify_rules = rewrite_rule[Unify_rec_simpl] rules4; ``` paulson@2113 ` 411` paulson@2113 ` 412` paulson@2113 ` 413` ```goal theory ``` paulson@2113 ` 414` ``` "(! M1 N1 M2 N2. \ ``` paulson@2113 ` 415` ```\ (! theta. \ ``` paulson@2113 ` 416` ```\ Unify (M1, M2) = Subst theta --> \ ``` paulson@2113 ` 417` ```\ ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R --> \ ``` paulson@2113 ` 418` ```\ ?Phi (N1 <| theta) (N2 <| theta)) & ?Phi M1 M2 --> \ ``` paulson@2113 ` 419` ```\ ?Phi (Comb M1 N1) (Comb M2 N2)) \ ``` paulson@2113 ` 420` ```\ = \ ``` paulson@2113 ` 421` ```\ (! M1 N1 M2 N2. \ ``` paulson@2113 ` 422` ```\ (! theta. \ ``` paulson@2113 ` 423` ```\ Unify (M1, M2) = Subst theta --> \ ``` paulson@2113 ` 424` ```\ ?Phi (N1 <| theta) (N2 <| theta)) & ?Phi M1 M2 --> \ ``` paulson@2113 ` 425` ```\ ?Phi (Comb M1 N1) (Comb M2 N2))"; ``` paulson@2113 ` 426` ```by (simp_tac (HOL_ss addsimps [Unify_TC2]) 1); ``` paulson@2113 ` 427` ```val Unify_induction = rewrite_rule[result() RS eq_reflection] induction4; ``` paulson@2113 ` 428` paulson@2113 ` 429` paulson@2113 ` 430` paulson@2113 ` 431` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 432` ``` * Correctness. Notice that idempotence is not needed to prove that the ``` paulson@2113 ` 433` ``` * algorithm terminates and is not needed to prove the algorithm correct, ``` paulson@2113 ` 434` ``` * if you are only interested in an MGU. This is in contrast to the ``` paulson@2113 ` 435` ``` * approach of M&W, who used idempotence and MGU-ness in the termination proof. ``` paulson@2113 ` 436` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 437` paulson@2113 ` 438` ```goal theory "!theta. Unify (P,Q) = Subst theta --> MGUnifier theta P Q"; ``` paulson@2113 ` 439` ```by (res_inst_tac [("xa","P"),("x","Q")] ``` paulson@2113 ` 440` ``` (standard (Unify_induction RS mp RS spec RS spec)) 1); ``` paulson@2113 ` 441` ```by (simp_tac (!simpset addsimps [Unify_rules] ``` paulson@2113 ` 442` ``` setloop (split_tac [expand_if])) 1); ``` paulson@2113 ` 443` ```(*1*) ``` paulson@2113 ` 444` ```by (rtac conjI 1); ``` paulson@2113 ` 445` ```by (REPEAT (rtac allI 1)); ``` paulson@2113 ` 446` ```by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1); ``` paulson@2113 ` 447` ```by (my_strip_tac 1); ``` paulson@2113 ` 448` ```by (rtac MoreGen_Nil 1); ``` paulson@2113 ` 449` paulson@2113 ` 450` ```(*3*) ``` paulson@2113 ` 451` ```by (rtac conjI 1); ``` paulson@2113 ` 452` ```by (my_strip_tac 1); ``` paulson@2113 ` 453` ```by (rtac (mgu_sym RS iffD1) 1); ``` paulson@2113 ` 454` ```by (rtac MGUnifier_Var 1); ``` paulson@2113 ` 455` ```by (Simp_tac 1); ``` paulson@2113 ` 456` paulson@2113 ` 457` ```(*4*) ``` paulson@2113 ` 458` ```by (rtac conjI 1); ``` paulson@2113 ` 459` ```by (my_strip_tac 1); ``` paulson@2113 ` 460` ```by (rtac MGUnifier_Var 1); ``` paulson@2113 ` 461` ```by (assume_tac 1); ``` paulson@2113 ` 462` paulson@2113 ` 463` ```(*6*) ``` paulson@2113 ` 464` ```by (rtac conjI 1); ``` paulson@2113 ` 465` ```by (rewrite_tac NNF_rews); ``` paulson@2113 ` 466` ```by (my_strip_tac 1); ``` paulson@2113 ` 467` ```by (rtac (mgu_sym RS iffD1) 1); ``` paulson@2113 ` 468` ```by (rtac MGUnifier_Var 1); ``` paulson@2113 ` 469` ```by (Asm_simp_tac 1); ``` paulson@2113 ` 470` paulson@2113 ` 471` ```(*7*) ``` paulson@2113 ` 472` ```by (safe_tac HOL_cs); ``` paulson@2113 ` 473` ```by (Subst_case_tac [("v","Unify(M1, M2)")]); ``` paulson@2113 ` 474` ```by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]); ``` paulson@2113 ` 475` ```by (hyp_subst_tac 1); ``` paulson@2113 ` 476` ```by (asm_full_simp_tac(HOL_ss addsimps [MGUnifier_def,Unifier_def])1); ``` paulson@2113 ` 477` ```by (asm_simp_tac (!simpset addsimps [subst_comp]) 1); (* It's a unifier.*) ``` paulson@2113 ` 478` paulson@2113 ` 479` ```by (safe_tac HOL_cs); ``` nipkow@2597 ` 480` ```by (rename_tac "theta sigma gamma" 1); ``` paulson@2113 ` 481` paulson@2113 ` 482` ```by (rewrite_tac [MoreGeneral_def]); ``` paulson@2113 ` 483` ```by (rotate_tac ~3 1); ``` paulson@2113 ` 484` ```by (eres_inst_tac [("x","gamma")] allE 1); ``` paulson@2113 ` 485` ```by (Asm_full_simp_tac 1); ``` paulson@2113 ` 486` ```by (etac exE 1); ``` nipkow@2597 ` 487` ```by (rename_tac "delta" 1); ``` paulson@2113 ` 488` ```by (eres_inst_tac [("x","delta")] allE 1); ``` paulson@2113 ` 489` ```by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1); ``` paulson@2113 ` 490` ```by (dtac mp 1); ``` paulson@2113 ` 491` ```by (atac 1); ``` paulson@2113 ` 492` ```by (etac exE 1); ``` nipkow@2597 ` 493` ```by (rename_tac "rho" 1); ``` paulson@2113 ` 494` paulson@2113 ` 495` ```by (rtac exI 1); ``` paulson@2113 ` 496` ```by (rtac subst_trans 1); ``` paulson@2113 ` 497` ```by (assume_tac 1); ``` paulson@2113 ` 498` paulson@2113 ` 499` ```by (rtac subst_trans 1); ``` paulson@2113 ` 500` ```by (rtac (comp_assoc RS subst_sym) 2); ``` paulson@2113 ` 501` ```by (rtac subst_cong 1); ``` paulson@2113 ` 502` ```by (rtac (refl RS subst_refl) 1); ``` paulson@2113 ` 503` ```by (assume_tac 1); ``` paulson@2113 ` 504` paulson@2113 ` 505` ```by (asm_full_simp_tac (!simpset addsimps [subst_eq_iff,subst_comp]) 1); ``` paulson@2113 ` 506` ```by (forw_inst_tac [("x","N1")] spec 1); ``` paulson@2113 ` 507` ```by (dres_inst_tac [("x","N2")] spec 1); ``` paulson@2113 ` 508` ```by (Asm_full_simp_tac 1); ``` paulson@2113 ` 509` ```val Unify_gives_MGU = standard(result() RS spec RS mp); ``` paulson@2113 ` 510` paulson@2113 ` 511` paulson@2113 ` 512` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 513` ``` * Unify returns idempotent substitutions, when it succeeds. ``` paulson@2113 ` 514` ``` *---------------------------------------------------------------------------*) ``` paulson@2113 ` 515` ```goal theory "!theta. Unify (P,Q) = Subst theta --> Idem theta"; ``` paulson@2113 ` 516` ```by (res_inst_tac [("xa","P"),("x","Q")] ``` paulson@2113 ` 517` ``` (standard (Unify_induction RS mp RS spec RS spec)) 1); ``` paulson@2113 ` 518` ```(* Blows away all base cases automatically *) ``` paulson@2113 ` 519` ```by (simp_tac (!simpset addsimps [Unify_rules,Idem_Nil,Var_Idem] ``` paulson@2113 ` 520` ``` setloop (split_tac [expand_if])) 1); ``` paulson@2113 ` 521` paulson@2113 ` 522` ```(*7*) ``` paulson@2113 ` 523` ```by (safe_tac HOL_cs); ``` paulson@2113 ` 524` ```by (Subst_case_tac [("v","Unify(M1, M2)")]); ``` paulson@2113 ` 525` ```by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]); ``` paulson@2113 ` 526` ```by (hyp_subst_tac 1); ``` paulson@2113 ` 527` ```by prune_params_tac; ``` nipkow@2597 ` 528` ```by (rename_tac "theta sigma" 1); ``` paulson@2113 ` 529` paulson@2113 ` 530` ```by (dtac Unify_gives_MGU 1); ``` paulson@2113 ` 531` ```by (dtac Unify_gives_MGU 1); ``` paulson@2113 ` 532` ```by (rewrite_tac [MGUnifier_def]); ``` paulson@2113 ` 533` ```by (my_strip_tac 1); ``` paulson@2113 ` 534` ```by (rtac Idem_comp 1); ``` paulson@2113 ` 535` ```by (atac 1); ``` paulson@2113 ` 536` ```by (atac 1); ``` paulson@2113 ` 537` paulson@2113 ` 538` ```by (my_strip_tac 1); ``` paulson@2113 ` 539` ```by (eres_inst_tac [("x","q")] allE 1); ``` paulson@2113 ` 540` ```by (Asm_full_simp_tac 1); ``` paulson@2113 ` 541` ```by (rewrite_tac [MoreGeneral_def]); ``` paulson@2113 ` 542` ```by (my_strip_tac 1); ``` paulson@2113 ` 543` ```by (asm_full_simp_tac(termin_ss addsimps [subst_eq_iff,subst_comp,Idem_def])1); ``` paulson@2113 ` 544` ```val Unify_gives_Idem = result() RS spec RS mp; ``` paulson@2113 ` 545` paulson@2113 ` 546` paulson@2113 ` 547` paulson@2113 ` 548` ```(*--------------------------------------------------------------------------- ``` paulson@2113 ` 549` ``` * Exercise. The given algorithm is a bit inelegant. What about the ``` paulson@2113 ` 550` ``` * following "improvement", which adds a few recursive calls in former ``` paulson@2113 ` 551` ``` * base cases? It seems that the termination relation needs another ``` paulson@2113 ` 552` ``` * case in the lexico. product. ``` paulson@2113 ` 553` paulson@2113 ` 554` ```val {theory,induction,rules,tcs,typechecks} = ``` paulson@2113 ` 555` ```Rfunc Unify.thy ?? ``` paulson@2113 ` 556` ``` `(Unify(Const m, Const n) = (if (m=n) then Subst[] else Fail)) & ``` paulson@2113 ` 557` ``` (Unify(Const m, Comb M N) = Fail) & ``` paulson@2113 ` 558` ``` (Unify(Const m, Var v) = Unify(Var v, Const m)) & ``` paulson@2113 ` 559` ``` (Unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])) & ``` paulson@2113 ` 560` ``` (Unify(Comb M N, Const x) = Fail) & ``` paulson@2113 ` 561` ``` (Unify(Comb M N, Var v) = Unify(Var v, Comb M N)) & ``` paulson@2113 ` 562` ``` (Unify(Comb M1 N1, Comb M2 N2) = ``` paulson@2113 ` 563` ``` (case Unify(M1,M2) ``` paulson@2113 ` 564` ``` of Fail => Fail ``` paulson@2113 ` 565` ``` | Subst theta => (case Unify(N1 <| theta, N2 <| theta) ``` paulson@2113 ` 566` ``` of Fail => Fail ``` paulson@2113 ` 567` ``` | Subst sigma => Subst (theta <> sigma))))`; ``` paulson@2113 ` 568` paulson@2113 ` 569` ``` *---------------------------------------------------------------------------*) ```