# HG changeset patch # User paulson # Date 1112092248 -7200 # Node ID 8408a06590a644176e2e9953ed183ac07f399a01 # Parent bca33c49b083dee0e4c75edca102b757b0ed5f19 converted HOL-Subst to tactic scripts diff -r bca33c49b083 -r 8408a06590a6 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Mon Mar 28 16:19:56 2005 +0200 +++ b/src/HOL/IsaMakefile Tue Mar 29 12:30:48 2005 +0200 @@ -191,9 +191,8 @@ HOL-Subst: HOL $(LOG)/HOL-Subst.gz -$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.ML Subst/AList.thy \ - Subst/ROOT.ML Subst/Subst.ML Subst/Subst.thy Subst/UTerm.ML \ - Subst/UTerm.thy Subst/Unifier.ML Subst/Unifier.thy Subst/Unify.ML \ +$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy \ + Subst/ROOT.ML Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy \ Subst/Unify.thy @$(ISATOOL) usedir $(OUT)/HOL Subst diff -r bca33c49b083 -r 8408a06590a6 src/HOL/Subst/AList.ML --- a/src/HOL/Subst/AList.ML Mon Mar 28 16:19:56 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ -(* Title: Subst/AList.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Association lists. -*) - -open AList; - -val prems = goal AList.thy - "[| P([]); \ -\ !!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)"; -by (induct_tac "l" 1); -by (split_all_tac 2); -by (REPEAT (ares_tac prems 1)); -qed "alist_induct"; - -(*Perform induction on xs. *) -fun alist_ind_tac a M = - EVERY [induct_thm_tac alist_induct a M, - rename_last_tac a ["1"] (M+1)]; diff -r bca33c49b083 -r 8408a06590a6 src/HOL/Subst/AList.thy --- a/src/HOL/Subst/AList.thy Mon Mar 28 16:19:56 2005 +0200 +++ b/src/HOL/Subst/AList.thy Tue Mar 29 12:30:48 2005 +0200 @@ -1,12 +1,14 @@ -(* Title: Subst/AList.thy - ID: $Id$ +(* ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -Association lists. *) -AList = Main + +header{*Association Lists*} + +theory AList +imports Main +begin consts alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c" @@ -20,4 +22,10 @@ "assoc v d [] = d" "assoc v d (p # al) = (if v = fst p then snd p else assoc v d al)" + +lemma alist_induct: + "[| P([]); + !!x y xs. P(xs) ==> P((x,y)#xs) |] ==> P(l)" +by (induct_tac "l", auto) + end diff -r bca33c49b083 -r 8408a06590a6 src/HOL/Subst/Subst.ML --- a/src/HOL/Subst/Subst.ML Mon Mar 28 16:19:56 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,205 +0,0 @@ -(* Title: HOL/Subst/Subst.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Substitutions on uterms -*) - -open Subst; - - -(**** Substitutions ****) - -Goal "t <| [] = t"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed "subst_Nil"; - -Addsimps [subst_Nil]; - -Goal "t <: u --> t <| s <: u <| s"; -by (induct_tac "u" 1); -by (ALLGOALS Asm_simp_tac); -qed_spec_mp "subst_mono"; - -Goal "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s"; -by (case_tac "t = Var(v)" 1); -by (etac rev_mp 2); -by (res_inst_tac [("P", - "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")] - uterm.induct 2); -by (ALLGOALS Asm_simp_tac); -by (Blast_tac 1); -qed_spec_mp "Var_not_occs"; - -Goal "(t <|r = t <|s) = (! v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_full_simp_tac); -by (ALLGOALS Blast_tac); -qed "agreement"; - -Goal "~ v: vars_of(t) --> t <| (v,u)#s = t <| s"; -by (simp_tac (simpset() addsimps [agreement]) 1); -qed_spec_mp"repl_invariance"; - -val asms = goal Subst.thy - "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -qed_spec_mp"Var_in_subst"; - - -(**** Equality between Substitutions ****) - -Goalw [subst_eq_def] "r =$= s = (! t. t <| r = t <| s)"; -by (Simp_tac 1); -qed "subst_eq_iff"; - - -local fun prove 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 = prove "r =$= r"; - val subst_sym = prove "r =$= s ==> s =$= r"; - val subst_trans = prove "[| q =$= r; r =$= s |] ==> q =$= s"; -end; - - -AddIffs [subst_refl]; - - -val eq::prems = goalw Subst.thy [subst_eq_def] - "[| r =$= 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 ****) - -let fun prove s = - prove_goalw Subst.thy [comp_def,sdom_def] s (fn _ => [Simp_tac 1]) -in -Addsimps - ( - map prove - [ "[] <> 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 "s <> [] = s"; -by (alist_ind_tac "s" 1); -by (ALLGOALS Asm_simp_tac); -qed "comp_Nil"; - -Addsimps [comp_Nil]; - -Goal "s =$= s <> []"; -by (Simp_tac 1); -qed "subst_comp_Nil"; - -Goal "(t <| r <> s) = (t <| r <| s)"; -by (induct_tac "t" 1); -by (ALLGOALS Asm_simp_tac); -by (alist_ind_tac "r" 1); -by (ALLGOALS Asm_simp_tac); -qed "subst_comp"; - -Addsimps [subst_comp]; - -Goal "(q <> r) <> s =$= q <> (r <> s)"; -by (simp_tac (simpset() addsimps [subst_eq_iff]) 1); -qed "comp_assoc"; - -Goal "[| theta =$= theta1; sigma =$= sigma1|] ==> \ -\ (theta <> sigma) =$= (theta1 <> sigma1)"; -by (asm_full_simp_tac (simpset() addsimps [subst_eq_def]) 1); -qed "subst_cong"; - - -Goal "(w, Var(w) <| s) # s =$= s"; -by (simp_tac (simpset() addsimps [subst_eq_iff]) 1); -by (rtac allI 1); -by (induct_tac "t" 1); -by (ALLGOALS Asm_full_simp_tac); -qed "Cons_trivial"; - - -Goal "q <> r =$= s ==> t <| q <| r = t <| s"; -by (asm_full_simp_tac (simpset() addsimps [subst_eq_iff]) 1); -qed "comp_subst_subst"; - - -(**** Domain and range of Substitutions ****) - -Goal "(v : sdom(s)) = (Var(v) <| s ~= Var(v))"; -by (alist_ind_tac "s" 1); -by (ALLGOALS Asm_simp_tac); -by (Blast_tac 1); -qed "sdom_iff"; - - -Goalw [srange_def] - "v : srange(s) = (? w. w : sdom(s) & v : vars_of(Var(w) <| s))"; -by (Blast_tac 1); -qed "srange_iff"; - -Goalw [empty_def] "(A = {}) = (ALL a.~ a:A)"; -by (Blast_tac 1); -qed "empty_iff_all_not"; - -Goal "(t <| s = t) = (sdom(s) Int vars_of(t) = {})"; -by (induct_tac "t" 1); -by (ALLGOALS - (asm_full_simp_tac (simpset() addsimps [empty_iff_all_not, sdom_iff]))); -by (ALLGOALS Blast_tac); -qed "invariance"; - -Goal "v : sdom(s) --> v : vars_of(t <| s) --> v : srange(s)"; -by (induct_tac "t" 1); -by (case_tac "a : sdom(s)" 1); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff, srange_iff]))); -by (ALLGOALS Blast_tac); -qed_spec_mp "Var_in_srange"; - -Goal "[| v : sdom(s); v ~: srange(s) |] ==> v ~: vars_of(t <| s)"; -by (blast_tac (claset() addIs [Var_in_srange]) 1); -qed "Var_elim"; - -Goal "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)"; -by (induct_tac "t" 1); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff,srange_iff]))); -by (Blast_tac 2); -by (safe_tac (claset() addSIs [exI, vars_var_iff RS iffD1 RS sym])); -by Auto_tac; -qed_spec_mp "Var_intro"; - -Goal "v : srange(s) --> (? w. w : sdom(s) & v : vars_of(Var(w) <| s))"; -by (simp_tac (simpset() addsimps [srange_iff]) 1); -qed_spec_mp "srangeD"; - -Goal "sdom(s) Int srange(s) = {} = (! t. sdom(s) Int vars_of(t <| s) = {})"; -by (simp_tac (simpset() addsimps [empty_iff_all_not]) 1); -by (fast_tac (claset() addIs [Var_in_srange] addDs [srangeD]) 1); -qed "dom_range_disjoint"; - -Goal "~ u <| s = u ==> (? x. x : sdom(s))"; -by (full_simp_tac (simpset() addsimps [empty_iff_all_not, invariance]) 1); -by (Blast_tac 1); -qed "subst_not_empty"; - - -Goal "(M <| [(x, Var x)]) = M"; -by (induct_tac "M" 1); -by (ALLGOALS Asm_simp_tac); -qed "id_subst_lemma"; - -Addsimps [id_subst_lemma]; diff -r bca33c49b083 -r 8408a06590a6 src/HOL/Subst/Subst.thy --- a/src/HOL/Subst/Subst.thy Mon Mar 28 16:19:56 2005 +0200 +++ b/src/HOL/Subst/Subst.thy Tue Mar 29 12:30:48 2005 +0200 @@ -2,11 +2,13 @@ ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge - -Substitutions on uterms *) -Subst = AList + UTerm + +header{*Substitutions on uterms*} + +theory Subst +imports AList UTerm +begin consts @@ -19,22 +21,170 @@ primrec - 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)" + 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)" defs - subst_eq_def "r =$= s == ALL t. t <| r = t <| s" + subst_eq_def: "r =$= s == ALL t. t <| r = t <| s" - comp_def "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)" + comp_def: "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)" - sdom_def + 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_def: "srange(al) == Union({y. EX x:sdom(al). y=vars_of(Var(x) <| al)})" + + +subsection{*Basic Laws*} + +lemma subst_Nil [simp]: "t <| [] = t" +by (induct_tac "t", auto) + +lemma subst_mono [rule_format]: "t <: u --> t <| s <: u <| s" +by (induct_tac "u", auto) + +lemma Var_not_occs [rule_format]: + "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s" +apply (case_tac "t = Var v") +apply (erule_tac [2] rev_mp) +apply (rule_tac [2] P = "%x.~x=Var (v) --> ~ (Var (v) <: x) --> x <| (v,t<|s) #s=x<|s" in uterm.induct) +apply auto +done + +lemma agreement: "(t <|r = t <|s) = (\v. v : vars_of(t) --> Var(v) <|r = Var(v) <|s)" +by (induct_tac "t", auto) + +lemma repl_invariance: "~ v: vars_of(t) ==> t <| (v,u)#s = t <| s" +by (simp add: agreement) + +lemma Var_in_subst [rule_format]: + "v : vars_of(t) --> w : vars_of(t <| (v,Var(w))#s)" +by (induct_tac "t", auto) + + +subsection{*Equality between Substitutions*} + +lemma subst_eq_iff: "r =$= s = (\t. t <| r = t <| s)" +by (simp add: subst_eq_def) + +lemma subst_refl [iff]: "r =$= r" +by (simp add: subst_eq_iff) + +lemma subst_sym: "r =$= s ==> s =$= r" +by (simp add: subst_eq_iff) + +lemma subst_trans: "[| q =$= r; r =$= s |] ==> q =$= s" +by (simp add: subst_eq_iff) + +lemma subst_subst2: + "[| r =$= s; P (t <| r) (u <| r) |] ==> P (t <| s) (u <| s)" +by (simp add: subst_eq_def) + +lemmas ssubst_subst2 = subst_sym [THEN subst_subst2] + + +subsection{*Composition of Substitutions*} + +lemma [simp]: + "[] <> 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})" +by (simp_all add: comp_def sdom_def) + +lemma comp_Nil [simp]: "s <> [] = s" +by (induct "s", auto) + +lemma subst_comp_Nil: "s =$= s <> []" +by simp + +lemma subst_comp [simp]: "(t <| r <> s) = (t <| r <| s)" +apply (induct_tac "t") +apply (simp_all (no_asm_simp)) +apply (induct "r", auto) +done + +lemma comp_assoc: "(q <> r) <> s =$= q <> (r <> s)" +apply (simp (no_asm) add: subst_eq_iff) +done + +lemma subst_cong: + "[| theta =$= theta1; sigma =$= sigma1|] + ==> (theta <> sigma) =$= (theta1 <> sigma1)" +by (simp add: subst_eq_def) + + +lemma Cons_trivial: "(w, Var(w) <| s) # s =$= s" +apply (simp add: subst_eq_iff) +apply (rule allI) +apply (induct_tac "t", simp_all) +done + + +lemma comp_subst_subst: "q <> r =$= s ==> t <| q <| r = t <| s" +by (simp add: subst_eq_iff) + + +subsection{*Domain and range of Substitutions*} + +lemma sdom_iff: "(v : sdom(s)) = (Var(v) <| s ~= Var(v))" +apply (induct "s") +apply (case_tac [2] a, auto) +done + + +lemma srange_iff: + "v : srange(s) = (\w. w : sdom(s) & v : vars_of(Var(w) <| s))" +by (auto simp add: srange_def) + +lemma empty_iff_all_not: "(A = {}) = (ALL a.~ a:A)" +by (unfold empty_def, blast) + +lemma invariance: "(t <| s = t) = (sdom(s) Int vars_of(t) = {})" +apply (induct_tac "t") +apply (auto simp add: empty_iff_all_not sdom_iff) +done + +lemma Var_in_srange [rule_format]: + "v : sdom(s) --> v : vars_of(t <| s) --> v : srange(s)" +apply (induct_tac "t") +apply (case_tac "a : sdom (s) ") +apply (auto simp add: sdom_iff srange_iff) +done + +lemma Var_elim: "[| v : sdom(s); v ~: srange(s) |] ==> v ~: vars_of(t <| s)" +by (blast intro: Var_in_srange) + +lemma Var_intro [rule_format]: + "v : vars_of(t <| s) --> v : srange(s) | v : vars_of(t)" +apply (induct_tac "t") +apply (auto simp add: sdom_iff srange_iff) +apply (rule_tac x=a in exI, auto) +done + +lemma srangeD [rule_format]: + "v : srange(s) --> (\w. w : sdom(s) & v : vars_of(Var(w) <| s))" +apply (simp (no_asm) add: srange_iff) +done + +lemma dom_range_disjoint: + "sdom(s) Int srange(s) = {} = (\t. sdom(s) Int vars_of(t <| s) = {})" +apply (simp (no_asm) add: empty_iff_all_not) +apply (force intro: Var_in_srange dest: srangeD) +done + +lemma subst_not_empty: "~ u <| s = u ==> (\x. x : sdom(s))" +by (auto simp add: empty_iff_all_not invariance) + + +lemma id_subst_lemma [simp]: "(M <| [(x, Var x)]) = M" +by (induct_tac "M", auto) + + end diff -r bca33c49b083 -r 8408a06590a6 src/HOL/Subst/UTerm.ML --- a/src/HOL/Subst/UTerm.ML Mon Mar 28 16:19:56 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,45 +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 "(v : vars_of(Var(w))) = (w=v)"; -by (Simp_tac 1); -by (fast_tac HOL_cs 1); -qed "vars_var_iff"; - -Goal "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)"; -by (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 "M<:N --> vars_of(M) <= vars_of(N)"; -by (induct_tac "N" 1); -by (ALLGOALS Asm_simp_tac); -by (fast_tac set_cs 1); -val occs_vars_subset = result(); - - -Goal "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)"; -by (Blast_tac 1); -val monotone_vars_of = result(); - -Goal "finite(vars_of M)"; -by (induct_tac"M" 1); -by (ALLGOALS Simp_tac); -by (ftac finite_UnI 1); -by (assume_tac 1); -by (Asm_simp_tac 1); -val finite_vars_of = result(); diff -r bca33c49b083 -r 8408a06590a6 src/HOL/Subst/UTerm.thy --- a/src/HOL/Subst/UTerm.thy Mon Mar 28 16:19:56 2005 +0200 +++ b/src/HOL/Subst/UTerm.thy Tue Mar 29 12:30:48 2005 +0200 @@ -1,38 +1,61 @@ -(* Title: Subst/UTerm.thy - ID: $Id$ +(* ID: $Id$ 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 = Main + +header{*Simple Term Structure for Unification*} + +theory UTerm +imports Main -datatype 'a uterm = Var ('a) - | Const ('a) - | Comb ('a uterm) ('a uterm) +begin + +text{*Binary trees with leaves that are constants or variables.*} + +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 + vars_of :: "'a uterm => 'a set" + "<:" :: "'a uterm => 'a uterm => bool" (infixl 54) +uterm_size :: "'a uterm => nat" + + +primrec + 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 - 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))" - + 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 - 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)" + 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)" + + +lemma vars_var_iff: "(v : vars_of(Var(w))) = (w=v)" +by auto + +lemma vars_iff_occseq: "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)" +by (induct_tac "t", auto) + -primrec - 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)" +(* Not used, but perhaps useful in other proofs *) +lemma occs_vars_subset: "M<:N --> vars_of(M) <= vars_of(N)" +by (induct_tac "N", auto) + + +lemma monotone_vars_of: "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)" +by blast + +lemma finite_vars_of: "finite(vars_of M)" +by (induct_tac "M", auto) + end diff -r bca33c49b083 -r 8408a06590a6 src/HOL/Subst/Unifier.ML --- a/src/HOL/Subst/Unifier.ML Mon Mar 28 16:19:56 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,99 +0,0 @@ -(* Title: HOL/Subst/Unifier.ML - ID: $Id$ - Author: Martin Coen, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge - -Properties of unifiers. -*) - -open Unifier; - -val unify_defs = [Unifier_def, MoreGeneral_def, MGUnifier_def]; - -(*--------------------------------------------------------------------------- - * Unifiers - *---------------------------------------------------------------------------*) - -Goal "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)"; -by (simp_tac (simpset() addsimps [Unifier_def]) 1); -qed "Unifier_Comb"; - -AddIffs [Unifier_Comb]; - -Goal "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> \ -\ Unifier ((v,r)#s) t u"; -by (asm_full_simp_tac (simpset() addsimps [Unifier_def, repl_invariance]) 1); -qed "Cons_Unifier"; - - -(*--------------------------------------------------------------------------- - * Most General Unifiers - *---------------------------------------------------------------------------*) - -Goalw unify_defs "MGUnifier s t u = MGUnifier s u t"; -by (blast_tac (claset() addIs [sym]) 1); -qed "mgu_sym"; - - -Goal "[] >> s"; -by (simp_tac (simpset() addsimps [MoreGeneral_def]) 1); -by (Blast_tac 1); -qed "MoreGen_Nil"; - -AddIffs [MoreGen_Nil]; - -Goalw unify_defs - "MGUnifier s t u = (ALL r. Unifier r t u = s >> r)"; -by (auto_tac (claset() addIs [ssubst_subst2, subst_comp_Nil], simpset())); -qed "MGU_iff"; - - -Goal "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t"; -by (simp_tac(simpset() addsimps [MGU_iff, Unifier_def, MoreGeneral_def] - delsimps [subst_Var]) 1); -by Safe_tac; -by (rtac exI 1); -by (etac subst 1 THEN rtac (Cons_trivial RS subst_sym) 1); -by (etac ssubst_subst2 1); -by (asm_simp_tac (simpset() addsimps [Var_not_occs]) 1); -qed "MGUnifier_Var"; - -AddSIs [MGUnifier_Var]; - - -(*--------------------------------------------------------------------------- - * Idempotence. - *---------------------------------------------------------------------------*) - -Goalw [Idem_def] "Idem([])"; -by (Simp_tac 1); -qed "Idem_Nil"; - -AddIffs [Idem_Nil]; - -Goalw [Idem_def] "Idem(s) = (sdom(s) Int srange(s) = {})"; -by (simp_tac (simpset() addsimps [subst_eq_iff, invariance, - dom_range_disjoint]) 1); -qed "Idem_iff"; - -Goal "~ (Var(v) <: t) --> Idem([(v,t)])"; -by (simp_tac (simpset() addsimps [vars_iff_occseq, Idem_iff, srange_iff, - empty_iff_all_not]) 1); -qed_spec_mp "Var_Idem"; - -AddSIs [Var_Idem]; - -Goalw [Idem_def] - "[| Idem(r); Unifier s (t<|r) (u<|r) |] \ -\ ==> Unifier (r <> s) (t <| r) (u <| r)"; -by (asm_full_simp_tac (simpset() addsimps [Unifier_def, comp_subst_subst]) 1); -qed "Unifier_Idem_subst"; - -val [idemr,unifier,minor] = goal Unifier.thy - "[| Idem(r); Unifier s (t <| r) (u <| r); \ -\ !!q. Unifier q (t <| r) (u <| r) ==> s <> q =$= q \ -\ |] ==> Idem(r <> s)"; -by (cut_facts_tac [idemr, - unifier RS (idemr RS Unifier_Idem_subst RS minor)] 1); -by (asm_full_simp_tac (simpset() addsimps [Idem_def, subst_eq_iff]) 1); -qed "Idem_comp"; diff -r bca33c49b083 -r 8408a06590a6 src/HOL/Subst/Unifier.thy --- a/src/HOL/Subst/Unifier.thy Mon Mar 28 16:19:56 2005 +0200 +++ b/src/HOL/Subst/Unifier.thy Tue Mar 29 12:30:48 2005 +0200 @@ -1,12 +1,15 @@ -(* Title: Subst/Unifier.thy - ID: $Id$ +(* ID: $Id$ Author: Martin Coen, Cambridge University Computer Laboratory Copyright 1993 University of Cambridge -Definition of most general unifier *) -Unifier = Subst + +header{*Definition of Most General Unifier*} + +theory Unifier +imports Subst + +begin consts @@ -17,9 +20,76 @@ defs - Unifier_def "Unifier s t u == t <| s = u <| s" - MoreGeneral_def "r >> s == ? q. 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" + Unifier_def: "Unifier s t u == t <| s = u <| s" + MoreGeneral_def: "r >> s == ? q. 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" + + + +lemmas unify_defs = Unifier_def MoreGeneral_def MGUnifier_def + + +subsection{*Unifiers*} + +lemma Unifier_Comb [iff]: "Unifier s (Comb t u) (Comb v w) = (Unifier s t v & Unifier s u w)" +by (simp add: Unifier_def) + + +lemma Cons_Unifier: "[| v ~: vars_of t; v ~: vars_of u; Unifier s t u |] ==> Unifier ((v,r)#s) t u" +by (simp add: Unifier_def repl_invariance) + + +subsection{* Most General Unifiers*} + +lemma mgu_sym: "MGUnifier s t u = MGUnifier s u t" +by (simp add: unify_defs eq_commute) + + +lemma MoreGen_Nil [iff]: "[] >> s" +by (auto simp add: MoreGeneral_def) + +lemma MGU_iff: "MGUnifier s t u = (ALL r. Unifier r t u = s >> r)" +apply (unfold unify_defs) +apply (auto intro: ssubst_subst2 subst_comp_Nil) +done + +lemma MGUnifier_Var: "~ Var v <: t ==> MGUnifier [(v,t)] (Var v) t" +apply (simp (no_asm) add: MGU_iff Unifier_def MoreGeneral_def del: subst_Var) +apply safe +apply (rule exI) +apply (erule subst, rule Cons_trivial [THEN subst_sym]) +apply (erule ssubst_subst2) +apply (simp (no_asm_simp) add: Var_not_occs) +done + +declare MGUnifier_Var [intro!] + + +subsection{*Idempotence*} + +lemma Idem_Nil [iff]: "Idem([])" +by (simp add: Idem_def) + +lemma Idem_iff: "Idem(s) = (sdom(s) Int srange(s) = {})" +by (simp add: Idem_def subst_eq_iff invariance dom_range_disjoint) + +lemma Var_Idem [intro!]: "~ (Var(v) <: t) ==> Idem([(v,t)])" +by (simp add: vars_iff_occseq Idem_iff srange_iff empty_iff_all_not) + +lemma Unifier_Idem_subst: + "[| Idem(r); Unifier s (t<|r) (u<|r) |] + ==> Unifier (r <> s) (t <| r) (u <| r)" +by (simp add: Idem_def Unifier_def comp_subst_subst) + +lemma Idem_comp: + "[| Idem(r); Unifier s (t <| r) (u <| r); + !!q. Unifier q (t <| r) (u <| r) ==> s <> q =$= q + |] ==> Idem(r <> s)" +apply (frule Unifier_Idem_subst, blast) +apply (force simp add: Idem_def subst_eq_iff) +done + + end diff -r bca33c49b083 -r 8408a06590a6 src/HOL/Subst/Unify.ML --- a/src/HOL/Subst/Unify.ML Mon Mar 28 16:19:56 2005 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,251 +0,0 @@ -(* Title: Subst/Unify - ID: $Id$ - Author: Konrad Slind, Cambridge University Computer Laboratory - Copyright 1997 University of Cambridge - -Unification algorithm -*) - -(*--------------------------------------------------------------------------- - * 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). - *---------------------------------------------------------------------------*) - -(*--------------------------------------------------------------------------- - * The non-nested TC plus the wellfoundedness of unifyRel. - *---------------------------------------------------------------------------*) -Tfl.tgoalw Unify.thy [] unify.simps; -(* Wellfoundedness of unifyRel *) -by (simp_tac (simpset() addsimps [unifyRel_def, - wf_inv_image, wf_lex_prod, wf_finite_psubset, - wf_measure]) 1); -(* TC *) -by Safe_tac; -by (simp_tac (simpset() addsimps [finite_psubset_def, finite_vars_of, - lex_prod_def, measure_def, inv_image_def]) 1); -by (rtac (monotone_vars_of RS (subset_iff_psubset_eq RS iffD1) RS disjE) 1); -by (Blast_tac 1); -by (asm_simp_tac (simpset() addsimps [less_eq, less_add_Suc1]) 1); -qed "tc0"; - - -(*--------------------------------------------------------------------------- - * Termination proof. - *---------------------------------------------------------------------------*) - -Goalw [unifyRel_def, measure_def] "trans unifyRel"; -by (REPEAT (resolve_tac [trans_inv_image, trans_lex_prod, - trans_finite_psubset, trans_less_than, - trans_inv_image] 1)); -qed "trans_unifyRel"; - - -(*--------------------------------------------------------------------------- - * The following lemma is used in the last step of the termination proof for - * the nested call in Unify. Loosely, it says that unifyRel doesn't care - * about term structure. - *---------------------------------------------------------------------------*) -Goalw [unifyRel_def,lex_prod_def, inv_image_def] - "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel ==> \ -\ ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel"; -by (asm_full_simp_tac (simpset() addsimps [measure_def, - less_eq, inv_image_def,add_assoc]) 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 (Blast_tac 2); -by (Asm_simp_tac 1); -qed "Rassoc"; - - -(*--------------------------------------------------------------------------- - * This lemma proves the nested termination condition for the base cases - * 3, 4, and 6. - *---------------------------------------------------------------------------*) -Goal "~(Var x <: M) ==> \ -\ ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel \ -\ & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel"; -by (case_tac "Var x = M" 1); -by (hyp_subst_tac 1); -by (Simp_tac 1); -by (case_tac "x: (vars_of N1 Un vars_of N2)" 1); -(*uterm_less case*) -by (asm_simp_tac - (simpset() addsimps [less_eq, unifyRel_def, lex_prod_def, - measure_def, inv_image_def]) 1); -by (Blast_tac 1); -(*finite_psubset case*) -by (simp_tac - (simpset() addsimps [unifyRel_def, lex_prod_def, - measure_def, inv_image_def]) 1); -by (simp_tac (simpset() addsimps [finite_psubset_def, finite_vars_of, - psubset_def]) 1); -by (Blast_tac 1); -(** LEVEL 9 **) -(*Final case, also finite_psubset*) -by (simp_tac - (simpset() addsimps [finite_vars_of, unifyRel_def, finite_psubset_def, - lex_prod_def, measure_def, inv_image_def]) 1); -by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N2")] Var_elim 1); -by (cut_inst_tac [("s","[(x,M)]"), ("v", "x"), ("t","N1")] Var_elim 3); -by (ALLGOALS (asm_simp_tac(simpset() addsimps [srange_iff, vars_iff_occseq]))); -by (REPEAT_FIRST (resolve_tac [conjI, disjI1, psubsetI])); -by (ALLGOALS (asm_full_simp_tac - (simpset() addsimps [srange_iff]))); -by (ALLGOALS - (fast_tac (claset() addEs [Var_intro RS disjE] - addss (simpset() addsimps [srange_iff])))); -qed "var_elimR"; - - -(*--------------------------------------------------------------------------- - * Eliminate tc0 from the recursion equations and the induction theorem. - *---------------------------------------------------------------------------*) -val wfr = tc0 RS conjunct1 -and tc = tc0 RS conjunct2; -val unifyRules0 = map (rule_by_tactic (rtac wfr 1 THEN TRY(rtac tc 1))) - unify.simps; - -val unifyInduct0 = [wfr,tc] MRS unify.induct; - - -(*--------------------------------------------------------------------------- - * The nested TC. Proved by recursion induction. - *---------------------------------------------------------------------------*) -val [_,_,tc3] = unify.tcs; -goalw_cterm [] (cterm_of (sign_of Unify.thy) (HOLogic.mk_Trueprop tc3)); -(*--------------------------------------------------------------------------- - * 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) = Some theta --> \ - \ (!N1 N2. ((N1<|theta, N2<|theta), (Comb M1 N1, Comb M2 N2)) : unifyRel)" 1); -by (Blast_tac 1); -by (rtac allI 1); -by (rtac allI 1); -(* Apply induction *) -by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1); -by (ALLGOALS - (asm_simp_tac (simpset() addsimps (var_elimR::unifyRules0)))); -(*Const-Const case*) -by (simp_tac - (simpset() addsimps [unifyRel_def, lex_prod_def, measure_def, - inv_image_def, less_eq]) 1); -(** LEVEL 7 **) -(*Comb-Comb case*) -by (asm_simp_tac (simpset() addsplits [option.split]) 1); -by (strip_tac 1); -by (rtac (trans_unifyRel RS transD) 1); -by (Blast_tac 1); -by (simp_tac (HOL_ss addsimps [subst_Comb RS sym]) 1); -by (rtac Rassoc 1); -by (Blast_tac 1); -qed_spec_mp "unify_TC"; - - -(*--------------------------------------------------------------------------- - * Now for elimination of nested TC from unify.simps and induction. - *---------------------------------------------------------------------------*) - -(*Desired rule, copied from the theory file. Could it be made available?*) -Goal "unify(Comb M1 N1, Comb M2 N2) = \ -\ (case unify(M1,M2) \ -\ of None => None \ -\ | Some theta => (case unify(N1 <| theta, N2 <| theta) \ -\ of None => None \ -\ | Some sigma => Some (theta <> sigma)))"; -by (asm_simp_tac (simpset() addsimps (unify_TC::unifyRules0) - addsplits [option.split]) 1); -qed "unifyCombComb"; - - -val unifyRules = rev (unifyCombComb :: tl (rev unifyRules0)); - -Addsimps unifyRules; - -bind_thm ("unifyInduct", - rule_by_tactic - (ALLGOALS (full_simp_tac (simpset() addsimps [unify_TC]))) - unifyInduct0); - - -(*--------------------------------------------------------------------------- - * 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 "!theta. unify(M,N) = Some theta --> MGUnifier theta M N"; -by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1); -by (ALLGOALS Asm_simp_tac); -(*Const-Const case*) -by (simp_tac (simpset() addsimps [MGUnifier_def,Unifier_def]) 1); -(*Const-Var case*) -by (stac mgu_sym 1); -by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1); -(*Var-M case*) -by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1); -(*Comb-Var case*) -by (stac mgu_sym 1); -by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1); -(** LEVEL 8 **) -(*Comb-Comb case*) -by (asm_simp_tac (simpset() addsplits [option.split]) 1); -by (strip_tac 1); -by (asm_full_simp_tac - (simpset() addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1); -by (Safe_tac THEN rename_tac "theta sigma gamma" 1); -by (eres_inst_tac [("x","gamma")] allE 1 THEN mp_tac 1); -by (etac exE 1 THEN rename_tac "delta" 1); -by (eres_inst_tac [("x","delta")] allE 1); -by (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta" 1); -(*Proving the subgoal*) -by (full_simp_tac (simpset() addsimps [subst_eq_iff]) 2 - THEN blast_tac (claset() addIs [trans,sym] delrules [impCE]) 2); -by (blast_tac (claset() addIs [subst_trans, subst_cong, - comp_assoc RS subst_sym]) 1); -qed_spec_mp "unify_gives_MGU"; - - -(*--------------------------------------------------------------------------- - * Unify returns idempotent substitutions, when it succeeds. - *---------------------------------------------------------------------------*) -Goal "!theta. unify(M,N) = Some theta --> Idem theta"; -by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1); -by (ALLGOALS - (asm_simp_tac - (simpset() addsimps [Var_Idem] addsplits [option.split]))); -(*Comb-Comb case*) -by Safe_tac; -by (REPEAT (dtac spec 1 THEN mp_tac 1)); -by (safe_tac (claset() addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU])); -by (rtac Idem_comp 1); -by (atac 1); -by (atac 1); -by (best_tac (claset() addss (simpset() addsimps - [MoreGeneral_def, subst_eq_iff, Idem_def])) 1); -qed_spec_mp "unify_gives_Idem"; - diff -r bca33c49b083 -r 8408a06590a6 src/HOL/Subst/Unify.thy --- a/src/HOL/Subst/Unify.thy Mon Mar 28 16:19:56 2005 +0200 +++ b/src/HOL/Subst/Unify.thy Tue Mar 29 12:30:48 2005 +0200 @@ -1,12 +1,26 @@ -(* Title: Subst/Unify - ID: $Id$ +(* ID: $Id$ Author: Konrad Slind, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge -Unification algorithm *) -Unify = Unifier + +header{*Unification Algorithm*} + +theory Unify +imports Unifier +begin + +text{* +Substitution and Unification in Higher-Order Logic. + +Implements Manna and Waldinger's formalization, with Paulson's simplifications, +and some new simplifications by Slind. + +Z Manna and 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 +*} consts @@ -14,26 +28,218 @@ unify :: "'a uterm * 'a uterm => ('a * 'a uterm) list option" defs + unifyRel_def: + "unifyRel == inv_image (finite_psubset <*lex*> measure uterm_size) + (%(M,N). (vars_of M Un vars_of N, M))" + --{*Termination relation for the Unify function: + either the set of variables decreases, + or the first argument does (in fact, both do) *} - (*Termination relation for the Unify function: - --either the set of variables decreases - --or the first argument does (in fact, both do) - *) - unifyRel_def "unifyRel == inv_image (finite_psubset <*lex*> measure uterm_size) - (%(M,N). (vars_of M Un vars_of N, M))" +text{* Wellfoundedness of unifyRel *} +lemma wf_unifyRel [iff]: "wf unifyRel" +by (simp add: unifyRel_def wf_lex_prod wf_finite_psubset) -recdef unify "unifyRel" - "unify(Const m, Const n) = (if (m=n) then Some[] else None)" - "unify(Const m, Comb M N) = None" - "unify(Const m, Var v) = Some[(v,Const m)]" - "unify(Var v, M) = (if (Var v <: M) then None else Some[(v,M)])" - "unify(Comb M N, Const x) = None" - "unify(Comb M N, Var v) = (if (Var v <: Comb M N) then None - else Some[(v,Comb M N)])" + +recdef (permissive) unify "unifyRel" + unify_CC: "unify(Const m, Const n) = (if (m=n) then Some[] else None)" + unify_CB: "unify(Const m, Comb M N) = None" + unify_CV: "unify(Const m, Var v) = Some[(v,Const m)]" + unify_V: "unify(Var v, M) = (if (Var v <: M) then None else Some[(v,M)])" + unify_BC: "unify(Comb M N, Const x) = None" + unify_BV: "unify(Comb M N, Var v) = (if (Var v <: Comb M N) then None + else Some[(v,Comb M N)])" + unify_BB: "unify(Comb M1 N1, Comb M2 N2) = (case unify(M1,M2) of None => None | Some theta => (case unify(N1 <| theta, N2 <| theta) of None => None | Some sigma => Some (theta <> sigma)))" + (hints recdef_wf: wf_unifyRel) + + + +(*--------------------------------------------------------------------------- + * 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). + *---------------------------------------------------------------------------*) + +text{*The non-nested TC (terminiation condition). This declaration form +only seems to return one subgoal outstanding from the recdef.*} +recdef_tc unify_tc1: unify +apply (simp add: unifyRel_def wf_lex_prod wf_finite_psubset, safe) +apply (simp add: finite_psubset_def finite_vars_of lex_prod_def measure_def inv_image_def) +apply (rule monotone_vars_of [THEN subset_iff_psubset_eq [THEN iffD1]]) +done + + + + +text{*Termination proof.*} + +lemma trans_unifyRel: "trans unifyRel" +by (simp add: unifyRel_def measure_def trans_inv_image trans_lex_prod + trans_finite_psubset) + + +text{*The following lemma is used in the last step of the termination proof +for the nested call in Unify. Loosely, it says that unifyRel doesn't care +about term structure.*} +lemma Rassoc: + "((X,Y), (Comb A (Comb B C), Comb D (Comb E F))) : unifyRel ==> + ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) : unifyRel" +by (simp add: measure_def less_eq inv_image_def add_assoc Un_assoc + unifyRel_def lex_prod_def) + + +text{*This lemma proves the nested termination condition for the base cases + * 3, 4, and 6.*} +lemma var_elimR: + "~(Var x <: M) ==> + ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb M N1, Comb(Var x) N2)) : unifyRel + & ((N1 <| [(x,M)], N2 <| [(x,M)]), (Comb(Var x) N1, Comb M N2)) : unifyRel" +apply (case_tac "Var x = M", clarify, simp) +apply (case_tac "x: (vars_of N1 Un vars_of N2) ") +txt{*uterm_less case*} +apply (simp add: less_eq unifyRel_def lex_prod_def measure_def inv_image_def) +apply blast +txt{*@{text finite_psubset} case*} +apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def) +apply (simp add: finite_psubset_def finite_vars_of psubset_def) +apply blast +txt{*Final case, also {text finite_psubset}*} +apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_def measure_def inv_image_def) +apply (cut_tac s = "[ (x,M) ]" and v = x and t = N2 in Var_elim) +apply (cut_tac [3] s = "[ (x,M) ]" and v = x and t = N1 in Var_elim) +apply (simp_all (no_asm_simp) add: srange_iff vars_iff_occseq) +apply (auto elim!: Var_intro [THEN disjE] simp add: srange_iff) +done + + +text{*Eliminate tc1 from the recursion equations and the induction theorem.*} + +lemmas unify_nonrec [simp] = + unify_CC unify_CB unify_CV unify_V unify_BC unify_BV + +lemmas unify_simps0 = unify_nonrec unify_BB [OF unify_tc1] + +lemmas unify_induct0 = unify.induct [OF unify_tc1] + +text{*The nested TC. Proved by recursion induction.*} +lemma unify_tc2: + "\M1 M2 N1 N2 theta. + unify (M1, M2) = Some theta \ + ((N1 <| theta, N2 <| theta), Comb M1 N1, Comb M2 N2) \ unifyRel" +txt{*The extracted TC needs the scope of its quantifiers adjusted, so our + first step is to restrict the scopes of N1 and N2.*} +apply (subgoal_tac "\M1 M2 theta. unify (M1, M2) = Some theta --> + (\N1 N2.((N1<|theta, N2<|theta), (Comb M1 N1, Comb M2 N2)) : unifyRel)") +apply blast +apply (rule allI) +apply (rule allI) +txt{*Apply induction on this still-quantified formula*} +apply (rule_tac u = M1 and v = M2 in unify_induct0) +apply (simp_all (no_asm_simp) add: var_elimR unify_simps0) +txt{*Const-Const case*} +apply (simp add: unifyRel_def lex_prod_def measure_def inv_image_def less_eq) +txt{*Comb-Comb case*} +apply (simp (no_asm_simp) split add: option.split) +apply (intro strip) +apply (rule trans_unifyRel [THEN transD], blast) +apply (simp only: subst_Comb [symmetric]) +apply (rule Rassoc, blast) +done + + +text{* Now for elimination of nested TC from unify.simps and induction.*} + +text{*Desired rule, copied from the theory file.*} +lemma unifyCombComb [simp]: + "unify(Comb M1 N1, Comb M2 N2) = + (case unify(M1,M2) + of None => None + | Some theta => (case unify(N1 <| theta, N2 <| theta) + of None => None + | Some sigma => Some (theta <> sigma)))" +by (simp add: unify_tc2 unify_simps0 split add: option.split) + +text{*The ML version had this, but it can't be used: we get +*** exception THM raised: transfer: not a super theory +All we can do is state the desired induction rule in full and prove it.*} +ML{* +bind_thm ("unify_induct", + rule_by_tactic + (ALLGOALS (full_simp_tac (simpset() addsimps [thm"unify_tc2"]))) + (thm"unify_induct0")); +*} + + +text{*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.*} + +theorem unify_gives_MGU [rule_format]: + "\theta. unify(M,N) = Some theta --> MGUnifier theta M N" +apply (rule_tac u = M and v = N in unify_induct0) +apply (simp_all (no_asm_simp)) +(*Const-Const case*) +apply (simp (no_asm) add: MGUnifier_def Unifier_def) +(*Const-Var case*) +apply (subst mgu_sym) +apply (simp (no_asm) add: MGUnifier_Var) +(*Var-M case*) +apply (simp (no_asm) add: MGUnifier_Var) +(*Comb-Var case*) +apply (subst mgu_sym) +apply (simp (no_asm) add: MGUnifier_Var) +(** LEVEL 8 **) +(*Comb-Comb case*) +apply (simp add: unify_tc2) +apply (simp (no_asm_simp) split add: option.split) +apply (intro strip) +apply (simp add: MGUnifier_def Unifier_def MoreGeneral_def) +apply (safe, rename_tac theta sigma gamma) +apply (erule_tac x = gamma in allE, erule (1) notE impE) +apply (erule exE, rename_tac delta) +apply (erule_tac x = delta in allE) +apply (subgoal_tac "N1 <| theta <| delta = N2 <| theta <| delta") + apply (blast intro: subst_trans intro!: subst_cong comp_assoc[THEN subst_sym]) +apply (simp add: subst_eq_iff) +done + + +text{*Unify returns idempotent substitutions, when it succeeds.*} +theorem unify_gives_Idem [rule_format]: + "\theta. unify(M,N) = Some theta --> Idem theta" +apply (rule_tac u = M and v = N in unify_induct0) +apply (simp_all add: Var_Idem unify_tc2 split add: option.split) +txt{*Comb-Comb case*} +apply safe +apply (drule spec, erule (1) notE impE)+ +apply (safe dest!: unify_gives_MGU [unfolded MGUnifier_def]) +apply (rule Idem_comp, assumption+) +apply (force simp add: MoreGeneral_def subst_eq_iff Idem_def) +done + end