# HG changeset patch # User paulson # Date 863772224 -7200 # Node ID 8336393de4825e29f275d5445a43a2013322f6b7 # Parent fe79ad367d7751fd121837eb476d147e110d5212 Subst now moved to directory HOL diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/AList.ML --- a/TFL/examples/Subst/AList.ML Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,34 +0,0 @@ -(* Title: Substitutions/AList.ML - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -For AList.thy. -*) - -open AList; - -val al_rews = - let fun mk_thm s = prove_goalw AList.thy [alist_rec_def,assoc_def] s - (fn _ => [Simp_tac 1]) - in map mk_thm - ["alist_rec [] c d = c", - "alist_rec ((a,b)#al) c d = d a b al (alist_rec al c d)", - "assoc v d [] = d", - "assoc v d ((a,b)#al) = (if v=a then b else assoc v d al)"] end; - - -val prems = goal AList.thy - "[| P([]); \ -\ !!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)"; -by (list.induct_tac "l" 1); -by (resolve_tac prems 1); -by (rtac PairE 1); -by (etac ssubst 1); -by (resolve_tac prems 1); -by (assume_tac 1); -qed "alist_induct"; - -(*Perform induction on xs. *) -fun alist_ind_tac a M = - EVERY [res_inst_tac [("l",a)] alist_induct M, - rename_last_tac a ["1"] (M+1)]; diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/AList.thy --- a/TFL/examples/Subst/AList.thy Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,21 +0,0 @@ -(* Title: Substitutions/alist.thy - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Association lists. -*) - -AList = List + - -consts - - alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c" - assoc :: "['a,'b,('a*'b) list] => 'b" - -rules - - alist_rec_def "alist_rec al b c == list_rec b (split c) al" - - assoc_def "assoc v d al == alist_rec al d (%x y xs g.if v=x then y else g)" - -end diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/NNF.ML --- a/TFL/examples/Subst/NNF.ML Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ -goal HOL.thy "(~(!x. P x)) = (? x. ~(P x)) & \ - \ (~(? x. P x)) = (!x. ~(P x)) & \ - \ (~(x-->y)) = (x & (~ y)) & \ - \ ((~ x) | y) = (x --> y) & \ - \ (~(x & y)) = ((~ x) | (~ y)) & \ - \ (~(x | y)) = ((~ x) & (~ y)) & \ - \ (~(~x)) = x"; -by (fast_tac HOL_cs 1); -val NNF_rews = map (fn th => th RS eq_reflection) - (Prim.Rules.CONJUNCTS (result())) - diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/NNF.thy --- a/TFL/examples/Subst/NNF.thy Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1 +0,0 @@ -NNF = HOL diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/README --- a/TFL/examples/Subst/README Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,11 +0,0 @@ -A first order unification algorithm is formalized and proved in this -directory. The files "ROOT.ML" and "ROOT1.ML" give instructions for -running the proof. "ROOT1.ML" is will run on the current Isabelle release - - "Isabelle-94 revision 5: January 96" - -while "ROOT.ML" builds on an internal release that Carsten Clasholm was -maintaining. Features of this internal release will make their way into -the public release (I hope). Eventually, the definition facility used to -define the Unify algorithm will be incorporated into the syntax for -".thy" files. diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/ROOT.ML --- a/TFL/examples/Subst/ROOT.ML Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -(* Title: HOL/Subst/ROOT.ML - ID: $Id$ - Authors: Martin Coen, Cambridge University Computer Laboratory - Konrad Slind, TU Munich - Copyright 1993 University of Cambridge, - 1996 TU Munich - -Substitution and Unification in Higher-Order Logic. - -Implements Manna & Waldinger's formalization, with Paulson's simplifications, -and some new simplifications by Slind. - -Z Manna & R Waldinger, Deductive Synthesis of the Unification Algorithm. -SCP 1 (1981), 5-48 - -L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170 - -Setplus - minor additions to HOL's set theory -Alist - association lists -Uterm - data type of terms -Subst - substitutions -Unify - specification of unification and conditions for - correctness and termination - -To load, type use"ROOT.ML"; into an Isabelle-HOL that has TFL -also loaded. -*) - -HOL_build_completed; (*Cause examples to fail if HOL did*) - -writeln"Root file for Substitutions and Unification"; -loadpath := "../../" :: !loadpath; -use_thy "Unify"; - -writeln"END: Root file for Substitutions and Unification"; diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/ROOT1.ML --- a/TFL/examples/Subst/ROOT1.ML Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,35 +0,0 @@ -(* Title: HOL/Subst/ROOT.ML - ID: $Id$ - Authors: Martin Coen, Cambridge University Computer Laboratory - Konrad Slind, TU Munich - Copyright 1993 University of Cambridge, - 1996 TU Munich - -Substitution and Unification in Higher-Order Logic. - -Implements Manna & Waldinger's formalization, with Paulson's simplifications, -and some new simplifications by Slind. - -Z Manna & R Waldinger, Deductive Synthesis of the Unification Algorithm. -SCP 1 (1981), 5-48 - -L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170 - -Setplus - minor additions to HOL's set theory -Alist - association lists -Uterm - data type of terms -Subst - substitutions -Unify - specification of unification and conditions for - correctness and termination - -To load, type use"ROOT1.ML"; into an Isabelle-HOL that has TFL -also loaded. -*) - -HOL_build_completed; (*Cause examples to fail if HOL did*) - -writeln"Root file for Substitutions and Unification"; -loadpath := "../../" :: !loadpath; (* to get "WF1" *) -use_thy "Unify1"; - -writeln"END: Root file for Substitutions and Unification"; diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/Setplus.ML --- a/TFL/examples/Subst/Setplus.ML Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,130 +0,0 @@ -(* Title: Substitutions/setplus.ML - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -For setplus.thy. -Properties of subsets and empty sets. -*) - -open Setplus; -val eq_cs = claset_of "equalities"; - -(*********) - -(*** Rules for subsets ***) - -goal Set.thy "A <= B = (! t.t:A --> t:B)"; -by (fast_tac set_cs 1); -qed "subset_iff"; - -goalw Setplus.thy [ssubset_def] "A < B = ((A <= B) & ~(A=B))"; -by (rtac refl 1); -qed "ssubset_iff"; - -goal Setplus.thy "((A::'a set) <= B) = ((A < B) | (A=B))"; -by (simp_tac (simpset_of "Fun" addsimps [ssubset_iff]) 1); -by (fast_tac set_cs 1); -qed "subseteq_iff_subset_eq"; - -(*Rule in Modus Ponens style*) -goal Setplus.thy "A < B --> c:A --> c:B"; -by (simp_tac (simpset_of "Fun" addsimps [ssubset_iff]) 1); -by (fast_tac set_cs 1); -qed "ssubsetD"; - -(*********) - -goalw Setplus.thy [empty_def] "~ a : {}"; -by (fast_tac set_cs 1); -qed "not_in_empty"; - -goalw Setplus.thy [empty_def] "(A = {}) = (ALL a.~ a:A)"; -by (fast_tac (set_cs addIs [set_ext]) 1); -qed "empty_iff"; - - -(*********) - -goal Set.thy "(~A=B) = ((? x.x:A & ~x:B) | (? x.~x:A & x:B))"; -by (fast_tac (set_cs addIs [set_ext]) 1); -qed "not_equal_iff"; - -(*********) - -val setplus_rews = [ssubset_iff,not_in_empty,empty_iff]; - -(*********) - -(*Case analysis for rewriting; P also gets rewritten*) -val [prem1,prem2] = goal HOL.thy "[| P-->Q; ~P-->Q |] ==> Q"; -by (rtac (excluded_middle RS disjE) 1); -by (etac (prem2 RS mp) 1); -by (etac (prem1 RS mp) 1); -qed "imp_excluded_middle"; - -fun imp_excluded_middle_tac s = res_inst_tac [("P",s)] imp_excluded_middle; - - -goal Set.thy "(insert a A ~= insert a B) --> A ~= B"; -by (fast_tac set_cs 1); -val insert_lim = result() RS mp; - -goal Set.thy "x~:A --> (A-{x} = A)"; -by (fast_tac eq_cs 1); -val lem = result() RS mp; - -goal Nat.thy "B<=A --> B = Suc A --> P"; -by (strip_tac 1); -by (hyp_subst_tac 1); -by (Asm_full_simp_tac 1); -val leq_lem = standard(result() RS mp RS mp); - -goal Nat.thy "A<=B --> (A ~= Suc B)"; -by (strip_tac 1); -by (rtac notI 1); -by (rtac leq_lem 1); -by (REPEAT (atac 1)); -val leq_lem1 = standard(result() RS mp); - -(* The following is an adaptation of the proof for the "<=" version - * in Finite. *) - -goalw Setplus.thy [ssubset_def] -"!!B. finite B ==> !A. A < B --> card(A) < card(B)"; -by (etac finite_induct 1); -by (Simp_tac 1); -by (fast_tac set_cs 1); -by (strip_tac 1); -by (etac conjE 1); -by (case_tac "x:A" 1); -(*1*) -by (dtac mk_disjoint_insert 1); -by (etac exE 1); -by (etac conjE 1); -by (hyp_subst_tac 1); -by (rotate_tac ~1 1); -by (asm_full_simp_tac (!simpset addsimps - [subset_insert_iff,finite_subset,lem]) 1); -by (dtac insert_lim 1); -by (Asm_full_simp_tac 1); -(*2*) -by (rotate_tac ~1 1); -by (asm_full_simp_tac (!simpset addsimps - [subset_insert_iff,finite_subset,lem]) 1); -by (case_tac "A=F" 1); -by (Asm_simp_tac 1); -by (Asm_simp_tac 1); -by (rtac leq_lem1 1); -by (Asm_simp_tac 1); -val ssubset_card = result() ; - - -goal Set.thy "(A = B) = ((A <= (B::'a set)) & (B<=A))"; -by (rtac iffI 1); -by (simp_tac (HOL_ss addsimps [subset_iff]) 1); -by (fast_tac set_cs 1); -by (rtac subset_antisym 1); -by (ALLGOALS Asm_simp_tac); -val set_eq_subset = result(); - - diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/Setplus.thy --- a/TFL/examples/Subst/Setplus.thy Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,14 +0,0 @@ -(* Title: Substitutions/setplus.thy - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Minor additions to HOL's set theory -*) - -Setplus = Finite + - -rules - - ssubset_def "A < B == A <= B & ~ A=B" - -end diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/Subst.ML --- a/TFL/examples/Subst/Subst.ML Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,199 +0,0 @@ -(* Title: HOL/Subst/subst.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -For subst.thy. -*) - -open Subst; - - -(**** Substitutions ****) - -goal Subst.thy "t <| [] = t"; -by (uterm.induct_tac "t" 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps al_rews))); -qed "subst_Nil"; - -goal Subst.thy "t <: u --> t <| s <: u <| s"; -by (uterm.induct_tac "u" 1); -by (ALLGOALS Asm_simp_tac); -val subst_mono = store_thm("subst_mono", result() RS mp); - -goal Subst.thy "~ (Var(v) <: t) --> t <| (v,t <| s)#s = t <| s"; -by (imp_excluded_middle_tac "t = Var(v)" 1); -by (res_inst_tac [("P", - "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")] - uterm.induct 2); -by (ALLGOALS (simp_tac (!simpset addsimps al_rews))); -by (fast_tac HOL_cs 1); -val Var_not_occs = store_thm("Var_not_occs", result() RS mp); - -goal Subst.thy - "(t <|r = t <|s) = (! v.v : vars_of(t) --> Var(v) <|r = Var(v) <|s)"; -by (uterm.induct_tac "t" 1); -by (REPEAT (etac rev_mp 3)); -by (ALLGOALS Asm_simp_tac); -by (ALLGOALS (fast_tac HOL_cs)); -qed "agreement"; - -goal Subst.thy "~ v: vars_of(t) --> t <| (v,u)#s = t <| s"; -by(simp_tac (!simpset addsimps (agreement::al_rews) - setloop (split_tac [expand_if])) 1); -val repl_invariance = store_thm("repl_invariance", result() RS mp); - -val asms = goal Subst.thy - "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)"; -by (uterm.induct_tac "t" 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps al_rews))); -val Var_in_subst = store_thm("Var_in_subst", result() RS mp); - - -(**** Equality between Substitutions ****) - -goalw Subst.thy [subst_eq_def] "r =s= s = (! t.t <| r = t <| s)"; -by (Simp_tac 1); -qed "subst_eq_iff"; - - -local fun mk_thm s = prove_goal Subst.thy s - (fn prems => [cut_facts_tac prems 1, - REPEAT (etac rev_mp 1), - simp_tac (!simpset addsimps [subst_eq_iff]) 1]) -in - val subst_refl = mk_thm "r = s ==> r =s= s"; - val subst_sym = mk_thm "r =s= s ==> s =s= r"; - val subst_trans = mk_thm "[| q =s= r; r =s= s |] ==> q =s= s"; -end; - -val eq::prems = goalw Subst.thy [subst_eq_def] - "[| r =s= s; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)"; -by (resolve_tac [eq RS spec RS subst] 1); -by (resolve_tac (prems RL [eq RS spec RS subst]) 1); -qed "subst_subst2"; - -val ssubst_subst2 = subst_sym RS subst_subst2; - -(**** Composition of Substitutions ****) - -local fun mk_thm s = - prove_goalw Subst.thy [comp_def,sdom_def] s - (fn _ => [simp_tac (simpset_of "UTerm" addsimps al_rews) 1]) -in -val subst_rews = - map mk_thm - [ "[] <> bl = bl", - "((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)", - "sdom([]) = {}", - "sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else (sdom al) Un {a})"] -end; - - -goal Subst.thy "s <> [] = s"; -by (alist_ind_tac "s" 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps (subst_Nil::subst_rews)))); -qed "comp_Nil"; - -goal Subst.thy "(t <| r <> s) = (t <| r <| s)"; -by (uterm.induct_tac "t" 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps al_rews))); -by (alist_ind_tac "r" 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps (subst_Nil::(al_rews@subst_rews)) - setloop (split_tac [expand_if])))); -qed "subst_comp"; - - -goal Subst.thy "(q <> r) <> s =s= q <> (r <> s)"; -by (simp_tac (!simpset addsimps [subst_eq_iff,subst_comp]) 1); -qed "comp_assoc"; - -goal Subst.thy "(theta =s= theta1) --> \ - \ (sigma =s= sigma1) --> \ - \ ((theta <> sigma) =s= (theta1 <> sigma1))"; -by (simp_tac (!simpset addsimps [subst_eq_def,subst_comp]) 1); -val subst_cong = result() RS mp RS mp; - - -goal Subst.thy "(w,Var(w) <| s)#s =s= s"; -by (rtac (allI RS (subst_eq_iff RS iffD2)) 1); -by (uterm.induct_tac "t" 1); -by (REPEAT (etac rev_mp 3)); -by (ALLGOALS (simp_tac (!simpset addsimps al_rews - setloop (split_tac [expand_if])))); -qed "Cons_trivial"; - - -val [prem] = goal Subst.thy "q <> r =s= s ==> t <| q <| r = t <| s"; -by (simp_tac (!simpset addsimps [prem RS (subst_eq_iff RS iffD1), - subst_comp RS sym]) 1); -qed "comp_subst_subst"; - - -(**** Domain and range of Substitutions ****) - -goal Subst.thy "(v : sdom(s)) = (~ Var(v) <| s = Var(v))"; -by (alist_ind_tac "s" 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps (al_rews@subst_rews) - setloop (split_tac[expand_if])))); -by (fast_tac HOL_cs 1); -qed "sdom_iff"; - - -goalw Subst.thy [srange_def] - "v : srange(s) = (? w.w : sdom(s) & v : vars_of(Var(w) <| s))"; -by (fast_tac set_cs 1); -qed "srange_iff"; - -goal Subst.thy "(t <| s = t) = (sdom(s) Int vars_of(t) = {})"; -by (uterm.induct_tac "t" 1); -by (REPEAT (etac rev_mp 3)); -by (ALLGOALS (simp_tac (!simpset addsimps - (sdom_iff::(subst_rews@al_rews@setplus_rews))))); -by (ALLGOALS (fast_tac set_cs)); -qed "invariance"; - -goal Subst.thy "v : sdom(s) --> ~v : srange(s) --> ~v : vars_of(t <| s)"; -by (uterm.induct_tac "t" 1); -by (imp_excluded_middle_tac "a : sdom(s)" 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps [sdom_iff,srange_iff]))); -by (ALLGOALS (fast_tac set_cs)); -val Var_elim = store_thm("Var_elim", result() RS mp RS mp); - -val asms = goal Subst.thy - "[| v : sdom(s); v : vars_of(t <| s) |] ==> v : srange(s)"; -by (REPEAT (ares_tac (asms @ [Var_elim RS swap RS classical]) 1)); -qed "Var_elim2"; - -goal Subst.thy "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)"; -by (uterm.induct_tac "t" 1); -by (REPEAT_SOME (etac rev_mp )); -by (ALLGOALS (simp_tac (!simpset addsimps [sdom_iff,srange_iff]))); -by (REPEAT (step_tac (set_cs addIs [vars_var_iff RS iffD1 RS sym]) 1)); -by (etac notE 1); -by (etac subst 1); -by (ALLGOALS (fast_tac set_cs)); -val Var_intro = store_thm("Var_intro", result() RS mp); - -goal Subst.thy - "v : srange(s) --> (? w.w : sdom(s) & v : vars_of(Var(w) <| s))"; -by (simp_tac (!simpset addsimps [srange_iff]) 1); -val srangeE = store_thm("srangeE", make_elim (result() RS mp)); - -val asms = goal Subst.thy - "sdom(s) Int srange(s) = {} = (! t.sdom(s) Int vars_of(t <| s) = {})"; -by (simp_tac (!simpset addsimps setplus_rews) 1); -by (fast_tac (set_cs addIs [Var_elim2] addEs [srangeE]) 1); -qed "dom_range_disjoint"; - -val asms = goal Subst.thy "~ u <| s = u --> (? x. x : sdom(s))"; -by (simp_tac (!simpset addsimps (invariance::setplus_rews)) 1); -by (fast_tac set_cs 1); -val subst_not_empty = store_thm("subst_not_empty", result() RS mp); - - -goal Subst.thy "(M <| [(x, Var x)]) = M"; -by (UTerm.uterm.induct_tac "M" 1); -by (ALLGOALS (asm_simp_tac (!simpset addsimps (subst_rews@al_rews) - setloop (split_tac [expand_if])))); -val id_subst_lemma = result(); diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/Subst.thy --- a/TFL/examples/Subst/Subst.thy Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -(* Title: Substitutions/subst.thy - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Substitutions on uterms -*) - -Subst = Setplus + AList + UTerm + - -consts - - "=s=" :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr 52) - "<|" :: "'a uterm => ('a * 'a uterm) list => 'a uterm" (infixl 55) - "<>" :: "[('a*('a uterm)) list, ('a*('a uterm)) list] - => ('a*('a uterm)) list" (infixl 56) - sdom :: "('a*('a uterm)) list => 'a set" - srange :: "('a*('a uterm)) list => 'a set" - - -primrec "op <|" uterm - subst_Var "(Var v <| s) = assoc v (Var v) s" - subst_Const "(Const c <| s) = Const c" - subst_Comb "(Comb M N <| s) = Comb (M <| s) (N <| s)" - - -rules - - subst_eq_def "r =s= s == ALL t.t <| r = t <| s" - - comp_def "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)" - - sdom_def - "sdom(al) == alist_rec al {} - (%x y xs g. if Var(x)=y then g - {x} else g Un {x})" - - srange_def - "srange(al) == Union({y. EX x:sdom(al). y=vars_of(Var(x) <| al)})" - -end diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/UTerm.ML --- a/TFL/examples/Subst/UTerm.ML Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,47 +0,0 @@ -(* Title: HOL/Subst/UTerm.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Simple term structure for unifiation. -Binary trees with leaves that are constants or variables. -*) - -open UTerm; - - -(**** vars_of lemmas ****) - -goal UTerm.thy "(v : vars_of(Var(w))) = (w=v)"; -by (Simp_tac 1); -by (fast_tac HOL_cs 1); -qed "vars_var_iff"; - -goal UTerm.thy "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)"; -by (uterm.induct_tac "t" 1); -by (ALLGOALS Simp_tac); -by (fast_tac HOL_cs 1); -qed "vars_iff_occseq"; - - -(* Not used, but perhaps useful in other proofs *) -goal UTerm.thy "M<:N --> vars_of(M) <= vars_of(N)"; -by (uterm.induct_tac "N" 1); -by (ALLGOALS Asm_simp_tac); -by (fast_tac set_cs 1); -val occs_vars_subset = result(); - - -goal UTerm.thy - "vars_of M Un vars_of N <= vars_of(Comb M P) Un vars_of(Comb N Q)"; -by (Simp_tac 1); -by (fast_tac set_cs 1); -val monotone_vars_of = result(); - -goal UTerm.thy "finite(vars_of M)"; -by (uterm.induct_tac"M" 1); -by (ALLGOALS Simp_tac); -by (forward_tac [finite_UnI] 1); -by (assume_tac 1); -by (Asm_simp_tac 1); -val finite_vars_of = result(); diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/UTerm.thy --- a/TFL/examples/Subst/UTerm.thy Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,37 +0,0 @@ -(* Title: Substitutions/UTerm.thy - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Simple term structure for unification. -Binary trees with leaves that are constants or variables. -*) - -UTerm = Finite + - -datatype 'a uterm = Var ('a) - | Const ('a) - | Comb ('a uterm) ('a uterm) - -consts - vars_of :: 'a uterm => 'a set - "<:" :: 'a uterm => 'a uterm => bool (infixl 54) -uterm_size :: 'a uterm => nat - - -primrec vars_of uterm -vars_of_Var "vars_of (Var v) = {v}" -vars_of_Const "vars_of (Const c) = {}" -vars_of_Comb "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))" - - -primrec "op <:" uterm -occs_Var "u <: (Var v) = False" -occs_Const "u <: (Const c) = False" -occs_Comb "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)" - -primrec uterm_size uterm -uterm_size_Var "uterm_size (Var v) = 0" -uterm_size_Const "uterm_size (Const c) = 0" -uterm_size_Comb "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)" - -end diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/Unifier.ML --- a/TFL/examples/Subst/Unifier.ML Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,114 +0,0 @@ -(* Title: HOL/Subst/unifier.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -For Unifier.thy. -Properties of unifiers. -*) - -open Unifier; - -val unify_defs = [Unifier_def,MoreGeneral_def,MGUnifier_def]; - -val rews = subst_rews@al_rews@setplus_rews; - -(*--------------------------------------------------------------------------- - * Unifiers - *---------------------------------------------------------------------------*) - -goalw Unifier.thy [Unifier_def] "Unifier s t u = (t <| s = u <| s)"; -by (rtac refl 1); -val Unifier_iff = result(); - -goal Unifier.thy - "Unifier s (Comb t u) (Comb v w) --> Unifier s t v & Unifier s u w"; -by (simp_tac (!simpset addsimps [Unifier_iff]) 1); -val Unifier_Comb = result() RS mp RS conjE; - -goal Unifier.thy - "~v : vars_of(t) --> ~v : vars_of(u) --> Unifier s t u --> \ -\ Unifier ((v,r)#s) t u"; -by (simp_tac (!simpset addsimps [Unifier_iff,repl_invariance]) 1); -val Cons_Unifier = result() RS mp RS mp RS mp; - - -(*--------------------------------------------------------------------------- - * Most General Unifiers - *---------------------------------------------------------------------------*) - -goalw Unifier.thy unify_defs "MGUnifier s t u = MGUnifier s u t"; -by (safe_tac (HOL_cs addSEs ([sym]@([spec] RL [mp])))); -val mgu_sym = result(); - - -goalw Unifier.thy [MoreGeneral_def] "r >> s = (EX q. s =s= r <> q)"; -by (rtac refl 1); -val MoreGen_iff = result(); - - -goal Unifier.thy "[] >> s"; -by (simp_tac (!simpset addsimps (MoreGen_iff::subst_rews)) 1); -by (fast_tac (set_cs addIs [refl RS subst_refl]) 1); -val MoreGen_Nil = result(); - - -goalw Unifier.thy unify_defs - "MGUnifier s t u = (ALL r. Unifier r t u = s >> r)"; -by (REPEAT (ares_tac [iffI,allI] 1 ORELSE - eresolve_tac [conjE,allE,mp,exE,ssubst_subst2] 1)); -by (asm_simp_tac (!simpset addsimps [subst_comp]) 1); -by (fast_tac (set_cs addIs [comp_Nil RS sym RS subst_refl]) 1); -val MGU_iff = result(); - - -val [prem] = goal Unifier.thy - "~ Var(v) <: t ==> MGUnifier [(v,t)] (Var v) t"; -by(simp_tac(HOL_ss addsimps([MGU_iff,MoreGen_iff,Unifier_iff]@rews))1); -by (REPEAT_SOME (step_tac set_cs)); -by (etac subst 1); -by (etac ssubst_subst2 2); -by (rtac (Cons_trivial RS subst_sym) 1); -by (simp_tac (!simpset addsimps ((prem RS Var_not_occs)::rews)) 1); -val MGUnifier_Var = result(); - - - -(*--------------------------------------------------------------------------- - * Idempotence. - *---------------------------------------------------------------------------*) - -goalw Unifier.thy [Idem_def] "Idem([])"; -by (simp_tac (!simpset addsimps (refl RS subst_refl)::rews) 1); -qed "Idem_Nil"; - -goalw Unifier.thy [Idem_def] "Idem(s) = (sdom(s) Int srange(s) = {})"; -by (simp_tac (!simpset addsimps [subst_eq_iff,subst_comp, - invariance,dom_range_disjoint])1); -qed "Idem_iff"; - -val rews = subst_rews@al_rews@setplus_rews; -goal Unifier.thy "~ (Var(v) <: t) --> Idem([(v,t)])"; -by (simp_tac (!simpset addsimps (vars_iff_occseq::Idem_iff::srange_iff::rews) - setloop (split_tac [expand_if])) 1); -by (fast_tac set_cs 1); -val Var_Idem = store_thm("Var_Idem", result() RS mp); - - -val [prem] = goalw Unifier.thy [Idem_def] -"Idem(r) ==> Unifier s (t<|r) (u<|r) --> Unifier (r <> s) (t <| r) (u <| r)"; -by (simp_tac (!simpset addsimps - [Unifier_iff,subst_comp,prem RS comp_subst_subst]) 1); -val Unifier_Idem_subst = store_thm("Unifier_Idem_subst", result() RS mp); - -val [p1,p2,p3] = goal Unifier.thy - "[| Idem(r); Unifier s (t <| r) (u <| r); \ -\ (!q. Unifier q (t <| r) (u <| r) --> s <> q =s= q) \ -\ |] ==> Idem(r <> s)"; - -by (cut_facts_tac [p1, - p2 RS (p1 RS Unifier_Idem_subst RS (p3 RS spec RS mp))] 1); -by (REPEAT_SOME (etac rev_mp)); -by (simp_tac (!simpset addsimps [Idem_def,subst_eq_iff,subst_comp]) 1); -qed "Idem_comp"; - diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/Unifier.thy --- a/TFL/examples/Subst/Unifier.thy Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -(* Title: Subst/unifier.thy - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Definition of most general unifier -*) - -Unifier = Subst + - -consts - - Unifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool" - ">>" :: "[('a*('a uterm))list,('a*('a uterm))list] => bool" (infixr 52) - MGUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool" - Idem :: "('a*('a uterm))list => bool" - -rules (*Definitions*) - - Unifier_def "Unifier s t u == t <| s = u <| s" - MoreGeneral_def "r >> s == ? q. s =s= r <> q" - MGUnifier_def "MGUnifier s t u == Unifier s t u & - (!r. Unifier r t u --> s >> r)" - Idem_def "Idem(s) == s <> s =s= s" -end diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/Unify.ML --- a/TFL/examples/Subst/Unify.ML Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,569 +0,0 @@ -(*--------------------------------------------------------------------------- - * This file defines a nested unification algorithm, then proves that it - * terminates, then proves 2 correctness theorems: that when the algorithm - * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution. - * Although the proofs may seem long, they are actually quite direct, in that - * the correctness and termination properties are not mingled as much as in - * previous proofs of this algorithm. - * - * Our approach for nested recursive functions is as follows: - * - * 0. Prove the wellfoundedness of the termination relation. - * 1. Prove the non-nested termination conditions. - * 2. Eliminate (0) and (1) from the recursion equations and the - * induction theorem. - * 3. Prove the nested termination conditions by using the induction - * theorem from (2) and by using the recursion equations from (2). - * These are constrained by the nested termination conditions, but - * things work out magically (by wellfoundedness of the termination - * relation). - * 4. Eliminate the nested TCs from the results of (2). - * 5. Prove further correctness properties using the results of (4). - * - * Deeper nestings require iteration of steps (3) and (4). - *---------------------------------------------------------------------------*) - -(* This is just a wrapper for the definition mechanism. *) -local fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[]))); -in -fun Rfunc thy R eqs = - let val read = term_of o cread thy; - in Tfl.Rfunction thy (read R) (read eqs) - end -end; - -(*--------------------------------------------------------------------------- - * The algorithm. - *---------------------------------------------------------------------------*) -val {theory,induction,rules,tcs} = -Rfunc Unify.thy "R" - "(Unify(Const m, Const n) = (if (m=n) then Subst[] else Fail)) & \ -\ (Unify(Const m, Comb M N) = Fail) & \ -\ (Unify(Const m, Var v) = Subst[(v,Const m)]) & \ -\ (Unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])) & \ -\ (Unify(Comb M N, Const x) = Fail) & \ -\ (Unify(Comb M N, Var v) = (if (Var v <: Comb M N) then Fail \ -\ else Subst[(v,Comb M N)])) & \ -\ (Unify(Comb M1 N1, Comb M2 N2) = \ -\ (case Unify(M1,M2) \ -\ of Fail => Fail \ -\ | Subst theta => (case Unify(N1 <| theta, N2 <| theta) \ -\ of Fail => Fail \ -\ | Subst sigma => Subst (theta <> sigma))))"; - -open Unify; - -(*--------------------------------------------------------------------------- - * A slightly augmented strip_tac. - *---------------------------------------------------------------------------*) -fun my_strip_tac i = - CHANGED (strip_tac i - THEN REPEAT ((etac exE ORELSE' etac conjE) i) - THEN TRY (hyp_subst_tac i)); - -(*--------------------------------------------------------------------------- - * A slightly augmented fast_tac for sets. It handles the case where the - * top connective is "=". - *---------------------------------------------------------------------------*) -fun my_fast_set_tac i = (TRY(rtac set_ext i) THEN fast_tac set_cs i); - - -(*--------------------------------------------------------------------------- - * Wellfoundedness of proper subset on finite sets. - *---------------------------------------------------------------------------*) -goalw Unify.thy [R0_def] "wf(R0)"; -by (rtac ((wf_subset RS mp) RS mp) 1); -by (rtac wf_measure 1); -by(simp_tac(!simpset addsimps[measure_def,inv_image_def,symmetric less_def])1); -by (my_strip_tac 1); -by (forward_tac[ssubset_card] 1); -by (fast_tac set_cs 1); -val wf_R0 = result(); - - -(*--------------------------------------------------------------------------- - * Tactic for selecting and working on the first projection of R. - *---------------------------------------------------------------------------*) -fun R0_tac thms i = - (simp_tac (!simpset addsimps (thms@[R_def,lex_prod_def, - measure_def,inv_image_def,point_to_prod_def])) i THEN - REPEAT (rtac exI i) THEN - REPEAT ((rtac conjI THEN' rtac refl) i) THEN - rtac disjI1 i THEN - simp_tac (!simpset addsimps [R0_def,finite_vars_of]) i); - - - -(*--------------------------------------------------------------------------- - * Tactic for selecting and working on the second projection of R. - *---------------------------------------------------------------------------*) -fun R1_tac thms i = - (simp_tac (!simpset addsimps (thms@[R_def,lex_prod_def, - measure_def,inv_image_def,point_to_prod_def])) i THEN - REPEAT (rtac exI i) THEN - REPEAT ((rtac conjI THEN' rtac refl) i) THEN - rtac disjI2 i THEN - asm_simp_tac (!simpset addsimps [R1_def,rprod_def]) i); - - -(*--------------------------------------------------------------------------- - * The non-nested TC plus the wellfoundedness of R. - *---------------------------------------------------------------------------*) -Tfl.tgoalw Unify.thy [] rules; -by (rtac conjI 1); -(* TC *) -by (my_strip_tac 1); -by (cut_facts_tac [monotone_vars_of] 1); -by (asm_full_simp_tac(!simpset addsimps [subseteq_iff_subset_eq]) 1); -by (etac disjE 1); -by (R0_tac[] 1); -by (R1_tac[] 1); -by (simp_tac - (!simpset addsimps [measure_def,inv_image_def,less_eq,less_add_Suc1]) 1); - -(* Wellfoundedness of R *) -by (simp_tac (!simpset addsimps [Unify.R_def,Unify.R1_def]) 1); -by (REPEAT (resolve_tac [wf_inv_image,wf_lex_prod,wf_R0, - wf_rel_prod, wf_measure] 1)); -val tc0 = result(); - - -(*--------------------------------------------------------------------------- - * Eliminate tc0 from the recursion equations and the induction theorem. - *---------------------------------------------------------------------------*) -val [tc,wfr] = Prim.Rules.CONJUNCTS tc0; -val rules1 = implies_intr_hyps rules; -val rules2 = wfr RS rules1; - -val [a,b,c,d,e,f,g] = Prim.Rules.CONJUNCTS rules2; -val g' = tc RS (g RS mp); -val rules4 = standard (Prim.Rules.LIST_CONJ[a,b,c,d,e,f,g']); - -val induction1 = implies_intr_hyps induction; -val induction2 = wfr RS induction1; -val induction3 = tc RS induction2; - -val induction4 = standard - (rewrite_rule[fst_conv RS eq_reflection, snd_conv RS eq_reflection] - (induction3 RS (read_instantiate_sg (sign_of theory) - [("x","%p. Phi (fst p) (snd p)")] spec))); - - -(*--------------------------------------------------------------------------- - * Some theorems about transitivity of WF combinators. Only the last - * (transR) is used, in the proof of termination. The others are generic and - * should maybe go somewhere. - *---------------------------------------------------------------------------*) -goalw WF1.thy [trans_def,lex_prod_def,mem_Collect_eq RS eq_reflection] - "trans R1 & trans R2 --> trans (R1 ** R2)"; -by (my_strip_tac 1); -by (res_inst_tac [("x","a")] exI 1); -by (res_inst_tac [("x","a'a")] exI 1); -by (res_inst_tac [("x","b")] exI 1); -by (res_inst_tac [("x","b'a")] exI 1); -by (REPEAT (rewrite_tac [Pair_eq RS eq_reflection] THEN my_strip_tac 1)); -by (Simp_tac 1); -by (REPEAT (etac disjE 1)); -by (rtac disjI1 1); -by (ALLGOALS (fast_tac set_cs)); -val trans_lex_prod = result() RS mp; - - -goalw WF1.thy [trans_def,rprod_def,mem_Collect_eq RS eq_reflection] - "trans R1 & trans R2 --> trans (rprod R1 R2)"; -by (my_strip_tac 1); -by (res_inst_tac [("x","a")] exI 1); -by (res_inst_tac [("x","a'a")] exI 1); -by (res_inst_tac [("x","b")] exI 1); -by (res_inst_tac [("x","b'a")] exI 1); -by (REPEAT (rewrite_tac [Pair_eq RS eq_reflection] THEN my_strip_tac 1)); -by (Simp_tac 1); -by (fast_tac set_cs 1); -val trans_rprod = result() RS mp; - - -goalw Unify.thy [trans_def,inv_image_def,mem_Collect_eq RS eq_reflection] - "trans r --> trans (inv_image r f)"; -by (rewrite_tac [fst_conv RS eq_reflection, snd_conv RS eq_reflection]); -by (fast_tac set_cs 1); -val trans_inv_image = result() RS mp; - -goalw Unify.thy [R0_def, trans_def, mem_Collect_eq RS eq_reflection] - "trans R0"; -by (rewrite_tac [fst_conv RS eq_reflection,snd_conv RS eq_reflection, - ssubset_def, set_eq_subset RS eq_reflection]); -by (fast_tac set_cs 1); -val trans_R0 = result(); - -goalw Unify.thy [R_def,R1_def,measure_def] "trans R"; -by (REPEAT (resolve_tac[trans_inv_image,trans_lex_prod,conjI, trans_R0, - trans_rprod, trans_inv_image, trans_trancl] 1)); -val transR = result(); - - -(*--------------------------------------------------------------------------- - * The following lemma is used in the last step of the termination proof for - * the nested call in Unify. Loosely, it says that R doesn't care so much - * about term structure. - *---------------------------------------------------------------------------*) -goalw Unify.thy [R_def,lex_prod_def, inv_image_def,point_to_prod_def] - "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : R --> \ - \ ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : R"; -by (Simp_tac 1); -by (rtac conjI 1); -by (strip_tac 1); -by (rtac disjI1 1); -by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \ - \ (vars_of D Un vars_of E Un vars_of F)) = \ - \ (vars_of A Un (vars_of B Un vars_of C) Un \ - \ (vars_of D Un (vars_of E Un vars_of F)))" 1); -by (my_fast_set_tac 2); -by (Asm_simp_tac 1); -by (strip_tac 1); -by (rtac disjI2 1); -by (etac conjE 1); -by (Asm_simp_tac 1); -by (rtac conjI 1); -by (my_fast_set_tac 1); -by (asm_full_simp_tac (!simpset addsimps [R1_def, measure_def, rprod_def, - less_eq, inv_image_def,add_assoc]) 1); -val Rassoc = result() RS mp; - -(*--------------------------------------------------------------------------- - * Rewriting support. - *---------------------------------------------------------------------------*) - -val termin_ss = (!simpset addsimps (srange_iff::(subst_rews@al_rews))); - - -(*--------------------------------------------------------------------------- - * This lemma proves the nested termination condition for the base cases - * 3, 4, and 6. It's a clumsy formulation (requiring two conjuncts, each with - * exactly the same proof) of a more general theorem. - *---------------------------------------------------------------------------*) -goal theory "(~(Var x <: M)) --> [(x, M)] = theta --> \ -\ (! N1 N2. (((N1 <| theta, N2 <| theta), (Comb M N1, Comb (Var x) N2)) : R) \ -\ & (((N1 <| theta, N2 <| theta), (Comb(Var x) N1, Comb M N2)) : R))"; -by (my_strip_tac 1); -by (case_tac "Var x = M" 1); -by (hyp_subst_tac 1); -by (case_tac "x:(vars_of N1 Un vars_of N2)" 1); -let val case1 = - EVERY1[R1_tac[id_subst_lemma], rtac conjI, my_fast_set_tac, - REPEAT o (rtac exI), REPEAT o (rtac conjI THEN' rtac refl), - simp_tac (!simpset addsimps [measure_def,inv_image_def,less_eq])]; -in by (rtac conjI 1); - by case1; - by case1 -end; - -let val case2 = - EVERY1[R0_tac[id_subst_lemma], - simp_tac (!simpset addsimps [ssubset_def,set_eq_subset]), - fast_tac set_cs] -in by (rtac conjI 1); - by case2; - by case2 -end; - -let val case3 = - EVERY1 [R0_tac[], - cut_inst_tac [("s2","[(x, M)]"), ("v2", "x"), ("t2","N1")] Var_elim] - THEN ALLGOALS(asm_simp_tac(termin_ss addsimps [vars_iff_occseq])) - THEN cut_inst_tac [("s2","[(x, M)]"),("v2", "x"), ("t2","N2")] Var_elim 1 - THEN ALLGOALS(asm_simp_tac(termin_ss addsimps [vars_iff_occseq])) - THEN EVERY1 [simp_tac (HOL_ss addsimps [ssubset_def]), - rtac conjI, simp_tac (HOL_ss addsimps [subset_iff]), - my_strip_tac, etac UnE, dtac Var_intro] - THEN dtac Var_intro 2 - THEN ALLGOALS (asm_full_simp_tac (termin_ss addsimps [set_eq_subset])) - THEN TRYALL (fast_tac set_cs) -in - by (rtac conjI 1); - by case3; - by case3 -end; -val var_elimR = result() RS mp RS mp RS spec RS spec; - - -val Some{nchotomy = subst_nchotomy,...} = assoc(!datatypes,"subst"); - -(*--------------------------------------------------------------------------- - * Do a case analysis on something of type 'a subst. - *---------------------------------------------------------------------------*) - -fun Subst_case_tac theta = -(cut_inst_tac theta (standard (Prim.Rules.SPEC_ALL subst_nchotomy)) 1 - THEN etac disjE 1 - THEN rotate_tac ~1 1 - THEN Asm_full_simp_tac 1 - THEN etac exE 1 - THEN rotate_tac ~1 1 - THEN Asm_full_simp_tac 1); - - -goals_limit := 1; - -(*--------------------------------------------------------------------------- - * The nested TC. Proved by recursion induction. - *---------------------------------------------------------------------------*) -goalw_cterm [] - (hd(tl(tl(map (cterm_of (sign_of theory) o USyntax.mk_prop) tcs)))); -(*--------------------------------------------------------------------------- - * The extracted TC needs the scope of its quantifiers adjusted, so our - * first step is to restrict the scopes of N1 and N2. - *---------------------------------------------------------------------------*) -by (subgoal_tac "!M1 M2 theta. \ - \ Unify (M1, M2) = Subst theta --> \ - \ (!N1 N2. ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R)" 1); -by (fast_tac HOL_cs 1); -by (rtac allI 1); -by (rtac allI 1); -(* Apply induction *) -by (res_inst_tac [("xa","M1"),("x","M2")] - (standard (induction4 RS mp RS spec RS spec)) 1); -by (simp_tac (!simpset addsimps (rules4::(subst_rews@al_rews)) - setloop (split_tac [expand_if])) 1); -(* 1 *) -by (rtac conjI 1); -by (my_strip_tac 1); -by (R1_tac[subst_Nil] 1); -by (REPEAT (rtac exI 1) THEN REPEAT ((rtac conjI THEN' rtac refl) 1)); -by (simp_tac (!simpset addsimps [measure_def,inv_image_def,less_eq]) 1); - -(* 3 *) -by (rtac conjI 1); -by (my_strip_tac 1); -by (rtac (Prim.Rules.CONJUNCT1 var_elimR) 1); -by (Simp_tac 1); -by (rtac refl 1); - -(* 4 *) -by (rtac conjI 1); -by (strip_tac 1); -by (rtac (Prim.Rules.CONJUNCT2 var_elimR) 1); -by (assume_tac 1); -by (rtac refl 1); - -(* 6 *) -by (rtac conjI 1); -by (rewrite_tac [symmetric (occs_Comb RS eq_reflection)]); -by (my_strip_tac 1); -by (rtac (Prim.Rules.CONJUNCT1 var_elimR) 1); -by (Asm_simp_tac 1); -by (rtac refl 1); - -(* 7 *) -by (REPEAT (rtac allI 1)); -by (rtac impI 1); -by (etac conjE 1); -by (Subst_case_tac [("v","Unify(M1, M2)")]); -by (rename_tac "theta" 1); - -by (Subst_case_tac [("v","Unify(N1 <| theta, N2 <| theta)")]); -by (rename_tac "sigma" 1); -by (REPEAT (rtac allI 1)); -by (rename_tac "P Q" 1); -by (simp_tac (HOL_ss addsimps [subst_comp]) 1); -by(rtac(rewrite_rule[trans_def] transR RS spec RS spec RS spec RS mp RS mp) 1); -by (fast_tac HOL_cs 1); -by (simp_tac (HOL_ss addsimps [symmetric (subst_Comb RS eq_reflection)]) 1); -by (subgoal_tac "((Comb N1 P <| theta, Comb N2 Q <| theta), \ - \ (Comb M1 (Comb N1 P), Comb M2 (Comb N2 Q))) :R" 1); -by (asm_simp_tac HOL_ss 2); - -by (rtac Rassoc 1); -by (assume_tac 1); -val Unify_TC2 = result(); - - -(*--------------------------------------------------------------------------- - * Now for elimination of nested TC from rules and induction. This step - * would be easier if "rewrite_rule" used context. - *---------------------------------------------------------------------------*) -goal theory - "(Unify (Comb M1 N1, Comb M2 N2) = \ -\ (case Unify (M1, M2) of Fail => Fail \ -\ | Subst theta => \ -\ (case if ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R \ -\ then Unify (N1 <| theta, N2 <| theta) else @ z. True of \ -\ Fail => Fail | Subst sigma => Subst (theta <> sigma)))) \ -\ = \ -\ (Unify (Comb M1 N1, Comb M2 N2) = \ -\ (case Unify (M1, M2) \ -\ of Fail => Fail \ -\ | Subst theta => (case Unify (N1 <| theta, N2 <| theta) \ -\ of Fail => Fail \ -\ | Subst sigma => Subst (theta <> sigma))))"; -by (cut_inst_tac [("v","Unify(M1, M2)")] - (standard (Prim.Rules.SPEC_ALL subst_nchotomy)) 1); -by (etac disjE 1); -by (Asm_simp_tac 1); -by (etac exE 1); -by (Asm_simp_tac 1); -by (cut_inst_tac - [("x","list"), ("xb","N1"), ("xa","N2"),("xc","M2"), ("xd","M1")] - (standard(Unify_TC2 RS spec RS spec RS spec RS spec RS spec)) 1); -by (Asm_full_simp_tac 1); -val Unify_rec_simpl = result() RS eq_reflection; - -val Unify_rules = rewrite_rule[Unify_rec_simpl] rules4; - - -goal theory - "(! M1 N1 M2 N2. \ -\ (! theta. \ -\ Unify (M1, M2) = Subst theta --> \ -\ ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R --> \ -\ ?Phi (N1 <| theta) (N2 <| theta)) & ?Phi M1 M2 --> \ -\ ?Phi (Comb M1 N1) (Comb M2 N2)) \ -\ = \ -\ (! M1 N1 M2 N2. \ -\ (! theta. \ -\ Unify (M1, M2) = Subst theta --> \ -\ ?Phi (N1 <| theta) (N2 <| theta)) & ?Phi M1 M2 --> \ -\ ?Phi (Comb M1 N1) (Comb M2 N2))"; -by (simp_tac (HOL_ss addsimps [Unify_TC2]) 1); -val Unify_induction = rewrite_rule[result() RS eq_reflection] induction4; - - - -(*--------------------------------------------------------------------------- - * Correctness. Notice that idempotence is not needed to prove that the - * algorithm terminates and is not needed to prove the algorithm correct, - * if you are only interested in an MGU. This is in contrast to the - * approach of M&W, who used idempotence and MGU-ness in the termination proof. - *---------------------------------------------------------------------------*) - -goal theory "!theta. Unify (P,Q) = Subst theta --> MGUnifier theta P Q"; -by (res_inst_tac [("xa","P"),("x","Q")] - (standard (Unify_induction RS mp RS spec RS spec)) 1); -by (simp_tac (!simpset addsimps [Unify_rules] - setloop (split_tac [expand_if])) 1); -(*1*) -by (rtac conjI 1); -by (REPEAT (rtac allI 1)); -by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1); -by (my_strip_tac 1); -by (rtac MoreGen_Nil 1); - -(*3*) -by (rtac conjI 1); -by (my_strip_tac 1); -by (rtac (mgu_sym RS iffD1) 1); -by (rtac MGUnifier_Var 1); -by (Simp_tac 1); - -(*4*) -by (rtac conjI 1); -by (my_strip_tac 1); -by (rtac MGUnifier_Var 1); -by (assume_tac 1); - -(*6*) -by (rtac conjI 1); -by (rewrite_tac NNF_rews); -by (my_strip_tac 1); -by (rtac (mgu_sym RS iffD1) 1); -by (rtac MGUnifier_Var 1); -by (Asm_simp_tac 1); - -(*7*) -by (safe_tac HOL_cs); -by (Subst_case_tac [("v","Unify(M1, M2)")]); -by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]); -by (hyp_subst_tac 1); -by (asm_full_simp_tac(HOL_ss addsimps [MGUnifier_def,Unifier_def])1); -by (asm_simp_tac (!simpset addsimps [subst_comp]) 1); (* It's a unifier.*) - -by (safe_tac HOL_cs); -by (rename_tac "theta sigma gamma" 1); - -by (rewrite_tac [MoreGeneral_def]); -by (rotate_tac ~3 1); -by (eres_inst_tac [("x","gamma")] allE 1); -by (Asm_full_simp_tac 1); -by (etac exE 1); -by (rename_tac "delta" 1); -by (eres_inst_tac [("x","delta")] allE 1); -by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1); -by (dtac mp 1); -by (atac 1); -by (etac exE 1); -by (rename_tac "rho" 1); - -by (rtac exI 1); -by (rtac subst_trans 1); -by (assume_tac 1); - -by (rtac subst_trans 1); -by (rtac (comp_assoc RS subst_sym) 2); -by (rtac subst_cong 1); -by (rtac (refl RS subst_refl) 1); -by (assume_tac 1); - -by (asm_full_simp_tac (!simpset addsimps [subst_eq_iff,subst_comp]) 1); -by (forw_inst_tac [("x","N1")] spec 1); -by (dres_inst_tac [("x","N2")] spec 1); -by (Asm_full_simp_tac 1); -val Unify_gives_MGU = standard(result() RS spec RS mp); - - -(*--------------------------------------------------------------------------- - * Unify returns idempotent substitutions, when it succeeds. - *---------------------------------------------------------------------------*) -goal theory "!theta. Unify (P,Q) = Subst theta --> Idem theta"; -by (res_inst_tac [("xa","P"),("x","Q")] - (standard (Unify_induction RS mp RS spec RS spec)) 1); -(* Blows away all base cases automatically *) -by (simp_tac (!simpset addsimps [Unify_rules,Idem_Nil,Var_Idem] - setloop (split_tac [expand_if])) 1); - -(*7*) -by (safe_tac HOL_cs); -by (Subst_case_tac [("v","Unify(M1, M2)")]); -by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]); -by (hyp_subst_tac 1); -by prune_params_tac; -by (rename_tac "theta sigma" 1); - -by (dtac Unify_gives_MGU 1); -by (dtac Unify_gives_MGU 1); -by (rewrite_tac [MGUnifier_def]); -by (my_strip_tac 1); -by (rtac Idem_comp 1); -by (atac 1); -by (atac 1); - -by (my_strip_tac 1); -by (eres_inst_tac [("x","q")] allE 1); -by (Asm_full_simp_tac 1); -by (rewrite_tac [MoreGeneral_def]); -by (my_strip_tac 1); -by (asm_full_simp_tac(termin_ss addsimps [subst_eq_iff,subst_comp,Idem_def])1); -val Unify_gives_Idem = result() RS spec RS mp; - - - -(*--------------------------------------------------------------------------- - * Exercise. The given algorithm is a bit inelegant. What about the - * following "improvement", which adds a few recursive calls in former - * base cases? It seems that the termination relation needs another - * case in the lexico. product. - -val {theory,induction,rules,tcs,typechecks} = -Rfunc Unify.thy ?? - `(Unify(Const m, Const n) = (if (m=n) then Subst[] else Fail)) & - (Unify(Const m, Comb M N) = Fail) & - (Unify(Const m, Var v) = Unify(Var v, Const m)) & - (Unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])) & - (Unify(Comb M N, Const x) = Fail) & - (Unify(Comb M N, Var v) = Unify(Var v, Comb M N)) & - (Unify(Comb M1 N1, Comb M2 N2) = - (case Unify(M1,M2) - of Fail => Fail - | Subst theta => (case Unify(N1 <| theta, N2 <| theta) - of Fail => Fail - | Subst sigma => Subst (theta <> sigma))))`; - - *---------------------------------------------------------------------------*) diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/Unify.thy --- a/TFL/examples/Subst/Unify.thy Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ -Unify = Unifier + WF1 + "NNF" + - -datatype 'a subst = Fail | Subst ('a list) - -consts - - "##" :: "('a => 'b) => ('a => 'c) => 'a => ('b * 'c)" (infixr 50) - R0 :: "('a set * 'a set) set" - R1 :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" - R :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" - - -rules - - point_to_prod_def "(f ## g) x == (f x, g x)" - - (* finite proper subset -- should go in WF1.thy maybe *) - R0_def "R0 == {p. fst p < snd p & finite(snd p)}" - - R1_def "R1 == rprod (measure uterm_size) (measure uterm_size)" - - (* The termination relation for the Unify function *) - R_def "R == inv_image (R0 ** R1) - ((%(x,y). vars_of x Un vars_of y) ## (%x.x))" - -end diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/Unify1.ML --- a/TFL/examples/Subst/Unify1.ML Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,637 +0,0 @@ -(*--------------------------------------------------------------------------- - * This file defines a nested unification algorithm, then proves that it - * terminates, then proves 2 correctness theorems: that when the algorithm - * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution. - * Although the proofs may seem long, they are actually quite direct, in that - * the correctness and termination properties are not mingled as much as in - * previous proofs of this algorithm. - * - * Our approach for nested recursive functions is as follows: - * - * 0. Prove the wellfoundedness of the termination relation. - * 1. Prove the non-nested termination conditions. - * 2. Eliminate (0) and (1) from the recursion equations and the - * induction theorem. - * 3. Prove the nested termination conditions by using the induction - * theorem from (2) and by using the recursion equations from (2). - * These are constrained by the nested termination conditions, but - * things work out magically (by wellfoundedness of the termination - * relation). - * 4. Eliminate the nested TCs from the results of (2). - * 5. Prove further correctness properties using the results of (4). - * - * Deeper nestings require iteration of steps (3) and (4). - *---------------------------------------------------------------------------*) - -Thry.add_datatype_facts - (UTerm.thy, ("uterm",["Var", "Const", "Comb"]), uterm.induct_tac); - -Thry.add_datatype_facts - (Unify1.thy, ("subst",["Fail", "Subst"]), Unify1.subst.induct_tac); - -(* This is just a wrapper for the definition mechanism. *) -local fun cread thy s = read_cterm (sign_of thy) (s, (TVar(("DUMMY",0),[]))); -in -fun Rfunc thy R eqs = - let val _ = reset_count() - val _ = tych_counting true - val read = term_of o cread thy; - val {induction,rules,theory,tcs} = Tfl.Rfunction thy (read R) (read eqs) - in {induction=induction, rules=rules, theory=theory, - typechecks = count(), tcs = tcs} - end -end; - -(*--------------------------------------------------------------------------- - * The algorithm. - *---------------------------------------------------------------------------*) -val {theory,induction,rules,tcs,typechecks} = -Rfunc Unify1.thy "R" - "(Unify(Const m, Const n) = (if (m=n) then Subst[] else Fail)) & \ -\ (Unify(Const m, Comb M N) = Fail) & \ -\ (Unify(Const m, Var v) = Subst[(v,Const m)]) & \ -\ (Unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])) & \ -\ (Unify(Comb M N, Const x) = Fail) & \ -\ (Unify(Comb M N, Var v) = (if (Var v <: Comb M N) then Fail \ -\ else Subst[(v,Comb M N)])) & \ -\ (Unify(Comb M1 N1, Comb M2 N2) = \ -\ (case Unify(M1,M2) \ -\ of Fail => Fail \ -\ | Subst theta => (case Unify(N1 <| theta, N2 <| theta) \ -\ of Fail => Fail \ -\ | Subst sigma => Subst (theta <> sigma))))"; - - - -open Unify1; - -(*--------------------------------------------------------------------------- - * A slightly augmented strip_tac. - *---------------------------------------------------------------------------*) -(* Needs a correct "CHANGED" to work! This one taken from Carsten's version. *) -(*Returns all changed states*) -fun CHANGED tac st = - let fun diff st' = not (eq_thm(st,st')) - in Sequence.filters diff (tac st) end; - -fun my_strip_tac i = - CHANGED (strip_tac i - THEN REPEAT ((etac exE ORELSE' etac conjE) i) - THEN TRY (hyp_subst_tac i)); - -(*--------------------------------------------------------------------------- - * A slightly augmented fast_tac for sets. It handles the case where the - * top connective is "=". - *---------------------------------------------------------------------------*) -fun my_fast_set_tac i = (TRY(rtac set_ext i) THEN fast_tac set_cs i); - - -(*--------------------------------------------------------------------------- - * Wellfoundedness of proper subset on finite sets. - *---------------------------------------------------------------------------*) -goalw Unify1.thy [R0_def] "wf(R0)"; -by (rtac ((wf_subset RS mp) RS mp) 1); -by (rtac wf_measure 1); -by(simp_tac(!simpset addsimps[measure_def,inv_image_def,symmetric less_def])1); -by (my_strip_tac 1); -by (forward_tac[ssubset_card] 1); -by (fast_tac set_cs 1); -val wf_R0 = result(); - - -(*--------------------------------------------------------------------------- - * Tactic for selecting and working on the first projection of R. - *---------------------------------------------------------------------------*) -fun R0_tac thms i = - (simp_tac (!simpset addsimps (thms@[R_def,lex_prod_def, - measure_def,inv_image_def,point_to_prod_def])) i THEN - REPEAT (rtac exI i) THEN - REPEAT ((rtac conjI THEN' rtac refl) i) THEN - rtac disjI1 i THEN - simp_tac (!simpset addsimps [R0_def,finite_vars_of]) i); - - - -(*--------------------------------------------------------------------------- - * Tactic for selecting and working on the second projection of R. - *---------------------------------------------------------------------------*) -fun R1_tac thms i = - (simp_tac (!simpset addsimps (thms@[R_def,lex_prod_def, - measure_def,inv_image_def,point_to_prod_def])) i THEN - REPEAT (rtac exI i) THEN - REPEAT ((rtac conjI THEN' rtac refl) i) THEN - rtac disjI2 i THEN - asm_simp_tac (!simpset addsimps [R1_def,rprod_def]) i); - - -(*--------------------------------------------------------------------------- - * The non-nested TC plus the wellfoundedness of R. - *---------------------------------------------------------------------------*) -tgoalw Unify1.thy [] rules; -by (rtac conjI 1); -(* TC *) -by (my_strip_tac 1); -by (cut_facts_tac [monotone_vars_of] 1); -by (asm_full_simp_tac(!simpset addsimps [subseteq_iff_subset_eq]) 1); -by (etac disjE 1); -by (R0_tac[] 1); -by (R1_tac[] 1); -by (REPEAT (rtac exI 1) THEN REPEAT ((rtac conjI THEN' rtac refl) 1)); -by (simp_tac - (!simpset addsimps [measure_def,inv_image_def,less_eq,less_add_Suc1]) 1); - -(* Wellfoundedness of R *) -by (simp_tac (!simpset addsimps [Unify1.R_def,Unify1.R1_def]) 1); -by (REPEAT (resolve_tac [wf_inv_image,wf_lex_prod,wf_R0, - wf_rel_prod, wf_measure] 1)); -val tc0 = result(); - - -(*--------------------------------------------------------------------------- - * Eliminate tc0 from the recursion equations and the induction theorem. - *---------------------------------------------------------------------------*) -val [tc,wfr] = Prim.Rules.CONJUNCTS tc0; -val rules1 = implies_intr_hyps rules; -val rules2 = wfr RS rules1; - -val [a,b,c,d,e,f,g] = Prim.Rules.CONJUNCTS rules2; -val g' = tc RS (g RS mp); -val rules4 = standard (Prim.Rules.LIST_CONJ[a,b,c,d,e,f,g']); - -val induction1 = implies_intr_hyps induction; -val induction2 = wfr RS induction1; -val induction3 = tc RS induction2; - -val induction4 = standard - (rewrite_rule[fst_conv RS eq_reflection, snd_conv RS eq_reflection] - (induction3 RS (read_instantiate_sg (sign_of theory) - [("x","%p. Phi (fst p) (snd p)")] spec))); - - -(*--------------------------------------------------------------------------- - * Some theorems about transitivity of WF combinators. Only the last - * (transR) is used, in the proof of termination. The others are generic and - * should maybe go somewhere. - *---------------------------------------------------------------------------*) -goalw WF1.thy [trans_def,lex_prod_def,mem_Collect_eq RS eq_reflection] - "trans R1 & trans R2 --> trans (R1 ** R2)"; -by (my_strip_tac 1); -by (res_inst_tac [("x","a")] exI 1); -by (res_inst_tac [("x","a'a")] exI 1); -by (res_inst_tac [("x","b")] exI 1); -by (res_inst_tac [("x","b'a")] exI 1); -by (REPEAT (rewrite_tac [Pair_eq RS eq_reflection] THEN my_strip_tac 1)); -by (Simp_tac 1); -by (REPEAT (etac disjE 1)); -by (rtac disjI1 1); -by (ALLGOALS (fast_tac set_cs)); -val trans_lex_prod = result() RS mp; - - -goalw WF1.thy [trans_def,rprod_def,mem_Collect_eq RS eq_reflection] - "trans R1 & trans R2 --> trans (rprod R1 R2)"; -by (my_strip_tac 1); -by (res_inst_tac [("x","a")] exI 1); -by (res_inst_tac [("x","a'a")] exI 1); -by (res_inst_tac [("x","b")] exI 1); -by (res_inst_tac [("x","b'a")] exI 1); -by (REPEAT (rewrite_tac [Pair_eq RS eq_reflection] THEN my_strip_tac 1)); -by (Simp_tac 1); -by (fast_tac set_cs 1); -val trans_rprod = result() RS mp; - - -goalw Unify1.thy [trans_def,inv_image_def,mem_Collect_eq RS eq_reflection] - "trans r --> trans (inv_image r f)"; -by (rewrite_tac [fst_conv RS eq_reflection, snd_conv RS eq_reflection]); -by (fast_tac set_cs 1); -val trans_inv_image = result() RS mp; - -goalw Unify1.thy [R0_def, trans_def, mem_Collect_eq RS eq_reflection] - "trans R0"; -by (rewrite_tac [fst_conv RS eq_reflection,snd_conv RS eq_reflection, - ssubset_def, set_eq_subset RS eq_reflection]); -by (fast_tac set_cs 1); -val trans_R0 = result(); - -goalw Unify1.thy [R_def,R1_def,measure_def] "trans R"; -by (REPEAT (resolve_tac[trans_inv_image,trans_lex_prod,conjI, trans_R0, - trans_rprod, trans_inv_image, trans_trancl] 1)); -val transR = result(); - - -(*--------------------------------------------------------------------------- - * The following lemma is used in the last step of the termination proof for - * the nested call in Unify. Loosely, it says that R doesn't care so much - * about term structure. - *---------------------------------------------------------------------------*) -goalw Unify1.thy [R_def,lex_prod_def, inv_image_def,point_to_prod_def] - "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : R --> \ - \ ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : R"; -by (Simp_tac 1); -by (my_strip_tac 1); -by (REPEAT (rtac exI 1) THEN REPEAT ((rtac conjI THEN' rtac refl) 1)); -by (etac disjE 1); -by (rtac disjI1 1); -by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \ - \ (vars_of D Un vars_of E Un vars_of F)) = \ - \ (vars_of A Un (vars_of B Un vars_of C) Un \ - \ (vars_of D Un (vars_of E Un vars_of F)))" 1); -by (my_fast_set_tac 2); -by (Asm_simp_tac 1); -by (rtac disjI2 1); -by (etac conjE 1); -by (Asm_simp_tac 1); -by (rtac conjI 1); -by (my_fast_set_tac 1); -by (asm_full_simp_tac (!simpset addsimps [R1_def, measure_def, rprod_def, - less_eq, inv_image_def]) 1); -by (my_strip_tac 1); -by (REPEAT (rtac exI 1) THEN REPEAT ((rtac conjI THEN' rtac refl) 1)); -by (asm_full_simp_tac (HOL_ss addsimps [uterm_size_Comb, - add_Suc_right,add_Suc,add_assoc]) 1); -val Rassoc = result() RS mp; - - -(*--------------------------------------------------------------------------- - * Rewriting support. - *---------------------------------------------------------------------------*) - -val termin_ss = (!simpset addsimps (srange_iff::(subst_rews@al_rews))); - - -(*--------------------------------------------------------------------------- - * This lemma proves the nested termination condition for the base cases - * 3, 4, and 6. It's a clumsy formulation (requiring two conjuncts, each with - * exactly the same proof) of a more general theorem. - *---------------------------------------------------------------------------*) -goal theory "(~(Var x <: M)) --> [(x, M)] = theta --> \ -\ (! N1 N2. (((N1 <| theta, N2 <| theta), (Comb M N1, Comb (Var x) N2)) : R) \ -\ & (((N1 <| theta, N2 <| theta), (Comb(Var x) N1, Comb M N2)) : R))"; -by (my_strip_tac 1); -by (case_tac "Var x = M" 1); -by (hyp_subst_tac 1); -by (case_tac "x:(vars_of N1 Un vars_of N2)" 1); -let val case1 = - EVERY1[R1_tac[id_subst_lemma], rtac conjI, my_fast_set_tac, - REPEAT o (rtac exI), REPEAT o (rtac conjI THEN' rtac refl), - simp_tac (!simpset addsimps [measure_def,inv_image_def,less_eq])]; -in by (rtac conjI 1); - by case1; - by case1 -end; - -let val case2 = - EVERY1[R0_tac[id_subst_lemma], - simp_tac (!simpset addsimps [ssubset_def,set_eq_subset]), - fast_tac set_cs] -in by (rtac conjI 1); - by case2; - by case2 -end; - -let val case3 = - EVERY1 [R0_tac[], - cut_inst_tac [("s2","[(x, M)]"), ("v2", "x"), ("t2","N1")] Var_elim] - THEN ALLGOALS(asm_simp_tac(termin_ss addsimps [vars_iff_occseq])) - THEN cut_inst_tac [("s2","[(x, M)]"),("v2", "x"), ("t2","N2")] Var_elim 1 - THEN ALLGOALS(asm_simp_tac(termin_ss addsimps [vars_iff_occseq])) - THEN EVERY1 [simp_tac (HOL_ss addsimps [ssubset_def]), - rtac conjI, simp_tac (HOL_ss addsimps [subset_iff]), - my_strip_tac, etac UnE, dtac Var_intro] - THEN dtac Var_intro 2 - THEN ALLGOALS (asm_full_simp_tac (termin_ss addsimps [set_eq_subset])) - THEN TRYALL (fast_tac set_cs) -in - by (rtac conjI 1); - by case3; - by case3 -end; -val var_elimR = result() RS mp RS mp RS spec RS spec; - - -val Some{nchotomy = subst_nchotomy,...} = - assoc(Thry.datatype_facts theory,"subst"); - -(*--------------------------------------------------------------------------- - * Do a case analysis on something of type 'a subst. - *---------------------------------------------------------------------------*) - -fun Subst_case_tac theta = -(cut_inst_tac theta (standard (Prim.Rules.SPEC_ALL subst_nchotomy)) 1 - THEN etac disjE 1 - THEN rotate_tac ~1 1 - THEN Asm_full_simp_tac 1 - THEN etac exE 1 - THEN rotate_tac ~1 1 - THEN Asm_full_simp_tac 1); - - -goals_limit := 1; - -(*--------------------------------------------------------------------------- - * The nested TC. Proved by recursion induction. - *---------------------------------------------------------------------------*) -goalw_cterm [] - (hd(tl(tl(map (cterm_of (sign_of theory) o USyntax.mk_prop) tcs)))); -(*--------------------------------------------------------------------------- - * The extracted TC needs the scope of its quantifiers adjusted, so our - * first step is to restrict the scopes of N1 and N2. - *---------------------------------------------------------------------------*) -by (subgoal_tac "!M1 M2 theta. \ - \ Unify (M1, M2) = Subst theta --> \ - \ (!N1 N2. ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R)" 1); -by (fast_tac HOL_cs 1); -by (rtac allI 1); -by (rtac allI 1); -(* Apply induction *) -by (res_inst_tac [("xa","M1"),("x","M2")] - (standard (induction4 RS mp RS spec RS spec)) 1); -by (simp_tac (!simpset addsimps (rules4::(subst_rews@al_rews)) - setloop (split_tac [expand_if])) 1); -(* 1 *) -by (rtac conjI 1); -by (my_strip_tac 1); -by (R1_tac[subst_Nil] 1); -by (REPEAT (rtac exI 1) THEN REPEAT ((rtac conjI THEN' rtac refl) 1)); -by (simp_tac (!simpset addsimps [measure_def,inv_image_def,less_eq]) 1); - -(* 3 *) -by (rtac conjI 1); -by (my_strip_tac 1); -by (rtac (Prim.Rules.CONJUNCT1 var_elimR) 1); -by (Simp_tac 1); -by (rtac refl 1); - -(* 4 *) -by (rtac conjI 1); -by (strip_tac 1); -by (rtac (Prim.Rules.CONJUNCT2 var_elimR) 1); -by (assume_tac 1); -by (assume_tac 1); - -(* 6 *) -by (rtac conjI 1); -by (rewrite_tac [symmetric (occs_Comb RS eq_reflection)]); -by (my_strip_tac 1); -by (rtac (Prim.Rules.CONJUNCT1 var_elimR) 1); -by (assume_tac 1); -by (rtac refl 1); - -(* 7 *) -by (REPEAT (rtac allI 1)); -by (rtac impI 1); -by (etac conjE 1); -by (Subst_case_tac [("v","Unify(M1a, M2a)")]); -by (REPEAT (eres_inst_tac [("x","list")] allE 1)); -by (asm_full_simp_tac HOL_ss 1); -by (subgoal_tac "((N1 <| list, N2 <| list), Comb M1a N1, Comb M2a N2) : R" 1); -by (asm_simp_tac HOL_ss 2); -by (dtac mp 1); -by (assume_tac 1); - -by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]); -by (eres_inst_tac [("x","lista")] allE 1); -by (asm_full_simp_tac HOL_ss 1); - -by (rtac allI 1); -by (rtac impI 1); - -by (hyp_subst_tac 1); -by (REPEAT (rtac allI 1)); -by (rename_tac "foo bar M1 N1 M2 N2 theta sigma gamma P1 P2" 1); -by (simp_tac (HOL_ss addsimps [subst_comp]) 1); -by(rtac(rewrite_rule[trans_def] transR RS spec RS spec RS spec RS mp RS mp) 1); -by (fast_tac HOL_cs 1); -by (simp_tac (HOL_ss addsimps [symmetric (subst_Comb RS eq_reflection)]) 1); -by (subgoal_tac "((Comb N1 P1 <| theta, Comb N2 P2 <| theta), \ - \ (Comb M1 (Comb N1 P1), Comb M2 (Comb N2 P2))) :R" 1); -by (asm_simp_tac HOL_ss 2); -by (rtac Rassoc 1); -by (assume_tac 1); -val Unify_TC2 = result(); - - -(*--------------------------------------------------------------------------- - * Now for elimination of nested TC from rules and induction. This step - * would be easier if "rewrite_rule" used context. - *---------------------------------------------------------------------------*) -goal theory - "(Unify (Comb M1 N1, Comb M2 N2) = \ -\ (case Unify (M1, M2) of Fail => Fail \ -\ | Subst theta => \ -\ (case if ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R \ -\ then Unify (N1 <| theta, N2 <| theta) else @ z. True of \ -\ Fail => Fail | Subst sigma => Subst (theta <> sigma)))) \ -\ = \ -\ (Unify (Comb M1 N1, Comb M2 N2) = \ -\ (case Unify (M1, M2) \ -\ of Fail => Fail \ -\ | Subst theta => (case Unify (N1 <| theta, N2 <| theta) \ -\ of Fail => Fail \ -\ | Subst sigma => Subst (theta <> sigma))))"; -by (cut_inst_tac [("v","Unify(M1, M2)")] - (standard (Prim.Rules.SPEC_ALL subst_nchotomy)) 1); -by (etac disjE 1); -by (Asm_simp_tac 1); -by (etac exE 1); -by (Asm_simp_tac 1); -by (cut_inst_tac - [("x","list"), ("xb","N1"), ("xa","N2"),("xc","M2"), ("xd","M1")] - (standard(Unify_TC2 RS spec RS spec RS spec RS spec RS spec)) 1); -by (Asm_full_simp_tac 1); -val Unify_rec_simpl = result() RS eq_reflection; - -val Unify_rules = rewrite_rule[Unify_rec_simpl] rules4; - - -goal theory - "(! M1 N1 M2 N2. \ -\ (! theta. \ -\ Unify (M1, M2) = Subst theta --> \ -\ ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) : R --> \ -\ ?Phi (N1 <| theta) (N2 <| theta)) & ?Phi M1 M2 --> \ -\ ?Phi (Comb M1 N1) (Comb M2 N2)) \ -\ = \ -\ (! M1 N1 M2 N2. \ -\ (! theta. \ -\ Unify (M1, M2) = Subst theta --> \ -\ ?Phi (N1 <| theta) (N2 <| theta)) & ?Phi M1 M2 --> \ -\ ?Phi (Comb M1 N1) (Comb M2 N2))"; -by (simp_tac (HOL_ss addsimps [Unify_TC2]) 1); -val Unify_induction = rewrite_rule[result() RS eq_reflection] induction4; - - - -(*--------------------------------------------------------------------------- - * Correctness. Notice that idempotence is not needed to prove that the - * algorithm terminates and is not needed to prove the algorithm correct, - * if you are only interested in an MGU. This is in contrast to the - * approach of M&W, who used idempotence and MGU-ness in the termination proof. - *---------------------------------------------------------------------------*) - -goal theory "!theta. Unify (P,Q) = Subst theta --> MGUnifier theta P Q"; -by (res_inst_tac [("xa","P"),("x","Q")] - (standard (Unify_induction RS mp RS spec RS spec)) 1); -by (simp_tac (!simpset addsimps [Unify_rules] - setloop (split_tac [expand_if])) 1); -(*1*) -by (rtac conjI 1); -by (REPEAT (rtac allI 1)); -by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1); -by (my_strip_tac 1); -by (rtac MoreGen_Nil 1); - -(*3*) -by (rtac conjI 1); -by (my_strip_tac 1); -by (rtac (mgu_sym RS iffD1) 1); -by (rtac MGUnifier_Var 1); -by (Simp_tac 1); - -(*4*) -by (rtac conjI 1); -by (my_strip_tac 1); -by (rtac MGUnifier_Var 1); -by (assume_tac 1); - -(*6*) -by (rtac conjI 1); -by (rewrite_tac NNF_rews); -by (my_strip_tac 1); -by (rtac (mgu_sym RS iffD1) 1); -by (rtac MGUnifier_Var 1); -by (Asm_simp_tac 1); - -(*7*) -by (safe_tac HOL_cs); -by (Subst_case_tac [("v","Unify(M1, M2)")]); -by (REPEAT (eres_inst_tac[("x","list")] allE 1)); -by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]); -by (eres_inst_tac[("x","lista")] allE 1); -by (Asm_full_simp_tac 1); -by (hyp_subst_tac 1); -by prune_params_tac; -by (rename_tac "M1 N1 M2 N2 theta sigma" 1); - -by (asm_full_simp_tac(HOL_ss addsimps [MGUnifier_def,Unifier_def])1); -by (rtac conjI 1); -by (asm_simp_tac (!simpset addsimps [subst_comp]) 1); (* It's a unifier.*) -by (Simp_tac 1); -by (safe_tac HOL_cs); -by (rename_tac "M1 N1 M2 N2 theta sigma gamma" 1); - -by (rewrite_tac [MoreGeneral_def]); -by (eres_inst_tac [("x","gamma")] allE 1); -by (Asm_full_simp_tac 1); -by (etac exE 1); -by (rename_tac "M1 N1 M2 N2 theta sigma gamma theta1" 1); -by (eres_inst_tac [("x","theta1")] allE 1); -by (subgoal_tac "N1 <| theta <| theta1 = N2 <| theta <| theta1" 1); - -by (simp_tac (HOL_ss addsimps [subst_comp RS sym]) 2); -by (rtac subst_subst2 2); -by (assume_tac 3); -by (assume_tac 2); - -by (dtac mp 1); -by (assume_tac 1); -by (etac exE 1); - -by (rename_tac "M1 N1 M2 N2 theta sigma gamma theta1 sigma1" 1); -by (res_inst_tac [("x","sigma1")] exI 1); -by (rtac subst_trans 1); -by (assume_tac 1); -by (rtac subst_trans 1); -by (rtac subst_sym 2); -by (rtac comp_assoc 2); -by (rtac subst_cong 1); -by (assume_tac 2); -by (simp_tac (HOL_ss addsimps [subst_eq_def]) 1); -val Unify_gives_MGU = standard(result() RS spec RS mp); - - -(*--------------------------------------------------------------------------- - * Unify returns idempotent substitutions, when it succeeds. - *---------------------------------------------------------------------------*) -goal theory "!theta. Unify (P,Q) = Subst theta --> Idem theta"; -by (res_inst_tac [("xa","P"),("x","Q")] - (standard (Unify_induction RS mp RS spec RS spec)) 1); -by (simp_tac (!simpset addsimps [Unify_rules] - setloop (split_tac [expand_if])) 1); -(*1*) -by (rtac conjI 1); -by (my_strip_tac 1); -by (rtac Idem_Nil 1); - -(*3*) -by (rtac conjI 1); -by (my_strip_tac 1); -by (rtac Var_Idem 1); -by (Simp_tac 1); - -(*4*) -by (rtac conjI 1); -by (my_strip_tac 1); -by (rtac Var_Idem 1); -by (atac 1); - -(*6*) -by (rtac conjI 1); -by (rewrite_tac [symmetric (occs_Comb RS eq_reflection)]); -by (my_strip_tac 1); -by (rtac Var_Idem 1); -by (atac 1); - -(*7*) -by (safe_tac HOL_cs); -by (Subst_case_tac [("v","Unify(M1, M2)")]); -by (REPEAT (eres_inst_tac[("x","list")] allE 1)); -by (Subst_case_tac [("v","Unify(N1 <| list, N2 <| list)")]); -by (eres_inst_tac[("x","lista")] allE 1); -by (Asm_full_simp_tac 1); -by (hyp_subst_tac 1); -by prune_params_tac; -by (rename_tac "M1 N1 M2 N2 theta sigma" 1); - -by (dtac Unify_gives_MGU 1); -by (dtac Unify_gives_MGU 1); -by (rewrite_tac [MGUnifier_def]); -by (my_strip_tac 1); -by (rtac Idem_comp 1); -by (atac 1); -by (atac 1); - -by (rewrite_tac [MGUnifier_def]); -by (my_strip_tac 1); -by (eres_inst_tac [("x","q")] allE 1); -by (Asm_full_simp_tac 1); -by (rewrite_tac [MoreGeneral_def]); -by (my_strip_tac 1); -by (asm_full_simp_tac(termin_ss addsimps [subst_eq_iff,subst_comp,Idem_def])1); -val Unify_gives_Idem = result(); - - - -(*--------------------------------------------------------------------------- - * Exercise. The given algorithm is a bit inelegant. What about the - * following "improvement", which adds a few recursive calls in former - * base cases? It seems that the termination relation needs another - * case in the lexico. product. - -val {theory,induction,rules,tcs,typechecks} = -Rfunc Unify.thy ?? - `(Unify(Const m, Const n) = (if (m=n) then Subst[] else Fail)) & - (Unify(Const m, Comb M N) = Fail) & - (Unify(Const m, Var v) = Unify(Var v, Const m)) & - (Unify(Var v, M) = (if (Var v <: M) then Fail else Subst[(v,M)])) & - (Unify(Comb M N, Const x) = Fail) & - (Unify(Comb M N, Var v) = Unify(Var v, Comb M N)) & - (Unify(Comb M1 N1, Comb M2 N2) = - (case Unify(M1,M2) - of Fail => Fail - | Subst theta => (case Unify(N1 <| theta, N2 <| theta) - of Fail => Fail - | Subst sigma => Subst (theta <> sigma))))`; - - *---------------------------------------------------------------------------*) diff -r fe79ad367d77 -r 8336393de482 TFL/examples/Subst/Unify1.thy --- a/TFL/examples/Subst/Unify1.thy Thu May 15 15:51:47 1997 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ -Unify1 = Unifier + WF1 + "NNF" + - -datatype 'a subst = Fail | Subst ('a list) - -consts - - "##" :: "('a => 'b) => ('a => 'c) => 'a => ('b * 'c)" (infixr 50) - R0 :: "('a set * 'a set) set" - R1 :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" - R :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" - - -rules - - point_to_prod_def "(f ## g) x == (f x, g x)" - - (* finite proper subset -- should go in WF1.thy maybe *) - R0_def "R0 == {p. fst p < snd p & finite(snd p)}" - - R1_def "R1 == rprod (measure uterm_size) (measure uterm_size)" - - (* The termination relation for the Unify function *) - R_def "R == inv_image (R0 ** R1) - ((%(x,y). vars_of x Un vars_of y) ## (%x.x))" - -end diff -r fe79ad367d77 -r 8336393de482 TFL/post.sml --- a/TFL/post.sml Thu May 15 15:51:47 1997 +0200 +++ b/TFL/post.sml Fri May 16 10:43:44 1997 +0200 @@ -58,21 +58,19 @@ * Simple wellfoundedness prover. *--------------------------------------------------------------------------*) fun WF_TAC thms = REPEAT(FIRST1(map rtac thms)) - val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, + val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, wf_less_than, wf_pred_nat, wf_pred_list, wf_trancl]; - val terminator = simp_tac(HOL_ss addsimps[pred_nat_def,pred_list_def, - fst_conv,snd_conv, - mem_Collect_eq,lessI]) 1 - THEN TRY(fast_tac set_cs 1); - -val length_Cons = prove_goal List.thy "length(h#t) = Suc(length t)" - (fn _ => [Simp_tac 1]); + val terminator = simp_tac(!simpset addsimps [less_than_def, pred_nat_def, + pred_list_def]) 1 + THEN TRY(best_tac + (!claset addSDs [not0_implies_Suc] + addIs [r_into_trancl, + trans_trancl RS transD] + addss (!simpset)) 1); val simpls = [less_eq RS eq_reflection, - lex_prod_def, measure_def, inv_image_def, - fst_conv RS eq_reflection, snd_conv RS eq_reflection, - mem_Collect_eq RS eq_reflection, length_Cons RS eq_reflection]; + lex_prod_def, rprod_def, measure_def, inv_image_def]; (*--------------------------------------------------------------------------- * Does some standard things with the termination conditions of a definition: @@ -84,8 +82,8 @@ terminator = terminator, simplifier = Prim.Rules.simpl_conv simpls}; - val simplifier = rewrite_rule (simpls @ #simps(rep_ss HOL_ss) @ - [pred_nat_def,pred_list_def]); + val simplifier = rewrite_rule (simpls @ #simps(rep_ss (!simpset)) @ + [less_than_def, pred_nat_def, pred_list_def]); fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy)); @@ -198,7 +196,10 @@ fun simplify_defn (thy,(id,pats)) = - let val def = freezeT(get_def thy id RS meta_eq_to_obj_eq) + let val dummy = deny (id mem map ! (stamps_of_thy thy)) + ("Recursive definition " ^ id ^ + " would clash with the theory of the same name!") + val def = freezeT(get_def thy id RS meta_eq_to_obj_eq) val {theory,rules,TCs,full_pats_TCs,patterns} = Prim.post_definition (thy,(def,pats)) val {lhs=f,rhs} = S.dest_eq(concl def) @@ -225,17 +226,16 @@ * inference at theory-construction time. * -local fun floutput s = (output(std_out,s); flush_out std_out) - structure R = Prim.Rules +local structure R = Prim.Rules in fun function theory eqs = - let val dummy = floutput "Making definition.. " + let val dummy = prs "Making definition.. " val {rules,R,theory,full_pats_TCs,...} = Prim.lazyR_def theory eqs val f = func_of_cond_eqn (concl(R.CONJUNCT1 rules handle _ => rules)) - val dummy = floutput "Definition made.\n" - val dummy = floutput "Proving induction theorem.. " + val dummy = prs "Definition made.\n" + val dummy = prs "Proving induction theorem.. " val induction = Prim.mk_induction theory f R full_pats_TCs - val dummy = floutput "Induction theorem proved.\n" + val dummy = prs "Induction theorem proved.\n" in {theory = theory, eq_ind = standard (induction RS (rules RS conjI))} end