--- a/src/HOL/Induct/LFilter.ML Wed Jan 07 13:55:54 1998 +0100
+++ b/src/HOL/Induct/LFilter.ML Thu Jan 08 11:21:45 1998 +0100
@@ -71,32 +71,34 @@
goalw thy [find_def] "find p LNil = LNil";
by (blast_tac (claset() addIs [select_equality]) 1);
qed "find_LNil";
+Addsimps [find_LNil];
goalw thy [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
by (blast_tac (claset() addIs [select_equality] addDs [findRel_functional]) 1);
qed "findRel_imp_find";
+Addsimps [findRel_imp_find];
goal thy "!!p. p x ==> find p (LCons x l) = LCons x l";
by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
qed "find_LCons_found";
+Addsimps [find_LCons_found];
goalw thy [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
by (blast_tac (claset() addIs [select_equality]) 1);
qed "diverge_find_LNil";
-
Addsimps [diverge_find_LNil];
goal thy "!!p. ~ (p x) ==> find p (LCons x l) = find p l";
by (case_tac "LCons x l : Domain(findRel p)" 1);
by (Asm_full_simp_tac 2);
by (Clarify_tac 1);
-by (asm_simp_tac (simpset() addsimps [findRel_imp_find]) 1);
+by (Asm_simp_tac 1);
by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
qed "find_LCons_seek";
+Addsimps [find_LCons_seek];
goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
-by (asm_simp_tac (simpset() addsimps [find_LCons_found, find_LCons_seek]
- addsplits [expand_if]) 1);
+by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
qed "find_LCons";
@@ -105,54 +107,60 @@
goal thy "lfilter p LNil = LNil";
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (simp_tac (simpset() addsimps [find_LNil]) 1);
+by (Simp_tac 1);
qed "lfilter_LNil";
+Addsimps [lfilter_LNil];
goal thy "!!p. l ~: Domain(findRel p) ==> lfilter p l = LNil";
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
by (Asm_simp_tac 1);
qed "diverge_lfilter_LNil";
+Addsimps [diverge_lfilter_LNil];
+
goal thy "!!p. p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (asm_simp_tac (simpset() addsimps [find_LCons_found]) 1);
+by (Asm_simp_tac 1);
qed "lfilter_LCons_found";
+(*This rewrite and lfilter_LCons_seek are NOT added because lfilter_LCons
+ subsumes both*)
goal thy "!!p. (l, LCons x l') : findRel p \
\ ==> lfilter p l = LCons x (lfilter p l')";
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
-by (asm_simp_tac (simpset() addsimps [findRel_imp_find]) 1);
+by (Asm_simp_tac 1);
qed "findRel_imp_lfilter";
+Addsimps [findRel_imp_lfilter];
+
+
goal thy "!!p. ~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
by (case_tac "LCons x l : Domain(findRel p)" 1);
-by (asm_full_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
+by (Asm_full_simp_tac 2);
by (etac Domain_findRelE 1);
by (safe_tac (claset() delrules [conjI]));
-by (asm_full_simp_tac
- (simpset() addsimps [findRel_imp_lfilter, findRel_imp_find,
- find_LCons_seek]) 1);
+by (Asm_full_simp_tac 1);
qed "lfilter_LCons_seek";
goal thy "lfilter p (LCons x l) = \
\ (if p x then LCons x (lfilter p l) else lfilter p l)";
by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]
- addsplits [expand_if]) 1);
+ addsplits [expand_if]) 1);
qed "lfilter_LCons";
AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
-Addsimps [lfilter_LNil, lfilter_LCons];
+Addsimps [lfilter_LCons];
goal thy "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
by (rtac notI 1);
by (etac Domain_findRelE 1);
by (etac rev_mp 1);
-by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
+by (Asm_simp_tac 1);
qed "lfilter_eq_LNil";
@@ -162,7 +170,7 @@
by (case_tac "l : Domain(findRel p)" 1);
by (etac Domain_findRelE 1);
by (Asm_simp_tac 2);
-by (asm_simp_tac (simpset() addsimps [findRel_imp_find]) 1);
+by (Asm_simp_tac 1);
by (Blast_tac 1);
qed_spec_mp "lfilter_eq_LCons";
@@ -170,9 +178,9 @@
goal thy "lfilter p l = LNil | \
\ (EX y l'. lfilter p l = LCons y (lfilter p l') & p y)";
by (case_tac "l : Domain(findRel p)" 1);
-by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
+by (Asm_simp_tac 2);
by (blast_tac (claset() addSEs [Domain_findRelE]
- addIs [findRel_imp_lfilter]) 1);
+ addIs [findRel_imp_lfilter]) 1);
qed "lfilter_cases";
@@ -228,7 +236,7 @@
\ --> l : Domain (findRel(%x. p x & q x))";
by (etac findRel.induct 1);
by (blast_tac (claset() addSDs [sym RS lfilter_eq_LCons]
- addIs [findRel_conj]) 1);
+ addIs [findRel_conj]) 1);
by Auto_tac;
by (dtac (sym RS lfilter_eq_LCons) 1);
by Auto_tac;
@@ -256,14 +264,13 @@
by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
by (blast_tac (claset() addIs [impOfSubs Domain_findRel_mono]) 3);
(*There are no qs in l: both lists are LNil*)
-by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
+by (Asm_simp_tac 2);
by (etac Domain_findRelE 1);
(*case q x*)
by (case_tac "p x" 1);
-by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter,
- findRel_conj RS findRel_imp_lfilter]) 1);
+by (asm_simp_tac (simpset() addsimps [findRel_conj RS findRel_imp_lfilter]) 1);
(*case q x and ~(p x) *)
-by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
+by (Asm_simp_tac 1);
by (case_tac "l' : Domain (findRel (%x. p x & q x))" 1);
(*subcase: there is no p&q in l' and therefore none in l*)
by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
@@ -271,14 +278,14 @@
by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2);
by (blast_tac (claset() addIs [findRel_lfilter_Domain_conj]) 3);
(* ...and therefore too, no p in lfilter q l'. Both results are Lnil*)
-by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
+by (Asm_simp_tac 2);
(*subcase: there is a p&q in l' and therefore also one in l*)
by (etac Domain_findRelE 1);
by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
by (blast_tac (claset() addIs [findRel_conj2]) 2);
by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
by (blast_tac (claset() addIs [findRel_conj_lfilter]) 2);
-by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
+by (Asm_simp_tac 1);
val lemma = result();
@@ -327,9 +334,9 @@
by (case_tac "lmap f l : Domain (findRel p)" 1);
by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
by (blast_tac (claset() addIs [findRel_lmap_Domain]) 3);
-by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
+by (Asm_simp_tac 2);
by (etac Domain_findRelE 1);
by (forward_tac [lmap_LCons_findRel] 1);
by (Clarify_tac 1);
-by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
+by (Asm_simp_tac 1);
qed "lfilter_lmap";
--- a/src/HOL/Induct/LList.ML Wed Jan 07 13:55:54 1998 +0100
+++ b/src/HOL/Induct/LList.ML Thu Jan 08 11:21:45 1998 +0100
@@ -14,11 +14,6 @@
simpset_ref() := simpset() addsplits [expand_split, expand_sum_case];
-(*For adding _eqI rules to a simpset; we must remove Pair_eq because
- it may turn an instance of reflexivity into a conjunction!*)
-fun add_eqI ss = ss addsimps [range_eqI, image_eqI]
- delsimps [Pair_eq];
-
(*This justifies using llist in other recursive type definitions*)
goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
@@ -49,11 +44,14 @@
goalw LList.thy [list_Fun_def, NIL_def] "NIL: list_Fun A X";
by (Fast_tac 1);
qed "list_Fun_NIL_I";
+AddIffs [list_Fun_NIL_I];
goalw LList.thy [list_Fun_def,CONS_def]
"!!M N. [| M: A; N: X |] ==> CONS M N : list_Fun A X";
by (Fast_tac 1);
qed "list_Fun_CONS_I";
+Addsimps [list_Fun_CONS_I];
+AddSIs [list_Fun_CONS_I];
(*Utilise the "strong" part, i.e. gfp(f)*)
goalw LList.thy (llist.defs @ [list_Fun_def])
@@ -130,8 +128,7 @@
by (rtac rangeI 1);
by Safe_tac;
by (stac LList_corec 1);
-by (simp_tac (simpset() addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI]
- |> add_eqI) 1);
+by (Simp_tac 1);
qed "LList_corec_type";
(*Lemma for the proof of llist_corec*)
@@ -142,8 +139,7 @@
by (rtac rangeI 1);
by Safe_tac;
by (stac LList_corec 1);
-by (asm_simp_tac (simpset() addsimps [list_Fun_NIL_I]) 1);
-by (fast_tac (claset() addSIs [list_Fun_CONS_I]) 1);
+by (Asm_simp_tac 1);
qed "LList_corec_type2";
@@ -163,11 +159,11 @@
by (etac LListD.elim 1);
by (safe_tac (claset_of Prod.thy delrules [equalityI] addSEs [diagE]));
by (res_inst_tac [("n", "n")] natE 1);
-by (asm_simp_tac (simpset() addsimps [ntrunc_0]) 1);
+by (Asm_simp_tac 1);
by (rename_tac "n'" 1);
by (res_inst_tac [("n", "n'")] natE 1);
-by (asm_simp_tac (simpset() addsimps [CONS_def, ntrunc_one_In1]) 1);
-by (asm_simp_tac (simpset() addsimps [CONS_def, ntrunc_In1, ntrunc_Scons, less_Suc_eq]) 1);
+by (asm_simp_tac (simpset() addsimps [CONS_def]) 1);
+by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1);
qed "LListD_implies_ntrunc_equality";
(*The domain of the LListD relation*)
@@ -234,7 +230,7 @@
by (eresolve_tac [llist.elim] 1);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [diagI, LListD_Fun_NIL_I,
- LListD_Fun_CONS_I])));
+ LListD_Fun_CONS_I])));
qed "diag_subset_LListD";
goal LList.thy "LListD(diag(A)) = diag(llist(A))";
@@ -265,6 +261,12 @@
(*** Finality of llist(A): Uniqueness of functions defined by corecursion ***)
+(*We must remove Pair_eq because it may turn an instance of reflexivity
+ (h1 b, h2 b) = (h1 ?x17, h2 ?x17) into a conjunction!
+ (or strengthen the Solver?)
+*)
+Delsimps [Pair_eq];
+
(*abstract proof using a bisimulation*)
val [prem1,prem2] = goal LList.thy
"[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x); \
@@ -279,8 +281,7 @@
by (stac prem1 1);
by (stac prem2 1);
by (simp_tac (simpset() addsimps [LListD_Fun_NIL_I,
- CollectI RS LListD_Fun_CONS_I]
- |> add_eqI) 1);
+ CollectI RS LListD_Fun_CONS_I]) 1);
qed "LList_corec_unique";
val [prem] = goal LList.thy
@@ -298,9 +299,12 @@
goalw LList.thy [CONS_def]
"ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)";
-by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_In1]) 1);
+by (Simp_tac 1);
qed "ntrunc_CONS";
+Addsimps [ntrunc_one_CONS, ntrunc_CONS];
+
+
val [prem1,prem2] = goal LList.thy
"[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x); \
\ !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
@@ -319,8 +323,7 @@
by (res_inst_tac [("n", "n")] natE 1);
by (rename_tac "m" 2);
by (res_inst_tac [("n", "m")] natE 2);
-by (ALLGOALS(asm_simp_tac(simpset() addsimps
- [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS, less_Suc_eq])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
result();
@@ -436,9 +439,7 @@
\ |] ==> f(M) = g(M)";
by (rtac LList_equalityI 1);
by (rtac (Mlist RS imageI) 1);
-by (rtac subsetI 1);
-by (etac imageE 1);
-by (etac ssubst 1);
+by (rtac image_subsetI 1);
by (etac llist.elim 1);
by (etac ssubst 1);
by (stac NILcase 1);
@@ -460,13 +461,15 @@
by (Simp_tac 1);
qed "Lmap_CONS";
+Addsimps [Lmap_NIL, Lmap_CONS];
+
(*Another type-checking proof by coinduction*)
val [major,minor] = goal LList.thy
"[| M: llist(A); !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
by (rtac (major RS imageI RS llist_coinduct) 1);
by Safe_tac;
by (etac llist.elim 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
+by (ALLGOALS Asm_simp_tac);
by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I,
minor, imageI, UnI1] 1));
qed "Lmap_type";
@@ -484,7 +487,7 @@
by (rtac (prem RS imageI RS LList_equalityI) 1);
by Safe_tac;
by (etac llist.elim 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
+by (ALLGOALS Asm_simp_tac);
by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
rangeI RS LListD_Fun_CONS_I] 1));
qed "Lmap_compose";
@@ -493,7 +496,7 @@
by (rtac (prem RS imageI RS LList_equalityI) 1);
by Safe_tac;
by (etac llist.elim 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
+by (ALLGOALS Asm_simp_tac);
by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1,
rangeI RS LListD_Fun_CONS_I] 1));
qed "Lmap_ident";
@@ -520,7 +523,7 @@
Addsimps [llist.NIL_I, Lappend_NIL_NIL, Lappend_NIL_CONS,
Lappend_CONS, LListD_Fun_CONS_I, range_eqI, image_eqI];
-Delsimps [Pair_eq];
+
goal LList.thy "!!M. M: llist(A) ==> Lappend NIL M = M";
by (etac LList_fun_equalityI 1);
@@ -532,6 +535,9 @@
by (ALLGOALS Asm_simp_tac);
qed "Lappend_NIL2";
+Addsimps [Lappend_NIL, Lappend_NIL2];
+
+
(** Alternative type-checking proofs for Lappend **)
(*weak co-induction: bisimulation and case analysis on both variables*)
@@ -543,9 +549,8 @@
by Safe_tac;
by (eres_inst_tac [("a", "u")] llist.elim 1);
by (eres_inst_tac [("a", "v")] llist.elim 1);
-by (ALLGOALS
- (Asm_simp_tac THEN'
- fast_tac (claset() addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
qed "Lappend_type";
(*strong co-induction: bisimulation and case analysis on one variable*)
@@ -553,12 +558,10 @@
"!!M N. [| M: llist(A); N: llist(A) |] ==> Lappend M N: llist(A)";
by (res_inst_tac [("X", "(%u. Lappend u N)``llist(A)")] llist_coinduct 1);
by (etac imageI 1);
-by (rtac subsetI 1);
-by (etac imageE 1);
-by (eres_inst_tac [("a", "u")] llist.elim 1);
-by (asm_simp_tac (simpset() addsimps [Lappend_NIL, list_Fun_llist_I]) 1);
+by (rtac image_subsetI 1);
+by (eres_inst_tac [("a", "x")] llist.elim 1);
+by (asm_simp_tac (simpset() addsimps [list_Fun_llist_I]) 1);
by (Asm_simp_tac 1);
-by (fast_tac (claset() addSIs [list_Fun_CONS_I]) 1);
qed "Lappend_type";
(**** Lazy lists as the type 'a llist -- strongly typed versions of above ****)
@@ -587,7 +590,8 @@
by (assume_tac 1);
by (etac rangeE 1);
by (rtac (inj_Rep_llist RS injD RS prem2) 1);
-by (asm_simp_tac (simpset() delsimps [CONS_CONS_eq] addsimps [Rep_llist_LCons]) 1);
+by (asm_simp_tac (simpset() delsimps [CONS_CONS_eq]
+ addsimps [Rep_llist_LCons]) 1);
by (etac (Abs_llist_inverse RS ssubst) 1);
by (rtac refl 1);
qed "llistE";
@@ -629,7 +633,8 @@
goal LList.thy
"prod_fun Rep_llist Rep_llist `` r <= \
\ (llist(range Leaf)) Times (llist(range Leaf))";
-by (fast_tac (claset() addIs [Rep_llist]) 1);
+by (fast_tac (claset() delrules [image_subsetI]
+ addIs [Rep_llist]) 1);
qed "subset_Sigma_llist";
val [prem] = goal LList.thy
@@ -638,7 +643,7 @@
by Safe_tac;
by (rtac (prem RS subsetD RS SigmaE2) 1);
by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [o_def,prod_fun,Abs_llist_inverse]) 1);
+by (asm_simp_tac (simpset() addsimps [Abs_llist_inverse]) 1);
qed "prod_fun_lemma";
goal LList.thy
--- a/src/HOL/Induct/SList.ML Wed Jan 07 13:55:54 1998 +0100
+++ b/src/HOL/Induct/SList.ML Thu Jan 08 11:21:45 1998 +0100
@@ -1,7 +1,7 @@
(* Title: HOL/ex/SList.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
+ Copyright 1998 University of Cambridge
Definition of type 'a list by a least fixed point
*)
@@ -138,9 +138,12 @@
qed "List_case_NIL";
goalw SList.thy [List_case_def,CONS_def] "List_case c h (CONS M N) = h M N";
-by (simp_tac (simpset() addsimps [Split,Case_In1]) 1);
+by (Simp_tac 1);
qed "List_case_CONS";
+Addsimps [List_case_NIL, List_case_CONS];
+
+
(*** List_rec -- by wf recursion on pred_sexp ***)
(* The trancl(pred_sexp) is essential because pred_sexp_CONS_I1,2 would not
@@ -185,23 +188,25 @@
goal SList.thy "List_rec NIL c h = c";
by (rtac (List_rec_unfold RS trans) 1);
-by (simp_tac (simpset() addsimps [List_case_NIL]) 1);
+by (Simp_tac 1);
qed "List_rec_NIL";
goal SList.thy "!!M. [| M: sexp; N: sexp |] ==> \
\ List_rec (CONS M N) c h = h M N (List_rec N c h)";
by (rtac (List_rec_unfold RS trans) 1);
-by (asm_simp_tac (simpset() addsimps [List_case_CONS, pred_sexp_CONS_I2]) 1);
+by (asm_simp_tac (simpset() addsimps [pred_sexp_CONS_I2]) 1);
qed "List_rec_CONS";
+Addsimps [List_rec_NIL, List_rec_CONS];
+
+
(*** list_rec -- by List_rec ***)
val Rep_list_in_sexp =
[range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD;
local
- val list_rec_simps = [List_rec_NIL, List_rec_CONS,
- Abs_list_inverse, Rep_list_inverse,
+ val list_rec_simps = [Abs_list_inverse, Rep_list_inverse,
Rep_list, rangeI, inj_Leaf, inv_f_f,
sexp.LeafI, Rep_list_in_sexp]
in
@@ -364,8 +369,8 @@
goal SList.thy "!!f. (!!x. f(x): sexp) ==> \
\ Abs_map g (Rep_map f xs) = map (%t. g(f(t))) xs";
by (list_ind_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac(simpset() addsimps
- [Rep_map_type,list_sexp RS subsetD])));
+by (ALLGOALS (asm_simp_tac(simpset() addsimps
+ [Rep_map_type, list_sexp RS subsetD])));
qed "Abs_Rep_map";
Addsimps [append_Nil4, map_ident2];
--- a/src/HOL/Prod.ML Wed Jan 07 13:55:54 1998 +0100
+++ b/src/HOL/Prod.ML Thu Jan 08 11:21:45 1998 +0100
@@ -241,19 +241,21 @@
goalw Prod.thy [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
by (rtac split 1);
qed "prod_fun";
+Addsimps [prod_fun];
goal Prod.thy
"prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
by (rtac ext 1);
by (res_inst_tac [("p","x")] PairE 1);
-by (asm_simp_tac (simpset() addsimps [prod_fun,o_def]) 1);
+by (Asm_simp_tac 1);
qed "prod_fun_compose";
goal Prod.thy "prod_fun (%x. x) (%y. y) = (%z. z)";
by (rtac ext 1);
by (res_inst_tac [("p","z")] PairE 1);
-by (asm_simp_tac (simpset() addsimps [prod_fun]) 1);
+by (Asm_simp_tac 1);
qed "prod_fun_ident";
+Addsimps [prod_fun_ident];
val prems = goal Prod.thy "(a,b):r ==> (f(a),g(b)) : (prod_fun f g)``r";
by (rtac image_eqI 1);
@@ -271,6 +273,7 @@
by (blast_tac (claset() addIs [prod_fun]) 1);
qed "prod_fun_imageE";
+
(*** Disjoint union of a family of sets - Sigma ***)
qed_goalw "SigmaI" Prod.thy [Sigma_def]
--- a/src/HOL/Sexp.ML Wed Jan 07 13:55:54 1998 +0100
+++ b/src/HOL/Sexp.ML Thu Jan 08 11:21:45 1998 +0100
@@ -22,6 +22,8 @@
by (blast_tac (claset() addSIs [select_equality]) 1);
qed "sexp_case_Scons";
+Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons];
+
(** Introduction rules for sexp constructors **)
@@ -100,6 +102,13 @@
"(%M. sexp_rec M c d e) = wfrec pred_sexp \
\ (%g. sexp_case c d (%N1 N2. e N1 N2 (g N1) (g N2)))";
by (simp_tac (HOL_ss addsimps [sexp_rec_def]) 1);
+
+(* sexp_rec a c d e =
+ sexp_case c d
+ (%N1 N2.
+ e N1 N2 (cut (%M. sexp_rec M c d e) pred_sexp a N1)
+ (cut (%M. sexp_rec M c d e) pred_sexp a N2)) a
+*)
bind_thm("sexp_rec_unfold",
[result() RS eq_reflection, wf_pred_sexp] MRS def_wfrec);
@@ -118,6 +127,5 @@
goal Sexp.thy "!!M. [| M: sexp; N: sexp |] ==> \
\ sexp_rec (M$N) c d h = h M N (sexp_rec M c d h) (sexp_rec N c d h)";
by (rtac (sexp_rec_unfold RS trans) 1);
-by (asm_simp_tac (simpset() addsimps [sexp_case_Scons,pred_sexpI1,pred_sexpI2])
- 1);
+by (asm_simp_tac (simpset() addsimps [pred_sexpI1, pred_sexpI2]) 1);
qed "sexp_rec_Scons";
--- a/src/HOL/Univ.ML Wed Jan 07 13:55:54 1998 +0100
+++ b/src/HOL/Univ.ML Thu Jan 08 11:21:45 1998 +0100
@@ -265,30 +265,35 @@
assume_tac 1));
qed "ntrunc_Scons";
+Addsimps [ntrunc_0, ntrunc_Atom, ntrunc_Leaf, ntrunc_Numb, ntrunc_Scons];
+
+
(** Injection nodes **)
goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
-by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_0]) 1);
+by (Simp_tac 1);
by (rewtac Scons_def);
by (Blast_tac 1);
qed "ntrunc_one_In0";
goalw Univ.thy [In0_def]
"ntrunc (Suc (Suc k)) (In0 M) = In0 (ntrunc (Suc k) M)";
-by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
+by (Simp_tac 1);
qed "ntrunc_In0";
goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
-by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_0]) 1);
+by (Simp_tac 1);
by (rewtac Scons_def);
by (Blast_tac 1);
qed "ntrunc_one_In1";
goalw Univ.thy [In1_def]
"ntrunc (Suc (Suc k)) (In1 M) = In1 (ntrunc (Suc k) M)";
-by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_Numb]) 1);
+by (Simp_tac 1);
qed "ntrunc_In1";
+Addsimps [ntrunc_one_In0, ntrunc_In0, ntrunc_one_In1, ntrunc_In1];
+
(*** Cartesian Product ***)
@@ -383,7 +388,7 @@
val [major] = goalw Univ.thy [ntrunc_def]
"(!!k. ntrunc k M <= N) ==> M<=N";
by (blast_tac (claset() addIs [less_add_Suc1, less_add_Suc2,
- major RS subsetD]) 1);
+ major RS subsetD]) 1);
qed "ntrunc_subsetD";
(*A generalized form of the take-lemma*)
@@ -438,6 +443,9 @@
by (blast_tac (claset() addIs [select_equality]) 1);
qed "Case_In1";
+Addsimps [Split, Case_In0, Case_In1];
+
+
(**** UN x. B(x) rules ****)
goalw Univ.thy [ntrunc_def] "ntrunc k (UN x. f(x)) = (UN x. ntrunc k (f x))";
@@ -562,15 +570,15 @@
(*** Domain ***)
goal Univ.thy "fst `` diag(A) = A";
-by (Blast_tac 1);
+by Auto_tac;
qed "fst_image_diag";
goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
-by (Blast_tac 1);
+by Auto_tac;
qed "fst_image_dprod";
goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
-by (Blast_tac 1);
+by Auto_tac;
qed "fst_image_dsum";
Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum];