src/HOL/Induct/LFilter.ML
changeset 4521 c7f56322a84b
parent 4477 b3e5857d8d99
child 4535 f24cebc299e4
     1.1 --- a/src/HOL/Induct/LFilter.ML	Wed Jan 07 13:55:54 1998 +0100
     1.2 +++ b/src/HOL/Induct/LFilter.ML	Thu Jan 08 11:21:45 1998 +0100
     1.3 @@ -71,32 +71,34 @@
     1.4  goalw thy [find_def] "find p LNil = LNil";
     1.5  by (blast_tac (claset() addIs [select_equality]) 1);
     1.6  qed "find_LNil";
     1.7 +Addsimps [find_LNil];
     1.8  
     1.9  goalw thy [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
    1.10  by (blast_tac (claset() addIs [select_equality] addDs [findRel_functional]) 1);
    1.11  qed "findRel_imp_find";
    1.12 +Addsimps [findRel_imp_find];
    1.13  
    1.14  goal thy "!!p. p x ==> find p (LCons x l) = LCons x l";
    1.15  by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
    1.16  qed "find_LCons_found";
    1.17 +Addsimps [find_LCons_found];
    1.18  
    1.19  goalw thy [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
    1.20  by (blast_tac (claset() addIs [select_equality]) 1);
    1.21  qed "diverge_find_LNil";
    1.22 -
    1.23  Addsimps [diverge_find_LNil];
    1.24  
    1.25  goal thy "!!p. ~ (p x) ==> find p (LCons x l) = find p l";
    1.26  by (case_tac "LCons x l : Domain(findRel p)" 1);
    1.27  by (Asm_full_simp_tac 2);
    1.28  by (Clarify_tac 1);
    1.29 -by (asm_simp_tac (simpset() addsimps [findRel_imp_find]) 1);
    1.30 +by (Asm_simp_tac 1);
    1.31  by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
    1.32  qed "find_LCons_seek";
    1.33 +Addsimps [find_LCons_seek];
    1.34  
    1.35  goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
    1.36 -by (asm_simp_tac (simpset() addsimps [find_LCons_found, find_LCons_seek]
    1.37 -                           addsplits [expand_if]) 1);
    1.38 +by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
    1.39  qed "find_LCons";
    1.40  
    1.41  
    1.42 @@ -105,54 +107,60 @@
    1.43  
    1.44  goal thy "lfilter p LNil = LNil";
    1.45  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
    1.46 -by (simp_tac (simpset() addsimps [find_LNil]) 1);
    1.47 +by (Simp_tac 1);
    1.48  qed "lfilter_LNil";
    1.49 +Addsimps [lfilter_LNil];
    1.50  
    1.51  goal thy "!!p. l ~: Domain(findRel p) ==> lfilter p l = LNil";
    1.52  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
    1.53  by (Asm_simp_tac 1);
    1.54  qed "diverge_lfilter_LNil";
    1.55  
    1.56 +Addsimps [diverge_lfilter_LNil];
    1.57 +
    1.58  
    1.59  goal thy "!!p. p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
    1.60  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
    1.61 -by (asm_simp_tac (simpset() addsimps [find_LCons_found]) 1);
    1.62 +by (Asm_simp_tac 1);
    1.63  qed "lfilter_LCons_found";
    1.64 +(*This rewrite and lfilter_LCons_seek are NOT added because lfilter_LCons
    1.65 +  subsumes both*)
    1.66  
    1.67  
    1.68  goal thy "!!p. (l, LCons x l') : findRel p \
    1.69  \              ==> lfilter p l = LCons x (lfilter p l')";
    1.70  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
    1.71 -by (asm_simp_tac (simpset() addsimps [findRel_imp_find]) 1);
    1.72 +by (Asm_simp_tac 1);
    1.73  qed "findRel_imp_lfilter";
    1.74  
    1.75 +Addsimps [findRel_imp_lfilter];
    1.76 +
    1.77 +
    1.78  goal thy "!!p. ~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
    1.79  by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
    1.80  by (case_tac "LCons x l : Domain(findRel p)" 1);
    1.81 -by (asm_full_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
    1.82 +by (Asm_full_simp_tac 2);
    1.83  by (etac Domain_findRelE 1);
    1.84  by (safe_tac (claset() delrules [conjI]));
    1.85 -by (asm_full_simp_tac 
    1.86 -    (simpset() addsimps [findRel_imp_lfilter, findRel_imp_find,
    1.87 -                        find_LCons_seek]) 1);
    1.88 +by (Asm_full_simp_tac 1);
    1.89  qed "lfilter_LCons_seek";
    1.90  
    1.91  
    1.92  goal thy "lfilter p (LCons x l) = \
    1.93  \         (if p x then LCons x (lfilter p l) else lfilter p l)";
    1.94  by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]
    1.95 -                           addsplits [expand_if]) 1);
    1.96 +                            addsplits [expand_if]) 1);
    1.97  qed "lfilter_LCons";
    1.98  
    1.99  AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
   1.100 -Addsimps [lfilter_LNil, lfilter_LCons];
   1.101 +Addsimps [lfilter_LCons];
   1.102  
   1.103  
   1.104  goal thy "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
   1.105  by (rtac notI 1);
   1.106  by (etac Domain_findRelE 1);
   1.107  by (etac rev_mp 1);
   1.108 -by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
   1.109 +by (Asm_simp_tac 1);
   1.110  qed "lfilter_eq_LNil";
   1.111  
   1.112  
   1.113 @@ -162,7 +170,7 @@
   1.114  by (case_tac "l : Domain(findRel p)" 1);
   1.115  by (etac Domain_findRelE 1);
   1.116  by (Asm_simp_tac 2);
   1.117 -by (asm_simp_tac (simpset() addsimps [findRel_imp_find]) 1);
   1.118 +by (Asm_simp_tac 1);
   1.119  by (Blast_tac 1);
   1.120  qed_spec_mp "lfilter_eq_LCons";
   1.121  
   1.122 @@ -170,9 +178,9 @@
   1.123  goal thy "lfilter p l = LNil  |  \
   1.124  \         (EX y l'. lfilter p l = LCons y (lfilter p l') & p y)";
   1.125  by (case_tac "l : Domain(findRel p)" 1);
   1.126 -by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
   1.127 +by (Asm_simp_tac 2);
   1.128  by (blast_tac (claset() addSEs [Domain_findRelE] 
   1.129 -                       addIs [findRel_imp_lfilter]) 1);
   1.130 +                        addIs  [findRel_imp_lfilter]) 1);
   1.131  qed "lfilter_cases";
   1.132  
   1.133  
   1.134 @@ -228,7 +236,7 @@
   1.135  \                  --> l : Domain (findRel(%x. p x & q x))";
   1.136  by (etac findRel.induct 1);
   1.137  by (blast_tac (claset() addSDs [sym RS lfilter_eq_LCons]
   1.138 -                       addIs  [findRel_conj]) 1);
   1.139 +                        addIs  [findRel_conj]) 1);
   1.140  by Auto_tac;
   1.141  by (dtac (sym RS lfilter_eq_LCons) 1);
   1.142  by Auto_tac;
   1.143 @@ -256,14 +264,13 @@
   1.144  by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
   1.145  by (blast_tac (claset() addIs [impOfSubs Domain_findRel_mono]) 3);
   1.146  (*There are no qs in l: both lists are LNil*)
   1.147 -by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
   1.148 +by (Asm_simp_tac 2);
   1.149  by (etac Domain_findRelE 1);
   1.150  (*case q x*)
   1.151  by (case_tac "p x" 1);
   1.152 -by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter,
   1.153 -                                     findRel_conj RS findRel_imp_lfilter]) 1);
   1.154 +by (asm_simp_tac (simpset() addsimps [findRel_conj RS findRel_imp_lfilter]) 1);
   1.155  (*case q x and ~(p x) *)
   1.156 -by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
   1.157 +by (Asm_simp_tac 1);
   1.158  by (case_tac "l' : Domain (findRel (%x. p x & q x))" 1);
   1.159  (*subcase: there is no p&q in l' and therefore none in l*)
   1.160  by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
   1.161 @@ -271,14 +278,14 @@
   1.162  by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2);
   1.163  by (blast_tac (claset() addIs [findRel_lfilter_Domain_conj]) 3);
   1.164  (*    ...and therefore too, no p in lfilter q l'.  Both results are Lnil*)
   1.165 -by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
   1.166 +by (Asm_simp_tac 2);
   1.167  (*subcase: there is a p&q in l' and therefore also one in l*)
   1.168  by (etac Domain_findRelE 1);
   1.169  by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
   1.170  by (blast_tac (claset() addIs [findRel_conj2]) 2);
   1.171  by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
   1.172  by (blast_tac (claset() addIs [findRel_conj_lfilter]) 2);
   1.173 -by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
   1.174 +by (Asm_simp_tac 1);
   1.175  val lemma = result();
   1.176  
   1.177  
   1.178 @@ -327,9 +334,9 @@
   1.179  by (case_tac "lmap f l : Domain (findRel p)" 1);
   1.180  by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
   1.181  by (blast_tac (claset() addIs [findRel_lmap_Domain]) 3);
   1.182 -by (asm_simp_tac (simpset() addsimps [diverge_lfilter_LNil]) 2);
   1.183 +by (Asm_simp_tac 2);
   1.184  by (etac Domain_findRelE 1);
   1.185  by (forward_tac [lmap_LCons_findRel] 1);
   1.186  by (Clarify_tac 1);
   1.187 -by (asm_simp_tac (simpset() addsimps [findRel_imp_lfilter]) 1);
   1.188 +by (Asm_simp_tac 1);
   1.189  qed "lfilter_lmap";