moved MiniML and AVL to archive of formal proofs
authorkleing
Thu Mar 25 05:37:32 2004 +0100 (2004-03-25)
changeset 1448282774ac788ae
parent 14481 ab1e47451aaa
child 14483 6eac487f9cfa
moved MiniML and AVL to archive of formal proofs
src/HOL/IsaMakefile
src/HOL/MiniML/Generalize.thy
src/HOL/MiniML/Instance.thy
src/HOL/MiniML/Maybe.thy
src/HOL/MiniML/MiniML.thy
src/HOL/MiniML/README.html
src/HOL/MiniML/ROOT.ML
src/HOL/MiniML/Type.thy
src/HOL/MiniML/W.thy
src/HOL/ex/AVL.thy
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/IsaMakefile	Wed Mar 24 10:55:38 2004 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Thu Mar 25 05:37:32 2004 +0100
     1.3 @@ -30,7 +30,6 @@
     1.4    HOL-Lattice \
     1.5    HOL-Lex \
     1.6    HOL-MicroJava \
     1.7 -  HOL-MiniML \
     1.8    HOL-Modelcheck \
     1.9    HOL-NanoJava \
    1.10    HOL-NumberTheory \
    1.11 @@ -432,16 +431,6 @@
    1.12  	@$(ISATOOL) usedir $(OUT)/HOL W0
    1.13  
    1.14  
    1.15 -## HOL-MiniML
    1.16 -
    1.17 -HOL-MiniML: HOL $(LOG)/HOL-MiniML.gz
    1.18 -
    1.19 -$(LOG)/HOL-MiniML.gz: $(OUT)/HOL MiniML/Generalize.thy\
    1.20 -  MiniML/Instance.thy MiniML/Maybe.thy MiniML/MiniML.thy \
    1.21 -  MiniML/ROOT.ML MiniML/Type.thy MiniML/W.thy
    1.22 -	@$(ISATOOL) usedir $(OUT)/HOL MiniML
    1.23 -
    1.24 -
    1.25  ## HOL-MicroJava
    1.26  
    1.27  HOL-MicroJava: HOL $(LOG)/HOL-MicroJava.gz
    1.28 @@ -559,7 +548,7 @@
    1.29  
    1.30  HOL-ex: HOL $(LOG)/HOL-ex.gz
    1.31  
    1.32 -$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/AVL.thy ex/Antiquote.thy \
    1.33 +$(LOG)/HOL-ex.gz: $(OUT)/HOL ex/Antiquote.thy \
    1.34    ex/BT.thy ex/BinEx.thy ex/Group.ML ex/Group.thy ex/Higher_Order_Logic.thy \
    1.35    ex/Hilbert_Classical.thy ex/InSort.thy ex/IntRing.ML \
    1.36    ex/InductiveInvariant.thy  ex/InductiveInvariant_examples.thy\
    1.37 @@ -666,7 +655,6 @@
    1.38  		$(LOG)/HOL-Lex.gz $(LOG)/HOL-Algebra.gz \
    1.39  		$(LOG)/HOL-Auth.gz $(LOG)/HOL-UNITY.gz \
    1.40  		$(LOG)/HOL-Modelcheck.gz $(LOG)/HOL-Lambda.gz \
    1.41 -		$(LOG)/HOL-W0.gz $(LOG)/HOL-MiniML.gz \
    1.42                  $(LOG)/HOL-Bali.gz $(LOG)/HOL-CTL.gz \
    1.43  		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz \
    1.44  		$(LOG)/HOL-IOA.gz $(LOG)/HOL-AxClasses \
     2.1 --- a/src/HOL/MiniML/Generalize.thy	Wed Mar 24 10:55:38 2004 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,171 +0,0 @@
     2.4 -(* Title:     HOL/MiniML/Generalize.thy
     2.5 -   ID:        $Id$
     2.6 -   Author:    Wolfgang Naraschewski and Tobias Nipkow
     2.7 -   Copyright  1996 TU Muenchen
     2.8 -
     2.9 -Generalizing type schemes with respect to a context
    2.10 -*)
    2.11 -
    2.12 -theory Generalize = Instance:
    2.13 -
    2.14 -
    2.15 -(* gen: binding (generalising) the variables which are not free in the context *)
    2.16 -
    2.17 -types ctxt = "type_scheme list"
    2.18 -    
    2.19 -consts
    2.20 -  gen :: "[ctxt, typ] => type_scheme"
    2.21 -
    2.22 -primrec
    2.23 -  "gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
    2.24 -  "gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)"
    2.25 -
    2.26 -(* executable version of gen: Implementation with free_tv_ML *)
    2.27 -
    2.28 -consts
    2.29 -  gen_ML_aux :: "[nat list, typ] => type_scheme"
    2.30 -primrec
    2.31 -  "gen_ML_aux A (TVar n) = (if (n: set A) then (FVar n) else (BVar n))"
    2.32 -  "gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
    2.33 -
    2.34 -consts
    2.35 -  gen_ML :: "[ctxt, typ] => type_scheme"
    2.36 -defs
    2.37 -  gen_ML_def: "gen_ML A t == gen_ML_aux (free_tv_ML A) t"
    2.38 -
    2.39 -
    2.40 -declare equalityE [elim!]
    2.41 -
    2.42 -lemma gen_eq_on_free_tv: "free_tv A = free_tv B ==> gen A t = gen B t"
    2.43 -apply (induct_tac "t")
    2.44 -apply (simp_all (no_asm_simp))
    2.45 -done
    2.46 -
    2.47 -lemma gen_without_effect [rule_format (no_asm)]: "(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)"
    2.48 -apply (induct_tac "t")
    2.49 -apply (simp (no_asm_simp))
    2.50 -apply (simp (no_asm))
    2.51 -apply fast
    2.52 -done
    2.53 -
    2.54 -declare gen_without_effect [simp]
    2.55 -
    2.56 -lemma free_tv_gen: "free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)"
    2.57 -apply (induct_tac "t")
    2.58 -apply (simp (no_asm))
    2.59 -apply (case_tac "nat : free_tv ($ S A) ")
    2.60 -apply (simp (no_asm_simp))
    2.61 -apply fast
    2.62 -apply (simp (no_asm_simp))
    2.63 -apply fast
    2.64 -apply simp
    2.65 -apply fast
    2.66 -done
    2.67 -
    2.68 -declare free_tv_gen [simp]
    2.69 -
    2.70 -lemma free_tv_gen_cons: "free_tv (gen ($ S A) t # $ S A) = free_tv ($ S A)"
    2.71 -apply (simp (no_asm))
    2.72 -apply fast
    2.73 -done
    2.74 -
    2.75 -declare free_tv_gen_cons [simp]
    2.76 -
    2.77 -lemma bound_tv_gen: "bound_tv (gen A t1) = (free_tv t1) - (free_tv A)"
    2.78 -apply (induct_tac "t1")
    2.79 -apply (simp (no_asm))
    2.80 -apply (case_tac "nat : free_tv A")
    2.81 -apply (simp (no_asm_simp))
    2.82 -apply (simp (no_asm_simp))
    2.83 -apply fast
    2.84 -apply (simp (no_asm_simp))
    2.85 -apply fast
    2.86 -done
    2.87 -
    2.88 -declare bound_tv_gen [simp]
    2.89 -
    2.90 -lemma new_tv_compatible_gen [rule_format (no_asm)]: "new_tv n t --> new_tv n (gen A t)"
    2.91 -apply (induct_tac "t")
    2.92 -apply auto
    2.93 -done
    2.94 -
    2.95 -lemma gen_eq_gen_ML: "gen A t = gen_ML A t"
    2.96 -apply (unfold gen_ML_def)
    2.97 -apply (induct_tac "t")
    2.98 - apply (simp (no_asm) add: free_tv_ML_scheme_list)
    2.99 -apply (simp (no_asm_simp) add: free_tv_ML_scheme_list)
   2.100 -done
   2.101 -
   2.102 -lemma gen_subst_commutes [rule_format (no_asm)]: "(free_tv S) Int ((free_tv t) - (free_tv A)) = {}  
   2.103 -      --> gen ($ S A) ($ S t) = $ S (gen A t)"
   2.104 -apply (induct_tac "t")
   2.105 - apply (intro strip)
   2.106 - apply (case_tac "nat: (free_tv A) ")
   2.107 -  apply (simp (no_asm_simp))
   2.108 - apply simp
   2.109 - apply (subgoal_tac "nat ~: free_tv S")
   2.110 -  prefer 2 apply (fast)
   2.111 - apply (simp add: free_tv_subst dom_def)
   2.112 - apply (cut_tac free_tv_app_subst_scheme_list)
   2.113 - apply fast
   2.114 -apply (simp (no_asm_simp))
   2.115 -apply blast
   2.116 -done
   2.117 -
   2.118 -lemma bound_typ_inst_gen [rule_format (no_asm)]: "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t"
   2.119 -apply (induct_tac "t")
   2.120 -apply (simp_all (no_asm_simp))
   2.121 -apply fast
   2.122 -done
   2.123 -declare bound_typ_inst_gen [simp]
   2.124 -
   2.125 -lemma gen_bound_typ_instance: 
   2.126 -  "gen ($ S A) ($ S t) <= $ S (gen A t)"
   2.127 -apply (unfold le_type_scheme_def is_bound_typ_instance)
   2.128 -apply safe
   2.129 -apply (rename_tac "R")
   2.130 -apply (rule_tac x = " (%a. bound_typ_inst R (gen ($S A) (S a))) " in exI)
   2.131 -apply (induct_tac "t")
   2.132 - apply (simp (no_asm))
   2.133 -apply (simp (no_asm_simp))
   2.134 -done
   2.135 -
   2.136 -lemma free_tv_subset_gen_le: 
   2.137 -  "free_tv B <= free_tv A ==> gen A t <= gen B t"
   2.138 -apply (unfold le_type_scheme_def is_bound_typ_instance)
   2.139 -apply safe
   2.140 -apply (rename_tac "S")
   2.141 -apply (rule_tac x = "%b. if b:free_tv A then TVar b else S b" in exI)
   2.142 -apply (induct_tac "t")
   2.143 - apply (simp (no_asm_simp))
   2.144 - apply fast
   2.145 -apply (simp (no_asm_simp))
   2.146 -done
   2.147 -
   2.148 -lemma gen_t_le_gen_alpha_t [rule_format (no_asm)]: 
   2.149 -  "new_tv n A -->  
   2.150 -   gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)"
   2.151 -apply (unfold le_type_scheme_def is_bound_typ_instance)
   2.152 -apply (intro strip)
   2.153 -apply (erule exE)
   2.154 -apply (hypsubst)
   2.155 -apply (rule_tac x = " (%x. S (if n <= x then x - n else x))" in exI)
   2.156 -apply (induct_tac "t")
   2.157 -apply (simp (no_asm))
   2.158 -apply (case_tac "nat : free_tv A")
   2.159 -apply (simp (no_asm_simp))
   2.160 -apply (simp (no_asm_simp))
   2.161 -apply (subgoal_tac "n <= n + nat")
   2.162 -apply (frule_tac t = "A" in new_tv_le)
   2.163 -apply assumption
   2.164 -apply (drule new_tv_not_free_tv)
   2.165 -apply (drule new_tv_not_free_tv)
   2.166 -apply (simp (no_asm_simp) add: diff_add_inverse)
   2.167 -apply (simp (no_asm) add: le_add1)
   2.168 -apply (simp (no_asm_simp))
   2.169 -done
   2.170 -
   2.171 -declare gen_t_le_gen_alpha_t [simp]
   2.172 -
   2.173 -
   2.174 -end
     3.1 --- a/src/HOL/MiniML/Instance.thy	Wed Mar 24 10:55:38 2004 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,341 +0,0 @@
     3.4 -(* Title:     HOL/MiniML/Instance.thy
     3.5 -   ID:        $Id$
     3.6 -   Author:    Wolfgang Naraschewski and Tobias Nipkow
     3.7 -   Copyright  1996 TU Muenchen
     3.8 -
     3.9 -Instances of type schemes
    3.10 -*)
    3.11 -
    3.12 -theory Instance = Type:
    3.13 -
    3.14 -  
    3.15 -(* generic instances of a type scheme *)
    3.16 -
    3.17 -consts
    3.18 -  bound_typ_inst :: "[subst, type_scheme] => typ"
    3.19 -
    3.20 -primrec
    3.21 -  "bound_typ_inst S (FVar n) = (TVar n)"
    3.22 -  "bound_typ_inst S (BVar n) = (S n)"
    3.23 -  "bound_typ_inst S (sch1 =-> sch2) = ((bound_typ_inst S sch1) -> (bound_typ_inst S sch2))"
    3.24 -
    3.25 -consts
    3.26 -  bound_scheme_inst :: "[nat => type_scheme, type_scheme] => type_scheme"
    3.27 -
    3.28 -primrec
    3.29 -  "bound_scheme_inst S (FVar n) = (FVar n)"
    3.30 -  "bound_scheme_inst S (BVar n) = (S n)"
    3.31 -  "bound_scheme_inst S (sch1 =-> sch2) = ((bound_scheme_inst S sch1) =-> (bound_scheme_inst S sch2))"
    3.32 -  
    3.33 -consts
    3.34 -  "<|" :: "[typ, type_scheme] => bool" (infixr 70)
    3.35 -defs
    3.36 -  is_bound_typ_instance: "t <| sch == ? S. t = (bound_typ_inst S sch)" 
    3.37 -
    3.38 -instance type_scheme :: ord ..
    3.39 -defs le_type_scheme_def: "sch' <= (sch::type_scheme) == !t. t <| sch' --> t <| sch"
    3.40 -
    3.41 -consts
    3.42 -  subst_to_scheme :: "[nat => type_scheme, typ] => type_scheme"
    3.43 -
    3.44 -primrec
    3.45 -  "subst_to_scheme B (TVar n) = (B n)"
    3.46 -  "subst_to_scheme B (t1 -> t2) = ((subst_to_scheme B t1) =-> (subst_to_scheme B t2))"
    3.47 -  
    3.48 -instance list :: (ord)ord ..
    3.49 -defs le_env_def:
    3.50 -  "A <= B == length B = length A & (!i. i < length A --> A!i <= B!i)"
    3.51 -
    3.52 -
    3.53 -(* lemmatas for instatiation *)
    3.54 -
    3.55 -
    3.56 -(* lemmatas for bound_typ_inst *)
    3.57 -
    3.58 -lemma bound_typ_inst_mk_scheme: "bound_typ_inst S (mk_scheme t) = t"
    3.59 -apply (induct_tac "t")
    3.60 -apply (simp_all (no_asm_simp))
    3.61 -done
    3.62 -
    3.63 -declare bound_typ_inst_mk_scheme [simp]
    3.64 -
    3.65 -lemma bound_typ_inst_composed_subst: "bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)"
    3.66 -apply (induct_tac "sch")
    3.67 -apply simp_all
    3.68 -done
    3.69 -
    3.70 -declare bound_typ_inst_composed_subst [simp]
    3.71 -
    3.72 -lemma bound_typ_inst_eq: "S = S' ==> sch = sch' ==> bound_typ_inst S sch = bound_typ_inst S' sch'"
    3.73 -apply simp
    3.74 -done
    3.75 -
    3.76 -
    3.77 -
    3.78 -(* lemmatas for bound_scheme_inst *)
    3.79 -
    3.80 -lemma bound_scheme_inst_mk_scheme: "bound_scheme_inst B (mk_scheme t) = mk_scheme t"
    3.81 -apply (induct_tac "t")
    3.82 -apply (simp (no_asm))
    3.83 -apply (simp (no_asm_simp))
    3.84 -done
    3.85 -
    3.86 -declare bound_scheme_inst_mk_scheme [simp]
    3.87 -
    3.88 -lemma substitution_lemma: "$S (bound_scheme_inst B sch) = (bound_scheme_inst ($S o B) ($ S sch))"
    3.89 -apply (induct_tac "sch")
    3.90 -apply (simp (no_asm))
    3.91 -apply (simp (no_asm))
    3.92 -apply (simp (no_asm_simp))
    3.93 -done
    3.94 -
    3.95 -lemma bound_scheme_inst_type [rule_format (no_asm)]: "!t. mk_scheme t = bound_scheme_inst B sch -->  
    3.96 -          (? S. !x:bound_tv sch. B x = mk_scheme (S x))"
    3.97 -apply (induct_tac "sch")
    3.98 -apply (simp (no_asm))
    3.99 -apply safe
   3.100 -apply (rule exI)
   3.101 -apply (rule ballI)
   3.102 -apply (rule sym)
   3.103 -apply simp
   3.104 -apply simp
   3.105 -apply (drule mk_scheme_Fun)
   3.106 -apply (erule exE)+
   3.107 -apply (erule conjE)
   3.108 -apply (drule sym)
   3.109 -apply (drule sym)
   3.110 -apply (drule mp, fast)+
   3.111 -apply safe
   3.112 -apply (rename_tac S1 S2)
   3.113 -apply (rule_tac x = "%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x) " in exI)
   3.114 -apply auto
   3.115 -done
   3.116 -
   3.117 -
   3.118 -(* lemmas for subst_to_scheme *)
   3.119 -
   3.120 -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)  
   3.121 -                                                  (bound_typ_inst (%k. TVar (k + n)) sch) = sch"
   3.122 -apply (induct_tac "sch")
   3.123 -apply (simp (no_asm) add: le_def)
   3.124 -apply (simp (no_asm) add: le_add2 diff_add_inverse2)
   3.125 -apply (simp (no_asm_simp))
   3.126 -done
   3.127 -
   3.128 -lemma aux: "t = t' ==>  
   3.129 -      subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t =  
   3.130 -      subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) t'"
   3.131 -apply fast
   3.132 -done
   3.133 -
   3.134 -lemma aux2 [rule_format]: "new_tv n sch -->  
   3.135 -      subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) =  
   3.136 -       bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch"
   3.137 -apply (induct_tac "sch")
   3.138 -apply auto
   3.139 -done
   3.140 -
   3.141 -
   3.142 -(* lemmata for <= *)
   3.143 -
   3.144 -lemma le_type_scheme_def2: 
   3.145 -  "!!(sch::type_scheme) sch'.  
   3.146 -   (sch' <= sch) = (? B. sch' = bound_scheme_inst B sch)"
   3.147 -
   3.148 -apply (unfold le_type_scheme_def is_bound_typ_instance)
   3.149 -apply (rule iffI)
   3.150 -apply (cut_tac sch = "sch" in fresh_variable_type_schemes)
   3.151 -apply (cut_tac sch = "sch'" in fresh_variable_type_schemes)
   3.152 -apply (drule make_one_new_out_of_two)
   3.153 -apply assumption
   3.154 -apply (erule_tac V = "? n. new_tv n sch'" in thin_rl)
   3.155 -apply (erule exE)
   3.156 -apply (erule allE)
   3.157 -apply (drule mp)
   3.158 -apply (rule_tac x = " (%k. TVar (k + n))" in exI)
   3.159 -apply (rule refl)
   3.160 -apply (erule exE)
   3.161 -apply (erule conjE)+
   3.162 -apply (drule_tac n = "n" in aux)
   3.163 -apply (simp add: subst_to_scheme_inverse)
   3.164 -apply (rule_tac x = " (subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S" in exI)
   3.165 -apply (simp (no_asm_simp) add: aux2)
   3.166 -apply safe
   3.167 -apply (rule_tac x = "%n. bound_typ_inst S (B n) " in exI)
   3.168 -apply (induct_tac "sch")
   3.169 -apply (simp (no_asm))
   3.170 -apply (simp (no_asm))
   3.171 -apply (simp (no_asm_simp))
   3.172 -done
   3.173 -
   3.174 -lemma le_type_eq_is_bound_typ_instance [rule_format (no_asm)]: "(mk_scheme t) <= sch = t <| sch"
   3.175 -apply (unfold is_bound_typ_instance)
   3.176 -apply (simp (no_asm) add: le_type_scheme_def2)
   3.177 -apply (rule iffI)
   3.178 -apply (erule exE)
   3.179 -apply (frule bound_scheme_inst_type)
   3.180 -apply (erule exE)
   3.181 -apply (rule exI)
   3.182 -apply (rule mk_scheme_injective)
   3.183 -apply simp
   3.184 -apply (rotate_tac 1)
   3.185 -apply (rule mp)
   3.186 -prefer 2 apply (assumption)
   3.187 -apply (induct_tac "sch")
   3.188 -apply (simp (no_asm))
   3.189 -apply simp
   3.190 -apply fast
   3.191 -apply (intro strip)
   3.192 -apply simp
   3.193 -apply (erule exE)
   3.194 -apply simp
   3.195 -apply (rule exI)
   3.196 -apply (induct_tac "sch")
   3.197 -apply (simp (no_asm))
   3.198 -apply (simp (no_asm))
   3.199 -apply simp
   3.200 -done
   3.201 -
   3.202 -lemma le_env_Cons: 
   3.203 -  "(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)"
   3.204 -apply (unfold le_env_def)
   3.205 -apply (simp (no_asm))
   3.206 -apply (rule iffI)
   3.207 - apply clarify
   3.208 - apply (rule conjI) 
   3.209 -  apply (erule_tac x = "0" in allE)
   3.210 -  apply simp
   3.211 - apply (rule conjI, assumption)
   3.212 - apply clarify
   3.213 - apply (erule_tac x = "Suc i" in allE) 
   3.214 - apply simp
   3.215 -apply (rule conjI)
   3.216 - apply fast
   3.217 -apply (rule allI)
   3.218 -apply (induct_tac "i")
   3.219 -apply (simp_all (no_asm_simp))
   3.220 -done
   3.221 -declare le_env_Cons [iff]
   3.222 -
   3.223 -lemma is_bound_typ_instance_closed_subst: "t <| sch ==> $S t <| $S sch"
   3.224 -apply (unfold is_bound_typ_instance)
   3.225 -apply (erule exE)
   3.226 -apply (rename_tac "SA") 
   3.227 -apply (simp)
   3.228 -apply (rule_tac x = "$S o SA" in exI)
   3.229 -apply (simp (no_asm))
   3.230 -done
   3.231 -
   3.232 -lemma S_compatible_le_scheme: "!!(sch::type_scheme) sch'. sch' <= sch ==> $S sch' <= $ S sch"
   3.233 -apply (simp add: le_type_scheme_def2)
   3.234 -apply (erule exE)
   3.235 -apply (simp add: substitution_lemma)
   3.236 -apply fast
   3.237 -done
   3.238 -
   3.239 -lemma S_compatible_le_scheme_lists: 
   3.240 - "!!(A::type_scheme list) A'. A' <= A ==> $S A' <= $ S A"
   3.241 -apply (unfold le_env_def app_subst_list)
   3.242 -apply (simp (no_asm) cong add: conj_cong)
   3.243 -apply (fast intro!: S_compatible_le_scheme)
   3.244 -done
   3.245 -
   3.246 -lemma bound_typ_instance_trans: "[| t <| sch; sch <= sch' |] ==> t <| sch'"
   3.247 -apply (unfold le_type_scheme_def)
   3.248 -apply fast
   3.249 -done
   3.250 -
   3.251 -lemma le_type_scheme_refl: "sch <= (sch::type_scheme)"
   3.252 -apply (unfold le_type_scheme_def)
   3.253 -apply fast
   3.254 -done
   3.255 -declare le_type_scheme_refl [iff]
   3.256 -
   3.257 -lemma le_env_refl: "A <= (A::type_scheme list)"
   3.258 -apply (unfold le_env_def)
   3.259 -apply fast
   3.260 -done
   3.261 -declare le_env_refl [iff]
   3.262 -
   3.263 -lemma bound_typ_instance_BVar: "sch <= BVar n"
   3.264 -apply (unfold le_type_scheme_def is_bound_typ_instance)
   3.265 -apply (intro strip)
   3.266 -apply (rule_tac x = "%a. t" in exI)
   3.267 -apply (simp (no_asm))
   3.268 -done
   3.269 -declare bound_typ_instance_BVar [iff]
   3.270 -
   3.271 -lemma le_FVar: 
   3.272 - "(sch <= FVar n) = (sch = FVar n)"
   3.273 -apply (unfold le_type_scheme_def is_bound_typ_instance)
   3.274 -apply (induct_tac "sch")
   3.275 -  apply (simp (no_asm))
   3.276 - apply (simp (no_asm))
   3.277 - apply fast
   3.278 -apply simp
   3.279 -apply fast
   3.280 -done
   3.281 -declare le_FVar [simp]
   3.282 -
   3.283 -lemma not_FVar_le_Fun: "~(FVar n <= sch1 =-> sch2)"
   3.284 -apply (unfold le_type_scheme_def is_bound_typ_instance)
   3.285 -apply (simp (no_asm))
   3.286 -done
   3.287 -declare not_FVar_le_Fun [iff]
   3.288 -
   3.289 -lemma not_BVar_le_Fun: "~(BVar n <= sch1 =-> sch2)"
   3.290 -apply (unfold le_type_scheme_def is_bound_typ_instance)
   3.291 -apply (simp (no_asm))
   3.292 -apply (rule_tac x = "TVar n" in exI)
   3.293 -apply (simp (no_asm))
   3.294 -apply fast
   3.295 -done
   3.296 -declare not_BVar_le_Fun [iff]
   3.297 -
   3.298 -lemma Fun_le_FunD: 
   3.299 -  "(sch1 =-> sch2 <= sch1' =-> sch2') ==> sch1 <= sch1' & sch2 <= sch2'"
   3.300 -apply (unfold le_type_scheme_def is_bound_typ_instance)
   3.301 -apply (fastsimp)
   3.302 -done
   3.303 -
   3.304 -lemma scheme_le_Fun [rule_format (no_asm)]: "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)"
   3.305 -apply (induct_tac "sch'")
   3.306 -apply (simp (no_asm_simp))
   3.307 -apply (simp (no_asm_simp))
   3.308 -apply fast
   3.309 -done
   3.310 -
   3.311 -lemma le_type_scheme_free_tv [rule_format (no_asm)]: "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch"
   3.312 -apply (induct_tac "sch")
   3.313 -  apply (rule allI)
   3.314 -  apply (induct_tac "sch'")
   3.315 -    apply (simp (no_asm))
   3.316 -   apply (simp (no_asm))
   3.317 -  apply (simp (no_asm))
   3.318 - apply (rule allI)
   3.319 - apply (induct_tac "sch'")
   3.320 -   apply (simp (no_asm))
   3.321 -  apply (simp (no_asm))
   3.322 - apply (simp (no_asm))
   3.323 -apply (rule allI)
   3.324 -apply (induct_tac "sch'")
   3.325 -  apply (simp (no_asm))
   3.326 - apply (simp (no_asm))
   3.327 -apply simp
   3.328 -apply (intro strip)
   3.329 -apply (drule Fun_le_FunD)
   3.330 -apply fast
   3.331 -done
   3.332 -
   3.333 -lemma le_env_free_tv [rule_format (no_asm)]: "!A::type_scheme list. A <= B --> free_tv B <= free_tv A"
   3.334 -apply (induct_tac "B")
   3.335 - apply (simp (no_asm))
   3.336 -apply (rule allI)
   3.337 -apply (induct_tac "A")
   3.338 - apply (simp (no_asm) add: le_env_def)
   3.339 -apply (simp (no_asm))
   3.340 -apply (fast dest: le_type_scheme_free_tv)
   3.341 -done
   3.342 -
   3.343 -
   3.344 -end
     4.1 --- a/src/HOL/MiniML/Maybe.thy	Wed Mar 24 10:55:38 2004 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,51 +0,0 @@
     4.4 -(* Title:     HOL/MiniML/Maybe.thy
     4.5 -   ID:        $Id$
     4.6 -   Author:    Wolfgang Naraschewski and Tobias Nipkow
     4.7 -   Copyright  1996 TU Muenchen
     4.8 -
     4.9 -Universal error monad.
    4.10 -*)
    4.11 -
    4.12 -theory Maybe = Main:
    4.13 -
    4.14 -constdefs
    4.15 -  option_bind :: "['a option, 'a => 'b option] => 'b option"
    4.16 -  "option_bind m f == case m of None => None | Some r => f r"
    4.17 -
    4.18 -syntax "@option_bind" :: "[pttrns,'a option,'b] => 'c" ("(_ := _;//_)" 0)
    4.19 -translations "P := E; F" == "option_bind E (%P. F)"
    4.20 -
    4.21 -
    4.22 -(* constructor laws for option_bind *)
    4.23 -lemma option_bind_Some: "option_bind (Some s) f = (f s)"
    4.24 -apply (unfold option_bind_def)
    4.25 -apply (simp (no_asm))
    4.26 -done
    4.27 -
    4.28 -lemma option_bind_None: "option_bind None f = None"
    4.29 -apply (unfold option_bind_def)
    4.30 -apply (simp (no_asm))
    4.31 -done
    4.32 -
    4.33 -declare option_bind_Some [simp] option_bind_None [simp]
    4.34 -
    4.35 -(* expansion of option_bind *)
    4.36 -lemma split_option_bind: "P(option_bind res f) =  
    4.37 -          ((res = None --> P None) & (!s. res = Some s --> P(f s)))"
    4.38 -apply (unfold option_bind_def)
    4.39 -apply (rule option.split)
    4.40 -done
    4.41 -
    4.42 -lemma option_bind_eq_None: 
    4.43 -  "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))"
    4.44 -apply (simp (no_asm) split add: split_option_bind)
    4.45 -done
    4.46 -
    4.47 -declare option_bind_eq_None [simp]
    4.48 -
    4.49 -(* auxiliary lemma *)
    4.50 -lemma rotate_Some: "(y = Some x) = (Some x = y)"
    4.51 -apply ( simp (no_asm) add: eq_sym_conv)
    4.52 -done
    4.53 -
    4.54 -end
     5.1 --- a/src/HOL/MiniML/MiniML.thy	Wed Mar 24 10:55:38 2004 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,271 +0,0 @@
     5.4 -(* Title:     HOL/MiniML/MiniML.thy
     5.5 -   ID:        $Id$
     5.6 -   Author:    Dieter Nazareth, Wolfgang Naraschewski and Tobias Nipkow
     5.7 -   Copyright  1996 TU Muenchen
     5.8 -
     5.9 -Mini_ML with type inference rules.
    5.10 -*)
    5.11 -
    5.12 -theory MiniML = Generalize:
    5.13 -
    5.14 -(* expressions *)
    5.15 -datatype
    5.16 -        expr = Var nat | Abs expr | App expr expr | LET expr expr
    5.17 -
    5.18 -(* type inference rules *)
    5.19 -consts
    5.20 -        has_type :: "(ctxt * expr * typ)set"
    5.21 -syntax
    5.22 -        "@has_type" :: "[ctxt, expr, typ] => bool"
    5.23 -                       ("((_) |-/ (_) :: (_))" [60,0,60] 60)
    5.24 -translations 
    5.25 -        "A |- e :: t" == "(A,e,t):has_type"
    5.26 -
    5.27 -inductive has_type
    5.28 -intros
    5.29 -  VarI: "[| n < length A; t <| A!n |] ==> A |- Var n :: t"
    5.30 -  AbsI: "[| (mk_scheme t1)#A |- e :: t2 |] ==> A |- Abs e :: t1 -> t2"
    5.31 -  AppI: "[| A |- e1 :: t2 -> t1; A |- e2 :: t2 |] 
    5.32 -         ==> A |- App e1 e2 :: t1"
    5.33 -  LETI: "[| A |- e1 :: t1; (gen A t1)#A |- e2 :: t |] ==> A |- LET e1 e2 :: t"
    5.34 -
    5.35 -
    5.36 -declare has_type.intros [simp]
    5.37 -declare Un_upper1 [simp] Un_upper2 [simp]
    5.38 -
    5.39 -declare is_bound_typ_instance_closed_subst [simp]
    5.40 -
    5.41 -
    5.42 -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"
    5.43 -apply (rule typ_substitutions_only_on_free_variables)
    5.44 -apply (simp add: Ball_def)
    5.45 -done
    5.46 -
    5.47 -declare s'_t_equals_s_t [simp]
    5.48 -
    5.49 -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"
    5.50 -apply (rule scheme_list_substitutions_only_on_free_variables)
    5.51 -apply (simp add: Ball_def)
    5.52 -done
    5.53 -
    5.54 -declare s'_a_equals_s_a [simp]
    5.55 -
    5.56 -lemma replace_s_by_s': 
    5.57 - "$(%n. if n : (free_tv A) Un (free_tv t) then S n else TVar n) A |-  
    5.58 -     e :: $(%n. if n : (free_tv A) Un (free_tv t) then S n else TVar n) t  
    5.59 -  ==> $S A |- e :: $S t"
    5.60 -
    5.61 -apply (rule_tac P = "%A. A |- e :: $S t" in ssubst)
    5.62 -apply (rule s'_a_equals_s_a [symmetric])
    5.63 -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)
    5.64 -apply (rule s'_t_equals_s_t [symmetric])
    5.65 -apply simp
    5.66 -done
    5.67 -
    5.68 -lemma alpha_A': "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = $ id_subst A"
    5.69 -apply (rule scheme_list_substitutions_only_on_free_variables)
    5.70 -apply (simp add: id_subst_def)
    5.71 -done
    5.72 -
    5.73 -lemma alpha_A: "!!A::type_scheme list. $ (%x. TVar (if x : free_tv A then x else n + x)) A = A"
    5.74 -apply (rule alpha_A' [THEN ssubst])
    5.75 -apply simp
    5.76 -done
    5.77 -
    5.78 -lemma S_o_alpha_typ: "$ (S o alpha) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)"
    5.79 -apply (induct_tac "t")
    5.80 -apply (simp_all)
    5.81 -done
    5.82 -
    5.83 -lemma S_o_alpha_typ': "$ (%u. (S o alpha) u) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)"
    5.84 -apply (induct_tac "t")
    5.85 -apply (simp_all)
    5.86 -done
    5.87 -
    5.88 -lemma S_o_alpha_type_scheme: "$ (S o alpha) (sch::type_scheme) = $ S ($ (%x. TVar (alpha x)) sch)"
    5.89 -apply (induct_tac "sch")
    5.90 -apply (simp_all)
    5.91 -done
    5.92 -
    5.93 -lemma S_o_alpha_type_scheme_list: "$ (S o alpha) (A::type_scheme list) = $ S ($ (%x. TVar (alpha x)) A)"
    5.94 -apply (induct_tac "A")
    5.95 -apply (simp_all) 
    5.96 -apply (rule S_o_alpha_type_scheme [unfolded o_def])
    5.97 -done
    5.98 -
    5.99 -lemma S'_A_eq_S'_alpha_A: "!!A::type_scheme list.  
   5.100 -      $ (%n. if n : free_tv A Un free_tv t then S n else TVar n) A =  
   5.101 -      $ ((%x. if x : free_tv A Un free_tv t then S x else TVar x) o  
   5.102 -         (%x. if x : free_tv A then x else n + x)) A"
   5.103 -apply (subst S_o_alpha_type_scheme_list)
   5.104 -apply (subst alpha_A)
   5.105 -apply (rule refl)
   5.106 -done
   5.107 -
   5.108 -lemma dom_S': 
   5.109 - "dom (%n. if n : free_tv A Un free_tv t then S n else TVar n) <=  
   5.110 -  free_tv A Un free_tv t"
   5.111 -apply (unfold free_tv_subst dom_def)
   5.112 -apply (simp (no_asm))
   5.113 -apply fast
   5.114 -done
   5.115 -
   5.116 -lemma cod_S': 
   5.117 -  "!!(A::type_scheme list) (t::typ).   
   5.118 -   cod (%n. if n : free_tv A Un free_tv t then S n else TVar n) <=  
   5.119 -   free_tv ($ S A) Un free_tv ($ S t)"
   5.120 -apply (unfold free_tv_subst cod_def subset_def)
   5.121 -apply (rule ballI)
   5.122 -apply (erule UN_E)
   5.123 -apply (drule dom_S' [THEN subsetD])
   5.124 -apply simp
   5.125 -apply (fast dest: free_tv_of_substitutions_extend_to_scheme_lists intro: free_tv_of_substitutions_extend_to_types [THEN subsetD])
   5.126 -done
   5.127 -
   5.128 -lemma free_tv_S': 
   5.129 - "!!(A::type_scheme list) (t::typ).  
   5.130 -  free_tv (%n. if n : free_tv A Un free_tv t then S n else TVar n) <=  
   5.131 -  free_tv A Un free_tv ($ S A) Un free_tv t Un free_tv ($ S t)"
   5.132 -apply (unfold free_tv_subst)
   5.133 -apply (fast dest: dom_S' [THEN subsetD] cod_S' [THEN subsetD])
   5.134 -done
   5.135 -
   5.136 -lemma free_tv_alpha: "!!t1::typ.  
   5.137 -      (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <=  
   5.138 -          {x. ? y. x = n + y}"
   5.139 -apply (induct_tac "t1")
   5.140 -apply (simp (no_asm))
   5.141 -apply fast
   5.142 -apply (simp (no_asm))
   5.143 -apply fast
   5.144 -done
   5.145 -
   5.146 -lemma aux_plus: "!!(k::nat). n <= n + k"
   5.147 -apply (induct_tac "k" rule: nat_induct)
   5.148 -apply (simp (no_asm))
   5.149 -apply (simp (no_asm_simp))
   5.150 -done
   5.151 -
   5.152 -declare aux_plus [simp]
   5.153 -
   5.154 -lemma new_tv_Int_free_tv_empty_type: "!!t::typ. new_tv n t ==> {x. ? y. x = n + y} Int free_tv t = {}"
   5.155 -apply safe
   5.156 -apply (cut_tac aux_plus)
   5.157 -apply (drule new_tv_le)
   5.158 -apply assumption
   5.159 -apply (rotate_tac 1)
   5.160 -apply (drule new_tv_not_free_tv)
   5.161 -apply fast
   5.162 -done
   5.163 -
   5.164 -lemma new_tv_Int_free_tv_empty_scheme: "!!sch::type_scheme. new_tv n sch ==> {x. ? y. x = n + y} Int free_tv sch = {}"
   5.165 -apply safe
   5.166 -apply (cut_tac aux_plus)
   5.167 -apply (drule new_tv_le)
   5.168 -apply assumption
   5.169 -apply (rotate_tac 1)
   5.170 -apply (drule new_tv_not_free_tv)
   5.171 -apply fast
   5.172 -done
   5.173 -
   5.174 -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 = {}"
   5.175 -apply (rule allI)
   5.176 -apply (induct_tac "A")
   5.177 -apply (simp (no_asm))
   5.178 -apply (simp (no_asm))
   5.179 -apply (fast dest: new_tv_Int_free_tv_empty_scheme)
   5.180 -done
   5.181 -
   5.182 -lemma gen_t_le_gen_alpha_t [rule_format (no_asm)]: 
   5.183 -   "new_tv n A --> gen A t <= gen A ($ (%x. TVar (if x : free_tv A then x else n + x)) t)"
   5.184 -apply (unfold le_type_scheme_def is_bound_typ_instance)
   5.185 -apply (intro strip)
   5.186 -apply (erule exE)
   5.187 -apply (hypsubst)
   5.188 -apply (rule_tac x = " (%x. S (if n <= x then x - n else x))" in exI)
   5.189 -apply (induct_tac "t")
   5.190 -apply (simp (no_asm))
   5.191 -apply (case_tac "nat : free_tv A")
   5.192 -apply (simp (no_asm_simp))
   5.193 -apply (subgoal_tac "n <= n + nat")
   5.194 -apply (drule new_tv_le)
   5.195 -apply assumption
   5.196 -apply (drule new_tv_not_free_tv)
   5.197 -apply (drule new_tv_not_free_tv)
   5.198 -apply (simp (no_asm_simp) add: diff_add_inverse)
   5.199 -apply (simp (no_asm))
   5.200 -apply (simp (no_asm_simp))
   5.201 -done
   5.202 -
   5.203 -declare has_type.intros [intro!]
   5.204 -
   5.205 -lemma has_type_le_env [rule_format (no_asm)]: "A |- e::t ==> !B. A <= B -->  B |- e::t"
   5.206 -apply (erule has_type.induct)
   5.207 -   apply (simp (no_asm) add: le_env_def)
   5.208 -   apply (fastsimp elim: bound_typ_instance_trans)
   5.209 -  apply simp
   5.210 - apply fast
   5.211 -apply (slow elim: le_env_free_tv [THEN free_tv_subset_gen_le])
   5.212 -done
   5.213 -
   5.214 -(* has_type is closed w.r.t. substitution *)
   5.215 -lemma has_type_cl_sub: "A |- e :: t ==> !S. $S A |- e :: $S t"
   5.216 -apply (erule has_type.induct)
   5.217 -(* case VarI *)
   5.218 -   apply (rule allI)
   5.219 -   apply (rule has_type.VarI)
   5.220 -    apply (simp add: app_subst_list)
   5.221 -   apply (simp (no_asm_simp) add: app_subst_list)
   5.222 -  (* case AbsI *)
   5.223 -  apply (rule allI)
   5.224 -  apply (simp (no_asm))
   5.225 -  apply (rule has_type.AbsI)
   5.226 -  apply simp
   5.227 - (* case AppI *)
   5.228 - apply (rule allI)
   5.229 - apply (rule has_type.AppI)
   5.230 -  apply simp
   5.231 -  apply (erule spec)
   5.232 - apply (erule spec)
   5.233 -(* case LetI *)
   5.234 -apply (rule allI)
   5.235 -apply (rule replace_s_by_s')
   5.236 -apply (cut_tac A = "$ S A" and A' = "A" and t = "t" and t' = "$ S t" in ex_fresh_variable)
   5.237 -apply (erule exE)
   5.238 -apply (erule conjE)+ 
   5.239 -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)
   5.240 - 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)
   5.241 - apply (subst S'_A_eq_S'_alpha_A)
   5.242 - apply assumption
   5.243 -apply (subst S_o_alpha_typ)
   5.244 -apply (subst gen_subst_commutes)
   5.245 - apply (rule subset_antisym)
   5.246 -  apply (rule subsetI)
   5.247 -  apply (erule IntE)
   5.248 -  apply (drule free_tv_S' [THEN subsetD])
   5.249 -  apply (drule free_tv_alpha [THEN subsetD])
   5.250 -  apply (simp del: full_SetCompr_eq)
   5.251 -  apply (erule exE)
   5.252 -  apply (hypsubst)
   5.253 -  apply (subgoal_tac "new_tv (n + y) ($ S A) ")
   5.254 -   apply (subgoal_tac "new_tv (n + y) ($ S t) ")
   5.255 -    apply (subgoal_tac "new_tv (n + y) A")
   5.256 -     apply (subgoal_tac "new_tv (n + y) t")
   5.257 -      apply (drule new_tv_not_free_tv)+
   5.258 -      apply fast
   5.259 -     apply (rule new_tv_le) prefer 2 apply assumption apply simp
   5.260 -    apply (rule new_tv_le) prefer 2 apply assumption apply simp
   5.261 -   apply (rule new_tv_le) prefer 2 apply assumption apply simp
   5.262 -  apply (rule new_tv_le) prefer 2 apply assumption apply simp
   5.263 - apply fast
   5.264 -apply (rule has_type_le_env)
   5.265 - apply (drule spec)
   5.266 - apply (drule spec)
   5.267 - apply assumption
   5.268 -apply (rule app_subst_Cons [THEN subst])
   5.269 -apply (rule S_compatible_le_scheme_lists)
   5.270 -apply (simp (no_asm_simp))
   5.271 -done
   5.272 -
   5.273 -
   5.274 -end
     6.1 --- a/src/HOL/MiniML/README.html	Wed Mar 24 10:55:38 2004 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,18 +0,0 @@
     6.4 -<HTML><HEAD><TITLE>HOL/MiniML/README</TITLE></HEAD>
     6.5 -<BODY>
     6.6 -
     6.7 -<H1>Type Inference for MiniML</H1>
     6.8 -
     6.9 -This theory defines the type inference rules and the type inference algorithm
    6.10 -<em>W</em> for MiniML (simply-typed lambda terms with <tt>let</tt>) due to
    6.11 -Milner. It proves the soundness and completeness of <em>W</em> w.r.t. the
    6.12 -rules.
    6.13 -
    6.14 -<P>
    6.15 -
    6.16 -A report describing the theory is found here:<br>
    6.17 -<A HREF = "http://www4.informatik.tu-muenchen.de/~nipkow/pubs/W.html">
    6.18 -Type Inference Verified: Algorithm <i>W</i> in Isabelle/HOL</A>.
    6.19 -
    6.20 -</BODY>
    6.21 -</HTML>
     7.1 --- a/src/HOL/MiniML/ROOT.ML	Wed Mar 24 10:55:38 2004 +0100
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,9 +0,0 @@
     7.4 -(*  Title:      HOL/MiniML/ROOT.ML
     7.5 -    ID:         $Id$
     7.6 -    Author:     Wolfgang Naraschewski and Tobias Nipkow
     7.7 -    Copyright   1995 TUM
     7.8 -
     7.9 -Type inference for MiniML
    7.10 -*)
    7.11 -
    7.12 -time_use_thy "W";
     8.1 --- a/src/HOL/MiniML/Type.thy	Wed Mar 24 10:55:38 2004 +0100
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,918 +0,0 @@
     8.4 -(* Title:     HOL/MiniML/Type.thy
     8.5 -   ID:        $Id$
     8.6 -   Author:    Wolfgang Naraschewski and Tobias Nipkow
     8.7 -   Copyright  1996 TU Muenchen
     8.8 -
     8.9 -MiniML-types and type substitutions.
    8.10 -*)
    8.11 -
    8.12 -theory Type = Maybe:
    8.13 -
    8.14 -(* new class for structures containing type variables *)
    8.15 -axclass  type_struct < type
    8.16 -
    8.17 -
    8.18 -(* type expressions *)
    8.19 -datatype "typ" = TVar nat | "->" "typ" "typ" (infixr 70)
    8.20 -
    8.21 -(* type schemata *)
    8.22 -datatype type_scheme = FVar nat | BVar nat | "=->" type_scheme type_scheme (infixr 70)
    8.23 -
    8.24 -
    8.25 -(* embedding types into type schemata *)    
    8.26 -consts
    8.27 -  mk_scheme :: "typ => type_scheme"
    8.28 -
    8.29 -primrec
    8.30 -  "mk_scheme (TVar n) = (FVar n)"
    8.31 -  "mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))"
    8.32 -
    8.33 -
    8.34 -instance  "typ"::type_struct ..
    8.35 -instance  type_scheme::type_struct ..  
    8.36 -instance  list::(type_struct)type_struct ..
    8.37 -instance  fun::(type,type_struct)type_struct ..
    8.38 -
    8.39 -
    8.40 -(* free_tv s: the type variables occuring freely in the type structure s *)
    8.41 -
    8.42 -consts
    8.43 -  free_tv :: "['a::type_struct] => nat set"
    8.44 -
    8.45 -primrec (free_tv_typ)
    8.46 -  free_tv_TVar:    "free_tv (TVar m) = {m}"
    8.47 -  free_tv_Fun:     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
    8.48 -
    8.49 -primrec (free_tv_type_scheme)
    8.50 -  "free_tv (FVar m) = {m}"
    8.51 -  "free_tv (BVar m) = {}"
    8.52 -  "free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)"
    8.53 -
    8.54 -primrec (free_tv_list)
    8.55 -  "free_tv [] = {}"
    8.56 -  "free_tv (x#l) = (free_tv x) Un (free_tv l)"
    8.57 -
    8.58 -  
    8.59 -(* executable version of free_tv: Implementation with lists *)
    8.60 -consts
    8.61 -  free_tv_ML :: "['a::type_struct] => nat list"
    8.62 -
    8.63 -primrec (free_tv_ML_type_scheme)
    8.64 -  "free_tv_ML (FVar m) = [m]"
    8.65 -  "free_tv_ML (BVar m) = []"
    8.66 -  "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"
    8.67 -
    8.68 -primrec (free_tv_ML_list)
    8.69 -  "free_tv_ML [] = []"
    8.70 -  "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"
    8.71 -
    8.72 -  
    8.73 -(* new_tv s n computes whether n is a new type variable w.r.t. a type 
    8.74 -   structure s, i.e. whether n is greater than any type variable 
    8.75 -   occuring in the type structure *)
    8.76 -constdefs
    8.77 -        new_tv :: "[nat,'a::type_struct] => bool"
    8.78 -        "new_tv n ts == ! m. m:(free_tv ts) --> m<n"
    8.79 -
    8.80 -  
    8.81 -(* bound_tv s: the type variables occuring bound in the type structure s *)
    8.82 -
    8.83 -consts
    8.84 -  bound_tv :: "['a::type_struct] => nat set"
    8.85 -
    8.86 -primrec (bound_tv_type_scheme)
    8.87 -  "bound_tv (FVar m) = {}"
    8.88 -  "bound_tv (BVar m) = {m}"
    8.89 -  "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"
    8.90 -
    8.91 -primrec (bound_tv_list)
    8.92 -  "bound_tv [] = {}"
    8.93 -  "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"
    8.94 -
    8.95 -
    8.96 -(* minimal new free / bound variable *)
    8.97 -
    8.98 -consts
    8.99 -  min_new_bound_tv :: "'a::type_struct => nat"
   8.100 -
   8.101 -primrec (min_new_bound_tv_type_scheme)
   8.102 -  "min_new_bound_tv (FVar n) = 0"
   8.103 -  "min_new_bound_tv (BVar n) = Suc n"
   8.104 -  "min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)"
   8.105 -
   8.106 -
   8.107 -(* substitutions *)
   8.108 -
   8.109 -(* type variable substitution *) 
   8.110 -types
   8.111 -        subst = "nat => typ"
   8.112 -
   8.113 -(* identity *)
   8.114 -constdefs
   8.115 -        id_subst :: subst
   8.116 -        "id_subst == (%n. TVar n)"
   8.117 -
   8.118 -(* extension of substitution to type structures *)
   8.119 -consts
   8.120 -  app_subst :: "[subst, 'a::type_struct] => 'a::type_struct" ("$")
   8.121 -
   8.122 -primrec (app_subst_typ)
   8.123 -  app_subst_TVar: "$ S (TVar n) = S n" 
   8.124 -  app_subst_Fun:  "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" 
   8.125 -
   8.126 -primrec (app_subst_type_scheme)
   8.127 -  "$ S (FVar n) = mk_scheme (S n)"
   8.128 -  "$ S (BVar n) = (BVar n)"
   8.129 -  "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"
   8.130 -
   8.131 -defs
   8.132 -  app_subst_list: "$ S == map ($ S)"
   8.133 -
   8.134 -(* domain of a substitution *)
   8.135 -constdefs
   8.136 -        dom :: "subst => nat set"
   8.137 -        "dom S == {n. S n ~= TVar n}" 
   8.138 -
   8.139 -(* codomain of a substitution: the introduced variables *)
   8.140 -
   8.141 -constdefs
   8.142 -        cod :: "subst => nat set"
   8.143 -        "cod S == (UN m:dom S. (free_tv (S m)))"
   8.144 -
   8.145 -defs
   8.146 -        free_tv_subst:   "free_tv S == (dom S) Un (cod S)" 
   8.147 -
   8.148 -  
   8.149 -(* unification algorithm mgu *)
   8.150 -consts
   8.151 -        mgu :: "[typ,typ] => subst option"
   8.152 -axioms
   8.153 -        mgu_eq:   "mgu t1 t2 = Some U ==> $U t1 = $U t2"
   8.154 -        mgu_mg:   "[| (mgu t1 t2) = Some U; $S t1 = $S t2 |] ==> ? R. S = $R o U"
   8.155 -        mgu_Some:   "$S t1 = $S t2 ==> ? U. mgu t1 t2 = Some U"
   8.156 -        mgu_free: "mgu t1 t2 = Some U ==> (free_tv U) <= (free_tv t1) Un (free_tv t2)"
   8.157 -
   8.158 -
   8.159 -declare mgu_eq [simp] mgu_mg [simp] mgu_free [simp]
   8.160 -
   8.161 -
   8.162 -(* lemmata for make scheme *)
   8.163 -
   8.164 -lemma mk_scheme_Fun [rule_format (no_asm)]: "mk_scheme t = sch1 =-> sch2 --> (? t1 t2. sch1 = mk_scheme t1 & sch2 = mk_scheme t2)"
   8.165 -apply (induct_tac "t")
   8.166 -apply (simp (no_asm))
   8.167 -apply simp
   8.168 -apply fast
   8.169 -done
   8.170 -
   8.171 -lemma mk_scheme_injective [rule_format (no_asm)]: "!t'. mk_scheme t = mk_scheme t' --> t=t'"
   8.172 -apply (induct_tac "t")
   8.173 - apply (rule allI)
   8.174 - apply (induct_tac "t'")
   8.175 -  apply (simp (no_asm))
   8.176 - apply simp
   8.177 -apply (rule allI)
   8.178 -apply (induct_tac "t'")
   8.179 - apply (simp (no_asm))
   8.180 -apply simp
   8.181 -done
   8.182 -
   8.183 -lemma free_tv_mk_scheme: "free_tv (mk_scheme t) = free_tv t"
   8.184 -apply (induct_tac "t")
   8.185 -apply (simp_all (no_asm_simp))
   8.186 -done
   8.187 -
   8.188 -declare free_tv_mk_scheme [simp]
   8.189 -
   8.190 -lemma subst_mk_scheme: "$ S (mk_scheme t) = mk_scheme ($ S t)"
   8.191 -apply (induct_tac "t")
   8.192 -apply (simp_all (no_asm_simp))
   8.193 -done
   8.194 -
   8.195 -declare subst_mk_scheme [simp]
   8.196 -
   8.197 -
   8.198 -(* constructor laws for app_subst *)
   8.199 -
   8.200 -lemma app_subst_Nil: 
   8.201 -  "$ S [] = []"
   8.202 -
   8.203 -apply (unfold app_subst_list)
   8.204 -apply (simp (no_asm))
   8.205 -done
   8.206 -
   8.207 -lemma app_subst_Cons: 
   8.208 -  "$ S (x#l) = ($ S x)#($ S l)"
   8.209 -apply (unfold app_subst_list)
   8.210 -apply (simp (no_asm))
   8.211 -done
   8.212 -
   8.213 -declare app_subst_Nil [simp] app_subst_Cons [simp]
   8.214 -
   8.215 -
   8.216 -(* constructor laws for new_tv *)
   8.217 -
   8.218 -lemma new_tv_TVar: 
   8.219 -  "new_tv n (TVar m) = (m<n)"
   8.220 -
   8.221 -apply (unfold new_tv_def)
   8.222 -apply (fastsimp)
   8.223 -done
   8.224 -
   8.225 -lemma new_tv_FVar: 
   8.226 -  "new_tv n (FVar m) = (m<n)"
   8.227 -apply (unfold new_tv_def)
   8.228 -apply (fastsimp)
   8.229 -done
   8.230 -
   8.231 -lemma new_tv_BVar: 
   8.232 -  "new_tv n (BVar m) = True"
   8.233 -apply (unfold new_tv_def)
   8.234 -apply (simp (no_asm))
   8.235 -done
   8.236 -
   8.237 -lemma new_tv_Fun: 
   8.238 -  "new_tv n (t1 -> t2) = (new_tv n t1 & new_tv n t2)"
   8.239 -apply (unfold new_tv_def)
   8.240 -apply (fastsimp)
   8.241 -done
   8.242 -
   8.243 -lemma new_tv_Fun2: 
   8.244 -  "new_tv n (t1 =-> t2) = (new_tv n t1 & new_tv n t2)"
   8.245 -apply (unfold new_tv_def)
   8.246 -apply (fastsimp)
   8.247 -done
   8.248 -
   8.249 -lemma new_tv_Nil: 
   8.250 -  "new_tv n []"
   8.251 -apply (unfold new_tv_def)
   8.252 -apply (simp (no_asm))
   8.253 -done
   8.254 -
   8.255 -lemma new_tv_Cons: 
   8.256 -  "new_tv n (x#l) = (new_tv n x & new_tv n l)"
   8.257 -apply (unfold new_tv_def)
   8.258 -apply (fastsimp)
   8.259 -done
   8.260 -
   8.261 -lemma new_tv_TVar_subst: "new_tv n TVar"
   8.262 -apply (unfold new_tv_def)
   8.263 -apply (intro strip)
   8.264 -apply (simp add: free_tv_subst dom_def cod_def)
   8.265 -done
   8.266 -
   8.267 -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]
   8.268 -
   8.269 -lemma new_tv_id_subst: 
   8.270 -  "new_tv n id_subst"
   8.271 -apply (unfold id_subst_def new_tv_def free_tv_subst dom_def cod_def)
   8.272 -apply (simp (no_asm))
   8.273 -done
   8.274 -declare new_tv_id_subst [simp]
   8.275 -
   8.276 -lemma new_if_subst_type_scheme: "new_tv n (sch::type_scheme) -->  
   8.277 -      $(%k. if k<n then S k else S' k) sch = $S sch"
   8.278 -apply (induct_tac "sch")
   8.279 -apply (simp_all (no_asm_simp))
   8.280 -done
   8.281 -declare new_if_subst_type_scheme [simp]
   8.282 -
   8.283 -lemma new_if_subst_type_scheme_list: "new_tv n (A::type_scheme list) -->  
   8.284 -      $(%k. if k<n then S k else S' k) A = $S A"
   8.285 -apply (induct_tac "A")
   8.286 -apply (simp_all (no_asm_simp))
   8.287 -done
   8.288 -declare new_if_subst_type_scheme_list [simp]
   8.289 -
   8.290 -
   8.291 -(* constructor laws for dom and cod *)
   8.292 -
   8.293 -lemma dom_id_subst: 
   8.294 -  "dom id_subst = {}"
   8.295 -
   8.296 -apply (unfold dom_def id_subst_def empty_def)
   8.297 -apply (simp (no_asm))
   8.298 -done
   8.299 -declare dom_id_subst [simp]
   8.300 -
   8.301 -lemma cod_id_subst: 
   8.302 -  "cod id_subst = {}"
   8.303 -apply (unfold cod_def)
   8.304 -apply (simp (no_asm))
   8.305 -done
   8.306 -declare cod_id_subst [simp]
   8.307 -
   8.308 -
   8.309 -(* lemmata for free_tv *)
   8.310 -
   8.311 -lemma free_tv_id_subst: 
   8.312 -  "free_tv id_subst = {}"
   8.313 -
   8.314 -apply (unfold free_tv_subst)
   8.315 -apply (simp (no_asm))
   8.316 -done
   8.317 -declare free_tv_id_subst [simp]
   8.318 -
   8.319 -lemma free_tv_nth_A_impl_free_tv_A [rule_format (no_asm)]: "!n. n < length A --> x : free_tv (A!n) --> x : free_tv A"
   8.320 -apply (induct_tac "A")
   8.321 -apply simp
   8.322 -apply (rule allI)
   8.323 -apply (induct_tac "n" rule: nat_induct)
   8.324 -apply simp
   8.325 -apply simp
   8.326 -done
   8.327 -
   8.328 -declare free_tv_nth_A_impl_free_tv_A [simp]
   8.329 -
   8.330 -lemma free_tv_nth_nat_A [rule_format (no_asm)]: "!nat. nat < length A --> x : free_tv (A!nat) --> x : free_tv A"
   8.331 -apply (induct_tac "A")
   8.332 -apply simp
   8.333 -apply (rule allI)
   8.334 -apply (induct_tac "nat" rule: nat_induct)
   8.335 -apply (intro strip)
   8.336 -apply simp
   8.337 -apply (simp (no_asm))
   8.338 -done
   8.339 -
   8.340 -
   8.341 -(* if two substitutions yield the same result if applied to a type
   8.342 -   structure the substitutions coincide on the free type variables
   8.343 -   occurring in the type structure *)
   8.344 -
   8.345 -lemma typ_substitutions_only_on_free_variables [rule_format (no_asm)]: "(!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t"
   8.346 -apply (induct_tac "t")
   8.347 -apply (simp (no_asm))
   8.348 -apply simp
   8.349 -done
   8.350 -
   8.351 -lemma eq_free_eq_subst_te: "(!n. n:(free_tv t) --> S1 n = S2 n) ==> $ S1 (t::typ) = $ S2 t"
   8.352 -apply (rule typ_substitutions_only_on_free_variables)
   8.353 -apply (simp (no_asm) add: Ball_def)
   8.354 -done
   8.355 -
   8.356 -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"
   8.357 -apply (induct_tac "sch")
   8.358 -apply (simp (no_asm))
   8.359 -apply (simp (no_asm))
   8.360 -apply simp
   8.361 -done
   8.362 -
   8.363 -lemma eq_free_eq_subst_type_scheme: 
   8.364 -  "(!n. n:(free_tv sch) --> S1 n = S2 n) ==> $ S1 (sch::type_scheme) = $ S2 sch"
   8.365 -apply (rule scheme_substitutions_only_on_free_variables)
   8.366 -apply (simp (no_asm) add: Ball_def)
   8.367 -done
   8.368 -
   8.369 -lemma eq_free_eq_subst_scheme_list [rule_format (no_asm)]: 
   8.370 -  "(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A"
   8.371 -apply (induct_tac "A")
   8.372 -(* case [] *)
   8.373 -apply (fastsimp)
   8.374 -(* case x#xl *)
   8.375 -apply (fastsimp intro: eq_free_eq_subst_type_scheme)
   8.376 -done
   8.377 -
   8.378 -lemma weaken_asm_Un: "((!x:A. (P x)) --> Q) ==> ((!x:A Un B. (P x)) --> Q)"
   8.379 -apply fast
   8.380 -done
   8.381 -
   8.382 -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"
   8.383 -apply (induct_tac "A")
   8.384 -apply (simp (no_asm))
   8.385 -apply simp
   8.386 -apply (rule weaken_asm_Un)
   8.387 -apply (intro strip)
   8.388 -apply (erule scheme_substitutions_only_on_free_variables)
   8.389 -done
   8.390 -
   8.391 -lemma eq_subst_te_eq_free [rule_format (no_asm)]: 
   8.392 -  "$ S1 (t::typ) = $ S2 t --> n:(free_tv t) --> S1 n = S2 n"
   8.393 -apply (induct_tac "t")
   8.394 -(* case TVar n *)
   8.395 -apply (fastsimp)
   8.396 -(* case Fun t1 t2 *)
   8.397 -apply (fastsimp)
   8.398 -done
   8.399 -
   8.400 -lemma eq_subst_type_scheme_eq_free [rule_format (no_asm)]: 
   8.401 -  "$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n"
   8.402 -apply (induct_tac "sch")
   8.403 -(* case TVar n *)
   8.404 -apply (simp (no_asm_simp))
   8.405 -(* case BVar n *)
   8.406 -apply (intro strip)
   8.407 -apply (erule mk_scheme_injective)
   8.408 -apply (simp (no_asm_simp))
   8.409 -(* case Fun t1 t2 *)
   8.410 -apply simp
   8.411 -done
   8.412 -
   8.413 -lemma eq_subst_scheme_list_eq_free [rule_format (no_asm)]: 
   8.414 -  "$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n"
   8.415 -apply (induct_tac "A")
   8.416 -(* case [] *)
   8.417 -apply (fastsimp)
   8.418 -(* case x#xl *)
   8.419 -apply (fastsimp intro: eq_subst_type_scheme_eq_free)
   8.420 -done
   8.421 -
   8.422 -lemma codD: 
   8.423 -      "v : cod S ==> v : free_tv S"
   8.424 -apply (unfold free_tv_subst)
   8.425 -apply (fast)
   8.426 -done
   8.427 - 
   8.428 -lemma not_free_impl_id: 
   8.429 -      "x ~: free_tv S ==> S x = TVar x"
   8.430 - 
   8.431 -apply (unfold free_tv_subst dom_def)
   8.432 -apply (fast)
   8.433 -done
   8.434 -
   8.435 -lemma free_tv_le_new_tv: 
   8.436 -      "[| new_tv n t; m:free_tv t |] ==> m<n"
   8.437 -apply (unfold new_tv_def)
   8.438 -apply (fast)
   8.439 -done
   8.440 -
   8.441 -lemma cod_app_subst: 
   8.442 -  "[| v : free_tv(S n); v~=n |] ==> v : cod S"
   8.443 -apply (unfold dom_def cod_def UNION_def Bex_def)
   8.444 -apply (simp (no_asm))
   8.445 -apply (safe intro!: exI conjI notI)
   8.446 -prefer 2 apply (assumption)
   8.447 -apply simp
   8.448 -done
   8.449 -declare cod_app_subst [simp]
   8.450 -
   8.451 -lemma free_tv_subst_var: "free_tv (S (v::nat)) <= insert v (cod S)"
   8.452 -apply (case_tac "v:dom S")
   8.453 -apply (fastsimp simp add: cod_def)
   8.454 -apply (fastsimp simp add: dom_def)
   8.455 -done
   8.456 -
   8.457 -lemma free_tv_app_subst_te: "free_tv ($ S (t::typ)) <= cod S Un free_tv t"
   8.458 -apply (induct_tac "t")
   8.459 -(* case TVar n *)
   8.460 -apply (simp (no_asm) add: free_tv_subst_var)
   8.461 -(* case Fun t1 t2 *)
   8.462 -apply (fastsimp)
   8.463 -done
   8.464 -
   8.465 -lemma free_tv_app_subst_type_scheme: "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch"
   8.466 -apply (induct_tac "sch")
   8.467 -(* case FVar n *)
   8.468 -apply (simp (no_asm) add: free_tv_subst_var)
   8.469 -(* case BVar n *)
   8.470 -apply (simp (no_asm))
   8.471 -(* case Fun t1 t2 *)
   8.472 -apply (fastsimp)
   8.473 -done
   8.474 -
   8.475 -lemma free_tv_app_subst_scheme_list: "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A"
   8.476 -apply (induct_tac "A")
   8.477 -(* case [] *)
   8.478 -apply (simp (no_asm))
   8.479 -(* case a#al *)
   8.480 -apply (cut_tac free_tv_app_subst_type_scheme)
   8.481 -apply (fastsimp)
   8.482 -done
   8.483 -
   8.484 -lemma free_tv_comp_subst: 
   8.485 -     "free_tv (%u::nat. $ s1 (s2 u) :: typ) <=    
   8.486 -      free_tv s1 Un free_tv s2"
   8.487 -apply (unfold free_tv_subst dom_def) 
   8.488 -apply (clarsimp simp add: cod_def dom_def)
   8.489 -apply (drule free_tv_app_subst_te [THEN subsetD])
   8.490 -apply clarsimp
   8.491 -apply (auto simp add: cod_def dom_def)
   8.492 -apply (drule free_tv_subst_var [THEN subsetD])
   8.493 -apply (auto simp add: cod_def dom_def)
   8.494 -done
   8.495 -
   8.496 -lemma free_tv_o_subst: 
   8.497 -     "free_tv ($ S1 o S2) <= free_tv S1 Un free_tv (S2 :: nat => typ)"
   8.498 -apply (unfold o_def)
   8.499 -apply (rule free_tv_comp_subst)
   8.500 -done
   8.501 -
   8.502 -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)"
   8.503 -apply (induct_tac "t")
   8.504 -apply (simp (no_asm))
   8.505 -apply (simp (no_asm))
   8.506 -apply fast
   8.507 -done
   8.508 -
   8.509 -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)"
   8.510 -apply (induct_tac "sch")
   8.511 -apply (simp (no_asm))
   8.512 -apply (simp (no_asm))
   8.513 -apply (simp (no_asm))
   8.514 -apply fast
   8.515 -done
   8.516 -
   8.517 -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)"
   8.518 -apply (induct_tac "A")
   8.519 -apply (simp (no_asm))
   8.520 -apply (simp (no_asm))
   8.521 -apply (fast dest: free_tv_of_substitutions_extend_to_schemes)
   8.522 -done
   8.523 -
   8.524 -declare free_tv_of_substitutions_extend_to_scheme_lists [simp]
   8.525 -
   8.526 -lemma free_tv_ML_scheme: "!!sch::type_scheme. (n : free_tv sch) = (n: set (free_tv_ML sch))"
   8.527 -apply (induct_tac "sch")
   8.528 -apply (simp_all (no_asm_simp))
   8.529 -done
   8.530 -
   8.531 -lemma free_tv_ML_scheme_list: "!!A::type_scheme list. (n : free_tv A) = (n: set (free_tv_ML A))"
   8.532 -apply (induct_tac "A")
   8.533 -apply (simp (no_asm))
   8.534 -apply (simp (no_asm_simp) add: free_tv_ML_scheme)
   8.535 -done
   8.536 -
   8.537 -
   8.538 -(* lemmata for bound_tv *)
   8.539 -
   8.540 -lemma bound_tv_mk_scheme: "bound_tv (mk_scheme t) = {}"
   8.541 -apply (induct_tac "t")
   8.542 -apply (simp_all (no_asm_simp))
   8.543 -done
   8.544 -
   8.545 -declare bound_tv_mk_scheme [simp]
   8.546 -
   8.547 -lemma bound_tv_subst_scheme: "!!sch::type_scheme. bound_tv ($ S sch) = bound_tv sch"
   8.548 -apply (induct_tac "sch")
   8.549 -apply (simp_all (no_asm_simp))
   8.550 -done
   8.551 -
   8.552 -declare bound_tv_subst_scheme [simp]
   8.553 -
   8.554 -lemma bound_tv_subst_scheme_list: "!!A::type_scheme list. bound_tv ($ S A) = bound_tv A"
   8.555 -apply (rule list.induct)
   8.556 -apply (simp (no_asm))
   8.557 -apply (simp (no_asm_simp))
   8.558 -done
   8.559 -
   8.560 -declare bound_tv_subst_scheme_list [simp]
   8.561 -
   8.562 -
   8.563 -(* lemmata for new_tv *)
   8.564 -
   8.565 -lemma new_tv_subst: 
   8.566 -  "new_tv n S = ((!m. n <= m --> (S m = TVar m)) &  
   8.567 -                 (! l. l < n --> new_tv n (S l) ))"
   8.568 -
   8.569 -apply (unfold new_tv_def)
   8.570 -apply (safe)
   8.571 -  (* ==> *)
   8.572 -  apply (fastsimp dest: leD simp add: free_tv_subst dom_def)
   8.573 - apply (subgoal_tac "m:cod S | S l = TVar l")
   8.574 -  apply safe
   8.575 -   apply (fastsimp dest: UnI2 simp add: free_tv_subst)
   8.576 -  apply (drule_tac P = "%x. m:free_tv x" in subst , assumption)
   8.577 -  apply simp
   8.578 - apply (fastsimp simp add: free_tv_subst cod_def dom_def)
   8.579 -(* <== *)
   8.580 -apply (unfold free_tv_subst cod_def dom_def)
   8.581 -apply safe
   8.582 - apply (cut_tac m = "m" and n = "n" in less_linear)
   8.583 - apply (fast intro!: less_or_eq_imp_le)
   8.584 -apply (cut_tac m = "ma" and n = "n" in less_linear)
   8.585 -apply (fast intro!: less_or_eq_imp_le) 
   8.586 -done
   8.587 -
   8.588 -lemma new_tv_list: "new_tv n x = (!y:set x. new_tv n y)"
   8.589 -apply (induct_tac "x")
   8.590 -apply (simp_all (no_asm_simp))
   8.591 -done
   8.592 -
   8.593 -(* substitution affects only variables occurring freely *)
   8.594 -lemma subst_te_new_tv: 
   8.595 -  "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t"
   8.596 -apply (induct_tac "t")
   8.597 -apply (simp_all (no_asm_simp))
   8.598 -done
   8.599 -declare subst_te_new_tv [simp]
   8.600 -
   8.601 -lemma subst_te_new_type_scheme [rule_format (no_asm)]: 
   8.602 -  "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch"
   8.603 -apply (induct_tac "sch")
   8.604 -apply (simp_all (no_asm_simp))
   8.605 -done
   8.606 -declare subst_te_new_type_scheme [simp]
   8.607 -
   8.608 -lemma subst_tel_new_scheme_list [rule_format (no_asm)]: 
   8.609 -  "new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A"
   8.610 -apply (induct_tac "A")
   8.611 -apply simp_all
   8.612 -done
   8.613 -declare subst_tel_new_scheme_list [simp]
   8.614 -
   8.615 -(* all greater variables are also new *)
   8.616 -lemma new_tv_le: 
   8.617 -  "n<=m ==> new_tv n t ==> new_tv m t"
   8.618 -apply (unfold new_tv_def)
   8.619 -apply safe
   8.620 -apply (drule spec)
   8.621 -apply (erule (1) notE impE)
   8.622 -apply (simp (no_asm))
   8.623 -done
   8.624 -declare lessI [THEN less_imp_le [THEN new_tv_le], simp]
   8.625 -
   8.626 -lemma new_tv_typ_le: "n<=m ==> new_tv n (t::typ) ==> new_tv m t"
   8.627 -apply (simp (no_asm_simp) add: new_tv_le)
   8.628 -done
   8.629 -
   8.630 -lemma new_scheme_list_le: "n<=m ==> new_tv n (A::type_scheme list) ==> new_tv m A"
   8.631 -apply (simp (no_asm_simp) add: new_tv_le)
   8.632 -done
   8.633 -
   8.634 -lemma new_tv_subst_le: "n<=m ==> new_tv n (S::subst) ==> new_tv m S"
   8.635 -apply (simp (no_asm_simp) add: new_tv_le)
   8.636 -done
   8.637 -
   8.638 -(* new_tv property remains if a substitution is applied *)
   8.639 -lemma new_tv_subst_var: 
   8.640 -  "[| n<m; new_tv m (S::subst) |] ==> new_tv m (S n)"
   8.641 -apply (simp add: new_tv_subst)
   8.642 -done
   8.643 -
   8.644 -lemma new_tv_subst_te [rule_format (no_asm)]: 
   8.645 -  "new_tv n S --> new_tv n (t::typ) --> new_tv n ($ S t)"
   8.646 -apply (induct_tac "t")
   8.647 -apply (fastsimp simp add: new_tv_subst)+
   8.648 -done
   8.649 -declare new_tv_subst_te [simp]
   8.650 -
   8.651 -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)"
   8.652 -apply (induct_tac "sch")
   8.653 -apply (simp_all)
   8.654 -apply (unfold new_tv_def)
   8.655 -apply (simp (no_asm) add: free_tv_subst dom_def cod_def)
   8.656 -apply (intro strip)
   8.657 -apply (case_tac "S nat = TVar nat")
   8.658 -apply simp
   8.659 -apply (drule_tac x = "m" in spec)
   8.660 -apply fast
   8.661 -done
   8.662 -declare new_tv_subst_type_scheme [simp]
   8.663 -
   8.664 -lemma new_tv_subst_scheme_list [rule_format (no_asm)]: 
   8.665 -  "new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)"
   8.666 -apply (induct_tac "A")
   8.667 -apply (fastsimp)+
   8.668 -done
   8.669 -declare new_tv_subst_scheme_list [simp]
   8.670 -
   8.671 -lemma new_tv_Suc_list: "new_tv n A --> new_tv (Suc n) ((TVar n)#A)"
   8.672 -apply (simp (no_asm) add: new_tv_list)
   8.673 -done
   8.674 -
   8.675 -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')"
   8.676 -apply (unfold new_tv_def)
   8.677 -apply (simp (no_asm_simp))
   8.678 -done
   8.679 -
   8.680 -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')"
   8.681 -apply (unfold new_tv_def)
   8.682 -apply (simp (no_asm_simp))
   8.683 -done
   8.684 -
   8.685 -lemma new_tv_nth_nat_A [rule_format (no_asm)]: 
   8.686 -  "!nat. nat < length A --> new_tv n A --> (new_tv n (A!nat))"
   8.687 -apply (unfold new_tv_def)
   8.688 -apply (induct_tac "A")
   8.689 -apply simp
   8.690 -apply (rule allI)
   8.691 -apply (induct_tac "nat" rule: nat_induct)
   8.692 -apply (intro strip)
   8.693 -apply simp
   8.694 -apply (simp (no_asm))
   8.695 -done
   8.696 -
   8.697 -
   8.698 -(* composition of substitutions preserves new_tv proposition *)
   8.699 -lemma new_tv_subst_comp_1: "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (($ R) o S)"
   8.700 -apply (simp add: new_tv_subst)
   8.701 -done
   8.702 -
   8.703 -lemma new_tv_subst_comp_2: "[| new_tv n (S::subst); new_tv n R |] ==> new_tv n (%v.$ R (S v))"
   8.704 -apply (simp add: new_tv_subst)
   8.705 -done
   8.706 -
   8.707 -declare new_tv_subst_comp_1 [simp] new_tv_subst_comp_2 [simp]
   8.708 -
   8.709 -(* new type variables do not occur freely in a type structure *)
   8.710 -lemma new_tv_not_free_tv: 
   8.711 -      "new_tv n A ==> n~:(free_tv A)"
   8.712 -apply (unfold new_tv_def)
   8.713 -apply (fast elim: less_irrefl)
   8.714 -done
   8.715 -declare new_tv_not_free_tv [simp]
   8.716 -
   8.717 -lemma fresh_variable_types: "!!t::typ. ? n. (new_tv n t)"
   8.718 -apply (unfold new_tv_def)
   8.719 -apply (induct_tac "t")
   8.720 -apply (rule_tac x = "Suc nat" in exI)
   8.721 -apply (simp (no_asm_simp))
   8.722 -apply (erule exE)+
   8.723 -apply (rename_tac "n'")
   8.724 -apply (rule_tac x = "max n n'" in exI)
   8.725 -apply (simp (no_asm) add: less_max_iff_disj)
   8.726 -apply blast
   8.727 -done
   8.728 -
   8.729 -declare fresh_variable_types [simp]
   8.730 -
   8.731 -lemma fresh_variable_type_schemes: "!!sch::type_scheme. ? n. (new_tv n sch)"
   8.732 -apply (unfold new_tv_def)
   8.733 -apply (induct_tac "sch")
   8.734 -apply (rule_tac x = "Suc nat" in exI)
   8.735 -apply (simp (no_asm))
   8.736 -apply (rule_tac x = "Suc nat" in exI)
   8.737 -apply (simp (no_asm))
   8.738 -apply (erule exE)+
   8.739 -apply (rename_tac "n'")
   8.740 -apply (rule_tac x = "max n n'" in exI)
   8.741 -apply (simp (no_asm) add: less_max_iff_disj)
   8.742 -apply blast
   8.743 -done
   8.744 -
   8.745 -declare fresh_variable_type_schemes [simp]
   8.746 -
   8.747 -lemma fresh_variable_type_scheme_lists: "!!A::type_scheme list. ? n. (new_tv n A)"
   8.748 -apply (induct_tac "A")
   8.749 -apply (simp (no_asm))
   8.750 -apply (simp (no_asm))
   8.751 -apply (erule exE)
   8.752 -apply (cut_tac sch = "a" in fresh_variable_type_schemes)
   8.753 -apply (erule exE)
   8.754 -apply (rename_tac "n'")
   8.755 -apply (rule_tac x = " (max n n') " in exI)
   8.756 -apply (subgoal_tac "n <= (max n n') ")
   8.757 -apply (subgoal_tac "n' <= (max n n') ")
   8.758 -apply (fast dest: new_tv_le)
   8.759 -apply (simp_all (no_asm) add: le_max_iff_disj)
   8.760 -done
   8.761 -
   8.762 -declare fresh_variable_type_scheme_lists [simp]
   8.763 -
   8.764 -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)"
   8.765 -apply (erule exE)+
   8.766 -apply (rename_tac "n1" "n2")
   8.767 -apply (rule_tac x = " (max n1 n2) " in exI)
   8.768 -apply (subgoal_tac "n1 <= max n1 n2")
   8.769 -apply (subgoal_tac "n2 <= max n1 n2")
   8.770 -apply (fast dest: new_tv_le)
   8.771 -apply (simp_all (no_asm) add: le_max_iff_disj)
   8.772 -done
   8.773 -
   8.774 -lemma ex_fresh_variable: "!!(A::type_scheme list) (A'::type_scheme list) (t::typ) (t'::typ).  
   8.775 -          ? n. (new_tv n A) & (new_tv n A') & (new_tv n t) & (new_tv n t')"
   8.776 -apply (cut_tac t = "t" in fresh_variable_types)
   8.777 -apply (cut_tac t = "t'" in fresh_variable_types)
   8.778 -apply (drule make_one_new_out_of_two)
   8.779 -apply assumption
   8.780 -apply (erule_tac V = "? n. new_tv n t'" in thin_rl)
   8.781 -apply (cut_tac A = "A" in fresh_variable_type_scheme_lists)
   8.782 -apply (cut_tac A = "A'" in fresh_variable_type_scheme_lists)
   8.783 -apply (rotate_tac 1)
   8.784 -apply (drule make_one_new_out_of_two)
   8.785 -apply assumption
   8.786 -apply (erule_tac V = "? n. new_tv n A'" in thin_rl)
   8.787 -apply (erule exE)+
   8.788 -apply (rename_tac n2 n1)
   8.789 -apply (rule_tac x = " (max n1 n2) " in exI)
   8.790 -apply (unfold new_tv_def)
   8.791 -apply (simp (no_asm) add: less_max_iff_disj)
   8.792 -apply blast
   8.793 -done
   8.794 -
   8.795 -(* mgu does not introduce new type variables *)
   8.796 -lemma mgu_new: 
   8.797 -      "[|mgu t1 t2 = Some u; new_tv n t1; new_tv n t2|] ==> new_tv n u"
   8.798 -apply (unfold new_tv_def)
   8.799 -apply (fast dest: mgu_free)
   8.800 -done
   8.801 -
   8.802 -
   8.803 -(* lemmata for substitutions *)
   8.804 -
   8.805 -lemma length_app_subst_list: 
   8.806 -   "!!A:: ('a::type_struct) list. length ($ S A) = length A"
   8.807 -
   8.808 -apply (unfold app_subst_list)
   8.809 -apply (simp (no_asm))
   8.810 -done
   8.811 -declare length_app_subst_list [simp]
   8.812 -
   8.813 -lemma subst_TVar_scheme: "!!sch::type_scheme. $ TVar sch = sch"
   8.814 -apply (induct_tac "sch")
   8.815 -apply (simp_all (no_asm_simp))
   8.816 -done
   8.817 -
   8.818 -declare subst_TVar_scheme [simp]
   8.819 -
   8.820 -lemma subst_TVar_scheme_list: "!!A::type_scheme list. $ TVar A = A"
   8.821 -apply (rule list.induct)
   8.822 -apply (simp_all add: app_subst_list)
   8.823 -done
   8.824 -
   8.825 -declare subst_TVar_scheme_list [simp]
   8.826 -
   8.827 -(* application of id_subst does not change type expression *)
   8.828 -lemma app_subst_id_te: 
   8.829 -  "$ id_subst = (%t::typ. t)"
   8.830 -apply (unfold id_subst_def)
   8.831 -apply (rule ext)
   8.832 -apply (induct_tac "t")
   8.833 -apply (simp_all (no_asm_simp))
   8.834 -done
   8.835 -declare app_subst_id_te [simp]
   8.836 -
   8.837 -lemma app_subst_id_type_scheme: 
   8.838 -  "$ id_subst = (%sch::type_scheme. sch)"
   8.839 -apply (unfold id_subst_def)
   8.840 -apply (rule ext)
   8.841 -apply (induct_tac "sch")
   8.842 -apply (simp_all (no_asm_simp))
   8.843 -done
   8.844 -declare app_subst_id_type_scheme [simp]
   8.845 -
   8.846 -(* application of id_subst does not change list of type expressions *)
   8.847 -lemma app_subst_id_tel: 
   8.848 -  "$ id_subst = (%A::type_scheme list. A)"
   8.849 -apply (unfold app_subst_list)
   8.850 -apply (rule ext)
   8.851 -apply (induct_tac "A")
   8.852 -apply (simp_all (no_asm_simp))
   8.853 -done
   8.854 -declare app_subst_id_tel [simp]
   8.855 -
   8.856 -lemma id_subst_sch: "!!sch::type_scheme. $ id_subst sch = sch"
   8.857 -apply (induct_tac "sch")
   8.858 -apply (simp_all add: id_subst_def)
   8.859 -done
   8.860 -
   8.861 -declare id_subst_sch [simp]
   8.862 -
   8.863 -lemma id_subst_A: "!!A::type_scheme list. $ id_subst A = A"
   8.864 -apply (induct_tac "A")
   8.865 -apply simp
   8.866 -apply simp
   8.867 -done
   8.868 -
   8.869 -declare id_subst_A [simp]
   8.870 -
   8.871 -(* composition of substitutions *)
   8.872 -lemma o_id_subst: "$S o id_subst = S"
   8.873 -apply (unfold id_subst_def o_def)
   8.874 -apply (rule ext)
   8.875 -apply (simp (no_asm))
   8.876 -done
   8.877 -declare o_id_subst [simp]
   8.878 -
   8.879 -lemma subst_comp_te: "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t"
   8.880 -apply (induct_tac "t")
   8.881 -apply (simp_all (no_asm_simp))
   8.882 -done
   8.883 -
   8.884 -lemma subst_comp_type_scheme: "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch"
   8.885 -apply (induct_tac "sch")
   8.886 -apply simp_all
   8.887 -done
   8.888 -
   8.889 -lemma subst_comp_scheme_list: 
   8.890 -  "$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A"
   8.891 -apply (unfold app_subst_list)
   8.892 -apply (induct_tac "A")
   8.893 -(* case [] *)
   8.894 -apply (simp (no_asm))
   8.895 -(* case x#xl *)
   8.896 -apply (simp add: subst_comp_type_scheme)
   8.897 -done
   8.898 -
   8.899 -lemma subst_id_on_type_scheme_list': "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = $ id_subst A"
   8.900 -apply (rule scheme_list_substitutions_only_on_free_variables)
   8.901 -apply (simp add: id_subst_def)
   8.902 -done
   8.903 -
   8.904 -lemma subst_id_on_type_scheme_list: "!!A::type_scheme list. !x : free_tv A. S x = (TVar x) ==> $ S A = A"
   8.905 -apply (subst subst_id_on_type_scheme_list')
   8.906 -apply assumption
   8.907 -apply (simp (no_asm))
   8.908 -done
   8.909 -
   8.910 -lemma nth_subst [rule_format (no_asm)]: "!n. n < length A --> ($ S A)!n = $S (A!n)"
   8.911 -apply (induct_tac "A")
   8.912 -apply simp
   8.913 -apply (rule allI)
   8.914 -apply (rename_tac "n1")
   8.915 -apply (induct_tac "n1" rule: nat_induct)
   8.916 -apply simp
   8.917 -apply simp
   8.918 -done
   8.919 -
   8.920 -
   8.921 -end
     9.1 --- a/src/HOL/MiniML/W.thy	Wed Mar 24 10:55:38 2004 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,568 +0,0 @@
     9.4 -(* Title:     HOL/MiniML/W.thy
     9.5 -   ID:        $Id$
     9.6 -   Author:    Dieter Nazareth, Wolfgang Naraschewski and Tobias Nipkow
     9.7 -   Copyright  1996 TU Muenchen
     9.8 -
     9.9 -Correctness and completeness of type inference algorithm W
    9.10 -*)
    9.11 -
    9.12 -
    9.13 -theory W = MiniML:
    9.14 -
    9.15 -types result_W = "(subst * typ * nat)option"
    9.16 -
    9.17 --- "type inference algorithm W"
    9.18 -consts W :: "[expr, ctxt, nat] => result_W"
    9.19 -
    9.20 -primrec
    9.21 -  "W (Var i) A n =  
    9.22 -     (if i < length A then Some( id_subst,   
    9.23 -	                         bound_typ_inst (%b. TVar(b+n)) (A!i),   
    9.24 -	                         n + (min_new_bound_tv (A!i)) )  
    9.25 -	              else None)"
    9.26 -  
    9.27 -  "W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);
    9.28 -                     Some( S, (S n) -> t, m) )"
    9.29 -  
    9.30 -  "W (App e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
    9.31 -                         (S2,t2,m2) := W e2 ($S1 A) m1;
    9.32 -                         U := mgu ($S2 t1) (t2 -> (TVar m2));
    9.33 -                         Some( $U o $S2 o S1, U m2, Suc m2) )"
    9.34 -  
    9.35 -  "W (LET e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
    9.36 -                         (S2,t2,m2) := W e2 ((gen ($S1 A) t1)#($S1 A)) m1;
    9.37 -                         Some( $S2 o S1, t2, m2) )"
    9.38 -
    9.39 -
    9.40 -declare Suc_le_lessD [simp]
    9.41 -declare less_imp_le [simp del]  (*the combination loops*)
    9.42 -
    9.43 -inductive_cases has_type_casesE:
    9.44 -"A |- Var n :: t"
    9.45 -"A |- Abs e :: t"
    9.46 -"A |- App e1 e2 ::t"
    9.47 -"A |- LET e1 e2 ::t"
    9.48 -
    9.49 -
    9.50 -(* the resulting type variable is always greater or equal than the given one *)
    9.51 -lemma W_var_ge [rule_format (no_asm)]: "!A n S t m. W e A n  = Some (S,t,m) --> n<=m"
    9.52 -apply (induct_tac "e")
    9.53 -(* case Var(n) *)
    9.54 -apply (simp (no_asm) split add: split_option_bind)
    9.55 -(* case Abs e *)
    9.56 -apply (simp (no_asm) split add: split_option_bind)
    9.57 -apply (fast dest: Suc_leD)
    9.58 -(* case App e1 e2 *)
    9.59 -apply (simp (no_asm) split add: split_option_bind)
    9.60 -apply (blast intro: le_SucI le_trans)
    9.61 -(* case LET e1 e2 *)
    9.62 -apply (simp (no_asm) split add: split_option_bind)
    9.63 -apply (blast intro: le_trans)
    9.64 -done
    9.65 -
    9.66 -declare W_var_ge [simp]
    9.67 -
    9.68 -lemma W_var_geD: "Some (S,t,m) = W e A n ==> n<=m"
    9.69 -apply (simp add: eq_sym_conv)
    9.70 -done
    9.71 -
    9.72 -lemma new_tv_compatible_W: "new_tv n A ==> Some (S,t,m) = W e A n ==> new_tv m A"
    9.73 -apply (drule W_var_geD)
    9.74 -apply (rule new_scheme_list_le)
    9.75 -apply assumption
    9.76 -apply assumption
    9.77 -done
    9.78 -
    9.79 -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)"
    9.80 -apply (induct_tac "sch")
    9.81 -  apply simp
    9.82 - apply (simp add: add_commute)
    9.83 -apply (intro strip)
    9.84 -apply simp
    9.85 -apply (erule conjE)
    9.86 -apply (rule conjI)
    9.87 - apply (rule new_tv_le)
    9.88 -  prefer 2 apply (assumption)
    9.89 - apply (rule add_le_mono)
    9.90 -  apply (simp (no_asm))
    9.91 - apply (simp (no_asm) add: max_def)
    9.92 -apply (rule new_tv_le)
    9.93 - prefer 2 apply (assumption)
    9.94 -apply (rule add_le_mono)
    9.95 - apply (simp (no_asm))
    9.96 -apply (simp (no_asm) add: max_def)
    9.97 -done
    9.98 -
    9.99 -declare new_tv_bound_typ_inst_sch [simp]
   9.100 -
   9.101 -(* resulting type variable is new *)
   9.102 -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) -->     
   9.103 -                  new_tv m S & new_tv m t"
   9.104 -apply (induct_tac "e")
   9.105 -(* case Var n *)
   9.106 -apply (simp (no_asm) split add: split_option_bind)
   9.107 -apply (intro strip)
   9.108 -apply (drule new_tv_nth_nat_A)
   9.109 -apply assumption
   9.110 -apply (simp (no_asm_simp))
   9.111 -(* case Abs e *)
   9.112 -apply (simp (no_asm) add: new_tv_subst new_tv_Suc_list split add: split_option_bind)
   9.113 -apply (intro strip)
   9.114 -apply (erule_tac x = "Suc n" in allE)
   9.115 -apply (erule_tac x = " (FVar n) #A" in allE)
   9.116 -apply (fastsimp simp add: new_tv_subst new_tv_Suc_list)
   9.117 -(* case App e1 e2 *)
   9.118 -apply (simp (no_asm) split add: split_option_bind)
   9.119 -apply (intro strip)
   9.120 -apply (rename_tac S1 t1 n1 S2 t2 n2 S3)
   9.121 -apply (erule_tac x = "n" in allE)
   9.122 -apply (erule_tac x = "A" in allE)
   9.123 -apply (erule_tac x = "S1" in allE)
   9.124 -apply (erule_tac x = "t1" in allE)
   9.125 -apply (erule_tac x = "n1" in allE)
   9.126 -apply (erule_tac x = "n1" in allE)
   9.127 -apply (simp add: eq_sym_conv del: all_simps)
   9.128 -apply (erule_tac x = "$S1 A" in allE)
   9.129 -apply (erule_tac x = "S2" in allE)
   9.130 -apply (erule_tac x = "t2" in allE)
   9.131 -apply (erule_tac x = "n2" in allE)
   9.132 -apply ( simp add: o_def rotate_Some)
   9.133 -apply (rule conjI)
   9.134 -apply (rule new_tv_subst_comp_2)
   9.135 -apply (rule new_tv_subst_comp_2)
   9.136 -apply (rule lessI [THEN less_imp_le, THEN new_tv_le])
   9.137 -apply (rule_tac n = "n1" in new_tv_subst_le)
   9.138 -apply (simp add: rotate_Some)
   9.139 -apply (simp (no_asm_simp))
   9.140 -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]])
   9.141 -apply (erule sym [THEN mgu_new])
   9.142 -apply (blast dest!: W_var_geD
   9.143 -             intro: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te 
   9.144 -                    new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
   9.145 -
   9.146 -apply (erule impE)
   9.147 -apply (blast dest: W_var_geD intro: new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
   9.148 -apply clarsimp
   9.149 -
   9.150 -apply (rule lessI [THEN new_tv_subst_var])
   9.151 -apply (erule sym [THEN mgu_new])
   9.152 -apply (blast dest!: W_var_geD
   9.153 -             intro: lessI [THEN less_imp_le, THEN new_tv_le] new_tv_subst_te 
   9.154 -                    new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
   9.155 -
   9.156 -apply (erule impE)
   9.157 -apply (blast dest: W_var_geD intro: new_tv_subst_scheme_list new_scheme_list_le new_tv_le)
   9.158 -apply clarsimp
   9.159 -
   9.160 --- "41: case LET e1 e2"
   9.161 -apply (simp (no_asm) split add: split_option_bind)
   9.162 -apply (intro strip)
   9.163 -apply (erule allE,erule allE,erule allE,erule allE,erule allE, erule impE, assumption, erule impE, assumption) 
   9.164 -apply (erule conjE)
   9.165 -apply (erule allE,erule allE,erule allE,erule allE,erule allE, erule impE, erule_tac [2] notE impE, tactic "assume_tac 2")
   9.166 -apply (simp only: new_tv_def)
   9.167 -apply (simp (no_asm_simp))
   9.168 -apply (drule W_var_ge)+
   9.169 -apply (rule allI)
   9.170 -apply (intro strip)
   9.171 -apply (simp only: free_tv_subst)
   9.172 -apply (drule free_tv_app_subst_scheme_list [THEN subsetD])
   9.173 -apply (best elim: less_le_trans)
   9.174 -apply (erule conjE)
   9.175 -apply (rule conjI)
   9.176 -apply (simp only: o_def)
   9.177 -apply (rule new_tv_subst_comp_2)
   9.178 -apply (erule W_var_ge [THEN new_tv_subst_le])
   9.179 -apply assumption
   9.180 -apply assumption
   9.181 -apply assumption
   9.182 -done
   9.183 -
   9.184 -
   9.185 -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)"
   9.186 -apply (induct_tac "sch")
   9.187 -apply simp
   9.188 -apply simp
   9.189 -apply (intro strip)
   9.190 -apply (rule exI)
   9.191 -apply (rule refl)
   9.192 -apply simp
   9.193 -done
   9.194 -
   9.195 -declare free_tv_bound_typ_inst1 [simp]
   9.196 -
   9.197 -lemma free_tv_W [rule_format (no_asm)]: "!n A S t m v. W e A n = Some (S,t,m) -->             
   9.198 -          (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A"
   9.199 -apply (induct_tac "e")
   9.200 -(* case Var n *)
   9.201 -apply (simp (no_asm) add: free_tv_subst split add: split_option_bind)
   9.202 -apply (intro strip)
   9.203 -apply (case_tac "v : free_tv (A!nat) ")
   9.204 - apply simp
   9.205 -apply (drule free_tv_bound_typ_inst1)
   9.206 - apply (simp (no_asm) add: o_def)
   9.207 -apply (erule exE)
   9.208 -apply simp
   9.209 -(* case Abs e *)
   9.210 -apply (simp add: free_tv_subst split add: split_option_bind del: all_simps)
   9.211 -apply (intro strip)
   9.212 -apply (rename_tac S t n1 v)
   9.213 -apply (erule_tac x = "Suc n" in allE)
   9.214 -apply (erule_tac x = "FVar n # A" in allE)
   9.215 -apply (erule_tac x = "S" in allE)
   9.216 -apply (erule_tac x = "t" in allE)
   9.217 -apply (erule_tac x = "n1" in allE)
   9.218 -apply (erule_tac x = "v" in allE)
   9.219 -apply (bestsimp intro: cod_app_subst simp add: less_Suc_eq)
   9.220 -(* case App e1 e2 *)
   9.221 -apply (simp (no_asm) split add: split_option_bind del: all_simps)
   9.222 -apply (intro strip)
   9.223 -apply (rename_tac S t n1 S1 t1 n2 S2 v)
   9.224 -apply (erule_tac x = "n" in allE)
   9.225 -apply (erule_tac x = "A" in allE)
   9.226 -apply (erule_tac x = "S" in allE)
   9.227 -apply (erule_tac x = "t" in allE)
   9.228 -apply (erule_tac x = "n1" in allE)
   9.229 -apply (erule_tac x = "n1" in allE)
   9.230 -apply (erule_tac x = "v" in allE)
   9.231 -(* second case *)
   9.232 -apply (erule_tac x = "$ S A" in allE)
   9.233 -apply (erule_tac x = "S1" in allE)
   9.234 -apply (erule_tac x = "t1" in allE)
   9.235 -apply (erule_tac x = "n2" in allE)
   9.236 -apply (erule_tac x = "v" in allE)
   9.237 -apply (intro conjI impI | elim conjE)+
   9.238 - apply (simp add: rotate_Some o_def)
   9.239 - apply (drule W_var_geD)
   9.240 - apply (drule W_var_geD)
   9.241 - apply ( (frule less_le_trans) , (assumption))
   9.242 - apply clarsimp 
   9.243 - apply (drule free_tv_comp_subst [THEN subsetD])
   9.244 - apply (drule sym [THEN mgu_free])
   9.245 - apply clarsimp 
   9.246 - 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)
   9.247 -apply simp
   9.248 -apply (drule sym [THEN W_var_geD])
   9.249 -apply (drule sym [THEN W_var_geD])
   9.250 -apply ( (frule less_le_trans) , (assumption))
   9.251 -apply clarsimp
   9.252 -apply (drule mgu_free)
   9.253 -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)
   9.254 -(* LET e1 e2 *)
   9.255 -apply (simp (no_asm) split add: split_option_bind del: all_simps)
   9.256 -apply (intro strip)
   9.257 -apply (rename_tac S1 t1 n2 S2 t2 n3 v)
   9.258 -apply (erule_tac x = "n" in allE)
   9.259 -apply (erule_tac x = "A" in allE)
   9.260 -apply (erule_tac x = "S1" in allE)
   9.261 -apply (erule_tac x = "t1" in allE)
   9.262 -apply (rotate_tac -1)
   9.263 -apply (erule_tac x = "n2" in allE)
   9.264 -apply (rotate_tac -1)
   9.265 -apply (erule_tac x = "v" in allE)
   9.266 -apply (erule (1) notE impE)
   9.267 -apply (erule allE,erule allE,erule allE,erule allE,erule allE,erule_tac  x = "v" in allE)
   9.268 -apply (erule (1) notE impE)
   9.269 -apply simp
   9.270 -apply (rule conjI)
   9.271 -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)
   9.272 -apply (fast dest!: codD free_tv_app_subst_scheme_list [THEN subsetD] W_var_ge dest: less_le_trans)
   9.273 -done
   9.274 -
   9.275 -lemma weaken_A_Int_B_eq_empty: "(!x. x : A --> x ~: B) ==> A Int B = {}"
   9.276 -apply fast
   9.277 -done
   9.278 -
   9.279 -lemma weaken_not_elem_A_minus_B: "x ~: A | x : B ==> x ~: A - B"
   9.280 -apply fast
   9.281 -done
   9.282 -
   9.283 -(* correctness of W with respect to has_type *)
   9.284 -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"
   9.285 -apply (induct_tac "e")
   9.286 -(* case Var n *)
   9.287 -apply simp
   9.288 -apply (intro strip)
   9.289 -apply (rule has_type.VarI)
   9.290 -apply (simp (no_asm))
   9.291 -apply (simp (no_asm) add: is_bound_typ_instance)
   9.292 -apply (rule exI)
   9.293 -apply (rule refl)
   9.294 -(* case Abs e *)
   9.295 -apply (simp add: app_subst_list split add: split_option_bind)
   9.296 -apply (intro strip)
   9.297 -apply (erule_tac x = " (mk_scheme (TVar n)) # A" in allE)
   9.298 -apply simp
   9.299 -apply (rule has_type.AbsI)
   9.300 -apply (drule le_refl [THEN le_SucI, THEN new_scheme_list_le])
   9.301 -apply (drule sym)
   9.302 -apply (erule allE)+
   9.303 -apply (erule impE)
   9.304 -apply (erule_tac [2] notE impE, tactic "assume_tac 2")
   9.305 -apply (simp (no_asm_simp))
   9.306 -apply assumption
   9.307 -(* case App e1 e2 *)
   9.308 -apply (simp (no_asm) split add: split_option_bind)
   9.309 -apply (intro strip)
   9.310 -apply (rename_tac S1 t1 n1 S2 t2 n2 S3)
   9.311 -apply (rule_tac ?t2.0 = "$ S3 t2" in has_type.AppI)
   9.312 -apply (rule_tac S1 = "S3" in app_subst_TVar [THEN subst])
   9.313 -apply (rule app_subst_Fun [THEN subst])
   9.314 -apply (rule_tac t = "$S3 (t2 -> (TVar n2))" and s = "$S3 ($S2 t1) " in subst)
   9.315 -apply simp
   9.316 -apply (simp only: subst_comp_scheme_list [symmetric] o_def) 
   9.317 -apply ((rule has_type_cl_sub [THEN spec]) , (rule has_type_cl_sub [THEN spec]))
   9.318 -apply (simp add: eq_sym_conv)
   9.319 -apply (simp add: subst_comp_scheme_list [symmetric] o_def has_type_cl_sub eq_sym_conv)
   9.320 -apply (rule has_type_cl_sub [THEN spec])
   9.321 -apply (frule new_tv_W)
   9.322 -apply assumption
   9.323 -apply (drule conjunct1)
   9.324 -apply (frule new_tv_subst_scheme_list)
   9.325 -apply (rule new_scheme_list_le)
   9.326 -apply (rule W_var_ge)
   9.327 -apply assumption
   9.328 -apply assumption
   9.329 -apply (erule thin_rl)
   9.330 -apply (erule allE)+
   9.331 -apply (drule sym)
   9.332 -apply (drule sym)
   9.333 -apply (erule thin_rl)
   9.334 -apply (erule thin_rl)
   9.335 -apply (erule (1) notE impE)
   9.336 -apply (erule (1) notE impE)
   9.337 -apply assumption
   9.338 -(* case Let e1 e2 *)
   9.339 -apply (simp (no_asm) split add: split_option_bind)
   9.340 -apply (intro strip)
   9.341 -(*by (rename_tac "w q m1 S1 t1 m2 S2 t n2" 1); *)
   9.342 -apply (rename_tac S1 t1 m1 S2)
   9.343 -apply (rule_tac ?t1.0 = "$ S2 t1" in has_type.LETI)
   9.344 - apply (simp (no_asm) add: o_def)
   9.345 - apply (simp only: subst_comp_scheme_list [symmetric])
   9.346 - apply (rule has_type_cl_sub [THEN spec])
   9.347 - apply (drule_tac x = "A" in spec)
   9.348 - apply (drule_tac x = "S1" in spec)
   9.349 - apply (drule_tac x = "t1" in spec)
   9.350 - apply (drule_tac x = "m1" in spec)
   9.351 - apply (drule_tac x = "n" in spec)
   9.352 - apply (erule (1) notE impE)
   9.353 - apply (simp add: eq_sym_conv)
   9.354 -apply (simp (no_asm) add: o_def)
   9.355 -apply (simp only: subst_comp_scheme_list [symmetric])
   9.356 -apply (rule gen_subst_commutes [symmetric, THEN subst])
   9.357 - apply (rule_tac [2] app_subst_Cons [THEN subst])
   9.358 - apply (erule_tac [2] thin_rl)
   9.359 - apply (drule_tac [2] x = "gen ($S1 A) t1 # $ S1 A" in spec)
   9.360 - apply (drule_tac [2] x = "S2" in spec)
   9.361 - apply (drule_tac [2] x = "t" in spec)
   9.362 - apply (drule_tac [2] x = "m" in spec)
   9.363 - apply (drule_tac [2] x = "m1" in spec)
   9.364 - apply (frule_tac [2] new_tv_W)
   9.365 -  prefer 2 apply (assumption)
   9.366 - apply (drule_tac [2] conjunct1)
   9.367 - apply (frule_tac [2] new_tv_subst_scheme_list)
   9.368 -  apply (rule_tac [2] new_scheme_list_le)
   9.369 -   apply (rule_tac [2] W_var_ge)
   9.370 -   prefer 2 apply (assumption)
   9.371 -  prefer 2 apply (assumption)
   9.372 - apply (erule_tac [2] impE)
   9.373 -  apply (rule_tac [2] A = "$ S1 A" in new_tv_only_depends_on_free_tv_scheme_list)
   9.374 -   prefer 2 apply simp
   9.375 -   apply (fast)
   9.376 -  prefer 2 apply (assumption)
   9.377 - prefer 2 apply simp
   9.378 -apply (rule weaken_A_Int_B_eq_empty)
   9.379 -apply (rule allI)
   9.380 -apply (intro strip)
   9.381 -apply (rule weaken_not_elem_A_minus_B)
   9.382 -apply (case_tac "x < m1")
   9.383 - apply (rule disjI2)
   9.384 - apply (rule free_tv_gen_cons [THEN subst])
   9.385 - apply (rule free_tv_W)
   9.386 -   apply assumption
   9.387 -  apply simp
   9.388 - apply assumption
   9.389 -apply (rule disjI1)
   9.390 -apply (drule new_tv_W)
   9.391 -apply assumption
   9.392 -apply (drule conjunct2)
   9.393 -apply (rule new_tv_not_free_tv)
   9.394 -apply (rule new_tv_le)
   9.395 - prefer 2 apply (assumption)
   9.396 -apply (simp add: not_less_iff_le)
   9.397 -done
   9.398 -
   9.399 -(* Completeness of W w.r.t. has_type *)
   9.400 -lemma W_complete_lemma [rule_format (no_asm)]: 
   9.401 -  "ALL S' A t' n. $S' A |- e :: t' --> new_tv n A -->      
   9.402 -               (EX S t. (EX m. W e A n = Some (S,t,m)) &   
   9.403 -                       (EX R. $S' A = $R ($S A) & t' = $R t))"
   9.404 -apply (induct_tac "e")
   9.405 -   (* case Var n *)
   9.406 -   apply (intro strip)
   9.407 -   apply (simp (no_asm) cong add: conj_cong)
   9.408 -   apply (erule has_type_casesE)
   9.409 -   apply (simp add: is_bound_typ_instance)
   9.410 -   apply (erule exE)
   9.411 -   apply (hypsubst)
   9.412 -   apply (rename_tac "S")
   9.413 -   apply (rule_tac x = "%x. (if x < n then S' x else S (x - n))" in exI)
   9.414 -   apply (rule conjI)
   9.415 -   apply (simp (no_asm_simp))
   9.416 -   apply (simp (no_asm_simp) add: bound_typ_inst_composed_subst [symmetric] new_tv_nth_nat_A o_def nth_subst 
   9.417 -                             del: bound_typ_inst_composed_subst)
   9.418 -
   9.419 -  (* case Abs e *)
   9.420 -  apply (intro strip)
   9.421 -  apply (erule has_type_casesE)
   9.422 -  apply (erule_tac x = "%x. if x=n then t1 else (S' x) " in allE)
   9.423 -  apply (erule_tac x = " (FVar n) #A" in allE)
   9.424 -  apply (erule_tac x = "t2" in allE)
   9.425 -  apply (erule_tac x = "Suc n" in allE)
   9.426 -  apply (bestsimp dest!: mk_scheme_injective cong: conj_cong split: split_option_bind)
   9.427 -
   9.428 - (* case App e1 e2 *)
   9.429 - apply (intro strip)
   9.430 - apply (erule has_type_casesE)
   9.431 - apply (erule_tac x = "S'" in allE)
   9.432 - apply (erule_tac x = "A" in allE)
   9.433 - apply (erule_tac x = "t2 -> t'" in allE)
   9.434 - apply (erule_tac x = "n" in allE)
   9.435 - apply safe
   9.436 - apply (erule_tac x = "R" in allE)
   9.437 - apply (erule_tac x = "$ S A" in allE)
   9.438 - apply (erule_tac x = "t2" in allE)
   9.439 - apply (erule_tac x = "m" in allE)
   9.440 - apply simp
   9.441 - apply safe
   9.442 -  apply (blast intro: sym [THEN W_var_geD] new_tv_W [THEN conjunct1] new_scheme_list_le new_tv_subst_scheme_list)
   9.443 - 
   9.444 - (** LEVEL 33 **)
   9.445 -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))")
   9.446 -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)
   9.447 -prefer 2 apply (simp (no_asm_simp) add: subst_comp_te) prefer 2
   9.448 -apply (rule_tac [2] eq_free_eq_subst_te)
   9.449 -prefer 2 apply (intro strip) prefer 2
   9.450 -apply (subgoal_tac [2] "na ~=ma")
   9.451 - prefer 3 apply (best dest: new_tv_W sym [THEN W_var_geD] new_tv_not_free_tv new_tv_le)
   9.452 -apply (case_tac [2] "na:free_tv Sa")
   9.453 -(* n1 ~: free_tv S1 *)
   9.454 -apply (frule_tac [3] not_free_impl_id)
   9.455 - prefer 3 apply (simp)
   9.456 -(* na : free_tv Sa *)
   9.457 -apply (drule_tac [2] A1 = "$ S A" in trans [OF _ subst_comp_scheme_list])
   9.458 -apply (drule_tac [2] eq_subst_scheme_list_eq_free)
   9.459 - prefer 2 apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
   9.460 -prefer 2 apply (simp (no_asm_simp)) prefer 2
   9.461 -apply (case_tac [2] "na:dom Sa")
   9.462 -(* na ~: dom Sa *)
   9.463 - prefer 3 apply (simp add: dom_def)
   9.464 -(* na : dom Sa *)
   9.465 -apply (rule_tac [2] eq_free_eq_subst_te)
   9.466 -prefer 2 apply (intro strip) prefer 2
   9.467 -apply (subgoal_tac [2] "nb ~= ma")
   9.468 -apply (frule_tac [3] new_tv_W) prefer 3 apply assumption
   9.469 -apply (erule_tac [3] conjE)
   9.470 -apply (drule_tac [3] new_tv_subst_scheme_list)
   9.471 -   prefer 3 apply (fast intro: new_scheme_list_le dest: sym [THEN W_var_geD])
   9.472 -  prefer 3 apply (fastsimp dest: new_tv_W new_tv_not_free_tv simp add: cod_def free_tv_subst)
   9.473 - prefer 2 apply (fastsimp simp add: cod_def free_tv_subst)
   9.474 -prefer 2 apply (simp (no_asm)) prefer 2
   9.475 -apply (rule_tac [2] eq_free_eq_subst_te)
   9.476 -prefer 2 apply (intro strip) prefer 2
   9.477 -apply (subgoal_tac [2] "na ~= ma")
   9.478 -apply (frule_tac [3] new_tv_W) prefer 3 apply assumption
   9.479 -apply (erule_tac [3] conjE)
   9.480 -apply (drule_tac [3] sym [THEN W_var_geD])
   9.481 - prefer 3 apply (fast dest: new_scheme_list_le new_tv_subst_scheme_list new_tv_W new_tv_not_free_tv)
   9.482 -apply (case_tac [2] "na: free_tv t - free_tv Sa")
   9.483 -(* case na ~: free_tv t - free_tv Sa *)
   9.484 - prefer 3 
   9.485 - apply simp
   9.486 - apply fast
   9.487 -(* case na : free_tv t - free_tv Sa *)
   9.488 -prefer 2 apply simp prefer 2
   9.489 -apply (drule_tac [2] A1 = "$ S A" and r = "$ R ($ S A)" in trans [OF _ subst_comp_scheme_list])
   9.490 -apply (drule_tac [2] eq_subst_scheme_list_eq_free)
   9.491 - prefer 2 
   9.492 - apply (fast intro: free_tv_W free_tv_le_new_tv dest: new_tv_W)
   9.493 -(** LEVEL 73 **)
   9.494 - prefer 2 apply (simp add: free_tv_subst dom_def)
   9.495 -apply (simp (no_asm_simp) split add: split_option_bind)
   9.496 -apply safe
   9.497 -apply (drule mgu_Some)
   9.498 - apply fastsimp  
   9.499 -(** LEVEL 78 *)
   9.500 -apply (drule mgu_mg, assumption)
   9.501 -apply (erule exE)
   9.502 -apply (rule_tac x = "Rb" in exI)
   9.503 -apply (rule conjI)
   9.504 -apply (drule_tac [2] x = "ma" in fun_cong)
   9.505 - prefer 2 apply (simp add: eq_sym_conv)
   9.506 -apply (simp (no_asm) add: subst_comp_scheme_list)
   9.507 -apply (simp (no_asm) add: subst_comp_scheme_list [symmetric])
   9.508 -apply (rule_tac A2 = "($ Sa ($ S A))" in trans [OF _ subst_comp_scheme_list [symmetric]])
   9.509 -apply (simp add: o_def eq_sym_conv)
   9.510 -apply (drule_tac s = "Some ?X" in sym)
   9.511 -apply (rule eq_free_eq_subst_scheme_list)
   9.512 -apply safe
   9.513 -apply (subgoal_tac "ma ~= na")
   9.514 -apply (frule_tac [2] new_tv_W) prefer 2 apply assumption
   9.515 -apply (erule_tac [2] conjE)
   9.516 -apply (drule_tac [2] new_tv_subst_scheme_list)
   9.517 - prefer 2 apply (fast intro: new_scheme_list_le dest: sym [THEN W_var_geD])
   9.518 -apply (frule_tac [2] n = "m" in new_tv_W) prefer 2 apply assumption
   9.519 -apply (erule_tac [2] conjE)
   9.520 -apply (drule_tac [2] free_tv_app_subst_scheme_list [THEN subsetD])
   9.521 - apply (tactic {* 
   9.522 -   (fast_tac (set_cs addDs [sym RS thm "W_var_geD", thm "new_scheme_list_le", thm "codD",
   9.523 -   thm "new_tv_not_free_tv"]) 2) *})
   9.524 -apply (case_tac "na: free_tv t - free_tv Sa")
   9.525 -(* case na ~: free_tv t - free_tv Sa *)
   9.526 - prefer 2 apply simp apply blast
   9.527 -(* case na : free_tv t - free_tv Sa *)
   9.528 -apply simp
   9.529 -apply (drule free_tv_app_subst_scheme_list [THEN subsetD])
   9.530 - apply (fastsimp dest: codD trans [OF _ subst_comp_scheme_list]
   9.531 -                       eq_subst_scheme_list_eq_free 
   9.532 -             simp add: free_tv_subst dom_def)
   9.533 -(* case Let e1 e2 *)
   9.534 -apply (erule has_type_casesE)
   9.535 -apply (erule_tac x = "S'" in allE)
   9.536 -apply (erule_tac x = "A" in allE)
   9.537 -apply (erule_tac x = "t1" in allE)
   9.538 -apply (erule_tac x = "n" in allE)
   9.539 -apply (erule (1) notE impE)
   9.540 -apply (erule (1) notE impE)
   9.541 -apply safe  
   9.542 -apply (simp (no_asm_simp))
   9.543 -apply (erule_tac x = "R" in allE)
   9.544 -apply (erule_tac x = "gen ($ S A) t # $ S A" in allE)
   9.545 -apply (erule_tac x = "t'" in allE)
   9.546 -apply (erule_tac x = "m" in allE)
   9.547 -apply simp
   9.548 -apply (drule mp)
   9.549 -apply (rule has_type_le_env)
   9.550 -apply assumption
   9.551 -apply (simp (no_asm))
   9.552 -apply (rule gen_bound_typ_instance)
   9.553 -apply (drule mp)
   9.554 -apply (frule new_tv_compatible_W)
   9.555 -apply (rule sym)
   9.556 -apply assumption
   9.557 -apply (fast dest: new_tv_compatible_gen new_tv_subst_scheme_list new_tv_W)
   9.558 -apply safe
   9.559 -apply simp
   9.560 -apply (rule_tac x = "Ra" in exI)
   9.561 -apply (simp (no_asm) add: o_def subst_comp_scheme_list [symmetric])
   9.562 -done
   9.563 -
   9.564 -
   9.565 -lemma W_complete: "[] |- e :: t' ==>  (? S t. (? m. W e [] n = Some(S,t,m)) &   
   9.566 -                                  (? R. t' = $ R t))"
   9.567 -apply (cut_tac A = "[]" and S' = "id_subst" and e = "e" and t' = "t'" in W_complete_lemma)
   9.568 -apply simp_all
   9.569 -done
   9.570 -
   9.571 -end
    10.1 --- a/src/HOL/ex/AVL.thy	Wed Mar 24 10:55:38 2004 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,421 +0,0 @@
    10.4 -(*  Title:      HOL/ex/AVL.thy
    10.5 -    ID:         $Id$
    10.6 -    Author:     Cornelia Pusch and Tobias Nipkow, converted to Isar by Gerwin Klein
    10.7 -    Copyright   1998  TUM
    10.8 -*)
    10.9 -
   10.10 -header "AVL Trees"
   10.11 -
   10.12 -theory AVL = Main:
   10.13 -
   10.14 -text {* 
   10.15 -  At the moment only insertion is formalized.
   10.16 -
   10.17 -  This theory would be a nice candidate for structured Isar proof
   10.18 -  texts and for extensions (delete operation). 
   10.19 -*}
   10.20 -
   10.21 -(*
   10.22 -  This version works exclusively with nat. Balance check could be
   10.23 -  simplified by working with int: 
   10.24 -  is_bal (MKT n l r) = (abs(int(height l) - int(height r)) <= 1 & is_bal l & is_bal r)
   10.25 -*)
   10.26 -
   10.27 -datatype tree = ET | MKT nat tree tree
   10.28 -
   10.29 -consts
   10.30 -  height :: "tree \<Rightarrow> nat"
   10.31 -  is_in  :: "nat \<Rightarrow> tree \<Rightarrow> bool"
   10.32 -  is_ord :: "tree \<Rightarrow> bool"
   10.33 -  is_bal :: "tree \<Rightarrow> bool"
   10.34 -
   10.35 -primrec
   10.36 -  "height ET = 0"
   10.37 -  "height (MKT n l r) = 1 + max (height l) (height r)"
   10.38 -
   10.39 -primrec
   10.40 -  "is_in k ET = False"
   10.41 -  "is_in k (MKT n l r) = (k=n \<or> is_in k l \<or> is_in k r)"
   10.42 -
   10.43 -primrec
   10.44 -  "is_ord ET = True"
   10.45 -  "is_ord (MKT n l r) = ((\<forall>n'. is_in n' l \<longrightarrow> n' < n) \<and>
   10.46 -                        (\<forall>n'. is_in n' r \<longrightarrow> n < n') \<and>
   10.47 -                        is_ord l \<and> is_ord r)"
   10.48 -
   10.49 -primrec
   10.50 -  "is_bal ET = True"
   10.51 -  "is_bal (MKT n l r) = ((height l = height r \<or>
   10.52 -                         height l = 1+height r \<or>
   10.53 -                         height r = 1+height l) \<and> 
   10.54 -                         is_bal l \<and> is_bal r)"
   10.55 -
   10.56 -
   10.57 -datatype bal = Just | Left | Right
   10.58 -
   10.59 -constdefs
   10.60 -  bal :: "tree \<Rightarrow> bal"
   10.61 -  "bal t \<equiv> case t of ET \<Rightarrow> Just
   10.62 -                   | (MKT n l r) \<Rightarrow> if height l = height r then Just
   10.63 -                                    else if height l < height r then Right else Left"
   10.64 -
   10.65 -consts
   10.66 -  r_rot  :: "nat \<times> tree \<times> tree \<Rightarrow> tree"
   10.67 -  l_rot  :: "nat \<times> tree \<times> tree \<Rightarrow> tree"
   10.68 -  lr_rot :: "nat \<times> tree \<times> tree \<Rightarrow> tree"
   10.69 -  rl_rot :: "nat \<times> tree \<times> tree \<Rightarrow> tree"
   10.70 -
   10.71 -recdef r_rot "{}"
   10.72 -  "r_rot (n, MKT ln ll lr, r) = MKT ln ll (MKT n lr r)"
   10.73 -
   10.74 -recdef l_rot "{}"
   10.75 -  "l_rot(n, l, MKT rn rl rr) = MKT rn (MKT n l rl) rr"
   10.76 -
   10.77 -recdef lr_rot "{}"
   10.78 -  "lr_rot(n, MKT ln ll (MKT lrn lrl lrr), r) = MKT lrn (MKT ln ll lrl) (MKT n lrr r)"
   10.79 -
   10.80 -recdef rl_rot "{}"
   10.81 -  "rl_rot(n, l, MKT rn (MKT rln rll rlr) rr) = MKT rln (MKT n l rll) (MKT rn rlr rr)"
   10.82 -
   10.83 -
   10.84 -constdefs 
   10.85 -  l_bal :: "nat \<Rightarrow> tree \<Rightarrow> tree \<Rightarrow> tree"
   10.86 -  "l_bal n l r \<equiv> if bal l = Right 
   10.87 -                  then lr_rot (n, l, r)
   10.88 -                  else r_rot (n, l, r)"
   10.89 -
   10.90 -  r_bal :: "nat \<Rightarrow> tree \<Rightarrow> tree \<Rightarrow> tree"
   10.91 -  "r_bal n l r \<equiv> if bal r = Left
   10.92 -                  then rl_rot (n, l, r)
   10.93 -                  else l_rot (n, l, r)"
   10.94 -
   10.95 -consts
   10.96 -  insert :: "nat \<Rightarrow> tree \<Rightarrow> tree"
   10.97 -primrec
   10.98 -"insert x ET = MKT x ET ET"
   10.99 -"insert x (MKT n l r) = 
  10.100 -   (if x=n
  10.101 -    then MKT n l r
  10.102 -    else if x<n
  10.103 -         then let l' = insert x l
  10.104 -              in if height l' = 2+height r
  10.105 -                 then l_bal n l' r
  10.106 -                 else MKT n l' r
  10.107 -         else let r' = insert x r
  10.108 -              in if height r' = 2+height l
  10.109 -                 then r_bal n l r'
  10.110 -                 else MKT n l r')"
  10.111 -
  10.112 -
  10.113 -
  10.114 -subsection "is-bal"
  10.115 -
  10.116 -declare Let_def [simp]
  10.117 -
  10.118 -lemma is_bal_lr_rot: 
  10.119 -"\<lbrakk> height l = Suc(Suc(height r)); bal l = Right; is_bal l; is_bal r \<rbrakk>
  10.120 -  \<Longrightarrow> is_bal (lr_rot (n, l, r))"
  10.121 -apply (unfold bal_def)
  10.122 -apply (cases l)
  10.123 - apply simp
  10.124 -apply (rename_tac t1 t2)
  10.125 -apply (case_tac t2)
  10.126 - apply simp
  10.127 -apply (simp add: max_def split: split_if_asm)
  10.128 -apply arith
  10.129 -done
  10.130 -
  10.131 -
  10.132 -lemma is_bal_r_rot: 
  10.133 -"\<lbrakk> height l = Suc(Suc(height r)); bal l \<noteq> Right; is_bal l; is_bal r \<rbrakk>
  10.134 -  \<Longrightarrow> is_bal (r_rot (n, l, r))"
  10.135 -apply (unfold bal_def)
  10.136 -apply (cases "l")
  10.137 - apply simp
  10.138 -apply (simp add: max_def split: split_if_asm)
  10.139 -done
  10.140 -
  10.141 -
  10.142 -lemma is_bal_rl_rot: 
  10.143 -"\<lbrakk> height r = Suc(Suc(height l)); bal r = Left; is_bal l; is_bal r \<rbrakk>
  10.144 -  \<Longrightarrow> is_bal (rl_rot (n, l, r))"
  10.145 -apply (unfold bal_def)
  10.146 -apply (cases r)
  10.147 - apply simp
  10.148 -apply (rename_tac t1 t2)
  10.149 -apply (case_tac t1)
  10.150 - apply (simp add: max_def split: split_if_asm)
  10.151 -apply (simp add: max_def split: split_if_asm)
  10.152 -apply arith
  10.153 -done
  10.154 -
  10.155 -
  10.156 -lemma is_bal_l_rot: 
  10.157 -"\<lbrakk> height r = Suc(Suc(height l)); bal r \<noteq> Left; is_bal l; is_bal r \<rbrakk>
  10.158 -  \<Longrightarrow> is_bal (l_rot (n, l, r))"
  10.159 -apply (unfold bal_def)
  10.160 -apply (cases r)
  10.161 - apply simp 
  10.162 -apply (simp add: max_def split: split_if_asm)
  10.163 -done
  10.164 -
  10.165 -
  10.166 -text {* Lemmas about height after rotation *}
  10.167 -
  10.168 -lemma height_lr_rot:
  10.169 -"\<lbrakk> bal l = Right; height l = Suc(Suc(height r)) \<rbrakk>
  10.170 - \<Longrightarrow> Suc(height (lr_rot (n, l, r))) = height (MKT n l r) "
  10.171 -apply (unfold bal_def)
  10.172 -apply (cases l)
  10.173 - apply simp
  10.174 -apply (rename_tac t1 t2)
  10.175 -apply (case_tac t2)
  10.176 - apply simp
  10.177 -apply (simp add: max_def split: split_if_asm)
  10.178 -done
  10.179 -
  10.180 -
  10.181 -lemma height_r_rot: 
  10.182 -"\<lbrakk> height l = Suc(Suc(height r)); bal l \<noteq> Right \<rbrakk>
  10.183 -  \<Longrightarrow> Suc(height (r_rot (n, l, r))) = height (MKT n l r) \<or>
  10.184 -          height (r_rot (n, l, r)) = height (MKT n l r)"
  10.185 -apply (unfold bal_def)
  10.186 -apply (cases l)
  10.187 - apply simp 
  10.188 -apply (simp add: max_def split: split_if_asm)
  10.189 -done
  10.190 -
  10.191 -
  10.192 -lemma height_l_bal:
  10.193 -"height l = Suc(Suc(height r))   
  10.194 -  \<Longrightarrow> Suc(height (l_bal n l r)) = height (MKT n l r) |  
  10.195 -          height (l_bal n l r)  = height (MKT n l r)"
  10.196 -apply (unfold l_bal_def)
  10.197 -apply (cases "bal l = Right")
  10.198 - apply (fastsimp dest: height_lr_rot)
  10.199 -apply (fastsimp dest: height_r_rot)
  10.200 -done
  10.201 -
  10.202 -
  10.203 -lemma height_rl_rot [rule_format (no_asm)]: 
  10.204 -"height r = Suc(Suc(height l)) \<longrightarrow> bal r = Left  
  10.205 -  \<longrightarrow> Suc(height (rl_rot (n, l, r)))  = height (MKT n l r)"
  10.206 -apply (unfold bal_def)
  10.207 -apply (cases r)
  10.208 - apply simp
  10.209 -apply (rename_tac t1 t2)
  10.210 -apply (case_tac t1)
  10.211 - apply simp
  10.212 -apply (simp add: max_def split: split_if_asm)
  10.213 -done
  10.214 -
  10.215 -
  10.216 -lemma height_l_rot [rule_format (no_asm)]: 
  10.217 -"height r = Suc(Suc(height l)) \<longrightarrow> bal r \<noteq> Left  
  10.218 - \<longrightarrow> Suc(height (l_rot (n, l, r))) = height (MKT n l r) \<or>  
  10.219 -          height (l_rot (n, l, r)) = height (MKT n l r)"
  10.220 -apply (unfold bal_def)
  10.221 -apply (cases r)
  10.222 - apply simp
  10.223 -apply (simp add: max_def)
  10.224 -done
  10.225 -
  10.226 -
  10.227 -lemma height_r_bal: 
  10.228 -"height r = Suc(Suc(height l))   
  10.229 -  \<Longrightarrow> Suc(height (r_bal n l r)) = height (MKT n l r) \<or>  
  10.230 -          height (r_bal n l r) = height (MKT n l r)"
  10.231 -apply (unfold r_bal_def)
  10.232 -apply (cases "bal r = Left")
  10.233 - apply (fastsimp dest: height_rl_rot)
  10.234 -apply (fastsimp dest: height_l_rot)
  10.235 -done
  10.236 -
  10.237 -lemma height_insert [rule_format (no_asm)]: 
  10.238 -"is_bal t
  10.239 -  \<longrightarrow> height (insert x t) = height t \<or> height (insert x t) = Suc(height t)"
  10.240 -apply (induct_tac "t")
  10.241 - apply simp
  10.242 -apply (rename_tac n t1 t2)
  10.243 -apply (case_tac "x=n")
  10.244 - apply simp
  10.245 -apply (case_tac "x<n")
  10.246 - apply (case_tac "height (insert x t1) = Suc (Suc (height t2))")
  10.247 -  apply (frule_tac n = n in height_l_bal)
  10.248 -  apply (simp add: max_def)
  10.249 -  apply fastsimp
  10.250 - apply (simp add: max_def)
  10.251 - apply fastsimp
  10.252 -apply (case_tac "height (insert x t2) = Suc (Suc (height t1))")
  10.253 - apply (frule_tac n = n in height_r_bal)
  10.254 - apply (fastsimp simp add: max_def)
  10.255 -apply (simp add: max_def)
  10.256 -apply fastsimp
  10.257 -done
  10.258 -
  10.259 -
  10.260 -lemma is_bal_insert_left: 
  10.261 -"\<lbrakk>height (insert x l) \<noteq> Suc(Suc(height r)); is_bal (insert x l); is_bal (MKT n l r)\<rbrakk>  
  10.262 -  \<Longrightarrow> is_bal (MKT n (insert x l) r)"
  10.263 -apply (cut_tac x = "x" and t = "l" in height_insert)
  10.264 - apply simp
  10.265 -apply fastsimp
  10.266 -done
  10.267 -
  10.268 -
  10.269 -lemma is_bal_insert_right: 
  10.270 -"\<lbrakk> height (insert x r) \<noteq> Suc(Suc(height l)); is_bal (insert x r); is_bal (MKT n l r) \<rbrakk>
  10.271 -  \<Longrightarrow> is_bal (MKT n l (insert x r))"
  10.272 -apply (cut_tac x = "x" and t = "r" in height_insert)
  10.273 - apply simp
  10.274 -apply fastsimp
  10.275 -done
  10.276 -
  10.277 -
  10.278 -lemma is_bal_insert [rule_format (no_asm)]: 
  10.279 -"is_bal t \<longrightarrow> is_bal(insert x t)"
  10.280 -apply (induct_tac "t")
  10.281 - apply simp
  10.282 -apply (rename_tac n t1 t2)
  10.283 -apply (case_tac "x=n")
  10.284 - apply simp
  10.285 -apply (case_tac "x<n")
  10.286 - apply (case_tac "height (insert x t1) = Suc (Suc (height t2))")
  10.287 -  apply (case_tac "bal (insert x t1) = Right")
  10.288 -   apply (fastsimp intro: is_bal_lr_rot simp add: l_bal_def)
  10.289 -  apply (fastsimp intro: is_bal_r_rot simp add: l_bal_def)
  10.290 - apply clarify
  10.291 - apply (frule is_bal_insert_left)
  10.292 -   apply simp
  10.293 -  apply assumption
  10.294 - apply simp
  10.295 -apply (case_tac "height (insert x t2) = Suc (Suc (height t1))")
  10.296 - apply (case_tac "bal (insert x t2) = Left")
  10.297 -  apply (fastsimp intro: is_bal_rl_rot simp add: r_bal_def)
  10.298 - apply (fastsimp intro: is_bal_l_rot simp add: r_bal_def)
  10.299 -apply clarify
  10.300 -apply (frule is_bal_insert_right)
  10.301 -   apply simp
  10.302 -  apply assumption
  10.303 - apply simp
  10.304 -done
  10.305 -
  10.306 -
  10.307 -subsection "is-in"
  10.308 -
  10.309 -lemma is_in_lr_rot: 
  10.310 -"\<lbrakk> height l = Suc(Suc(height r)); bal l = Right \<rbrakk>
  10.311 -  \<Longrightarrow> is_in x (lr_rot (n, l, r)) = is_in x (MKT n l r)"
  10.312 -apply (unfold bal_def)
  10.313 -apply (cases l)
  10.314 - apply simp
  10.315 -apply (rename_tac t1 t2)
  10.316 -apply (case_tac t2)
  10.317 - apply simp 
  10.318 -apply fastsimp
  10.319 -done
  10.320 -
  10.321 -
  10.322 -lemma is_in_r_rot: 
  10.323 -"\<lbrakk> height l = Suc(Suc(height r)); bal l \<noteq> Right \<rbrakk>
  10.324 -  \<Longrightarrow> is_in x (r_rot (n, l, r)) = is_in x (MKT n l r)"
  10.325 -apply (unfold bal_def)
  10.326 -apply (cases l)
  10.327 - apply simp
  10.328 -apply fastsimp
  10.329 -done
  10.330 -
  10.331 -
  10.332 -lemma is_in_rl_rot:
  10.333 -"\<lbrakk> height r = Suc(Suc(height l)); bal r = Left \<rbrakk>
  10.334 -  \<Longrightarrow> is_in x (rl_rot (n, l, r)) = is_in x (MKT n l r)"
  10.335 -apply (unfold bal_def)
  10.336 -apply (cases r)
  10.337 - apply simp
  10.338 -apply (rename_tac t1 t2)
  10.339 -apply (case_tac t1)
  10.340 - apply (simp add: max_def le_def)
  10.341 -apply fastsimp
  10.342 -done
  10.343 -
  10.344 -
  10.345 -lemma is_in_l_rot:
  10.346 -"\<lbrakk> height r = Suc(Suc(height l)); bal r ~= Left \<rbrakk>
  10.347 -  \<Longrightarrow> is_in x (l_rot (n, l, r)) = is_in x (MKT n l r)"
  10.348 -apply (unfold bal_def)
  10.349 -apply (cases r)
  10.350 - apply simp
  10.351 -apply fastsimp
  10.352 -done
  10.353 -
  10.354 -
  10.355 -lemma is_in_insert: 
  10.356 -"is_in y (insert x t) = (y=x \<or> is_in y t)"
  10.357 -apply (induct t)
  10.358 - apply simp
  10.359 -apply (simp add: l_bal_def is_in_lr_rot is_in_r_rot r_bal_def 
  10.360 -                 is_in_rl_rot is_in_l_rot)
  10.361 -apply blast
  10.362 -done
  10.363 -
  10.364 -
  10.365 -subsection "is-ord"
  10.366 -
  10.367 -lemma is_ord_lr_rot [rule_format (no_asm)]: 
  10.368 -"\<lbrakk> height l = Suc(Suc(height r)); bal l = Right; is_ord (MKT n l r) \<rbrakk>
  10.369 -  \<Longrightarrow> is_ord (lr_rot (n, l, r))"
  10.370 -apply (unfold bal_def)
  10.371 -apply (cases l)
  10.372 - apply simp
  10.373 -apply (rename_tac t1 t2)
  10.374 -apply (case_tac t2)
  10.375 - apply simp
  10.376 -apply simp
  10.377 -apply (blast intro: less_trans)
  10.378 -done
  10.379 -
  10.380 -
  10.381 -lemma is_ord_r_rot:
  10.382 -"\<lbrakk> height l = Suc(Suc(height r)); bal l \<noteq> Right; is_ord (MKT n l r) \<rbrakk>
  10.383 -  \<Longrightarrow> is_ord (r_rot (n, l, r))"
  10.384 -apply (unfold bal_def)
  10.385 -apply (cases l)
  10.386 -apply (auto intro: less_trans)
  10.387 -done
  10.388 -
  10.389 -
  10.390 -lemma is_ord_rl_rot: 
  10.391 -"\<lbrakk> height r = Suc(Suc(height l)); bal r = Left; is_ord (MKT n l r) \<rbrakk>
  10.392 -  \<Longrightarrow> is_ord (rl_rot (n, l, r))"
  10.393 -apply (unfold bal_def)
  10.394 -apply (cases r)
  10.395 - apply simp
  10.396 -apply (rename_tac t1 t2)
  10.397 -apply (case_tac t1)
  10.398 - apply (simp add: le_def)
  10.399 -apply simp
  10.400 -apply (blast intro: less_trans)
  10.401 -done
  10.402 -
  10.403 -
  10.404 -lemma is_ord_l_rot: 
  10.405 -"\<lbrakk> height r = Suc(Suc(height l)); bal r \<noteq> Left; is_ord (MKT n l r) \<rbrakk>
  10.406 -  \<Longrightarrow> is_ord (l_rot (n, l, r))"
  10.407 -apply (unfold bal_def)
  10.408 -apply (cases r)
  10.409 - apply simp
  10.410 -apply simp
  10.411 -apply (blast intro: less_trans)
  10.412 -done
  10.413 -
  10.414 -
  10.415 -lemma is_ord_insert: 
  10.416 -"is_ord t \<Longrightarrow> is_ord(insert x t)"
  10.417 -apply (induct t)
  10.418 - apply simp
  10.419 -apply (cut_tac m = "x" and n = "nat" in less_linear)
  10.420 -apply (fastsimp simp add: l_bal_def is_ord_lr_rot is_ord_r_rot r_bal_def
  10.421 -                          is_ord_l_rot is_ord_rl_rot is_in_insert)
  10.422 -done
  10.423 -
  10.424 -end
    11.1 --- a/src/HOL/ex/ROOT.ML	Wed Mar 24 10:55:38 2004 +0100
    11.2 +++ b/src/HOL/ex/ROOT.ML	Thu Mar 25 05:37:32 2004 +0100
    11.3 @@ -25,7 +25,6 @@
    11.4  time_use_thy "mesontest2";
    11.5  time_use_thy "PresburgerEx";
    11.6  time_use_thy "BT";
    11.7 -time_use_thy "AVL";
    11.8  time_use_thy "InSort";
    11.9  time_use_thy "Qsort";
   11.10  time_use_thy "MergeSort";