# HG changeset patch # User narasche # Date 855932503 -3600 # Node ID 69c1b8a493de6c5c6bda2de1796dbb847b5419ac # Parent ab311b6e5e29afbe903ccb1fdae1bcaf4ded240e Some lemmas changed to valuesd diff -r ab311b6e5e29 -r 69c1b8a493de src/HOL/MiniML/Generalize.thy --- a/src/HOL/MiniML/Generalize.thy Fri Feb 14 15:32:00 1997 +0100 +++ b/src/HOL/MiniML/Generalize.thy Fri Feb 14 16:01:43 1997 +0100 @@ -9,7 +9,7 @@ Generalize = Instance + -(* gen: binding (generalising) the variables which are not free in the type scheme *) +(* gen: binding (generalising) the variables which are not free in the context *) types ctxt = type_scheme list @@ -18,7 +18,7 @@ primrec gen typ "gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))" - "gen A (t1 -> t2) = ((gen A t1) =-> (gen A t2))" + "gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)" (* executable version of gen: Implementation with free_tv_ML *) @@ -27,7 +27,7 @@ primrec gen_ML_aux typ "gen_ML_aux A (TVar n) = (if (n mem A) then (FVar n) else (BVar n))" - "gen_ML_aux A (t1 -> t2) = ((gen_ML_aux A t1) =-> (gen_ML_aux A t2))" + "gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)" consts gen_ML :: [ctxt, typ] => type_scheme diff -r ab311b6e5e29 -r 69c1b8a493de src/HOL/MiniML/Instance.ML --- a/src/HOL/MiniML/Instance.ML Fri Feb 14 15:32:00 1997 +0100 +++ b/src/HOL/MiniML/Instance.ML Fri Feb 14 16:01:43 1997 +0100 @@ -15,6 +15,7 @@ qed "bound_typ_inst_mk_scheme"; Addsimps [bound_typ_inst_mk_scheme]; + goal thy "!!S. bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)"; by (type_scheme.induct_tac "sch" 1); by (ALLGOALS Asm_full_simp_tac); @@ -27,6 +28,7 @@ qed "bound_typ_inst_eq"; + (* lemmatas for bound_scheme_inst *) goal thy "!!t. bound_scheme_inst B (mk_scheme t) = mk_scheme t"; diff -r ab311b6e5e29 -r 69c1b8a493de src/HOL/MiniML/Maybe.ML --- a/src/HOL/MiniML/Maybe.ML Fri Feb 14 15:32:00 1997 +0100 +++ b/src/HOL/MiniML/Maybe.ML Fri Feb 14 16:01:43 1997 +0100 @@ -23,9 +23,14 @@ by (Asm_simp_tac 1); qed "expand_option_bind"; -goal Maybe.thy +goal thy "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))"; by(simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1); qed "option_bind_eq_None"; Addsimps [option_bind_eq_None]; + +(* auxiliary lemma *) +goal Maybe.thy "(y = Some x) = (Some x = y)"; +by( simp_tac (!simpset addsimps [eq_sym_conv]) 1); +qed "rotate_Some"; diff -r ab311b6e5e29 -r 69c1b8a493de src/HOL/MiniML/Type.ML --- a/src/HOL/MiniML/Type.ML Fri Feb 14 15:32:00 1997 +0100 +++ b/src/HOL/MiniML/Type.ML Fri Feb 14 16:01:43 1997 +0100 @@ -16,7 +16,7 @@ by (Fast_tac 1); qed_spec_mp "mk_scheme_Fun"; -goal Type.thy "!t'.mk_scheme t = mk_scheme t' --> t=t'"; +goal thy "!t'.mk_scheme t = mk_scheme t' --> t=t'"; by (typ.induct_tac "t" 1); br allI 1; by (typ.induct_tac "t'" 1); @@ -96,19 +96,33 @@ by (fast_tac (HOL_cs addss !simpset) 1); qed "new_tv_Cons"; -goalw Type.thy [new_tv_def] "!!n. new_tv n TVar"; +goalw thy [new_tv_def] "!!n. new_tv n TVar"; by (strip_tac 1); by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,cod_def]) 1); qed "new_tv_TVar_subst"; Addsimps [new_tv_TVar,new_tv_FVar,new_tv_BVar,new_tv_Fun,new_tv_Fun2,new_tv_Nil,new_tv_Cons,new_tv_TVar_subst]; -goalw Type.thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def] +goalw thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def] "new_tv n id_subst"; by(Simp_tac 1); qed "new_tv_id_subst"; Addsimps[new_tv_id_subst]; +goal thy "new_tv n (sch::type_scheme) --> \ +\ $(%k.if k \ +\ $(%k.if k m < max n n'"; by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); by (fast_tac (!claset addDs [not_leE] addIs [less_trans]) 1); -qed "less_maxR"; +val less_maxR = result(); goalw thy [new_tv_def] "!!t::typ. ? n. (new_tv n t)"; by (typ.induct_tac "t" 1); @@ -574,12 +588,12 @@ goalw thy [max_def] "!!n::nat. n <= (max n n')"; by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); -qed "le_maxL"; +val le_maxL = result(); goalw thy [max_def] "!!n'::nat. n' <= (max n n')"; by (simp_tac (!simpset setloop (split_tac [expand_if])) 1); by (fast_tac (!claset addDs [not_leE] addIs [less_or_eq_imp_le]) 1); -qed "le_maxR"; +val le_maxR = result(); goal thy "!!A::type_scheme list. ? n. (new_tv n A)"; by (list.induct_tac "A" 1); diff -r ab311b6e5e29 -r 69c1b8a493de src/HOL/MiniML/Type.thy --- a/src/HOL/MiniML/Type.thy Fri Feb 14 15:32:00 1997 +0100 +++ b/src/HOL/MiniML/Type.thy Fri Feb 14 16:01:43 1997 +0100 @@ -54,6 +54,7 @@ "free_tv [] = {}" "free_tv (x#l) = (free_tv x) Un (free_tv l)" + (* executable version of free_tv: Implementation with lists *) consts free_tv_ML :: ['a::type_struct] => nat list diff -r ab311b6e5e29 -r 69c1b8a493de src/HOL/MiniML/W.ML --- a/src/HOL/MiniML/W.ML Fri Feb 14 15:32:00 1997 +0100 +++ b/src/HOL/MiniML/W.ML Fri Feb 14 16:01:43 1997 +0100 @@ -74,11 +74,6 @@ ba 1; qed "new_tv_compatible_W"; -(* auxiliary lemma *) -goal Maybe.thy "(y = Some x) = (Some x = y)"; -by( simp_tac (!simpset addsimps [eq_sym_conv]) 1); -qed "rotate_Some"; - goal thy "!!sch. new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)"; by (type_scheme.induct_tac "sch" 1); by (Asm_full_simp_tac 1); @@ -335,11 +330,11 @@ goal thy "!!A. (!x. x : A --> x ~: B) ==> A Int B = {}"; by (Fast_tac 1); -qed "weaken_A_Int_B_eq_empty"; +val weaken_A_Int_B_eq_empty = result(); goal thy "!!A. x ~: A | x : B ==> x ~: A - B"; by (Fast_tac 1); -qed "weaken_not_elem_A_minus_B"; +val weaken_not_elem_A_minus_B = result(); (* correctness of W with respect to has_type *) goal W.thy @@ -462,25 +457,11 @@ by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le]) 1); qed_spec_mp "W_correct_lemma"; -goal Type.thy "new_tv n (sch::type_scheme) --> \ -\ $(%k.if k \ -\ $(%k.if k