--- 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)];
--- 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
--- 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()))
-
--- 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
--- 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.
--- 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";
--- 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";
--- 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();
-
-
--- 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
--- 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();
--- 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
--- 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();
--- 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
--- 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";
-
--- 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
--- 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))))`;
-
- *---------------------------------------------------------------------------*)
--- 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
--- 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))))`;
-
- *---------------------------------------------------------------------------*)
--- 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
--- 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