Adapted to removal of UN1_I, etc
authorpaulson
Wed Nov 05 13:45:01 1997 +0100 (1997-11-05)
changeset 416059826ea67cba
parent 4159 4aff9b7e5597
child 4161 ac7f082e64a5
Adapted to removal of UN1_I, etc
src/HOL/Induct/LList.ML
     1.1 --- a/src/HOL/Induct/LList.ML	Wed Nov 05 13:32:07 1997 +0100
     1.2 +++ b/src/HOL/Induct/LList.ML	Wed Nov 05 13:45:01 1997 +0100
     1.3 @@ -8,6 +8,8 @@
     1.4  
     1.5  open LList;
     1.6  
     1.7 +bind_thm ("UN1_I", UNIV_I RS UN_I);
     1.8 +
     1.9  (** Simplification **)
    1.10  
    1.11  simpset_ref() := simpset() addsplits [expand_split, expand_sum_case];
    1.12 @@ -89,18 +91,20 @@
    1.13  goalw LList.thy [LList_corec_def]
    1.14      "LList_corec a f <= sum_case (%u. NIL) \
    1.15  \                          (split(%z w. CONS z (LList_corec w f))) (f a)";
    1.16 -by (rtac UN1_least 1);
    1.17 -by (res_inst_tac [("n","k")] natE 1);
    1.18 -by (ALLGOALS (Asm_simp_tac));
    1.19 -by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, UN1_upper] 1));
    1.20 +by (rtac UN_least 1);
    1.21 +by (exhaust_tac "k" 1);
    1.22 +by (ALLGOALS Asm_simp_tac);
    1.23 +by (REPEAT (resolve_tac [allI, impI, subset_refl RS CONS_mono, 
    1.24 +			 UNIV_I RS UN_upper] 1));
    1.25  qed "LList_corec_subset1";
    1.26  
    1.27  goalw LList.thy [LList_corec_def]
    1.28      "sum_case (%u. NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
    1.29  \    LList_corec a f";
    1.30  by (simp_tac (simpset() addsimps [CONS_UN1]) 1);
    1.31 -by (safe_tac (claset()));
    1.32 -by (ALLGOALS (res_inst_tac [("x","Suc(?k)")] UN1_I THEN' Asm_simp_tac));
    1.33 +by Safe_tac;
    1.34 +by (ALLGOALS (res_inst_tac [("a","Suc(?k)")] UN_I));
    1.35 +by (ALLGOALS Asm_simp_tac);
    1.36  qed "LList_corec_subset2";
    1.37  
    1.38  (*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
    1.39 @@ -124,7 +128,7 @@
    1.40  goal LList.thy "LList_corec a f : llist({u. True})";
    1.41  by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
    1.42  by (rtac rangeI 1);
    1.43 -by (safe_tac (claset()));
    1.44 +by Safe_tac;
    1.45  by (stac LList_corec 1);
    1.46  by (simp_tac (simpset() addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI]
    1.47                         |> add_eqI) 1);
    1.48 @@ -136,7 +140,7 @@
    1.49  \   llist(range Leaf)";
    1.50  by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
    1.51  by (rtac rangeI 1);
    1.52 -by (safe_tac (claset()));
    1.53 +by Safe_tac;
    1.54  by (stac LList_corec 1);
    1.55  by (asm_simp_tac (simpset() addsimps [list_Fun_NIL_I]) 1);
    1.56  by (fast_tac (claset() addSIs [list_Fun_CONS_I]) 1);
    1.57 @@ -180,7 +184,7 @@
    1.58  goal LList.thy "LListD(diag(A)) <= diag(llist(A))";
    1.59  by (rtac subsetI 1);
    1.60  by (res_inst_tac [("p","x")] PairE 1);
    1.61 -by (safe_tac (claset()));
    1.62 +by Safe_tac;
    1.63  by (rtac diag_eqI 1);
    1.64  by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS 
    1.65            ntrunc_equality) 1);
    1.66 @@ -255,7 +259,7 @@
    1.67  by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
    1.68  by (etac LListD_coinduct 1);
    1.69  by (asm_simp_tac (simpset() addsimps [LListD_eq_diag]) 1);
    1.70 -by (safe_tac (claset()));
    1.71 +by Safe_tac;
    1.72  qed "LList_equalityI";
    1.73  
    1.74  
    1.75 @@ -271,7 +275,7 @@
    1.76  by (res_inst_tac [("A", "{u. True}"),
    1.77                    ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
    1.78  by (rtac rangeI 1);
    1.79 -by (safe_tac (claset()));
    1.80 +by Safe_tac;
    1.81  by (stac prem1 1);
    1.82  by (stac prem2 1);
    1.83  by (simp_tac (simpset() addsimps [LListD_Fun_NIL_I,
    1.84 @@ -333,7 +337,7 @@
    1.85    The containing set is simply the singleton {Lconst(M)}. *)
    1.86  goal LList.thy "!!M A. M:A ==> Lconst(M): llist(A)";
    1.87  by (rtac (singletonI RS llist_coinduct) 1);
    1.88 -by (safe_tac (claset()));
    1.89 +by Safe_tac;
    1.90  by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1);
    1.91  by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
    1.92  qed "Lconst_type";
    1.93 @@ -460,7 +464,7 @@
    1.94  val [major,minor] = goal LList.thy
    1.95      "[| M: llist(A);  !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
    1.96  by (rtac (major RS imageI RS llist_coinduct) 1);
    1.97 -by (safe_tac (claset()));
    1.98 +by Safe_tac;
    1.99  by (etac llist.elim 1);
   1.100  by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
   1.101  by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I, 
   1.102 @@ -478,7 +482,7 @@
   1.103  val [prem] = goalw LList.thy [o_def]
   1.104      "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
   1.105  by (rtac (prem RS imageI RS LList_equalityI) 1);
   1.106 -by (safe_tac (claset()));
   1.107 +by Safe_tac;
   1.108  by (etac llist.elim 1);
   1.109  by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
   1.110  by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
   1.111 @@ -487,7 +491,7 @@
   1.112  
   1.113  val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x. x) M = M";
   1.114  by (rtac (prem RS imageI RS LList_equalityI) 1);
   1.115 -by (safe_tac (claset()));
   1.116 +by Safe_tac;
   1.117  by (etac llist.elim 1);
   1.118  by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
   1.119  by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1,
   1.120 @@ -536,7 +540,7 @@
   1.121  by (res_inst_tac
   1.122      [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
   1.123  by (Fast_tac 1);
   1.124 -by (safe_tac (claset()));
   1.125 +by Safe_tac;
   1.126  by (eres_inst_tac [("a", "u")] llist.elim 1);
   1.127  by (eres_inst_tac [("a", "v")] llist.elim 1);
   1.128  by (ALLGOALS
   1.129 @@ -631,7 +635,7 @@
   1.130  val [prem] = goal LList.thy
   1.131      "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
   1.132  \    prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r";
   1.133 -by (safe_tac (claset()));
   1.134 +by Safe_tac;
   1.135  by (rtac (prem RS subsetD RS SigmaE2) 1);
   1.136  by (assume_tac 1);
   1.137  by (asm_simp_tac (simpset() addsimps [o_def,prod_fun,Abs_llist_inverse]) 1);
   1.138 @@ -757,7 +761,7 @@
   1.139  by (res_inst_tac [("r", "range(%u.(lmap f (iterates f u),iterates f (f u)))")] 
   1.140      llist_equalityI 1);
   1.141  by (rtac rangeI 1);
   1.142 -by (safe_tac (claset()));
   1.143 +by Safe_tac;
   1.144  by (res_inst_tac [("x1", "f(u)")] (iterates RS ssubst) 1);
   1.145  by (res_inst_tac [("x1", "u")] (iterates RS ssubst) 1);
   1.146  by (Simp_tac 1);
   1.147 @@ -797,7 +801,7 @@
   1.148  \                    nat_rec (iterates f u) (%m y. lmap f y) n))")] 
   1.149      llist_equalityI 1);
   1.150  by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
   1.151 -by (safe_tac (claset()));
   1.152 +by (Clarify_tac 1);
   1.153  by (stac iterates 1);
   1.154  by (stac prem 1);
   1.155  by (stac fun_power_lmap 1);
   1.156 @@ -849,7 +853,7 @@
   1.157  by (res_inst_tac [("r", "range(%u.(lappend (iterates f u) N,iterates f u))")] 
   1.158      llist_equalityI 1);
   1.159  by (rtac rangeI 1);
   1.160 -by (safe_tac (claset()));
   1.161 +by Safe_tac;
   1.162  by (stac iterates 1);
   1.163  by (Simp_tac 1);
   1.164  qed "lappend_iterates";
   1.165 @@ -864,7 +868,7 @@
   1.166      llist_equalityI 1);
   1.167  by (rtac UN1_I 1);
   1.168  by (rtac rangeI 1);
   1.169 -by (safe_tac (claset()));
   1.170 +by Safe_tac;
   1.171  by (res_inst_tac [("l", "l")] llistE 1);
   1.172  by (res_inst_tac [("l", "n")] llistE 1);
   1.173  by (ALLGOALS Asm_simp_tac);