# HG changeset patch
# User kleing
# Date 1080189452 -3600
# Node ID 82774ac788aef076dbdef2114928f04fb1c2f87a
# Parent ab1e47451aaa88689c6ab644733e0b7e4420209c
moved MiniML and AVL to archive of formal proofs
diff -r ab1e47451aaa -r 82774ac788ae src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile Wed Mar 24 10:55:38 2004 +0100
+++ b/src/HOL/IsaMakefile Thu Mar 25 05:37:32 2004 +0100
@@ -30,7 +30,6 @@
HOL-Lattice \
HOL-Lex \
HOL-MicroJava \
- HOL-MiniML \
HOL-Modelcheck \
HOL-NanoJava \
HOL-NumberTheory \
@@ -432,16 +431,6 @@
@$(ISATOOL) usedir $(OUT)/HOL W0
-## HOL-MiniML
-
-HOL-MiniML: HOL $(LOG)/HOL-MiniML.gz
-
-$(LOG)/HOL-MiniML.gz: $(OUT)/HOL MiniML/Generalize.thy\
- MiniML/Instance.thy MiniML/Maybe.thy MiniML/MiniML.thy \
- MiniML/ROOT.ML MiniML/Type.thy MiniML/W.thy
- @$(ISATOOL) usedir $(OUT)/HOL MiniML
-
-
## HOL-MicroJava
HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
@@ -559,7 +548,7 @@
HOL-ex: HOL $(LOG)/HOL-ex.gz
-$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/AVL.thy ex/Antiquote.thy \
+$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/Antiquote.thy \
ex/BT.thy ex/BinEx.thy ex/Group.ML ex/Group.thy ex/Higher_Order_Logic.thy \
ex/Hilbert_Classical.thy ex/InSort.thy ex/IntRing.ML \
ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy\
@@ -666,7 +655,6 @@
$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
- $(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
$(LOG)/HOL-Bali.gz $(LOG)/HOL-CTL.gz \
$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
diff -r ab1e47451aaa -r 82774ac788ae src/HOL/MiniML/Generalize.thy
--- a/src/HOL/MiniML/Generalize.thy Wed Mar 24 10:55:38 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,171 +0,0 @@
-(* Title: HOL/MiniML/Generalize.thy
- ID: $Id$
- Author: Wolfgang Naraschewski and Tobias Nipkow
- Copyright 1996 TU Muenchen
-
-Generalizing type schemes with respect to a context
-*)
-
-theory Generalize = Instance:
-
-
-(* gen: binding (generalising) the variables which are not free in the context *)
-
-types ctxt = "type_scheme list"
-
-consts
- gen :: "[ctxt, typ] => type_scheme"
-
-primrec
- "gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
- "gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)"
-
-(* executable version of gen: Implementation with free_tv_ML *)
-
-consts
- gen_ML_aux :: "[nat list, typ] => type_scheme"
-primrec
- "gen_ML_aux A (TVar n) = (if (n: set A) then (FVar n) else (BVar n))"
- "gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
-
-consts
- gen_ML :: "[ctxt, typ] => type_scheme"
-defs
- gen_ML_def: "gen_ML A t == gen_ML_aux (free_tv_ML A) t"
-
-
-declare equalityE [elim!]
-
-lemma gen_eq_on_free_tv: "free_tv A = free_tv B ==> gen A t = gen B t"
-apply (induct_tac "t")
-apply (simp_all (no_asm_simp))
-done
-
-lemma gen_without_effect [rule_format (no_asm)]: "(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)"
-apply (induct_tac "t")
-apply (simp (no_asm_simp))
-apply (simp (no_asm))
-apply fast
-done
-
-declare gen_without_effect [simp]
-
-lemma free_tv_gen: "free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)"
-apply (induct_tac "t")
-apply (simp (no_asm))
-apply (case_tac "nat : free_tv ($ S A) ")
-apply (simp (no_asm_simp))
-apply fast
-apply (simp (no_asm_simp))
-apply fast
-apply simp
-apply fast
-done
-
-declare free_tv_gen [simp]
-
-lemma free_tv_gen_cons: "free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)"
-apply (simp (no_asm))
-apply fast
-done
-
-declare free_tv_gen_cons [simp]
-
-lemma bound_tv_gen: "bound_tv (gen A t1) = (free_tv t1) - (free_tv A)"
-apply (induct_tac "t1")
-apply (simp (no_asm))
-apply (case_tac "nat : free_tv A")
-apply (simp (no_asm_simp))
-apply (simp (no_asm_simp))
-apply fast
-apply (simp (no_asm_simp))
-apply fast
-done
-
-declare bound_tv_gen [simp]
-
-lemma new_tv_compatible_gen [rule_format (no_asm)]: "new_tv n t --> new_tv n (gen A t)"
-apply (induct_tac "t")
-apply auto
-done
-
-lemma gen_eq_gen_ML: "gen A t = gen_ML A t"
-apply (unfold gen_ML_def)
-apply (induct_tac "t")
- apply (simp (no_asm) add: free_tv_ML_scheme_list)
-apply (simp (no_asm_simp) add: free_tv_ML_scheme_list)
-done
-
-lemma gen_subst_commutes [rule_format (no_asm)]: "(free_tv S) Int ((free_tv t) - (free_tv A)) = {}
- --> gen ($ S A) ($ S t) = $ S (gen A t)"
-apply (induct_tac "t")
- apply (intro strip)
- apply (case_tac "nat: (free_tv A) ")
- apply (simp (no_asm_simp))
- apply simp
- apply (subgoal_tac "nat ~: free_tv S")
- prefer 2 apply (fast)
- apply (simp add: free_tv_subst dom_def)
- apply (cut_tac free_tv_app_subst_scheme_list)
- apply fast
-apply (simp (no_asm_simp))
-apply blast
-done
-
-lemma bound_typ_inst_gen [rule_format (no_asm)]: "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t"
-apply (induct_tac "t")
-apply (simp_all (no_asm_simp))
-apply fast
-done
-declare bound_typ_inst_gen [simp]
-
-lemma gen_bound_typ_instance:
- "gen ($ S A) ($ S t) <= $ S (gen A t)"
-apply (unfold le_type_scheme_def is_bound_typ_instance)
-apply safe
-apply (rename_tac "R")
-apply (rule_tac x = " (%a. bound_typ_inst R (gen ($S A) (S a))) " in exI)
-apply (induct_tac "t")
- apply (simp (no_asm))
-apply (simp (no_asm_simp))
-done
-
-lemma free_tv_subset_gen_le:
- "free_tv B <= free_tv A ==> gen A t <= gen B t"
-apply (unfold le_type_scheme_def is_bound_typ_instance)
-apply safe
-apply (rename_tac "S")
-apply (rule_tac x = "%b. if b:free_tv A then TVar b else S b" in exI)
-apply (induct_tac "t")
- apply (simp (no_asm_simp))
- apply fast
-apply (simp (no_asm_simp))
-done
-
-lemma gen_t_le_gen_alpha_t [rule_format (no_asm)]:
- "new_tv n A -->
- gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)"
-apply (unfold le_type_scheme_def is_bound_typ_instance)
-apply (intro strip)
-apply (erule exE)
-apply (hypsubst)
-apply (rule_tac x = " (%x. S (if n <= x then x - n else x))" in exI)
-apply (induct_tac "t")
-apply (simp (no_asm))
-apply (case_tac "nat : free_tv A")
-apply (simp (no_asm_simp))
-apply (simp (no_asm_simp))
-apply (subgoal_tac "n <= n + nat")
-apply (frule_tac t = "A" in new_tv_le)
-apply assumption
-apply (drule new_tv_not_free_tv)
-apply (drule new_tv_not_free_tv)
-apply (simp (no_asm_simp) add: diff_add_inverse)
-apply (simp (no_asm) add: le_add1)
-apply (simp (no_asm_simp))
-done
-
-declare gen_t_le_gen_alpha_t [simp]
-
-
-end
diff -r ab1e47451aaa -r 82774ac788ae src/HOL/MiniML/Instance.thy
--- a/src/HOL/MiniML/Instance.thy Wed Mar 24 10:55:38 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,341 +0,0 @@
-(* Title: HOL/MiniML/Instance.thy
- ID: $Id$
- Author: Wolfgang Naraschewski and Tobias Nipkow
- Copyright 1996 TU Muenchen
-
-Instances of type schemes
-*)
-
-theory Instance = Type:
-
-
-(* generic instances of a type scheme *)
-
-consts
- bound_typ_inst :: "[subst, type_scheme] => typ"
-
-primrec
- "bound_typ_inst S (FVar n) = (TVar n)"
- "bound_typ_inst S (BVar n) = (S n)"
- "bound_typ_inst S (sch1 =-> sch2) = ((bound_typ_inst S sch1) -> (bound_typ_inst S sch2))"
-
-consts
- bound_scheme_inst :: "[nat => type_scheme, type_scheme] => type_scheme"
-
-primrec
- "bound_scheme_inst S (FVar n) = (FVar n)"
- "bound_scheme_inst S (BVar n) = (S n)"
- "bound_scheme_inst S (sch1 =-> sch2) = ((bound_scheme_inst S sch1) =-> (bound_scheme_inst S sch2))"
-
-consts
- "<|" :: "[typ, type_scheme] => bool" (infixr 70)
-defs
- is_bound_typ_instance: "t <| sch == ? S. t = (bound_typ_inst S sch)"
-
-instance type_scheme :: ord ..
-defs le_type_scheme_def: "sch' <= (sch::type_scheme) == !t. t <| sch' --> t <| sch"
-
-consts
- subst_to_scheme :: "[nat => type_scheme, typ] => type_scheme"
-
-primrec
- "subst_to_scheme B (TVar n) = (B n)"
- "subst_to_scheme B (t1 -> t2) = ((subst_to_scheme B t1) =-> (subst_to_scheme B t2))"
-
-instance list :: (ord)ord ..
-defs le_env_def:
- "A <= B == length B = length A & (!i. i < length A --> A!i <= B!i)"
-
-
-(* lemmatas for instatiation *)
-
-
-(* lemmatas for bound_typ_inst *)
-
-lemma bound_typ_inst_mk_scheme: "bound_typ_inst S (mk_scheme t) = t"
-apply (induct_tac "t")
-apply (simp_all (no_asm_simp))
-done
-
-declare bound_typ_inst_mk_scheme [simp]
-
-lemma bound_typ_inst_composed_subst: "bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)"
-apply (induct_tac "sch")
-apply simp_all
-done
-
-declare bound_typ_inst_composed_subst [simp]
-
-lemma bound_typ_inst_eq: "S = S' ==> sch = sch' ==> bound_typ_inst S sch = bound_typ_inst S' sch'"
-apply simp
-done
-
-
-
-(* lemmatas for bound_scheme_inst *)
-
-lemma bound_scheme_inst_mk_scheme: "bound_scheme_inst B (mk_scheme t) = mk_scheme t"
-apply (induct_tac "t")
-apply (simp (no_asm))
-apply (simp (no_asm_simp))
-done
-
-declare bound_scheme_inst_mk_scheme [simp]
-
-lemma substitution_lemma: "$S (bound_scheme_inst B sch) = (bound_scheme_inst ($S o B) ($ S sch))"
-apply (induct_tac "sch")
-apply (simp (no_asm))
-apply (simp (no_asm))
-apply (simp (no_asm_simp))
-done
-
-lemma bound_scheme_inst_type [rule_format (no_asm)]: "!t. mk_scheme t = bound_scheme_inst B sch -->
- (? S. !x:bound_tv sch. B x = mk_scheme (S x))"
-apply (induct_tac "sch")
-apply (simp (no_asm))
-apply safe
-apply (rule exI)
-apply (rule ballI)
-apply (rule sym)
-apply simp
-apply simp
-apply (drule mk_scheme_Fun)
-apply (erule exE)+
-apply (erule conjE)
-apply (drule sym)
-apply (drule sym)
-apply (drule mp, fast)+
-apply safe
-apply (rename_tac S1 S2)
-apply (rule_tac x = "%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x) " in exI)
-apply auto
-done
-
-
-(* lemmas for subst_to_scheme *)
-
-lemma subst_to_scheme_inverse [rule_format (no_asm)]: "new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)
- (bound_typ_inst (%k. TVar (k + n)) sch) = sch"
-apply (induct_tac "sch")
-apply (simp (no_asm) add: le_def)
-apply (simp (no_asm) add: le_add2 diff_add_inverse2)
-apply (simp (no_asm_simp))
-done
-
-lemma aux: "t = t' ==>
- subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t =
- subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t'"
-apply fast
-done
-
-lemma aux2 [rule_format]: "new_tv n sch -->
- subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) =
- bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch"
-apply (induct_tac "sch")
-apply auto
-done
-
-
-(* lemmata for <= *)
-
-lemma le_type_scheme_def2:
- "!!(sch::type_scheme) sch'.
- (sch' <= sch) = (? B. sch' = bound_scheme_inst B sch)"
-
-apply (unfold le_type_scheme_def is_bound_typ_instance)
-apply (rule iffI)
-apply (cut_tac sch = "sch" in fresh_variable_type_schemes)
-apply (cut_tac sch = "sch'" in fresh_variable_type_schemes)
-apply (drule make_one_new_out_of_two)
-apply assumption
-apply (erule_tac V = "? n. new_tv n sch'" in thin_rl)
-apply (erule exE)
-apply (erule allE)
-apply (drule mp)
-apply (rule_tac x = " (%k. TVar (k + n))" in exI)
-apply (rule refl)
-apply (erule exE)
-apply (erule conjE)+
-apply (drule_tac n = "n" in aux)
-apply (simp add: subst_to_scheme_inverse)
-apply (rule_tac x = " (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S" in exI)
-apply (simp (no_asm_simp) add: aux2)
-apply safe
-apply (rule_tac x = "%n. bound_typ_inst S (B n) " in exI)
-apply (induct_tac "sch")
-apply (simp (no_asm))
-apply (simp (no_asm))
-apply (simp (no_asm_simp))
-done
-
-lemma le_type_eq_is_bound_typ_instance [rule_format (no_asm)]: "(mk_scheme t) <= sch = t <| sch"
-apply (unfold is_bound_typ_instance)
-apply (simp (no_asm) add: le_type_scheme_def2)
-apply (rule iffI)
-apply (erule exE)
-apply (frule bound_scheme_inst_type)
-apply (erule exE)
-apply (rule exI)
-apply (rule mk_scheme_injective)
-apply simp
-apply (rotate_tac 1)
-apply (rule mp)
-prefer 2 apply (assumption)
-apply (induct_tac "sch")
-apply (simp (no_asm))
-apply simp
-apply fast
-apply (intro strip)
-apply simp
-apply (erule exE)
-apply simp
-apply (rule exI)
-apply (induct_tac "sch")
-apply (simp (no_asm))
-apply (simp (no_asm))
-apply simp
-done
-
-lemma le_env_Cons:
- "(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)"
-apply (unfold le_env_def)
-apply (simp (no_asm))
-apply (rule iffI)
- apply clarify
- apply (rule conjI)
- apply (erule_tac x = "0" in allE)
- apply simp
- apply (rule conjI, assumption)
- apply clarify
- apply (erule_tac x = "Suc i" in allE)
- apply simp
-apply (rule conjI)
- apply fast
-apply (rule allI)
-apply (induct_tac "i")
-apply (simp_all (no_asm_simp))
-done
-declare le_env_Cons [iff]
-
-lemma is_bound_typ_instance_closed_subst: "t <| sch ==> $S t <| $S sch"
-apply (unfold is_bound_typ_instance)
-apply (erule exE)
-apply (rename_tac "SA")
-apply (simp)
-apply (rule_tac x = "$S o SA" in exI)
-apply (simp (no_asm))
-done
-
-lemma S_compatible_le_scheme: "!!(sch::type_scheme) sch'. sch' <= sch ==> $S sch' <= $ S sch"
-apply (simp add: le_type_scheme_def2)
-apply (erule exE)
-apply (simp add: substitution_lemma)
-apply fast
-done
-
-lemma S_compatible_le_scheme_lists:
- "!!(A::type_scheme list) A'. A' <= A ==> $S A' <= $ S A"
-apply (unfold le_env_def app_subst_list)
-apply (simp (no_asm) cong add: conj_cong)
-apply (fast intro!: S_compatible_le_scheme)
-done
-
-lemma bound_typ_instance_trans: "[| t <| sch; sch <= sch' |] ==> t <| sch'"
-apply (unfold le_type_scheme_def)
-apply fast
-done
-
-lemma le_type_scheme_refl: "sch <= (sch::type_scheme)"
-apply (unfold le_type_scheme_def)
-apply fast
-done
-declare le_type_scheme_refl [iff]
-
-lemma le_env_refl: "A <= (A::type_scheme list)"
-apply (unfold le_env_def)
-apply fast
-done
-declare le_env_refl [iff]
-
-lemma bound_typ_instance_BVar: "sch <= BVar n"
-apply (unfold le_type_scheme_def is_bound_typ_instance)
-apply (intro strip)
-apply (rule_tac x = "%a. t" in exI)
-apply (simp (no_asm))
-done
-declare bound_typ_instance_BVar [iff]
-
-lemma le_FVar:
- "(sch <= FVar n) = (sch = FVar n)"
-apply (unfold le_type_scheme_def is_bound_typ_instance)
-apply (induct_tac "sch")
- apply (simp (no_asm))
- apply (simp (no_asm))
- apply fast
-apply simp
-apply fast
-done
-declare le_FVar [simp]
-
-lemma not_FVar_le_Fun: "~(FVar n <= sch1 =-> sch2)"
-apply (unfold le_type_scheme_def is_bound_typ_instance)
-apply (simp (no_asm))
-done
-declare not_FVar_le_Fun [iff]
-
-lemma not_BVar_le_Fun: "~(BVar n <= sch1 =-> sch2)"
-apply (unfold le_type_scheme_def is_bound_typ_instance)
-apply (simp (no_asm))
-apply (rule_tac x = "TVar n" in exI)
-apply (simp (no_asm))
-apply fast
-done
-declare not_BVar_le_Fun [iff]
-
-lemma Fun_le_FunD:
- "(sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'"
-apply (unfold le_type_scheme_def is_bound_typ_instance)
-apply (fastsimp)
-done
-
-lemma scheme_le_Fun [rule_format (no_asm)]: "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)"
-apply (induct_tac "sch'")
-apply (simp (no_asm_simp))
-apply (simp (no_asm_simp))
-apply fast
-done
-
-lemma le_type_scheme_free_tv [rule_format (no_asm)]: "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch"
-apply (induct_tac "sch")
- apply (rule allI)
- apply (induct_tac "sch'")
- apply (simp (no_asm))
- apply (simp (no_asm))
- apply (simp (no_asm))
- apply (rule allI)
- apply (induct_tac "sch'")
- apply (simp (no_asm))
- apply (simp (no_asm))
- apply (simp (no_asm))
-apply (rule allI)
-apply (induct_tac "sch'")
- apply (simp (no_asm))
- apply (simp (no_asm))
-apply simp
-apply (intro strip)
-apply (drule Fun_le_FunD)
-apply fast
-done
-
-lemma le_env_free_tv [rule_format (no_asm)]: "!A::type_scheme list. A <= B --> free_tv B <= free_tv A"
-apply (induct_tac "B")
- apply (simp (no_asm))
-apply (rule allI)
-apply (induct_tac "A")
- apply (simp (no_asm) add: le_env_def)
-apply (simp (no_asm))
-apply (fast dest: le_type_scheme_free_tv)
-done
-
-
-end
diff -r ab1e47451aaa -r 82774ac788ae src/HOL/MiniML/Maybe.thy
--- a/src/HOL/MiniML/Maybe.thy Wed Mar 24 10:55:38 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-(* Title: HOL/MiniML/Maybe.thy
- ID: $Id$
- Author: Wolfgang Naraschewski and Tobias Nipkow
- Copyright 1996 TU Muenchen
-
-Universal error monad.
-*)
-
-theory Maybe = Main:
-
-constdefs
- option_bind :: "['a option, 'a => 'b option] => 'b option"
- "option_bind m f == case m of None => None | Some r => f r"
-
-syntax "@option_bind" :: "[pttrns,'a option,'b] => 'c" ("(_ := _;//_)" 0)
-translations "P := E; F" == "option_bind E (%P. F)"
-
-
-(* constructor laws for option_bind *)
-lemma option_bind_Some: "option_bind (Some s) f = (f s)"
-apply (unfold option_bind_def)
-apply (simp (no_asm))
-done
-
-lemma option_bind_None: "option_bind None f = None"
-apply (unfold option_bind_def)
-apply (simp (no_asm))
-done
-
-declare option_bind_Some [simp] option_bind_None [simp]
-
-(* expansion of option_bind *)
-lemma split_option_bind: "P(option_bind res f) =
- ((res = None --> P None) & (!s. res = Some s --> P(f s)))"
-apply (unfold option_bind_def)
-apply (rule option.split)
-done
-
-lemma option_bind_eq_None:
- "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))"
-apply (simp (no_asm) split add: split_option_bind)
-done
-
-declare option_bind_eq_None [simp]
-
-(* auxiliary lemma *)
-lemma rotate_Some: "(y = Some x) = (Some x = y)"
-apply ( simp (no_asm) add: eq_sym_conv)
-done
-
-end
diff -r ab1e47451aaa -r 82774ac788ae src/HOL/MiniML/MiniML.thy
--- a/src/HOL/MiniML/MiniML.thy Wed Mar 24 10:55:38 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,271 +0,0 @@
-(* Title: HOL/MiniML/MiniML.thy
- ID: $Id$
- Author: Dieter Nazareth, Wolfgang Naraschewski and Tobias Nipkow
- Copyright 1996 TU Muenchen
-
-Mini_ML with type inference rules.
-*)
-
-theory MiniML = Generalize:
-
-(* expressions *)
-datatype
- expr = Var nat | Abs expr | App expr expr | LET expr expr
-
-(* type inference rules *)
-consts
- has_type :: "(ctxt * expr * typ)set"
-syntax
- "@has_type" :: "[ctxt, expr, typ] => bool"
- ("((_) |-/ (_) :: (_))" [60,0,60] 60)
-translations
- "A |- e :: t" == "(A,e,t):has_type"
-
-inductive has_type
-intros
- VarI: "[| n < length A; t <| A!n |] ==> A |- Var n :: t"
- AbsI: "[| (mk_scheme t1)#A |- e :: t2 |] ==> A |- Abs e :: t1 -> t2"
- AppI: "[| A |- e1 :: t2 -> t1; A |- e2 :: t2 |]
- ==> A |- App e1 e2 :: t1"
- LETI: "[| A |- e1 :: t1; (gen A t1)#A |- e2 :: t |] ==> A |- LET e1 e2 :: t"
-
-
-declare has_type.intros [simp]
-declare Un_upper1 [simp] Un_upper2 [simp]
-
-declare is_bound_typ_instance_closed_subst [simp]
-
-
-lemma s'_t_equals_s_t: "!!t::typ. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) t = $S t"
-apply (rule typ_substitutions_only_on_free_variables)
-apply (simp add: Ball_def)
-done
-
-declare s'_t_equals_s_t [simp]
-
-lemma s'_a_equals_s_a: "!!A::type_scheme list. $(%n. if n : (free_tv A) Un (free_tv t) then (S n) else (TVar n)) A = $S A"
-apply (rule scheme_list_substitutions_only_on_free_variables)
-apply (simp add: Ball_def)
-done
-
-declare s'_a_equals_s_a [simp]
-
-lemma replace_s_by_s':
- "$(%n. if n : (free_tv A) Un (free_tv t) then S n else TVar n) A |-
- e :: $(%n. if n : (free_tv A) Un (free_tv t) then S n else TVar n) t
- ==> $S A |- e :: $S t"
-
-apply (rule_tac P = "%A. A |- e :: $S t" in ssubst)
-apply (rule s'_a_equals_s_a [symmetric])
-apply (rule_tac P = "%t. $ (%n. if n : free_tv A Un free_tv (?t1 S) then S n else TVar n) A |- e :: t" in ssubst)
-apply (rule s'_t_equals_s_t [symmetric])
-apply simp
-done
-
-lemma alpha_A': "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = $ id_subst A"
-apply (rule scheme_list_substitutions_only_on_free_variables)
-apply (simp add: id_subst_def)
-done
-
-lemma alpha_A: "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = A"
-apply (rule alpha_A' [THEN ssubst])
-apply simp
-done
-
-lemma S_o_alpha_typ: "$ (S o alpha) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)"
-apply (induct_tac "t")
-apply (simp_all)
-done
-
-lemma S_o_alpha_typ': "$ (%u. (S o alpha) u) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)"
-apply (induct_tac "t")
-apply (simp_all)
-done
-
-lemma S_o_alpha_type_scheme: "$ (S o alpha) (sch::type_scheme) = $ S ($ (%x. TVar (alpha x)) sch)"
-apply (induct_tac "sch")
-apply (simp_all)
-done
-
-lemma S_o_alpha_type_scheme_list: "$ (S o alpha) (A::type_scheme list) = $ S ($ (%x. TVar (alpha x)) A)"
-apply (induct_tac "A")
-apply (simp_all)
-apply (rule S_o_alpha_type_scheme [unfolded o_def])
-done
-
-lemma S'_A_eq_S'_alpha_A: "!!A::type_scheme list.
- $ (%n. if n : free_tv A Un free_tv t then S n else TVar n) A =
- $ ((%x. if x : free_tv A Un free_tv t then S x else TVar x) o
- (%x. if x : free_tv A then x else n + x)) A"
-apply (subst S_o_alpha_type_scheme_list)
-apply (subst alpha_A)
-apply (rule refl)
-done
-
-lemma dom_S':
- "dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <=
- free_tv A Un free_tv t"
-apply (unfold free_tv_subst dom_def)
-apply (simp (no_asm))
-apply fast
-done
-
-lemma cod_S':
- "!!(A::type_scheme list) (t::typ).
- cod (%n. if n : free_tv A Un free_tv t then S n else TVar n) <=
- free_tv ($ S A) Un free_tv ($ S t)"
-apply (unfold free_tv_subst cod_def subset_def)
-apply (rule ballI)
-apply (erule UN_E)
-apply (drule dom_S' [THEN subsetD])
-apply simp
-apply (fast dest: free_tv_of_substitutions_extend_to_scheme_lists intro: free_tv_of_substitutions_extend_to_types [THEN subsetD])
-done
-
-lemma free_tv_S':
- "!!(A::type_scheme list) (t::typ).
- free_tv (%n. if n : free_tv A Un free_tv t then S n else TVar n) <=
- free_tv A Un free_tv ($ S A) Un free_tv t Un free_tv ($ S t)"
-apply (unfold free_tv_subst)
-apply (fast dest: dom_S' [THEN subsetD] cod_S' [THEN subsetD])
-done
-
-lemma free_tv_alpha: "!!t1::typ.
- (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <=
- {x. ? y. x = n + y}"
-apply (induct_tac "t1")
-apply (simp (no_asm))
-apply fast
-apply (simp (no_asm))
-apply fast
-done
-
-lemma aux_plus: "!!(k::nat). n <= n + k"
-apply (induct_tac "k" rule: nat_induct)
-apply (simp (no_asm))
-apply (simp (no_asm_simp))
-done
-
-declare aux_plus [simp]
-
-lemma new_tv_Int_free_tv_empty_type: "!!t::typ. new_tv n t ==> {x. ? y. x = n + y} Int free_tv t = {}"
-apply safe
-apply (cut_tac aux_plus)
-apply (drule new_tv_le)
-apply assumption
-apply (rotate_tac 1)
-apply (drule new_tv_not_free_tv)
-apply fast
-done
-
-lemma new_tv_Int_free_tv_empty_scheme: "!!sch::type_scheme. new_tv n sch ==> {x. ? y. x = n + y} Int free_tv sch = {}"
-apply safe
-apply (cut_tac aux_plus)
-apply (drule new_tv_le)
-apply assumption
-apply (rotate_tac 1)
-apply (drule new_tv_not_free_tv)
-apply fast
-done
-
-lemma new_tv_Int_free_tv_empty_scheme_list: "!A::type_scheme list. new_tv n A --> {x. ? y. x = n + y} Int free_tv A = {}"
-apply (rule allI)
-apply (induct_tac "A")
-apply (simp (no_asm))
-apply (simp (no_asm))
-apply (fast dest: new_tv_Int_free_tv_empty_scheme)
-done
-
-lemma gen_t_le_gen_alpha_t [rule_format (no_asm)]:
- "new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)"
-apply (unfold le_type_scheme_def is_bound_typ_instance)
-apply (intro strip)
-apply (erule exE)
-apply (hypsubst)
-apply (rule_tac x = " (%x. S (if n <= x then x - n else x))" in exI)
-apply (induct_tac "t")
-apply (simp (no_asm))
-apply (case_tac "nat : free_tv A")
-apply (simp (no_asm_simp))
-apply (subgoal_tac "n <= n + nat")
-apply (drule new_tv_le)
-apply assumption
-apply (drule new_tv_not_free_tv)
-apply (drule new_tv_not_free_tv)
-apply (simp (no_asm_simp) add: diff_add_inverse)
-apply (simp (no_asm))
-apply (simp (no_asm_simp))
-done
-
-declare has_type.intros [intro!]
-
-lemma has_type_le_env [rule_format (no_asm)]: "A |- e::t ==> !B. A <= B --> B |- e::t"
-apply (erule has_type.induct)
- apply (simp (no_asm) add: le_env_def)
- apply (fastsimp elim: bound_typ_instance_trans)
- apply simp
- apply fast
-apply (slow elim: le_env_free_tv [THEN free_tv_subset_gen_le])
-done
-
-(* has_type is closed w.r.t. substitution *)
-lemma has_type_cl_sub: "A |- e :: t ==> !S. $S A |- e :: $S t"
-apply (erule has_type.induct)
-(* case VarI *)
- apply (rule allI)
- apply (rule has_type.VarI)
- apply (simp add: app_subst_list)
- apply (simp (no_asm_simp) add: app_subst_list)
- (* case AbsI *)
- apply (rule allI)
- apply (simp (no_asm))
- apply (rule has_type.AbsI)
- apply simp
- (* case AppI *)
- apply (rule allI)
- apply (rule has_type.AppI)
- apply simp
- apply (erule spec)
- apply (erule spec)
-(* case LetI *)
-apply (rule allI)
-apply (rule replace_s_by_s')
-apply (cut_tac A = "$ S A" and A' = "A" and t = "t" and t' = "$ S t" in ex_fresh_variable)
-apply (erule exE)
-apply (erule conjE)+
-apply (rule_tac ?t1.0 = "$ ((%x. if x : free_tv A Un free_tv t then S x else TVar x) o (%x. if x : free_tv A then x else n + x)) t1" in has_type.LETI)
- apply (drule_tac x = " (%x. if x : free_tv A Un free_tv t then S x else TVar x) o (%x. if x : free_tv A then x else n + x) " in spec)
- apply (subst S'_A_eq_S'_alpha_A)
- apply assumption
-apply (subst S_o_alpha_typ)
-apply (subst gen_subst_commutes)
- apply (rule subset_antisym)
- apply (rule subsetI)
- apply (erule IntE)
- apply (drule free_tv_S' [THEN subsetD])
- apply (drule free_tv_alpha [THEN subsetD])
- apply (simp del: full_SetCompr_eq)
- apply (erule exE)
- apply (hypsubst)
- apply (subgoal_tac "new_tv (n + y) ($ S A) ")
- apply (subgoal_tac "new_tv (n + y) ($ S t) ")
- apply (subgoal_tac "new_tv (n + y) A")
- apply (subgoal_tac "new_tv (n + y) t")
- apply (drule new_tv_not_free_tv)+
- apply fast
- apply (rule new_tv_le) prefer 2 apply assumption apply simp
- apply (rule new_tv_le) prefer 2 apply assumption apply simp
- apply (rule new_tv_le) prefer 2 apply assumption apply simp
- apply (rule new_tv_le) prefer 2 apply assumption apply simp
- apply fast
-apply (rule has_type_le_env)
- apply (drule spec)
- apply (drule spec)
- apply assumption
-apply (rule app_subst_Cons [THEN subst])
-apply (rule S_compatible_le_scheme_lists)
-apply (simp (no_asm_simp))
-done
-
-
-end
diff -r ab1e47451aaa -r 82774ac788ae src/HOL/MiniML/README.html
--- a/src/HOL/MiniML/README.html Wed Mar 24 10:55:38 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-HOL/MiniML/README
-
-
-Type Inference for MiniML
-
-This theory defines the type inference rules and the type inference algorithm
-W for MiniML (simply-typed lambda terms with let) due to
-Milner. It proves the soundness and completeness of W w.r.t. the
-rules.
-
-
-
-A report describing the theory is found here:
-
-Type Inference Verified: Algorithm W in Isabelle/HOL.
-
-
-
diff -r ab1e47451aaa -r 82774ac788ae src/HOL/MiniML/ROOT.ML
--- a/src/HOL/MiniML/ROOT.ML Wed Mar 24 10:55:38 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-(* Title: HOL/MiniML/ROOT.ML
- ID: $Id$
- Author: Wolfgang Naraschewski and Tobias Nipkow
- Copyright 1995 TUM
-
-Type inference for MiniML
-*)
-
-time_use_thy "W";
diff -r ab1e47451aaa -r 82774ac788ae src/HOL/MiniML/Type.thy
--- a/src/HOL/MiniML/Type.thy Wed Mar 24 10:55:38 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,918 +0,0 @@
-(* Title: HOL/MiniML/Type.thy
- ID: $Id$
- Author: Wolfgang Naraschewski and Tobias Nipkow
- Copyright 1996 TU Muenchen
-
-MiniML-types and type substitutions.
-*)
-
-theory Type = Maybe:
-
-(* new class for structures containing type variables *)
-axclass type_struct < type
-
-
-(* type expressions *)
-datatype "typ" = TVar nat | "->" "typ" "typ" (infixr 70)
-
-(* type schemata *)
-datatype type_scheme = FVar nat | BVar nat | "=->" type_scheme type_scheme (infixr 70)
-
-
-(* embedding types into type schemata *)
-consts
- mk_scheme :: "typ => type_scheme"
-
-primrec
- "mk_scheme (TVar n) = (FVar n)"
- "mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))"
-
-
-instance "typ"::type_struct ..
-instance type_scheme::type_struct ..
-instance list::(type_struct)type_struct ..
-instance fun::(type,type_struct)type_struct ..
-
-
-(* free_tv s: the type variables occuring freely in the type structure s *)
-
-consts
- free_tv :: "['a::type_struct] => nat set"
-
-primrec (free_tv_typ)
- free_tv_TVar: "free_tv (TVar m) = {m}"
- free_tv_Fun: "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
-
-primrec (free_tv_type_scheme)
- "free_tv (FVar m) = {m}"
- "free_tv (BVar m) = {}"
- "free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)"
-
-primrec (free_tv_list)
- "free_tv [] = {}"
- "free_tv (x#l) = (free_tv x) Un (free_tv l)"
-
-
-(* executable version of free_tv: Implementation with lists *)
-consts
- free_tv_ML :: "['a::type_struct] => nat list"
-
-primrec (free_tv_ML_type_scheme)
- "free_tv_ML (FVar m) = [m]"
- "free_tv_ML (BVar m) = []"
- "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"
-
-primrec (free_tv_ML_list)
- "free_tv_ML [] = []"
- "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"
-
-
-(* new_tv s n computes whether n is a new type variable w.r.t. a type
- structure s, i.e. whether n is greater than any type variable
- occuring in the type structure *)
-constdefs
- new_tv :: "[nat,'a::type_struct] => bool"
- "new_tv n ts == ! m. m:(free_tv ts) --> m nat set"
-
-primrec (bound_tv_type_scheme)
- "bound_tv (FVar m) = {}"
- "bound_tv (BVar m) = {m}"
- "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"
-
-primrec (bound_tv_list)
- "bound_tv [] = {}"
- "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"
-
-
-(* minimal new free / bound variable *)
-
-consts
- min_new_bound_tv :: "'a::type_struct => nat"
-
-primrec (min_new_bound_tv_type_scheme)
- "min_new_bound_tv (FVar n) = 0"
- "min_new_bound_tv (BVar n) = Suc n"
- "min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)"
-
-
-(* substitutions *)
-
-(* type variable substitution *)
-types
- subst = "nat => typ"
-
-(* identity *)
-constdefs
- id_subst :: subst
- "id_subst == (%n. TVar n)"
-
-(* extension of substitution to type structures *)
-consts
- app_subst :: "[subst, 'a::type_struct] => 'a::type_struct" ("$")
-
-primrec (app_subst_typ)
- app_subst_TVar: "$ S (TVar n) = S n"
- app_subst_Fun: "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)"
-
-primrec (app_subst_type_scheme)
- "$ S (FVar n) = mk_scheme (S n)"
- "$ S (BVar n) = (BVar n)"
- "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"
-
-defs
- app_subst_list: "$ S == map ($ S)"
-
-(* domain of a substitution *)
-constdefs
- dom :: "subst => nat set"
- "dom S == {n. S n ~= TVar n}"
-
-(* codomain of a substitution: the introduced variables *)
-
-constdefs
- cod :: "subst => nat set"
- "cod S == (UN m:dom S. (free_tv (S m)))"
-
-defs
- free_tv_subst: "free_tv S == (dom S) Un (cod S)"
-
-
-(* unification algorithm mgu *)
-consts
- mgu :: "[typ,typ] => subst option"
-axioms
- mgu_eq: "mgu t1 t2 = Some U ==> $U t1 = $U t2"
- mgu_mg: "[| (mgu t1 t2) = Some U; $S t1 = $S t2 |] ==> ? R. S = $R o U"
- mgu_Some: "$S t1 = $S t2 ==> ? U. mgu t1 t2 = Some U"
- mgu_free: "mgu t1 t2 = Some U ==> (free_tv U) <= (free_tv t1) Un (free_tv t2)"
-
-
-declare mgu_eq [simp] mgu_mg [simp] mgu_free [simp]
-
-
-(* lemmata for make scheme *)
-
-lemma mk_scheme_Fun [rule_format (no_asm)]: "mk_scheme t = sch1 =-> sch2 --> (? t1 t2. sch1 = mk_scheme t1 & sch2 = mk_scheme t2)"
-apply (induct_tac "t")
-apply (simp (no_asm))
-apply simp
-apply fast
-done
-
-lemma mk_scheme_injective [rule_format (no_asm)]: "!t'. mk_scheme t = mk_scheme t' --> t=t'"
-apply (induct_tac "t")
- apply (rule allI)
- apply (induct_tac "t'")
- apply (simp (no_asm))
- apply simp
-apply (rule allI)
-apply (induct_tac "t'")
- apply (simp (no_asm))
-apply simp
-done
-
-lemma free_tv_mk_scheme: "free_tv (mk_scheme t) = free_tv t"
-apply (induct_tac "t")
-apply (simp_all (no_asm_simp))
-done
-
-declare free_tv_mk_scheme [simp]
-
-lemma subst_mk_scheme: "$ S (mk_scheme t) = mk_scheme ($ S t)"
-apply (induct_tac "t")
-apply (simp_all (no_asm_simp))
-done
-
-declare subst_mk_scheme [simp]
-
-
-(* constructor laws for app_subst *)
-
-lemma app_subst_Nil:
- "$ S [] = []"
-
-apply (unfold app_subst_list)
-apply (simp (no_asm))
-done
-
-lemma app_subst_Cons:
- "$ S (x#l) = ($ S x)#($ S l)"
-apply (unfold app_subst_list)
-apply (simp (no_asm))
-done
-
-declare app_subst_Nil [simp] app_subst_Cons [simp]
-
-
-(* constructor laws for new_tv *)
-
-lemma new_tv_TVar:
- "new_tv n (TVar m) = (m t2) = (new_tv n t1 & new_tv n t2)"
-apply (unfold new_tv_def)
-apply (fastsimp)
-done
-
-lemma new_tv_Fun2:
- "new_tv n (t1 =-> t2) = (new_tv n t1 & new_tv n t2)"
-apply (unfold new_tv_def)
-apply (fastsimp)
-done
-
-lemma new_tv_Nil:
- "new_tv n []"
-apply (unfold new_tv_def)
-apply (simp (no_asm))
-done
-
-lemma new_tv_Cons:
- "new_tv n (x#l) = (new_tv n x & new_tv n l)"
-apply (unfold new_tv_def)
-apply (fastsimp)
-done
-
-lemma new_tv_TVar_subst: "new_tv n TVar"
-apply (unfold new_tv_def)
-apply (intro strip)
-apply (simp add: free_tv_subst dom_def cod_def)
-done
-
-declare new_tv_TVar [simp] new_tv_FVar [simp] new_tv_BVar [simp] new_tv_Fun [simp] new_tv_Fun2 [simp] new_tv_Nil [simp] new_tv_Cons [simp] new_tv_TVar_subst [simp]
-
-lemma new_tv_id_subst:
- "new_tv n id_subst"
-apply (unfold id_subst_def new_tv_def free_tv_subst dom_def cod_def)
-apply (simp (no_asm))
-done
-declare new_tv_id_subst [simp]
-
-lemma new_if_subst_type_scheme: "new_tv n (sch::type_scheme) -->
- $(%k. if k
- $(%k. if k x : free_tv (A!n) --> x : free_tv A"
-apply (induct_tac "A")
-apply simp
-apply (rule allI)
-apply (induct_tac "n" rule: nat_induct)
-apply simp
-apply simp
-done
-
-declare free_tv_nth_A_impl_free_tv_A [simp]
-
-lemma free_tv_nth_nat_A [rule_format (no_asm)]: "!nat. nat < length A --> x : free_tv (A!nat) --> x : free_tv A"
-apply (induct_tac "A")
-apply simp
-apply (rule allI)
-apply (induct_tac "nat" rule: nat_induct)
-apply (intro strip)
-apply simp
-apply (simp (no_asm))
-done
-
-
-(* 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 typ_substitutions_only_on_free_variables [rule_format (no_asm)]: "(!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t"
-apply (induct_tac "t")
-apply (simp (no_asm))
-apply simp
-done
-
-lemma eq_free_eq_subst_te: "(!n. n:(free_tv t) --> S1 n = S2 n) ==> $ S1 (t::typ) = $ S2 t"
-apply (rule typ_substitutions_only_on_free_variables)
-apply (simp (no_asm) add: Ball_def)
-done
-
-lemma scheme_substitutions_only_on_free_variables [rule_format (no_asm)]: "(!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch"
-apply (induct_tac "sch")
-apply (simp (no_asm))
-apply (simp (no_asm))
-apply simp
-done
-
-lemma eq_free_eq_subst_type_scheme:
- "(!n. n:(free_tv sch) --> S1 n = S2 n) ==> $ S1 (sch::type_scheme) = $ S2 sch"
-apply (rule scheme_substitutions_only_on_free_variables)
-apply (simp (no_asm) add: Ball_def)
-done
-
-lemma eq_free_eq_subst_scheme_list [rule_format (no_asm)]:
- "(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A"
-apply (induct_tac "A")
-(* case [] *)
-apply (fastsimp)
-(* case x#xl *)
-apply (fastsimp intro: eq_free_eq_subst_type_scheme)
-done
-
-lemma weaken_asm_Un: "((!x:A. (P x)) --> Q) ==> ((!x:A Un B. (P x)) --> Q)"
-apply fast
-done
-
-lemma scheme_list_substitutions_only_on_free_variables [rule_format (no_asm)]: "(!x:free_tv A. (S x) = (S' x)) --> $ S (A::type_scheme list) = $ S' A"
-apply (induct_tac "A")
-apply (simp (no_asm))
-apply simp
-apply (rule weaken_asm_Un)
-apply (intro strip)
-apply (erule scheme_substitutions_only_on_free_variables)
-done
-
-lemma eq_subst_te_eq_free [rule_format (no_asm)]:
- "$ S1 (t::typ) = $ S2 t --> n:(free_tv t) --> S1 n = S2 n"
-apply (induct_tac "t")
-(* case TVar n *)
-apply (fastsimp)
-(* case Fun t1 t2 *)
-apply (fastsimp)
-done
-
-lemma eq_subst_type_scheme_eq_free [rule_format (no_asm)]:
- "$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n"
-apply (induct_tac "sch")
-(* case TVar n *)
-apply (simp (no_asm_simp))
-(* case BVar n *)
-apply (intro strip)
-apply (erule mk_scheme_injective)
-apply (simp (no_asm_simp))
-(* case Fun t1 t2 *)
-apply simp
-done
-
-lemma eq_subst_scheme_list_eq_free [rule_format (no_asm)]:
- "$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n"
-apply (induct_tac "A")
-(* case [] *)
-apply (fastsimp)
-(* case x#xl *)
-apply (fastsimp intro: eq_subst_type_scheme_eq_free)
-done
-
-lemma codD:
- "v : cod S ==> v : free_tv S"
-apply (unfold free_tv_subst)
-apply (fast)
-done
-
-lemma not_free_impl_id:
- "x ~: free_tv S ==> S x = TVar x"
-
-apply (unfold free_tv_subst dom_def)
-apply (fast)
-done
-
-lemma free_tv_le_new_tv:
- "[| new_tv n t; m:free_tv t |] ==> m v : cod S"
-apply (unfold dom_def cod_def UNION_def Bex_def)
-apply (simp (no_asm))
-apply (safe intro!: exI conjI notI)
-prefer 2 apply (assumption)
-apply simp
-done
-declare cod_app_subst [simp]
-
-lemma free_tv_subst_var: "free_tv (S (v::nat)) <= insert v (cod S)"
-apply (case_tac "v:dom S")
-apply (fastsimp simp add: cod_def)
-apply (fastsimp simp add: dom_def)
-done
-
-lemma free_tv_app_subst_te: "free_tv ($ S (t::typ)) <= cod S Un free_tv t"
-apply (induct_tac "t")
-(* case TVar n *)
-apply (simp (no_asm) add: free_tv_subst_var)
-(* case Fun t1 t2 *)
-apply (fastsimp)
-done
-
-lemma free_tv_app_subst_type_scheme: "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch"
-apply (induct_tac "sch")
-(* case FVar n *)
-apply (simp (no_asm) add: free_tv_subst_var)
-(* case BVar n *)
-apply (simp (no_asm))
-(* case Fun t1 t2 *)
-apply (fastsimp)
-done
-
-lemma free_tv_app_subst_scheme_list: "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A"
-apply (induct_tac "A")
-(* case [] *)
-apply (simp (no_asm))
-(* case a#al *)
-apply (cut_tac free_tv_app_subst_type_scheme)
-apply (fastsimp)
-done
-
-lemma free_tv_comp_subst:
- "free_tv (%u::nat. $ s1 (s2 u) :: typ) <=
- free_tv s1 Un free_tv s2"
-apply (unfold free_tv_subst dom_def)
-apply (clarsimp simp add: cod_def dom_def)
-apply (drule free_tv_app_subst_te [THEN subsetD])
-apply clarsimp
-apply (auto simp add: cod_def dom_def)
-apply (drule free_tv_subst_var [THEN subsetD])
-apply (auto simp add: cod_def dom_def)
-done
-
-lemma free_tv_o_subst:
- "free_tv ($ S1 o S2) <= free_tv S1 Un free_tv (S2 :: nat => typ)"
-apply (unfold o_def)
-apply (rule free_tv_comp_subst)
-done
-
-lemma free_tv_of_substitutions_extend_to_types [rule_format (no_asm)]: "n : free_tv t --> free_tv (S n) <= free_tv ($ S t::typ)"
-apply (induct_tac "t")
-apply (simp (no_asm))
-apply (simp (no_asm))
-apply fast
-done
-
-lemma free_tv_of_substitutions_extend_to_schemes [rule_format (no_asm)]: "n : free_tv sch --> free_tv (S n) <= free_tv ($ S sch::type_scheme)"
-apply (induct_tac "sch")
-apply (simp (no_asm))
-apply (simp (no_asm))
-apply (simp (no_asm))
-apply fast
-done
-
-lemma free_tv_of_substitutions_extend_to_scheme_lists [rule_format (no_asm)]: "n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)"
-apply (induct_tac "A")
-apply (simp (no_asm))
-apply (simp (no_asm))
-apply (fast dest: free_tv_of_substitutions_extend_to_schemes)
-done
-
-declare free_tv_of_substitutions_extend_to_scheme_lists [simp]
-
-lemma free_tv_ML_scheme: "!!sch::type_scheme. (n : free_tv sch) = (n: set (free_tv_ML sch))"
-apply (induct_tac "sch")
-apply (simp_all (no_asm_simp))
-done
-
-lemma free_tv_ML_scheme_list: "!!A::type_scheme list. (n : free_tv A) = (n: set (free_tv_ML A))"
-apply (induct_tac "A")
-apply (simp (no_asm))
-apply (simp (no_asm_simp) add: free_tv_ML_scheme)
-done
-
-
-(* lemmata for bound_tv *)
-
-lemma bound_tv_mk_scheme: "bound_tv (mk_scheme t) = {}"
-apply (induct_tac "t")
-apply (simp_all (no_asm_simp))
-done
-
-declare bound_tv_mk_scheme [simp]
-
-lemma bound_tv_subst_scheme: "!!sch::type_scheme. bound_tv ($ S sch) = bound_tv sch"
-apply (induct_tac "sch")
-apply (simp_all (no_asm_simp))
-done
-
-declare bound_tv_subst_scheme [simp]
-
-lemma bound_tv_subst_scheme_list: "!!A::type_scheme list. bound_tv ($ S A) = bound_tv A"
-apply (rule list.induct)
-apply (simp (no_asm))
-apply (simp (no_asm_simp))
-done
-
-declare bound_tv_subst_scheme_list [simp]
-
-
-(* lemmata for new_tv *)
-
-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 (safe)
- (* ==> *)
- apply (fastsimp dest: leD simp add: free_tv_subst dom_def)
- apply (subgoal_tac "m:cod S | S l = TVar l")
- apply safe
- apply (fastsimp dest: UnI2 simp add: free_tv_subst)
- apply (drule_tac P = "%x. m:free_tv x" in subst , assumption)
- apply simp
- apply (fastsimp simp add: free_tv_subst cod_def dom_def)
-(* <== *)
-apply (unfold free_tv_subst cod_def dom_def)
-apply safe
- apply (cut_tac m = "m" and n = "n" in less_linear)
- apply (fast intro!: less_or_eq_imp_le)
-apply (cut_tac m = "ma" and n = "n" in less_linear)
-apply (fast intro!: less_or_eq_imp_le)
-done
-
-lemma new_tv_list: "new_tv n x = (!y:set x. new_tv n y)"
-apply (induct_tac "x")
-apply (simp_all (no_asm_simp))
-done
-
-(* substitution affects only variables occurring freely *)
-lemma subst_te_new_tv:
- "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t"
-apply (induct_tac "t")
-apply (simp_all (no_asm_simp))
-done
-declare subst_te_new_tv [simp]
-
-lemma subst_te_new_type_scheme [rule_format (no_asm)]:
- "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch"
-apply (induct_tac "sch")
-apply (simp_all (no_asm_simp))
-done
-declare subst_te_new_type_scheme [simp]
-
-lemma subst_tel_new_scheme_list [rule_format (no_asm)]:
- "new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A"
-apply (induct_tac "A")
-apply simp_all
-done
-declare subst_tel_new_scheme_list [simp]
-
-(* all greater variables are also new *)
-lemma new_tv_le:
- "n<=m ==> new_tv n t ==> new_tv m t"
-apply (unfold new_tv_def)
-apply safe
-apply (drule spec)
-apply (erule (1) notE impE)
-apply (simp (no_asm))
-done
-declare lessI [THEN less_imp_le [THEN new_tv_le], simp]
-
-lemma new_tv_typ_le: "n<=m ==> new_tv n (t::typ) ==> new_tv m t"
-apply (simp (no_asm_simp) add: new_tv_le)
-done
-
-lemma new_scheme_list_le: "n<=m ==> new_tv n (A::type_scheme list) ==> new_tv m A"
-apply (simp (no_asm_simp) add: new_tv_le)
-done
-
-lemma new_tv_subst_le: "n<=m ==> new_tv n (S::subst) ==> new_tv m S"
-apply (simp (no_asm_simp) add: new_tv_le)
-done
-
-(* new_tv property remains if a substitution is applied *)
-lemma new_tv_subst_var:
- "[| n new_tv m (S n)"
-apply (simp add: new_tv_subst)
-done
-
-lemma new_tv_subst_te [rule_format (no_asm)]:
- "new_tv n S --> new_tv n (t::typ) --> new_tv n ($ S t)"
-apply (induct_tac "t")
-apply (fastsimp simp add: new_tv_subst)+
-done
-declare new_tv_subst_te [simp]
-
-lemma new_tv_subst_type_scheme [rule_format (no_asm)]: "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)"
-apply (induct_tac "sch")
-apply (simp_all)
-apply (unfold new_tv_def)
-apply (simp (no_asm) add: free_tv_subst dom_def cod_def)
-apply (intro strip)
-apply (case_tac "S nat = TVar nat")
-apply simp
-apply (drule_tac x = "m" in spec)
-apply fast
-done
-declare new_tv_subst_type_scheme [simp]
-
-lemma new_tv_subst_scheme_list [rule_format (no_asm)]:
- "new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)"
-apply (induct_tac "A")
-apply (fastsimp)+
-done
-declare new_tv_subst_scheme_list [simp]
-
-lemma new_tv_Suc_list: "new_tv n A --> new_tv (Suc n) ((TVar n)#A)"
-apply (simp (no_asm) add: new_tv_list)
-done
-
-lemma new_tv_only_depends_on_free_tv_type_scheme [rule_format (no_asm)]: "!!sch::type_scheme. (free_tv sch) = (free_tv sch') --> (new_tv n sch --> new_tv n sch')"
-apply (unfold new_tv_def)
-apply (simp (no_asm_simp))
-done
-
-lemma new_tv_only_depends_on_free_tv_scheme_list [rule_format (no_asm)]: "!!A::type_scheme list. (free_tv A) = (free_tv A') --> (new_tv n A --> new_tv n A')"
-apply (unfold new_tv_def)
-apply (simp (no_asm_simp))
-done
-
-lemma new_tv_nth_nat_A [rule_format (no_asm)]:
- "!nat. nat < length A --> new_tv n A --> (new_tv n (A!nat))"
-apply (unfold new_tv_def)
-apply (induct_tac "A")
-apply simp
-apply (rule allI)
-apply (induct_tac "nat" rule: nat_induct)
-apply (intro strip)
-apply simp
-apply (simp (no_asm))
-done
-
-
-(* composition of substitutions preserves new_tv proposition *)
-lemma new_tv_subst_comp_1: "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (($ R) o S)"
-apply (simp add: new_tv_subst)
-done
-
-lemma new_tv_subst_comp_2: "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (%v.$ R (S v))"
-apply (simp add: new_tv_subst)
-done
-
-declare new_tv_subst_comp_1 [simp] new_tv_subst_comp_2 [simp]
-
-(* new type variables do not occur freely in a type structure *)
-lemma new_tv_not_free_tv:
- "new_tv n A ==> n~:(free_tv A)"
-apply (unfold new_tv_def)
-apply (fast elim: less_irrefl)
-done
-declare new_tv_not_free_tv [simp]
-
-lemma fresh_variable_types: "!!t::typ. ? n. (new_tv n t)"
-apply (unfold new_tv_def)
-apply (induct_tac "t")
-apply (rule_tac x = "Suc nat" in exI)
-apply (simp (no_asm_simp))
-apply (erule exE)+
-apply (rename_tac "n'")
-apply (rule_tac x = "max n n'" in exI)
-apply (simp (no_asm) add: less_max_iff_disj)
-apply blast
-done
-
-declare fresh_variable_types [simp]
-
-lemma fresh_variable_type_schemes: "!!sch::type_scheme. ? n. (new_tv n sch)"
-apply (unfold new_tv_def)
-apply (induct_tac "sch")
-apply (rule_tac x = "Suc nat" in exI)
-apply (simp (no_asm))
-apply (rule_tac x = "Suc nat" in exI)
-apply (simp (no_asm))
-apply (erule exE)+
-apply (rename_tac "n'")
-apply (rule_tac x = "max n n'" in exI)
-apply (simp (no_asm) add: less_max_iff_disj)
-apply blast
-done
-
-declare fresh_variable_type_schemes [simp]
-
-lemma fresh_variable_type_scheme_lists: "!!A::type_scheme list. ? n. (new_tv n A)"
-apply (induct_tac "A")
-apply (simp (no_asm))
-apply (simp (no_asm))
-apply (erule exE)
-apply (cut_tac sch = "a" in fresh_variable_type_schemes)
-apply (erule exE)
-apply (rename_tac "n'")
-apply (rule_tac x = " (max n n') " in exI)
-apply (subgoal_tac "n <= (max n n') ")
-apply (subgoal_tac "n' <= (max n n') ")
-apply (fast dest: new_tv_le)
-apply (simp_all (no_asm) add: le_max_iff_disj)
-done
-
-declare fresh_variable_type_scheme_lists [simp]
-
-lemma make_one_new_out_of_two: "[| ? n1. (new_tv n1 x); ? n2. (new_tv n2 y)|] ==> ? n. (new_tv n x) & (new_tv n y)"
-apply (erule exE)+
-apply (rename_tac "n1" "n2")
-apply (rule_tac x = " (max n1 n2) " in exI)
-apply (subgoal_tac "n1 <= max n1 n2")
-apply (subgoal_tac "n2 <= max n1 n2")
-apply (fast dest: new_tv_le)
-apply (simp_all (no_asm) add: le_max_iff_disj)
-done
-
-lemma ex_fresh_variable: "!!(A::type_scheme list) (A'::type_scheme list) (t::typ) (t'::typ).
- ? n. (new_tv n A) & (new_tv n A') & (new_tv n t) & (new_tv n t')"
-apply (cut_tac t = "t" in fresh_variable_types)
-apply (cut_tac t = "t'" in fresh_variable_types)
-apply (drule make_one_new_out_of_two)
-apply assumption
-apply (erule_tac V = "? n. new_tv n t'" in thin_rl)
-apply (cut_tac A = "A" in fresh_variable_type_scheme_lists)
-apply (cut_tac A = "A'" in fresh_variable_type_scheme_lists)
-apply (rotate_tac 1)
-apply (drule make_one_new_out_of_two)
-apply assumption
-apply (erule_tac V = "? n. new_tv n A'" in thin_rl)
-apply (erule exE)+
-apply (rename_tac n2 n1)
-apply (rule_tac x = " (max n1 n2) " in exI)
-apply (unfold new_tv_def)
-apply (simp (no_asm) add: less_max_iff_disj)
-apply blast
-done
-
-(* mgu does not introduce new type variables *)
-lemma mgu_new:
- "[|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> new_tv n u"
-apply (unfold new_tv_def)
-apply (fast dest: mgu_free)
-done
-
-
-(* lemmata for substitutions *)
-
-lemma length_app_subst_list:
- "!!A:: ('a::type_struct) list. length ($ S A) = length A"
-
-apply (unfold app_subst_list)
-apply (simp (no_asm))
-done
-declare length_app_subst_list [simp]
-
-lemma subst_TVar_scheme: "!!sch::type_scheme. $ TVar sch = sch"
-apply (induct_tac "sch")
-apply (simp_all (no_asm_simp))
-done
-
-declare subst_TVar_scheme [simp]
-
-lemma subst_TVar_scheme_list: "!!A::type_scheme list. $ TVar A = A"
-apply (rule list.induct)
-apply (simp_all add: app_subst_list)
-done
-
-declare subst_TVar_scheme_list [simp]
-
-(* application of id_subst does not change type expression *)
-lemma app_subst_id_te:
- "$ id_subst = (%t::typ. t)"
-apply (unfold id_subst_def)
-apply (rule ext)
-apply (induct_tac "t")
-apply (simp_all (no_asm_simp))
-done
-declare app_subst_id_te [simp]
-
-lemma app_subst_id_type_scheme:
- "$ id_subst = (%sch::type_scheme. sch)"
-apply (unfold id_subst_def)
-apply (rule ext)
-apply (induct_tac "sch")
-apply (simp_all (no_asm_simp))
-done
-declare app_subst_id_type_scheme [simp]
-
-(* application of id_subst does not change list of type expressions *)
-lemma app_subst_id_tel:
- "$ id_subst = (%A::type_scheme list. A)"
-apply (unfold app_subst_list)
-apply (rule ext)
-apply (induct_tac "A")
-apply (simp_all (no_asm_simp))
-done
-declare app_subst_id_tel [simp]
-
-lemma id_subst_sch: "!!sch::type_scheme. $ id_subst sch = sch"
-apply (induct_tac "sch")
-apply (simp_all add: id_subst_def)
-done
-
-declare id_subst_sch [simp]
-
-lemma id_subst_A: "!!A::type_scheme list. $ id_subst A = A"
-apply (induct_tac "A")
-apply simp
-apply simp
-done
-
-declare id_subst_A [simp]
-
-(* composition of substitutions *)
-lemma o_id_subst: "$S o id_subst = S"
-apply (unfold id_subst_def o_def)
-apply (rule ext)
-apply (simp (no_asm))
-done
-declare o_id_subst [simp]
-
-lemma subst_comp_te: "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t"
-apply (induct_tac "t")
-apply (simp_all (no_asm_simp))
-done
-
-lemma subst_comp_type_scheme: "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch"
-apply (induct_tac "sch")
-apply simp_all
-done
-
-lemma subst_comp_scheme_list:
- "$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A"
-apply (unfold app_subst_list)
-apply (induct_tac "A")
-(* case [] *)
-apply (simp (no_asm))
-(* case x#xl *)
-apply (simp add: subst_comp_type_scheme)
-done
-
-lemma subst_id_on_type_scheme_list': "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = $ id_subst A"
-apply (rule scheme_list_substitutions_only_on_free_variables)
-apply (simp add: id_subst_def)
-done
-
-lemma subst_id_on_type_scheme_list: "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A"
-apply (subst subst_id_on_type_scheme_list')
-apply assumption
-apply (simp (no_asm))
-done
-
-lemma nth_subst [rule_format (no_asm)]: "!n. n < length A --> ($ S A)!n = $S (A!n)"
-apply (induct_tac "A")
-apply simp
-apply (rule allI)
-apply (rename_tac "n1")
-apply (induct_tac "n1" rule: nat_induct)
-apply simp
-apply simp
-done
-
-
-end
diff -r ab1e47451aaa -r 82774ac788ae src/HOL/MiniML/W.thy
--- a/src/HOL/MiniML/W.thy Wed Mar 24 10:55:38 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,568 +0,0 @@
-(* Title: HOL/MiniML/W.thy
- ID: $Id$
- Author: Dieter Nazareth, Wolfgang Naraschewski and Tobias Nipkow
- Copyright 1996 TU Muenchen
-
-Correctness and completeness of type inference algorithm W
-*)
-
-
-theory W = MiniML:
-
-types result_W = "(subst * typ * nat)option"
-
--- "type inference algorithm W"
-consts W :: "[expr, ctxt, nat] => result_W"
-
-primrec
- "W (Var i) A n =
- (if i < length A then Some( id_subst,
- bound_typ_inst (%b. TVar(b+n)) (A!i),
- n + (min_new_bound_tv (A!i)) )
- else None)"
-
- "W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);
- Some( S, (S n) -> t, m) )"
-
- "W (App e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
- (S2,t2,m2) := W e2 ($S1 A) m1;
- U := mgu ($S2 t1) (t2 -> (TVar m2));
- Some( $U o $S2 o S1, U m2, Suc m2) )"
-
- "W (LET e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
- (S2,t2,m2) := W e2 ((gen ($S1 A) t1)#($S1 A)) m1;
- Some( $S2 o S1, t2, m2) )"
-
-
-declare Suc_le_lessD [simp]
-declare less_imp_le [simp del] (*the combination loops*)
-
-inductive_cases has_type_casesE:
-"A |- Var n :: t"
-"A |- Abs e :: t"
-"A |- App e1 e2 ::t"
-"A |- LET e1 e2 ::t"
-
-
-(* the resulting type variable is always greater or equal than the given one *)
-lemma W_var_ge [rule_format (no_asm)]: "!A n S t m. W e A n = Some (S,t,m) --> n<=m"
-apply (induct_tac "e")
-(* case Var(n) *)
-apply (simp (no_asm) split add: split_option_bind)
-(* case Abs e *)
-apply (simp (no_asm) split add: split_option_bind)
-apply (fast dest: Suc_leD)
-(* case App e1 e2 *)
-apply (simp (no_asm) split add: split_option_bind)
-apply (blast intro: le_SucI le_trans)
-(* case LET e1 e2 *)
-apply (simp (no_asm) split add: split_option_bind)
-apply (blast intro: le_trans)
-done
-
-declare W_var_ge [simp]
-
-lemma W_var_geD: "Some (S,t,m) = W e A n ==> n<=m"
-apply (simp add: eq_sym_conv)
-done
-
-lemma new_tv_compatible_W: "new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A"
-apply (drule W_var_geD)
-apply (rule new_scheme_list_le)
-apply assumption
-apply assumption
-done
-
-lemma new_tv_bound_typ_inst_sch [rule_format (no_asm)]: "new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)"
-apply (induct_tac "sch")
- apply simp
- apply (simp add: add_commute)
-apply (intro strip)
-apply simp
-apply (erule conjE)
-apply (rule conjI)
- apply (rule new_tv_le)
- prefer 2 apply (assumption)
- apply (rule add_le_mono)
- apply (simp (no_asm))
- apply (simp (no_asm) add: max_def)
-apply (rule new_tv_le)
- prefer 2 apply (assumption)
-apply (rule add_le_mono)
- apply (simp (no_asm))
-apply (simp (no_asm) add: max_def)
-done
-
-declare new_tv_bound_typ_inst_sch [simp]
-
-(* resulting type variable is new *)
-lemma new_tv_W [rule_format (no_asm)]: "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) -->
- new_tv m S & new_tv m t"
-apply (induct_tac "e")
-(* case Var n *)
-apply (simp (no_asm) split add: split_option_bind)
-apply (intro strip)
-apply (drule new_tv_nth_nat_A)
-apply assumption
-apply (simp (no_asm_simp))
-(* case Abs e *)
-apply (simp (no_asm) add: new_tv_subst new_tv_Suc_list split add: split_option_bind)
-apply (intro strip)
-apply (erule_tac x = "Suc n" in allE)
-apply (erule_tac x = " (FVar n) #A" in allE)
-apply (fastsimp simp add: new_tv_subst new_tv_Suc_list)
-(* case App e1 e2 *)
-apply (simp (no_asm) split add: split_option_bind)
-apply (intro strip)
-apply (rename_tac S1 t1 n1 S2 t2 n2 S3)
-apply (erule_tac x = "n" in allE)
-apply (erule_tac x = "A" 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 = "n1" in allE)
-apply (simp add: eq_sym_conv del: all_simps)
-apply (erule_tac x = "$S1 A" in allE)
-apply (erule_tac x = "S2" in allE)
-apply (erule_tac x = "t2" in allE)
-apply (erule_tac x = "n2" in allE)
-apply ( simp add: o_def rotate_Some)
-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_le])
-apply (rule_tac n = "n1" in new_tv_subst_le)
-apply (simp add: rotate_Some)
-apply (simp (no_asm_simp))
-apply (fast dest: W_var_geD intro: new_scheme_list_le new_tv_subst_scheme_list lessI [THEN less_imp_le [THEN new_tv_subst_le]])
-apply (erule sym [THEN mgu_new])
-apply (blast dest!: W_var_geD
- intro: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te
- new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
-
-apply (erule impE)
-apply (blast dest: W_var_geD intro: new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
-apply clarsimp
-
-apply (rule lessI [THEN new_tv_subst_var])
-apply (erule sym [THEN mgu_new])
-apply (blast dest!: W_var_geD
- intro: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te
- new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
-
-apply (erule impE)
-apply (blast dest: W_var_geD intro: new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
-apply clarsimp
-
--- "41: case LET e1 e2"
-apply (simp (no_asm) split add: split_option_bind)
-apply (intro strip)
-apply (erule allE,erule allE,erule allE,erule allE,erule allE, erule impE, assumption, erule impE, assumption)
-apply (erule conjE)
-apply (erule allE,erule allE,erule allE,erule allE,erule allE, erule impE, erule_tac [2] notE impE, tactic "assume_tac 2")
-apply (simp only: new_tv_def)
-apply (simp (no_asm_simp))
-apply (drule W_var_ge)+
-apply (rule allI)
-apply (intro strip)
-apply (simp only: free_tv_subst)
-apply (drule free_tv_app_subst_scheme_list [THEN subsetD])
-apply (best elim: less_le_trans)
-apply (erule conjE)
-apply (rule conjI)
-apply (simp only: o_def)
-apply (rule new_tv_subst_comp_2)
-apply (erule W_var_ge [THEN new_tv_subst_le])
-apply assumption
-apply assumption
-apply assumption
-done
-
-
-lemma free_tv_bound_typ_inst1 [rule_format (no_asm)]: "(v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)"
-apply (induct_tac "sch")
-apply simp
-apply simp
-apply (intro strip)
-apply (rule exI)
-apply (rule refl)
-apply simp
-done
-
-declare free_tv_bound_typ_inst1 [simp]
-
-lemma free_tv_W [rule_format (no_asm)]: "!n A S t m v. W e A n = Some (S,t,m) -->
- (v:free_tv S | v:free_tv t) --> v v:free_tv A"
-apply (induct_tac "e")
-(* case Var n *)
-apply (simp (no_asm) add: free_tv_subst split add: split_option_bind)
-apply (intro strip)
-apply (case_tac "v : free_tv (A!nat) ")
- apply simp
-apply (drule free_tv_bound_typ_inst1)
- apply (simp (no_asm) add: o_def)
-apply (erule exE)
-apply simp
-(* case Abs e *)
-apply (simp add: free_tv_subst split add: split_option_bind del: all_simps)
-apply (intro strip)
-apply (rename_tac S t n1 v)
-apply (erule_tac x = "Suc n" in allE)
-apply (erule_tac x = "FVar 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 (bestsimp intro: cod_app_subst simp add: less_Suc_eq)
-(* case App e1 e2 *)
-apply (simp (no_asm) split add: split_option_bind del: all_simps)
-apply (intro strip)
-apply (rename_tac S t n1 S1 t1 n2 S2 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)
-(* 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 (intro conjI impI | elim conjE)+
- apply (simp add: rotate_Some o_def)
- apply (drule W_var_geD)
- apply (drule W_var_geD)
- apply ( (frule less_le_trans) , (assumption))
- apply clarsimp
- apply (drule free_tv_comp_subst [THEN subsetD])
- apply (drule sym [THEN mgu_free])
- apply clarsimp
- 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_scheme_list [THEN subsetD] less_le_trans less_not_refl2 subsetD)
-apply simp
-apply (drule sym [THEN W_var_geD])
-apply (drule sym [THEN W_var_geD])
-apply ( (frule less_le_trans) , (assumption))
-apply clarsimp
-apply (drule mgu_free)
-apply (fastsimp dest: mgu_free codD free_tv_subst_var [THEN subsetD] free_tv_app_subst_te [THEN subsetD] free_tv_app_subst_scheme_list [THEN subsetD] less_le_trans subsetD)
-(* LET e1 e2 *)
-apply (simp (no_asm) split add: split_option_bind del: all_simps)
-apply (intro strip)
-apply (rename_tac S1 t1 n2 S2 t2 n3 v)
-apply (erule_tac x = "n" in allE)
-apply (erule_tac x = "A" in allE)
-apply (erule_tac x = "S1" in allE)
-apply (erule_tac x = "t1" in allE)
-apply (rotate_tac -1)
-apply (erule_tac x = "n2" in allE)
-apply (rotate_tac -1)
-apply (erule_tac x = "v" in allE)
-apply (erule (1) notE impE)
-apply (erule allE,erule allE,erule allE,erule allE,erule allE,erule_tac x = "v" in allE)
-apply (erule (1) notE impE)
-apply simp
-apply (rule conjI)
-apply (fast dest!: codD free_tv_app_subst_scheme_list [THEN subsetD] free_tv_o_subst [THEN subsetD] W_var_ge dest: less_le_trans)
-apply (fast dest!: codD free_tv_app_subst_scheme_list [THEN subsetD] W_var_ge dest: less_le_trans)
-done
-
-lemma weaken_A_Int_B_eq_empty: "(!x. x : A --> x ~: B) ==> A Int B = {}"
-apply fast
-done
-
-lemma weaken_not_elem_A_minus_B: "x ~: A | x : B ==> x ~: A - B"
-apply fast
-done
-
-(* correctness of W with respect to has_type *)
-lemma W_correct_lemma [rule_format (no_asm)]: "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t"
-apply (induct_tac "e")
-(* case Var n *)
-apply simp
-apply (intro strip)
-apply (rule has_type.VarI)
-apply (simp (no_asm))
-apply (simp (no_asm) add: is_bound_typ_instance)
-apply (rule exI)
-apply (rule refl)
-(* case Abs e *)
-apply (simp add: app_subst_list split add: split_option_bind)
-apply (intro strip)
-apply (erule_tac x = " (mk_scheme (TVar n)) # A" in allE)
-apply simp
-apply (rule has_type.AbsI)
-apply (drule le_refl [THEN le_SucI, THEN new_scheme_list_le])
-apply (drule sym)
-apply (erule allE)+
-apply (erule impE)
-apply (erule_tac [2] notE impE, tactic "assume_tac 2")
-apply (simp (no_asm_simp))
-apply assumption
-(* case App e1 e2 *)
-apply (simp (no_asm) split add: split_option_bind)
-apply (intro strip)
-apply (rename_tac S1 t1 n1 S2 t2 n2 S3)
-apply (rule_tac ?t2.0 = "$ S3 t2" in has_type.AppI)
-apply (rule_tac S1 = "S3" in app_subst_TVar [THEN subst])
-apply (rule app_subst_Fun [THEN subst])
-apply (rule_tac t = "$S3 (t2 -> (TVar n2))" and s = "$S3 ($S2 t1) " in subst)
-apply simp
-apply (simp only: subst_comp_scheme_list [symmetric] o_def)
-apply ((rule has_type_cl_sub [THEN spec]) , (rule has_type_cl_sub [THEN spec]))
-apply (simp add: eq_sym_conv)
-apply (simp add: subst_comp_scheme_list [symmetric] o_def has_type_cl_sub eq_sym_conv)
-apply (rule has_type_cl_sub [THEN spec])
-apply (frule new_tv_W)
-apply assumption
-apply (drule conjunct1)
-apply (frule new_tv_subst_scheme_list)
-apply (rule new_scheme_list_le)
-apply (rule W_var_ge)
-apply assumption
-apply assumption
-apply (erule thin_rl)
-apply (erule allE)+
-apply (drule sym)
-apply (drule sym)
-apply (erule thin_rl)
-apply (erule thin_rl)
-apply (erule (1) notE impE)
-apply (erule (1) notE impE)
-apply assumption
-(* case Let e1 e2 *)
-apply (simp (no_asm) split add: split_option_bind)
-apply (intro strip)
-(*by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); *)
-apply (rename_tac S1 t1 m1 S2)
-apply (rule_tac ?t1.0 = "$ S2 t1" in has_type.LETI)
- apply (simp (no_asm) add: o_def)
- apply (simp only: subst_comp_scheme_list [symmetric])
- apply (rule has_type_cl_sub [THEN spec])
- apply (drule_tac x = "A" in spec)
- apply (drule_tac x = "S1" in spec)
- apply (drule_tac x = "t1" in spec)
- apply (drule_tac x = "m1" in spec)
- apply (drule_tac x = "n" in spec)
- apply (erule (1) notE impE)
- apply (simp add: eq_sym_conv)
-apply (simp (no_asm) add: o_def)
-apply (simp only: subst_comp_scheme_list [symmetric])
-apply (rule gen_subst_commutes [symmetric, THEN subst])
- apply (rule_tac [2] app_subst_Cons [THEN subst])
- apply (erule_tac [2] thin_rl)
- apply (drule_tac [2] x = "gen ($S1 A) t1 # $ S1 A" in spec)
- apply (drule_tac [2] x = "S2" in spec)
- apply (drule_tac [2] x = "t" in spec)
- apply (drule_tac [2] x = "m" in spec)
- apply (drule_tac [2] x = "m1" in spec)
- apply (frule_tac [2] new_tv_W)
- prefer 2 apply (assumption)
- apply (drule_tac [2] conjunct1)
- apply (frule_tac [2] new_tv_subst_scheme_list)
- apply (rule_tac [2] new_scheme_list_le)
- apply (rule_tac [2] W_var_ge)
- prefer 2 apply (assumption)
- prefer 2 apply (assumption)
- apply (erule_tac [2] impE)
- apply (rule_tac [2] A = "$ S1 A" in new_tv_only_depends_on_free_tv_scheme_list)
- prefer 2 apply simp
- apply (fast)
- prefer 2 apply (assumption)
- prefer 2 apply simp
-apply (rule weaken_A_Int_B_eq_empty)
-apply (rule allI)
-apply (intro strip)
-apply (rule weaken_not_elem_A_minus_B)
-apply (case_tac "x < m1")
- apply (rule disjI2)
- apply (rule free_tv_gen_cons [THEN subst])
- apply (rule free_tv_W)
- apply assumption
- apply simp
- apply assumption
-apply (rule disjI1)
-apply (drule new_tv_W)
-apply assumption
-apply (drule conjunct2)
-apply (rule new_tv_not_free_tv)
-apply (rule new_tv_le)
- prefer 2 apply (assumption)
-apply (simp add: not_less_iff_le)
-done
-
-(* Completeness of W w.r.t. has_type *)
-lemma W_complete_lemma [rule_format (no_asm)]:
- "ALL S' A t' n. $S' A |- e :: t' --> new_tv n A -->
- (EX S t. (EX m. W e A n = Some (S,t,m)) &
- (EX R. $S' A = $R ($S A) & t' = $R t))"
-apply (induct_tac "e")
- (* case Var n *)
- apply (intro strip)
- apply (simp (no_asm) cong add: conj_cong)
- apply (erule has_type_casesE)
- apply (simp add: is_bound_typ_instance)
- apply (erule exE)
- apply (hypsubst)
- apply (rename_tac "S")
- apply (rule_tac x = "%x. (if x < n then S' x else S (x - n))" in exI)
- apply (rule conjI)
- apply (simp (no_asm_simp))
- apply (simp (no_asm_simp) add: bound_typ_inst_composed_subst [symmetric] new_tv_nth_nat_A o_def nth_subst
- del: bound_typ_inst_composed_subst)
-
- (* case 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 = " (FVar n) #A" in allE)
- apply (erule_tac x = "t2" in allE)
- apply (erule_tac x = "Suc n" in allE)
- apply (bestsimp dest!: mk_scheme_injective cong: conj_cong split: split_option_bind)
-
- (* case 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 safe
- 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 safe
- apply (blast intro: sym [THEN W_var_geD] new_tv_W [THEN conjunct1] new_scheme_list_le new_tv_subst_scheme_list)
-
- (** LEVEL 33 **)
-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 (no_asm_simp) add: subst_comp_te) prefer 2
-apply (rule_tac [2] eq_free_eq_subst_te)
-prefer 2 apply (intro strip) prefer 2
-apply (subgoal_tac [2] "na ~=ma")
- prefer 3 apply (best dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le)
-apply (case_tac [2] "na:free_tv Sa")
-(* n1 ~: free_tv S1 *)
-apply (frule_tac [3] not_free_impl_id)
- prefer 3 apply (simp)
-(* na : free_tv Sa *)
-apply (drule_tac [2] A1 = "$ S A" in trans [OF _ subst_comp_scheme_list])
-apply (drule_tac [2] eq_subst_scheme_list_eq_free)
- prefer 2 apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
-prefer 2 apply (simp (no_asm_simp)) prefer 2
-apply (case_tac [2] "na:dom Sa")
-(* na ~: dom Sa *)
- prefer 3 apply (simp add: dom_def)
-(* na : dom Sa *)
-apply (rule_tac [2] eq_free_eq_subst_te)
-prefer 2 apply (intro strip) prefer 2
-apply (subgoal_tac [2] "nb ~= ma")
-apply (frule_tac [3] new_tv_W) prefer 3 apply assumption
-apply (erule_tac [3] conjE)
-apply (drule_tac [3] new_tv_subst_scheme_list)
- prefer 3 apply (fast intro: new_scheme_list_le dest: sym [THEN W_var_geD])
- prefer 3 apply (fastsimp dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst)
- prefer 2 apply (fastsimp simp add: cod_def free_tv_subst)
-prefer 2 apply (simp (no_asm)) prefer 2
-apply (rule_tac [2] eq_free_eq_subst_te)
-prefer 2 apply (intro strip) prefer 2
-apply (subgoal_tac [2] "na ~= ma")
-apply (frule_tac [3] new_tv_W) prefer 3 apply assumption
-apply (erule_tac [3] conjE)
-apply (drule_tac [3] sym [THEN W_var_geD])
- prefer 3 apply (fast dest: new_scheme_list_le new_tv_subst_scheme_list new_tv_W new_tv_not_free_tv)
-apply (case_tac [2] "na: free_tv t - free_tv Sa")
-(* case na ~: free_tv t - free_tv Sa *)
- prefer 3
- apply simp
- apply fast
-(* case na : free_tv t - free_tv Sa *)
-prefer 2 apply simp prefer 2
-apply (drule_tac [2] A1 = "$ S A" and r = "$ R ($ S A)" in trans [OF _ subst_comp_scheme_list])
-apply (drule_tac [2] eq_subst_scheme_list_eq_free)
- prefer 2
- apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
-(** LEVEL 73 **)
- prefer 2 apply (simp add: free_tv_subst dom_def)
-apply (simp (no_asm_simp) split add: split_option_bind)
-apply safe
-apply (drule mgu_Some)
- apply fastsimp
-(** LEVEL 78 *)
-apply (drule mgu_mg, assumption)
-apply (erule exE)
-apply (rule_tac x = "Rb" in exI)
-apply (rule conjI)
-apply (drule_tac [2] x = "ma" in fun_cong)
- prefer 2 apply (simp add: eq_sym_conv)
-apply (simp (no_asm) add: subst_comp_scheme_list)
-apply (simp (no_asm) add: subst_comp_scheme_list [symmetric])
-apply (rule_tac A2 = "($ Sa ($ S A))" in trans [OF _ subst_comp_scheme_list [symmetric]])
-apply (simp add: o_def eq_sym_conv)
-apply (drule_tac s = "Some ?X" in sym)
-apply (rule eq_free_eq_subst_scheme_list)
-apply safe
-apply (subgoal_tac "ma ~= na")
-apply (frule_tac [2] new_tv_W) prefer 2 apply assumption
-apply (erule_tac [2] conjE)
-apply (drule_tac [2] new_tv_subst_scheme_list)
- prefer 2 apply (fast intro: new_scheme_list_le dest: sym [THEN W_var_geD])
-apply (frule_tac [2] n = "m" in new_tv_W) prefer 2 apply assumption
-apply (erule_tac [2] conjE)
-apply (drule_tac [2] free_tv_app_subst_scheme_list [THEN subsetD])
- apply (tactic {*
- (fast_tac (set_cs addDs [sym RS thm "W_var_geD", thm "new_scheme_list_le", thm "codD",
- thm "new_tv_not_free_tv"]) 2) *})
-apply (case_tac "na: free_tv t - free_tv Sa")
-(* case na ~: free_tv t - free_tv Sa *)
- prefer 2 apply simp apply blast
-(* case na : free_tv t - free_tv Sa *)
-apply simp
-apply (drule free_tv_app_subst_scheme_list [THEN subsetD])
- apply (fastsimp dest: codD trans [OF _ subst_comp_scheme_list]
- eq_subst_scheme_list_eq_free
- simp add: free_tv_subst dom_def)
-(* case Let e1 e2 *)
-apply (erule has_type_casesE)
-apply (erule_tac x = "S'" in allE)
-apply (erule_tac x = "A" in allE)
-apply (erule_tac x = "t1" in allE)
-apply (erule_tac x = "n" in allE)
-apply (erule (1) notE impE)
-apply (erule (1) notE impE)
-apply safe
-apply (simp (no_asm_simp))
-apply (erule_tac x = "R" in allE)
-apply (erule_tac x = "gen ($ S A) t # $ S A" in allE)
-apply (erule_tac x = "t'" in allE)
-apply (erule_tac x = "m" in allE)
-apply simp
-apply (drule mp)
-apply (rule has_type_le_env)
-apply assumption
-apply (simp (no_asm))
-apply (rule gen_bound_typ_instance)
-apply (drule mp)
-apply (frule new_tv_compatible_W)
-apply (rule sym)
-apply assumption
-apply (fast dest: new_tv_compatible_gen new_tv_subst_scheme_list new_tv_W)
-apply safe
-apply simp
-apply (rule_tac x = "Ra" in exI)
-apply (simp (no_asm) add: o_def subst_comp_scheme_list [symmetric])
-done
-
-
-lemma W_complete: "[] |- e :: t' ==> (? S t. (? m. W e [] n = Some(S,t,m)) &
- (? R. t' = $ R t))"
-apply (cut_tac A = "[]" and S' = "id_subst" and e = "e" and t' = "t'" in W_complete_lemma)
-apply simp_all
-done
-
-end
diff -r ab1e47451aaa -r 82774ac788ae src/HOL/ex/AVL.thy
--- a/src/HOL/ex/AVL.thy Wed Mar 24 10:55:38 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,421 +0,0 @@
-(* Title: HOL/ex/AVL.thy
- ID: $Id$
- Author: Cornelia Pusch and Tobias Nipkow, converted to Isar by Gerwin Klein
- Copyright 1998 TUM
-*)
-
-header "AVL Trees"
-
-theory AVL = Main:
-
-text {*
- At the moment only insertion is formalized.
-
- This theory would be a nice candidate for structured Isar proof
- texts and for extensions (delete operation).
-*}
-
-(*
- This version works exclusively with nat. Balance check could be
- simplified by working with int:
- is_bal (MKT n l r) = (abs(int(height l) - int(height r)) <= 1 & is_bal l & is_bal r)
-*)
-
-datatype tree = ET | MKT nat tree tree
-
-consts
- height :: "tree \ nat"
- is_in :: "nat \ tree \ bool"
- is_ord :: "tree \ bool"
- is_bal :: "tree \ bool"
-
-primrec
- "height ET = 0"
- "height (MKT n l r) = 1 + max (height l) (height r)"
-
-primrec
- "is_in k ET = False"
- "is_in k (MKT n l r) = (k=n \ is_in k l \ is_in k r)"
-
-primrec
- "is_ord ET = True"
- "is_ord (MKT n l r) = ((\n'. is_in n' l \ n' < n) \
- (\n'. is_in n' r \ n < n') \
- is_ord l \ is_ord r)"
-
-primrec
- "is_bal ET = True"
- "is_bal (MKT n l r) = ((height l = height r \
- height l = 1+height r \
- height r = 1+height l) \
- is_bal l \ is_bal r)"
-
-
-datatype bal = Just | Left | Right
-
-constdefs
- bal :: "tree \ bal"
- "bal t \ case t of ET \ Just
- | (MKT n l r) \ if height l = height r then Just
- else if height l < height r then Right else Left"
-
-consts
- r_rot :: "nat \ tree \ tree \ tree"
- l_rot :: "nat \ tree \ tree \ tree"
- lr_rot :: "nat \ tree \ tree \ tree"
- rl_rot :: "nat \ tree \ tree \ tree"
-
-recdef r_rot "{}"
- "r_rot (n, MKT ln ll lr, r) = MKT ln ll (MKT n lr r)"
-
-recdef l_rot "{}"
- "l_rot(n, l, MKT rn rl rr) = MKT rn (MKT n l rl) rr"
-
-recdef lr_rot "{}"
- "lr_rot(n, MKT ln ll (MKT lrn lrl lrr), r) = MKT lrn (MKT ln ll lrl) (MKT n lrr r)"
-
-recdef rl_rot "{}"
- "rl_rot(n, l, MKT rn (MKT rln rll rlr) rr) = MKT rln (MKT n l rll) (MKT rn rlr rr)"
-
-
-constdefs
- l_bal :: "nat \ tree \ tree \ tree"
- "l_bal n l r \ if bal l = Right
- then lr_rot (n, l, r)
- else r_rot (n, l, r)"
-
- r_bal :: "nat \ tree \ tree \ tree"
- "r_bal n l r \ if bal r = Left
- then rl_rot (n, l, r)
- else l_rot (n, l, r)"
-
-consts
- insert :: "nat \ tree \ tree"
-primrec
-"insert x ET = MKT x ET ET"
-"insert x (MKT n l r) =
- (if x=n
- then MKT n l r
- else if x height l = Suc(Suc(height r)); bal l = Right; is_bal l; is_bal r \
- \ is_bal (lr_rot (n, l, r))"
-apply (unfold bal_def)
-apply (cases l)
- apply simp
-apply (rename_tac t1 t2)
-apply (case_tac t2)
- apply simp
-apply (simp add: max_def split: split_if_asm)
-apply arith
-done
-
-
-lemma is_bal_r_rot:
-"\ height l = Suc(Suc(height r)); bal l \ Right; is_bal l; is_bal r \
- \ is_bal (r_rot (n, l, r))"
-apply (unfold bal_def)
-apply (cases "l")
- apply simp
-apply (simp add: max_def split: split_if_asm)
-done
-
-
-lemma is_bal_rl_rot:
-"\ height r = Suc(Suc(height l)); bal r = Left; is_bal l; is_bal r \
- \ is_bal (rl_rot (n, l, r))"
-apply (unfold bal_def)
-apply (cases r)
- apply simp
-apply (rename_tac t1 t2)
-apply (case_tac t1)
- apply (simp add: max_def split: split_if_asm)
-apply (simp add: max_def split: split_if_asm)
-apply arith
-done
-
-
-lemma is_bal_l_rot:
-"\ height r = Suc(Suc(height l)); bal r \ Left; is_bal l; is_bal r \
- \ is_bal (l_rot (n, l, r))"
-apply (unfold bal_def)
-apply (cases r)
- apply simp
-apply (simp add: max_def split: split_if_asm)
-done
-
-
-text {* Lemmas about height after rotation *}
-
-lemma height_lr_rot:
-"\ bal l = Right; height l = Suc(Suc(height r)) \
- \ Suc(height (lr_rot (n, l, r))) = height (MKT n l r) "
-apply (unfold bal_def)
-apply (cases l)
- apply simp
-apply (rename_tac t1 t2)
-apply (case_tac t2)
- apply simp
-apply (simp add: max_def split: split_if_asm)
-done
-
-
-lemma height_r_rot:
-"\ height l = Suc(Suc(height r)); bal l \ Right \
- \ Suc(height (r_rot (n, l, r))) = height (MKT n l r) \
- height (r_rot (n, l, r)) = height (MKT n l r)"
-apply (unfold bal_def)
-apply (cases l)
- apply simp
-apply (simp add: max_def split: split_if_asm)
-done
-
-
-lemma height_l_bal:
-"height l = Suc(Suc(height r))
- \ Suc(height (l_bal n l r)) = height (MKT n l r) |
- height (l_bal n l r) = height (MKT n l r)"
-apply (unfold l_bal_def)
-apply (cases "bal l = Right")
- apply (fastsimp dest: height_lr_rot)
-apply (fastsimp dest: height_r_rot)
-done
-
-
-lemma height_rl_rot [rule_format (no_asm)]:
-"height r = Suc(Suc(height l)) \ bal r = Left
- \ Suc(height (rl_rot (n, l, r))) = height (MKT n l r)"
-apply (unfold bal_def)
-apply (cases r)
- apply simp
-apply (rename_tac t1 t2)
-apply (case_tac t1)
- apply simp
-apply (simp add: max_def split: split_if_asm)
-done
-
-
-lemma height_l_rot [rule_format (no_asm)]:
-"height r = Suc(Suc(height l)) \ bal r \ Left
- \ Suc(height (l_rot (n, l, r))) = height (MKT n l r) \
- height (l_rot (n, l, r)) = height (MKT n l r)"
-apply (unfold bal_def)
-apply (cases r)
- apply simp
-apply (simp add: max_def)
-done
-
-
-lemma height_r_bal:
-"height r = Suc(Suc(height l))
- \ Suc(height (r_bal n l r)) = height (MKT n l r) \
- height (r_bal n l r) = height (MKT n l r)"
-apply (unfold r_bal_def)
-apply (cases "bal r = Left")
- apply (fastsimp dest: height_rl_rot)
-apply (fastsimp dest: height_l_rot)
-done
-
-lemma height_insert [rule_format (no_asm)]:
-"is_bal t
- \ height (insert x t) = height t \ height (insert x t) = Suc(height t)"
-apply (induct_tac "t")
- apply simp
-apply (rename_tac n t1 t2)
-apply (case_tac "x=n")
- apply simp
-apply (case_tac "xheight (insert x l) \ Suc(Suc(height r)); is_bal (insert x l); is_bal (MKT n l r)\
- \ is_bal (MKT n (insert x l) r)"
-apply (cut_tac x = "x" and t = "l" in height_insert)
- apply simp
-apply fastsimp
-done
-
-
-lemma is_bal_insert_right:
-"\ height (insert x r) \ Suc(Suc(height l)); is_bal (insert x r); is_bal (MKT n l r) \
- \ is_bal (MKT n l (insert x r))"
-apply (cut_tac x = "x" and t = "r" in height_insert)
- apply simp
-apply fastsimp
-done
-
-
-lemma is_bal_insert [rule_format (no_asm)]:
-"is_bal t \ is_bal(insert x t)"
-apply (induct_tac "t")
- apply simp
-apply (rename_tac n t1 t2)
-apply (case_tac "x=n")
- apply simp
-apply (case_tac "x height l = Suc(Suc(height r)); bal l = Right \
- \ is_in x (lr_rot (n, l, r)) = is_in x (MKT n l r)"
-apply (unfold bal_def)
-apply (cases l)
- apply simp
-apply (rename_tac t1 t2)
-apply (case_tac t2)
- apply simp
-apply fastsimp
-done
-
-
-lemma is_in_r_rot:
-"\ height l = Suc(Suc(height r)); bal l \ Right \
- \ is_in x (r_rot (n, l, r)) = is_in x (MKT n l r)"
-apply (unfold bal_def)
-apply (cases l)
- apply simp
-apply fastsimp
-done
-
-
-lemma is_in_rl_rot:
-"\ height r = Suc(Suc(height l)); bal r = Left \
- \ is_in x (rl_rot (n, l, r)) = is_in x (MKT n l r)"
-apply (unfold bal_def)
-apply (cases r)
- apply simp
-apply (rename_tac t1 t2)
-apply (case_tac t1)
- apply (simp add: max_def le_def)
-apply fastsimp
-done
-
-
-lemma is_in_l_rot:
-"\ height r = Suc(Suc(height l)); bal r ~= Left \
- \ is_in x (l_rot (n, l, r)) = is_in x (MKT n l r)"
-apply (unfold bal_def)
-apply (cases r)
- apply simp
-apply fastsimp
-done
-
-
-lemma is_in_insert:
-"is_in y (insert x t) = (y=x \ is_in y t)"
-apply (induct t)
- apply simp
-apply (simp add: l_bal_def is_in_lr_rot is_in_r_rot r_bal_def
- is_in_rl_rot is_in_l_rot)
-apply blast
-done
-
-
-subsection "is-ord"
-
-lemma is_ord_lr_rot [rule_format (no_asm)]:
-"\ height l = Suc(Suc(height r)); bal l = Right; is_ord (MKT n l r) \
- \ is_ord (lr_rot (n, l, r))"
-apply (unfold bal_def)
-apply (cases l)
- apply simp
-apply (rename_tac t1 t2)
-apply (case_tac t2)
- apply simp
-apply simp
-apply (blast intro: less_trans)
-done
-
-
-lemma is_ord_r_rot:
-"\ height l = Suc(Suc(height r)); bal l \ Right; is_ord (MKT n l r) \
- \ is_ord (r_rot (n, l, r))"
-apply (unfold bal_def)
-apply (cases l)
-apply (auto intro: less_trans)
-done
-
-
-lemma is_ord_rl_rot:
-"\ height r = Suc(Suc(height l)); bal r = Left; is_ord (MKT n l r) \
- \ is_ord (rl_rot (n, l, r))"
-apply (unfold bal_def)
-apply (cases r)
- apply simp
-apply (rename_tac t1 t2)
-apply (case_tac t1)
- apply (simp add: le_def)
-apply simp
-apply (blast intro: less_trans)
-done
-
-
-lemma is_ord_l_rot:
-"\ height r = Suc(Suc(height l)); bal r \ Left; is_ord (MKT n l r) \
- \ is_ord (l_rot (n, l, r))"
-apply (unfold bal_def)
-apply (cases r)
- apply simp
-apply simp
-apply (blast intro: less_trans)
-done
-
-
-lemma is_ord_insert:
-"is_ord t \ is_ord(insert x t)"
-apply (induct t)
- apply simp
-apply (cut_tac m = "x" and n = "nat" in less_linear)
-apply (fastsimp simp add: l_bal_def is_ord_lr_rot is_ord_r_rot r_bal_def
- is_ord_l_rot is_ord_rl_rot is_in_insert)
-done
-
-end
diff -r ab1e47451aaa -r 82774ac788ae src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML Wed Mar 24 10:55:38 2004 +0100
+++ b/src/HOL/ex/ROOT.ML Thu Mar 25 05:37:32 2004 +0100
@@ -25,7 +25,6 @@
time_use_thy "mesontest2";
time_use_thy "PresburgerEx";
time_use_thy "BT";
-time_use_thy "AVL";
time_use_thy "InSort";
time_use_thy "Qsort";
time_use_thy "MergeSort";