converted HOL-Subst to tactic scripts
authorpaulson
Tue Mar 29 12:30:48 2005 +0200 (2005-03-29)
changeset 156358408a06590a6
parent 15634 bca33c49b083
child 15636 57c437b70521
converted HOL-Subst to tactic scripts
src/HOL/IsaMakefile
src/HOL/Subst/AList.ML
src/HOL/Subst/AList.thy
src/HOL/Subst/Subst.ML
src/HOL/Subst/Subst.thy
src/HOL/Subst/UTerm.ML
src/HOL/Subst/UTerm.thy
src/HOL/Subst/Unifier.ML
src/HOL/Subst/Unifier.thy
src/HOL/Subst/Unify.ML
src/HOL/Subst/Unify.thy
     1.1 --- a/src/HOL/IsaMakefile	Mon Mar 28 16:19:56 2005 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Mar 29 12:30:48 2005 +0200
     1.3 @@ -191,9 +191,8 @@
     1.4  
     1.5  HOL-Subst: HOL $(LOG)/HOL-Subst.gz
     1.6  
     1.7 -$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.ML Subst/AList.thy \
     1.8 -  Subst/ROOT.ML Subst/Subst.ML Subst/Subst.thy Subst/UTerm.ML \
     1.9 -  Subst/UTerm.thy Subst/Unifier.ML Subst/Unifier.thy Subst/Unify.ML \
    1.10 +$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy \
    1.11 +  Subst/ROOT.ML Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy \
    1.12    Subst/Unify.thy
    1.13  	@$(ISATOOL) usedir $(OUT)/HOL Subst
    1.14  
     2.1 --- a/src/HOL/Subst/AList.ML	Mon Mar 28 16:19:56 2005 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,22 +0,0 @@
     2.4 -(*  Title:      Subst/AList.ML
     2.5 -    ID:         $Id$
     2.6 -    Author:     Martin Coen, Cambridge University Computer Laboratory
     2.7 -    Copyright   1993  University of Cambridge
     2.8 -
     2.9 -Association lists.
    2.10 -*)
    2.11 -
    2.12 -open AList;
    2.13 -
    2.14 -val prems = goal AList.thy
    2.15 -    "[| P([]);   \
    2.16 -\       !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)";
    2.17 -by (induct_tac "l" 1);
    2.18 -by (split_all_tac 2);
    2.19 -by (REPEAT (ares_tac prems 1));
    2.20 -qed "alist_induct";
    2.21 -
    2.22 -(*Perform induction on xs. *)
    2.23 -fun alist_ind_tac a M = 
    2.24 -    EVERY [induct_thm_tac alist_induct a M,
    2.25 -           rename_last_tac a ["1"] (M+1)];
     3.1 --- a/src/HOL/Subst/AList.thy	Mon Mar 28 16:19:56 2005 +0200
     3.2 +++ b/src/HOL/Subst/AList.thy	Tue Mar 29 12:30:48 2005 +0200
     3.3 @@ -1,12 +1,14 @@
     3.4 -(*  Title:      Subst/AList.thy
     3.5 -    ID:         $Id$
     3.6 +(*  ID:         $Id$
     3.7      Author:     Martin Coen, Cambridge University Computer Laboratory
     3.8      Copyright   1993  University of Cambridge
     3.9  
    3.10 -Association lists.
    3.11  *)
    3.12  
    3.13 -AList = Main +
    3.14 +header{*Association Lists*}
    3.15 +
    3.16 +theory AList
    3.17 +imports Main
    3.18 +begin
    3.19  
    3.20  consts
    3.21    alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
    3.22 @@ -20,4 +22,10 @@
    3.23    "assoc v d [] = d"
    3.24    "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)"
    3.25  
    3.26 +
    3.27 +lemma alist_induct:
    3.28 +    "[| P([]);    
    3.29 +        !!x y xs. P(xs) ==> P((x,y)#xs) |]  ==> P(l)"
    3.30 +by (induct_tac "l", auto)
    3.31 +
    3.32  end
     4.1 --- a/src/HOL/Subst/Subst.ML	Mon Mar 28 16:19:56 2005 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,205 +0,0 @@
     4.4 -(*  Title:      HOL/Subst/Subst.ML
     4.5 -    ID:         $Id$
     4.6 -    Author:     Martin Coen, Cambridge University Computer Laboratory
     4.7 -    Copyright   1993  University of Cambridge
     4.8 -
     4.9 -Substitutions on uterms
    4.10 -*)
    4.11 -
    4.12 -open Subst;
    4.13 -
    4.14 -
    4.15 -(**** Substitutions ****)
    4.16 -
    4.17 -Goal "t <| [] = t";
    4.18 -by (induct_tac "t" 1);
    4.19 -by (ALLGOALS Asm_simp_tac);
    4.20 -qed "subst_Nil";
    4.21 -
    4.22 -Addsimps [subst_Nil];
    4.23 -
    4.24 -Goal "t <: u --> t <| s <: u <| s";
    4.25 -by (induct_tac "u" 1);
    4.26 -by (ALLGOALS Asm_simp_tac);
    4.27 -qed_spec_mp "subst_mono";
    4.28 -
    4.29 -Goal  "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s";
    4.30 -by (case_tac "t = Var(v)" 1);
    4.31 -by (etac rev_mp 2);
    4.32 -by (res_inst_tac [("P",
    4.33 -    "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")]
    4.34 -    uterm.induct 2);
    4.35 -by (ALLGOALS Asm_simp_tac);
    4.36 -by (Blast_tac 1);
    4.37 -qed_spec_mp "Var_not_occs";
    4.38 -
    4.39 -Goal "(t <|r = t <|s) = (! v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)";
    4.40 -by (induct_tac "t" 1);
    4.41 -by (ALLGOALS Asm_full_simp_tac);
    4.42 -by (ALLGOALS Blast_tac);
    4.43 -qed "agreement";
    4.44 -
    4.45 -Goal   "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
    4.46 -by (simp_tac (simpset() addsimps [agreement]) 1);
    4.47 -qed_spec_mp"repl_invariance";
    4.48 -
    4.49 -val asms = goal Subst.thy 
    4.50 -     "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)";
    4.51 -by (induct_tac "t" 1);
    4.52 -by (ALLGOALS Asm_simp_tac);
    4.53 -qed_spec_mp"Var_in_subst";
    4.54 -
    4.55 -
    4.56 -(**** Equality between Substitutions ****)
    4.57 -
    4.58 -Goalw [subst_eq_def] "r =$= s = (! t. t <| r = t <| s)";
    4.59 -by (Simp_tac 1);
    4.60 -qed "subst_eq_iff";
    4.61 -
    4.62 -
    4.63 -local fun prove s = prove_goal Subst.thy s
    4.64 -                  (fn prems => [cut_facts_tac prems 1,
    4.65 -                                REPEAT (etac rev_mp 1),
    4.66 -                                simp_tac (simpset() addsimps [subst_eq_iff]) 1])
    4.67 -in 
    4.68 -  val subst_refl      = prove "r =$= r";
    4.69 -  val subst_sym       = prove "r =$= s ==> s =$= r";
    4.70 -  val subst_trans     = prove "[| q =$= r; r =$= s |] ==> q =$= s";
    4.71 -end;
    4.72 -
    4.73 -
    4.74 -AddIffs [subst_refl];
    4.75 -
    4.76 -
    4.77 -val eq::prems = goalw Subst.thy [subst_eq_def] 
    4.78 -    "[| r =$= s; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)";
    4.79 -by (resolve_tac [eq RS spec RS subst] 1);
    4.80 -by (resolve_tac (prems RL [eq RS spec RS subst]) 1);
    4.81 -qed "subst_subst2";
    4.82 -
    4.83 -val ssubst_subst2 = subst_sym RS subst_subst2;
    4.84 -
    4.85 -(**** Composition of Substitutions ****)
    4.86 -
    4.87 -let fun prove s = 
    4.88 - prove_goalw Subst.thy [comp_def,sdom_def] s (fn _ => [Simp_tac 1])
    4.89 -in 
    4.90 -Addsimps
    4.91 - (
    4.92 -   map prove 
    4.93 -   [ "[] <> bl = bl",
    4.94 -     "((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)",
    4.95 -     "sdom([]) = {}",
    4.96 -     "sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else sdom al Un {a})"]
    4.97 - )
    4.98 -end;
    4.99 -
   4.100 -
   4.101 -Goal "s <> [] = s";
   4.102 -by (alist_ind_tac "s" 1);
   4.103 -by (ALLGOALS Asm_simp_tac);
   4.104 -qed "comp_Nil";
   4.105 -
   4.106 -Addsimps [comp_Nil];
   4.107 -
   4.108 -Goal "s =$= s <> []";
   4.109 -by (Simp_tac 1);
   4.110 -qed "subst_comp_Nil";
   4.111 -
   4.112 -Goal "(t <| r <> s) = (t <| r <| s)";
   4.113 -by (induct_tac "t" 1);
   4.114 -by (ALLGOALS Asm_simp_tac);
   4.115 -by (alist_ind_tac "r" 1);
   4.116 -by (ALLGOALS Asm_simp_tac);
   4.117 -qed "subst_comp";
   4.118 -
   4.119 -Addsimps [subst_comp];
   4.120 -
   4.121 -Goal "(q <> r) <> s =$= q <> (r <> s)";
   4.122 -by (simp_tac (simpset() addsimps [subst_eq_iff]) 1);
   4.123 -qed "comp_assoc";
   4.124 -
   4.125 -Goal "[| theta =$= theta1; sigma =$= sigma1|] ==> \
   4.126 -\     (theta <> sigma) =$= (theta1 <> sigma1)";
   4.127 -by (asm_full_simp_tac (simpset() addsimps [subst_eq_def]) 1);
   4.128 -qed "subst_cong";
   4.129 -
   4.130 -
   4.131 -Goal "(w, Var(w) <| s) # s =$= s"; 
   4.132 -by (simp_tac (simpset() addsimps [subst_eq_iff]) 1);
   4.133 -by (rtac allI 1);
   4.134 -by (induct_tac "t" 1);
   4.135 -by (ALLGOALS Asm_full_simp_tac);
   4.136 -qed "Cons_trivial";
   4.137 -
   4.138 -
   4.139 -Goal "q <> r =$= s ==>  t <| q <| r = t <| s";
   4.140 -by (asm_full_simp_tac (simpset() addsimps [subst_eq_iff]) 1);
   4.141 -qed "comp_subst_subst";
   4.142 -
   4.143 -
   4.144 -(****  Domain and range of Substitutions ****)
   4.145 -
   4.146 -Goal  "(v : sdom(s)) = (Var(v) <| s ~= Var(v))";
   4.147 -by (alist_ind_tac "s" 1);
   4.148 -by (ALLGOALS Asm_simp_tac);
   4.149 -by (Blast_tac 1);
   4.150 -qed "sdom_iff";
   4.151 -
   4.152 -
   4.153 -Goalw [srange_def]  
   4.154 -   "v : srange(s) = (? w. w : sdom(s) & v : vars_of(Var(w) <| s))";
   4.155 -by (Blast_tac 1);
   4.156 -qed "srange_iff";
   4.157 -
   4.158 -Goalw [empty_def] "(A = {}) = (ALL a.~ a:A)";
   4.159 -by (Blast_tac 1);
   4.160 -qed "empty_iff_all_not";
   4.161 -
   4.162 -Goal  "(t <| s = t) = (sdom(s) Int vars_of(t) = {})";
   4.163 -by (induct_tac "t" 1);
   4.164 -by (ALLGOALS
   4.165 -    (asm_full_simp_tac (simpset() addsimps [empty_iff_all_not, sdom_iff])));
   4.166 -by (ALLGOALS Blast_tac);
   4.167 -qed "invariance";
   4.168 -
   4.169 -Goal  "v : sdom(s) -->  v : vars_of(t <| s) --> v : srange(s)";
   4.170 -by (induct_tac "t" 1);
   4.171 -by (case_tac "a : sdom(s)" 1);
   4.172 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff, srange_iff])));
   4.173 -by (ALLGOALS Blast_tac);
   4.174 -qed_spec_mp "Var_in_srange";
   4.175 -
   4.176 -Goal "[| v : sdom(s); v ~: srange(s) |] ==>  v ~: vars_of(t <| s)";
   4.177 -by (blast_tac (claset() addIs [Var_in_srange]) 1);
   4.178 -qed "Var_elim";
   4.179 -
   4.180 -Goal "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)";
   4.181 -by (induct_tac "t" 1);
   4.182 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff,srange_iff])));
   4.183 -by (Blast_tac 2);
   4.184 -by (safe_tac (claset() addSIs [exI, vars_var_iff RS iffD1 RS sym]));
   4.185 -by Auto_tac;
   4.186 -qed_spec_mp "Var_intro";
   4.187 -
   4.188 -Goal "v : srange(s) --> (? w. w : sdom(s) & v : vars_of(Var(w) <| s))";
   4.189 -by (simp_tac (simpset() addsimps [srange_iff]) 1);
   4.190 -qed_spec_mp "srangeD";
   4.191 -
   4.192 -Goal "sdom(s) Int srange(s) = {} = (! t. sdom(s) Int vars_of(t <| s) = {})";
   4.193 -by (simp_tac (simpset() addsimps [empty_iff_all_not]) 1);
   4.194 -by (fast_tac (claset() addIs [Var_in_srange] addDs [srangeD]) 1);
   4.195 -qed "dom_range_disjoint";
   4.196 -
   4.197 -Goal "~ u <| s = u ==> (? x. x : sdom(s))";
   4.198 -by (full_simp_tac (simpset() addsimps [empty_iff_all_not, invariance]) 1);
   4.199 -by (Blast_tac 1);
   4.200 -qed "subst_not_empty";
   4.201 -
   4.202 -
   4.203 -Goal "(M <| [(x, Var x)]) = M";
   4.204 -by (induct_tac "M" 1);
   4.205 -by (ALLGOALS Asm_simp_tac);
   4.206 -qed "id_subst_lemma";
   4.207 -
   4.208 -Addsimps [id_subst_lemma];
     5.1 --- a/src/HOL/Subst/Subst.thy	Mon Mar 28 16:19:56 2005 +0200
     5.2 +++ b/src/HOL/Subst/Subst.thy	Tue Mar 29 12:30:48 2005 +0200
     5.3 @@ -2,11 +2,13 @@
     5.4      ID:         $Id$
     5.5      Author:     Martin Coen, Cambridge University Computer Laboratory
     5.6      Copyright   1993  University of Cambridge
     5.7 -
     5.8 -Substitutions on uterms
     5.9  *)
    5.10  
    5.11 -Subst = AList + UTerm +
    5.12 +header{*Substitutions on uterms*}
    5.13 +
    5.14 +theory Subst
    5.15 +imports AList UTerm
    5.16 +begin
    5.17  
    5.18  consts
    5.19  
    5.20 @@ -19,22 +21,170 @@
    5.21  
    5.22  
    5.23  primrec
    5.24 -  subst_Var      "(Var v <| s) = assoc v (Var v) s"
    5.25 -  subst_Const  "(Const c <| s) = Const c"
    5.26 -  subst_Comb  "(Comb M N <| s) = Comb (M <| s) (N <| s)"
    5.27 +  subst_Var:      "(Var v <| s) = assoc v (Var v) s"
    5.28 +  subst_Const:  "(Const c <| s) = Const c"
    5.29 +  subst_Comb:  "(Comb M N <| s) = Comb (M <| s) (N <| s)"
    5.30  
    5.31  
    5.32  defs 
    5.33  
    5.34 -  subst_eq_def  "r =$= s == ALL t. t <| r = t <| s"
    5.35 +  subst_eq_def:  "r =$= s == ALL t. t <| r = t <| s"
    5.36  
    5.37 -  comp_def    "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)"
    5.38 +  comp_def:    "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)"
    5.39  
    5.40 -  sdom_def
    5.41 +  sdom_def:
    5.42    "sdom(al) == alist_rec al {}  
    5.43                  (%x y xs g. if Var(x)=y then g - {x} else g Un {x})"
    5.44  
    5.45 -  srange_def   
    5.46 +  srange_def:
    5.47     "srange(al) == Union({y. EX x:sdom(al). y=vars_of(Var(x) <| al)})"
    5.48  
    5.49 +
    5.50 +
    5.51 +subsection{*Basic Laws*}
    5.52 +
    5.53 +lemma subst_Nil [simp]: "t <| [] = t"
    5.54 +by (induct_tac "t", auto)
    5.55 +
    5.56 +lemma subst_mono [rule_format]: "t <: u --> t <| s <: u <| s"
    5.57 +by (induct_tac "u", auto)
    5.58 +
    5.59 +lemma Var_not_occs [rule_format]:
    5.60 +     "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s"
    5.61 +apply (case_tac "t = Var v")
    5.62 +apply (erule_tac [2] rev_mp)
    5.63 +apply (rule_tac [2] P = "%x.~x=Var (v) --> ~ (Var (v) <: x) --> x <| (v,t<|s) #s=x<|s" in uterm.induct)
    5.64 +apply auto 
    5.65 +done
    5.66 +
    5.67 +lemma agreement: "(t <|r = t <|s) = (\<forall>v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)"
    5.68 +by (induct_tac "t", auto)
    5.69 +
    5.70 +lemma repl_invariance: "~ v: vars_of(t) ==> t <| (v,u)#s = t <| s"
    5.71 +by (simp add: agreement)
    5.72 +
    5.73 +lemma Var_in_subst [rule_format]:
    5.74 +     "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)"
    5.75 +by (induct_tac "t", auto)
    5.76 +
    5.77 +
    5.78 +subsection{*Equality between Substitutions*}
    5.79 +
    5.80 +lemma subst_eq_iff: "r =$= s = (\<forall>t. t <| r = t <| s)"
    5.81 +by (simp add: subst_eq_def)
    5.82 +
    5.83 +lemma subst_refl [iff]: "r =$= r"
    5.84 +by (simp add: subst_eq_iff)
    5.85 +
    5.86 +lemma subst_sym: "r =$= s ==> s =$= r"
    5.87 +by (simp add: subst_eq_iff)
    5.88 +
    5.89 +lemma subst_trans: "[| q =$= r; r =$= s |] ==> q =$= s"
    5.90 +by (simp add: subst_eq_iff)
    5.91 +
    5.92 +lemma subst_subst2:
    5.93 +    "[| r =$= s; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)"
    5.94 +by (simp add: subst_eq_def)
    5.95 +
    5.96 +lemmas ssubst_subst2 = subst_sym [THEN subst_subst2]
    5.97 +
    5.98 +
    5.99 +subsection{*Composition of Substitutions*}
   5.100 +
   5.101 +lemma [simp]: 
   5.102 +     "[] <> bl = bl"
   5.103 +     "((a,b)#al) <> bl = (a,b <| bl) # (al <> bl)"
   5.104 +     "sdom([]) = {}"
   5.105 +     "sdom((a,b)#al) = (if Var(a)=b then (sdom al) - {a} else sdom al Un {a})"
   5.106 +by (simp_all add: comp_def sdom_def) 
   5.107 +
   5.108 +lemma comp_Nil [simp]: "s <> [] = s"
   5.109 +by (induct "s", auto)
   5.110 +
   5.111 +lemma subst_comp_Nil: "s =$= s <> []"
   5.112 +by simp
   5.113 +
   5.114 +lemma subst_comp [simp]: "(t <| r <> s) = (t <| r <| s)"
   5.115 +apply (induct_tac "t")
   5.116 +apply (simp_all (no_asm_simp))
   5.117 +apply (induct "r", auto)
   5.118 +done
   5.119 +
   5.120 +lemma comp_assoc: "(q <> r) <> s =$= q <> (r <> s)"
   5.121 +apply (simp (no_asm) add: subst_eq_iff)
   5.122 +done
   5.123 +
   5.124 +lemma subst_cong:
   5.125 +     "[| theta =$= theta1; sigma =$= sigma1|] 
   5.126 +      ==> (theta <> sigma) =$= (theta1 <> sigma1)"
   5.127 +by (simp add: subst_eq_def)
   5.128 +
   5.129 +
   5.130 +lemma Cons_trivial: "(w, Var(w) <| s) # s =$= s"
   5.131 +apply (simp add: subst_eq_iff)
   5.132 +apply (rule allI)
   5.133 +apply (induct_tac "t", simp_all)
   5.134 +done
   5.135 +
   5.136 +
   5.137 +lemma comp_subst_subst: "q <> r =$= s ==>  t <| q <| r = t <| s"
   5.138 +by (simp add: subst_eq_iff)
   5.139 +
   5.140 +
   5.141 +subsection{*Domain and range of Substitutions*}
   5.142 +
   5.143 +lemma sdom_iff: "(v : sdom(s)) = (Var(v) <| s ~= Var(v))"
   5.144 +apply (induct "s")
   5.145 +apply (case_tac [2] a, auto)  
   5.146 +done
   5.147 +
   5.148 +
   5.149 +lemma srange_iff: 
   5.150 +   "v : srange(s) = (\<exists>w. w : sdom(s) & v : vars_of(Var(w) <| s))"
   5.151 +by (auto simp add: srange_def)
   5.152 +
   5.153 +lemma empty_iff_all_not: "(A = {}) = (ALL a.~ a:A)"
   5.154 +by (unfold empty_def, blast)
   5.155 +
   5.156 +lemma invariance: "(t <| s = t) = (sdom(s) Int vars_of(t) = {})"
   5.157 +apply (induct_tac "t")
   5.158 +apply (auto simp add: empty_iff_all_not sdom_iff)
   5.159 +done
   5.160 +
   5.161 +lemma Var_in_srange [rule_format]:
   5.162 +     "v : sdom(s) -->  v : vars_of(t <| s) --> v : srange(s)"
   5.163 +apply (induct_tac "t")
   5.164 +apply (case_tac "a : sdom (s) ")
   5.165 +apply (auto simp add: sdom_iff srange_iff)
   5.166 +done
   5.167 +
   5.168 +lemma Var_elim: "[| v : sdom(s); v ~: srange(s) |] ==>  v ~: vars_of(t <| s)"
   5.169 +by (blast intro: Var_in_srange)
   5.170 +
   5.171 +lemma Var_intro [rule_format]:
   5.172 +     "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)"
   5.173 +apply (induct_tac "t")
   5.174 +apply (auto simp add: sdom_iff srange_iff)
   5.175 +apply (rule_tac x=a in exI, auto) 
   5.176 +done
   5.177 +
   5.178 +lemma srangeD [rule_format]:
   5.179 +     "v : srange(s) --> (\<exists>w. w : sdom(s) & v : vars_of(Var(w) <| s))"
   5.180 +apply (simp (no_asm) add: srange_iff)
   5.181 +done
   5.182 +
   5.183 +lemma dom_range_disjoint:
   5.184 +     "sdom(s) Int srange(s) = {} = (\<forall>t. sdom(s) Int vars_of(t <| s) = {})"
   5.185 +apply (simp (no_asm) add: empty_iff_all_not)
   5.186 +apply (force intro: Var_in_srange dest: srangeD)
   5.187 +done
   5.188 +
   5.189 +lemma subst_not_empty: "~ u <| s = u ==> (\<exists>x. x : sdom(s))"
   5.190 +by (auto simp add: empty_iff_all_not invariance)
   5.191 +
   5.192 +
   5.193 +lemma id_subst_lemma [simp]: "(M <| [(x, Var x)]) = M"
   5.194 +by (induct_tac "M", auto)
   5.195 +
   5.196 +
   5.197  end
     6.1 --- a/src/HOL/Subst/UTerm.ML	Mon Mar 28 16:19:56 2005 +0200
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,45 +0,0 @@
     6.4 -(*  Title:      HOL/Subst/UTerm.ML
     6.5 -    ID:         $Id$
     6.6 -    Author:     Martin Coen, Cambridge University Computer Laboratory
     6.7 -    Copyright   1993  University of Cambridge
     6.8 -
     6.9 -Simple term structure for unifiation.
    6.10 -Binary trees with leaves that are constants or variables.
    6.11 -*)
    6.12 -
    6.13 -open UTerm;
    6.14 -
    6.15 -
    6.16 -(**** vars_of lemmas  ****)
    6.17 -
    6.18 -Goal "(v : vars_of(Var(w))) = (w=v)";
    6.19 -by (Simp_tac 1);
    6.20 -by (fast_tac HOL_cs 1);
    6.21 -qed "vars_var_iff";
    6.22 -
    6.23 -Goal  "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)";
    6.24 -by (induct_tac "t" 1);
    6.25 -by (ALLGOALS Simp_tac);
    6.26 -by (fast_tac HOL_cs 1);
    6.27 -qed "vars_iff_occseq";
    6.28 -
    6.29 -
    6.30 -(* Not used, but perhaps useful in other proofs *)
    6.31 -Goal "M<:N --> vars_of(M) <= vars_of(N)";
    6.32 -by (induct_tac "N" 1);
    6.33 -by (ALLGOALS Asm_simp_tac);
    6.34 -by (fast_tac set_cs 1);
    6.35 -val occs_vars_subset = result();
    6.36 -
    6.37 -
    6.38 -Goal "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)";
    6.39 -by (Blast_tac 1);
    6.40 -val monotone_vars_of = result();
    6.41 -
    6.42 -Goal "finite(vars_of M)";
    6.43 -by (induct_tac"M" 1);
    6.44 -by (ALLGOALS Simp_tac);
    6.45 -by (ftac finite_UnI 1);
    6.46 -by (assume_tac 1);
    6.47 -by (Asm_simp_tac 1);
    6.48 -val finite_vars_of = result();
     7.1 --- a/src/HOL/Subst/UTerm.thy	Mon Mar 28 16:19:56 2005 +0200
     7.2 +++ b/src/HOL/Subst/UTerm.thy	Tue Mar 29 12:30:48 2005 +0200
     7.3 @@ -1,38 +1,61 @@
     7.4 -(*  Title:      Subst/UTerm.thy
     7.5 -    ID:         $Id$
     7.6 +(*  ID:         $Id$
     7.7      Author:     Martin Coen, Cambridge University Computer Laboratory
     7.8      Copyright   1993  University of Cambridge
     7.9 -
    7.10 -Simple term structure for unification.
    7.11 -Binary trees with leaves that are constants or variables.
    7.12  *)
    7.13  
    7.14 -UTerm = Main +
    7.15 +header{*Simple Term Structure for Unification*}
    7.16 +
    7.17 +theory UTerm
    7.18 +imports Main
    7.19  
    7.20 -datatype 'a uterm = Var ('a) 
    7.21 -                  | Const ('a)
    7.22 -                  | Comb ('a uterm) ('a uterm)
    7.23 +begin
    7.24 +
    7.25 +text{*Binary trees with leaves that are constants or variables.*}
    7.26 +
    7.27 +datatype 'a uterm = Var 'a
    7.28 +                  | Const 'a
    7.29 +                  | Comb "'a uterm" "'a uterm"
    7.30  
    7.31  consts
    7.32 -  vars_of  ::  'a uterm => 'a set
    7.33 -  "<:"     ::  'a uterm => 'a uterm => bool   (infixl 54) 
    7.34 -uterm_size ::  'a uterm => nat
    7.35 +  vars_of  ::  "'a uterm => 'a set"
    7.36 +  "<:"     ::  "'a uterm => 'a uterm => bool"   (infixl 54) 
    7.37 +uterm_size ::  "'a uterm => nat"
    7.38 +
    7.39 +
    7.40 +primrec
    7.41 +  vars_of_Var:   "vars_of (Var v) = {v}"
    7.42 +  vars_of_Const: "vars_of (Const c) = {}"
    7.43 +  vars_of_Comb:  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
    7.44  
    7.45  
    7.46  primrec
    7.47 -  vars_of_Var   "vars_of (Var v) = {v}"
    7.48 -  vars_of_Const "vars_of (Const c) = {}"
    7.49 -  vars_of_Comb  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
    7.50 -
    7.51 +  occs_Var:   "u <: (Var v) = False"
    7.52 +  occs_Const: "u <: (Const c) = False"
    7.53 +  occs_Comb:  "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)"
    7.54  
    7.55  primrec
    7.56 -  occs_Var   "u <: (Var v) = False"
    7.57 -  occs_Const "u <: (Const c) = False"
    7.58 -  occs_Comb  "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)"
    7.59 +  uterm_size_Var:   "uterm_size (Var v) = 0"
    7.60 +  uterm_size_Const: "uterm_size (Const c) = 0"
    7.61 +  uterm_size_Comb:  "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
    7.62 +
    7.63 +
    7.64 +lemma vars_var_iff: "(v : vars_of(Var(w))) = (w=v)"
    7.65 +by auto
    7.66 +
    7.67 +lemma vars_iff_occseq: "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)"
    7.68 +by (induct_tac "t", auto)
    7.69 +
    7.70  
    7.71 -primrec
    7.72 -  uterm_size_Var   "uterm_size (Var v) = 0"
    7.73 -  uterm_size_Const "uterm_size (Const c) = 0"
    7.74 -  uterm_size_Comb  "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
    7.75 +(* Not used, but perhaps useful in other proofs *)
    7.76 +lemma occs_vars_subset: "M<:N --> vars_of(M) <= vars_of(N)"
    7.77 +by (induct_tac "N", auto)
    7.78 +
    7.79 +
    7.80 +lemma monotone_vars_of: "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)"
    7.81 +by blast
    7.82 +
    7.83 +lemma finite_vars_of: "finite(vars_of M)"
    7.84 +by (induct_tac "M", auto)
    7.85 +
    7.86  
    7.87  end
     8.1 --- a/src/HOL/Subst/Unifier.ML	Mon Mar 28 16:19:56 2005 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,99 +0,0 @@
     8.4 -(*  Title:      HOL/Subst/Unifier.ML
     8.5 -    ID:         $Id$
     8.6 -    Author:     Martin Coen, Cambridge University Computer Laboratory
     8.7 -    Copyright   1993  University of Cambridge
     8.8 -
     8.9 -Properties of unifiers.
    8.10 -*)
    8.11 -
    8.12 -open Unifier;
    8.13 -
    8.14 -val unify_defs = [Unifier_def, MoreGeneral_def, MGUnifier_def];
    8.15 -
    8.16 -(*---------------------------------------------------------------------------
    8.17 - * Unifiers 
    8.18 - *---------------------------------------------------------------------------*)
    8.19 -
    8.20 -Goal "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)";
    8.21 -by (simp_tac (simpset() addsimps [Unifier_def]) 1);
    8.22 -qed "Unifier_Comb";
    8.23 -
    8.24 -AddIffs [Unifier_Comb];
    8.25 -
    8.26 -Goal "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> \
    8.27 -\  Unifier ((v,r)#s) t u";
    8.28 -by (asm_full_simp_tac (simpset() addsimps [Unifier_def, repl_invariance]) 1);
    8.29 -qed "Cons_Unifier";
    8.30 -
    8.31 -
    8.32 -(*---------------------------------------------------------------------------
    8.33 - * Most General Unifiers 
    8.34 - *---------------------------------------------------------------------------*)
    8.35 -
    8.36 -Goalw unify_defs "MGUnifier s t u = MGUnifier s u t";
    8.37 -by (blast_tac (claset() addIs [sym]) 1);
    8.38 -qed "mgu_sym";
    8.39 -
    8.40 -
    8.41 -Goal  "[] >> s";
    8.42 -by (simp_tac (simpset() addsimps [MoreGeneral_def]) 1);
    8.43 -by (Blast_tac 1);
    8.44 -qed "MoreGen_Nil";
    8.45 -
    8.46 -AddIffs [MoreGen_Nil];
    8.47 -
    8.48 -Goalw unify_defs
    8.49 -    "MGUnifier s t u = (ALL r. Unifier r t u = s >> r)";
    8.50 -by (auto_tac (claset() addIs [ssubst_subst2, subst_comp_Nil], simpset()));
    8.51 -qed "MGU_iff";
    8.52 -
    8.53 -
    8.54 -Goal "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t";
    8.55 -by (simp_tac(simpset() addsimps [MGU_iff, Unifier_def, MoreGeneral_def]
    8.56 -	              delsimps [subst_Var]) 1);
    8.57 -by Safe_tac;
    8.58 -by (rtac exI 1);
    8.59 -by (etac subst 1 THEN rtac (Cons_trivial RS subst_sym) 1);
    8.60 -by (etac ssubst_subst2 1);
    8.61 -by (asm_simp_tac (simpset() addsimps [Var_not_occs]) 1);
    8.62 -qed "MGUnifier_Var";
    8.63 -
    8.64 -AddSIs [MGUnifier_Var];
    8.65 -
    8.66 -
    8.67 -(*---------------------------------------------------------------------------
    8.68 - * Idempotence.
    8.69 - *---------------------------------------------------------------------------*)
    8.70 -
    8.71 -Goalw [Idem_def] "Idem([])";
    8.72 -by (Simp_tac 1);
    8.73 -qed "Idem_Nil";
    8.74 -
    8.75 -AddIffs [Idem_Nil];
    8.76 -
    8.77 -Goalw [Idem_def] "Idem(s) = (sdom(s) Int srange(s) = {})";
    8.78 -by (simp_tac (simpset() addsimps [subst_eq_iff, invariance, 
    8.79 -				 dom_range_disjoint]) 1);
    8.80 -qed "Idem_iff";
    8.81 -
    8.82 -Goal "~ (Var(v) <: t) --> Idem([(v,t)])";
    8.83 -by (simp_tac (simpset() addsimps [vars_iff_occseq, Idem_iff, srange_iff, 
    8.84 -				  empty_iff_all_not]) 1);
    8.85 -qed_spec_mp "Var_Idem";
    8.86 -
    8.87 -AddSIs [Var_Idem];
    8.88 -
    8.89 -Goalw [Idem_def]
    8.90 -  "[| Idem(r); Unifier s (t<|r) (u<|r) |] \
    8.91 -\  ==> Unifier (r <> s) (t <| r) (u <| r)";
    8.92 -by (asm_full_simp_tac (simpset() addsimps [Unifier_def, comp_subst_subst]) 1);
    8.93 -qed "Unifier_Idem_subst";
    8.94 -
    8.95 -val [idemr,unifier,minor] = goal Unifier.thy
    8.96 -     "[| Idem(r);  Unifier s (t <| r) (u <| r); \
    8.97 -\        !!q. Unifier q (t <| r) (u <| r) ==> s <> q =$= q \
    8.98 -\     |] ==> Idem(r <> s)";
    8.99 -by (cut_facts_tac [idemr,
   8.100 -                   unifier RS (idemr RS Unifier_Idem_subst RS minor)] 1);
   8.101 -by (asm_full_simp_tac (simpset() addsimps [Idem_def, subst_eq_iff]) 1);
   8.102 -qed "Idem_comp";
     9.1 --- a/src/HOL/Subst/Unifier.thy	Mon Mar 28 16:19:56 2005 +0200
     9.2 +++ b/src/HOL/Subst/Unifier.thy	Tue Mar 29 12:30:48 2005 +0200
     9.3 @@ -1,12 +1,15 @@
     9.4 -(*  Title:      Subst/Unifier.thy
     9.5 -    ID:         $Id$
     9.6 +(*  ID:         $Id$
     9.7      Author:     Martin Coen, Cambridge University Computer Laboratory
     9.8      Copyright   1993  University of Cambridge
     9.9  
    9.10 -Definition of most general unifier
    9.11  *)
    9.12  
    9.13 -Unifier = Subst + 
    9.14 +header{*Definition of Most General Unifier*}
    9.15 +
    9.16 +theory Unifier
    9.17 +imports Subst
    9.18 +
    9.19 +begin
    9.20  
    9.21  consts
    9.22  
    9.23 @@ -17,9 +20,76 @@
    9.24  
    9.25  defs
    9.26  
    9.27 -  Unifier_def      "Unifier s t u == t <| s = u <| s"
    9.28 -  MoreGeneral_def  "r >> s == ? q. s =$= r <> q"
    9.29 -  MGUnifier_def    "MGUnifier s t u == Unifier s t u & 
    9.30 -                                       (!r. Unifier r t u --> s >> r)"
    9.31 -  Idem_def         "Idem(s) == (s <> s) =$= s"
    9.32 +  Unifier_def:      "Unifier s t u == t <| s = u <| s"
    9.33 +  MoreGeneral_def:  "r >> s == ? q. s =$= r <> q"
    9.34 +  MGUnifier_def:    "MGUnifier s t u == Unifier s t u & 
    9.35 +                                        (!r. Unifier r t u --> s >> r)"
    9.36 +  Idem_def:         "Idem(s) == (s <> s) =$= s"
    9.37 +
    9.38 +
    9.39 +
    9.40 +lemmas unify_defs = Unifier_def MoreGeneral_def MGUnifier_def
    9.41 +
    9.42 +
    9.43 +subsection{*Unifiers*}
    9.44 +
    9.45 +lemma Unifier_Comb [iff]: "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)"
    9.46 +by (simp add: Unifier_def)
    9.47 +
    9.48 +
    9.49 +lemma Cons_Unifier: "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> Unifier ((v,r)#s) t u"
    9.50 +by (simp add: Unifier_def repl_invariance)
    9.51 +
    9.52 +
    9.53 +subsection{* Most General Unifiers*}
    9.54 +
    9.55 +lemma mgu_sym: "MGUnifier s t u = MGUnifier s u t"
    9.56 +by (simp add: unify_defs eq_commute)
    9.57 +
    9.58 +
    9.59 +lemma MoreGen_Nil [iff]: "[] >> s"
    9.60 +by (auto simp add: MoreGeneral_def)
    9.61 +
    9.62 +lemma MGU_iff: "MGUnifier s t u = (ALL r. Unifier r t u = s >> r)"
    9.63 +apply (unfold unify_defs)
    9.64 +apply (auto intro: ssubst_subst2 subst_comp_Nil)
    9.65 +done
    9.66 +
    9.67 +lemma MGUnifier_Var: "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t"
    9.68 +apply (simp (no_asm) add: MGU_iff Unifier_def MoreGeneral_def del: subst_Var)
    9.69 +apply safe
    9.70 +apply (rule exI)
    9.71 +apply (erule subst, rule Cons_trivial [THEN subst_sym])
    9.72 +apply (erule ssubst_subst2)
    9.73 +apply (simp (no_asm_simp) add: Var_not_occs)
    9.74 +done
    9.75 +
    9.76 +declare MGUnifier_Var [intro!]
    9.77 +
    9.78 +
    9.79 +subsection{*Idempotence*}
    9.80 +
    9.81 +lemma Idem_Nil [iff]: "Idem([])"
    9.82 +by (simp add: Idem_def)
    9.83 +
    9.84 +lemma Idem_iff: "Idem(s) = (sdom(s) Int srange(s) = {})"
    9.85 +by (simp add: Idem_def subst_eq_iff invariance dom_range_disjoint)
    9.86 +
    9.87 +lemma Var_Idem [intro!]: "~ (Var(v) <: t) ==> Idem([(v,t)])"
    9.88 +by (simp add: vars_iff_occseq Idem_iff srange_iff empty_iff_all_not)
    9.89 +
    9.90 +lemma Unifier_Idem_subst: 
    9.91 +  "[| Idem(r); Unifier s (t<|r) (u<|r) |]  
    9.92 +   ==> Unifier (r <> s) (t <| r) (u <| r)"
    9.93 +by (simp add: Idem_def Unifier_def comp_subst_subst)
    9.94 +
    9.95 +lemma Idem_comp:
    9.96 +     "[| Idem(r);  Unifier s (t <| r) (u <| r);  
    9.97 +         !!q. Unifier q (t <| r) (u <| r) ==> s <> q =$= q  
    9.98 +      |] ==> Idem(r <> s)"
    9.99 +apply (frule Unifier_Idem_subst, blast) 
   9.100 +apply (force simp add: Idem_def subst_eq_iff)
   9.101 +done
   9.102 +
   9.103 +
   9.104  end
    10.1 --- a/src/HOL/Subst/Unify.ML	Mon Mar 28 16:19:56 2005 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,251 +0,0 @@
    10.4 -(*  Title:      Subst/Unify
    10.5 -    ID:         $Id$
    10.6 -    Author:     Konrad Slind, Cambridge University Computer Laboratory
    10.7 -    Copyright   1997  University of Cambridge
    10.8 -
    10.9 -Unification algorithm
   10.10 -*)
   10.11 -
   10.12 -(*---------------------------------------------------------------------------
   10.13 - * This file defines a nested unification algorithm, then proves that it 
   10.14 - * terminates, then proves 2 correctness theorems: that when the algorithm
   10.15 - * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution.
   10.16 - * Although the proofs may seem long, they are actually quite direct, in that
   10.17 - * the correctness and termination properties are not mingled as much as in 
   10.18 - * previous proofs of this algorithm. 
   10.19 - *
   10.20 - * Our approach for nested recursive functions is as follows: 
   10.21 - *
   10.22 - *    0. Prove the wellfoundedness of the termination relation.
   10.23 - *    1. Prove the non-nested termination conditions.
   10.24 - *    2. Eliminate (0) and (1) from the recursion equations and the 
   10.25 - *       induction theorem.
   10.26 - *    3. Prove the nested termination conditions by using the induction 
   10.27 - *       theorem from (2) and by using the recursion equations from (2). 
   10.28 - *       These are constrained by the nested termination conditions, but 
   10.29 - *       things work out magically (by wellfoundedness of the termination 
   10.30 - *       relation).
   10.31 - *    4. Eliminate the nested TCs from the results of (2).
   10.32 - *    5. Prove further correctness properties using the results of (4).
   10.33 - *
   10.34 - * Deeper nestings require iteration of steps (3) and (4).
   10.35 - *---------------------------------------------------------------------------*)
   10.36 -
   10.37 -(*---------------------------------------------------------------------------
   10.38 - * The non-nested TC plus the wellfoundedness of unifyRel.
   10.39 - *---------------------------------------------------------------------------*)
   10.40 -Tfl.tgoalw Unify.thy [] unify.simps;
   10.41 -(* Wellfoundedness of unifyRel *)
   10.42 -by (simp_tac (simpset() addsimps [unifyRel_def,
   10.43 -				 wf_inv_image, wf_lex_prod, wf_finite_psubset,
   10.44 -				 wf_measure]) 1);
   10.45 -(* TC *)
   10.46 -by Safe_tac;
   10.47 -by (simp_tac (simpset() addsimps [finite_psubset_def, finite_vars_of,
   10.48 -				 lex_prod_def, measure_def, inv_image_def]) 1);
   10.49 -by (rtac (monotone_vars_of RS (subset_iff_psubset_eq RS iffD1) RS disjE) 1);
   10.50 -by (Blast_tac 1);
   10.51 -by (asm_simp_tac (simpset() addsimps [less_eq, less_add_Suc1]) 1);
   10.52 -qed "tc0";
   10.53 -
   10.54 -
   10.55 -(*---------------------------------------------------------------------------
   10.56 - * Termination proof.
   10.57 - *---------------------------------------------------------------------------*)
   10.58 -
   10.59 -Goalw [unifyRel_def, measure_def] "trans unifyRel";
   10.60 -by (REPEAT (resolve_tac [trans_inv_image, trans_lex_prod, 
   10.61 -			 trans_finite_psubset, trans_less_than,
   10.62 -			 trans_inv_image] 1));
   10.63 -qed "trans_unifyRel";
   10.64 -
   10.65 -
   10.66 -(*---------------------------------------------------------------------------
   10.67 - * The following lemma is used in the last step of the termination proof for 
   10.68 - * the nested call in Unify.  Loosely, it says that unifyRel doesn't care
   10.69 - * about term structure.
   10.70 - *---------------------------------------------------------------------------*)
   10.71 -Goalw [unifyRel_def,lex_prod_def, inv_image_def]
   10.72 -  "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel  ==> \
   10.73 -\  ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel";
   10.74 -by (asm_full_simp_tac (simpset() addsimps [measure_def, 
   10.75 -                          less_eq, inv_image_def,add_assoc]) 1);
   10.76 -by (subgoal_tac "(vars_of A Un vars_of B Un vars_of C Un \
   10.77 -                \  (vars_of D Un vars_of E Un vars_of F)) = \
   10.78 -                \ (vars_of A Un (vars_of B Un vars_of C) Un \
   10.79 -                \  (vars_of D Un (vars_of E Un vars_of F)))" 1);
   10.80 -by (Blast_tac 2);
   10.81 -by (Asm_simp_tac 1);
   10.82 -qed "Rassoc";
   10.83 -
   10.84 -
   10.85 -(*---------------------------------------------------------------------------
   10.86 - * This lemma proves the nested termination condition for the base cases 
   10.87 - * 3, 4, and 6. 
   10.88 - *---------------------------------------------------------------------------*)
   10.89 -Goal "~(Var x <: M) ==> \
   10.90 -\   ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel \
   10.91 -\ & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel";
   10.92 -by (case_tac "Var x = M" 1);
   10.93 -by (hyp_subst_tac 1);
   10.94 -by (Simp_tac 1);
   10.95 -by (case_tac "x: (vars_of N1 Un vars_of N2)" 1);
   10.96 -(*uterm_less case*)
   10.97 -by (asm_simp_tac
   10.98 -    (simpset() addsimps [less_eq, unifyRel_def, lex_prod_def,
   10.99 -			measure_def, inv_image_def]) 1);
  10.100 -by (Blast_tac 1);
  10.101 -(*finite_psubset case*)
  10.102 -by (simp_tac
  10.103 -    (simpset() addsimps [unifyRel_def, lex_prod_def,
  10.104 -			measure_def, inv_image_def]) 1);
  10.105 -by (simp_tac (simpset() addsimps [finite_psubset_def, finite_vars_of,
  10.106 -				 psubset_def]) 1);
  10.107 -by (Blast_tac 1);
  10.108 -(** LEVEL 9 **)
  10.109 -(*Final case, also finite_psubset*)
  10.110 -by (simp_tac
  10.111 -    (simpset() addsimps [finite_vars_of, unifyRel_def, finite_psubset_def,
  10.112 -			lex_prod_def, measure_def, inv_image_def]) 1);
  10.113 -by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N2")] Var_elim 1);
  10.114 -by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N1")] Var_elim 3);
  10.115 -by (ALLGOALS (asm_simp_tac(simpset() addsimps [srange_iff, vars_iff_occseq])));
  10.116 -by (REPEAT_FIRST (resolve_tac [conjI, disjI1, psubsetI]));
  10.117 -by (ALLGOALS (asm_full_simp_tac 
  10.118 -	      (simpset() addsimps [srange_iff]))); 
  10.119 -by (ALLGOALS
  10.120 -    (fast_tac (claset() addEs [Var_intro RS disjE]
  10.121 -	               addss (simpset() addsimps [srange_iff]))));
  10.122 -qed "var_elimR";
  10.123 -
  10.124 -
  10.125 -(*---------------------------------------------------------------------------
  10.126 - * Eliminate tc0 from the recursion equations and the induction theorem.
  10.127 - *---------------------------------------------------------------------------*)
  10.128 -val wfr = tc0 RS conjunct1
  10.129 -and tc  = tc0 RS conjunct2;
  10.130 -val unifyRules0 = map (rule_by_tactic (rtac wfr 1 THEN TRY(rtac tc 1)))
  10.131 -                     unify.simps;
  10.132 -
  10.133 -val unifyInduct0 = [wfr,tc] MRS unify.induct;
  10.134 -
  10.135 -
  10.136 -(*---------------------------------------------------------------------------
  10.137 - * The nested TC. Proved by recursion induction.
  10.138 - *---------------------------------------------------------------------------*)
  10.139 -val [_,_,tc3] = unify.tcs;
  10.140 -goalw_cterm [] (cterm_of (sign_of Unify.thy) (HOLogic.mk_Trueprop tc3));
  10.141 -(*---------------------------------------------------------------------------
  10.142 - * The extracted TC needs the scope of its quantifiers adjusted, so our 
  10.143 - * first step is to restrict the scopes of N1 and N2.
  10.144 - *---------------------------------------------------------------------------*)
  10.145 -by (subgoal_tac "!M1 M2 theta.  \
  10.146 - \   unify(M1, M2) = Some theta --> \
  10.147 - \   (!N1 N2. ((N1<|theta, N2<|theta), (Comb M1 N1, Comb M2 N2)) : unifyRel)" 1);
  10.148 -by (Blast_tac 1);
  10.149 -by (rtac allI 1); 
  10.150 -by (rtac allI 1);
  10.151 -(* Apply induction *)
  10.152 -by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1);
  10.153 -by (ALLGOALS 
  10.154 -    (asm_simp_tac (simpset() addsimps (var_elimR::unifyRules0))));
  10.155 -(*Const-Const case*)
  10.156 -by (simp_tac
  10.157 -    (simpset() addsimps [unifyRel_def, lex_prod_def, measure_def,
  10.158 -			inv_image_def, less_eq]) 1);
  10.159 -(** LEVEL 7 **)
  10.160 -(*Comb-Comb case*)
  10.161 -by (asm_simp_tac (simpset() addsplits [option.split]) 1);
  10.162 -by (strip_tac 1);
  10.163 -by (rtac (trans_unifyRel RS transD) 1);
  10.164 -by (Blast_tac 1);
  10.165 -by (simp_tac (HOL_ss addsimps [subst_Comb RS sym]) 1);
  10.166 -by (rtac Rassoc 1);
  10.167 -by (Blast_tac 1);
  10.168 -qed_spec_mp "unify_TC";
  10.169 -
  10.170 -
  10.171 -(*---------------------------------------------------------------------------
  10.172 - * Now for elimination of nested TC from unify.simps and induction. 
  10.173 - *---------------------------------------------------------------------------*)
  10.174 -
  10.175 -(*Desired rule, copied from the theory file.  Could it be made available?*)
  10.176 -Goal "unify(Comb M1 N1, Comb M2 N2) =      \
  10.177 -\      (case unify(M1,M2)               \
  10.178 -\        of None => None                \
  10.179 -\         | Some theta => (case unify(N1 <| theta, N2 <| theta)        \
  10.180 -\                            of None => None    \
  10.181 -\                             | Some sigma => Some (theta <> sigma)))";
  10.182 -by (asm_simp_tac (simpset() addsimps (unify_TC::unifyRules0)
  10.183 -			   addsplits [option.split]) 1);
  10.184 -qed "unifyCombComb";
  10.185 -
  10.186 -
  10.187 -val unifyRules = rev (unifyCombComb :: tl (rev unifyRules0));
  10.188 -
  10.189 -Addsimps unifyRules;
  10.190 -
  10.191 -bind_thm ("unifyInduct",
  10.192 -	  rule_by_tactic
  10.193 -	     (ALLGOALS (full_simp_tac (simpset() addsimps [unify_TC])))
  10.194 -	     unifyInduct0);
  10.195 -
  10.196 -
  10.197 -(*---------------------------------------------------------------------------
  10.198 - * Correctness. Notice that idempotence is not needed to prove that the 
  10.199 - * algorithm terminates and is not needed to prove the algorithm correct, 
  10.200 - * if you are only interested in an MGU.  This is in contrast to the
  10.201 - * approach of M&W, who used idempotence and MGU-ness in the termination proof.
  10.202 - *---------------------------------------------------------------------------*)
  10.203 -
  10.204 -Goal "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
  10.205 -by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
  10.206 -by (ALLGOALS Asm_simp_tac);
  10.207 -(*Const-Const case*)
  10.208 -by (simp_tac (simpset() addsimps [MGUnifier_def,Unifier_def]) 1);
  10.209 -(*Const-Var case*)
  10.210 -by (stac mgu_sym 1);
  10.211 -by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
  10.212 -(*Var-M case*)
  10.213 -by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
  10.214 -(*Comb-Var case*)
  10.215 -by (stac mgu_sym 1);
  10.216 -by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
  10.217 -(** LEVEL 8 **)
  10.218 -(*Comb-Comb case*)
  10.219 -by (asm_simp_tac (simpset() addsplits [option.split]) 1);
  10.220 -by (strip_tac 1);
  10.221 -by (asm_full_simp_tac 
  10.222 -    (simpset() addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1);
  10.223 -by (Safe_tac THEN rename_tac "theta sigma gamma" 1);
  10.224 -by (eres_inst_tac [("x","gamma")] allE 1 THEN mp_tac 1);
  10.225 -by (etac exE 1 THEN rename_tac "delta" 1);
  10.226 -by (eres_inst_tac [("x","delta")] allE 1);
  10.227 -by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1);
  10.228 -(*Proving the subgoal*)
  10.229 -by (full_simp_tac (simpset() addsimps [subst_eq_iff]) 2
  10.230 -    THEN blast_tac (claset() addIs [trans,sym] delrules [impCE]) 2);
  10.231 -by (blast_tac (claset() addIs [subst_trans, subst_cong, 
  10.232 -			      comp_assoc RS subst_sym]) 1);
  10.233 -qed_spec_mp "unify_gives_MGU";
  10.234 -
  10.235 -
  10.236 -(*---------------------------------------------------------------------------
  10.237 - * Unify returns idempotent substitutions, when it succeeds.
  10.238 - *---------------------------------------------------------------------------*)
  10.239 -Goal "!theta. unify(M,N) = Some theta --> Idem theta";
  10.240 -by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
  10.241 -by (ALLGOALS 
  10.242 -    (asm_simp_tac 
  10.243 -       (simpset() addsimps [Var_Idem] addsplits [option.split])));
  10.244 -(*Comb-Comb case*)
  10.245 -by Safe_tac;
  10.246 -by (REPEAT (dtac spec 1 THEN mp_tac 1));
  10.247 -by (safe_tac (claset() addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU]));
  10.248 -by (rtac Idem_comp 1);
  10.249 -by (atac 1);
  10.250 -by (atac 1);
  10.251 -by (best_tac (claset() addss (simpset() addsimps 
  10.252 -			     [MoreGeneral_def, subst_eq_iff, Idem_def])) 1);
  10.253 -qed_spec_mp "unify_gives_Idem";
  10.254 -
    11.1 --- a/src/HOL/Subst/Unify.thy	Mon Mar 28 16:19:56 2005 +0200
    11.2 +++ b/src/HOL/Subst/Unify.thy	Tue Mar 29 12:30:48 2005 +0200
    11.3 @@ -1,12 +1,26 @@
    11.4 -(*  Title:      Subst/Unify
    11.5 -    ID:         $Id$
    11.6 +(*  ID:         $Id$
    11.7      Author:     Konrad Slind, Cambridge University Computer Laboratory
    11.8      Copyright   1997  University of Cambridge
    11.9  
   11.10 -Unification algorithm
   11.11  *)
   11.12  
   11.13 -Unify = Unifier +
   11.14 +header{*Unification Algorithm*}
   11.15 +
   11.16 +theory Unify
   11.17 +imports Unifier
   11.18 +begin
   11.19 +
   11.20 +text{*
   11.21 +Substitution and Unification in Higher-Order Logic. 
   11.22 +
   11.23 +Implements Manna and Waldinger's formalization, with Paulson's simplifications,
   11.24 +and some new simplifications by Slind.
   11.25 +
   11.26 +Z Manna and R Waldinger, Deductive Synthesis of the Unification Algorithm. 
   11.27 +SCP 1 (1981), 5-48
   11.28 +
   11.29 +L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170
   11.30 +*}
   11.31  
   11.32  consts
   11.33  
   11.34 @@ -14,26 +28,218 @@
   11.35     unify    :: "'a uterm * 'a uterm => ('a * 'a uterm) list option"
   11.36  
   11.37  defs
   11.38 +  unifyRel_def:
   11.39 +       "unifyRel == inv_image (finite_psubset <*lex*> measure uterm_size)
   11.40 +                               (%(M,N). (vars_of M Un vars_of N, M))"
   11.41 +   --{*Termination relation for the Unify function:
   11.42 +         either the set of variables decreases, 
   11.43 +         or the first argument does (in fact, both do) *}
   11.44  
   11.45 -  (*Termination relation for the Unify function:
   11.46 -    --either the set of variables decreases
   11.47 -    --or the first argument does (in fact, both do)
   11.48 -  *)
   11.49 -  unifyRel_def  "unifyRel == inv_image (finite_psubset <*lex*> measure uterm_size)
   11.50 -                               (%(M,N). (vars_of M Un vars_of N, M))"
   11.51 +text{* Wellfoundedness of unifyRel *}
   11.52 +lemma wf_unifyRel [iff]: "wf unifyRel"
   11.53 +by (simp add: unifyRel_def wf_lex_prod wf_finite_psubset)
   11.54  
   11.55 -recdef unify "unifyRel"
   11.56 -  "unify(Const m, Const n)  = (if (m=n) then Some[] else None)"
   11.57 -  "unify(Const m, Comb M N) = None"
   11.58 -  "unify(Const m, Var v)    = Some[(v,Const m)]"
   11.59 -  "unify(Var v, M)          = (if (Var v <: M) then None else Some[(v,M)])"
   11.60 -  "unify(Comb M N, Const x) = None"
   11.61 -  "unify(Comb M N, Var v)   = (if (Var v <: Comb M N) then None   
   11.62 -                               else Some[(v,Comb M N)])"
   11.63 +
   11.64 +recdef (permissive) unify "unifyRel"
   11.65 + unify_CC: "unify(Const m, Const n)  = (if (m=n) then Some[] else None)"
   11.66 + unify_CB: "unify(Const m, Comb M N) = None"
   11.67 + unify_CV: "unify(Const m, Var v)    = Some[(v,Const m)]"
   11.68 + unify_V:  "unify(Var v, M) = (if (Var v <: M) then None else Some[(v,M)])"
   11.69 + unify_BC: "unify(Comb M N, Const x) = None"
   11.70 + unify_BV: "unify(Comb M N, Var v)   = (if (Var v <: Comb M N) then None   
   11.71 +                                        else Some[(v,Comb M N)])"
   11.72 + unify_BB:
   11.73    "unify(Comb M1 N1, Comb M2 N2) =   
   11.74        (case unify(M1,M2)  
   11.75          of None       => None  
   11.76           | Some theta => (case unify(N1 <| theta, N2 <| theta)  
   11.77                              of None       => None  
   11.78                               | Some sigma => Some (theta <> sigma)))"
   11.79 +  (hints recdef_wf: wf_unifyRel)
   11.80 +
   11.81 +
   11.82 +
   11.83 +(*---------------------------------------------------------------------------
   11.84 + * This file defines a nested unification algorithm, then proves that it 
   11.85 + * terminates, then proves 2 correctness theorems: that when the algorithm
   11.86 + * succeeds, it 1) returns an MGU; and 2) returns an idempotent substitution.
   11.87 + * Although the proofs may seem long, they are actually quite direct, in that
   11.88 + * the correctness and termination properties are not mingled as much as in 
   11.89 + * previous proofs of this algorithm. 
   11.90 + *
   11.91 + * Our approach for nested recursive functions is as follows: 
   11.92 + *
   11.93 + *    0. Prove the wellfoundedness of the termination relation.
   11.94 + *    1. Prove the non-nested termination conditions.
   11.95 + *    2. Eliminate (0) and (1) from the recursion equations and the 
   11.96 + *       induction theorem.
   11.97 + *    3. Prove the nested termination conditions by using the induction 
   11.98 + *       theorem from (2) and by using the recursion equations from (2). 
   11.99 + *       These are constrained by the nested termination conditions, but 
  11.100 + *       things work out magically (by wellfoundedness of the termination 
  11.101 + *       relation).
  11.102 + *    4. Eliminate the nested TCs from the results of (2).
  11.103 + *    5. Prove further correctness properties using the results of (4).
  11.104 + *
  11.105 + * Deeper nestings require iteration of steps (3) and (4).
  11.106 + *---------------------------------------------------------------------------*)
  11.107 +
  11.108 +text{*The non-nested TC (terminiation condition). This declaration form
  11.109 +only seems to return one subgoal outstanding from the recdef.*}
  11.110 +recdef_tc unify_tc1: unify
  11.111 +apply (simp add: unifyRel_def wf_lex_prod wf_finite_psubset, safe)
  11.112 +apply (simp add: finite_psubset_def finite_vars_of lex_prod_def measure_def inv_image_def)
  11.113 +apply (rule monotone_vars_of [THEN subset_iff_psubset_eq [THEN iffD1]])
  11.114 +done
  11.115 +
  11.116 +
  11.117 +
  11.118 +
  11.119 +text{*Termination proof.*}
  11.120 +
  11.121 +lemma trans_unifyRel: "trans unifyRel"
  11.122 +by (simp add: unifyRel_def measure_def trans_inv_image trans_lex_prod
  11.123 +              trans_finite_psubset)
  11.124 +
  11.125 +
  11.126 +text{*The following lemma is used in the last step of the termination proof
  11.127 +for the nested call in Unify.  Loosely, it says that unifyRel doesn't care
  11.128 +about term structure.*}
  11.129 +lemma Rassoc: 
  11.130 +  "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel  ==>  
  11.131 +   ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel"
  11.132 +by (simp add: measure_def less_eq inv_image_def add_assoc Un_assoc 
  11.133 +              unifyRel_def lex_prod_def)
  11.134 +
  11.135 +
  11.136 +text{*This lemma proves the nested termination condition for the base cases 
  11.137 + * 3, 4, and 6.*}
  11.138 +lemma var_elimR:
  11.139 +  "~(Var x <: M) ==>  
  11.140 +    ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel  
  11.141 +  & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel"
  11.142 +apply (case_tac "Var x = M", clarify, simp)
  11.143 +apply (case_tac "x: (vars_of N1 Un vars_of N2) ")
  11.144 +txt{*uterm_less case*}
  11.145 +apply (simp add: less_eq unifyRel_def lex_prod_def measure_def inv_image_def)
  11.146 +apply blast
  11.147 +txt{*@{text finite_psubset} case*}
  11.148 +apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def)
  11.149 +apply (simp add: finite_psubset_def finite_vars_of psubset_def)
  11.150 +apply blast
  11.151 +txt{*Final case, also {text finite_psubset}*}
  11.152 +apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def measure_def inv_image_def)
  11.153 +apply (cut_tac s = "[ (x,M) ]" and v = x and t = N2 in Var_elim)
  11.154 +apply (cut_tac [3] s = "[ (x,M) ]" and v = x and t = N1 in Var_elim)
  11.155 +apply (simp_all (no_asm_simp) add: srange_iff vars_iff_occseq)
  11.156 +apply (auto elim!: Var_intro [THEN disjE] simp add: srange_iff)
  11.157 +done
  11.158 +
  11.159 +
  11.160 +text{*Eliminate tc1 from the recursion equations and the induction theorem.*}
  11.161 +
  11.162 +lemmas unify_nonrec [simp] = 
  11.163 +       unify_CC unify_CB unify_CV unify_V unify_BC unify_BV 
  11.164 +
  11.165 +lemmas unify_simps0 = unify_nonrec unify_BB [OF unify_tc1]
  11.166 +
  11.167 +lemmas unify_induct0 = unify.induct [OF unify_tc1]
  11.168 +
  11.169 +text{*The nested TC. Proved by recursion induction.*}
  11.170 +lemma unify_tc2:
  11.171 +     "\<forall>M1 M2 N1 N2 theta.
  11.172 +       unify (M1, M2) = Some theta \<longrightarrow>
  11.173 +       ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) \<in> unifyRel"
  11.174 +txt{*The extracted TC needs the scope of its quantifiers adjusted, so our
  11.175 + first step is to restrict the scopes of N1 and N2.*}
  11.176 +apply (subgoal_tac "\<forall>M1 M2 theta. unify (M1, M2) = Some theta --> 
  11.177 +      (\<forall>N1 N2.((N1<|theta, N2<|theta), (Comb M1 N1, Comb M2 N2)) : unifyRel)")
  11.178 +apply blast
  11.179 +apply (rule allI)
  11.180 +apply (rule allI)
  11.181 +txt{*Apply induction on this still-quantified formula*}
  11.182 +apply (rule_tac u = M1 and v = M2 in unify_induct0)
  11.183 +apply (simp_all (no_asm_simp) add: var_elimR unify_simps0)
  11.184 +txt{*Const-Const case*}
  11.185 +apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def less_eq)
  11.186 +txt{*Comb-Comb case*}
  11.187 +apply (simp (no_asm_simp) split add: option.split)
  11.188 +apply (intro strip)
  11.189 +apply (rule trans_unifyRel [THEN transD], blast)
  11.190 +apply (simp only: subst_Comb [symmetric])
  11.191 +apply (rule Rassoc, blast)
  11.192 +done
  11.193 +
  11.194 +
  11.195 +text{* Now for elimination of nested TC from unify.simps and induction.*}
  11.196 +
  11.197 +text{*Desired rule, copied from the theory file.*}
  11.198 +lemma unifyCombComb [simp]:
  11.199 +    "unify(Comb M1 N1, Comb M2 N2) =       
  11.200 +       (case unify(M1,M2)                
  11.201 +         of None => None                 
  11.202 +          | Some theta => (case unify(N1 <| theta, N2 <| theta)         
  11.203 +                             of None => None     
  11.204 +                              | Some sigma => Some (theta <> sigma)))"
  11.205 +by (simp add: unify_tc2 unify_simps0 split add: option.split)
  11.206 +
  11.207 +text{*The ML version had this, but it can't be used: we get
  11.208 +*** exception THM raised: transfer: not a super theory
  11.209 +All we can do is state the desired induction rule in full and prove it.*}
  11.210 +ML{*
  11.211 +bind_thm ("unify_induct",
  11.212 +	  rule_by_tactic
  11.213 +	     (ALLGOALS (full_simp_tac (simpset() addsimps [thm"unify_tc2"])))
  11.214 +	     (thm"unify_induct0"));
  11.215 +*}
  11.216 +
  11.217 +
  11.218 +text{*Correctness. Notice that idempotence is not needed to prove that the
  11.219 +algorithm terminates and is not needed to prove the algorithm correct, if you
  11.220 +are only interested in an MGU.  This is in contrast to the approach of M&W,
  11.221 +who used idempotence and MGU-ness in the termination proof.*}
  11.222 +
  11.223 +theorem unify_gives_MGU [rule_format]:
  11.224 +     "\<forall>theta. unify(M,N) = Some theta --> MGUnifier theta M N"
  11.225 +apply (rule_tac u = M and v = N in unify_induct0)
  11.226 +apply (simp_all (no_asm_simp))
  11.227 +(*Const-Const case*)
  11.228 +apply (simp (no_asm) add: MGUnifier_def Unifier_def)
  11.229 +(*Const-Var case*)
  11.230 +apply (subst mgu_sym)
  11.231 +apply (simp (no_asm) add: MGUnifier_Var)
  11.232 +(*Var-M case*)
  11.233 +apply (simp (no_asm) add: MGUnifier_Var)
  11.234 +(*Comb-Var case*)
  11.235 +apply (subst mgu_sym)
  11.236 +apply (simp (no_asm) add: MGUnifier_Var)
  11.237 +(** LEVEL 8 **)
  11.238 +(*Comb-Comb case*)
  11.239 +apply (simp add: unify_tc2) 
  11.240 +apply (simp (no_asm_simp) split add: option.split)
  11.241 +apply (intro strip)
  11.242 +apply (simp add: MGUnifier_def Unifier_def MoreGeneral_def)
  11.243 +apply (safe, rename_tac theta sigma gamma)
  11.244 +apply (erule_tac x = gamma in allE, erule (1) notE impE)
  11.245 +apply (erule exE, rename_tac delta)
  11.246 +apply (erule_tac x = delta in allE)
  11.247 +apply (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta")
  11.248 + apply (blast intro: subst_trans intro!: subst_cong comp_assoc[THEN subst_sym])
  11.249 +apply (simp add: subst_eq_iff) 
  11.250 +done
  11.251 +
  11.252 +
  11.253 +text{*Unify returns idempotent substitutions, when it succeeds.*}
  11.254 +theorem unify_gives_Idem [rule_format]:
  11.255 +     "\<forall>theta. unify(M,N) = Some theta --> Idem theta"
  11.256 +apply (rule_tac u = M and v = N in unify_induct0)
  11.257 +apply (simp_all add: Var_Idem unify_tc2 split add: option.split)
  11.258 +txt{*Comb-Comb case*}
  11.259 +apply safe
  11.260 +apply (drule spec, erule (1) notE impE)+
  11.261 +apply (safe dest!: unify_gives_MGU [unfolded MGUnifier_def])
  11.262 +apply (rule Idem_comp, assumption+)
  11.263 +apply (force simp add: MoreGeneral_def subst_eq_iff Idem_def)
  11.264 +done
  11.265 +
  11.266  end