# HG changeset patch
# User haftmann
# Date 1266916291 -3600
# Node ID 4140f31b2ed207024c86f9af7b9a1d64e0cc62f2
# Parent e1b61c5fd494a3bffbca9a05b6723a084b04f95d
dropped session W0; c.f. MiniML in AFP
diff -r e1b61c5fd494 -r 4140f31b2ed2 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile Tue Feb 23 10:11:16 2010 +0100
+++ b/src/HOL/IsaMakefile Tue Feb 23 10:11:31 2010 +0100
@@ -66,7 +66,6 @@
TLA-Memory \
HOL-UNITY \
HOL-Unix \
- HOL-W0 \
HOL-Word-Examples \
HOL-ZF
# ^ this is the sort position
@@ -592,9 +591,10 @@
$(LOG)/HOL-Hoare.gz: $(OUT)/HOL Hoare/Arith2.thy Hoare/Examples.thy \
Hoare/Hoare.thy Hoare/hoare_tac.ML Hoare/Heap.thy \
+ Hoare/Hoare_Logic.thy Hoare/Hoare_Logic_Abort.thy \
Hoare/HeapSyntax.thy Hoare/Pointer_Examples.thy Hoare/ROOT.ML \
Hoare/ExamplesAbort.thy Hoare/HeapSyntaxAbort.thy \
- Hoare/HoareAbort.thy Hoare/SchorrWaite.thy Hoare/Separation.thy \
+ Hoare/SchorrWaite.thy Hoare/Separation.thy \
Hoare/SepLogHeap.thy Hoare/document/root.tex Hoare/document/root.bib
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Hoare
@@ -848,14 +848,6 @@
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Prolog
-## HOL-W0
-
-HOL-W0: HOL $(LOG)/HOL-W0.gz
-
-$(LOG)/HOL-W0.gz: $(OUT)/HOL W0/ROOT.ML W0/W0.thy W0/document/root.tex
- @$(ISABELLE_TOOL) usedir $(OUT)/HOL W0
-
-
## HOL-MicroJava
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
@@ -1321,7 +1313,7 @@
$(LOG)/HOL-SMT-Examples.gz $(LOG)/HOL-SMT.gz \
$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz \
$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz \
- $(LOG)/HOL-W0.gz $(LOG)/HOL-Word-Examples.gz \
+ $(LOG)/HOL-Word-Examples.gz \
$(LOG)/HOL-Word.gz $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz \
$(LOG)/HOL.gz $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz \
$(LOG)/TLA-Inc.gz $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz \
diff -r e1b61c5fd494 -r 4140f31b2ed2 src/HOL/W0/README.html
--- a/src/HOL/W0/README.html Tue Feb 23 10:11:16 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-
-
-
-
-
-
-
-
- HOL/W0/README
-
-
-
-
-Type Inference for MiniML (without let)
-
-This theory defines the type inference rules and the type inference algorithm
-W for simply-typed lambda terms due to Milner. It proves the
-soundness and completeness of W w.r.t. to the rules. An optimized
-version I is shown to implement W.
-
-
-
-A report describing the theory is found here:
-
-Formal Verification of Algorithm W: The Monomorphic Case.
-
-
-
-NOTE: This theory has been superseded by a more recent development
-which formalizes type inference for a language including let. For
-details click here.
-
-
diff -r e1b61c5fd494 -r 4140f31b2ed2 src/HOL/W0/ROOT.ML
--- a/src/HOL/W0/ROOT.ML Tue Feb 23 10:11:16 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-use_thys ["W0"];
diff -r e1b61c5fd494 -r 4140f31b2ed2 src/HOL/W0/W0.thy
--- a/src/HOL/W0/W0.thy Tue Feb 23 10:11:16 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,925 +0,0 @@
-(* Title: HOL/W0/W0.thy
- ID: $Id$
- Author: Dieter Nazareth, Tobias Nipkow, Thomas Stauner, Markus Wenzel
-*)
-
-theory W0
-imports Main
-begin
-
-section {* Universal error monad *}
-
-datatype 'a maybe = Ok 'a | Fail
-
-definition
- bind :: "'a maybe \ ('a \ 'b maybe) \ 'b maybe" (infixl "\" 60) where
- "m \ f = (case m of Ok r \ f r | Fail \ Fail)"
-
-syntax
- "_bind" :: "patterns \ 'a maybe \ 'b \ 'c" ("(_ := _;//_)" 0)
-translations
- "P := E; F" == "E \ (\P. F)"
-
-lemma bind_Ok [simp]: "(Ok s) \ f = (f s)"
- by (simp add: bind_def)
-
-lemma bind_Fail [simp]: "Fail \ f = Fail"
- by (simp add: bind_def)
-
-lemma split_bind:
- "P (res \ f) = ((res = Fail \ P Fail) \ (\s. res = Ok s \ P (f s)))"
- by (induct res) simp_all
-
-lemma split_bind_asm:
- "P (res \ f) = (\ (res = Fail \ \ P Fail \ (\s. res = Ok s \ \ P (f s))))"
- by (simp split: split_bind)
-
-lemmas bind_splits = split_bind split_bind_asm
-
-lemma bind_eq_Fail [simp]:
- "((m \ f) = Fail) = ((m = Fail) \ (\p. m = Ok p \ f p = Fail))"
- by (simp split: split_bind)
-
-lemma rotate_Ok: "(y = Ok x) = (Ok x = y)"
- by (rule eq_sym_conv)
-
-
-section {* MiniML-types and type substitutions *}
-
-axclass type_struct \ type
- -- {* new class for structures containing type variables *}
-
-datatype "typ" = TVar nat | TFun "typ" "typ" (infixr "->" 70)
- -- {* type expressions *}
-
-types subst = "nat => typ"
- -- {* type variable substitution *}
-
-instance "typ" :: type_struct ..
-instance list :: (type_struct) type_struct ..
-instance "fun" :: (type, type_struct) type_struct ..
-
-
-subsection {* Substitutions *}
-
-consts
- app_subst :: "subst \ 'a::type_struct \ 'a::type_struct" ("$")
- -- {* extension of substitution to type structures *}
-primrec (app_subst_typ)
- app_subst_TVar: "$s (TVar n) = s n"
- app_subst_Fun: "$s (t1 -> t2) = $s t1 -> $s t2"
-
-defs (overloaded)
- app_subst_list: "$s \ map ($s)"
-
-consts
- free_tv :: "'a::type_struct \ nat set"
- -- {* @{text "free_tv s"}: the type variables occuring freely in the type structure @{text s} *}
-
-primrec (free_tv_typ)
- "free_tv (TVar m) = {m}"
- "free_tv (t1 -> t2) = free_tv t1 \ free_tv t2"
-
-primrec (free_tv_list)
- "free_tv [] = {}"
- "free_tv (x # xs) = free_tv x \ free_tv xs"
-
-definition
- dom :: "subst \ nat set" where
- "dom s = {n. s n \ TVar n}"
- -- {* domain of a substitution *}
-
-definition
- cod :: "subst \ nat set" where
- "cod s = (\m \ dom s. free_tv (s m))"
- -- {* codomain of a substitutions: the introduced variables *}
-
-defs (overloaded)
- free_tv_subst: "free_tv s \ dom s \ cod s"
-
-text {*
- @{text "new_tv s n"} checks whether @{text n} is a new type variable
- wrt.\ a type structure @{text s}, i.e.\ whether @{text n} is greater
- than any type variable occuring in the type structure.
-*}
-
-definition
- new_tv :: "nat \ 'a::type_struct \ bool" where
- "new_tv n ts = (\m. m \ free_tv ts \ m < n)"
-
-
-subsubsection {* Identity substitution *}
-
-definition
- id_subst :: subst where
- "id_subst = (\n. TVar n)"
-
-lemma app_subst_id_te [simp]:
- "$id_subst = (\t::typ. t)"
- -- {* application of @{text id_subst} does not change type expression *}
-proof
- fix t :: "typ"
- show "$id_subst t = t"
- by (induct t) (simp_all add: id_subst_def)
-qed
-
-lemma app_subst_id_tel [simp]: "$id_subst = (\ts::typ list. ts)"
- -- {* application of @{text id_subst} does not change list of type expressions *}
-proof
- fix ts :: "typ list"
- show "$id_subst ts = ts"
- by (induct ts) (simp_all add: app_subst_list)
-qed
-
-lemma o_id_subst [simp]: "$s o id_subst = s"
- by (rule ext) (simp add: id_subst_def)
-
-lemma dom_id_subst [simp]: "dom id_subst = {}"
- by (simp add: dom_def id_subst_def)
-
-lemma cod_id_subst [simp]: "cod id_subst = {}"
- by (simp add: cod_def)
-
-lemma free_tv_id_subst [simp]: "free_tv id_subst = {}"
- by (simp add: free_tv_subst)
-
-
-lemma cod_app_subst [simp]:
- assumes free: "v \ free_tv (s n)"
- and neq: "v \ n"
- shows "v \ cod s"
-proof -
- have "s n \ TVar n"
- proof
- assume "s n = TVar n"
- with free have "v = n" by simp
- with neq show False ..
- qed
- with free show ?thesis
- by (auto simp add: dom_def cod_def)
-qed
-
-lemma subst_comp_te: "$g ($f t :: typ) = $(\x. $g (f x)) t"
- -- {* composition of substitutions *}
- by (induct t) simp_all
-
-lemma subst_comp_tel: "$g ($f ts :: typ list) = $(\x. $g (f x)) ts"
- by (induct ts) (simp_all add: app_subst_list subst_comp_te)
-
-
-lemma app_subst_Nil [simp]: "$s [] = []"
- by (simp add: app_subst_list)
-
-lemma app_subst_Cons [simp]: "$s (t # ts) = ($s t) # ($s ts)"
- by (simp add: app_subst_list)
-
-lemma new_tv_TVar [simp]: "new_tv n (TVar m) = (m < n)"
- by (simp add: new_tv_def)
-
-lemma new_tv_Fun [simp]:
- "new_tv n (t1 -> t2) = (new_tv n t1 \ new_tv n t2)"
- by (auto simp add: new_tv_def)
-
-lemma new_tv_Nil [simp]: "new_tv n []"
- by (simp add: new_tv_def)
-
-lemma new_tv_Cons [simp]: "new_tv n (t # ts) = (new_tv n t \ new_tv n ts)"
- by (auto simp add: new_tv_def)
-
-lemma new_tv_id_subst [simp]: "new_tv n id_subst"
- by (simp add: id_subst_def new_tv_def free_tv_subst dom_def cod_def)
-
-lemma new_tv_subst:
- "new_tv n s =
- ((\m. n \ m \ s m = TVar m) \
- (\l. l < n \ new_tv n (s l)))"
- apply (unfold new_tv_def)
- apply (tactic "safe_tac HOL_cs")
- -- {* @{text \} *}
- apply (tactic {* fast_tac (HOL_cs addDs [@{thm leD}] addss (@{simpset}
- addsimps [thm "free_tv_subst", thm "dom_def"])) 1 *})
- apply (subgoal_tac "m \ cod s \ s l = TVar l")
- apply (tactic "safe_tac HOL_cs")
- apply (tactic {* fast_tac (HOL_cs addDs [UnI2] addss (@{simpset}
- addsimps [thm "free_tv_subst"])) 1 *})
- apply (drule_tac P = "\x. m \ free_tv x" in subst, assumption)
- apply simp
- apply (unfold free_tv_subst cod_def dom_def)
- apply clarsimp
- apply safe
- apply metis
- apply (metis linorder_not_less)+
- done
-
-lemma new_tv_list: "new_tv n x = (\y \ set x. new_tv n y)"
- by (induct x) simp_all
-
-lemma subst_te_new_tv [simp]:
- "new_tv n (t::typ) \ $(\x. if x = n then t' else s x) t = $s t"
- -- {* substitution affects only variables occurring freely *}
- by (induct t) simp_all
-
-lemma subst_tel_new_tv [simp]:
- "new_tv n (ts::typ list) \ $(\x. if x = n then t else s x) ts = $s ts"
- by (induct ts) simp_all
-
-lemma new_tv_le: "n \ m \ new_tv n (t::typ) \ new_tv m t"
- -- {* all greater variables are also new *}
-proof (induct t)
- case (TVar n)
- then show ?case by (auto intro: less_le_trans)
-next
- case TFun
- then show ?case by simp
-qed
-
-lemma [simp]: "new_tv n t \ new_tv (Suc n) (t::typ)"
- by (rule lessI [THEN less_imp_le [THEN new_tv_le]])
-
-lemma new_tv_list_le:
- assumes "n \ m"
- shows "new_tv n (ts::typ list) \ new_tv m ts"
-proof (induct ts)
- case Nil
- then show ?case by simp
-next
- case Cons
- with `n \ m` show ?case by (auto intro: new_tv_le)
-qed
-
-lemma [simp]: "new_tv n ts \ new_tv (Suc n) (ts::typ list)"
- by (rule lessI [THEN less_imp_le [THEN new_tv_list_le]])
-
-lemma new_tv_subst_le: "n \ m \ new_tv n (s::subst) \ new_tv m s"
- apply (simp add: new_tv_subst)
- apply clarify
- apply (rule_tac P = "l < n" and Q = "n <= l" in disjE)
- apply clarify
- apply (simp_all add: new_tv_le)
- done
-
-lemma [simp]: "new_tv n s \ new_tv (Suc n) (s::subst)"
- by (rule lessI [THEN less_imp_le [THEN new_tv_subst_le]])
-
-lemma new_tv_subst_var:
- "n < m \ new_tv m (s::subst) \ new_tv m (s n)"
- -- {* @{text new_tv} property remains if a substitution is applied *}
- by (simp add: new_tv_subst)
-
-lemma new_tv_subst_te [simp]:
- "new_tv n s \ new_tv n (t::typ) \ new_tv n ($s t)"
- by (induct t) (auto simp add: new_tv_subst)
-
-lemma new_tv_subst_tel [simp]:
- "new_tv n s \ new_tv n (ts::typ list) \ new_tv n ($s ts)"
- by (induct ts) (fastsimp simp add: new_tv_subst)+
-
-lemma new_tv_Suc_list: "new_tv n ts --> new_tv (Suc n) (TVar n # ts)"
- -- {* auxilliary lemma *}
- by (simp add: new_tv_list)
-
-lemma new_tv_subst_comp_1 [simp]:
- "new_tv n (s::subst) \ new_tv n r \ new_tv n ($r o s)"
- -- {* composition of substitutions preserves @{text new_tv} proposition *}
- by (simp add: new_tv_subst)
-
-lemma new_tv_subst_comp_2 [simp]:
- "new_tv n (s::subst) \ new_tv n r \ new_tv n (\v. $r (s v))"
- by (simp add: new_tv_subst)
-
-lemma new_tv_not_free_tv [simp]: "new_tv n ts \ n \ free_tv ts"
- -- {* new type variables do not occur freely in a type structure *}
- by (auto simp add: new_tv_def)
-
-lemma ftv_mem_sub_ftv_list [simp]:
- "(t::typ) \ set ts \ free_tv t \ free_tv ts"
- by (induct ts) auto
-
-text {*
- If two substitutions yield the same result if applied to a type
- structure the substitutions coincide on the free type variables
- occurring in the type structure.
-*}
-
-lemma eq_subst_te_eq_free:
- "$s1 (t::typ) = $s2 t \ n \ free_tv t \ s1 n = s2 n"
- by (induct t) auto
-
-lemma eq_free_eq_subst_te:
- "(\n. n \ free_tv t --> s1 n = s2 n) \ $s1 (t::typ) = $s2 t"
- by (induct t) auto
-
-lemma eq_subst_tel_eq_free:
- "$s1 (ts::typ list) = $s2 ts \ n \ free_tv ts \ s1 n = s2 n"
- by (induct ts) (auto intro: eq_subst_te_eq_free)
-
-lemma eq_free_eq_subst_tel:
- "(\n. n \ free_tv ts --> s1 n = s2 n) \ $s1 (ts::typ list) = $s2 ts"
- by (induct ts) (auto intro: eq_free_eq_subst_te)
-
-text {*
- \medskip Some useful lemmas.
-*}
-
-lemma codD: "v \ cod s \ v \ free_tv s"
- by (simp add: free_tv_subst)
-
-lemma not_free_impl_id: "x \ free_tv s \ s x = TVar x"
- by (simp add: free_tv_subst dom_def)
-
-lemma free_tv_le_new_tv: "new_tv n t \ m \ free_tv t \ m < n"
- by (unfold new_tv_def) fast
-
-lemma free_tv_subst_var: "free_tv (s (v::nat)) \ insert v (cod s)"
- by (cases "v \ dom s") (auto simp add: cod_def dom_def)
-
-lemma free_tv_app_subst_te: "free_tv ($s (t::typ)) \ cod s \ free_tv t"
- by (induct t) (auto simp add: free_tv_subst_var)
-
-lemma free_tv_app_subst_tel: "free_tv ($s (ts::typ list)) \ cod s \ free_tv ts"
- apply (induct ts)
- apply simp
- apply (cut_tac free_tv_app_subst_te)
- apply fastsimp
- done
-
-lemma free_tv_comp_subst:
- "free_tv (\u::nat. $s1 (s2 u) :: typ) \ free_tv s1 \ free_tv s2"
- apply (unfold free_tv_subst dom_def)
- apply (auto dest!: free_tv_subst_var [THEN subsetD] free_tv_app_subst_te [THEN subsetD]
- simp add: cod_def dom_def simp del: bex_simps)
- done
-
-
-subsection {* Most general unifiers *}
-
-consts
- mgu :: "typ \ typ \ subst maybe"
-axioms
- mgu_eq [simp]: "mgu t1 t2 = Ok u \ $u t1 = $u t2"
- mgu_mg [simp]: "mgu t1 t2 = Ok u \ $s t1 = $s t2 \ \r. s = $r o u"
- mgu_Ok: "$s t1 = $s t2 \ \u. mgu t1 t2 = Ok u"
- mgu_free [simp]: "mgu t1 t2 = Ok u \ free_tv u \ free_tv t1 \ free_tv t2"
-
-lemma mgu_new: "mgu t1 t2 = Ok u \ new_tv n t1 \ new_tv n t2 \ new_tv n u"
- -- {* @{text mgu} does not introduce new type variables *}
- by (unfold new_tv_def) (blast dest: mgu_free)
-
-
-section {* Mini-ML with type inference rules *}
-
-datatype
- expr = Var nat | Abs expr | App expr expr
-
-
-text {* Type inference rules. *}
-
-inductive
- has_type :: "typ list \ expr \ typ \ bool" ("((_) |-/ (_) :: (_))" [60, 0, 60] 60)
- where
- Var: "n < length a \ a |- Var n :: a ! n"
- | Abs: "t1#a |- e :: t2 \ a |- Abs e :: t1 -> t2"
- | App: "a |- e1 :: t2 -> t1 \ a |- e2 :: t2
- \ a |- App e1 e2 :: t1"
-
-
-text {* Type assigment is closed wrt.\ substitution. *}
-
-lemma has_type_subst_closed: "a |- e :: t ==> $s a |- e :: $s t"
-proof (induct set: has_type)
- case (Var n a)
- then have "n < length (map ($ s) a)" by simp
- then have "map ($ s) a |- Var n :: map ($ s) a ! n"
- by (rule has_type.Var)
- also have "map ($ s) a ! n = $ s (a ! n)"
- by (rule nth_map) (rule Var)
- also have "map ($ s) a = $ s a"
- by (simp only: app_subst_list)
- finally show ?case .
-next
- case (Abs t1 a e t2)
- then have "$ s t1 # map ($ s) a |- e :: $ s t2"
- by (simp add: app_subst_list)
- then have "map ($ s) a |- Abs e :: $ s t1 -> $ s t2"
- by (rule has_type.Abs)
- then show ?case
- by (simp add: app_subst_list)
-next
- case App
- then show ?case by (simp add: has_type.App)
-qed
-
-
-section {* Correctness and completeness of the type inference algorithm W *}
-
-consts
- "\" :: "expr \ typ list \ nat \ (subst \ typ \ nat) maybe"
-primrec
- "\ (Var i) a n =
- (if i < length a then Ok (id_subst, a ! i, n) else Fail)"
- "\ (Abs e) a n =
- ((s, t, m) := \ e (TVar n # a) (Suc n);
- Ok (s, (s n) -> t, m))"
- "\ (App e1 e2) a n =
- ((s1, t1, m1) := \ e1 a n;
- (s2, t2, m2) := \ e2 ($s1 a) m1;
- u := mgu ($ s2 t1) (t2 -> TVar m2);
- Ok ($u o $s2 o s1, $u (TVar m2), Suc m2))"
-
-theorem W_correct: "Ok (s, t, m) = \ e a n ==> $s a |- e :: t"
-proof (induct e arbitrary: a s t m n)
- case (Var i)
- from `Ok (s, t, m) = \ (Var i) a n`
- show "$s a |- Var i :: t" by (simp add: has_type.Var split: if_splits)
-next
- case (Abs e)
- from `Ok (s, t, m) = \ (Abs e) a n`
- obtain t' where "t = s n -> t'"
- and "Ok (s, t', m) = \ e (TVar n # a) (Suc n)"
- by (auto split: bind_splits)
- with Abs.hyps show "$s a |- Abs e :: t"
- by (force intro: has_type.Abs)
-next
- case (App e1 e2)
- from `Ok (s, t, m) = \ (App e1 e2) a n`
- obtain s1 t1 n1 s2 t2 n2 u where
- s: "s = $u o $s2 o s1"
- and t: "t = u n2"
- and mgu_ok: "mgu ($s2 t1) (t2 -> TVar n2) = Ok u"
- and W1_ok: "Ok (s1, t1, n1) = \ e1 a n"
- and W2_ok: "Ok (s2, t2, n2) = \ e2 ($s1 a) n1"
- by (auto split: bind_splits simp: that)
- show "$s a |- App e1 e2 :: t"
- proof (rule has_type.App)
- from s have s': "$u ($s2 ($s1 a)) = $s a"
- by (simp add: subst_comp_tel o_def)
- show "$s a |- e1 :: $u t2 -> t"
- proof -
- from W1_ok have "$s1 a |- e1 :: t1" by (rule App.hyps(1))
- then have "$u ($s2 ($s1 a)) |- e1 :: $u ($s2 t1)"
- by (intro has_type_subst_closed)
- with s' t mgu_ok show ?thesis by simp
- qed
- show "$s a |- e2 :: $u t2"
- proof -
- from W2_ok have "$s2 ($s1 a) |- e2 :: t2" by (rule App.hyps(2))
- then have "$u ($s2 ($s1 a)) |- e2 :: $u t2"
- by (rule has_type_subst_closed)
- with s' show ?thesis by simp
- qed
- qed
-qed
-
-
-inductive_cases has_type_casesE:
- "s |- Var n :: t"
- "s |- Abs e :: t"
- "s |- App e1 e2 ::t"
-
-
-lemmas [simp] = Suc_le_lessD
- and [simp del] = less_imp_le ex_simps all_simps
-
-lemma W_var_ge [simp]: "!!a n s t m. \ e a n = Ok (s, t, m) \ n \ m"
- -- {* the resulting type variable is always greater or equal than the given one *}
- apply (atomize (full))
- apply (induct e)
- txt {* case @{text "Var n"} *}
- apply clarsimp
- txt {* case @{text "Abs e"} *}
- apply (simp split add: split_bind)
- apply (fast dest: Suc_leD)
- txt {* case @{text "App e1 e2"} *}
- apply (simp (no_asm) split add: split_bind)
- apply (intro strip)
- apply (rename_tac s t na sa ta nb sb)
- apply (erule_tac x = a in allE)
- apply (erule_tac x = n in allE)
- apply (erule_tac x = "$s a" in allE)
- apply (erule_tac x = s in allE)
- apply (erule_tac x = t in allE)
- apply (erule_tac x = na in allE)
- apply (erule_tac x = na in allE)
- apply (simp add: eq_sym_conv)
- done
-
-lemma W_var_geD: "Ok (s, t, m) = \ e a n \ n \ m"
- by (simp add: eq_sym_conv)
-
-lemma new_tv_W: "!!n a s t m.
- new_tv n a \ \ e a n = Ok (s, t, m) \ new_tv m s & new_tv m t"
- -- {* resulting type variable is new *}
- apply (atomize (full))
- apply (induct e)
- txt {* case @{text "Var n"} *}
- apply clarsimp
- apply (force elim: list_ball_nth simp add: id_subst_def new_tv_list new_tv_subst)
- txt {* case @{text "Abs e"} *}
- apply (simp (no_asm) add: new_tv_subst new_tv_Suc_list split add: split_bind)
- apply (intro strip)
- apply (erule_tac x = "Suc n" in allE)
- apply (erule_tac x = "TVar n # a" in allE)
- apply (fastsimp simp add: new_tv_subst new_tv_Suc_list)
- txt {* case @{text "App e1 e2"} *}
- apply (simp (no_asm) split add: split_bind)
- apply (intro strip)
- apply (rename_tac s t na sa ta nb sb)
- apply (erule_tac x = n in allE)
- apply (erule_tac x = a in allE)
- apply (erule_tac x = s in allE)
- apply (erule_tac x = t in allE)
- apply (erule_tac x = na in allE)
- apply (erule_tac x = na in allE)
- apply (simp add: eq_sym_conv)
- apply (erule_tac x = "$s a" in allE)
- apply (erule_tac x = sa in allE)
- apply (erule_tac x = ta in allE)
- apply (erule_tac x = nb in allE)
- apply (simp add: o_def rotate_Ok)
- apply (rule conjI)
- apply (rule new_tv_subst_comp_2)
- apply (rule new_tv_subst_comp_2)
- apply (rule lessI [THEN less_imp_le, THEN new_tv_subst_le])
- apply (rule_tac n = na in new_tv_subst_le)
- apply (simp add: rotate_Ok)
- apply (simp (no_asm_simp))
- apply (fast dest: W_var_geD intro: new_tv_list_le new_tv_subst_tel
- lessI [THEN less_imp_le, THEN new_tv_subst_le])
- apply (erule sym [THEN mgu_new])
- apply (best dest: W_var_geD intro: new_tv_subst_te new_tv_list_le new_tv_subst_tel
- lessI [THEN less_imp_le, THEN new_tv_le] lessI [THEN less_imp_le, THEN new_tv_subst_le]
- new_tv_le)
- apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
- addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
- addss @{simpset}) 1 *})
- apply (rule lessI [THEN new_tv_subst_var])
- apply (erule sym [THEN mgu_new])
- apply (bestsimp intro!: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te
- dest!: W_var_geD intro: new_tv_list_le new_tv_subst_tel
- lessI [THEN less_imp_le, THEN new_tv_subst_le] new_tv_le)
- apply (tactic {* fast_tac (HOL_cs addDs [thm "W_var_geD"]
- addIs [thm "new_tv_list_le", thm "new_tv_subst_tel", thm "new_tv_le"]
- addss @{simpset}) 1 *})
- done
-
-lemma free_tv_W: "!!n a s t m v. \ e a n = Ok (s, t, m) \
- (v \ free_tv s \ v \ free_tv t) \ v < n \ v \ free_tv a"
- apply (atomize (full))
- apply (induct e)
- txt {* case @{text "Var n"} *}
- apply clarsimp
- apply (tactic {* fast_tac (HOL_cs addIs [thm "nth_mem", subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *})
- txt {* case @{text "Abs e"} *}
- apply (simp add: free_tv_subst split add: split_bind)
- apply (intro strip)
- apply (rename_tac s t n1 v)
- apply (erule_tac x = "Suc n" in allE)
- apply (erule_tac x = "TVar n # a" in allE)
- apply (erule_tac x = s in allE)
- apply (erule_tac x = t in allE)
- apply (erule_tac x = n1 in allE)
- apply (erule_tac x = v in allE)
- apply (force elim!: allE intro: cod_app_subst)
- txt {* case @{text "App e1 e2"} *}
- apply (simp (no_asm) split add: split_bind)
- apply (intro strip)
- apply (rename_tac s t n1 s1 t1 n2 s3 v)
- apply (erule_tac x = n in allE)
- apply (erule_tac x = a in allE)
- apply (erule_tac x = s in allE)
- apply (erule_tac x = t in allE)
- apply (erule_tac x = n1 in allE)
- apply (erule_tac x = n1 in allE)
- apply (erule_tac x = v in allE)
- txt {* second case *}
- apply (erule_tac x = "$ s a" in allE)
- apply (erule_tac x = s1 in allE)
- apply (erule_tac x = t1 in allE)
- apply (erule_tac x = n2 in allE)
- apply (erule_tac x = v in allE)
- apply (tactic "safe_tac (empty_cs addSIs [conjI, impI] addSEs [conjE])")
- apply (simp add: rotate_Ok o_def)
- apply (drule W_var_geD)
- apply (drule W_var_geD)
- apply (frule less_le_trans, assumption)
- apply (fastsimp dest: free_tv_comp_subst [THEN subsetD] sym [THEN mgu_free] codD
- free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_tel [THEN subsetD] subsetD elim: UnE)
- apply simp
- apply (drule sym [THEN W_var_geD])
- apply (drule sym [THEN W_var_geD])
- apply (frule less_le_trans, assumption)
- apply (tactic {* fast_tac (HOL_cs addDs [thm "mgu_free", thm "codD",
- thm "free_tv_subst_var" RS subsetD,
- thm "free_tv_app_subst_te" RS subsetD,
- thm "free_tv_app_subst_tel" RS subsetD, @{thm less_le_trans}, subsetD]
- addSEs [UnE] addss (@{simpset} setSolver unsafe_solver)) 1 *})
- -- {* builtin arithmetic in simpset messes things up *}
- done
-
-text {*
- \medskip Completeness of @{text \} wrt.\ @{text has_type}.
-*}
-
-lemma W_complete_aux: "!!s' a t' n. $s' a |- e :: t' \ new_tv n a \
- (\s t. (\m. \ e a n = Ok (s, t, m)) \ (\r. $s' a = $r ($s a) \ t' = $r t))"
- apply (atomize (full))
- apply (induct e)
- txt {* case @{text "Var n"} *}
- apply (intro strip)
- apply (simp (no_asm) cong add: conj_cong)
- apply (erule has_type_casesE)
- apply (simp add: eq_sym_conv app_subst_list)
- apply (rule_tac x = s' in exI)
- apply simp
- txt {* case @{text "Abs e"} *}
- apply (intro strip)
- apply (erule has_type_casesE)
- apply (erule_tac x = "\x. if x = n then t1 else (s' x)" in allE)
- apply (erule_tac x = "TVar n # a" in allE)
- apply (erule_tac x = t2 in allE)
- apply (erule_tac x = "Suc n" in allE)
- apply (fastsimp cong add: conj_cong split add: split_bind)
- txt {* case @{text "App e1 e2"} *}
- apply (intro strip)
- apply (erule has_type_casesE)
- apply (erule_tac x = s' in allE)
- apply (erule_tac x = a in allE)
- apply (erule_tac x = "t2 -> t'" in allE)
- apply (erule_tac x = n in allE)
- apply (tactic "safe_tac HOL_cs")
- apply (erule_tac x = r in allE)
- apply (erule_tac x = "$s a" in allE)
- apply (erule_tac x = t2 in allE)
- apply (erule_tac x = m in allE)
- apply simp
- apply (tactic "safe_tac HOL_cs")
- apply (tactic {* fast_tac (HOL_cs addIs [sym RS thm "W_var_geD",
- thm "new_tv_W" RS conjunct1, thm "new_tv_list_le", thm "new_tv_subst_tel"]) 1 *})
- apply (subgoal_tac
- "$(\x. if x = ma then t' else (if x \ free_tv t - free_tv sa then r x
- else ra x)) ($ sa t) =
- $(\x. if x = ma then t' else (if x \ free_tv t - free_tv sa then r x
- else ra x)) (ta -> (TVar ma))")
- apply (rule_tac [2] t = "$(\x. if x = ma then t'
- else (if x \ (free_tv t - free_tv sa) then r x else ra x)) ($sa t)" and
- s = "($ ra ta) -> t'" in ssubst)
- prefer 2
- apply (simp add: subst_comp_te)
- apply (rule eq_free_eq_subst_te)
- apply (intro strip)
- apply (subgoal_tac "na \ ma")
- prefer 2
- apply (fast dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le)
- apply (case_tac "na \ free_tv sa")
- txt {* @{text "na \ free_tv sa"} *}
- prefer 2
- apply (frule not_free_impl_id)
- apply simp
- txt {* @{text "na \ free_tv sa"} *}
- apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans])
- apply (drule_tac eq_subst_tel_eq_free)
- apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
- apply simp
- apply (case_tac "na \ dom sa")
- prefer 2
- txt {* @{text "na \ dom sa"} *}
- apply (simp add: dom_def)
- txt {* @{text "na \ dom sa"} *}
- apply (rule eq_free_eq_subst_te)
- apply (intro strip)
- apply (subgoal_tac "nb \ ma")
- prefer 2
- apply (frule new_tv_W, assumption)
- apply (erule conjE)
- apply (drule new_tv_subst_tel)
- apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD])
- apply (fastsimp dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst)
- apply (fastsimp simp add: cod_def free_tv_subst)
- prefer 2
- apply (simp (no_asm))
- apply (rule eq_free_eq_subst_te)
- apply (intro strip)
- apply (subgoal_tac "na \ ma")
- prefer 2
- apply (frule new_tv_W, assumption)
- apply (erule conjE)
- apply (drule sym [THEN W_var_geD])
- apply (fast dest: new_tv_list_le new_tv_subst_tel new_tv_W new_tv_not_free_tv)
- apply (case_tac "na \ free_tv t - free_tv sa")
- prefer 2
- txt {* case @{text "na \ free_tv t - free_tv sa"} *}
- apply simp
- defer
- txt {* case @{text "na \ free_tv t - free_tv sa"} *}
- apply simp
- apply (drule_tac ts1 = "$s a" and r = "$ r ($ s a)" in subst_comp_tel [THEN [2] trans])
- apply (drule eq_subst_tel_eq_free)
- apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
- apply (simp add: free_tv_subst dom_def)
- prefer 2 apply fast
- apply (simp (no_asm_simp) split add: split_bind)
- apply (tactic "safe_tac HOL_cs")
- apply (drule mgu_Ok)
- apply fastsimp
- apply (drule mgu_mg, assumption)
- apply (erule exE)
- apply (rule_tac x = rb in exI)
- apply (rule conjI)
- prefer 2
- apply (drule_tac x = ma in fun_cong)
- apply (simp add: eq_sym_conv)
- apply (simp (no_asm) add: o_def subst_comp_tel [symmetric])
- apply (rule subst_comp_tel [symmetric, THEN [2] trans])
- apply (simp add: o_def eq_sym_conv)
- apply (rule eq_free_eq_subst_tel)
- apply (tactic "safe_tac HOL_cs")
- apply (subgoal_tac "ma \ na")
- prefer 2
- apply (frule new_tv_W, assumption)
- apply (erule conjE)
- apply (drule new_tv_subst_tel)
- apply (fast intro: new_tv_list_le dest: sym [THEN W_var_geD])
- apply (frule_tac n = m in new_tv_W, assumption)
- apply (erule conjE)
- apply (drule free_tv_app_subst_tel [THEN subsetD])
- apply (auto dest: W_var_geD [OF sym] new_tv_list_le
- codD new_tv_not_free_tv)
- apply (case_tac "na \ free_tv t - free_tv sa")
- prefer 2
- txt {* case @{text "na \ free_tv t - free_tv sa"} *}
- apply simp
- defer
- txt {* case @{text "na \ free_tv t - free_tv sa"} *}
- apply simp
- apply (drule free_tv_app_subst_tel [THEN subsetD])
- apply (fastsimp dest: codD subst_comp_tel [THEN [2] trans]
- eq_subst_tel_eq_free simp add: free_tv_subst dom_def)
- done
-
-lemma W_complete: "[] |- e :: t' ==>
- \s t. (\m. \ e [] n = Ok (s, t, m)) \ (\r. t' = $r t)"
- apply (cut_tac a = "[]" and s' = id_subst and e = e and t' = t' in W_complete_aux)
- apply simp_all
- done
-
-
-section {* Equivalence of W and I *}
-
-text {*
- Recursive definition of type inference algorithm @{text \} for
- Mini-ML.
-*}
-
-consts
- "\" :: "expr \ typ list \ nat \ subst \ (subst \ typ \ nat) maybe"
-primrec
- "\ (Var i) a n s = (if i < length a then Ok (s, a ! i, n) else Fail)"
- "\ (Abs e) a n s = ((s, t, m) := \ e (TVar n # a) (Suc n) s;
- Ok (s, TVar n -> t, m))"
- "\ (App e1 e2) a n s =
- ((s1, t1, m1) := \ e1 a n s;
- (s2, t2, m2) := \ e2 a m1 s1;
- u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
- Ok($u o s2, TVar m2, Suc m2))"
-
-text {* \medskip Correctness. *}
-
-lemma I_correct_wrt_W: "!!a m s s' t n.
- new_tv m a \ new_tv m s \ \ e a m s = Ok (s', t, n) \
- \r. \ e ($s a) m = Ok (r, $s' t, n) \ s' = ($r o s)"
- apply (atomize (full))
- apply (induct e)
- txt {* case @{text "Var n"} *}
- apply (simp add: app_subst_list split: split_if)
- txt {* case @{text "Abs e"} *}
- apply (tactic {* asm_full_simp_tac
- (@{simpset} setloop (split_inside_tac [thm "split_bind"])) 1 *})
- apply (intro strip)
- apply (rule conjI)
- apply (intro strip)
- apply (erule allE)+
- apply (erule impE)
- prefer 2 apply (fastsimp simp add: new_tv_subst)
- apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
- thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *})
- apply (intro strip)
- apply (erule allE)+
- apply (erule impE)
- prefer 2 apply (fastsimp simp add: new_tv_subst)
- apply (tactic {* fast_tac (HOL_cs addIs [thm "new_tv_Suc_list" RS mp,
- thm "new_tv_subst_le", @{thm less_imp_le}, @{thm lessI}]) 1 *})
- txt {* case @{text "App e1 e2"} *}
- apply (tactic {* simp_tac (@{simpset} setloop (split_inside_tac [thm "split_bind"])) 1 *})
- apply (intro strip)
- apply (rename_tac s1' t1 n1 s2' t2 n2 sa)
- apply (rule conjI)
- apply fastsimp
- apply (intro strip)
- apply (rename_tac s1 t1' n1')
- apply (erule_tac x = a in allE)
- apply (erule_tac x = m in allE)
- apply (erule_tac x = s in allE)
- apply (erule_tac x = s1' in allE)
- apply (erule_tac x = t1 in allE)
- apply (erule_tac x = n1 in allE)
- apply (erule_tac x = a in allE)
- apply (erule_tac x = n1 in allE)
- apply (erule_tac x = s1' in allE)
- apply (erule_tac x = s2' in allE)
- apply (erule_tac x = t2 in allE)
- apply (erule_tac x = n2 in allE)
- apply (rule conjI)
- apply (intro strip)
- apply (rule notI)
- apply simp
- apply (erule impE)
- apply (frule new_tv_subst_tel, assumption)
- apply (drule_tac a = "$s a" in new_tv_W, assumption)
- apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
- apply (fastsimp simp add: subst_comp_tel)
- apply (intro strip)
- apply (rename_tac s2 t2' n2')
- apply (rule conjI)
- apply (intro strip)
- apply (rule notI)
- apply simp
- apply (erule impE)
- apply (frule new_tv_subst_tel, assumption)
- apply (drule_tac a = "$s a" in new_tv_W, assumption)
- apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
- apply (fastsimp simp add: subst_comp_tel subst_comp_te)
- apply (intro strip)
- apply (erule (1) notE impE)
- apply (erule (1) notE impE)
- apply (erule exE)
- apply (erule conjE)
- apply (erule impE)
- apply (frule new_tv_subst_tel, assumption)
- apply (drule_tac a = "$s a" in new_tv_W, assumption)
- apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
- apply (erule (1) notE impE)
- apply (erule exE conjE)+
- apply (simp (asm_lr) add: subst_comp_tel subst_comp_te o_def, (erule conjE)+, hypsubst)+
- apply (subgoal_tac "new_tv n2 s \ new_tv n2 r \