--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Sun Aug 21 21:18:59 2011 -0700
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Mon Aug 22 10:57:33 2011 +0200
@@ -28,11 +28,12 @@
TYPE_DEFINITION > HOL4Setup.TYPE_DEFINITION
LET > HOL4Compat.LET;
-ignore_thms
+(*ignore_thms
BOUNDED_DEF
BOUNDED_THM
UNBOUNDED_DEF
UNBOUNDED_THM;
+*)
end_import;
--- a/src/HOL/Import/Generate-HOL/ROOT.ML Sun Aug 21 21:18:59 2011 -0700
+++ b/src/HOL/Import/Generate-HOL/ROOT.ML Mon Aug 22 10:57:33 2011 +0200
@@ -1,3 +1,5 @@
+Runtime.debug := true;
+
use_thy "GenHOL4Prob";
use_thy "GenHOL4Vec";
use_thy "GenHOL4Word32";
--- a/src/HOL/IsaMakefile Sun Aug 21 21:18:59 2011 -0700
+++ b/src/HOL/IsaMakefile Mon Aug 22 10:57:33 2011 +0200
@@ -70,7 +70,6 @@
HOL-SPARK-Examples \
HOL-Word-SMT_Examples \
HOL-Statespace \
- HOL-Subst \
TLA-Buffer \
TLA-Inc \
TLA-Memory \
@@ -496,15 +495,6 @@
@$(ISABELLE_TOOL) usedir -g true $(OUT)/HOL Hahn_Banach
-## HOL-Subst
-
-HOL-Subst: HOL $(LOG)/HOL-Subst.gz
-
-$(LOG)/HOL-Subst.gz: $(OUT)/HOL Subst/AList.thy Subst/ROOT.ML \
- Subst/Subst.thy Subst/UTerm.thy Subst/Unifier.thy Subst/Unify.thy
- @$(ISABELLE_TOOL) usedir $(OUT)/HOL Subst
-
-
## HOL-Induct
HOL-Induct: HOL $(LOG)/HOL-Induct.gz
@@ -1754,7 +1744,7 @@
$(LOG)/HOL-Proofs-Lambda.gz $(LOG)/HOL-SET_Protocol.gz \
$(LOG)/HOL-Word-SMT_Examples.gz \
$(LOG)/HOL-SPARK.gz $(LOG)/HOL-SPARK-Examples.gz \
- $(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \
+ $(LOG)/HOL-Statespace.gz \
$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \
$(LOG)/HOL-Word-Examples.gz $(LOG)/HOL-Word.gz \
$(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz $(LOG)/HOL.gz \
--- a/src/HOL/NanoJava/Decl.thy Sun Aug 21 21:18:59 2011 -0700
+++ b/src/HOL/NanoJava/Decl.thy Mon Aug 22 10:57:33 2011 +0200
@@ -44,9 +44,9 @@
(type) "cdecl" \<leftharpoondown> (type) "cname \<times> class"
(type) "prog " \<leftharpoondown> (type) "cdecl list"
-consts
-
+axiomatization
Prog :: prog --{* program as a global value *}
+and
Object :: cname --{* name of root class *}
--- a/src/HOL/NanoJava/Example.thy Sun Aug 21 21:18:59 2011 -0700
+++ b/src/HOL/NanoJava/Example.thy Mon Aug 22 10:57:33 2011 +0200
@@ -41,17 +41,18 @@
*}
-axioms This_neq_Par [simp]: "This \<noteq> Par"
- Res_neq_This [simp]: "Res \<noteq> This"
+axiomatization where
+ This_neq_Par [simp]: "This \<noteq> Par" and
+ Res_neq_This [simp]: "Res \<noteq> This"
subsection "Program representation"
-consts N :: cname ("Nat") (* with mixfix because of clash with NatDef.Nat *)
-consts pred :: fname
-consts suc :: mname
- add :: mname
-consts any :: vname
+axiomatization
+ N :: cname ("Nat") (* with mixfix because of clash with NatDef.Nat *)
+ and pred :: fname
+ and suc add :: mname
+ and any :: vname
abbreviation
dummy :: expr ("<>")
@@ -64,19 +65,19 @@
text {* The following properties could be derived from a more complete
program model, which we leave out for laziness. *}
-axioms Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)"
+axiomatization where Nat_no_subclasses [simp]: "D \<preceq>C Nat = (D=Nat)"
-axioms method_Nat_add [simp]: "method Nat add = Some
+axiomatization where method_Nat_add [simp]: "method Nat add = Some
\<lparr> par=Class Nat, res=Class Nat, lcl=[],
bdy= If((LAcc This..pred))
(Res :== {Nat}(LAcc This..pred)..add({Nat}LAcc Par..suc(<>)))
Else Res :== LAcc Par \<rparr>"
-axioms method_Nat_suc [simp]: "method Nat suc = Some
+axiomatization where method_Nat_suc [simp]: "method Nat suc = Some
\<lparr> par=NT, res=Class Nat, lcl=[],
bdy= Res :== new Nat;; LAcc Res..pred :== LAcc This \<rparr>"
-axioms field_Nat [simp]: "field Nat = empty(pred\<mapsto>Class Nat)"
+axiomatization where field_Nat [simp]: "field Nat = empty(pred\<mapsto>Class Nat)"
lemma init_locs_Nat_add [simp]: "init_locs Nat add s = s"
by (simp add: init_locs_def init_vars_def)
--- a/src/HOL/NanoJava/Term.thy Sun Aug 21 21:18:59 2011 -0700
+++ b/src/HOL/NanoJava/Term.thy Mon Aug 22 10:57:33 2011 +0200
@@ -11,14 +11,13 @@
typedecl fname --{* field name *}
typedecl vname --{* variable name *}
-consts
- This :: vname --{* This pointer *}
- Par :: vname --{* method parameter *}
+axiomatization
+ This --{* This pointer *}
+ Par --{* method parameter *}
Res :: vname --{* method result *}
-
-text {* Inequality axioms are not required for the meta theory. *}
+ -- {* Inequality axioms are not required for the meta theory. *}
(*
-axioms
+where
This_neq_Par [simp]: "This \<noteq> Par"
Par_neq_Res [simp]: "Par \<noteq> Res"
Res_neq_This [simp]: "Res \<noteq> This"
--- a/src/HOL/NanoJava/TypeRel.thy Sun Aug 21 21:18:59 2011 -0700
+++ b/src/HOL/NanoJava/TypeRel.thy Mon Aug 22 10:57:33 2011 +0200
@@ -6,8 +6,11 @@
theory TypeRel imports Decl "~~/src/HOL/Library/Wfrec" begin
-consts
- subcls1 :: "(cname \<times> cname) set" --{* subclass *}
+text{* Direct subclass relation *}
+
+definition subcls1 :: "(cname \<times> cname) set"
+where
+ "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
abbreviation
subcls1_syntax :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70)
@@ -20,17 +23,9 @@
subcls1_syntax ("_ \<prec>C1 _" [71,71] 70) and
subcls_syntax ("_ \<preceq>C _" [71,71] 70)
-consts
- method :: "cname => (mname \<rightharpoonup> methd)"
- field :: "cname => (fname \<rightharpoonup> ty)"
-
subsection "Declarations and properties not used in the meta theory"
-text{* Direct subclass relation *}
-defs
- subcls1_def: "subcls1 \<equiv> {(C,D). C\<noteq>Object \<and> (\<exists>c. class C = Some c \<and> super c=D)}"
-
text{* Widening, viz. method invocation conversion *}
inductive
widen :: "ty => ty => bool" ("_ \<preceq> _" [71,71] 70)
@@ -111,7 +106,8 @@
done
--{* Methods of a class, with inheritance and hiding *}
-defs method_def: "method C \<equiv> class_rec C methods"
+definition method :: "cname => (mname \<rightharpoonup> methd)" where
+ "method C \<equiv> class_rec C methods"
lemma method_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
method C = (if C=Object then empty else method (super m)) ++ map_of (methods m)"
@@ -122,7 +118,8 @@
--{* Fields of a class, with inheritance and hiding *}
-defs field_def: "field C \<equiv> class_rec C flds"
+definition field :: "cname => (fname \<rightharpoonup> ty)" where
+ "field C \<equiv> class_rec C flds"
lemma flds_rec: "\<lbrakk>class C = Some m; ws_prog\<rbrakk> \<Longrightarrow>
field C = (if C=Object then empty else field (super m)) ++ map_of (flds m)"
--- a/src/HOL/Subst/AList.thy Sun Aug 21 21:18:59 2011 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(* Title: HOL/Subst/AList.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-*)
-
-header {* Association Lists *}
-
-theory AList
-imports Main
-begin
-
-primrec alist_rec :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
-where
- "alist_rec [] c d = c"
-| "alist_rec (p # al) c d = d (fst p) (snd p) al (alist_rec al c d)"
-
-primrec assoc :: "['a,'b,('a*'b) list] => 'b"
-where
- "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 [] \<Longrightarrow> (!!x y xs. P xs \<Longrightarrow> P ((x,y) # xs)) \<Longrightarrow> P l"
- by (induct l) auto
-
-end
--- a/src/HOL/Subst/ROOT.ML Sun Aug 21 21:18:59 2011 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,26 +0,0 @@
-(* Title: HOL/Subst/ROOT.ML
- Authors: Martin Coen, Cambridge University Computer Laboratory
- Konrad Slind, TU Munich
- Copyright 1993 University of Cambridge,
- 1996 TU Munich
-
-Substitution and Unification in Higher-Order Logic.
-
-Implements Manna & Waldinger's formalization, with Paulson's simplifications,
-and some new simplifications by Slind.
-
-Z Manna & R Waldinger, Deductive Synthesis of the Unification Algorithm.
-SCP 1 (1981), 5-48
-
-L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5 (1985), 143-170
-
-AList - association lists
-UTerm - data type of terms
-Subst - substitutions
-Unifier - specification of unification and conditions for
- correctness and termination
-Unify - the unification function
-
-*)
-
-use_thys ["Unify"];
--- a/src/HOL/Subst/Subst.thy Sun Aug 21 21:18:59 2011 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,196 +0,0 @@
-(* Title: HOL/Subst/Subst.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-*)
-
-header {* Substitutions on uterms *}
-
-theory Subst
-imports AList UTerm
-begin
-
-primrec
- subst :: "'a uterm => ('a * 'a uterm) list => 'a uterm" (infixl "<|" 55)
-where
- 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)"
-
-notation (xsymbols)
- subst (infixl "\<lhd>" 55)
-
-definition
- subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr "=$=" 52)
- where "r =$= s \<longleftrightarrow> (\<forall>t. t \<lhd> r = t \<lhd> s)"
-
-notation (xsymbols)
- subst_eq (infixr "\<doteq>" 52)
-
-definition
- comp :: "('a * 'a uterm) list \<Rightarrow> ('a * 'a uterm) list \<Rightarrow> ('a* 'a uterm) list"
- (infixl "<>" 56)
- where "al <> bl = alist_rec al bl (%x y xs g. (x,y \<lhd> bl) # g)"
-
-notation (xsymbols)
- comp (infixl "\<lozenge>" 56)
-
-definition
- sdom :: "('a*('a uterm)) list => 'a set" where
- "sdom al = alist_rec al {} (%x y xs g. if Var(x)=y then g - {x} else g Un {x})"
-
-definition
- srange :: "('a*('a uterm)) list => 'a set" where
- "srange al = Union({y. \<exists>x \<in> sdom(al). y = vars_of(Var(x) \<lhd> al)})"
-
-
-
-subsection {* Basic Laws *}
-
-lemma subst_Nil [simp]: "t \<lhd> [] = t"
- by (induct t) auto
-
-lemma subst_mono: "t \<prec> u \<Longrightarrow> t \<lhd> s \<prec> u \<lhd> s"
- by (induct u) auto
-
-lemma Var_not_occs: "~ (Var(v) \<prec> t) \<Longrightarrow> t \<lhd> (v,t \<lhd> s) # s = t \<lhd> s"
- apply (case_tac "t = Var v")
- prefer 2
- apply (erule rev_mp)+
- apply (rule_tac P = "%x. x \<noteq> Var v \<longrightarrow> ~(Var v \<prec> x) \<longrightarrow> x \<lhd> (v,t\<lhd>s) #s = x\<lhd>s"
- in uterm.induct)
- apply auto
- done
-
-lemma agreement: "(t\<lhd>r = t\<lhd>s) = (\<forall>v \<in> vars_of t. Var v \<lhd> r = Var v \<lhd> s)"
- by (induct t) auto
-
-lemma repl_invariance: "~ v: vars_of t ==> t \<lhd> (v,u)#s = t \<lhd> s"
- by (simp add: agreement)
-
-lemma Var_in_subst:
- "v \<in> vars_of(t) --> w \<in> vars_of(t \<lhd> (v,Var(w))#s)"
- by (induct t) auto
-
-
-subsection{*Equality between Substitutions*}
-
-lemma subst_eq_iff: "r \<doteq> s = (\<forall>t. t \<lhd> r = t \<lhd> s)"
- by (simp add: subst_eq_def)
-
-lemma subst_refl [iff]: "r \<doteq> r"
- by (simp add: subst_eq_iff)
-
-lemma subst_sym: "r \<doteq> s ==> s \<doteq> r"
- by (simp add: subst_eq_iff)
-
-lemma subst_trans: "[| q \<doteq> r; r \<doteq> s |] ==> q \<doteq> s"
- by (simp add: subst_eq_iff)
-
-lemma subst_subst2:
- "[| r \<doteq> s; P (t \<lhd> r) (u \<lhd> r) |] ==> P (t \<lhd> s) (u \<lhd> s)"
- by (simp add: subst_eq_def)
-
-lemma ssubst_subst2:
- "[| s \<doteq> r; P (t \<lhd> r) (u \<lhd> r) |] ==> P (t \<lhd> s) (u \<lhd> s)"
- by (simp add: subst_eq_def)
-
-
-subsection{*Composition of Substitutions*}
-
-lemma [simp]:
- "[] \<lozenge> bl = bl"
- "((a,b)#al) \<lozenge> bl = (a,b \<lhd> bl) # (al \<lozenge> 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 \<lozenge> [] = s"
- by (induct s) auto
-
-lemma subst_comp_Nil: "s \<doteq> s \<lozenge> []"
- by simp
-
-lemma subst_comp [simp]: "(t \<lhd> r \<lozenge> s) = (t \<lhd> r \<lhd> s)"
- apply (induct t)
- apply simp_all
- apply (induct r)
- apply auto
- done
-
-lemma comp_assoc: "(q \<lozenge> r) \<lozenge> s \<doteq> q \<lozenge> (r \<lozenge> s)"
- by (simp add: subst_eq_iff)
-
-lemma subst_cong:
- "[| theta \<doteq> theta1; sigma \<doteq> sigma1|]
- ==> (theta \<lozenge> sigma) \<doteq> (theta1 \<lozenge> sigma1)"
- by (simp add: subst_eq_def)
-
-
-lemma Cons_trivial: "(w, Var(w) \<lhd> s) # s \<doteq> s"
- apply (simp add: subst_eq_iff)
- apply (rule allI)
- apply (induct_tac t)
- apply simp_all
- done
-
-
-lemma comp_subst_subst: "q \<lozenge> r \<doteq> s ==> t \<lhd> q \<lhd> r = t \<lhd> s"
- by (simp add: subst_eq_iff)
-
-
-subsection{*Domain and range of Substitutions*}
-
-lemma sdom_iff: "(v \<in> sdom(s)) = (Var(v) \<lhd> s ~= Var(v))"
- apply (induct s)
- apply (case_tac [2] a)
- apply auto
- done
-
-
-lemma srange_iff:
- "v \<in> srange(s) = (\<exists>w. w \<in> sdom(s) & v \<in> vars_of(Var(w) \<lhd> s))"
- by (auto simp add: srange_def)
-
-lemma empty_iff_all_not: "(A = {}) = (ALL a.~ a:A)"
- unfolding empty_def by blast
-
-lemma invariance: "(t \<lhd> s = t) = (sdom(s) Int vars_of(t) = {})"
- apply (induct t)
- apply (auto simp add: empty_iff_all_not sdom_iff)
- done
-
-lemma Var_in_srange:
- "v \<in> sdom(s) \<Longrightarrow> v \<in> vars_of(t \<lhd> s) \<Longrightarrow> v \<in> srange(s)"
- apply (induct t)
- apply (case_tac "a \<in> sdom s")
- apply (auto simp add: sdom_iff srange_iff)
- done
-
-lemma Var_elim: "[| v \<in> sdom(s); v \<notin> srange(s) |] ==> v \<notin> vars_of(t \<lhd> s)"
- by (blast intro: Var_in_srange)
-
-lemma Var_intro:
- "v \<in> vars_of(t \<lhd> s) \<Longrightarrow> v \<in> srange(s) | v \<in> vars_of(t)"
- apply (induct t)
- apply (auto simp add: sdom_iff srange_iff)
- apply (rule_tac x=a in exI)
- apply auto
- done
-
-lemma srangeD: "v \<in> srange(s) ==> \<exists>w. w \<in> sdom(s) & v \<in> vars_of(Var(w) \<lhd> s)"
- by (simp add: srange_iff)
-
-lemma dom_range_disjoint:
- "sdom(s) Int srange(s) = {} = (\<forall>t. sdom(s) Int vars_of(t \<lhd> s) = {})"
- apply (simp add: empty_iff_all_not)
- apply (force intro: Var_in_srange dest: srangeD)
- done
-
-lemma subst_not_empty: "~ u \<lhd> s = u ==> (\<exists>x. x \<in> sdom(s))"
- by (auto simp add: empty_iff_all_not invariance)
-
-
-lemma id_subst_lemma [simp]: "(M \<lhd> [(x, Var x)]) = M"
- by (induct M) auto
-
-end
--- a/src/HOL/Subst/UTerm.thy Sun Aug 21 21:18:59 2011 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(* Title: HOL/Subst/UTerm.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-*)
-
-header {* Simple Term Structure for Unification *}
-
-theory UTerm
-imports Main
-begin
-
-text {* Binary trees with leaves that are constants or variables. *}
-
-datatype 'a uterm =
- Var 'a
- | Const 'a
- | Comb "'a uterm" "'a uterm"
-
-primrec vars_of :: "'a uterm => 'a set"
-where
- 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 occs :: "'a uterm => 'a uterm => bool" (infixl "<:" 54)
-where
- 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)"
-
-notation (xsymbols)
- occs (infixl "\<prec>" 54)
-
-primrec uterm_size :: "'a uterm => nat"
-where
- 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 \<in> vars_of (Var w)) = (w = v)"
- by auto
-
-lemma vars_iff_occseq: "(x \<in> vars_of t) = (Var x \<prec> t | Var x = t)"
- by (induct t) auto
-
-
-text{* Not used, but perhaps useful in other proofs *}
-lemma occs_vars_subset: "M \<prec> N \<Longrightarrow> vars_of M \<subseteq> vars_of N"
- by (induct N) auto
-
-
-lemma monotone_vars_of:
- "vars_of M Un vars_of N \<subseteq> (vars_of M Un A) Un (vars_of N Un B)"
- by blast
-
-lemma finite_vars_of: "finite (vars_of M)"
- by (induct M) auto
-
-end
--- a/src/HOL/Subst/Unifier.thy Sun Aug 21 21:18:59 2011 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-(* Title: HOL/Subst/Unifier.thy
- Author: Martin Coen, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-*)
-
-header {* Definition of Most General Unifier *}
-
-theory Unifier
-imports Subst
-begin
-
-definition
- Unifier :: "('a * 'a uterm) list \<Rightarrow> 'a uterm \<Rightarrow> 'a uterm \<Rightarrow> bool"
- where "Unifier s t u \<longleftrightarrow> t <| s = u <| s"
-
-definition
- MoreGeneral :: "('a * 'a uterm) list \<Rightarrow> ('a * 'a uterm) list \<Rightarrow> bool" (infixr ">>" 52)
- where "r >> s \<longleftrightarrow> (\<exists>q. s =$= r <> q)"
-
-definition
- MGUnifier :: "('a * 'a uterm) list \<Rightarrow> 'a uterm \<Rightarrow> 'a uterm \<Rightarrow> bool"
- where "MGUnifier s t u \<longleftrightarrow> Unifier s t u & (\<forall>r. Unifier r t u --> s >> r)"
-
-definition
- Idem :: "('a * 'a uterm)list => bool" where
- "Idem s \<longleftrightarrow> (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 \<notin> vars_of t \<Longrightarrow> v \<notin> vars_of u \<Longrightarrow> Unifier s t u \<Longrightarrow> 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 [intro!]: "~ 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
-
-
-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) \<Longrightarrow> Unifier s (t<|r) (u<|r) \<Longrightarrow>
- Unifier (r <> s) (t <| r) (u <| r)"
- by (simp add: Idem_def Unifier_def comp_subst_subst)
-
-lemma Idem_comp:
- "Idem r \<Longrightarrow> Unifier s (t <| r) (u <| r) \<Longrightarrow>
- (!!q. Unifier q (t <| r) (u <| r) \<Longrightarrow> s <> q =$= q) \<Longrightarrow>
- Idem (r <> s)"
- apply (frule Unifier_Idem_subst, blast)
- apply (force simp add: Idem_def subst_eq_iff)
- done
-
-end
--- a/src/HOL/Subst/Unify.thy Sun Aug 21 21:18:59 2011 -0700
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,235 +0,0 @@
-(* Title: HOL/Subst/Unify.thy
- Author: Konrad Slind, Cambridge University Computer Laboratory
- Copyright 1997 University of Cambridge
-*)
-
-header {* Unification Algorithm *}
-
-theory Unify
-imports Unifier "~~/src/HOL/Library/Old_Recdef"
-begin
-
-subsection {* Substitution and Unification in Higher-Order Logic. *}
-
-text {*
-NB: This theory is already quite old.
-You might want to look at the newer Isar formalization of
-unification in HOL/ex/Unification.thy.
-
-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
-*}
-
-definition
- unifyRel :: "(('a uterm * 'a uterm) * ('a uterm * 'a uterm)) set" where
- "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) *}
-
-
-text{* Wellfoundedness of unifyRel *}
-lemma wf_unifyRel [iff]: "wf unifyRel"
- by (simp add: unifyRel_def wf_lex_prod wf_finite_psubset)
-
-consts unify :: "'a uterm * 'a uterm => ('a * 'a uterm) list option"
-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 \<prec> 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 \<prec> 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 \<lhd> theta, N2 \<lhd> theta)
- of None => None
- | Some sigma => Some (theta \<lozenge> sigma)))"
- (hints recdef_wf: wf_unifyRel)
-
-
-text{* 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).*}
-recdef_tc unify_tc1: unify (1)
- by (auto simp: unifyRel_def finite_psubset_def finite_vars_of)
-
-
-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))) \<in> unifyRel ==>
- ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) \<in> unifyRel"
- by (simp add: less_eq 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 \<prec> M) ==>
- ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb M N1, Comb(Var x) N2)) \<in> unifyRel
- & ((N1 \<lhd> [(x,M)], N2 \<lhd> [(x,M)]), (Comb(Var x) N1, Comb M N2)) \<in> unifyRel"
-apply (case_tac "Var x = M", clarify, simp)
-apply (case_tac "x \<in> (vars_of N1 Un vars_of N2)")
-txt{*@{text uterm_less} case*}
-apply (simp add: less_eq unifyRel_def lex_prod_def)
-apply blast
-txt{*@{text finite_psubset} case*}
-apply (simp add: unifyRel_def lex_prod_def)
-apply (simp add: finite_psubset_def finite_vars_of psubset_eq)
-apply blast
-txt{*Final case, also @{text finite_psubset}*}
-apply (simp add: finite_vars_of unifyRel_def finite_psubset_def lex_prod_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. The (2) requests the second one.
- Proved by recursion induction.*}
-recdef_tc unify_tc2: unify (2)
-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 "\<forall>M1 M2 theta. unify (M1, M2) = Some theta -->
- (\<forall>N1 N2.((N1\<lhd>theta, N2\<lhd>theta), (Comb M1 N1, Comb M2 N2)) \<in> 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 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 \<lhd> theta, N2 \<lhd> theta)
- of None => None
- | Some sigma => Some (theta \<lozenge> sigma)))"
-by (simp add: unify_tc2 unify_simps0 split add: option.split)
-
-lemma unify_induct:
- "(\<And>m n. P (Const m) (Const n)) \<Longrightarrow>
- (\<And>m M N. P (Const m) (Comb M N)) \<Longrightarrow>
- (\<And>m v. P (Const m) (Var v)) \<Longrightarrow>
- (\<And>v M. P (Var v) M) \<Longrightarrow>
- (\<And>M N x. P (Comb M N) (Const x)) \<Longrightarrow>
- (\<And>M N v. P (Comb M N) (Var v)) \<Longrightarrow>
- (\<And>M1 N1 M2 N2.
- \<forall>theta. unify (M1, M2) = Some theta \<longrightarrow> P (N1 \<lhd> theta) (N2 \<lhd> theta) \<Longrightarrow>
- P M1 M2 \<Longrightarrow> P (Comb M1 N1) (Comb M2 N2)) \<Longrightarrow>
- P u v"
-by (rule unify_induct0) (simp_all add: unify_tc2)
-
-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]:
- "\<forall>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))
- txt{*Const-Const case*}
- apply (simp add: MGUnifier_def Unifier_def)
- txt{*Const-Var case*}
- apply (subst mgu_sym)
- apply (simp add: MGUnifier_Var)
- txt{*Var-M case*}
- apply (simp add: MGUnifier_Var)
- txt{*Comb-Var case*}
- apply (subst mgu_sym)
- apply (simp add: MGUnifier_Var)
-txt{*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 \<lhd> theta \<lhd> delta = N2 \<lhd> theta \<lhd> 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]:
- "\<forall>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
--- a/src/HOL/ex/Unification.thy Sun Aug 21 21:18:59 2011 -0700
+++ b/src/HOL/ex/Unification.thy Mon Aug 22 10:57:33 2011 +0200
@@ -1,123 +1,159 @@
-(*
- Author: Alexander Krauss, Technische Universitaet Muenchen
+(* Title: HOL/ex/Unification.thy
+ Author: Martin Coen, Cambridge University Computer Laboratory
+ Author: Konrad Slind, TUM & Cambridge University Computer Laboratory
+ Author: Alexander Krauss, TUM
*)
-header {* Case study: Unification Algorithm *}
+header {* Substitution and Unification *}
theory Unification
imports Main
begin
text {*
- This is a formalization of a first-order unification
- algorithm. It uses the new "function" package to define recursive
- functions, which allows a better treatment of nested recursion.
+ Implements Manna & Waldinger's formalization, with Paulson's
+ simplifications, and some new simplifications by Slind and Krauss.
+
+ Z Manna & R Waldinger, Deductive Synthesis of the Unification
+ Algorithm. SCP 1 (1981), 5-48
- This is basically a modernized version of a previous formalization
- by Konrad Slind (see: HOL/Subst/Unify.thy), which itself builds on
- previous work by Paulson and Manna \& Waldinger (for details, see
- there).
+ L C Paulson, Verifying the Unification Algorithm in LCF. SCP 5
+ (1985), 143-170
- Unlike that formalization, where the proofs of termination and
- some partial correctness properties are intertwined, we can prove
- partial correctness and termination separately.
+ K Slind, Reasoning about Terminating Functional Programs,
+ Ph.D. thesis, TUM, 1999, Sect. 5.8
+
+ A Krauss, Partial and Nested Recursive Function Definitions in
+ Higher-Order Logic, JAR 44(4):303–336, 2010. Sect. 6.3
*}
-subsection {* Basic definitions *}
+subsection {* Terms *}
+
+text {* Binary trees with leaves that are constants or variables. *}
datatype 'a trm =
Var 'a
| Const 'a
- | App "'a trm" "'a trm" (infix "\<cdot>" 60)
+ | Comb "'a trm" "'a trm" (infix "\<cdot>" 60)
+
+primrec vars_of :: "'a trm \<Rightarrow> 'a set"
+where
+ "vars_of (Var v) = {v}"
+| "vars_of (Const c) = {}"
+| "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
+
+fun occs :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" (infixl "\<prec>" 54)
+where
+ "u \<prec> Var v \<longleftrightarrow> False"
+| "u \<prec> Const c \<longleftrightarrow> False"
+| "u \<prec> M \<cdot> N \<longleftrightarrow> u = M \<or> u = N \<or> u \<prec> M \<or> u \<prec> N"
+
+
+lemma finite_vars_of[intro]: "finite (vars_of t)"
+ by (induct t) simp_all
+
+lemma vars_iff_occseq: "x \<in> vars_of t \<longleftrightarrow> Var x \<prec> t \<or> Var x = t"
+ by (induct t) auto
+
+lemma occs_vars_subset: "M \<prec> N \<Longrightarrow> vars_of M \<subseteq> vars_of N"
+ by (induct N) auto
+
+
+subsection {* Substitutions *}
type_synonym 'a subst = "('a \<times> 'a trm) list"
-text {* Applying a substitution to a variable: *}
-
fun assoc :: "'a \<Rightarrow> 'b \<Rightarrow> ('a \<times> 'b) list \<Rightarrow> 'b"
where
"assoc x d [] = d"
| "assoc x d ((p,q)#t) = (if x = p then q else assoc x d t)"
-text {* Applying a substitution to a term: *}
-
-fun apply_subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<triangleleft>" 60)
+primrec subst :: "'a trm \<Rightarrow> 'a subst \<Rightarrow> 'a trm" (infixl "\<lhd>" 55)
where
- "(Var v) \<triangleleft> s = assoc v (Var v) s"
-| "(Const c) \<triangleleft> s = (Const c)"
-| "(M \<cdot> N) \<triangleleft> s = (M \<triangleleft> s) \<cdot> (N \<triangleleft> s)"
+ "(Var v) \<lhd> s = assoc v (Var v) s"
+| "(Const c) \<lhd> s = (Const c)"
+| "(M \<cdot> N) \<lhd> s = (M \<lhd> s) \<cdot> (N \<lhd> s)"
-text {* Composition of substitutions: *}
-
-fun
- "compose" :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<bullet>" 80)
+definition subst_eq (infixr "\<doteq>" 52)
where
- "[] \<bullet> bl = bl"
-| "((a,b) # al) \<bullet> bl = (a, b \<triangleleft> bl) # (al \<bullet> bl)"
+ "s1 \<doteq> s2 \<longleftrightarrow> (\<forall>t. t \<lhd> s1 = t \<lhd> s2)"
-text {* Equivalence of substitutions: *}
-
-definition eqv (infix "=\<^sub>s" 50)
+fun comp :: "'a subst \<Rightarrow> 'a subst \<Rightarrow> 'a subst" (infixl "\<lozenge>" 56)
where
- "s1 =\<^sub>s s2 \<equiv> \<forall>t. t \<triangleleft> s1 = t \<triangleleft> s2"
-
+ "[] \<lozenge> bl = bl"
+| "((a,b) # al) \<lozenge> bl = (a, b \<lhd> bl) # (al \<lozenge> bl)"
-subsection {* Basic lemmas *}
-
-lemma apply_empty[simp]: "t \<triangleleft> [] = t"
+lemma subst_Nil[simp]: "t \<lhd> [] = t"
by (induct t) auto
-lemma compose_empty[simp]: "\<sigma> \<bullet> [] = \<sigma>"
+lemma subst_mono: "t \<prec> u \<Longrightarrow> t \<lhd> s \<prec> u \<lhd> s"
+by (induct u) auto
+
+lemma agreement: "(t \<lhd> r = t \<lhd> s) \<longleftrightarrow> (\<forall>v \<in> vars_of t. Var v \<lhd> r = Var v \<lhd> s)"
+by (induct t) auto
+
+lemma repl_invariance: "v \<notin> vars_of t \<Longrightarrow> t \<lhd> (v,u) # s = t \<lhd> s"
+by (simp add: agreement)
+
+lemma remove_var: "v \<notin> vars_of s \<Longrightarrow> v \<notin> vars_of (t \<lhd> [(v, s)])"
+by (induct t) simp_all
+
+lemma subst_refl[iff]: "s \<doteq> s"
+ by (auto simp:subst_eq_def)
+
+lemma subst_sym[sym]: "\<lbrakk>s1 \<doteq> s2\<rbrakk> \<Longrightarrow> s2 \<doteq> s1"
+ by (auto simp:subst_eq_def)
+
+lemma subst_trans[trans]: "\<lbrakk>s1 \<doteq> s2; s2 \<doteq> s3\<rbrakk> \<Longrightarrow> s1 \<doteq> s3"
+ by (auto simp:subst_eq_def)
+
+lemma subst_no_occs: "\<not> Var v \<prec> t \<Longrightarrow> Var v \<noteq> t
+ \<Longrightarrow> t \<lhd> [(v,s)] = t"
+by (induct t) auto
+
+lemma comp_Nil[simp]: "\<sigma> \<lozenge> [] = \<sigma>"
by (induct \<sigma>) auto
-lemma apply_compose[simp]: "t \<triangleleft> (s1 \<bullet> s2) = t \<triangleleft> s1 \<triangleleft> s2"
+lemma subst_comp[simp]: "t \<lhd> (r \<lozenge> s) = t \<lhd> r \<lhd> s"
proof (induct t)
- case App thus ?case by simp
-next
- case Const thus ?case by simp
-next
case (Var v) thus ?case
- proof (induct s1)
- case Nil show ?case by simp
- next
- case (Cons p s1s) thus ?case by (cases p, simp)
- qed
+ by (induct r) auto
+qed auto
+
+lemma subst_eq_intro[intro]: "(\<And>t. t \<lhd> \<sigma> = t \<lhd> \<theta>) \<Longrightarrow> \<sigma> \<doteq> \<theta>"
+ by (auto simp:subst_eq_def)
+
+lemma subst_eq_dest[dest]: "s1 \<doteq> s2 \<Longrightarrow> t \<lhd> s1 = t \<lhd> s2"
+ by (auto simp:subst_eq_def)
+
+lemma comp_assoc: "(a \<lozenge> b) \<lozenge> c \<doteq> a \<lozenge> (b \<lozenge> c)"
+ by auto
+
+lemma subst_cong: "\<lbrakk>\<sigma> \<doteq> \<sigma>'; \<theta> \<doteq> \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<lozenge> \<theta>) \<doteq> (\<sigma>' \<lozenge> \<theta>')"
+ by (auto simp: subst_eq_def)
+
+lemma var_self: "[(v, Var v)] \<doteq> []"
+proof
+ fix t show "t \<lhd> [(v, Var v)] = t \<lhd> []"
+ by (induct t) simp_all
qed
-lemma eqv_refl[intro]: "s =\<^sub>s s"
- by (auto simp:eqv_def)
-
-lemma eqv_trans[trans]: "\<lbrakk>s1 =\<^sub>s s2; s2 =\<^sub>s s3\<rbrakk> \<Longrightarrow> s1 =\<^sub>s s3"
- by (auto simp:eqv_def)
-
-lemma eqv_sym[sym]: "\<lbrakk>s1 =\<^sub>s s2\<rbrakk> \<Longrightarrow> s2 =\<^sub>s s1"
- by (auto simp:eqv_def)
-
-lemma eqv_intro[intro]: "(\<And>t. t \<triangleleft> \<sigma> = t \<triangleleft> \<theta>) \<Longrightarrow> \<sigma> =\<^sub>s \<theta>"
- by (auto simp:eqv_def)
-
-lemma eqv_dest[dest]: "s1 =\<^sub>s s2 \<Longrightarrow> t \<triangleleft> s1 = t \<triangleleft> s2"
- by (auto simp:eqv_def)
-
-lemma compose_eqv: "\<lbrakk>\<sigma> =\<^sub>s \<sigma>'; \<theta> =\<^sub>s \<theta>'\<rbrakk> \<Longrightarrow> (\<sigma> \<bullet> \<theta>) =\<^sub>s (\<sigma>' \<bullet> \<theta>')"
- by (auto simp:eqv_def)
-
-lemma compose_assoc: "(a \<bullet> b) \<bullet> c =\<^sub>s a \<bullet> (b \<bullet> c)"
- by auto
+lemma var_same[simp]: "[(v, t)] \<doteq> [] \<longleftrightarrow> t = Var v"
+by (metis assoc.simps(2) subst.simps(1) subst_eq_def var_self)
-subsection {* Specification: Most general unifiers *}
+subsection {* Unifiers and Most General Unifiers *}
-definition
- "Unifier \<sigma> t u \<equiv> (t\<triangleleft>\<sigma> = u\<triangleleft>\<sigma>)"
+definition Unifier :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
+where "Unifier \<sigma> t u \<longleftrightarrow> (t \<lhd> \<sigma> = u \<lhd> \<sigma>)"
-definition
- "MGU \<sigma> t u \<equiv> Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u
- \<longrightarrow> (\<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>))"
+definition MGU :: "'a subst \<Rightarrow> 'a trm \<Rightarrow> 'a trm \<Rightarrow> bool" where
+ "MGU \<sigma> t u \<longleftrightarrow>
+ Unifier \<sigma> t u \<and> (\<forall>\<theta>. Unifier \<theta> t u \<longrightarrow> (\<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>))"
lemma MGUI[intro]:
- "\<lbrakk>t \<triangleleft> \<sigma> = u \<triangleleft> \<sigma>; \<And>\<theta>. t \<triangleleft> \<theta> = u \<triangleleft> \<theta> \<Longrightarrow> \<exists>\<gamma>. \<theta> =\<^sub>s \<sigma> \<bullet> \<gamma>\<rbrakk>
+ "\<lbrakk>t \<lhd> \<sigma> = u \<lhd> \<sigma>; \<And>\<theta>. t \<lhd> \<theta> = u \<lhd> \<theta> \<Longrightarrow> \<exists>\<gamma>. \<theta> \<doteq> \<sigma> \<lozenge> \<gamma>\<rbrakk>
\<Longrightarrow> MGU \<sigma> t u"
by (simp only:Unifier_def MGU_def, auto)
@@ -125,236 +161,77 @@
"MGU \<sigma> s t \<Longrightarrow> MGU \<sigma> t s"
by (auto simp:MGU_def Unifier_def)
+lemma MGU_is_Unifier: "MGU \<sigma> t u \<Longrightarrow> Unifier \<sigma> t u"
+unfolding MGU_def by (rule conjunct1)
+
+lemma MGU_Var:
+ assumes "\<not> Var v \<prec> t"
+ shows "MGU [(v,t)] (Var v) t"
+proof (intro MGUI exI)
+ show "Var v \<lhd> [(v,t)] = t \<lhd> [(v,t)]" using assms
+ by (metis assoc.simps(2) repl_invariance subst.simps(1) subst_Nil vars_iff_occseq)
+next
+ fix \<theta> assume th: "Var v \<lhd> \<theta> = t \<lhd> \<theta>"
+ show "\<theta> \<doteq> [(v,t)] \<lozenge> \<theta>"
+ proof
+ fix s show "s \<lhd> \<theta> = s \<lhd> [(v,t)] \<lozenge> \<theta>" using th
+ by (induct s) auto
+ qed
+qed
+
+lemma MGU_Const: "MGU [] (Const c) (Const d) \<longleftrightarrow> c = d"
+ by (auto simp: MGU_def Unifier_def)
+
subsection {* The unification algorithm *}
-text {* Occurs check: Proper subterm relation *}
-
-fun occ :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> bool"
-where
- "occ u (Var v) = False"
-| "occ u (Const c) = False"
-| "occ u (M \<cdot> N) = (u = M \<or> u = N \<or> occ u M \<or> occ u N)"
-
-text {* The unification algorithm: *}
-
function unify :: "'a trm \<Rightarrow> 'a trm \<Rightarrow> 'a subst option"
where
"unify (Const c) (M \<cdot> N) = None"
| "unify (M \<cdot> N) (Const c) = None"
| "unify (Const c) (Var v) = Some [(v, Const c)]"
-| "unify (M \<cdot> N) (Var v) = (if (occ (Var v) (M \<cdot> N))
+| "unify (M \<cdot> N) (Var v) = (if Var v \<prec> M \<cdot> N
then None
else Some [(v, M \<cdot> N)])"
-| "unify (Var v) M = (if (occ (Var v) M)
+| "unify (Var v) M = (if Var v \<prec> M
then None
else Some [(v, M)])"
| "unify (Const c) (Const d) = (if c=d then Some [] else None)"
| "unify (M \<cdot> N) (M' \<cdot> N') = (case unify M M' of
None \<Rightarrow> None |
- Some \<theta> \<Rightarrow> (case unify (N \<triangleleft> \<theta>) (N' \<triangleleft> \<theta>)
+ Some \<theta> \<Rightarrow> (case unify (N \<lhd> \<theta>) (N' \<lhd> \<theta>)
of None \<Rightarrow> None |
- Some \<sigma> \<Rightarrow> Some (\<theta> \<bullet> \<sigma>)))"
+ Some \<sigma> \<Rightarrow> Some (\<theta> \<lozenge> \<sigma>)))"
by pat_completeness auto
-declare unify.psimps[simp]
-
-subsection {* Partial correctness *}
-
-text {* Some lemmas about occ and MGU: *}
-
-lemma subst_no_occ: "\<not>occ (Var v) t \<Longrightarrow> Var v \<noteq> t
- \<Longrightarrow> t \<triangleleft> [(v,s)] = t"
-by (induct t) auto
-
-lemma MGU_Var[intro]:
- assumes no_occ: "\<not>occ (Var v) t"
- shows "MGU [(v,t)] (Var v) t"
-proof (intro MGUI exI)
- show "Var v \<triangleleft> [(v,t)] = t \<triangleleft> [(v,t)]" using no_occ
- by (cases "Var v = t", auto simp:subst_no_occ)
-next
- fix \<theta> assume th: "Var v \<triangleleft> \<theta> = t \<triangleleft> \<theta>"
- show "\<theta> =\<^sub>s [(v,t)] \<bullet> \<theta>"
- proof
- fix s show "s \<triangleleft> \<theta> = s \<triangleleft> [(v,t)] \<bullet> \<theta>" using th
- by (induct s) auto
- qed
-qed
-
-declare MGU_Var[symmetric, intro]
-
-lemma MGU_Const[simp]: "MGU [] (Const c) (Const d) = (c = d)"
- unfolding MGU_def Unifier_def
- by auto
-
-text {* If unification terminates, then it computes most general unifiers: *}
-
-lemma unify_partial_correctness:
- assumes "unify_dom (M, N)"
- assumes "unify M N = Some \<sigma>"
- shows "MGU \<sigma> M N"
-using assms
-proof (induct M N arbitrary: \<sigma>)
- case (7 M N M' N' \<sigma>) -- "The interesting case"
-
- then obtain \<theta>1 \<theta>2
- where "unify M M' = Some \<theta>1"
- and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
- and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
- and MGU_inner: "MGU \<theta>1 M M'"
- and MGU_outer: "MGU \<theta>2 (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1)"
- by (auto split:option.split_asm)
-
- show ?case
- proof
- from MGU_inner and MGU_outer
- have "M \<triangleleft> \<theta>1 = M' \<triangleleft> \<theta>1"
- and "N \<triangleleft> \<theta>1 \<triangleleft> \<theta>2 = N' \<triangleleft> \<theta>1 \<triangleleft> \<theta>2"
- unfolding MGU_def Unifier_def
- by auto
- thus "M \<cdot> N \<triangleleft> \<sigma> = M' \<cdot> N' \<triangleleft> \<sigma>" unfolding \<sigma>
- by simp
- next
- fix \<sigma>' assume "M \<cdot> N \<triangleleft> \<sigma>' = M' \<cdot> N' \<triangleleft> \<sigma>'"
- hence "M \<triangleleft> \<sigma>' = M' \<triangleleft> \<sigma>'"
- and Ns: "N \<triangleleft> \<sigma>' = N' \<triangleleft> \<sigma>'" by auto
-
- with MGU_inner obtain \<delta>
- where eqv: "\<sigma>' =\<^sub>s \<theta>1 \<bullet> \<delta>"
- unfolding MGU_def Unifier_def
- by auto
-
- from Ns have "N \<triangleleft> \<theta>1 \<triangleleft> \<delta> = N' \<triangleleft> \<theta>1 \<triangleleft> \<delta>"
- by (simp add:eqv_dest[OF eqv])
-
- with MGU_outer obtain \<rho>
- where eqv2: "\<delta> =\<^sub>s \<theta>2 \<bullet> \<rho>"
- unfolding MGU_def Unifier_def
- by auto
-
- have "\<sigma>' =\<^sub>s \<sigma> \<bullet> \<rho>" unfolding \<sigma>
- by (rule eqv_intro, auto simp:eqv_dest[OF eqv] eqv_dest[OF eqv2])
- thus "\<exists>\<gamma>. \<sigma>' =\<^sub>s \<sigma> \<bullet> \<gamma>" ..
- qed
-qed (auto split:split_if_asm) -- "Solve the remaining cases automatically"
-
-
subsection {* Properties used in termination proof *}
-text {* The variables of a term: *}
-
-fun vars_of:: "'a trm \<Rightarrow> 'a set"
-where
- "vars_of (Var v) = { v }"
-| "vars_of (Const c) = {}"
-| "vars_of (M \<cdot> N) = vars_of M \<union> vars_of N"
-
-lemma vars_of_finite[intro]: "finite (vars_of t)"
- by (induct t) simp_all
-
text {* Elimination of variables by a substitution: *}
definition
- "elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)"
+ "elim \<sigma> v \<equiv> \<forall>t. v \<notin> vars_of (t \<lhd> \<sigma>)"
-lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<triangleleft> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
+lemma elim_intro[intro]: "(\<And>t. v \<notin> vars_of (t \<lhd> \<sigma>)) \<Longrightarrow> elim \<sigma> v"
by (auto simp:elim_def)
-lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<triangleleft> \<sigma>)"
+lemma elim_dest[dest]: "elim \<sigma> v \<Longrightarrow> v \<notin> vars_of (t \<lhd> \<sigma>)"
by (auto simp:elim_def)
-lemma elim_eqv: "\<sigma> =\<^sub>s \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
- by (auto simp:elim_def eqv_def)
-
-
-text {* Replacing a variable by itself yields an identity subtitution: *}
-
-lemma var_self[intro]: "[(v, Var v)] =\<^sub>s []"
-proof
- fix t show "t \<triangleleft> [(v, Var v)] = t \<triangleleft> []"
- by (induct t) simp_all
-qed
-
-lemma var_same: "([(v, t)] =\<^sub>s []) = (t = Var v)"
-proof
- assume t_v: "t = Var v"
- thus "[(v, t)] =\<^sub>s []"
- by auto
-next
- assume id: "[(v, t)] =\<^sub>s []"
- show "t = Var v"
- proof -
- have "t = Var v \<triangleleft> [(v, t)]" by simp
- also from id have "\<dots> = Var v \<triangleleft> []" ..
- finally show ?thesis by simp
- qed
-qed
-
-text {* A lemma about occ and elim *}
-
-lemma remove_var:
- assumes [simp]: "v \<notin> vars_of s"
- shows "v \<notin> vars_of (t \<triangleleft> [(v, s)])"
- by (induct t) simp_all
+lemma elim_eq: "\<sigma> \<doteq> \<theta> \<Longrightarrow> elim \<sigma> x = elim \<theta> x"
+ by (auto simp:elim_def subst_eq_def)
-lemma occ_elim: "\<not>occ (Var v) t
- \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] =\<^sub>s []"
-proof (induct t)
- case (Var x)
- show ?case
- proof cases
- assume "v = x"
- thus ?thesis
- by (simp add:var_same)
- next
- assume neq: "v \<noteq> x"
- have "elim [(v, Var x)] v"
- by (auto intro!:remove_var simp:neq)
- thus ?thesis ..
- qed
-next
- case (Const c)
- have "elim [(v, Const c)] v"
- by (auto intro!:remove_var)
- thus ?case ..
-next
- case (App M N)
-
- hence ih1: "elim [(v, M)] v \<or> [(v, M)] =\<^sub>s []"
- and ih2: "elim [(v, N)] v \<or> [(v, N)] =\<^sub>s []"
- and nonocc: "Var v \<noteq> M" "Var v \<noteq> N"
- by auto
-
- from nonocc have "\<not> [(v,M)] =\<^sub>s []"
- by (simp add:var_same)
- with ih1 have "elim [(v, M)] v" by blast
- hence "v \<notin> vars_of (Var v \<triangleleft> [(v,M)])" ..
- hence not_in_M: "v \<notin> vars_of M" by simp
-
- from nonocc have "\<not> [(v,N)] =\<^sub>s []"
- by (simp add:var_same)
- with ih2 have "elim [(v, N)] v" by blast
- hence "v \<notin> vars_of (Var v \<triangleleft> [(v,N)])" ..
- hence not_in_N: "v \<notin> vars_of N" by simp
-
- have "elim [(v, M \<cdot> N)] v"
- proof
- fix t
- show "v \<notin> vars_of (t \<triangleleft> [(v, M \<cdot> N)])"
- proof (induct t)
- case (Var x) thus ?case by (simp add: not_in_M not_in_N)
- qed auto
- qed
- thus ?case ..
-qed
+lemma occs_elim: "\<not> Var v \<prec> t
+ \<Longrightarrow> elim [(v,t)] v \<or> [(v,t)] \<doteq> []"
+by (metis elim_intro remove_var var_same vars_iff_occseq)
text {* The result of a unification never introduces new variables: *}
+declare unify.psimps[simp]
+
lemma unify_vars:
assumes "unify_dom (M, N)"
assumes "unify M N = Some \<sigma>"
- shows "vars_of (t \<triangleleft> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
+ shows "vars_of (t \<lhd> \<sigma>) \<subseteq> vars_of M \<union> vars_of N \<union> vars_of t"
(is "?P M N \<sigma> t")
using assms
proof (induct M N arbitrary:\<sigma> t)
@@ -363,45 +240,45 @@
thus ?case by (induct t) auto
next
case (4 M N v)
- hence "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
+ hence "\<not> Var v \<prec> M \<cdot> N" by auto
with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
thus ?case by (induct t) auto
next
case (5 v M)
- hence "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
+ hence "\<not> Var v \<prec> M" by auto
with 5 have "\<sigma> = [(v, M)]" by simp
thus ?case by (induct t) auto
next
case (7 M N M' N' \<sigma>)
then obtain \<theta>1 \<theta>2
where "unify M M' = Some \<theta>1"
- and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
- and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
+ and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
+ and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
and ih1: "\<And>t. ?P M M' \<theta>1 t"
- and ih2: "\<And>t. ?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2 t"
+ and ih2: "\<And>t. ?P (N\<lhd>\<theta>1) (N'\<lhd>\<theta>1) \<theta>2 t"
by (auto split:option.split_asm)
show ?case
proof
- fix v assume a: "v \<in> vars_of (t \<triangleleft> \<sigma>)"
+ fix v assume a: "v \<in> vars_of (t \<lhd> \<sigma>)"
show "v \<in> vars_of (M \<cdot> N) \<union> vars_of (M' \<cdot> N') \<union> vars_of t"
proof (cases "v \<notin> vars_of M \<and> v \<notin> vars_of M'
\<and> v \<notin> vars_of N \<and> v \<notin> vars_of N'")
case True
- with ih1 have l:"\<And>t. v \<in> vars_of (t \<triangleleft> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
+ with ih1 have l:"\<And>t. v \<in> vars_of (t \<lhd> \<theta>1) \<Longrightarrow> v \<in> vars_of t"
by auto
- from a and ih2[where t="t \<triangleleft> \<theta>1"]
- have "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)
- \<or> v \<in> vars_of (t \<triangleleft> \<theta>1)" unfolding \<sigma>
+ from a and ih2[where t="t \<lhd> \<theta>1"]
+ have "v \<in> vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1)
+ \<or> v \<in> vars_of (t \<lhd> \<theta>1)" unfolding \<sigma>
by auto
hence "v \<in> vars_of t"
proof
- assume "v \<in> vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
+ assume "v \<in> vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1)"
with True show ?thesis by (auto dest:l)
next
- assume "v \<in> vars_of (t \<triangleleft> \<theta>1)"
+ assume "v \<in> vars_of (t \<lhd> \<theta>1)"
thus ?thesis by (rule l)
qed
@@ -417,7 +294,7 @@
lemma unify_eliminates:
assumes "unify_dom (M, N)"
assumes "unify M N = Some \<sigma>"
- shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> =\<^sub>s []"
+ shows "(\<exists>v\<in>vars_of M \<union> vars_of N. elim \<sigma> v) \<or> \<sigma> \<doteq> []"
(is "?P M N \<sigma>")
using assms
proof (induct M N arbitrary:\<sigma>)
@@ -426,21 +303,21 @@
case 2 thus ?case by simp
next
case (3 c v)
- have no_occ: "\<not> occ (Var v) (Const c)" by simp
+ have no_occs: "\<not> Var v \<prec> Const c" by simp
with 3 have "\<sigma> = [(v, Const c)]" by simp
- with occ_elim[OF no_occ]
+ with occs_elim[OF no_occs]
show ?case by auto
next
case (4 M N v)
- hence no_occ: "\<not>occ (Var v) (M\<cdot>N)" by (cases "occ (Var v) (M\<cdot>N)", auto)
+ hence no_occs: "\<not> Var v \<prec> M \<cdot> N" by auto
with 4 have "\<sigma> = [(v, M\<cdot>N)]" by simp
- with occ_elim[OF no_occ]
+ with occs_elim[OF no_occs]
show ?case by auto
next
case (5 v M)
- hence no_occ: "\<not>occ (Var v) M" by (cases "occ (Var v) M", auto)
+ hence no_occs: "\<not> Var v \<prec> M" by auto
with 5 have "\<sigma> = [(v, M)]" by simp
- with occ_elim[OF no_occ]
+ with occs_elim[OF no_occs]
show ?case by auto
next
case (6 c d) thus ?case
@@ -449,48 +326,49 @@
case (7 M N M' N' \<sigma>)
then obtain \<theta>1 \<theta>2
where "unify M M' = Some \<theta>1"
- and "unify (N \<triangleleft> \<theta>1) (N' \<triangleleft> \<theta>1) = Some \<theta>2"
- and \<sigma>: "\<sigma> = \<theta>1 \<bullet> \<theta>2"
+ and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
+ and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
and ih1: "?P M M' \<theta>1"
- and ih2: "?P (N\<triangleleft>\<theta>1) (N'\<triangleleft>\<theta>1) \<theta>2"
+ and ih2: "?P (N\<lhd>\<theta>1) (N'\<lhd>\<theta>1) \<theta>2"
by (auto split:option.split_asm)
from `unify_dom (M \<cdot> N, M' \<cdot> N')`
have "unify_dom (M, M')"
by (rule accp_downward) (rule unify_rel.intros)
hence no_new_vars:
- "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
+ "\<And>t. vars_of (t \<lhd> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)
from ih2 show ?case
proof
- assume "\<exists>v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1). elim \<theta>2 v"
+ assume "\<exists>v\<in>vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1). elim \<theta>2 v"
then obtain v
- where "v\<in>vars_of (N \<triangleleft> \<theta>1) \<union> vars_of (N' \<triangleleft> \<theta>1)"
+ where "v\<in>vars_of (N \<lhd> \<theta>1) \<union> vars_of (N' \<lhd> \<theta>1)"
and el: "elim \<theta>2 v" by auto
with no_new_vars show ?thesis unfolding \<sigma>
by (auto simp:elim_def)
next
- assume empty[simp]: "\<theta>2 =\<^sub>s []"
+ assume empty[simp]: "\<theta>2 \<doteq> []"
- have "\<sigma> =\<^sub>s (\<theta>1 \<bullet> [])" unfolding \<sigma>
- by (rule compose_eqv) auto
- also have "\<dots> =\<^sub>s \<theta>1" by auto
- finally have "\<sigma> =\<^sub>s \<theta>1" .
+ have "\<sigma> \<doteq> (\<theta>1 \<lozenge> [])" unfolding \<sigma>
+ by (rule subst_cong) auto
+ also have "\<dots> \<doteq> \<theta>1" by auto
+ finally have "\<sigma> \<doteq> \<theta>1" .
from ih1 show ?thesis
proof
assume "\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta>1 v"
- with elim_eqv[OF `\<sigma> =\<^sub>s \<theta>1`]
+ with elim_eq[OF `\<sigma> \<doteq> \<theta>1`]
show ?thesis by auto
next
- note `\<sigma> =\<^sub>s \<theta>1`
- also assume "\<theta>1 =\<^sub>s []"
+ note `\<sigma> \<doteq> \<theta>1`
+ also assume "\<theta>1 \<doteq> []"
finally show ?thesis ..
qed
qed
qed
+declare unify.psimps[simp del]
subsection {* Termination proof *}
@@ -500,7 +378,7 @@
\<lambda>(M, N). size M]"
show "wf ?R" by simp
- fix M N M' N'
+ fix M N M' N' :: "'a trm"
show "((M, M'), (M \<cdot> N, M' \<cdot> N')) \<in> ?R" -- "Inner call"
by (rule measures_lesseq) (auto intro: card_mono)
@@ -509,7 +387,7 @@
"unify M M' = Some \<theta>"
from unify_eliminates[OF inner]
- show "((N \<triangleleft> \<theta>, N' \<triangleleft> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
+ show "((N \<lhd> \<theta>, N' \<lhd> \<theta>), (M \<cdot> N, M' \<cdot> N')) \<in>?R"
proof
-- {* Either a variable is eliminated \ldots *}
assume "(\<exists>v\<in>vars_of M \<union> vars_of M'. elim \<theta> v)"
@@ -517,7 +395,7 @@
where "elim \<theta> v"
and "v\<in>vars_of M \<union> vars_of M'" by auto
with unify_vars[OF inner]
- have "vars_of (N\<triangleleft>\<theta>) \<union> vars_of (N'\<triangleleft>\<theta>)
+ have "vars_of (N\<lhd>\<theta>) \<union> vars_of (N'\<lhd>\<theta>)
\<subset> vars_of (M\<cdot>N) \<union> vars_of (M'\<cdot>N')"
by auto
@@ -525,14 +403,125 @@
by (auto intro!: measures_less intro: psubset_card_mono)
next
-- {* Or the substitution is empty *}
- assume "\<theta> =\<^sub>s []"
- hence "N \<triangleleft> \<theta> = N"
- and "N' \<triangleleft> \<theta> = N'" by auto
+ assume "\<theta> \<doteq> []"
+ hence "N \<lhd> \<theta> = N"
+ and "N' \<lhd> \<theta> = N'" by auto
thus ?thesis
by (auto intro!: measures_less intro: psubset_card_mono)
qed
qed
-declare unify.psimps[simp del]
+
+subsection {* Unification returns a Most General Unifier *}
+
+lemma unify_computes_MGU:
+ "unify M N = Some \<sigma> \<Longrightarrow> MGU \<sigma> M N"
+proof (induct M N arbitrary: \<sigma> rule: unify.induct)
+ case (7 M N M' N' \<sigma>) -- "The interesting case"
+
+ then obtain \<theta>1 \<theta>2
+ where "unify M M' = Some \<theta>1"
+ and "unify (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
+ and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
+ and MGU_inner: "MGU \<theta>1 M M'"
+ and MGU_outer: "MGU \<theta>2 (N \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
+ by (auto split:option.split_asm)
+
+ show ?case
+ proof
+ from MGU_inner and MGU_outer
+ have "M \<lhd> \<theta>1 = M' \<lhd> \<theta>1"
+ and "N \<lhd> \<theta>1 \<lhd> \<theta>2 = N' \<lhd> \<theta>1 \<lhd> \<theta>2"
+ unfolding MGU_def Unifier_def
+ by auto
+ thus "M \<cdot> N \<lhd> \<sigma> = M' \<cdot> N' \<lhd> \<sigma>" unfolding \<sigma>
+ by simp
+ next
+ fix \<sigma>' assume "M \<cdot> N \<lhd> \<sigma>' = M' \<cdot> N' \<lhd> \<sigma>'"
+ hence "M \<lhd> \<sigma>' = M' \<lhd> \<sigma>'"
+ and Ns: "N \<lhd> \<sigma>' = N' \<lhd> \<sigma>'" by auto
+
+ with MGU_inner obtain \<delta>
+ where eqv: "\<sigma>' \<doteq> \<theta>1 \<lozenge> \<delta>"
+ unfolding MGU_def Unifier_def
+ by auto
+
+ from Ns have "N \<lhd> \<theta>1 \<lhd> \<delta> = N' \<lhd> \<theta>1 \<lhd> \<delta>"
+ by (simp add:subst_eq_dest[OF eqv])
+
+ with MGU_outer obtain \<rho>
+ where eqv2: "\<delta> \<doteq> \<theta>2 \<lozenge> \<rho>"
+ unfolding MGU_def Unifier_def
+ by auto
+
+ have "\<sigma>' \<doteq> \<sigma> \<lozenge> \<rho>" unfolding \<sigma>
+ by (rule subst_eq_intro, auto simp:subst_eq_dest[OF eqv] subst_eq_dest[OF eqv2])
+ thus "\<exists>\<gamma>. \<sigma>' \<doteq> \<sigma> \<lozenge> \<gamma>" ..
+ qed
+qed (auto simp: MGU_Const intro: MGU_Var MGU_Var[symmetric] split: split_if_asm)
+
+
+subsection {* Unification returns Idempotent Substitution *}
+
+definition Idem :: "'a subst \<Rightarrow> bool"
+where "Idem s \<longleftrightarrow> (s \<lozenge> s) \<doteq> s"
+
+lemma Idem_Nil [iff]: "Idem []"
+ by (simp add: Idem_def)
+
+lemma Var_Idem:
+ assumes "~ (Var v \<prec> t)" shows "Idem [(v,t)]"
+ unfolding Idem_def
+proof
+ from assms have [simp]: "t \<lhd> [(v, t)] = t"
+ by (metis assoc.simps(2) subst.simps(1) subst_no_occs)
+
+ fix s show "s \<lhd> [(v, t)] \<lozenge> [(v, t)] = s \<lhd> [(v, t)]"
+ by (induct s) auto
+qed
+
+lemma Unifier_Idem_subst:
+ "Idem(r) \<Longrightarrow> Unifier s (t \<lhd> r) (u \<lhd> r) \<Longrightarrow>
+ Unifier (r \<lozenge> s) (t \<lhd> r) (u \<lhd> r)"
+by (simp add: Idem_def Unifier_def subst_eq_def)
+
+lemma Idem_comp:
+ "Idem r \<Longrightarrow> Unifier s (t \<lhd> r) (u \<lhd> r) \<Longrightarrow>
+ (!!q. Unifier q (t \<lhd> r) (u \<lhd> r) \<Longrightarrow> s \<lozenge> q \<doteq> q) \<Longrightarrow>
+ Idem (r \<lozenge> s)"
+ apply (frule Unifier_Idem_subst, blast)
+ apply (force simp add: Idem_def subst_eq_def)
+ done
+
+theorem unify_gives_Idem:
+ "unify M N = Some \<sigma> \<Longrightarrow> Idem \<sigma>"
+proof (induct M N arbitrary: \<sigma> rule: unify.induct)
+ case (7 M M' N N' \<sigma>)
+
+ then obtain \<theta>1 \<theta>2
+ where "unify M N = Some \<theta>1"
+ and \<theta>2: "unify (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1) = Some \<theta>2"
+ and \<sigma>: "\<sigma> = \<theta>1 \<lozenge> \<theta>2"
+ and "Idem \<theta>1"
+ and "Idem \<theta>2"
+ by (auto split: option.split_asm)
+
+ from \<theta>2 have "Unifier \<theta>2 (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
+ by (rule unify_computes_MGU[THEN MGU_is_Unifier])
+
+ with `Idem \<theta>1`
+ show "Idem \<sigma>" unfolding \<sigma>
+ proof (rule Idem_comp)
+ fix \<sigma> assume "Unifier \<sigma> (M' \<lhd> \<theta>1) (N' \<lhd> \<theta>1)"
+ with \<theta>2 obtain \<gamma> where \<sigma>: "\<sigma> \<doteq> \<theta>2 \<lozenge> \<gamma>"
+ using unify_computes_MGU MGU_def by blast
+
+ have "\<theta>2 \<lozenge> \<sigma> \<doteq> \<theta>2 \<lozenge> (\<theta>2 \<lozenge> \<gamma>)" by (rule subst_cong) (auto simp: \<sigma>)
+ also have "... \<doteq> (\<theta>2 \<lozenge> \<theta>2) \<lozenge> \<gamma>" by (rule comp_assoc[symmetric])
+ also have "... \<doteq> \<theta>2 \<lozenge> \<gamma>" by (rule subst_cong) (auto simp: `Idem \<theta>2`[unfolded Idem_def])
+ also have "... \<doteq> \<sigma>" by (rule \<sigma>[symmetric])
+ finally show "\<theta>2 \<lozenge> \<sigma> \<doteq> \<sigma>" .
+ qed
+qed (auto intro!: Var_Idem split: option.splits if_splits)
end