Some lemmas changed to valuesd
authornarasche
Fri Feb 14 16:01:43 1997 +0100 (1997-02-14)
changeset 262569c1b8a493de
parent 2624 ab311b6e5e29
child 2626 373daa468a74
Some lemmas changed to valuesd
src/HOL/MiniML/Generalize.thy
src/HOL/MiniML/Instance.ML
src/HOL/MiniML/Maybe.ML
src/HOL/MiniML/Type.ML
src/HOL/MiniML/Type.thy
src/HOL/MiniML/W.ML
     1.1 --- a/src/HOL/MiniML/Generalize.thy	Fri Feb 14 15:32:00 1997 +0100
     1.2 +++ b/src/HOL/MiniML/Generalize.thy	Fri Feb 14 16:01:43 1997 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  Generalize = Instance +
     1.5  
     1.6  
     1.7 -(* gen: binding (generalising) the variables which are not free in the type scheme *)
     1.8 +(* gen: binding (generalising) the variables which are not free in the context *)
     1.9  
    1.10  types ctxt = type_scheme list
    1.11      
    1.12 @@ -18,7 +18,7 @@
    1.13  
    1.14  primrec gen typ
    1.15    "gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
    1.16 -  "gen A (t1 -> t2) = ((gen A t1) =-> (gen A t2))"
    1.17 +  "gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)"
    1.18  
    1.19  (* executable version of gen: Implementation with free_tv_ML *)
    1.20  
    1.21 @@ -27,7 +27,7 @@
    1.22  
    1.23  primrec gen_ML_aux typ
    1.24    "gen_ML_aux A (TVar n) = (if (n mem A) then (FVar n) else (BVar n))"
    1.25 -  "gen_ML_aux A (t1 -> t2) = ((gen_ML_aux A t1) =-> (gen_ML_aux A t2))"
    1.26 +  "gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
    1.27  
    1.28  consts
    1.29    gen_ML :: [ctxt, typ] => type_scheme
     2.1 --- a/src/HOL/MiniML/Instance.ML	Fri Feb 14 15:32:00 1997 +0100
     2.2 +++ b/src/HOL/MiniML/Instance.ML	Fri Feb 14 16:01:43 1997 +0100
     2.3 @@ -15,6 +15,7 @@
     2.4  qed "bound_typ_inst_mk_scheme";
     2.5  
     2.6  Addsimps [bound_typ_inst_mk_scheme];
     2.7 +
     2.8  goal thy "!!S. bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)";
     2.9  by (type_scheme.induct_tac "sch" 1);
    2.10  by (ALLGOALS Asm_full_simp_tac);
    2.11 @@ -27,6 +28,7 @@
    2.12  qed "bound_typ_inst_eq";
    2.13  
    2.14  
    2.15 +
    2.16  (* lemmatas for bound_scheme_inst *)
    2.17  
    2.18  goal thy "!!t. bound_scheme_inst B (mk_scheme t) = mk_scheme t";
     3.1 --- a/src/HOL/MiniML/Maybe.ML	Fri Feb 14 15:32:00 1997 +0100
     3.2 +++ b/src/HOL/MiniML/Maybe.ML	Fri Feb 14 16:01:43 1997 +0100
     3.3 @@ -23,9 +23,14 @@
     3.4  by (Asm_simp_tac 1);
     3.5  qed "expand_option_bind";
     3.6  
     3.7 -goal Maybe.thy
     3.8 +goal thy
     3.9    "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
    3.10  by(simp_tac (!simpset setloop (split_tac [expand_option_bind])) 1);
    3.11  qed "option_bind_eq_None";
    3.12  
    3.13  Addsimps [option_bind_eq_None];
    3.14 +
    3.15 +(* auxiliary lemma *)
    3.16 +goal Maybe.thy "(y = Some x) = (Some x = y)";
    3.17 +by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
    3.18 +qed "rotate_Some";
     4.1 --- a/src/HOL/MiniML/Type.ML	Fri Feb 14 15:32:00 1997 +0100
     4.2 +++ b/src/HOL/MiniML/Type.ML	Fri Feb 14 16:01:43 1997 +0100
     4.3 @@ -16,7 +16,7 @@
     4.4  by (Fast_tac 1);
     4.5  qed_spec_mp "mk_scheme_Fun";
     4.6  
     4.7 -goal Type.thy "!t'.mk_scheme t = mk_scheme t' --> t=t'";
     4.8 +goal thy "!t'.mk_scheme t = mk_scheme t' --> t=t'";
     4.9  by (typ.induct_tac "t" 1);
    4.10   br allI 1;
    4.11   by (typ.induct_tac "t'" 1);
    4.12 @@ -96,19 +96,33 @@
    4.13  by (fast_tac (HOL_cs addss !simpset) 1);
    4.14  qed "new_tv_Cons";
    4.15  
    4.16 -goalw Type.thy [new_tv_def] "!!n. new_tv n TVar";
    4.17 +goalw thy [new_tv_def] "!!n. new_tv n TVar";
    4.18  by (strip_tac 1);
    4.19  by (asm_full_simp_tac (!simpset addsimps [free_tv_subst,dom_def,cod_def]) 1);
    4.20  qed "new_tv_TVar_subst";
    4.21  
    4.22  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];
    4.23  
    4.24 -goalw Type.thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def]
    4.25 +goalw thy [id_subst_def,new_tv_def,free_tv_subst,dom_def,cod_def]
    4.26    "new_tv n id_subst";
    4.27  by(Simp_tac 1);
    4.28  qed "new_tv_id_subst";
    4.29  Addsimps[new_tv_id_subst];
    4.30  
    4.31 +goal thy "new_tv n (sch::type_scheme) --> \
    4.32 +\              $(%k.if k<n then S k else S' k) sch = $S sch";
    4.33 +by (type_scheme.induct_tac "sch" 1);
    4.34 +by(ALLGOALS Asm_simp_tac);
    4.35 +qed "new_if_subst_type_scheme";
    4.36 +Addsimps [new_if_subst_type_scheme];
    4.37 +
    4.38 +goal thy "new_tv n (A::type_scheme list) --> \
    4.39 +\              $(%k.if k<n then S k else S' k) A = $S A";
    4.40 +by (list.induct_tac "A" 1);
    4.41 +by(ALLGOALS Asm_simp_tac);
    4.42 +qed "new_if_subst_type_scheme_list";
    4.43 +Addsimps [new_if_subst_type_scheme_list];
    4.44 +
    4.45  
    4.46  (* constructor laws for dom and cod *)
    4.47  
    4.48 @@ -542,7 +556,7 @@
    4.49  goalw thy [max_def] "!!n::nat. m < n' ==> m < max n n'";
    4.50  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    4.51  by (fast_tac (!claset addDs [not_leE] addIs [less_trans]) 1);
    4.52 -qed "less_maxR";
    4.53 +val less_maxR = result();
    4.54  
    4.55  goalw thy [new_tv_def] "!!t::typ. ? n. (new_tv n t)";
    4.56  by (typ.induct_tac "t" 1);
    4.57 @@ -574,12 +588,12 @@
    4.58  
    4.59  goalw thy [max_def] "!!n::nat. n <= (max n n')";
    4.60  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    4.61 -qed "le_maxL";
    4.62 +val le_maxL = result();
    4.63  
    4.64  goalw thy [max_def] "!!n'::nat. n' <= (max n n')";
    4.65  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    4.66  by (fast_tac (!claset addDs [not_leE] addIs [less_or_eq_imp_le]) 1);
    4.67 -qed "le_maxR";
    4.68 +val le_maxR = result();
    4.69  
    4.70  goal thy "!!A::type_scheme list. ? n. (new_tv n A)";
    4.71  by (list.induct_tac "A" 1);
     5.1 --- a/src/HOL/MiniML/Type.thy	Fri Feb 14 15:32:00 1997 +0100
     5.2 +++ b/src/HOL/MiniML/Type.thy	Fri Feb 14 16:01:43 1997 +0100
     5.3 @@ -54,6 +54,7 @@
     5.4    "free_tv [] = {}"
     5.5    "free_tv (x#l) = (free_tv x) Un (free_tv l)"
     5.6  
     5.7 +  
     5.8  (* executable version of free_tv: Implementation with lists *)
     5.9  consts
    5.10    free_tv_ML :: ['a::type_struct] => nat list
     6.1 --- a/src/HOL/MiniML/W.ML	Fri Feb 14 15:32:00 1997 +0100
     6.2 +++ b/src/HOL/MiniML/W.ML	Fri Feb 14 16:01:43 1997 +0100
     6.3 @@ -74,11 +74,6 @@
     6.4  ba 1;
     6.5  qed "new_tv_compatible_W";
     6.6  
     6.7 -(* auxiliary lemma *)
     6.8 -goal Maybe.thy "(y = Some x) = (Some x = y)";
     6.9 -by( simp_tac (!simpset addsimps [eq_sym_conv]) 1);
    6.10 -qed "rotate_Some";
    6.11 -
    6.12  goal thy "!!sch. new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
    6.13  by (type_scheme.induct_tac "sch" 1);
    6.14  by (Asm_full_simp_tac 1);
    6.15 @@ -335,11 +330,11 @@
    6.16  
    6.17  goal thy "!!A. (!x. x : A --> x ~: B) ==> A Int B = {}";
    6.18  by (Fast_tac 1);
    6.19 -qed "weaken_A_Int_B_eq_empty";
    6.20 +val weaken_A_Int_B_eq_empty = result();
    6.21  
    6.22  goal thy "!!A. x ~: A | x : B ==> x ~: A - B";
    6.23  by (Fast_tac 1);
    6.24 -qed "weaken_not_elem_A_minus_B";
    6.25 +val weaken_not_elem_A_minus_B = result();
    6.26  
    6.27  (* correctness of W with respect to has_type *)
    6.28  goal W.thy
    6.29 @@ -462,25 +457,11 @@
    6.30  by (asm_full_simp_tac (!simpset addsimps [not_less_iff_le]) 1);
    6.31  qed_spec_mp "W_correct_lemma";
    6.32  
    6.33 -goal Type.thy "new_tv n (sch::type_scheme) --> \
    6.34 -\              $(%k.if k<n then S k else S' k) sch = $S sch";
    6.35 -by (type_scheme.induct_tac "sch" 1);
    6.36 -by(ALLGOALS Asm_simp_tac);
    6.37 -qed "new_if_subst_type_scheme";
    6.38 -Addsimps [new_if_subst_type_scheme];
    6.39 -
    6.40 -goal Type.thy "new_tv n (A::type_scheme list) --> \
    6.41 -\              $(%k.if k<n then S k else S' k) A = $S A";
    6.42 -by (list.induct_tac "A" 1);
    6.43 -by(ALLGOALS Asm_simp_tac);
    6.44 -qed "new_if_subst_type_scheme_list";
    6.45 -Addsimps [new_if_subst_type_scheme_list];
    6.46 -
    6.47  goal Arith.thy "!!n::nat. ~ k+n < n";
    6.48  by (nat_ind_tac "k" 1);
    6.49  by(ALLGOALS Asm_simp_tac);
    6.50  by(trans_tac 1);
    6.51 -qed "not_add_less1";
    6.52 +val not_add_less1 = result();
    6.53  Addsimps [not_add_less1];
    6.54  
    6.55  (* Completeness of W w.r.t. has_type *)