tidied up list definitions, using type 'a option instead of
unit + 'a, also using real typedefs instead of faking them with extra rules
--- a/src/HOL/Induct/LFilter.thy Thu Nov 26 16:37:56 1998 +0100
+++ b/src/HOL/Induct/LFilter.thy Thu Nov 26 17:40:10 1998 +0100
@@ -23,7 +23,7 @@
lfilter :: ['a => bool, 'a llist] => 'a llist
"lfilter p l == llist_corec l (%l. case find p l of
- LNil => Inl ()
- | LCons y z => Inr(y,z))"
+ LNil => None
+ | LCons y z => Some(y,z))"
end
--- a/src/HOL/Induct/LList.ML Thu Nov 26 16:37:56 1998 +0100
+++ b/src/HOL/Induct/LList.ML Thu Nov 26 17:40:10 1998 +0100
@@ -10,7 +10,7 @@
(** Simplification **)
-Addsplits [split_split, split_sum_case];
+Addsplits [option.split];
(*This justifies using llist in other recursive type definitions*)
Goalw llist.defs "A<=B ==> llist(A) <= llist(B)";
@@ -22,7 +22,7 @@
Goal "llist(A) = {Numb(0)} <+> (A <*> llist(A))";
let val rew = rewrite_rule [NIL_def, CONS_def] in
by (fast_tac (claset() addSIs (map rew llist.intrs)
- addEs [rew llist.elim]) 1)
+ addEs [rew llist.elim]) 1)
end;
qed "llist_unfold";
@@ -63,9 +63,8 @@
by (simp_tac (simpset() addsimps [In1_UN1, Scons_UN1_y]) 1);
qed "CONS_UN1";
-val prems = goalw LList.thy [CONS_def]
- "[| M<=M'; N<=N' |] ==> CONS M N <= CONS M' N'";
-by (REPEAT (resolve_tac ([In1_mono,Scons_mono]@prems) 1));
+Goalw [CONS_def] "[| M<=M'; N<=N' |] ==> CONS M N <= CONS M' N'";
+by (REPEAT (ares_tac [In1_mono,Scons_mono] 1));
qed "CONS_mono";
Addsimps [LList_corec_fun_def RS def_nat_rec_0,
@@ -74,8 +73,8 @@
(** The directions of the equality are proved separately **)
Goalw [LList_corec_def]
- "LList_corec a f <= sum_case (%u. NIL) \
-\ (split(%z w. CONS z (LList_corec w f))) (f a)";
+ "LList_corec a f <= \
+\ (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
by (rtac UN_least 1);
by (exhaust_tac "k" 1);
by (ALLGOALS Asm_simp_tac);
@@ -84,7 +83,7 @@
qed "LList_corec_subset1";
Goalw [LList_corec_def]
- "sum_case (%u. NIL) (split(%z w. CONS z (LList_corec w f))) (f a) <= \
+ "(case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f)) <= \
\ LList_corec a f";
by (simp_tac (simpset() addsimps [CONS_UN1]) 1);
by Safe_tac;
@@ -93,16 +92,16 @@
qed "LList_corec_subset2";
(*the recursion equation for LList_corec -- NOT SUITABLE FOR REWRITING!*)
-Goal "LList_corec a f = sum_case (%u. NIL) \
-\ (split(%z w. CONS z (LList_corec w f))) (f a)";
+Goal "LList_corec a f = \
+\ (case f a of None => NIL | Some(z,w) => CONS z (LList_corec w f))";
by (REPEAT (resolve_tac [equalityI, LList_corec_subset1,
LList_corec_subset2] 1));
qed "LList_corec";
(*definitional version of same*)
-val [rew] = goal LList.thy
- "[| !!x. h(x) == LList_corec x f |] ==> \
-\ h(a) = sum_case (%u. NIL) (split(%z w. CONS z (h w))) (f a)";
+val [rew] =
+Goal "[| !!x. h(x) == LList_corec x f |] \
+\ ==> h(a) = (case f a of None => NIL | Some(z,w) => CONS z (h w))";
by (rewtac rew);
by (rtac LList_corec 1);
qed "def_LList_corec";
@@ -117,16 +116,6 @@
by (Simp_tac 1);
qed "LList_corec_type";
-(*Lemma for the proof of llist_corec*)
-Goal "LList_corec a (%z. sum_case Inl (split(%v w. Inr((Leaf(v),w)))) (f z)) : \
-\ llist(range Leaf)";
-by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
-by (rtac rangeI 1);
-by Safe_tac;
-by (stac LList_corec 1);
-by (Asm_simp_tac 1);
-qed "LList_corec_type2";
-
(**** llist equality as a gfp; the bisimulation principle ****)
@@ -140,9 +129,9 @@
Goal "!M N. (M,N) : LListD(diag A) --> ntrunc k M = ntrunc k N";
by (res_inst_tac [("n", "k")] less_induct 1);
-by (safe_tac ((claset_of Fun.thy) delrules [equalityI]));
+by (safe_tac (claset() delrules [equalityI]));
by (etac LListD.elim 1);
-by (safe_tac (claset_of Prod.thy delrules [equalityI] addSEs [diagE]));
+by (safe_tac (claset() delrules [equalityI]));
by (exhaust_tac "n" 1);
by (Asm_simp_tac 1);
by (rename_tac "n'" 1);
@@ -251,9 +240,10 @@
Delsimps [Pair_eq];
(*abstract proof using a bisimulation*)
-val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x); \
-\ !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
+val [prem1,prem2] =
+Goal
+ "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w)); \
+\ !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |]\
\ ==> h1=h2";
by (rtac ext 1);
(*next step avoids an unknown (and flexflex pair) in simplification*)
@@ -267,8 +257,9 @@
CollectI RS LListD_Fun_CONS_I]) 1);
qed "LList_corec_unique";
-val [prem] = goal LList.thy
- "[| !!x. h(x) = sum_case (%u. NIL) (split(%z w. CONS z (h w))) (f x) |] \
+val [prem] =
+Goal
+ "[| !!x. h(x) = (case f x of None => NIL | Some(z,w) => CONS z (h w)) |] \
\ ==> h = (%x. LList_corec x f)";
by (rtac (LList_corec RS (prem RS LList_corec_unique)) 1);
qed "equals_LList_corec";
@@ -288,9 +279,10 @@
Addsimps [ntrunc_one_CONS, ntrunc_CONS];
-val [prem1,prem2] = goal LList.thy
- "[| !!x. h1(x) = sum_case (%u. NIL) (split(%z w. CONS z (h1 w))) (f x); \
-\ !!x. h2(x) = sum_case (%u. NIL) (split(%z w. CONS z (h2 w))) (f x) |]\
+val [prem1,prem2] =
+Goal
+ "[| !!x. h1(x) = (case f x of None => NIL | Some(z,w) => CONS z (h1 w)); \
+\ !!x. h2(x) = (case f x of None => NIL | Some(z,w) => CONS z (h2 w)) |]\
\ ==> h1=h2";
by (rtac (ntrunc_equality RS ext) 1);
by (rename_tac "x k" 1);
@@ -328,14 +320,14 @@
by (REPEAT (ares_tac [list_Fun_CONS_I, singletonI, UnI1] 1));
qed "Lconst_type";
-Goal "Lconst(M) = LList_corec M (%x. Inr((x,x)))";
+Goal "Lconst(M) = LList_corec M (%x. Some((x,x)))";
by (rtac (equals_LList_corec RS fun_cong) 1);
by (Simp_tac 1);
by (rtac Lconst 1);
qed "Lconst_eq_LList_corec";
(*Thus we could have used gfp in the definition of Lconst*)
-Goal "gfp(%N. CONS M N) = LList_corec M (%x. Inr((x,x)))";
+Goal "gfp(%N. CONS M N) = LList_corec M (%x. Some((x,x)))";
by (rtac (equals_LList_corec RS fun_cong) 1);
by (Simp_tac 1);
by (rtac (Lconst_fun_mono RS gfp_Tarski) 1);
@@ -344,21 +336,31 @@
(*** Isomorphisms ***)
-Goal "inj(Rep_llist)";
+Goal "inj Rep_LList";
by (rtac inj_inverseI 1);
-by (rtac Rep_llist_inverse 1);
-qed "inj_Rep_llist";
+by (rtac Rep_LList_inverse 1);
+qed "inj_Rep_LList";
-Goal "inj_on Abs_llist (llist(range Leaf))";
+Goal "inj_on Abs_LList LList";
by (rtac inj_on_inverseI 1);
-by (etac Abs_llist_inverse 1);
-qed "inj_on_Abs_llist";
+by (etac Abs_LList_inverse 1);
+qed "inj_on_Abs_LList";
+
+Goalw [LList_def] "x : llist (range Leaf) ==> x : LList";
+by (Asm_simp_tac 1);
+qed "LListI";
+
+Goalw [LList_def] "x : LList ==> x : llist (range Leaf)";
+by (Asm_simp_tac 1);
+qed "LListD";
+
(** Distinctness of constructors **)
Goalw [LNil_def,LCons_def] "~ LCons x xs = LNil";
-by (rtac (CONS_not_NIL RS (inj_on_Abs_llist RS inj_on_contraD)) 1);
-by (REPEAT (resolve_tac (llist.intrs @ [rangeI, Rep_llist]) 1));
+by (rtac (CONS_not_NIL RS (inj_on_Abs_LList RS inj_on_contraD)) 1);
+by (REPEAT (resolve_tac (llist.intrs @
+ [rangeI, LListI, Rep_LList RS LListD]) 1));
qed "LCons_not_LNil";
bind_thm ("LNil_not_LCons", LCons_not_LNil RS not_sym);
@@ -368,16 +370,14 @@
(** llist constructors **)
-Goalw [LNil_def]
- "Rep_llist(LNil) = NIL";
-by (rtac (llist.NIL_I RS Abs_llist_inverse) 1);
-qed "Rep_llist_LNil";
+Goalw [LNil_def] "Rep_LList LNil = NIL";
+by (rtac (llist.NIL_I RS LListI RS Abs_LList_inverse) 1);
+qed "Rep_LList_LNil";
-Goalw [LCons_def]
- "Rep_llist(LCons x l) = CONS (Leaf x) (Rep_llist l)";
-by (REPEAT (resolve_tac [llist.CONS_I RS Abs_llist_inverse,
- rangeI, Rep_llist] 1));
-qed "Rep_llist_LCons";
+Goalw [LCons_def] "Rep_LList(LCons x l) = CONS (Leaf x) (Rep_LList l)";
+by (REPEAT (resolve_tac [llist.CONS_I RS LListI RS Abs_LList_inverse,
+ rangeI, Rep_LList RS LListD] 1));
+qed "Rep_LList_LCons";
(** Injectiveness of CONS and LCons **)
@@ -385,14 +385,16 @@
by (fast_tac (claset() addSEs [Scons_inject]) 1);
qed "CONS_CONS_eq2";
-bind_thm ("CONS_inject", (CONS_CONS_eq RS iffD1 RS conjE));
+bind_thm ("CONS_inject", CONS_CONS_eq RS iffD1 RS conjE);
(*For reasoning about abstract llist constructors*)
-AddIs ([Rep_llist]@llist.intrs);
-AddSDs [inj_on_Abs_llist RS inj_onD,
- inj_Rep_llist RS injD, Leaf_inject];
+AddIs [Rep_LList RS LListD, LListI];
+AddIs llist.intrs;
+
+AddSDs [inj_on_Abs_LList RS inj_onD,
+ inj_Rep_LList RS injD];
Goalw [LCons_def] "(LCons x xs=LCons y ys) = (x=y & xs=ys)";
by (Fast_tac 1);
@@ -400,8 +402,8 @@
AddIffs [LCons_LCons_eq];
-val [major] = goal LList.thy "CONS M N: llist(A) ==> M: A & N: llist(A)";
-by (rtac (major RS llist.elim) 1);
+Goal "CONS M N: llist(A) ==> M: A & N: llist(A)";
+by (etac llist.elim 1);
by (etac CONS_neq_NIL 1);
by (Fast_tac 1);
qed "CONS_D2";
@@ -412,7 +414,8 @@
Addsimps [List_case_NIL, List_case_CONS];
(*A special case of list_equality for functions over lazy lists*)
-val [Mlist,gMlist,NILcase,CONScase] = goal LList.thy
+val [Mlist,gMlist,NILcase,CONScase] =
+Goal
"[| M: llist(A); g(NIL): llist(A); \
\ f(NIL)=g(NIL); \
\ !!x l. [| x:A; l: llist(A) |] ==> \
@@ -447,8 +450,8 @@
Addsimps [Lmap_NIL, Lmap_CONS];
(*Another type-checking proof by coinduction*)
-val [major,minor] = goal LList.thy
- "[| M: llist(A); !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
+val [major,minor] =
+Goal "[| M: llist(A); !!x. x:A ==> f(x):B |] ==> Lmap f M: llist(B)";
by (rtac (major RS imageI RS llist_coinduct) 1);
by Safe_tac;
by (etac llist.elim 1);
@@ -458,16 +461,16 @@
qed "Lmap_type";
(*This type checking rule synthesises a sufficiently large set for f*)
-val [major] = goal LList.thy "M: llist(A) ==> Lmap f M: llist(f``A)";
-by (rtac (major RS Lmap_type) 1);
+Goal "M: llist(A) ==> Lmap f M: llist(f``A)";
+by (etac Lmap_type 1);
by (etac imageI 1);
qed "Lmap_type2";
(** Two easy results about Lmap **)
-val [prem] = goalw LList.thy [o_def]
- "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
-by (rtac (prem RS imageI RS LList_equalityI) 1);
+Goalw [o_def] "M: llist(A) ==> Lmap (f o g) M = Lmap f (Lmap g M)";
+by (dtac imageI 1);
+by (etac LList_equalityI 1);
by Safe_tac;
by (etac llist.elim 1);
by (ALLGOALS Asm_simp_tac);
@@ -475,8 +478,9 @@
rangeI RS LListD_Fun_CONS_I] 1));
qed "Lmap_compose";
-val [prem] = goal LList.thy "M: llist(A) ==> Lmap (%x. x) M = M";
-by (rtac (prem RS imageI RS LList_equalityI) 1);
+Goal "M: llist(A) ==> Lmap (%x. x) M = M";
+by (dtac imageI 1);
+by (etac LList_equalityI 1);
by Safe_tac;
by (etac llist.elim 1);
by (ALLGOALS Asm_simp_tac);
@@ -549,8 +553,8 @@
(** llist_case: case analysis for 'a llist **)
-Addsimps ([Abs_llist_inverse, Rep_llist_inverse,
- Rep_llist, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
+Addsimps ([LListI RS Abs_LList_inverse, Rep_LList_inverse,
+ Rep_LList RS LListD, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
Goalw [llist_case_def,LNil_def] "llist_case c d LNil = c";
by (Simp_tac 1);
@@ -562,39 +566,47 @@
qed "llist_case_LCons";
(*Elimination is case analysis, not induction.*)
-val [prem1,prem2] = goalw LList.thy [NIL_def,CONS_def]
- "[| l=LNil ==> P; !!x l'. l=LCons x l' ==> P \
-\ |] ==> P";
-by (rtac (Rep_llist RS llist.elim) 1);
-by (rtac (inj_Rep_llist RS injD RS prem1) 1);
-by (stac Rep_llist_LNil 1);
+val [prem1,prem2] =
+Goalw [NIL_def,CONS_def]
+ "[| l=LNil ==> P; !!x l'. l=LCons x l' ==> P |] ==> P";
+by (rtac (Rep_LList RS LListD RS llist.elim) 1);
+by (rtac (inj_Rep_LList RS injD RS prem1) 1);
+by (stac Rep_LList_LNil 1);
by (assume_tac 1);
by (etac rangeE 1);
-by (rtac (inj_Rep_llist RS injD RS prem2) 1);
+by (rtac (inj_Rep_LList RS injD RS prem2) 1);
by (asm_simp_tac (simpset() delsimps [CONS_CONS_eq]
- addsimps [Rep_llist_LCons]) 1);
-by (etac (Abs_llist_inverse RS ssubst) 1);
+ addsimps [Rep_LList_LCons]) 1);
+by (etac (LListI RS Abs_LList_inverse RS ssubst) 1);
by (rtac refl 1);
qed "llistE";
(** llist_corec: corecursion for 'a llist **)
-Goalw [llist_corec_def,LNil_def,LCons_def]
- "llist_corec a f = sum_case (%u. LNil) \
-\ (split(%z w. LCons z (llist_corec w f))) (f a)";
+(*Lemma for the proof of llist_corec*)
+Goal "LList_corec a \
+\ (%z. case f z of None => None | Some(v,w) => Some(Leaf(v),w)) : \
+\ llist(range Leaf)";
+by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
+by (rtac rangeI 1);
+by Safe_tac;
by (stac LList_corec 1);
-by (res_inst_tac [("s","f(a)")] sumE 1);
+by (Force_tac 1);
+qed "LList_corec_type2";
+
+Goalw [llist_corec_def,LNil_def,LCons_def]
+ "llist_corec a f = \
+\ (case f a of None => LNil | Some(z,w) => LCons z (llist_corec w f))";
+by (stac LList_corec 1);
+by (exhaust_tac "f a" 1);
by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
-by (res_inst_tac [("p","y")] PairE 1);
-by (asm_simp_tac (simpset() addsimps [LList_corec_type2]) 1);
-(*FIXME: correct case splits usd to be found automatically:
-by (ASM_SIMP_TAC(simpset() addsimps [LList_corec_type2]) 1);*)
+by (force_tac (claset(), simpset() addsimps [LList_corec_type2]) 1);
qed "llist_corec";
(*definitional version of same*)
-val [rew] = goal LList.thy
- "[| !!x. h(x) == llist_corec x f |] ==> \
-\ h(a) = sum_case (%u. LNil) (split(%z w. LCons z (h w))) (f a)";
+val [rew] =
+Goal "[| !!x. h(x) == llist_corec x f |] ==> \
+\ h(a) = (case f a of None => LNil | Some(z,w) => LCons z (h w))";
by (rewtac rew);
by (rtac llist_corec 1);
qed "def_llist_corec";
@@ -611,48 +623,47 @@
by (Fast_tac 1);
qed "LListD_Fun_subset_Sigma_llist";
-Goal "prod_fun Rep_llist Rep_llist `` r <= \
+Goal "prod_fun Rep_LList Rep_LList `` r <= \
\ (llist(range Leaf)) Times (llist(range Leaf))";
by (fast_tac (claset() delrules [image_subsetI]
- addIs [Rep_llist]) 1);
+ addIs [Rep_LList RS LListD]) 1);
qed "subset_Sigma_llist";
-val [prem] = goal LList.thy
- "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
-\ prod_fun (Rep_llist o Abs_llist) (Rep_llist o Abs_llist) `` r <= r";
+Goal "r <= (llist(range Leaf)) Times (llist(range Leaf)) ==> \
+\ prod_fun (Rep_LList o Abs_LList) (Rep_LList o Abs_LList) `` r <= r";
by Safe_tac;
-by (rtac (prem RS subsetD RS SigmaE2) 1);
+by (etac (subsetD RS SigmaE2) 1);
by (assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [Abs_llist_inverse]) 1);
+by (asm_simp_tac (simpset() addsimps [LListI RS Abs_LList_inverse]) 1);
qed "prod_fun_lemma";
-Goal "prod_fun Rep_llist Rep_llist `` range(%x. (x, x)) = \
+Goal "prod_fun Rep_LList Rep_LList `` range(%x. (x, x)) = \
\ diag(llist(range Leaf))";
by (rtac equalityI 1);
-by (fast_tac (claset() addIs [Rep_llist]) 1);
+by (Blast_tac 1);
by (fast_tac (claset() delSWrapper "split_all_tac"
- addSEs [Abs_llist_inverse RS subst]) 1);
+ addSEs [LListI RS Abs_LList_inverse RS subst]) 1);
qed "prod_fun_range_eq_diag";
-(*Surprisingly hard to prove. Used with lfilter*)
+(*Used with lfilter*)
Goalw [llistD_Fun_def, prod_fun_def]
"A<=B ==> llistD_Fun A <= llistD_Fun B";
by Auto_tac;
by (rtac image_eqI 1);
-by (fast_tac (claset() addss (simpset())) 1);
-by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 1);
+by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 2);
+by (Force_tac 1);
qed "llistD_Fun_mono";
(** To show two llists are equal, exhibit a bisimulation!
[also admits true equality] **)
-val [prem1,prem2] = goalw LList.thy [llistD_Fun_def]
+Goalw [llistD_Fun_def]
"[| (l1,l2) : r; r <= llistD_Fun(r Un range(%x.(x,x))) |] ==> l1=l2";
-by (rtac (inj_Rep_llist RS injD) 1);
-by (res_inst_tac [("r", "prod_fun Rep_llist Rep_llist ``r"),
+by (rtac (inj_Rep_LList RS injD) 1);
+by (res_inst_tac [("r", "prod_fun Rep_LList Rep_LList ``r"),
("A", "range(Leaf)")]
LList_equalityI 1);
-by (rtac (prem1 RS prod_fun_imageI) 1);
-by (rtac (prem2 RS image_mono RS subset_trans) 1);
+by (etac prod_fun_imageI 1);
+by (etac (image_mono RS subset_trans) 1);
by (rtac (image_compose RS subst) 1);
by (rtac (prod_fun_compose RS subst) 1);
by (stac image_Un 1);
@@ -667,28 +678,27 @@
by (rtac (LListD_Fun_NIL_I RS prod_fun_imageI) 1);
qed "llistD_Fun_LNil_I";
-val [prem] = goalw LList.thy [llistD_Fun_def,LCons_def]
+Goalw [llistD_Fun_def,LCons_def]
"(l1,l2):r ==> (LCons x l1, LCons x l2) : llistD_Fun(r)";
by (rtac (rangeI RS LListD_Fun_CONS_I RS prod_fun_imageI) 1);
-by (rtac (prem RS prod_fun_imageI) 1);
+by (etac prod_fun_imageI 1);
qed "llistD_Fun_LCons_I";
(*Utilise the "strong" part, i.e. gfp(f)*)
-Goalw [llistD_Fun_def]
- "(l,l) : llistD_Fun(r Un range(%x.(x,x)))";
-by (rtac (Rep_llist_inverse RS subst) 1);
+Goalw [llistD_Fun_def] "(l,l) : llistD_Fun(r Un range(%x.(x,x)))";
+by (rtac (Rep_LList_inverse RS subst) 1);
by (rtac prod_fun_imageI 1);
by (stac image_Un 1);
by (stac prod_fun_range_eq_diag 1);
-by (rtac (Rep_llist RS LListD_Fun_diag_I) 1);
+by (rtac (Rep_LList RS LListD RS LListD_Fun_diag_I) 1);
qed "llistD_Fun_range_I";
(*A special case of list_equality for functions over lazy lists*)
-val [prem1,prem2] = goal LList.thy
- "[| f(LNil)=g(LNil); \
-\ !!x l. (f(LCons x l),g(LCons x l)) : \
-\ llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v))) \
-\ |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)";
+val [prem1,prem2] =
+Goal "[| f(LNil)=g(LNil); \
+\ !!x l. (f(LCons x l),g(LCons x l)) : \
+\ llistD_Fun(range(%u. (f(u),g(u))) Un range(%v. (v,v))) \
+\ |] ==> f(l) = (g(l :: 'a llist) :: 'b llist)";
by (res_inst_tac [("r", "range(%u. (f(u),g(u)))")] llist_equalityI 1);
by (rtac rangeI 1);
by (rtac subsetI 1);
@@ -777,8 +787,7 @@
(*The bisimulation consists of {(lmap(f)^n (h(u)), lmap(f)^n (iterates(f,u)))}
for all u and all n::nat.*)
-val [prem] = goal LList.thy
- "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
+val [prem] = Goal "(!!x. h(x) = LCons x (lmap f (h x))) ==> h = iterates(f)";
by (rtac ext 1);
by (res_inst_tac [("r",
"UN u. range(%n. (nat_rec (h u) (%m y. lmap f y) n, \
--- a/src/HOL/Induct/LList.thy Thu Nov 26 16:37:56 1998 +0100
+++ b/src/HOL/Induct/LList.thy Thu Nov 26 17:40:10 1998 +0100
@@ -23,43 +23,12 @@
(UN x. (split(%l1 l2.(LCons(x,l1),LCons(x,l2))))``r)"
*)
-LList = Gfp + SList +
-
-types
- 'a llist
-
-arities
- llist :: (term)term
+LList = Main + SList +
consts
- list_Fun :: ['a item set, 'a item set] => 'a item set
- LListD_Fun ::
- "[('a item * 'a item)set, ('a item * 'a item)set] =>
- ('a item * 'a item)set"
llist :: 'a item set => 'a item set
LListD :: "('a item * 'a item)set => ('a item * 'a item)set"
- llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
-
- Rep_llist :: 'a llist => 'a item
- Abs_llist :: 'a item => 'a llist
- LNil :: 'a llist
- LCons :: ['a, 'a llist] => 'a llist
-
- llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
-
- LList_corec_fun :: "[nat, 'a=>unit+('b item * 'a), 'a] => 'b item"
- LList_corec :: "['a, 'a => unit + ('b item * 'a)] => 'b item"
- llist_corec :: "['a, 'a => unit + ('b * 'a)] => 'b llist"
-
- Lmap :: ('a item => 'b item) => ('a item => 'b item)
- lmap :: ('a=>'b) => ('a llist => 'b llist)
-
- iterates :: ['a => 'a, 'a] => 'a llist
-
- Lconst :: 'a item => 'a item
- Lappend :: ['a item, 'a item] => 'a item
- lappend :: ['a llist, 'a llist] => 'a llist
coinductive "llist(A)"
@@ -73,81 +42,92 @@
CONS_I "[| (a,b): r; (M,N) : LListD(r)
|] ==> (CONS a M, CONS b N) : LListD(r)"
+
+typedef (LList)
+ 'a llist = "llist(range Leaf)" (llist.NIL_I)
+
+constdefs
+ (*Now used exclusively for abbreviating the coinduction rule*)
+ list_Fun :: ['a item set, 'a item set] => 'a item set
+ "list_Fun A X == {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
+
+ LListD_Fun ::
+ "[('a item * 'a item)set, ('a item * 'a item)set] =>
+ ('a item * 'a item)set"
+ "LListD_Fun r X ==
+ {z. z = (NIL, NIL) |
+ (? M N a b. z = (CONS a M, CONS b N) & (a, b) : r & (M, N) : X)}"
+
+ (*the abstract constructors*)
+ LNil :: 'a llist
+ "LNil == Abs_LList NIL"
+
+ LCons :: ['a, 'a llist] => 'a llist
+ "LCons x xs == Abs_LList(CONS (Leaf x) (Rep_LList xs))"
+
+ llist_case :: ['b, ['a, 'a llist]=>'b, 'a llist] => 'b
+ "llist_case c d l ==
+ List_case c (%x y. d (inv Leaf x) (Abs_LList y)) (Rep_LList l)"
+
+ LList_corec_fun :: "[nat, 'a=> ('b item * 'a) option, 'a] => 'b item"
+ "LList_corec_fun k f ==
+ nat_rec (%x. {})
+ (%j r x. case f x of None => NIL
+ | Some(z,w) => CONS z (r w))
+ k"
+
+ LList_corec :: "['a, 'a => ('b item * 'a) option] => 'b item"
+ "LList_corec a f == UN k. LList_corec_fun k f a"
+
+ llist_corec :: "['a, 'a => ('b * 'a) option] => 'b llist"
+ "llist_corec a f ==
+ Abs_LList(LList_corec a
+ (%z. case f z of None => None
+ | Some(v,w) => Some(Leaf(v), w)))"
+
+ llistD_Fun :: "('a llist * 'a llist)set => ('a llist * 'a llist)set"
+ "llistD_Fun(r) ==
+ prod_fun Abs_LList Abs_LList ``
+ LListD_Fun (diag(range Leaf))
+ (prod_fun Rep_LList Rep_LList `` r)"
+
+
+
+(*The case syntax for type 'a llist*)
translations
"case p of LNil => a | LCons x l => b" == "llist_case a (%x l. b) p"
-defs
- (*Now used exclusively for abbreviating the coinduction rule*)
- list_Fun_def "list_Fun A X ==
- {z. z = NIL | (? M a. z = CONS a M & a : A & M : X)}"
-
- LListD_Fun_def "LListD_Fun r X ==
- {z. z = (NIL, NIL) |
- (? M N a b. z = (CONS a M, CONS b N) &
- (a, b) : r & (M, N) : X)}"
+(** Sample function definitions. Item-based ones start with L ***)
- (*defining the abstract constructors*)
- LNil_def "LNil == Abs_llist(NIL)"
- LCons_def "LCons x xs == Abs_llist(CONS (Leaf x) (Rep_llist xs))"
-
- llist_case_def
- "llist_case c d l ==
- List_case c (%x y. d (inv Leaf x) (Abs_llist y)) (Rep_llist l)"
-
- LList_corec_fun_def
- "LList_corec_fun k f ==
- nat_rec (%x. {})
- (%j r x. case f x of Inl u => NIL
- | Inr(z,w) => CONS z (r w))
- k"
+constdefs
+ Lmap :: ('a item => 'b item) => ('a item => 'b item)
+ "Lmap f M == LList_corec M (List_case None (%x M'. Some((f(x), M'))))"
- LList_corec_def
- "LList_corec a f == UN k. LList_corec_fun k f a"
-
- llist_corec_def
- "llist_corec a f ==
- Abs_llist(LList_corec a
- (%z. case f z of Inl x => Inl(x)
- | Inr(v,w) => Inr(Leaf(v), w)))"
+ lmap :: ('a=>'b) => ('a llist => 'b llist)
+ "lmap f l == llist_corec l (%z. case z of LNil => None
+ | LCons y z => Some(f(y), z))"
- llistD_Fun_def
- "llistD_Fun(r) ==
- prod_fun Abs_llist Abs_llist ``
- LListD_Fun (diag(range Leaf))
- (prod_fun Rep_llist Rep_llist `` r)"
-
- Lconst_def "Lconst(M) == lfp(%N. CONS M N)"
+ iterates :: ['a => 'a, 'a] => 'a llist
+ "iterates f a == llist_corec a (%x. Some((x, f(x))))"
- Lmap_def
- "Lmap f M == LList_corec M (List_case (Inl ()) (%x M'. Inr((f(x), M'))))"
-
- lmap_def
- "lmap f l == llist_corec l (%z. case z of LNil => (Inl ())
- | LCons y z => Inr(f(y), z))"
-
- iterates_def "iterates f a == llist_corec a (%x. Inr((x, f(x))))"
+ Lconst :: 'a item => 'a item
+ "Lconst(M) == lfp(%N. CONS M N)"
(*Append generates its result by applying f, where
- f((NIL,NIL)) = Inl(())
- f((NIL, CONS N1 N2)) = Inr((N1, (NIL,N2))
- f((CONS M1 M2, N)) = Inr((M1, (M2,N))
+ f((NIL,NIL)) = None
+ f((NIL, CONS N1 N2)) = Some((N1, (NIL,N2))
+ f((CONS M1 M2, N)) = Some((M1, (M2,N))
*)
- Lappend_def
+ Lappend :: ['a item, 'a item] => 'a item
"Lappend M N == LList_corec (M,N)
- (split(List_case (List_case (Inl ()) (%N1 N2. Inr((N1, (NIL,N2)))))
- (%M1 M2 N. Inr((M1, (M2,N))))))"
+ (split(List_case (List_case None (%N1 N2. Some((N1, (NIL,N2)))))
+ (%M1 M2 N. Some((M1, (M2,N))))))"
- lappend_def
- "lappend l n == llist_corec (l,n)
- (split(llist_case (llist_case (Inl ()) (%n1 n2. Inr((n1, (LNil,n2)))))
- (%l1 l2 n. Inr((l1, (l2,n))))))"
-
-rules
- (*faking a type definition...*)
- Rep_llist "Rep_llist(xs): llist(range(Leaf))"
- Rep_llist_inverse "Abs_llist(Rep_llist(xs)) = xs"
- Abs_llist_inverse "M: llist(range(Leaf)) ==> Rep_llist(Abs_llist(M)) = M"
+ lappend :: ['a llist, 'a llist] => 'a llist
+ "lappend l n == llist_corec (l,n)
+ (split(llist_case (llist_case None (%n1 n2. Some((n1, (LNil,n2)))))
+ (%l1 l2 n. Some((l1, (l2,n))))))"
end
--- a/src/HOL/Induct/SList.ML Thu Nov 26 16:37:56 1998 +0100
+++ b/src/HOL/Induct/SList.ML Thu Nov 26 17:40:10 1998 +0100
@@ -6,6 +6,15 @@
Definition of type 'a list by a least fixed point
*)
+
+Goalw [List_def] "x : list (range Leaf) ==> x : List";
+by (Asm_simp_tac 1);
+qed "ListI";
+
+Goalw [List_def] "x : List ==> x : list (range Leaf)";
+by (Asm_simp_tac 1);
+qed "ListD";
+
val list_con_defs = [NIL_def, CONS_def];
Goal "list(A) = {Numb(0)} <+> (A <*> list(A))";
@@ -28,16 +37,17 @@
qed "list_sexp";
(* A <= sexp ==> list(A) <= sexp *)
-bind_thm ("list_subset_sexp", ([list_mono, list_sexp] MRS subset_trans));
+bind_thm ("list_subset_sexp", [list_mono, list_sexp] MRS subset_trans);
(*Induction for the type 'a list *)
-val prems = goalw SList.thy [Nil_def,Cons_def]
+val prems = Goalw [Nil_def,Cons_def]
"[| P(Nil); \
\ !!x xs. P(xs) ==> P(x # xs) |] ==> P(l)";
-by (rtac (Rep_list_inverse RS subst) 1); (*types force good instantiation*)
-by (rtac (Rep_list RS list.induct) 1);
+by (rtac (Rep_List_inverse RS subst) 1); (*types force good instantiation*)
+by (rtac (Rep_List RS ListD RS list.induct) 1);
by (REPEAT (ares_tac prems 1
- ORELSE eresolve_tac [rangeE, ssubst, Abs_list_inverse RS subst] 1));
+ ORELSE eresolve_tac [rangeE, ssubst,
+ ListI RS Abs_List_inverse RS subst] 1));
qed "list_induct2";
(*Perform induction on xs. *)
@@ -47,15 +57,15 @@
(*** Isomorphisms ***)
-Goal "inj(Rep_list)";
+Goal "inj Rep_List";
by (rtac inj_inverseI 1);
-by (rtac Rep_list_inverse 1);
-qed "inj_Rep_list";
+by (rtac Rep_List_inverse 1);
+qed "inj_Rep_List";
-Goal "inj_on Abs_list (list(range Leaf))";
+Goal "inj_on Abs_List List";
by (rtac inj_on_inverseI 1);
-by (etac Abs_list_inverse 1);
-qed "inj_on_Abs_list";
+by (etac Abs_List_inverse 1);
+qed "inj_on_Abs_List";
(** Distinctness of constructors **)
@@ -68,8 +78,8 @@
val NIL_neq_CONS = sym RS CONS_neq_NIL;
Goalw [Nil_def,Cons_def] "x # xs ~= Nil";
-by (rtac (CONS_not_NIL RS (inj_on_Abs_list RS inj_on_contraD)) 1);
-by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_list]) 1));
+by (rtac (CONS_not_NIL RS (inj_on_Abs_List RS inj_on_contraD)) 1);
+by (REPEAT (resolve_tac (list.intrs @ [rangeI, Rep_List RS ListD, ListI]) 1));
qed "Cons_not_Nil";
bind_thm ("Nil_not_Cons", Cons_not_Nil RS not_sym);
@@ -81,27 +91,26 @@
qed "CONS_CONS_eq";
(*For reasoning about abstract list constructors*)
-AddIs ([Rep_list] @ list.intrs);
+AddIs [Rep_List RS ListD, ListI];
+AddIs list.intrs;
AddIffs [CONS_not_NIL, NIL_not_CONS, CONS_CONS_eq];
-AddSDs [inj_on_Abs_list RS inj_onD,
- inj_Rep_list RS injD, Leaf_inject];
+AddSDs [inj_on_Abs_List RS inj_onD,
+ inj_Rep_List RS injD, Leaf_inject];
Goalw [Cons_def] "(x#xs=y#ys) = (x=y & xs=ys)";
by (Fast_tac 1);
qed "Cons_Cons_eq";
-bind_thm ("Cons_inject2", (Cons_Cons_eq RS iffD1 RS conjE));
+bind_thm ("Cons_inject2", Cons_Cons_eq RS iffD1 RS conjE);
-val [major] = goal SList.thy "CONS M N: list(A) ==> M: A & N: list(A)";
-by (rtac (major RS setup_induction) 1);
+Goal "CONS M N: list(A) ==> M: A & N: list(A)";
+by (etac setup_induction 1);
by (etac list.induct 1);
-by (ALLGOALS (Fast_tac));
+by (ALLGOALS Fast_tac);
qed "CONS_D";
-val prems = goalw SList.thy [CONS_def,In1_def]
- "CONS M N: sexp ==> M: sexp & N: sexp";
-by (cut_facts_tac prems 1);
+Goalw [CONS_def,In1_def] "CONS M N: sexp ==> M: sexp & N: sexp";
by (fast_tac (claset() addSDs [Scons_D]) 1);
qed "sexp_CONS_D";
@@ -199,13 +208,14 @@
(*** list_rec -- by List_rec ***)
-val Rep_list_in_sexp =
- [range_Leaf_subset_sexp RS list_subset_sexp, Rep_list] MRS subsetD;
+val Rep_List_in_sexp =
+ [range_Leaf_subset_sexp RS list_subset_sexp, Rep_List RS ListD]
+ MRS subsetD;
local
- val list_rec_simps = [Abs_list_inverse, Rep_list_inverse,
- Rep_list, rangeI, inj_Leaf, inv_f_f,
- sexp.LeafI, Rep_list_in_sexp]
+ val list_rec_simps = [ListI RS Abs_List_inverse, Rep_List_inverse,
+ Rep_List RS ListD, rangeI, inj_Leaf, inv_f_f,
+ sexp.LeafI, Rep_List_in_sexp]
in
val list_rec_Nil = prove_goalw SList.thy [list_rec_def, Nil_def]
"list_rec Nil c h = c"
@@ -220,12 +230,12 @@
(*Type checking. Useful?*)
-val major::A_subset_sexp::prems = goal SList.thy
- "[| M: list(A); \
-\ A<=sexp; \
-\ c: C(NIL); \
-\ !!x y r. [| x: A; y: list(A); r: C(y) |] ==> h x y r: C(CONS x y) \
-\ |] ==> List_rec M c h : C(M :: 'a item)";
+val major::A_subset_sexp::prems =
+Goal "[| M: list(A); \
+\ A<=sexp; \
+\ c: C(NIL); \
+\ !!x y r. [| x: A; y: list(A); r: C(y) |] ==> h x y r: C(CONS x y) \
+\ |] ==> List_rec M c h : C(M :: 'a item)";
val sexp_ListA_I = A_subset_sexp RS list_subset_sexp RS subsetD;
val sexp_A_I = A_subset_sexp RS subsetD;
by (rtac (major RS list.induct) 1);
@@ -238,8 +248,7 @@
by (rtac list_rec_Nil 1);
qed "Rep_map_Nil";
-Goalw [Rep_map_def]
- "Rep_map f (x#xs) = CONS (f x) (Rep_map f xs)";
+Goalw [Rep_map_def] "Rep_map f (x#xs) = CONS (f x) (Rep_map f xs)";
by (rtac list_rec_Cons 1);
qed "Rep_map_Cons";
@@ -252,21 +261,20 @@
by (rtac List_rec_NIL 1);
qed "Abs_map_NIL";
-val prems = goalw SList.thy [Abs_map_def]
- "[| M: sexp; N: sexp |] ==> \
-\ Abs_map g (CONS M N) = g(M) # Abs_map g N";
-by (REPEAT (resolve_tac (List_rec_CONS::prems) 1));
+Goalw [Abs_map_def]
+ "[| M: sexp; N: sexp |] ==> Abs_map g (CONS M N) = g(M) # Abs_map g N";
+by (REPEAT (ares_tac [List_rec_CONS] 1));
qed "Abs_map_CONS";
(*These 2 rules ease the use of primitive recursion. NOTE USE OF == *)
-val [rew] = goal SList.thy
- "[| !!xs. f(xs) == list_rec xs c h |] ==> f([]) = c";
+val [rew] =
+Goal "[| !!xs. f(xs) == list_rec xs c h |] ==> f([]) = c";
by (rewtac rew);
by (rtac list_rec_Nil 1);
qed "def_list_rec_Nil";
-val [rew] = goal SList.thy
- "[| !!xs. f(xs) == list_rec xs c h |] ==> f(x#xs) = h x xs (f xs)";
+val [rew] =
+Goal "[| !!xs. f(xs) == list_rec xs c h |] ==> f(x#xs) = h x xs (f xs)";
by (rewtac rew);
by (rtac list_rec_Cons 1);
qed "def_list_rec_Cons";
@@ -327,11 +335,12 @@
Addsimps [Rep_map_Nil, Rep_map_Cons, Abs_map_NIL, Abs_map_CONS];
-val [major,A_subset_sexp,minor] = goal SList.thy
- "[| M: list(A); A<=sexp; !!z. z: A ==> f(g(z)) = z |] \
-\ ==> Rep_map f (Abs_map g M) = M";
+val [major,A_subset_sexp,minor] =
+Goal "[| M: list(A); A<=sexp; !!z. z: A ==> f(g(z)) = z |] \
+\ ==> Rep_map f (Abs_map g M) = M";
by (rtac (major RS list.induct) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [sexp_A_I,sexp_ListA_I,minor])));
+by (ALLGOALS
+ (asm_simp_tac (simpset() addsimps [sexp_A_I,sexp_ListA_I,minor])));
qed "Abs_map_inverse";
(*Rep_map_inverse is obtained via Abs_Rep_map and map_ident*)
@@ -339,7 +348,7 @@
(** list_case **)
Goal "P(list_case a f xs) = ((xs=[] --> P(a)) & \
-\ (!y ys. xs=y#ys --> P(f y ys)))";
+\ (!y ys. xs=y#ys --> P(f y ys)))";
by (list_ind_tac "xs" 1);
by (ALLGOALS Asm_simp_tac);
qed "split_list_case2";
--- a/src/HOL/Induct/SList.thy Thu Nov 26 16:37:56 1998 +0100
+++ b/src/HOL/Induct/SList.thy Thu Nov 26 17:40:10 1998 +0100
@@ -12,53 +12,14 @@
SList = Sexp +
-types
- 'a list
-
-arities
- list :: (term) term
-
-
consts
list :: 'a item set => 'a item set
- Rep_list :: 'a list => 'a item
- Abs_list :: 'a item => 'a list
NIL :: 'a item
CONS :: ['a item, 'a item] => 'a item
- Nil :: 'a list
- "#" :: ['a, 'a list] => 'a list (infixr 65)
List_case :: ['b, ['a item, 'a item]=>'b, 'a item] => 'b
List_rec :: ['a item, 'b, ['a item, 'a item, 'b]=>'b] => 'b
- list_case :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
- list_rec :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
- Rep_map :: ('b => 'a item) => ('b list => 'a item)
- Abs_map :: ('a item => 'b) => 'a item => 'b list
- null :: 'a list => bool
- hd :: 'a list => 'a
- tl,ttl :: 'a list => 'a list
- set :: ('a list => 'a set)
- mem :: ['a, 'a list] => bool (infixl 55)
- map :: ('a=>'b) => ('a list => 'b list)
- "@" :: ['a list, 'a list] => 'a list (infixr 65)
- filter :: ['a => bool, 'a list] => 'a list
- (* list Enumeration *)
-
- "[]" :: 'a list ("[]")
- "@list" :: args => 'a list ("[(_)]")
-
- (* Special syntax for filter *)
- "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
-
-translations
- "[x, xs]" == "x#[xs]"
- "[x]" == "x#[]"
- "[]" == "Nil"
-
- "case xs of Nil => a | y#ys => b" == "list_case a (%y ys. b) xs"
-
- "[x:xs . P]" == "filter (%x. P) xs"
defs
(* Defining the Concrete Constructors *)
@@ -70,17 +31,34 @@
NIL_I "NIL: list(A)"
CONS_I "[| a: A; M: list(A) |] ==> CONS a M : list(A)"
-rules
- (* Faking a Type Definition ... *)
- Rep_list "Rep_list(xs): list(range(Leaf))"
- Rep_list_inverse "Abs_list(Rep_list(xs)) = xs"
- Abs_list_inverse "M: list(range(Leaf)) ==> Rep_list(Abs_list(M)) = M"
+
+typedef (List)
+ 'a list = "list(range Leaf)" (list.NIL_I)
+
+
+(*Declaring the abstract list constructors*)
+consts
+ Nil :: 'a list
+ "#" :: ['a, 'a list] => 'a list (infixr 65)
+
+ (* list Enumeration *)
+
+ "[]" :: 'a list ("[]")
+ "@list" :: args => 'a list ("[(_)]")
+
+ (* Special syntax for filter *)
+ "@filter" :: [idt, 'a list, bool] => 'a list ("(1[_:_ ./ _])")
+
+
+translations
+ "[x, xs]" == "x#[xs]"
+ "[x]" == "x#[]"
+ "[]" == "Nil"
defs
- (* Defining the Abstract Constructors *)
- Nil_def "Nil == Abs_list(NIL)"
- Cons_def "x#xs == Abs_list(CONS (Leaf x) (Rep_list xs))"
+ Nil_def "Nil == Abs_List NIL"
+ Cons_def "x#xs == Abs_List(CONS (Leaf x) (Rep_List xs))"
List_case_def "List_case c d == Case (%x. c) (Split d)"
@@ -90,30 +68,61 @@
"List_rec M c d == wfrec (trancl pred_sexp)
(%g. List_case c (%x y. d x y (g y))) M"
- list_rec_def
- "list_rec l c d ==
- List_rec (Rep_list l) c (%x y r. d (inv Leaf x) (Abs_list y) r)"
+
+
+
+constdefs
+ (* Generalized Map Functionals *)
+ Rep_map :: ('b => 'a item) => ('b list => 'a item)
+ "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)"
+
+ Abs_map :: ('a item => 'b) => 'a item => 'b list
+ "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
+
- (* Generalized Map Functionals *)
+ list_rec :: ['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b
+ "list_rec l c d ==
+ List_rec (Rep_List l) c (%x y r. d (inv Leaf x) (Abs_List y) r)"
- Rep_map_def "Rep_map f xs == list_rec xs NIL (%x l r. CONS (f x) r)"
- Abs_map_def "Abs_map g M == List_rec M Nil (%N L r. g(N)#r)"
+ null :: 'a list => bool
+ "null(xs) == list_rec xs True (%x xs r. False)"
+
+ hd :: 'a list => 'a
+ "hd(xs) == list_rec xs arbitrary (%x xs r. x)"
+
+ tl :: 'a list => 'a list
+ "tl(xs) == list_rec xs arbitrary (%x xs r. xs)"
- null_def "null(xs) == list_rec xs True (%x xs r. False)"
- hd_def "hd(xs) == list_rec xs arbitrary (%x xs r. x)"
- tl_def "tl(xs) == list_rec xs arbitrary (%x xs r. xs)"
- (* a total version of tl: *)
- ttl_def "ttl(xs) == list_rec xs [] (%x xs r. xs)"
+ (* a total version of tl *)
+ ttl :: 'a list => 'a list
+ "ttl(xs) == list_rec xs [] (%x xs r. xs)"
+
+ set :: ('a list => 'a set)
+ "set xs == list_rec xs {} (%x l r. insert x r)"
- set_def "set xs == list_rec xs {} (%x l r. insert x r)"
+ mem :: ['a, 'a list] => bool (infixl 55)
+ "x mem xs == list_rec xs False (%y ys r. if y=x then True else r)"
+
+ map :: ('a=>'b) => ('a list => 'b list)
+ "map f xs == list_rec xs [] (%x l r. f(x)#r)"
+
+ filter :: ['a => bool, 'a list] => 'a list
+ "filter P xs == list_rec xs [] (%x xs r. if P(x) then x#r else r)"
- mem_def "x mem xs ==
- list_rec xs False (%y ys r. if y=x then True else r)"
- map_def "map f xs == list_rec xs [] (%x l r. f(x)#r)"
- append_def "xs@ys == list_rec xs ys (%x l r. x#r)"
- filter_def "filter P xs ==
- list_rec xs [] (%x xs r. if P(x) then x#r else r)"
+ list_case :: ['b, ['a, 'a list]=>'b, 'a list] => 'b
+ "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
+
+
+consts
+ "@" :: ['a list, 'a list] => 'a list (infixr 65)
- list_case_def "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
+defs
+ append_def "xs@ys == list_rec xs ys (%x l r. x#r)"
+
+
+translations
+ "case xs of Nil => a | y#ys => b" == "list_case a (%y ys. b) xs"
+
+ "[x:xs . P]" == "filter (%x. P) xs"
end