# HG changeset patch # User krauss # Date 1314003453 -7200 # Node ID 9c5cc8134cba3b43904a872089000a9cc4ec73fb # Parent dfc2e722fe47314064aba798bab2671d59e4c364# Parent 7ce460760f99483af6a031382873fd3567307cbb merged diff -r 7ce460760f99 -r 9c5cc8134cba src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- 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; diff -r 7ce460760f99 -r 9c5cc8134cba src/HOL/Import/Generate-HOL/ROOT.ML --- 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"; diff -r 7ce460760f99 -r 9c5cc8134cba src/HOL/IsaMakefile --- 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 \ diff -r 7ce460760f99 -r 9c5cc8134cba src/HOL/NanoJava/Decl.thy --- 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" \ (type) "cname \ class" (type) "prog " \ (type) "cdecl list" -consts - +axiomatization Prog :: prog --{* program as a global value *} +and Object :: cname --{* name of root class *} diff -r 7ce460760f99 -r 9c5cc8134cba src/HOL/NanoJava/Example.thy --- 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 \ Par" - Res_neq_This [simp]: "Res \ This" +axiomatization where + This_neq_Par [simp]: "This \ Par" and + Res_neq_This [simp]: "Res \ 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 \C Nat = (D=Nat)" +axiomatization where Nat_no_subclasses [simp]: "D \C Nat = (D=Nat)" -axioms method_Nat_add [simp]: "method Nat add = Some +axiomatization where method_Nat_add [simp]: "method Nat add = Some \ 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 \" -axioms method_Nat_suc [simp]: "method Nat suc = Some +axiomatization where method_Nat_suc [simp]: "method Nat suc = Some \ par=NT, res=Class Nat, lcl=[], bdy= Res :== new Nat;; LAcc Res..pred :== LAcc This \" -axioms field_Nat [simp]: "field Nat = empty(pred\Class Nat)" +axiomatization where field_Nat [simp]: "field Nat = empty(pred\Class Nat)" lemma init_locs_Nat_add [simp]: "init_locs Nat add s = s" by (simp add: init_locs_def init_vars_def) diff -r 7ce460760f99 -r 9c5cc8134cba src/HOL/NanoJava/Term.thy --- 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 \ Par" Par_neq_Res [simp]: "Par \ Res" Res_neq_This [simp]: "Res \ This" diff -r 7ce460760f99 -r 9c5cc8134cba src/HOL/NanoJava/TypeRel.thy --- 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 \ cname) set" --{* subclass *} +text{* Direct subclass relation *} + +definition subcls1 :: "(cname \ cname) set" +where + "subcls1 \ {(C,D). C\Object \ (\c. class C = Some c \ super c=D)}" abbreviation subcls1_syntax :: "[cname, cname] => bool" ("_ <=C1 _" [71,71] 70) @@ -20,17 +23,9 @@ subcls1_syntax ("_ \C1 _" [71,71] 70) and subcls_syntax ("_ \C _" [71,71] 70) -consts - method :: "cname => (mname \ methd)" - field :: "cname => (fname \ ty)" - subsection "Declarations and properties not used in the meta theory" -text{* Direct subclass relation *} -defs - subcls1_def: "subcls1 \ {(C,D). C\Object \ (\c. class C = Some c \ super c=D)}" - text{* Widening, viz. method invocation conversion *} inductive widen :: "ty => ty => bool" ("_ \ _" [71,71] 70) @@ -111,7 +106,8 @@ done --{* Methods of a class, with inheritance and hiding *} -defs method_def: "method C \ class_rec C methods" +definition method :: "cname => (mname \ methd)" where + "method C \ class_rec C methods" lemma method_rec: "\class C = Some m; ws_prog\ \ 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 \ class_rec C flds" +definition field :: "cname => (fname \ ty)" where + "field C \ class_rec C flds" lemma flds_rec: "\class C = Some m; ws_prog\ \ field C = (if C=Object then empty else field (super m)) ++ map_of (flds m)" diff -r 7ce460760f99 -r 9c5cc8134cba src/HOL/Subst/AList.thy --- 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 [] \ (!!x y xs. P xs \ P ((x,y) # xs)) \ P l" - by (induct l) auto - -end diff -r 7ce460760f99 -r 9c5cc8134cba src/HOL/Subst/ROOT.ML --- 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"]; diff -r 7ce460760f99 -r 9c5cc8134cba src/HOL/Subst/Subst.thy --- 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 "\" 55) - -definition - subst_eq :: "[('a*('a uterm)) list,('a*('a uterm)) list] => bool" (infixr "=$=" 52) - where "r =$= s \ (\t. t \ r = t \ s)" - -notation (xsymbols) - subst_eq (infixr "\" 52) - -definition - comp :: "('a * 'a uterm) list \ ('a * 'a uterm) list \ ('a* 'a uterm) list" - (infixl "<>" 56) - where "al <> bl = alist_rec al bl (%x y xs g. (x,y \ bl) # g)" - -notation (xsymbols) - comp (infixl "\" 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. \x \ sdom(al). y = vars_of(Var(x) \ al)})" - - - -subsection {* Basic Laws *} - -lemma subst_Nil [simp]: "t \ [] = t" - by (induct t) auto - -lemma subst_mono: "t \ u \ t \ s \ u \ s" - by (induct u) auto - -lemma Var_not_occs: "~ (Var(v) \ t) \ t \ (v,t \ s) # s = t \ s" - apply (case_tac "t = Var v") - prefer 2 - apply (erule rev_mp)+ - apply (rule_tac 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 \ vars_of t. Var v \ r = Var v \ s)" - by (induct t) auto - -lemma repl_invariance: "~ v: vars_of t ==> t \ (v,u)#s = t \ s" - by (simp add: agreement) - -lemma Var_in_subst: - "v \ vars_of(t) --> w \ vars_of(t \ (v,Var(w))#s)" - by (induct 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) - -lemma ssubst_subst2: - "[| s \ r; P (t \ r) (u \ r) |] ==> P (t \ s) (u \ s)" - by (simp add: subst_eq_def) - - -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 t) - apply simp_all - apply (induct r) - apply auto - done - -lemma comp_assoc: "(q \ r) \ s \ q \ (r \ s)" - by (simp add: subst_eq_iff) - -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) - apply 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) - apply 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)" - unfolding empty_def by blast - -lemma invariance: "(t \ 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 \ sdom(s) \ v \ vars_of(t \ s) \ v \ srange(s)" - apply (induct 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: - "v \ vars_of(t \ s) \ v \ srange(s) | v \ 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 \ srange(s) ==> \w. w \ sdom(s) & v \ vars_of(Var(w) \ s)" - by (simp add: srange_iff) - -lemma dom_range_disjoint: - "sdom(s) Int srange(s) = {} = (\t. sdom(s) Int vars_of(t \ s) = {})" - apply (simp 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 M) auto - -end diff -r 7ce460760f99 -r 9c5cc8134cba src/HOL/Subst/UTerm.thy --- 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 "\" 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 \ vars_of (Var w)) = (w = v)" - by auto - -lemma vars_iff_occseq: "(x \ vars_of t) = (Var x \ t | Var x = t)" - by (induct t) auto - - -text{* Not used, but perhaps useful in other proofs *} -lemma occs_vars_subset: "M \ N \ vars_of M \ vars_of N" - by (induct 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 M) auto - -end diff -r 7ce460760f99 -r 9c5cc8134cba src/HOL/Subst/Unifier.thy --- 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 \ 'a uterm \ 'a uterm \ bool" - where "Unifier s t u \ t <| s = u <| s" - -definition - MoreGeneral :: "('a * 'a uterm) list \ ('a * 'a uterm) list \ bool" (infixr ">>" 52) - where "r >> s \ (\q. s =$= r <> q)" - -definition - MGUnifier :: "('a * 'a uterm) list \ 'a uterm \ 'a uterm \ bool" - where "MGUnifier s t u \ Unifier s t u & (\r. Unifier r t u --> s >> r)" - -definition - Idem :: "('a * 'a uterm)list => bool" where - "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 [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) \ 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 7ce460760f99 -r 9c5cc8134cba src/HOL/Subst/Unify.thy --- 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 \ 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) - - -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))) \ unifyRel ==> - ((X,Y), (Comb (Comb A B) C, Comb (Comb D E) F)) \ 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 \ 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{*@{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 "\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 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) - -lemma unify_induct: - "(\m n. P (Const m) (Const n)) \ - (\m M N. P (Const m) (Comb M N)) \ - (\m v. P (Const m) (Var v)) \ - (\v M. P (Var v) M) \ - (\M N x. P (Comb M N) (Const x)) \ - (\M N v. P (Comb M N) (Var v)) \ - (\M1 N1 M2 N2. - \theta. unify (M1, M2) = Some theta \ P (N1 \ theta) (N2 \ theta) \ - P M1 M2 \ P (Comb M1 N1) (Comb M2 N2)) \ - 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]: - "\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 \ 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 diff -r 7ce460760f99 -r 9c5cc8134cba src/HOL/ex/Unification.thy --- 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 "\" 60) + | Comb "'a trm" "'a trm" (infix "\" 60) + +primrec vars_of :: "'a trm \ 'a set" +where + "vars_of (Var v) = {v}" +| "vars_of (Const c) = {}" +| "vars_of (M \ N) = vars_of M \ vars_of N" + +fun occs :: "'a trm \ 'a trm \ bool" (infixl "\" 54) +where + "u \ Var v \ False" +| "u \ Const c \ False" +| "u \ M \ N \ u = M \ u = N \ u \ M \ u \ N" + + +lemma finite_vars_of[intro]: "finite (vars_of t)" + by (induct t) simp_all + +lemma vars_iff_occseq: "x \ vars_of t \ Var x \ t \ Var x = t" + by (induct t) auto + +lemma occs_vars_subset: "M \ N \ vars_of M \ vars_of N" + by (induct N) auto + + +subsection {* Substitutions *} type_synonym 'a subst = "('a \ 'a trm) list" -text {* Applying a substitution to a variable: *} - fun assoc :: "'a \ 'b \ ('a \ 'b) list \ '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 \ 'a subst \ 'a trm" (infixl "\" 60) +primrec subst :: "'a trm \ 'a subst \ 'a trm" (infixl "\" 55) where - "(Var v) \ s = assoc v (Var v) s" -| "(Const c) \ s = (Const c)" -| "(M \ N) \ s = (M \ s) \ (N \ s)" + "(Var v) \ s = assoc v (Var v) s" +| "(Const c) \ s = (Const c)" +| "(M \ N) \ s = (M \ s) \ (N \ s)" -text {* Composition of substitutions: *} - -fun - "compose" :: "'a subst \ 'a subst \ 'a subst" (infixl "\" 80) +definition subst_eq (infixr "\" 52) where - "[] \ bl = bl" -| "((a,b) # al) \ bl = (a, b \ bl) # (al \ bl)" + "s1 \ s2 \ (\t. t \ s1 = t \ s2)" -text {* Equivalence of substitutions: *} - -definition eqv (infix "=\<^sub>s" 50) +fun comp :: "'a subst \ 'a subst \ 'a subst" (infixl "\" 56) where - "s1 =\<^sub>s s2 \ \t. t \ s1 = t \ s2" - + "[] \ bl = bl" +| "((a,b) # al) \ bl = (a, b \ bl) # (al \ bl)" -subsection {* Basic lemmas *} - -lemma apply_empty[simp]: "t \ [] = t" +lemma subst_Nil[simp]: "t \ [] = t" by (induct t) auto -lemma compose_empty[simp]: "\ \ [] = \" +lemma subst_mono: "t \ u \ t \ s \ u \ s" +by (induct u) auto + +lemma agreement: "(t \ r = t \ s) \ (\v \ vars_of t. Var v \ r = Var v \ s)" +by (induct t) auto + +lemma repl_invariance: "v \ vars_of t \ t \ (v,u) # s = t \ s" +by (simp add: agreement) + +lemma remove_var: "v \ vars_of s \ v \ vars_of (t \ [(v, s)])" +by (induct t) simp_all + +lemma subst_refl[iff]: "s \ s" + by (auto simp:subst_eq_def) + +lemma subst_sym[sym]: "\s1 \ s2\ \ s2 \ s1" + by (auto simp:subst_eq_def) + +lemma subst_trans[trans]: "\s1 \ s2; s2 \ s3\ \ s1 \ s3" + by (auto simp:subst_eq_def) + +lemma subst_no_occs: "\ Var v \ t \ Var v \ t + \ t \ [(v,s)] = t" +by (induct t) auto + +lemma comp_Nil[simp]: "\ \ [] = \" by (induct \) auto -lemma apply_compose[simp]: "t \ (s1 \ s2) = t \ s1 \ s2" +lemma subst_comp[simp]: "t \ (r \ s) = t \ r \ 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]: "(\t. t \ \ = t \ \) \ \ \ \" + by (auto simp:subst_eq_def) + +lemma subst_eq_dest[dest]: "s1 \ s2 \ t \ s1 = t \