tidied up list definitions, using type 'a option instead of
authorpaulson
Thu Nov 26 17:40:10 1998 +0100 (1998-11-26)
changeset 59779f0c8869cf71
parent 5976 44290b71a85f
child 5978 fa2c2dd74f8c
tidied up list definitions, using type 'a option instead of
unit + 'a, also using real typedefs instead of faking them with extra rules
src/HOL/Induct/LFilter.thy
src/HOL/Induct/LList.ML
src/HOL/Induct/LList.thy
src/HOL/Induct/SList.ML
src/HOL/Induct/SList.thy
     1.1 --- a/src/HOL/Induct/LFilter.thy	Thu Nov 26 16:37:56 1998 +0100
     1.2 +++ b/src/HOL/Induct/LFilter.thy	Thu Nov 26 17:40:10 1998 +0100
     1.3 @@ -23,7 +23,7 @@
     1.4  
     1.5    lfilter	:: ['a => bool, 'a llist] => 'a llist
     1.6      "lfilter p l == llist_corec l (%l. case find p l of
     1.7 -                                            LNil => Inl ()
     1.8 -                                          | LCons y z => Inr(y,z))"
     1.9 +                                            LNil => None
    1.10 +                                          | LCons y z => Some(y,z))"
    1.11  
    1.12  end
     2.1 --- a/src/HOL/Induct/LList.ML	Thu Nov 26 16:37:56 1998 +0100
     2.2 +++ b/src/HOL/Induct/LList.ML	Thu Nov 26 17:40:10 1998 +0100
     2.3 @@ -10,7 +10,7 @@
     2.4  
     2.5  (** Simplification **)
     2.6  
     2.7 -Addsplits [split_split, split_sum_case];
     2.8 +Addsplits [option.split];
     2.9  
    2.10  (*This justifies using llist in other recursive type definitions*)
    2.11  Goalw llist.defs "A<=B ==> llist(A) <= llist(B)";
    2.12 @@ -22,7 +22,7 @@
    2.13  Goal "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
    2.14  let val rew = rewrite_rule [NIL_def, CONS_def] in  
    2.15  by (fast_tac (claset() addSIs (map rew llist.intrs)
    2.16 -                      addEs [rew llist.elim]) 1)
    2.17 +                       addEs [rew llist.elim]) 1)
    2.18  end;
    2.19  qed "llist_unfold";
    2.20  
    2.21 @@ -63,9 +63,8 @@
    2.22  by (simp_tac (simpset() addsimps [In1_UN1, Scons_UN1_y]) 1);
    2.23  qed "CONS_UN1";
    2.24  
    2.25 -val prems = goalw LList.thy [CONS_def]
    2.26 -    "[| M<=M';  N<=N' |] ==> CONS M N <= CONS M' N'";
    2.27 -by (REPEAT (resolve_tac ([In1_mono,Scons_mono]@prems) 1));
    2.28 +Goalw [CONS_def] "[| M<=M';  N<=N' |] ==> CONS M N <= CONS M' N'";
    2.29 +by (REPEAT (ares_tac [In1_mono,Scons_mono] 1));
    2.30  qed "CONS_mono";
    2.31  
    2.32  Addsimps [LList_corec_fun_def RS def_nat_rec_0,
    2.33 @@ -74,8 +73,8 @@
    2.34  (** The directions of the equality are proved separately **)
    2.35  
    2.36  Goalw [LList_corec_def]
    2.37 -    "LList_corec a f <= sum_case (%u. NIL) \
    2.38 -\                          (split(%z w. CONS z (LList_corec w f))) (f a)";
    2.39 +    "LList_corec a f <= \
    2.40 +\    (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
    2.41  by (rtac UN_least 1);
    2.42  by (exhaust_tac "k" 1);
    2.43  by (ALLGOALS Asm_simp_tac);
    2.44 @@ -84,7 +83,7 @@
    2.45  qed "LList_corec_subset1";
    2.46  
    2.47  Goalw [LList_corec_def]
    2.48 -    "sum_case (%u. NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
    2.49 +    "(case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f)) <= \
    2.50  \    LList_corec a f";
    2.51  by (simp_tac (simpset() addsimps [CONS_UN1]) 1);
    2.52  by Safe_tac;
    2.53 @@ -93,16 +92,16 @@
    2.54  qed "LList_corec_subset2";
    2.55  
    2.56  (*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
    2.57 -Goal "LList_corec a f = sum_case (%u. NIL) \
    2.58 -\                           (split(%z w. CONS z (LList_corec w f))) (f a)";
    2.59 +Goal "LList_corec a f =  \
    2.60 +\     (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
    2.61  by (REPEAT (resolve_tac [equalityI, LList_corec_subset1, 
    2.62                           LList_corec_subset2] 1));
    2.63  qed "LList_corec";
    2.64  
    2.65  (*definitional version of same*)
    2.66 -val [rew] = goal LList.thy
    2.67 -    "[| !!x. h(x) == LList_corec x f |] ==>     \
    2.68 -\    h(a) = sum_case (%u. NIL) (split(%z w. CONS z (h w))) (f a)";
    2.69 +val [rew] = 
    2.70 +Goal "[| !!x. h(x) == LList_corec x f |]     \
    2.71 +\     ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))";
    2.72  by (rewtac rew);
    2.73  by (rtac LList_corec 1);
    2.74  qed "def_LList_corec";
    2.75 @@ -117,16 +116,6 @@
    2.76  by (Simp_tac 1);
    2.77  qed "LList_corec_type";
    2.78  
    2.79 -(*Lemma for the proof of llist_corec*)
    2.80 -Goal "LList_corec a (%z. sum_case Inl (split(%v w. Inr((Leaf(v),w)))) (f z)) : \
    2.81 -\   llist(range Leaf)";
    2.82 -by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
    2.83 -by (rtac rangeI 1);
    2.84 -by Safe_tac;
    2.85 -by (stac LList_corec 1);
    2.86 -by (Asm_simp_tac 1);
    2.87 -qed "LList_corec_type2";
    2.88 -
    2.89  
    2.90  (**** llist equality as a gfp; the bisimulation principle ****)
    2.91  
    2.92 @@ -140,9 +129,9 @@
    2.93  
    2.94  Goal "!M N. (M,N) : LListD(diag A) --> ntrunc k M = ntrunc k N";
    2.95  by (res_inst_tac [("n", "k")] less_induct 1);
    2.96 -by (safe_tac ((claset_of Fun.thy) delrules [equalityI]));
    2.97 +by (safe_tac (claset() delrules [equalityI]));
    2.98  by (etac LListD.elim 1);
    2.99 -by (safe_tac (claset_of Prod.thy delrules [equalityI] addSEs [diagE]));
   2.100 +by (safe_tac (claset() delrules [equalityI]));
   2.101  by (exhaust_tac "n" 1);
   2.102  by (Asm_simp_tac 1);
   2.103  by (rename_tac "n'" 1);
   2.104 @@ -251,9 +240,10 @@
   2.105  Delsimps [Pair_eq];
   2.106  
   2.107  (*abstract proof using a bisimulation*)
   2.108 -val [prem1,prem2] = goal LList.thy
   2.109 - "[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x);  \
   2.110 -\    !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
   2.111 +val [prem1,prem2] = 
   2.112 +Goal
   2.113 + "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w));  \
   2.114 +\    !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |]\
   2.115  \ ==> h1=h2";
   2.116  by (rtac ext 1);
   2.117  (*next step avoids an unknown (and flexflex pair) in simplification*)
   2.118 @@ -267,8 +257,9 @@
   2.119  				  CollectI RS LListD_Fun_CONS_I]) 1);
   2.120  qed "LList_corec_unique";
   2.121  
   2.122 -val [prem] = goal LList.thy
   2.123 - "[| !!x. h(x) = sum_case (%u. NIL) (split(%z w. CONS z (h w))) (f x) |] \
   2.124 +val [prem] = 
   2.125 +Goal 
   2.126 + "[| !!x. h(x) = (case f x of None => NIL | Some(z,w) => CONS z (h w)) |] \
   2.127  \ ==> h = (%x. LList_corec x f)";
   2.128  by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1);
   2.129  qed "equals_LList_corec";
   2.130 @@ -288,9 +279,10 @@
   2.131  Addsimps [ntrunc_one_CONS, ntrunc_CONS];
   2.132  
   2.133  
   2.134 -val [prem1,prem2] = goal LList.thy
   2.135 - "[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x);  \
   2.136 -\    !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
   2.137 +val [prem1,prem2] = 
   2.138 +Goal 
   2.139 + "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w));  \
   2.140 +\    !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |]\
   2.141  \ ==> h1=h2";
   2.142  by (rtac (ntrunc_equality RS ext) 1);
   2.143  by (rename_tac "x k" 1);
   2.144 @@ -328,14 +320,14 @@
   2.145  by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
   2.146  qed "Lconst_type";
   2.147  
   2.148 -Goal "Lconst(M) = LList_corec M (%x. Inr((x,x)))";
   2.149 +Goal "Lconst(M) = LList_corec M (%x. Some((x,x)))";
   2.150  by (rtac (equals_LList_corec RS fun_cong) 1);
   2.151  by (Simp_tac 1);
   2.152  by (rtac Lconst 1);
   2.153  qed "Lconst_eq_LList_corec";
   2.154  
   2.155  (*Thus we could have used gfp in the definition of Lconst*)
   2.156 -Goal "gfp(%N. CONS M N) = LList_corec M (%x. Inr((x,x)))";
   2.157 +Goal "gfp(%N. CONS M N) = LList_corec M (%x. Some((x,x)))";
   2.158  by (rtac (equals_LList_corec RS fun_cong) 1);
   2.159  by (Simp_tac 1);
   2.160  by (rtac (Lconst_fun_mono RS gfp_Tarski) 1);
   2.161 @@ -344,21 +336,31 @@
   2.162  
   2.163  (*** Isomorphisms ***)
   2.164  
   2.165 -Goal "inj(Rep_llist)";
   2.166 +Goal "inj Rep_LList";
   2.167  by (rtac inj_inverseI 1);
   2.168 -by (rtac Rep_llist_inverse 1);
   2.169 -qed "inj_Rep_llist";
   2.170 +by (rtac Rep_LList_inverse 1);
   2.171 +qed "inj_Rep_LList";
   2.172  
   2.173 -Goal "inj_on Abs_llist (llist(range Leaf))";
   2.174 +Goal "inj_on Abs_LList LList";
   2.175  by (rtac inj_on_inverseI 1);
   2.176 -by (etac Abs_llist_inverse 1);
   2.177 -qed "inj_on_Abs_llist";
   2.178 +by (etac Abs_LList_inverse 1);
   2.179 +qed "inj_on_Abs_LList";
   2.180 +
   2.181 +Goalw [LList_def] "x : llist (range Leaf) ==> x : LList";
   2.182 +by (Asm_simp_tac 1);
   2.183 +qed "LListI";
   2.184 +
   2.185 +Goalw [LList_def] "x : LList ==> x : llist (range Leaf)";
   2.186 +by (Asm_simp_tac 1);
   2.187 +qed "LListD";
   2.188 +
   2.189  
   2.190  (** Distinctness of constructors **)
   2.191  
   2.192  Goalw [LNil_def,LCons_def] "~ LCons x xs = LNil";
   2.193 -by (rtac (CONS_not_NIL RS (inj_on_Abs_llist RS inj_on_contraD)) 1);
   2.194 -by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1));
   2.195 +by (rtac (CONS_not_NIL RS (inj_on_Abs_LList RS inj_on_contraD)) 1);
   2.196 +by (REPEAT (resolve_tac (llist.intrs @
   2.197 +			 [rangeI, LListI, Rep_LList RS LListD]) 1));
   2.198  qed "LCons_not_LNil";
   2.199  
   2.200  bind_thm ("LNil_not_LCons", LCons_not_LNil RS not_sym);
   2.201 @@ -368,16 +370,14 @@
   2.202  
   2.203  (** llist constructors **)
   2.204  
   2.205 -Goalw [LNil_def]
   2.206 -    "Rep_llist(LNil) = NIL";
   2.207 -by (rtac (llist.NIL_I RS Abs_llist_inverse) 1);
   2.208 -qed "Rep_llist_LNil";
   2.209 +Goalw [LNil_def] "Rep_LList LNil = NIL";
   2.210 +by (rtac (llist.NIL_I RS LListI RS Abs_LList_inverse) 1);
   2.211 +qed "Rep_LList_LNil";
   2.212  
   2.213 -Goalw [LCons_def]
   2.214 -    "Rep_llist(LCons x l) = CONS (Leaf x) (Rep_llist l)";
   2.215 -by (REPEAT (resolve_tac [llist.CONS_I RS Abs_llist_inverse,
   2.216 -                         rangeI, Rep_llist] 1));
   2.217 -qed "Rep_llist_LCons";
   2.218 +Goalw [LCons_def] "Rep_LList(LCons x l) = CONS (Leaf x) (Rep_LList l)";
   2.219 +by (REPEAT (resolve_tac [llist.CONS_I RS LListI RS Abs_LList_inverse,
   2.220 +                         rangeI, Rep_LList RS LListD] 1));
   2.221 +qed "Rep_LList_LCons";
   2.222  
   2.223  (** Injectiveness of CONS and LCons **)
   2.224  
   2.225 @@ -385,14 +385,16 @@
   2.226  by (fast_tac (claset() addSEs [Scons_inject]) 1);
   2.227  qed "CONS_CONS_eq2";
   2.228  
   2.229 -bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
   2.230 +bind_thm ("CONS_inject", CONS_CONS_eq RS iffD1 RS conjE);
   2.231  
   2.232  
   2.233  (*For reasoning about abstract llist constructors*)
   2.234  
   2.235 -AddIs ([Rep_llist]@llist.intrs);
   2.236 -AddSDs [inj_on_Abs_llist RS inj_onD,
   2.237 -        inj_Rep_llist RS injD, Leaf_inject];
   2.238 +AddIs [Rep_LList RS LListD, LListI];
   2.239 +AddIs llist.intrs;
   2.240 +
   2.241 +AddSDs [inj_on_Abs_LList RS inj_onD,
   2.242 +        inj_Rep_LList RS injD];
   2.243  
   2.244  Goalw [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
   2.245  by (Fast_tac 1);
   2.246 @@ -400,8 +402,8 @@
   2.247  
   2.248  AddIffs [LCons_LCons_eq];
   2.249  
   2.250 -val [major] = goal LList.thy "CONS M N: llist(A) ==> M: A & N: llist(A)";
   2.251 -by (rtac (major RS llist.elim) 1);
   2.252 +Goal "CONS M N: llist(A) ==> M: A & N: llist(A)";
   2.253 +by (etac llist.elim 1);
   2.254  by (etac CONS_neq_NIL 1);
   2.255  by (Fast_tac 1);
   2.256  qed "CONS_D2";
   2.257 @@ -412,7 +414,8 @@
   2.258  Addsimps [List_case_NIL, List_case_CONS];
   2.259  
   2.260  (*A special case of list_equality for functions over lazy lists*)
   2.261 -val [Mlist,gMlist,NILcase,CONScase] = goal LList.thy
   2.262 +val [Mlist,gMlist,NILcase,CONScase] = 
   2.263 +Goal
   2.264   "[| M: llist(A); g(NIL): llist(A);                             \
   2.265  \    f(NIL)=g(NIL);                                             \
   2.266  \    !!x l. [| x:A;  l: llist(A) |] ==>                         \
   2.267 @@ -447,8 +450,8 @@
   2.268  Addsimps [Lmap_NIL, Lmap_CONS];
   2.269  
   2.270  (*Another type-checking proof by coinduction*)
   2.271 -val [major,minor] = goal LList.thy
   2.272 -    "[| M: llist(A);  !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
   2.273 +val [major,minor] = 
   2.274 +Goal "[| M: llist(A);  !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
   2.275  by (rtac (major RS imageI RS llist_coinduct) 1);
   2.276  by Safe_tac;
   2.277  by (etac llist.elim 1);
   2.278 @@ -458,16 +461,16 @@
   2.279  qed "Lmap_type";
   2.280  
   2.281  (*This type checking rule synthesises a sufficiently large set for f*)
   2.282 -val [major] = goal LList.thy  "M: llist(A) ==> Lmap f M: llist(f``A)";
   2.283 -by (rtac (major RS Lmap_type) 1);
   2.284 +Goal "M: llist(A) ==> Lmap f M: llist(f``A)";
   2.285 +by (etac Lmap_type 1);
   2.286  by (etac imageI 1);
   2.287  qed "Lmap_type2";
   2.288  
   2.289  (** Two easy results about Lmap **)
   2.290  
   2.291 -val [prem] = goalw LList.thy [o_def]
   2.292 -    "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
   2.293 -by (rtac (prem RS imageI RS LList_equalityI) 1);
   2.294 +Goalw [o_def] "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
   2.295 +by (dtac imageI 1);
   2.296 +by (etac LList_equalityI 1);
   2.297  by Safe_tac;
   2.298  by (etac llist.elim 1);
   2.299  by (ALLGOALS Asm_simp_tac);
   2.300 @@ -475,8 +478,9 @@
   2.301                        rangeI RS LListD_Fun_CONS_I] 1));
   2.302  qed "Lmap_compose";
   2.303  
   2.304 -val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x. x) M = M";
   2.305 -by (rtac (prem RS imageI RS LList_equalityI) 1);
   2.306 +Goal "M: llist(A) ==> Lmap (%x. x) M = M";
   2.307 +by (dtac imageI 1);
   2.308 +by (etac LList_equalityI 1);
   2.309  by Safe_tac;
   2.310  by (etac llist.elim 1);
   2.311  by (ALLGOALS Asm_simp_tac);
   2.312 @@ -549,8 +553,8 @@
   2.313  
   2.314  (** llist_case: case analysis for 'a llist **)
   2.315  
   2.316 -Addsimps ([Abs_llist_inverse, Rep_llist_inverse,
   2.317 -           Rep_llist, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
   2.318 +Addsimps ([LListI RS Abs_LList_inverse, Rep_LList_inverse,
   2.319 +           Rep_LList RS LListD, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
   2.320  
   2.321  Goalw [llist_case_def,LNil_def]  "llist_case c d LNil = c";
   2.322  by (Simp_tac 1);
   2.323 @@ -562,39 +566,47 @@
   2.324  qed "llist_case_LCons";
   2.325  
   2.326  (*Elimination is case analysis, not induction.*)
   2.327 -val [prem1,prem2] = goalw LList.thy [NIL_def,CONS_def]
   2.328 -    "[| l=LNil ==> P;  !!x l'. l=LCons x l' ==> P \
   2.329 -\    |] ==> P";
   2.330 -by (rtac (Rep_llist RS llist.elim) 1);
   2.331 -by (rtac (inj_Rep_llist RS injD RS prem1) 1);
   2.332 -by (stac Rep_llist_LNil 1);
   2.333 +val [prem1,prem2] = 
   2.334 +Goalw [NIL_def,CONS_def]
   2.335 +     "[| l=LNil ==> P;  !!x l'. l=LCons x l' ==> P |] ==> P";
   2.336 +by (rtac (Rep_LList RS LListD RS llist.elim) 1);
   2.337 +by (rtac (inj_Rep_LList RS injD RS prem1) 1);
   2.338 +by (stac Rep_LList_LNil 1);
   2.339  by (assume_tac 1);
   2.340  by (etac rangeE 1);
   2.341 -by (rtac (inj_Rep_llist RS injD RS prem2) 1);
   2.342 +by (rtac (inj_Rep_LList RS injD RS prem2) 1);
   2.343  by (asm_simp_tac (simpset() delsimps [CONS_CONS_eq] 
   2.344 -		            addsimps [Rep_llist_LCons]) 1);
   2.345 -by (etac (Abs_llist_inverse RS ssubst) 1);
   2.346 +		            addsimps [Rep_LList_LCons]) 1);
   2.347 +by (etac (LListI RS Abs_LList_inverse RS ssubst) 1);
   2.348  by (rtac refl 1);
   2.349  qed "llistE";
   2.350  
   2.351  (** llist_corec: corecursion for 'a llist **)
   2.352  
   2.353 -Goalw [llist_corec_def,LNil_def,LCons_def]
   2.354 -    "llist_corec a f = sum_case (%u. LNil) \
   2.355 -\                           (split(%z w. LCons z (llist_corec w f))) (f a)";
   2.356 +(*Lemma for the proof of llist_corec*)
   2.357 +Goal "LList_corec a \
   2.358 +\          (%z. case f z of None => None | Some(v,w) => Some(Leaf(v),w)) : \
   2.359 +\       llist(range Leaf)";
   2.360 +by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
   2.361 +by (rtac rangeI 1);
   2.362 +by Safe_tac;
   2.363  by (stac LList_corec 1);
   2.364 -by (res_inst_tac [("s","f(a)")] sumE 1);
   2.365 +by (Force_tac 1);
   2.366 +qed "LList_corec_type2";
   2.367 +
   2.368 +Goalw [llist_corec_def,LNil_def,LCons_def]
   2.369 +    "llist_corec a f =  \
   2.370 +\    (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))";
   2.371 +by (stac LList_corec 1);
   2.372 +by (exhaust_tac "f a" 1);
   2.373  by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
   2.374 -by (res_inst_tac [("p","y")] PairE 1);
   2.375 -by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
   2.376 -(*FIXME: correct case splits usd to be found automatically:
   2.377 -by (ASM_SIMP_TAC(simpset() addsimps [LList_corec_type2]) 1);*)
   2.378 +by (force_tac (claset(), simpset() addsimps [LList_corec_type2]) 1);
   2.379  qed "llist_corec";
   2.380  
   2.381  (*definitional version of same*)
   2.382 -val [rew] = goal LList.thy
   2.383 -    "[| !!x. h(x) == llist_corec x f |] ==>     \
   2.384 -\    h(a) = sum_case (%u. LNil) (split(%z w. LCons z (h w))) (f a)";
   2.385 +val [rew] = 
   2.386 +Goal "[| !!x. h(x) == llist_corec x f |] ==>     \
   2.387 +\     h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))";
   2.388  by (rewtac rew);
   2.389  by (rtac llist_corec 1);
   2.390  qed "def_llist_corec";
   2.391 @@ -611,48 +623,47 @@
   2.392  by (Fast_tac 1);
   2.393  qed "LListD_Fun_subset_Sigma_llist";
   2.394  
   2.395 -Goal "prod_fun Rep_llist Rep_llist `` r <= \
   2.396 +Goal "prod_fun Rep_LList Rep_LList `` r <= \
   2.397  \    (llist(range Leaf)) Times (llist(range Leaf))";
   2.398  by (fast_tac (claset() delrules [image_subsetI]
   2.399 -		       addIs [Rep_llist]) 1);
   2.400 +		       addIs [Rep_LList RS LListD]) 1);
   2.401  qed "subset_Sigma_llist";
   2.402  
   2.403 -val [prem] = goal LList.thy
   2.404 -    "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
   2.405 -\    prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r";
   2.406 +Goal "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
   2.407 +\    prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) `` r <= r";
   2.408  by Safe_tac;
   2.409 -by (rtac (prem RS subsetD RS SigmaE2) 1);
   2.410 +by (etac (subsetD RS SigmaE2) 1);
   2.411  by (assume_tac 1);
   2.412 -by (asm_simp_tac (simpset() addsimps [Abs_llist_inverse]) 1);
   2.413 +by (asm_simp_tac (simpset() addsimps [LListI RS Abs_LList_inverse]) 1);
   2.414  qed "prod_fun_lemma";
   2.415  
   2.416 -Goal "prod_fun Rep_llist  Rep_llist `` range(%x. (x, x)) = \
   2.417 +Goal "prod_fun Rep_LList  Rep_LList `` range(%x. (x, x)) = \
   2.418  \    diag(llist(range Leaf))";
   2.419  by (rtac equalityI 1);
   2.420 -by (fast_tac (claset() addIs [Rep_llist]) 1);
   2.421 +by (Blast_tac 1);
   2.422  by (fast_tac (claset() delSWrapper "split_all_tac"
   2.423 -		       addSEs [Abs_llist_inverse RS subst]) 1);
   2.424 +		       addSEs [LListI RS Abs_LList_inverse RS subst]) 1);
   2.425  qed "prod_fun_range_eq_diag";
   2.426  
   2.427 -(*Surprisingly hard to prove.  Used with lfilter*)
   2.428 +(*Used with lfilter*)
   2.429  Goalw [llistD_Fun_def, prod_fun_def]
   2.430      "A<=B ==> llistD_Fun A <= llistD_Fun B";
   2.431  by Auto_tac;
   2.432  by (rtac image_eqI 1);
   2.433 -by (fast_tac (claset() addss (simpset())) 1);
   2.434 -by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 1);
   2.435 +by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 2);
   2.436 +by (Force_tac 1);
   2.437  qed "llistD_Fun_mono";
   2.438  
   2.439  (** To show two llists are equal, exhibit a bisimulation! 
   2.440        [also admits true equality] **)
   2.441 -val [prem1,prem2] = goalw LList.thy [llistD_Fun_def]
   2.442 +Goalw [llistD_Fun_def]
   2.443      "[| (l1,l2) : r;  r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2";
   2.444 -by (rtac (inj_Rep_llist RS injD) 1);
   2.445 -by (res_inst_tac [("r", "prod_fun Rep_llist Rep_llist ``r"),
   2.446 +by (rtac (inj_Rep_LList RS injD) 1);
   2.447 +by (res_inst_tac [("r", "prod_fun Rep_LList Rep_LList ``r"),
   2.448                    ("A", "range(Leaf)")] 
   2.449          LList_equalityI 1);
   2.450 -by (rtac (prem1 RS prod_fun_imageI) 1);
   2.451 -by (rtac (prem2 RS image_mono RS subset_trans) 1);
   2.452 +by (etac prod_fun_imageI 1);
   2.453 +by (etac (image_mono RS subset_trans) 1);
   2.454  by (rtac (image_compose RS subst) 1);
   2.455  by (rtac (prod_fun_compose RS subst) 1);
   2.456  by (stac image_Un 1);
   2.457 @@ -667,28 +678,27 @@
   2.458  by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1);
   2.459  qed "llistD_Fun_LNil_I";
   2.460  
   2.461 -val [prem] = goalw LList.thy [llistD_Fun_def,LCons_def]
   2.462 +Goalw [llistD_Fun_def,LCons_def]
   2.463      "(l1,l2):r ==> (LCons x l1, LCons x l2) : llistD_Fun(r)";
   2.464  by (rtac (rangeI RS LListD_Fun_CONS_I RS prod_fun_imageI) 1);
   2.465 -by (rtac (prem RS prod_fun_imageI) 1);
   2.466 +by (etac prod_fun_imageI 1);
   2.467  qed "llistD_Fun_LCons_I";
   2.468  
   2.469  (*Utilise the "strong" part, i.e. gfp(f)*)
   2.470 -Goalw [llistD_Fun_def]
   2.471 -     "(l,l) : llistD_Fun(r Un range(%x.(x,x)))";
   2.472 -by (rtac (Rep_llist_inverse RS subst) 1);
   2.473 +Goalw [llistD_Fun_def] "(l,l) : llistD_Fun(r Un range(%x.(x,x)))";
   2.474 +by (rtac (Rep_LList_inverse RS subst) 1);
   2.475  by (rtac prod_fun_imageI 1);
   2.476  by (stac image_Un 1);
   2.477  by (stac prod_fun_range_eq_diag 1);
   2.478 -by (rtac (Rep_llist RS LListD_Fun_diag_I) 1);
   2.479 +by (rtac (Rep_LList RS LListD RS LListD_Fun_diag_I) 1);
   2.480  qed "llistD_Fun_range_I";
   2.481  
   2.482  (*A special case of list_equality for functions over lazy lists*)
   2.483 -val [prem1,prem2] = goal LList.thy
   2.484 -    "[| f(LNil)=g(LNil);                                                \
   2.485 -\       !!x l. (f(LCons x l),g(LCons x l)) :                            \
   2.486 -\              llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v)))   \
   2.487 -\    |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)";
   2.488 +val [prem1,prem2] =
   2.489 +Goal "[| f(LNil)=g(LNil);                                                \
   2.490 +\        !!x l. (f(LCons x l),g(LCons x l)) :                            \
   2.491 +\               llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v)))   \
   2.492 +\     |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)";
   2.493  by (res_inst_tac [("r", "range(%u. (f(u),g(u)))")] llist_equalityI 1);
   2.494  by (rtac rangeI 1);
   2.495  by (rtac subsetI 1);
   2.496 @@ -777,8 +787,7 @@
   2.497  
   2.498  (*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
   2.499    for all u and all n::nat.*)
   2.500 -val [prem] = goal LList.thy
   2.501 -    "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
   2.502 +val [prem] = Goal "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
   2.503  by (rtac ext 1);
   2.504  by (res_inst_tac [("r", 
   2.505     "UN u. range(%n. (nat_rec (h u) (%m y. lmap f y) n, \
     3.1 --- a/src/HOL/Induct/LList.thy	Thu Nov 26 16:37:56 1998 +0100
     3.2 +++ b/src/HOL/Induct/LList.thy	Thu Nov 26 17:40:10 1998 +0100
     3.3 @@ -23,43 +23,12 @@
     3.4         (UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
     3.5  *)
     3.6  
     3.7 -LList = Gfp + SList +
     3.8 -
     3.9 -types
    3.10 -  'a llist
    3.11 -
    3.12 -arities
    3.13 -   llist :: (term)term
    3.14 +LList = Main + SList +
    3.15  
    3.16  consts
    3.17 -  list_Fun   :: ['a item set, 'a item set] => 'a item set
    3.18 -  LListD_Fun :: 
    3.19 -      "[('a item * 'a item)set, ('a item * 'a item)set] => 
    3.20 -      ('a item * 'a item)set"
    3.21  
    3.22    llist      :: 'a item set => 'a item set
    3.23    LListD     :: "('a item * 'a item)set => ('a item * 'a item)set"
    3.24 -  llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
    3.25 -
    3.26 -  Rep_llist  :: 'a llist => 'a item
    3.27 -  Abs_llist  :: 'a item => 'a llist
    3.28 -  LNil       :: 'a llist
    3.29 -  LCons      :: ['a, 'a llist] => 'a llist
    3.30 -  
    3.31 -  llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
    3.32 -
    3.33 -  LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item"
    3.34 -  LList_corec     :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
    3.35 -  llist_corec     :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
    3.36 -
    3.37 -  Lmap       :: ('a item => 'b item) => ('a item => 'b item)
    3.38 -  lmap       :: ('a=>'b) => ('a llist => 'b llist)
    3.39 -
    3.40 -  iterates   :: ['a => 'a, 'a] => 'a llist
    3.41 -
    3.42 -  Lconst     :: 'a item => 'a item
    3.43 -  Lappend    :: ['a item, 'a item] => 'a item
    3.44 -  lappend    :: ['a llist, 'a llist] => 'a llist
    3.45  
    3.46  
    3.47  coinductive "llist(A)"
    3.48 @@ -73,81 +42,92 @@
    3.49      CONS_I "[| (a,b): r;  (M,N) : LListD(r)   
    3.50              |] ==> (CONS a M, CONS b N) : LListD(r)"
    3.51  
    3.52 +
    3.53 +typedef (LList)
    3.54 +  'a llist = "llist(range Leaf)" (llist.NIL_I)
    3.55 +
    3.56 +constdefs
    3.57 +  (*Now used exclusively for abbreviating the coinduction rule*)
    3.58 +  list_Fun   :: ['a item set, 'a item set] => 'a item set
    3.59 +     "list_Fun A X == {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
    3.60 +
    3.61 +  LListD_Fun :: 
    3.62 +      "[('a item * 'a item)set, ('a item * 'a item)set] => 
    3.63 +       ('a item * 'a item)set"
    3.64 +    "LListD_Fun r X ==   
    3.65 +       {z. z = (NIL, NIL) |   
    3.66 +           (? M N a b. z = (CONS a M, CONS b N) & (a, b) : r & (M, N) : X)}"
    3.67 +
    3.68 +  (*the abstract constructors*)
    3.69 +  LNil       :: 'a llist
    3.70 +    "LNil == Abs_LList NIL"
    3.71 +
    3.72 +  LCons      :: ['a, 'a llist] => 'a llist
    3.73 +    "LCons x xs == Abs_LList(CONS (Leaf x) (Rep_LList xs))"
    3.74 +
    3.75 +  llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
    3.76 +    "llist_case c d l == 
    3.77 +       List_case c (%x y. d (inv Leaf x) (Abs_LList y)) (Rep_LList l)"
    3.78 +
    3.79 +  LList_corec_fun :: "[nat, 'a=> ('b item * 'a) option, 'a] => 'b item"
    3.80 +    "LList_corec_fun k f == 
    3.81 +     nat_rec (%x. {})                         
    3.82 +             (%j r x. case f x of None    => NIL
    3.83 +                                | Some(z,w) => CONS z (r w)) 
    3.84 +             k"
    3.85 +
    3.86 +  LList_corec     :: "['a, 'a => ('b item * 'a) option] => 'b item"
    3.87 +    "LList_corec a f == UN k. LList_corec_fun k f a"
    3.88 +
    3.89 +  llist_corec     :: "['a, 'a => ('b * 'a) option] => 'b llist"
    3.90 +    "llist_corec a f == 
    3.91 +       Abs_LList(LList_corec a 
    3.92 +                 (%z. case f z of None      => None
    3.93 +                                | Some(v,w) => Some(Leaf(v), w)))"
    3.94 +
    3.95 +  llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
    3.96 +    "llistD_Fun(r) ==    
    3.97 +        prod_fun Abs_LList Abs_LList ``         
    3.98 +                LListD_Fun (diag(range Leaf))   
    3.99 +                            (prod_fun Rep_LList Rep_LList `` r)"
   3.100 +
   3.101 +
   3.102 +
   3.103 +(*The case syntax for type 'a llist*)
   3.104  translations
   3.105    "case p of LNil => a | LCons x l => b" == "llist_case a (%x l. b) p"
   3.106  
   3.107  
   3.108 -defs
   3.109 -  (*Now used exclusively for abbreviating the coinduction rule*)
   3.110 -  list_Fun_def   "list_Fun A X ==   
   3.111 -                  {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
   3.112 -
   3.113 -  LListD_Fun_def "LListD_Fun r X ==   
   3.114 -                  {z. z = (NIL, NIL) |   
   3.115 -                      (? M N a b. z = (CONS a M, CONS b N) &   
   3.116 -                                  (a, b) : r & (M, N) : X)}"
   3.117 +(** Sample function definitions.  Item-based ones start with L ***)
   3.118  
   3.119 -  (*defining the abstract constructors*)
   3.120 -  LNil_def      "LNil == Abs_llist(NIL)"
   3.121 -  LCons_def     "LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
   3.122 -
   3.123 -  llist_case_def
   3.124 -   "llist_case c d l == 
   3.125 -       List_case c (%x y. d (inv Leaf x) (Abs_llist y)) (Rep_llist l)"
   3.126 -
   3.127 -  LList_corec_fun_def
   3.128 -    "LList_corec_fun k f == 
   3.129 -     nat_rec (%x. {})                         
   3.130 -             (%j r x. case f x of Inl u    => NIL
   3.131 -                                | Inr(z,w) => CONS z (r w)) 
   3.132 -             k"
   3.133 +constdefs
   3.134 +  Lmap       :: ('a item => 'b item) => ('a item => 'b item)
   3.135 +    "Lmap f M == LList_corec M (List_case None (%x M'. Some((f(x), M'))))"
   3.136  
   3.137 -  LList_corec_def
   3.138 -    "LList_corec a f == UN k. LList_corec_fun k f a"
   3.139 -
   3.140 -  llist_corec_def
   3.141 -   "llist_corec a f == 
   3.142 -       Abs_llist(LList_corec a 
   3.143 -                 (%z. case f z of Inl x    => Inl(x)
   3.144 -                               | Inr(v,w) => Inr(Leaf(v), w)))"
   3.145 +  lmap       :: ('a=>'b) => ('a llist => 'b llist)
   3.146 +    "lmap f l == llist_corec l (%z. case z of LNil => None 
   3.147 +                                           | LCons y z => Some(f(y), z))"
   3.148  
   3.149 -  llistD_Fun_def
   3.150 -   "llistD_Fun(r) ==    
   3.151 -        prod_fun Abs_llist Abs_llist ``         
   3.152 -                LListD_Fun (diag(range Leaf))   
   3.153 -                            (prod_fun Rep_llist Rep_llist `` r)"
   3.154 -
   3.155 -  Lconst_def    "Lconst(M) == lfp(%N. CONS M N)"     
   3.156 +  iterates   :: ['a => 'a, 'a] => 'a llist
   3.157 +    "iterates f a == llist_corec a (%x. Some((x, f(x))))"     
   3.158  
   3.159 -  Lmap_def
   3.160 -   "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))"
   3.161 -
   3.162 -  lmap_def
   3.163 -   "lmap f l == llist_corec l (%z. case z of LNil => (Inl ()) 
   3.164 -                                           | LCons y z => Inr(f(y), z))"
   3.165 -
   3.166 -  iterates_def  "iterates f a == llist_corec a (%x. Inr((x, f(x))))"     
   3.167 +  Lconst     :: 'a item => 'a item
   3.168 +    "Lconst(M) == lfp(%N. CONS M N)"     
   3.169  
   3.170  (*Append generates its result by applying f, where
   3.171 -    f((NIL,NIL))          = Inl(())
   3.172 -    f((NIL, CONS N1 N2))  = Inr((N1, (NIL,N2))
   3.173 -    f((CONS M1 M2, N))    = Inr((M1, (M2,N))
   3.174 +    f((NIL,NIL))          = None
   3.175 +    f((NIL, CONS N1 N2))  = Some((N1, (NIL,N2))
   3.176 +    f((CONS M1 M2, N))    = Some((M1, (M2,N))
   3.177  *)
   3.178  
   3.179 -  Lappend_def
   3.180 +  Lappend    :: ['a item, 'a item] => 'a item
   3.181     "Lappend M N == LList_corec (M,N)                                         
   3.182 -     (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2))))) 
   3.183 -                      (%M1 M2 N. Inr((M1, (M2,N))))))"
   3.184 +     (split(List_case (List_case None (%N1 N2. Some((N1, (NIL,N2))))) 
   3.185 +                      (%M1 M2 N. Some((M1, (M2,N))))))"
   3.186  
   3.187 -  lappend_def
   3.188 -   "lappend l n == llist_corec (l,n)                                         
   3.189 -   (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2))))) 
   3.190 -                     (%l1 l2 n. Inr((l1, (l2,n))))))"
   3.191 -
   3.192 -rules
   3.193 -    (*faking a type definition...*)
   3.194 -  Rep_llist         "Rep_llist(xs): llist(range(Leaf))"
   3.195 -  Rep_llist_inverse "Abs_llist(Rep_llist(xs)) = xs"
   3.196 -  Abs_llist_inverse "M: llist(range(Leaf)) ==> Rep_llist(Abs_llist(M)) = M"
   3.197 +  lappend    :: ['a llist, 'a llist] => 'a llist
   3.198 +    "lappend l n == llist_corec (l,n)                                         
   3.199 +       (split(llist_case (llist_case None (%n1 n2. Some((n1, (LNil,n2))))) 
   3.200 +                         (%l1 l2 n. Some((l1, (l2,n))))))"
   3.201  
   3.202  end
     4.1 --- a/src/HOL/Induct/SList.ML	Thu Nov 26 16:37:56 1998 +0100
     4.2 +++ b/src/HOL/Induct/SList.ML	Thu Nov 26 17:40:10 1998 +0100
     4.3 @@ -6,6 +6,15 @@
     4.4  Definition of type 'a list by a least fixed point
     4.5  *)
     4.6  
     4.7 +
     4.8 +Goalw [List_def] "x : list (range Leaf) ==> x : List";
     4.9 +by (Asm_simp_tac 1);
    4.10 +qed "ListI";
    4.11 +
    4.12 +Goalw [List_def] "x : List ==> x : list (range Leaf)";
    4.13 +by (Asm_simp_tac 1);
    4.14 +qed "ListD";
    4.15 +
    4.16  val list_con_defs = [NIL_def, CONS_def];
    4.17  
    4.18  Goal "list(A) = {Numb(0)} <+> (A <*> list(A))";
    4.19 @@ -28,16 +37,17 @@
    4.20  qed "list_sexp";
    4.21  
    4.22  (* A <= sexp ==> list(A) <= sexp *)
    4.23 -bind_thm ("list_subset_sexp", ([list_mono, list_sexp] MRS subset_trans));
    4.24 +bind_thm ("list_subset_sexp", [list_mono, list_sexp] MRS subset_trans);
    4.25  
    4.26  (*Induction for the type 'a list *)
    4.27 -val prems = goalw SList.thy [Nil_def,Cons_def]
    4.28 +val prems = Goalw [Nil_def,Cons_def]
    4.29      "[| P(Nil);   \
    4.30  \       !!x xs. P(xs) ==> P(x # xs) |]  ==> P(l)";
    4.31 -by (rtac (Rep_list_inverse RS subst) 1);   (*types force good instantiation*)
    4.32 -by (rtac (Rep_list RS list.induct) 1);
    4.33 +by (rtac (Rep_List_inverse RS subst) 1);   (*types force good instantiation*)
    4.34 +by (rtac (Rep_List RS ListD RS list.induct) 1);
    4.35  by (REPEAT (ares_tac prems 1
    4.36 -     ORELSE eresolve_tac [rangeE, ssubst, Abs_list_inverse RS subst] 1));
    4.37 +     ORELSE eresolve_tac [rangeE, ssubst, 
    4.38 +			  ListI RS Abs_List_inverse RS subst] 1));
    4.39  qed "list_induct2";
    4.40  
    4.41  (*Perform induction on xs. *)
    4.42 @@ -47,15 +57,15 @@
    4.43  
    4.44  (*** Isomorphisms ***)
    4.45  
    4.46 -Goal "inj(Rep_list)";
    4.47 +Goal "inj Rep_List";
    4.48  by (rtac inj_inverseI 1);
    4.49 -by (rtac Rep_list_inverse 1);
    4.50 -qed "inj_Rep_list";
    4.51 +by (rtac Rep_List_inverse 1);
    4.52 +qed "inj_Rep_List";
    4.53  
    4.54 -Goal "inj_on Abs_list (list(range Leaf))";
    4.55 +Goal "inj_on Abs_List List";
    4.56  by (rtac inj_on_inverseI 1);
    4.57 -by (etac Abs_list_inverse 1);
    4.58 -qed "inj_on_Abs_list";
    4.59 +by (etac Abs_List_inverse 1);
    4.60 +qed "inj_on_Abs_List";
    4.61  
    4.62  (** Distinctness of constructors **)
    4.63  
    4.64 @@ -68,8 +78,8 @@
    4.65  val NIL_neq_CONS = sym RS CONS_neq_NIL;
    4.66  
    4.67  Goalw [Nil_def,Cons_def] "x # xs ~= Nil";
    4.68 -by (rtac (CONS_not_NIL RS (inj_on_Abs_list RS inj_on_contraD)) 1);
    4.69 -by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1));
    4.70 +by (rtac (CONS_not_NIL RS (inj_on_Abs_List RS inj_on_contraD)) 1);
    4.71 +by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_List RS ListD, ListI]) 1));
    4.72  qed "Cons_not_Nil";
    4.73  
    4.74  bind_thm ("Nil_not_Cons", Cons_not_Nil RS not_sym);
    4.75 @@ -81,27 +91,26 @@
    4.76  qed "CONS_CONS_eq";
    4.77  
    4.78  (*For reasoning about abstract list constructors*)
    4.79 -AddIs ([Rep_list] @ list.intrs);
    4.80 +AddIs [Rep_List RS ListD, ListI];
    4.81 +AddIs list.intrs;
    4.82  
    4.83  AddIffs [CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq];
    4.84  
    4.85 -AddSDs [inj_on_Abs_list RS inj_onD,
    4.86 -        inj_Rep_list RS injD, Leaf_inject];
    4.87 +AddSDs [inj_on_Abs_List RS inj_onD,
    4.88 +        inj_Rep_List RS injD, Leaf_inject];
    4.89  
    4.90  Goalw [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
    4.91  by (Fast_tac 1);
    4.92  qed "Cons_Cons_eq";
    4.93 -bind_thm ("Cons_inject2", (Cons_Cons_eq RS iffD1 RS conjE));
    4.94 +bind_thm ("Cons_inject2", Cons_Cons_eq RS iffD1 RS conjE);
    4.95  
    4.96 -val [major] = goal SList.thy "CONS M N: list(A) ==> M: A & N: list(A)";
    4.97 -by (rtac (major RS setup_induction) 1);
    4.98 +Goal "CONS M N: list(A) ==> M: A & N: list(A)";
    4.99 +by (etac setup_induction 1);
   4.100  by (etac list.induct 1);
   4.101 -by (ALLGOALS (Fast_tac));
   4.102 +by (ALLGOALS Fast_tac);
   4.103  qed "CONS_D";
   4.104  
   4.105 -val prems = goalw SList.thy [CONS_def,In1_def]
   4.106 -    "CONS M N: sexp ==> M: sexp & N: sexp";
   4.107 -by (cut_facts_tac prems 1);
   4.108 +Goalw [CONS_def,In1_def] "CONS M N: sexp ==> M: sexp & N: sexp";
   4.109  by (fast_tac (claset() addSDs [Scons_D]) 1);
   4.110  qed "sexp_CONS_D";
   4.111  
   4.112 @@ -199,13 +208,14 @@
   4.113  
   4.114  (*** list_rec -- by List_rec ***)
   4.115  
   4.116 -val Rep_list_in_sexp =
   4.117 -    [range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD;
   4.118 +val Rep_List_in_sexp =
   4.119 +    [range_Leaf_subset_sexp RS list_subset_sexp, Rep_List RS ListD] 
   4.120 +    MRS subsetD;
   4.121  
   4.122  local
   4.123 -  val list_rec_simps = [Abs_list_inverse, Rep_list_inverse,
   4.124 -                        Rep_list, rangeI, inj_Leaf, inv_f_f,
   4.125 -                        sexp.LeafI, Rep_list_in_sexp]
   4.126 +  val list_rec_simps = [ListI RS Abs_List_inverse, Rep_List_inverse,
   4.127 +                        Rep_List RS ListD, rangeI, inj_Leaf, inv_f_f,
   4.128 +                        sexp.LeafI, Rep_List_in_sexp]
   4.129  in
   4.130    val list_rec_Nil = prove_goalw SList.thy [list_rec_def, Nil_def]
   4.131        "list_rec Nil c h = c"
   4.132 @@ -220,12 +230,12 @@
   4.133  
   4.134  
   4.135  (*Type checking.  Useful?*)
   4.136 -val major::A_subset_sexp::prems = goal SList.thy
   4.137 -    "[| M: list(A);     \
   4.138 -\       A<=sexp;        \
   4.139 -\       c: C(NIL);      \
   4.140 -\       !!x y r. [| x: A;  y: list(A);  r: C(y) |] ==> h x y r: C(CONS x y) \
   4.141 -\    |] ==> List_rec M c h : C(M :: 'a item)";
   4.142 +val major::A_subset_sexp::prems = 
   4.143 +Goal "[| M: list(A);     \
   4.144 +\        A<=sexp;        \
   4.145 +\        c: C(NIL);      \
   4.146 +\        !!x y r. [| x: A;  y: list(A);  r: C(y) |] ==> h x y r: C(CONS x y) \
   4.147 +\     |] ==> List_rec M c h : C(M :: 'a item)";
   4.148  val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD;
   4.149  val sexp_A_I = A_subset_sexp RS subsetD;
   4.150  by (rtac (major RS list.induct) 1);
   4.151 @@ -238,8 +248,7 @@
   4.152  by (rtac list_rec_Nil 1);
   4.153  qed "Rep_map_Nil";
   4.154  
   4.155 -Goalw [Rep_map_def]
   4.156 -    "Rep_map f (x#xs) = CONS (f x) (Rep_map f xs)";
   4.157 +Goalw [Rep_map_def] "Rep_map f (x#xs) = CONS (f x) (Rep_map f xs)";
   4.158  by (rtac list_rec_Cons 1);
   4.159  qed "Rep_map_Cons";
   4.160  
   4.161 @@ -252,21 +261,20 @@
   4.162  by (rtac List_rec_NIL 1);
   4.163  qed "Abs_map_NIL";
   4.164  
   4.165 -val prems = goalw SList.thy [Abs_map_def]
   4.166 -    "[| M: sexp;  N: sexp |] ==> \
   4.167 -\    Abs_map g (CONS M N) = g(M) # Abs_map g N";
   4.168 -by (REPEAT (resolve_tac (List_rec_CONS::prems) 1));
   4.169 +Goalw [Abs_map_def]
   4.170 +    "[| M: sexp;  N: sexp |] ==> Abs_map g (CONS M N) = g(M) # Abs_map g N";
   4.171 +by (REPEAT (ares_tac [List_rec_CONS] 1));
   4.172  qed "Abs_map_CONS";
   4.173  
   4.174  (*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
   4.175 -val [rew] = goal SList.thy
   4.176 -    "[| !!xs. f(xs) == list_rec xs c h |] ==> f([]) = c";
   4.177 +val [rew] = 
   4.178 +Goal "[| !!xs. f(xs) == list_rec xs c h |] ==> f([]) = c";
   4.179  by (rewtac rew);
   4.180  by (rtac list_rec_Nil 1);
   4.181  qed "def_list_rec_Nil";
   4.182  
   4.183 -val [rew] = goal SList.thy
   4.184 -    "[| !!xs. f(xs) == list_rec xs c h |] ==> f(x#xs) = h x xs (f xs)";
   4.185 +val [rew] = 
   4.186 +Goal "[| !!xs. f(xs) == list_rec xs c h |] ==> f(x#xs) = h x xs (f xs)";
   4.187  by (rewtac rew);
   4.188  by (rtac list_rec_Cons 1);
   4.189  qed "def_list_rec_Cons";
   4.190 @@ -327,11 +335,12 @@
   4.191  
   4.192  Addsimps [Rep_map_Nil, Rep_map_Cons, Abs_map_NIL, Abs_map_CONS];
   4.193  
   4.194 -val [major,A_subset_sexp,minor] = goal SList.thy 
   4.195 -    "[| M: list(A);  A<=sexp;  !!z. z: A ==> f(g(z)) = z |] \
   4.196 -\    ==> Rep_map f (Abs_map g M) = M";
   4.197 +val [major,A_subset_sexp,minor] = 
   4.198 +Goal "[| M: list(A);  A<=sexp;  !!z. z: A ==> f(g(z)) = z |] \
   4.199 +\     ==> Rep_map f (Abs_map g M) = M";
   4.200  by (rtac (major RS list.induct) 1);
   4.201 -by (ALLGOALS (asm_simp_tac (simpset() addsimps [sexp_A_I,sexp_ListA_I,minor])));
   4.202 +by (ALLGOALS 
   4.203 +    (asm_simp_tac (simpset() addsimps [sexp_A_I,sexp_ListA_I,minor])));
   4.204  qed "Abs_map_inverse";
   4.205  
   4.206  (*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
   4.207 @@ -339,7 +348,7 @@
   4.208  (** list_case **)
   4.209  
   4.210  Goal "P(list_case a f xs) = ((xs=[] --> P(a)) & \
   4.211 -\                        (!y ys. xs=y#ys --> P(f y ys)))";
   4.212 +\                           (!y ys. xs=y#ys --> P(f y ys)))";
   4.213  by (list_ind_tac "xs" 1);
   4.214  by (ALLGOALS Asm_simp_tac);
   4.215  qed "split_list_case2";
     5.1 --- a/src/HOL/Induct/SList.thy	Thu Nov 26 16:37:56 1998 +0100
     5.2 +++ b/src/HOL/Induct/SList.thy	Thu Nov 26 17:40:10 1998 +0100
     5.3 @@ -12,53 +12,14 @@
     5.4  
     5.5  SList = Sexp +
     5.6  
     5.7 -types
     5.8 -  'a list
     5.9 -
    5.10 -arities
    5.11 -  list :: (term) term
    5.12 -
    5.13 -
    5.14  consts
    5.15  
    5.16    list        :: 'a item set => 'a item set
    5.17 -  Rep_list    :: 'a list => 'a item
    5.18 -  Abs_list    :: 'a item => 'a list
    5.19    NIL         :: 'a item
    5.20    CONS        :: ['a item, 'a item] => 'a item
    5.21 -  Nil         :: 'a list
    5.22 -  "#"         :: ['a, 'a list] => 'a list                         (infixr 65)
    5.23    List_case   :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
    5.24    List_rec    :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
    5.25 -  list_case   :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
    5.26 -  list_rec    :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
    5.27 -  Rep_map     :: ('b => 'a item) => ('b list => 'a item)
    5.28 -  Abs_map     :: ('a item => 'b) => 'a item => 'b list
    5.29 -  null        :: 'a list => bool
    5.30 -  hd          :: 'a list => 'a
    5.31 -  tl,ttl      :: 'a list => 'a list
    5.32 -  set         :: ('a list => 'a set)
    5.33 -  mem         :: ['a, 'a list] => bool                            (infixl 55)
    5.34 -  map         :: ('a=>'b) => ('a list => 'b list)
    5.35 -  "@"         :: ['a list, 'a list] => 'a list                    (infixr 65)
    5.36 -  filter      :: ['a => bool, 'a list] => 'a list
    5.37  
    5.38 -  (* list Enumeration *)
    5.39 -
    5.40 -  "[]"        :: 'a list                              ("[]")
    5.41 -  "@list"     :: args => 'a list                      ("[(_)]")
    5.42 -
    5.43 -  (* Special syntax for filter *)
    5.44 -  "@filter"   :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")
    5.45 -
    5.46 -translations
    5.47 -  "[x, xs]"     == "x#[xs]"
    5.48 -  "[x]"         == "x#[]"
    5.49 -  "[]"          == "Nil"
    5.50 -
    5.51 -  "case xs of Nil => a | y#ys => b" == "list_case a (%y ys. b) xs"
    5.52 -
    5.53 -  "[x:xs . P]"  == "filter (%x. P) xs"
    5.54  
    5.55  defs
    5.56    (* Defining the Concrete Constructors *)
    5.57 @@ -70,17 +31,34 @@
    5.58      NIL_I  "NIL: list(A)"
    5.59      CONS_I "[| a: A;  M: list(A) |] ==> CONS a M : list(A)"
    5.60  
    5.61 -rules
    5.62 -  (* Faking a Type Definition ... *)
    5.63 -  Rep_list          "Rep_list(xs): list(range(Leaf))"
    5.64 -  Rep_list_inverse  "Abs_list(Rep_list(xs)) = xs"
    5.65 -  Abs_list_inverse  "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M"
    5.66 +
    5.67 +typedef (List)
    5.68 +  'a list = "list(range Leaf)" (list.NIL_I)
    5.69 +
    5.70 +  
    5.71 +(*Declaring the abstract list constructors*)
    5.72 +consts
    5.73 +  Nil         :: 'a list
    5.74 +  "#"         :: ['a, 'a list] => 'a list                         (infixr 65)
    5.75 +
    5.76 +  (* list Enumeration *)
    5.77 +
    5.78 +  "[]"        :: 'a list                              ("[]")
    5.79 +  "@list"     :: args => 'a list                      ("[(_)]")
    5.80 +
    5.81 +  (* Special syntax for filter *)
    5.82 +  "@filter"   :: [idt, 'a list, bool] => 'a list      ("(1[_:_ ./ _])")
    5.83 +
    5.84 +
    5.85 +translations
    5.86 +  "[x, xs]"     == "x#[xs]"
    5.87 +  "[x]"         == "x#[]"
    5.88 +  "[]"          == "Nil"
    5.89  
    5.90  
    5.91  defs
    5.92 -  (* Defining the Abstract Constructors *)
    5.93 -  Nil_def       "Nil == Abs_list(NIL)"
    5.94 -  Cons_def      "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))"
    5.95 +  Nil_def       "Nil  == Abs_List NIL"
    5.96 +  Cons_def      "x#xs == Abs_List(CONS (Leaf x) (Rep_List xs))"
    5.97  
    5.98    List_case_def "List_case c d == Case (%x. c) (Split d)"
    5.99  
   5.100 @@ -90,30 +68,61 @@
   5.101     "List_rec M c d == wfrec (trancl pred_sexp)
   5.102                              (%g. List_case c (%x y. d x y (g y))) M"
   5.103  
   5.104 -  list_rec_def
   5.105 -   "list_rec l c d == 
   5.106 -   List_rec (Rep_list l) c (%x y r. d (inv Leaf x) (Abs_list y) r)"
   5.107 +
   5.108 +
   5.109 +
   5.110 +constdefs
   5.111 +  (* Generalized Map Functionals *)
   5.112 +  Rep_map     :: ('b => 'a item) => ('b list => 'a item)
   5.113 +    "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)"
   5.114 +  
   5.115 +  Abs_map     :: ('a item => 'b) => 'a item => 'b list
   5.116 +    "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
   5.117 +
   5.118  
   5.119 -  (* Generalized Map Functionals *)
   5.120 +  list_rec    :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
   5.121 +    "list_rec l c d == 
   5.122 +     List_rec (Rep_List l) c (%x y r. d (inv Leaf x) (Abs_List y) r)"
   5.123  
   5.124 -  Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)"
   5.125 -  Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
   5.126 +  null        :: 'a list => bool
   5.127 +    "null(xs)            == list_rec xs True (%x xs r. False)"
   5.128 +
   5.129 +  hd          :: 'a list => 'a
   5.130 +    "hd(xs)              == list_rec xs arbitrary (%x xs r. x)"
   5.131 +
   5.132 +  tl          :: 'a list => 'a list
   5.133 +     "tl(xs)              == list_rec xs arbitrary (%x xs r. xs)"
   5.134  
   5.135 -  null_def      "null(xs)            == list_rec xs True (%x xs r. False)"
   5.136 -  hd_def        "hd(xs)              == list_rec xs arbitrary (%x xs r. x)"
   5.137 -  tl_def        "tl(xs)              == list_rec xs arbitrary (%x xs r. xs)"
   5.138 -  (* a total version of tl: *)
   5.139 -  ttl_def       "ttl(xs)             == list_rec xs [] (%x xs r. xs)"
   5.140 +  (* a total version of tl *)
   5.141 +  ttl         :: 'a list => 'a list
   5.142 +    "ttl(xs)             == list_rec xs [] (%x xs r. xs)"
   5.143 +
   5.144 +  set         :: ('a list => 'a set)
   5.145 +    "set xs              == list_rec xs {} (%x l r. insert x r)"
   5.146  
   5.147 -  set_def       "set xs              == list_rec xs {} (%x l r. insert x r)"
   5.148 +  mem         :: ['a, 'a list] => bool                            (infixl 55)
   5.149 +    "x mem xs == list_rec xs False (%y ys r. if y=x then True else r)"
   5.150 +
   5.151 +  map         :: ('a=>'b) => ('a list => 'b list)
   5.152 +    "map f xs            == list_rec xs [] (%x l r. f(x)#r)"
   5.153 +
   5.154 +  filter      :: ['a => bool, 'a list] => 'a list
   5.155 +    "filter P xs == list_rec xs [] (%x xs r. if P(x) then x#r else r)"
   5.156  
   5.157 -  mem_def       "x mem xs            == 
   5.158 -                   list_rec xs False (%y ys r. if y=x then True else r)"
   5.159 -  map_def       "map f xs            == list_rec xs [] (%x l r. f(x)#r)"
   5.160 -  append_def    "xs@ys               == list_rec xs ys (%x l r. x#r)"
   5.161 -  filter_def    "filter P xs         == 
   5.162 -                  list_rec xs [] (%x xs r. if P(x) then x#r else r)"
   5.163 +  list_case   :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
   5.164 +    "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
   5.165 +
   5.166 +
   5.167 +consts
   5.168 +  "@" :: ['a list, 'a list] => 'a list                    (infixr 65)
   5.169  
   5.170 -  list_case_def  "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
   5.171 +defs
   5.172 +  append_def  "xs@ys == list_rec xs ys (%x l r. x#r)"
   5.173 +
   5.174 +
   5.175 +translations
   5.176 +  "case xs of Nil => a | y#ys => b" == "list_case a (%y ys. b) xs"
   5.177 +
   5.178 +  "[x:xs . P]"  == "filter (%x. P) xs"
   5.179  
   5.180  end