src/HOL/Induct/LList.ML
changeset 4089 96fba19bcbe2
parent 3919 c036caebfc75
child 4160 59826ea67cba
     1.1 --- a/src/HOL/Induct/LList.ML	Mon Nov 03 12:12:10 1997 +0100
     1.2 +++ b/src/HOL/Induct/LList.ML	Mon Nov 03 12:13:18 1997 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  (** Simplification **)
     1.6  
     1.7 -simpset := !simpset addsplits [expand_split, expand_sum_case];
     1.8 +simpset_ref() := simpset() addsplits [expand_split, expand_sum_case];
     1.9  
    1.10  (*For adding _eqI rules to a simpset; we must remove Pair_eq because
    1.11    it may turn an instance of reflexivity into a conjunction!*)
    1.12 @@ -27,7 +27,7 @@
    1.13  
    1.14  goal LList.thy "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
    1.15  let val rew = rewrite_rule [NIL_def, CONS_def] in  
    1.16 -by (fast_tac (!claset addSIs (map rew llist.intrs)
    1.17 +by (fast_tac (claset() addSIs (map rew llist.intrs)
    1.18                        addEs [rew llist.elim]) 1)
    1.19  end;
    1.20  qed "llist_unfold";
    1.21 @@ -63,16 +63,16 @@
    1.22  
    1.23  (*A continuity result?*)
    1.24  goalw LList.thy [CONS_def] "CONS M (UN x. f(x)) = (UN x. CONS M (f x))";
    1.25 -by (simp_tac (!simpset addsimps [In1_UN1, Scons_UN1_y]) 1);
    1.26 +by (simp_tac (simpset() addsimps [In1_UN1, Scons_UN1_y]) 1);
    1.27  qed "CONS_UN1";
    1.28  
    1.29  (*UNUSED; obsolete?
    1.30  goal Prod.thy "split p (%x y. UN z. f x y z) = (UN z. split p (%x y. f x y z))";
    1.31 -by (simp_tac (!simpset addsplits [expand_split]) 1);
    1.32 +by (simp_tac (simpset() addsplits [expand_split]) 1);
    1.33  qed "split_UN1";
    1.34  
    1.35  goal Sum.thy "sum_case s f (%y. UN z. g y z) = (UN z. sum_case s f (%y. g y z))";
    1.36 -by (simp_tac (!simpset addsplits [expand_sum_case]) 1);
    1.37 +by (simp_tac (simpset() addsplits [expand_sum_case]) 1);
    1.38  qed "sum_case2_UN1";
    1.39  *)
    1.40  
    1.41 @@ -98,8 +98,8 @@
    1.42  goalw LList.thy [LList_corec_def]
    1.43      "sum_case (%u. NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
    1.44  \    LList_corec a f";
    1.45 -by (simp_tac (!simpset addsimps [CONS_UN1]) 1);
    1.46 -by (safe_tac (!claset));
    1.47 +by (simp_tac (simpset() addsimps [CONS_UN1]) 1);
    1.48 +by (safe_tac (claset()));
    1.49  by (ALLGOALS (res_inst_tac [("x","Suc(?k)")] UN1_I THEN' Asm_simp_tac));
    1.50  qed "LList_corec_subset2";
    1.51  
    1.52 @@ -124,9 +124,9 @@
    1.53  goal LList.thy "LList_corec a f : llist({u. True})";
    1.54  by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
    1.55  by (rtac rangeI 1);
    1.56 -by (safe_tac (!claset));
    1.57 +by (safe_tac (claset()));
    1.58  by (stac LList_corec 1);
    1.59 -by (simp_tac (!simpset addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI]
    1.60 +by (simp_tac (simpset() addsimps [list_Fun_NIL_I, list_Fun_CONS_I, CollectI]
    1.61                         |> add_eqI) 1);
    1.62  qed "LList_corec_type";
    1.63  
    1.64 @@ -136,10 +136,10 @@
    1.65  \   llist(range Leaf)";
    1.66  by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
    1.67  by (rtac rangeI 1);
    1.68 -by (safe_tac (!claset));
    1.69 +by (safe_tac (claset()));
    1.70  by (stac LList_corec 1);
    1.71 -by (asm_simp_tac (!simpset addsimps [list_Fun_NIL_I]) 1);
    1.72 -by (fast_tac (!claset addSIs [list_Fun_CONS_I]) 1);
    1.73 +by (asm_simp_tac (simpset() addsimps [list_Fun_NIL_I]) 1);
    1.74 +by (fast_tac (claset() addSIs [list_Fun_CONS_I]) 1);
    1.75  qed "LList_corec_type2";
    1.76  
    1.77  
    1.78 @@ -148,22 +148,22 @@
    1.79  (*This theorem is actually used, unlike the many similar ones in ZF*)
    1.80  goal LList.thy "LListD(r) = diag({Numb(0)}) <++> (r <**> LListD(r))";
    1.81  let val rew = rewrite_rule [NIL_def, CONS_def] in  
    1.82 -by (fast_tac (!claset addSIs (map rew LListD.intrs)
    1.83 +by (fast_tac (claset() addSIs (map rew LListD.intrs)
    1.84                        addEs [rew LListD.elim]) 1)
    1.85  end;
    1.86  qed "LListD_unfold";
    1.87  
    1.88  goal LList.thy "!M N. (M,N) : LListD(diag(A)) --> ntrunc k M = ntrunc k N";
    1.89  by (res_inst_tac [("n", "k")] less_induct 1);
    1.90 -by (safe_tac ((claset_of "Fun") delrules [equalityI]));
    1.91 +by (safe_tac ((claset_of Fun.thy) delrules [equalityI]));
    1.92  by (etac LListD.elim 1);
    1.93 -by (safe_tac (claset_of "Prod" delrules [equalityI] addSEs [diagE]));
    1.94 +by (safe_tac (claset_of Prod.thy delrules [equalityI] addSEs [diagE]));
    1.95  by (res_inst_tac [("n", "n")] natE 1);
    1.96 -by (asm_simp_tac (!simpset addsimps [ntrunc_0]) 1);
    1.97 +by (asm_simp_tac (simpset() addsimps [ntrunc_0]) 1);
    1.98  by (rename_tac "n'" 1);
    1.99  by (res_inst_tac [("n", "n'")] natE 1);
   1.100 -by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_one_In1]) 1);
   1.101 -by (asm_simp_tac (!simpset addsimps [CONS_def, ntrunc_In1, ntrunc_Scons, less_Suc_eq]) 1);
   1.102 +by (asm_simp_tac (simpset() addsimps [CONS_def, ntrunc_one_In1]) 1);
   1.103 +by (asm_simp_tac (simpset() addsimps [CONS_def, ntrunc_In1, ntrunc_Scons, less_Suc_eq]) 1);
   1.104  qed "LListD_implies_ntrunc_equality";
   1.105  
   1.106  (*The domain of the LListD relation*)
   1.107 @@ -180,7 +180,7 @@
   1.108  goal LList.thy "LListD(diag(A)) <= diag(llist(A))";
   1.109  by (rtac subsetI 1);
   1.110  by (res_inst_tac [("p","x")] PairE 1);
   1.111 -by (safe_tac (!claset));
   1.112 +by (safe_tac (claset()));
   1.113  by (rtac diag_eqI 1);
   1.114  by (rtac (LListD_implies_ntrunc_equality RS spec RS spec RS mp RS 
   1.115            ntrunc_equality) 1);
   1.116 @@ -229,7 +229,7 @@
   1.117  by (etac ssubst 1);
   1.118  by (eresolve_tac [llist.elim] 1);
   1.119  by (ALLGOALS
   1.120 -    (asm_simp_tac (!simpset addsimps [diagI, LListD_Fun_NIL_I,
   1.121 +    (asm_simp_tac (simpset() addsimps [diagI, LListD_Fun_NIL_I,
   1.122                                        LListD_Fun_CONS_I])));
   1.123  qed "diag_subset_LListD";
   1.124  
   1.125 @@ -242,7 +242,7 @@
   1.126      "!!M N. M: llist(A) ==> (M,M) : LListD_Fun (diag A) (X Un diag(llist(A)))";
   1.127  by (rtac (LListD_eq_diag RS subst) 1);
   1.128  by (rtac LListD_Fun_LListD_I 1);
   1.129 -by (asm_simp_tac (!simpset addsimps [LListD_eq_diag, diagI]) 1);
   1.130 +by (asm_simp_tac (simpset() addsimps [LListD_eq_diag, diagI]) 1);
   1.131  qed "LListD_Fun_diag_I";
   1.132  
   1.133  
   1.134 @@ -254,8 +254,8 @@
   1.135  \         |] ==>  M=N";
   1.136  by (rtac (LListD_subset_diag RS subsetD RS diagE) 1);
   1.137  by (etac LListD_coinduct 1);
   1.138 -by (asm_simp_tac (!simpset addsimps [LListD_eq_diag]) 1);
   1.139 -by (safe_tac (!claset));
   1.140 +by (asm_simp_tac (simpset() addsimps [LListD_eq_diag]) 1);
   1.141 +by (safe_tac (claset()));
   1.142  qed "LList_equalityI";
   1.143  
   1.144  
   1.145 @@ -271,10 +271,10 @@
   1.146  by (res_inst_tac [("A", "{u. True}"),
   1.147                    ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
   1.148  by (rtac rangeI 1);
   1.149 -by (safe_tac (!claset));
   1.150 +by (safe_tac (claset()));
   1.151  by (stac prem1 1);
   1.152  by (stac prem2 1);
   1.153 -by (simp_tac (!simpset addsimps [LListD_Fun_NIL_I,
   1.154 +by (simp_tac (simpset() addsimps [LListD_Fun_NIL_I,
   1.155                                   CollectI RS LListD_Fun_CONS_I]
   1.156                         |> add_eqI) 1);
   1.157  qed "LList_corec_unique";
   1.158 @@ -294,7 +294,7 @@
   1.159  
   1.160  goalw LList.thy [CONS_def]
   1.161      "ntrunc (Suc(Suc(k))) (CONS M N) = CONS (ntrunc k M) (ntrunc k N)";
   1.162 -by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_In1]) 1);
   1.163 +by (simp_tac (simpset() addsimps [ntrunc_Scons,ntrunc_In1]) 1);
   1.164  qed "ntrunc_CONS";
   1.165  
   1.166  val [prem1,prem2] = goal LList.thy
   1.167 @@ -310,12 +310,12 @@
   1.168  by (rename_tac "y" 1);
   1.169  by (stac prem1 1);
   1.170  by (stac prem2 1);
   1.171 -by (simp_tac (!simpset addsplits [expand_sum_case]) 1);
   1.172 +by (simp_tac (simpset() addsplits [expand_sum_case]) 1);
   1.173  by (strip_tac 1);
   1.174  by (res_inst_tac [("n", "n")] natE 1);
   1.175  by (rename_tac "m" 2);
   1.176  by (res_inst_tac [("n", "m")] natE 2);
   1.177 -by (ALLGOALS(asm_simp_tac(!simpset addsimps
   1.178 +by (ALLGOALS(asm_simp_tac(simpset() addsimps
   1.179              [ntrunc_0,ntrunc_one_CONS,ntrunc_CONS, less_Suc_eq])));
   1.180  result();
   1.181  
   1.182 @@ -333,7 +333,7 @@
   1.183    The containing set is simply the singleton {Lconst(M)}. *)
   1.184  goal LList.thy "!!M A. M:A ==> Lconst(M): llist(A)";
   1.185  by (rtac (singletonI RS llist_coinduct) 1);
   1.186 -by (safe_tac (!claset));
   1.187 +by (safe_tac (claset()));
   1.188  by (res_inst_tac [("P", "%u. u: ?A")] (Lconst RS ssubst) 1);
   1.189  by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
   1.190  qed "Lconst_type";
   1.191 @@ -392,7 +392,7 @@
   1.192  (** Injectiveness of CONS and LCons **)
   1.193  
   1.194  goalw LList.thy [CONS_def] "(CONS M N=CONS M' N') = (M=M' & N=N')";
   1.195 -by (fast_tac (!claset addSEs [Scons_inject]) 1);
   1.196 +by (fast_tac (claset() addSEs [Scons_inject]) 1);
   1.197  qed "CONS_CONS_eq2";
   1.198  
   1.199  bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
   1.200 @@ -460,9 +460,9 @@
   1.201  val [major,minor] = goal LList.thy
   1.202      "[| M: llist(A);  !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
   1.203  by (rtac (major RS imageI RS llist_coinduct) 1);
   1.204 -by (safe_tac (!claset));
   1.205 +by (safe_tac (claset()));
   1.206  by (etac llist.elim 1);
   1.207 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
   1.208 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
   1.209  by (REPEAT (ares_tac [list_Fun_NIL_I, list_Fun_CONS_I, 
   1.210                        minor, imageI, UnI1] 1));
   1.211  qed "Lmap_type";
   1.212 @@ -478,18 +478,18 @@
   1.213  val [prem] = goalw LList.thy [o_def]
   1.214      "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
   1.215  by (rtac (prem RS imageI RS LList_equalityI) 1);
   1.216 -by (safe_tac (!claset));
   1.217 +by (safe_tac (claset()));
   1.218  by (etac llist.elim 1);
   1.219 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
   1.220 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
   1.221  by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI, UnI1,
   1.222                        rangeI RS LListD_Fun_CONS_I] 1));
   1.223  qed "Lmap_compose";
   1.224  
   1.225  val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x. x) M = M";
   1.226  by (rtac (prem RS imageI RS LList_equalityI) 1);
   1.227 -by (safe_tac (!claset));
   1.228 +by (safe_tac (claset()));
   1.229  by (etac llist.elim 1);
   1.230 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [Lmap_NIL,Lmap_CONS])));
   1.231 +by (ALLGOALS (asm_simp_tac (simpset() addsimps [Lmap_NIL,Lmap_CONS])));
   1.232  by (REPEAT (ares_tac [LListD_Fun_NIL_I, imageI RS UnI1,
   1.233                        rangeI RS LListD_Fun_CONS_I] 1));
   1.234  qed "Lmap_ident";
   1.235 @@ -536,12 +536,12 @@
   1.236  by (res_inst_tac
   1.237      [("X", "UN u:llist(A). UN v: llist(A). {Lappend u v}")] llist_coinduct 1);
   1.238  by (Fast_tac 1);
   1.239 -by (safe_tac (!claset));
   1.240 +by (safe_tac (claset()));
   1.241  by (eres_inst_tac [("a", "u")] llist.elim 1);
   1.242  by (eres_inst_tac [("a", "v")] llist.elim 1);
   1.243  by (ALLGOALS
   1.244      (Asm_simp_tac THEN'
   1.245 -     fast_tac (!claset addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
   1.246 +     fast_tac (claset() addSIs [llist.NIL_I, list_Fun_NIL_I, list_Fun_CONS_I])));
   1.247  qed "Lappend_type";
   1.248  
   1.249  (*strong co-induction: bisimulation and case analysis on one variable*)
   1.250 @@ -552,9 +552,9 @@
   1.251  by (rtac subsetI 1);
   1.252  by (etac imageE 1);
   1.253  by (eres_inst_tac [("a", "u")] llist.elim 1);
   1.254 -by (asm_simp_tac (!simpset addsimps [Lappend_NIL, list_Fun_llist_I]) 1);
   1.255 +by (asm_simp_tac (simpset() addsimps [Lappend_NIL, list_Fun_llist_I]) 1);
   1.256  by (Asm_simp_tac 1);
   1.257 -by (fast_tac (!claset addSIs [list_Fun_CONS_I]) 1);
   1.258 +by (fast_tac (claset() addSIs [list_Fun_CONS_I]) 1);
   1.259  qed "Lappend_type";
   1.260  
   1.261  (**** Lazy lists as the type 'a llist -- strongly typed versions of above ****)
   1.262 @@ -583,7 +583,7 @@
   1.263  by (assume_tac 1);
   1.264  by (etac rangeE 1);
   1.265  by (rtac (inj_Rep_llist RS injD RS prem2) 1);
   1.266 -by (asm_simp_tac (!simpset delsimps [CONS_CONS_eq] addsimps [Rep_llist_LCons]) 1);
   1.267 +by (asm_simp_tac (simpset() delsimps [CONS_CONS_eq] addsimps [Rep_llist_LCons]) 1);
   1.268  by (etac (Abs_llist_inverse RS ssubst) 1);
   1.269  by (rtac refl 1);
   1.270  qed "llistE";
   1.271 @@ -595,11 +595,11 @@
   1.272  \                           (split(%z w. LCons z (llist_corec w f))) (f a)";
   1.273  by (stac LList_corec 1);
   1.274  by (res_inst_tac [("s","f(a)")] sumE 1);
   1.275 -by (asm_simp_tac (!simpset addsimps [LList_corec_type2]) 1);
   1.276 +by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
   1.277  by (res_inst_tac [("p","y")] PairE 1);
   1.278 -by (asm_simp_tac (!simpset addsimps [LList_corec_type2]) 1);
   1.279 +by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
   1.280  (*FIXME: correct case splits usd to be found automatically:
   1.281 -by (ASM_SIMP_TAC(!simpset addsimps [LList_corec_type2]) 1);*)
   1.282 +by (ASM_SIMP_TAC(simpset() addsimps [LList_corec_type2]) 1);*)
   1.283  qed "llist_corec";
   1.284  
   1.285  (*definitional version of same*)
   1.286 @@ -618,31 +618,31 @@
   1.287      "!!r A. r <= (llist A) Times (llist A) ==> \
   1.288  \           LListD_Fun (diag A) r <= (llist A) Times (llist A)";
   1.289  by (stac llist_unfold 1);
   1.290 -by (simp_tac (!simpset addsimps [NIL_def, CONS_def]) 1);
   1.291 +by (simp_tac (simpset() addsimps [NIL_def, CONS_def]) 1);
   1.292  by (Fast_tac 1);
   1.293  qed "LListD_Fun_subset_Sigma_llist";
   1.294  
   1.295  goal LList.thy
   1.296      "prod_fun Rep_llist Rep_llist `` r <= \
   1.297  \    (llist(range Leaf)) Times (llist(range Leaf))";
   1.298 -by (fast_tac (!claset addIs [Rep_llist]) 1);
   1.299 +by (fast_tac (claset() addIs [Rep_llist]) 1);
   1.300  qed "subset_Sigma_llist";
   1.301  
   1.302  val [prem] = goal LList.thy
   1.303      "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
   1.304  \    prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r";
   1.305 -by (safe_tac (!claset));
   1.306 +by (safe_tac (claset()));
   1.307  by (rtac (prem RS subsetD RS SigmaE2) 1);
   1.308  by (assume_tac 1);
   1.309 -by (asm_simp_tac (!simpset addsimps [o_def,prod_fun,Abs_llist_inverse]) 1);
   1.310 +by (asm_simp_tac (simpset() addsimps [o_def,prod_fun,Abs_llist_inverse]) 1);
   1.311  qed "prod_fun_lemma";
   1.312  
   1.313  goal LList.thy
   1.314      "prod_fun Rep_llist  Rep_llist `` range(%x. (x, x)) = \
   1.315  \    diag(llist(range Leaf))";
   1.316  by (rtac equalityI 1);
   1.317 -by (fast_tac (!claset addIs [Rep_llist]) 1);
   1.318 -by (fast_tac (!claset addSEs [Abs_llist_inverse RS subst]) 1);
   1.319 +by (fast_tac (claset() addIs [Rep_llist]) 1);
   1.320 +by (fast_tac (claset() addSEs [Abs_llist_inverse RS subst]) 1);
   1.321  qed "prod_fun_range_eq_diag";
   1.322  
   1.323  (*Surprisingly hard to prove.  Used with lfilter*)
   1.324 @@ -650,8 +650,8 @@
   1.325      "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
   1.326  by (Auto_tac());
   1.327  by (rtac image_eqI 1);
   1.328 -by (fast_tac (!claset addss (!simpset)) 1);
   1.329 -by (blast_tac (!claset addIs [impOfSubs LListD_Fun_mono]) 1);
   1.330 +by (fast_tac (claset() addss (simpset())) 1);
   1.331 +by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 1);
   1.332  qed "llistD_Fun_mono";
   1.333  
   1.334  (** To show two llists are equal, exhibit a bisimulation! 
   1.335 @@ -757,7 +757,7 @@
   1.336  by (res_inst_tac [("r", "range(%u.(lmap f (iterates f u),iterates f (f u)))")] 
   1.337      llist_equalityI 1);
   1.338  by (rtac rangeI 1);
   1.339 -by (safe_tac (!claset));
   1.340 +by (safe_tac (claset()));
   1.341  by (res_inst_tac [("x1", "f(u)")] (iterates RS ssubst) 1);
   1.342  by (res_inst_tac [("x1", "u")] (iterates RS ssubst) 1);
   1.343  by (Simp_tac 1);
   1.344 @@ -797,7 +797,7 @@
   1.345  \                    nat_rec (iterates f u) (%m y. lmap f y) n))")] 
   1.346      llist_equalityI 1);
   1.347  by (REPEAT (resolve_tac [UN1_I, range_eqI, Pair_cong, nat_rec_0 RS sym] 1));
   1.348 -by (safe_tac (!claset));
   1.349 +by (safe_tac (claset()));
   1.350  by (stac iterates 1);
   1.351  by (stac prem 1);
   1.352  by (stac fun_power_lmap 1);
   1.353 @@ -849,7 +849,7 @@
   1.354  by (res_inst_tac [("r", "range(%u.(lappend (iterates f u) N,iterates f u))")] 
   1.355      llist_equalityI 1);
   1.356  by (rtac rangeI 1);
   1.357 -by (safe_tac (!claset));
   1.358 +by (safe_tac (claset()));
   1.359  by (stac iterates 1);
   1.360  by (Simp_tac 1);
   1.361  qed "lappend_iterates";
   1.362 @@ -864,7 +864,7 @@
   1.363      llist_equalityI 1);
   1.364  by (rtac UN1_I 1);
   1.365  by (rtac rangeI 1);
   1.366 -by (safe_tac (!claset));
   1.367 +by (safe_tac (claset()));
   1.368  by (res_inst_tac [("l", "l")] llistE 1);
   1.369  by (res_inst_tac [("l", "n")] llistE 1);
   1.370  by (ALLGOALS Asm_simp_tac);