# HG changeset patch
# User wenzelm
# Date 878556163 -3600
# Node ID 9f1eaab75e8c08106d4b836d7540e66bd71fff5b
# Parent  96fba19bcbe233db8243b016656925a75e6c02cb
isatool fixclasimp;
removed several blast_tacs;

diff -r 96fba19bcbe2 -r 9f1eaab75e8c src/HOL/Induct/LFilter.ML
--- a/src/HOL/Induct/LFilter.ML	Mon Nov 03 12:13:18 1997 +0100
+++ b/src/HOL/Induct/LFilter.ML	Mon Nov 03 12:22:43 1997 +0100
@@ -31,7 +31,7 @@
 qed_spec_mp "findRel_imp_LCons";
 
 goal thy "!!p. (LNil,l): findRel p ==> R";
-by (blast_tac (!claset addEs [findRel.elim]) 1);
+by (blast_tac (claset() addEs [findRel.elim]) 1);
 qed "findRel_LNil";
 
 AddSEs [findRel_LNil];
@@ -41,7 +41,7 @@
 
 goal thy "!!p. LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
 by (case_tac "p x" 1);
-by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
+by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
 qed "LCons_Domain_findRel";
 
 Addsimps [LCons_Domain_findRel];
@@ -61,27 +61,27 @@
     "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)";
 by (Clarify_tac 1);
 by (etac findRel.induct 1);
-by (blast_tac (!claset addIs (findRel.intrs@prems)) 1);
-by (blast_tac (!claset addIs findRel.intrs) 1);
+by (blast_tac (claset() addIs (findRel.intrs@prems)) 1);
+by (blast_tac (claset() addIs findRel.intrs) 1);
 qed "Domain_findRel_mono";
 
 
 (*** find: basic equations ***)
 
 goalw thy [find_def] "find p LNil = LNil";
-by (blast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (claset() addIs [select_equality]) 1);
 qed "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);
+by (blast_tac (claset() addIs [select_equality] addDs [findRel_functional]) 1);
 qed "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);
+by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
 qed "find_LCons_found";
 
 goalw thy [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
-by (blast_tac (!claset addIs [select_equality]) 1);
+by (blast_tac (claset() addIs [select_equality]) 1);
 qed "diverge_find_LNil";
 
 Addsimps [diverge_find_LNil];
@@ -90,12 +90,12 @@
 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 (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1);
+by (asm_simp_tac (simpset() addsimps [findRel_imp_find]) 1);
+by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
 qed "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]
+by (asm_simp_tac (simpset() addsimps [find_LCons_found, find_LCons_seek]
                            addsplits [expand_if]) 1);
 qed "find_LCons";
 
@@ -105,7 +105,7 @@
 
 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 (simpset() addsimps [find_LNil]) 1);
 qed "lfilter_LNil";
 
 goal thy "!!p. l ~: Domain(findRel p) ==> lfilter p l = LNil";
@@ -116,31 +116,31 @@
 
 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 (simpset() addsimps [find_LCons_found]) 1);
 qed "lfilter_LCons_found";
 
 
 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 (simpset() addsimps [findRel_imp_find]) 1);
 qed "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 (simpset() addsimps [diverge_lfilter_LNil]) 2);
 by (etac Domain_findRelE 1);
-by (safe_tac (!claset delrules [conjI]));
+by (safe_tac (claset() delrules [conjI]));
 by (asm_full_simp_tac 
-    (!simpset addsimps [findRel_imp_lfilter, findRel_imp_find,
+    (simpset() addsimps [findRel_imp_lfilter, findRel_imp_find,
                         find_LCons_seek]) 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]
+by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]
                            addsplits [expand_if]) 1);
 qed "lfilter_LCons";
 
@@ -152,7 +152,7 @@
 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 (simpset() addsimps [findRel_imp_lfilter]) 1);
 qed "lfilter_eq_LNil";
 
 
@@ -162,7 +162,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 (simpset() addsimps [findRel_imp_find]) 1);
 by (Blast_tac 1);
 qed_spec_mp "lfilter_eq_LCons";
 
@@ -170,8 +170,8 @@
 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 (blast_tac (!claset addSEs [Domain_findRelE] 
+by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
+by (blast_tac (claset() addSEs [Domain_findRelE] 
                        addIs [findRel_imp_lfilter]) 1);
 qed "lfilter_cases";
 
@@ -181,15 +181,13 @@
 goal thy "lfilter (%x. True) l = l";
 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
 by (ALLGOALS Simp_tac);
-by (Blast_tac 1);
 qed "lfilter_K_True";
 
 goal thy "lfilter p (lfilter p l) = lfilter p l";
 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
+by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
 by Safe_tac;
 (*Cases: p x is true or false*)
-by (Blast_tac 1);
 by (rtac (lfilter_cases RS disjE) 1);
 by (etac ssubst 1);
 by (Auto_tac());
@@ -203,8 +201,8 @@
 goal thy "!!p. (l,l') : findRel q \
 \           ==> l' = LCons x l'' --> p x --> (l,l') : findRel (%x. p x & q x)";
 by (etac findRel.induct 1);
-by (blast_tac (!claset addIs findRel.intrs) 1);
-by (blast_tac (!claset addIs findRel.intrs) 1);
+by (blast_tac (claset() addIs findRel.intrs) 1);
+by (blast_tac (claset() addIs findRel.intrs) 1);
 qed_spec_mp "findRel_conj_lemma";
 
 val findRel_conj = refl RSN (2, findRel_conj_lemma);
@@ -221,7 +219,7 @@
 \            lxx = LCons x lx --> (lx,lz) : findRel(%x. p x & q x) --> ~ p x \
 \            --> (l,lz) : findRel (%x. p x & q x)";
 by (etac findRel.induct 1);
-by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
+by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
 qed_spec_mp "findRel_conj2";
 
 
@@ -229,14 +227,14 @@
 \              ==> ALL l. lx = lfilter q l \
 \                  --> l : Domain (findRel(%x. p x & q x))";
 by (etac findRel.induct 1);
-by (blast_tac (!claset addSDs [sym RS lfilter_eq_LCons]
+by (blast_tac (claset() addSDs [sym RS lfilter_eq_LCons]
                        addIs  [findRel_conj]) 1);
 by (Auto_tac());
 by (dtac (sym RS lfilter_eq_LCons) 1);
 by (Auto_tac());
 by (dtac spec 1);
 by (dtac (refl RS rev_mp) 1);
-by (blast_tac (!claset addIs [findRel_conj2]) 1);
+by (blast_tac (claset() addIs [findRel_conj2]) 1);
 qed_spec_mp "findRel_lfilter_Domain_conj";
 
 
@@ -244,8 +242,8 @@
 \              ==> l'' = LCons y l' --> \
 \                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
 by (etac findRel.induct 1);
-by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
-by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
 qed_spec_mp "findRel_conj_lfilter";
 
 
@@ -256,40 +254,38 @@
 \                             lfilter (%x. p x & q x) u)))";
 by (case_tac "l : Domain(findRel q)" 1);
 by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
-by (blast_tac (!claset addIs [impOfSubs Domain_findRel_mono]) 3);
+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 (simpset() addsimps [diverge_lfilter_LNil]) 2);
 by (etac Domain_findRelE 1);
 (*case q x*)
 by (case_tac "p x" 1);
-by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter,
+by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter,
                                      findRel_conj RS findRel_imp_lfilter]) 1);
-by (Blast_tac 1);
 (*case q x and ~(p x) *)
-by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
+by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 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);
-by (blast_tac (!claset addIs [findRel_not_conj_Domain]) 3);
+by (blast_tac (claset() addIs [findRel_not_conj_Domain]) 3);
 by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2);
-by (blast_tac (!claset addIs [findRel_lfilter_Domain_conj]) 3);
+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 (simpset() addsimps [diverge_lfilter_LNil]) 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 (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 (Blast_tac 1);
+by (blast_tac (claset() addIs [findRel_conj_lfilter]) 2);
+by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
 val lemma = result();
 
 
 goal thy "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l";
 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
-by (blast_tac (!claset addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
+by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
+by (blast_tac (claset() addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
 qed "lfilter_conj";
 
 
@@ -317,25 +313,23 @@
 \    (l, LCons y l'') : findRel(%x. p(f x)))";
 by (etac findRel.induct 1);
 by (ALLGOALS Asm_simp_tac);
-by (safe_tac (!claset addSDs [lmap_eq_LCons]));
-by (blast_tac (!claset addIs findRel.intrs) 1);
-by (blast_tac (!claset addIs findRel.intrs) 1);
+by (safe_tac (claset() addSDs [lmap_eq_LCons]));
+by (blast_tac (claset() addIs findRel.intrs) 1);
+by (blast_tac (claset() addIs findRel.intrs) 1);
 qed_spec_mp "lmap_LCons_findRel_lemma";
 
 val lmap_LCons_findRel = refl RSN (2, refl RSN (2, lmap_LCons_findRel_lemma));
 
 goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
 by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
-by (ALLGOALS (simp_tac (!simpset addsplits [expand_if])));
+by (ALLGOALS (simp_tac (simpset() addsplits [expand_if])));
 by Safe_tac;
-by (Blast_tac 1);
 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 (blast_tac (claset() addIs [findRel_lmap_Domain]) 3);
+by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 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 (Blast_tac 1);
+by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
 qed "lfilter_lmap";