--- a/src/ZF/ex/Acc.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Acc.ML Fri Aug 12 12:28:46 1994 +0200
@@ -9,21 +9,19 @@
Research Report 92-49, LIP, ENS Lyon. Dec 1992.
*)
-structure Acc = Inductive_Fun
- (val thy = WF.thy |> add_consts [("acc","i=>i",NoSyn)]
- val thy_name = "Acc"
- val rec_doms = [("acc", "field(r)")]
- val sintrs = ["[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"]
- val monos = [Pow_mono]
- val con_defs = []
- val type_intrs = []
- val type_elims = []);
+open Acc;
(*The introduction rule must require a:field(r)
Otherwise acc(r) would be a proper class! *)
+(*The intended introduction rule*)
+val prems = goal Acc.thy
+ "[| !!b. <b,a>:r ==> b: acc(r); a: field(r) |] ==> a: acc(r)";
+by (fast_tac (ZF_cs addIs (prems@acc.intrs)) 1);
+val accI = result();
+
goal Acc.thy "!!a b r. [| b: acc(r); <a,b>: r |] ==> a: acc(r)";
-by (etac Acc.elim 1);
+by (etac acc.elim 1);
by (fast_tac ZF_cs 1);
val acc_downward = result();
@@ -31,12 +29,12 @@
"[| a : acc(r); \
\ !!x. [| x: acc(r); ALL y. <y,x>:r --> P(y) |] ==> P(x) \
\ |] ==> P(a)";
-by (rtac (major RS Acc.induct) 1);
+by (rtac (major RS acc.induct) 1);
by (rtac indhyp 1);
by (fast_tac ZF_cs 2);
-by (resolve_tac Acc.intrs 1);
+by (resolve_tac acc.intrs 1);
by (assume_tac 2);
-by (fast_tac ZF_cs 1);
+be (Collect_subset RS Pow_mono RS subsetD) 1;
val acc_induct = result();
goal Acc.thy "wf[acc(r)](r)";
@@ -52,7 +50,7 @@
by (rtac subsetI 1);
by (etac (major RS wf_induct2) 1);
by (rtac subset_refl 1);
-by (resolve_tac Acc.intrs 1);
+by (resolve_tac [accI] 1);
by (assume_tac 2);
by (fast_tac ZF_cs 1);
val acc_wfD = result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Acc.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,23 @@
+(* Title: ZF/ex/Acc.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Inductive definition of acc(r)
+
+See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
+Research Report 92-49, LIP, ENS Lyon. Dec 1992.
+*)
+
+Acc = WF + "inductive" +
+
+consts
+ "acc" :: "i=>i"
+
+inductive
+ domains "acc(r)" <= "field(r)"
+ intrs
+ vimage "[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"
+ monos "[Pow_mono]"
+
+end
--- a/src/ZF/ex/BT.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/BT.ML Fri Aug 12 12:28:46 1994 +0200
@@ -1,44 +1,29 @@
-(* Title: ZF/ex/bt.ML
+(* Title: ZF/ex/BT.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
+ Copyright 1994 University of Cambridge
Datatype definition of binary trees
*)
-structure BT = Datatype_Fun
- (val thy = Univ.thy;
- val thy_name = "BT";
- val rec_specs =
- [("bt", "univ(A)",
- [(["Lf"],"i",NoSyn),
- (["Br"],"[i,i,i]=>i", NoSyn)])];
- val rec_styp = "i=>i";
- val sintrs =
- ["Lf : bt(A)",
- "[| a: A; t1: bt(A); t2: bt(A) |] ==> Br(a,t1,t2) : bt(A)"];
- val monos = [];
- val type_intrs = datatype_intrs
- val type_elims = []);
-
-val [LfI, BrI] = BT.intrs;
+open BT;
(*Perform induction on l, then prove the major premise using prems. *)
fun bt_ind_tac a prems i =
- EVERY [res_inst_tac [("x",a)] BT.induct i,
+ EVERY [res_inst_tac [("x",a)] bt.induct i,
rename_last_tac a ["1","2"] (i+2),
ares_tac prems i];
(** Lemmas to justify using "bt" in other recursive type definitions **)
-goalw BT.thy BT.defs "!!A B. A<=B ==> bt(A) <= bt(B)";
+goalw BT.thy bt.defs "!!A B. A<=B ==> bt(A) <= bt(B)";
by (rtac lfp_mono 1);
-by (REPEAT (rtac BT.bnd_mono 1));
+by (REPEAT (rtac bt.bnd_mono 1));
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
val bt_mono = result();
-goalw BT.thy (BT.defs@BT.con_defs) "bt(univ(A)) <= univ(A)";
+goalw BT.thy (bt.defs@bt.con_defs) "bt(univ(A)) <= univ(A)";
by (rtac lfp_lowerbound 1);
by (rtac (A_subset_univ RS univ_mono) 2);
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
@@ -47,3 +32,119 @@
val bt_subset_univ = standard ([bt_mono, bt_univ] MRS subset_trans);
+
+(** bt_rec -- by Vset recursion **)
+
+goalw BT.thy bt.con_defs "rank(l) < rank(Br(a,l,r))";
+by (simp_tac rank_ss 1);
+val rank_Br1 = result();
+
+goalw BT.thy bt.con_defs "rank(r) < rank(Br(a,l,r))";
+by (simp_tac rank_ss 1);
+val rank_Br2 = result();
+
+goal BT.thy "bt_rec(Lf,c,h) = c";
+by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
+by (simp_tac (ZF_ss addsimps bt.case_eqns) 1);
+val bt_rec_Lf = result();
+
+goal BT.thy
+ "bt_rec(Br(a,l,r), c, h) = h(a, l, r, bt_rec(l,c,h), bt_rec(r,c,h))";
+by (rtac (bt_rec_def RS def_Vrec RS trans) 1);
+by (simp_tac (rank_ss addsimps (bt.case_eqns @ [rank_Br1, rank_Br2])) 1);
+val bt_rec_Br = result();
+
+(*Type checking -- proved by induction, as usual*)
+val prems = goal BT.thy
+ "[| t: bt(A); \
+\ c: C(Lf); \
+\ !!x y z r s. [| x:A; y:bt(A); z:bt(A); r:C(y); s:C(z) |] ==> \
+\ h(x,y,z,r,s): C(Br(x,y,z)) \
+\ |] ==> bt_rec(t,c,h) : C(t)";
+by (bt_ind_tac "t" prems 1);
+by (ALLGOALS (asm_simp_tac (ZF_ss addsimps
+ (prems@[bt_rec_Lf,bt_rec_Br]))));
+val bt_rec_type = result();
+
+(** Versions for use with definitions **)
+
+val [rew] = goal BT.thy "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Lf) = c";
+by (rewtac rew);
+by (rtac bt_rec_Lf 1);
+val def_bt_rec_Lf = result();
+
+val [rew] = goal BT.thy
+ "[| !!t. j(t)==bt_rec(t, c, h) |] ==> j(Br(a,l,r)) = h(a,l,r,j(l),j(r))";
+by (rewtac rew);
+by (rtac bt_rec_Br 1);
+val def_bt_rec_Br = result();
+
+fun bt_recs def = map standard ([def] RL [def_bt_rec_Lf, def_bt_rec_Br]);
+
+(** n_nodes **)
+
+val [n_nodes_Lf,n_nodes_Br] = bt_recs n_nodes_def;
+
+val prems = goalw BT.thy [n_nodes_def]
+ "xs: bt(A) ==> n_nodes(xs) : nat";
+by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
+val n_nodes_type = result();
+
+
+(** n_leaves **)
+
+val [n_leaves_Lf,n_leaves_Br] = bt_recs n_leaves_def;
+
+val prems = goalw BT.thy [n_leaves_def]
+ "xs: bt(A) ==> n_leaves(xs) : nat";
+by (REPEAT (ares_tac (prems @ [bt_rec_type, nat_0I, nat_succI, add_type]) 1));
+val n_leaves_type = result();
+
+(** bt_reflect **)
+
+val [bt_reflect_Lf, bt_reflect_Br] = bt_recs bt_reflect_def;
+
+goalw BT.thy [bt_reflect_def] "!!xs. xs: bt(A) ==> bt_reflect(xs) : bt(A)";
+by (REPEAT (ares_tac (bt.intrs @ [bt_rec_type]) 1));
+val bt_reflect_type = result();
+
+
+(** BT simplification **)
+
+
+val bt_typechecks =
+ bt.intrs @ [bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
+
+val bt_ss = arith_ss
+ addsimps bt.case_eqns
+ addsimps bt_typechecks
+ addsimps [bt_rec_Lf, bt_rec_Br,
+ n_nodes_Lf, n_nodes_Br,
+ n_leaves_Lf, n_leaves_Br,
+ bt_reflect_Lf, bt_reflect_Br];
+
+
+(*** theorems about n_leaves ***)
+
+val prems = goal BT.thy
+ "t: bt(A) ==> n_leaves(bt_reflect(t)) = n_leaves(t)";
+by (bt_ind_tac "t" prems 1);
+by (ALLGOALS (asm_simp_tac bt_ss));
+by (REPEAT (ares_tac [add_commute, n_leaves_type] 1));
+val n_leaves_reflect = result();
+
+val prems = goal BT.thy
+ "t: bt(A) ==> n_leaves(t) = succ(n_nodes(t))";
+by (bt_ind_tac "t" prems 1);
+by (ALLGOALS (asm_simp_tac (bt_ss addsimps [add_succ_right])));
+val n_leaves_nodes = result();
+
+(*** theorems about bt_reflect ***)
+
+val prems = goal BT.thy
+ "t: bt(A) ==> bt_reflect(bt_reflect(t))=t";
+by (bt_ind_tac "t" prems 1);
+by (ALLGOALS (asm_simp_tac bt_ss));
+val bt_reflect_bt_reflect_ident = result();
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/BT.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,29 @@
+(* Title: ZF/ex/bt-fn.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1992 University of Cambridge
+
+Binary trees
+*)
+
+BT = Univ +
+consts
+ bt_rec :: "[i, i, [i,i,i,i,i]=>i] => i"
+ n_nodes :: "i=>i"
+ n_leaves :: "i=>i"
+ bt_reflect :: "i=>i"
+
+ bt :: "i=>i"
+
+datatype
+ "bt(A)" = Lf | Br ("a: A", "t1: bt(A)", "t2: bt(A)")
+
+rules
+ bt_rec_def
+ "bt_rec(t,c,h) == Vrec(t, %t g.bt_case(c, %x y z. h(x,y,z,g`y,g`z), t))"
+
+ n_nodes_def "n_nodes(t) == bt_rec(t, 0, %x y z r s. succ(r#+s))"
+ n_leaves_def "n_leaves(t) == bt_rec(t, succ(0), %x y z r s. r#+s)"
+ bt_reflect_def "bt_reflect(t) == bt_rec(t, Lf, %x y z r s. Br(x,s,r))"
+
+end
--- a/src/ZF/ex/Bin.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Bin.ML Fri Aug 12 12:28:46 1994 +0200
@@ -1,31 +1,456 @@
-(* Title: ZF/ex/bin.ML
+(* Title: ZF/ex/Bin.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
+ Copyright 1994 University of Cambridge
-Datatype of binary integers
+For Bin.thy. Arithmetic on binary integers.
*)
-(*Example of a datatype with an infix constructor*)
-structure Bin = Datatype_Fun
- (val thy = Univ.thy;
- val thy_name = "Bin";
- val rec_specs =
- [("bin", "univ(0)",
- [(["Plus", "Minus"], "i", NoSyn),
- (["$$"], "[i,i]=>i", Infixl 60)])];
- val rec_styp = "i";
- val sintrs =
- ["Plus : bin",
- "Minus : bin",
- "[| w: bin; b: bool |] ==> w$$b : bin"];
- val monos = [];
- val type_intrs = datatype_intrs @ [bool_into_univ];
- val type_elims = []);
+open Bin;
(*Perform induction on l, then prove the major premise using prems. *)
fun bin_ind_tac a prems i =
- EVERY [res_inst_tac [("x",a)] Bin.induct i,
+ EVERY [res_inst_tac [("x",a)] bin.induct i,
rename_last_tac a ["1"] (i+3),
ares_tac prems i];
+
+(** bin_rec -- by Vset recursion **)
+
+goal Bin.thy "bin_rec(Plus,a,b,h) = a";
+by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac bin.con_defs);
+by (simp_tac rank_ss 1);
+val bin_rec_Plus = result();
+
+goal Bin.thy "bin_rec(Minus,a,b,h) = b";
+by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac bin.con_defs);
+by (simp_tac rank_ss 1);
+val bin_rec_Minus = result();
+
+goal Bin.thy "bin_rec(w$$x,a,b,h) = h(w, x, bin_rec(w,a,b,h))";
+by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac bin.con_defs);
+by (simp_tac rank_ss 1);
+val bin_rec_Bcons = result();
+
+(*Type checking*)
+val prems = goal Bin.thy
+ "[| w: bin; \
+\ a: C(Plus); b: C(Minus); \
+\ !!w x r. [| w: bin; x: bool; r: C(w) |] ==> h(w,x,r): C(w$$x) \
+\ |] ==> bin_rec(w,a,b,h) : C(w)";
+by (bin_ind_tac "w" prems 1);
+by (ALLGOALS
+ (asm_simp_tac (ZF_ss addsimps (prems@[bin_rec_Plus,bin_rec_Minus,
+ bin_rec_Bcons]))));
+val bin_rec_type = result();
+
+(** Versions for use with definitions **)
+
+val [rew] = goal Bin.thy
+ "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Plus) = a";
+by (rewtac rew);
+by (rtac bin_rec_Plus 1);
+val def_bin_rec_Plus = result();
+
+val [rew] = goal Bin.thy
+ "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Minus) = b";
+by (rewtac rew);
+by (rtac bin_rec_Minus 1);
+val def_bin_rec_Minus = result();
+
+val [rew] = goal Bin.thy
+ "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(w$$x) = h(w,x,j(w))";
+by (rewtac rew);
+by (rtac bin_rec_Bcons 1);
+val def_bin_rec_Bcons = result();
+
+fun bin_recs def = map standard
+ ([def] RL [def_bin_rec_Plus, def_bin_rec_Minus, def_bin_rec_Bcons]);
+
+(** Type checking **)
+
+val bin_typechecks0 = bin_rec_type :: bin.intrs;
+
+goalw Bin.thy [integ_of_bin_def]
+ "!!w. w: bin ==> integ_of_bin(w) : integ";
+by (typechk_tac (bin_typechecks0@integ_typechecks@
+ nat_typechecks@[bool_into_nat]));
+val integ_of_bin_type = result();
+
+goalw Bin.thy [bin_succ_def]
+ "!!w. w: bin ==> bin_succ(w) : bin";
+by (typechk_tac (bin_typechecks0@bool_typechecks));
+val bin_succ_type = result();
+
+goalw Bin.thy [bin_pred_def]
+ "!!w. w: bin ==> bin_pred(w) : bin";
+by (typechk_tac (bin_typechecks0@bool_typechecks));
+val bin_pred_type = result();
+
+goalw Bin.thy [bin_minus_def]
+ "!!w. w: bin ==> bin_minus(w) : bin";
+by (typechk_tac ([bin_pred_type]@bin_typechecks0@bool_typechecks));
+val bin_minus_type = result();
+
+goalw Bin.thy [bin_add_def]
+ "!!v w. [| v: bin; w: bin |] ==> bin_add(v,w) : bin";
+by (typechk_tac ([bin_succ_type,bin_pred_type]@bin_typechecks0@
+ bool_typechecks@ZF_typechecks));
+val bin_add_type = result();
+
+goalw Bin.thy [bin_mult_def]
+ "!!v w. [| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
+by (typechk_tac ([bin_minus_type,bin_add_type]@bin_typechecks0@
+ bool_typechecks));
+val bin_mult_type = result();
+
+val bin_typechecks = bin_typechecks0 @
+ [integ_of_bin_type, bin_succ_type, bin_pred_type,
+ bin_minus_type, bin_add_type, bin_mult_type];
+
+val bin_ss = integ_ss
+ addsimps([bool_1I, bool_0I,
+ bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @
+ bin_recs integ_of_bin_def @ bool_simps @ bin_typechecks);
+
+val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @
+ [bool_subset_nat RS subsetD];
+
+(**** The carry/borrow functions, bin_succ and bin_pred ****)
+
+(** Lemmas **)
+
+goal Integ.thy
+ "!!z v. [| z $+ v = z' $+ v'; \
+\ z: integ; z': integ; v: integ; v': integ; w: integ |] \
+\ ==> z $+ (v $+ w) = z' $+ (v' $+ w)";
+by (asm_simp_tac (integ_ss addsimps ([zadd_assoc RS sym])) 1);
+val zadd_assoc_cong = result();
+
+goal Integ.thy
+ "!!z v w. [| z: integ; v: integ; w: integ |] \
+\ ==> z $+ (v $+ w) = v $+ (z $+ w)";
+by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
+val zadd_assoc_swap = result();
+
+val zadd_cong =
+ read_instantiate_sg (sign_of Integ.thy) [("t","op $+")] subst_context2;
+
+val zadd_kill = (refl RS zadd_cong);
+val zadd_assoc_swap_kill = zadd_kill RSN (4, zadd_assoc_swap RS trans);
+
+(*Pushes 'constants' of the form $#m to the right -- LOOPS if two!*)
+val zadd_assoc_znat = standard (znat_type RS zadd_assoc_swap);
+
+goal Integ.thy
+ "!!z w. [| z: integ; w: integ |] \
+\ ==> w $+ (z $+ (w $+ z)) = w $+ (w $+ (z $+ z))";
+by (REPEAT (ares_tac [zadd_kill, zadd_assoc_swap] 1));
+val zadd_swap_pairs = result();
+
+
+val carry_ss = bin_ss addsimps
+ (bin_recs bin_succ_def @ bin_recs bin_pred_def);
+
+goal Bin.thy
+ "!!w. w: bin ==> integ_of_bin(bin_succ(w)) = $#1 $+ integ_of_bin(w)";
+by (etac bin.induct 1);
+by (simp_tac (carry_ss addsimps [zadd_0_right]) 1);
+by (simp_tac (carry_ss addsimps [zadd_zminus_inverse]) 1);
+by (etac boolE 1);
+by (ALLGOALS (asm_simp_tac (carry_ss addsimps [zadd_assoc])));
+by (REPEAT (ares_tac (zadd_swap_pairs::typechecks) 1));
+val integ_of_bin_succ = result();
+
+goal Bin.thy
+ "!!w. w: bin ==> integ_of_bin(bin_pred(w)) = $~ ($#1) $+ integ_of_bin(w)";
+by (etac bin.induct 1);
+by (simp_tac (carry_ss addsimps [zadd_0_right]) 1);
+by (simp_tac (carry_ss addsimps [zadd_zminus_inverse]) 1);
+by (etac boolE 1);
+by (ALLGOALS
+ (asm_simp_tac
+ (carry_ss addsimps [zadd_assoc RS sym,
+ zadd_zminus_inverse, zadd_zminus_inverse2])));
+by (REPEAT (ares_tac ([zadd_commute, zadd_cong, refl]@typechecks) 1));
+val integ_of_bin_pred = result();
+
+(*These two results replace the definitions of bin_succ and bin_pred*)
+
+
+(*** bin_minus: (unary!) negation of binary integers ***)
+
+val bin_minus_ss =
+ bin_ss addsimps (bin_recs bin_minus_def @
+ [integ_of_bin_succ, integ_of_bin_pred]);
+
+goal Bin.thy
+ "!!w. w: bin ==> integ_of_bin(bin_minus(w)) = $~ integ_of_bin(w)";
+by (etac bin.induct 1);
+by (simp_tac (bin_minus_ss addsimps [zminus_0]) 1);
+by (simp_tac (bin_minus_ss addsimps [zadd_0_right]) 1);
+by (etac boolE 1);
+by (ALLGOALS
+ (asm_simp_tac (bin_minus_ss addsimps [zminus_zadd_distrib, zadd_assoc])));
+val integ_of_bin_minus = result();
+
+
+(*** bin_add: binary addition ***)
+
+goalw Bin.thy [bin_add_def] "!!w. w: bin ==> bin_add(Plus,w) = w";
+by (asm_simp_tac bin_ss 1);
+val bin_add_Plus = result();
+
+goalw Bin.thy [bin_add_def] "!!w. w: bin ==> bin_add(Minus,w) = bin_pred(w)";
+by (asm_simp_tac bin_ss 1);
+val bin_add_Minus = result();
+
+goalw Bin.thy [bin_add_def] "bin_add(v$$x,Plus) = v$$x";
+by (simp_tac bin_ss 1);
+val bin_add_Bcons_Plus = result();
+
+goalw Bin.thy [bin_add_def] "bin_add(v$$x,Minus) = bin_pred(v$$x)";
+by (simp_tac bin_ss 1);
+val bin_add_Bcons_Minus = result();
+
+goalw Bin.thy [bin_add_def]
+ "!!w y. [| w: bin; y: bool |] ==> \
+\ bin_add(v$$x, w$$y) = \
+\ bin_add(v, cond(x and y, bin_succ(w), w)) $$ (x xor y)";
+by (asm_simp_tac bin_ss 1);
+val bin_add_Bcons_Bcons = result();
+
+val bin_add_rews = [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus,
+ bin_add_Bcons_Minus, bin_add_Bcons_Bcons,
+ integ_of_bin_succ, integ_of_bin_pred];
+
+val bin_add_ss = bin_ss addsimps ([bool_subset_nat RS subsetD] @ bin_add_rews);
+
+goal Bin.thy
+ "!!v. v: bin ==> \
+\ ALL w: bin. integ_of_bin(bin_add(v,w)) = \
+\ integ_of_bin(v) $+ integ_of_bin(w)";
+by (etac bin.induct 1);
+by (simp_tac bin_add_ss 1);
+by (simp_tac bin_add_ss 1);
+by (rtac ballI 1);
+by (bin_ind_tac "wa" [] 1);
+by (asm_simp_tac (bin_add_ss addsimps [zadd_0_right]) 1);
+by (asm_simp_tac bin_add_ss 1);
+by (REPEAT (ares_tac (zadd_commute::typechecks) 1));
+by (etac boolE 1);
+by (asm_simp_tac (bin_add_ss addsimps [zadd_assoc, zadd_swap_pairs]) 2);
+by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill]@typechecks) 2));
+by (etac boolE 1);
+by (ALLGOALS (asm_simp_tac (bin_add_ss addsimps [zadd_assoc,zadd_swap_pairs])));
+by (REPEAT (ares_tac ([refl, zadd_kill, zadd_assoc_swap_kill RS sym]@
+ typechecks) 1));
+val integ_of_bin_add_lemma = result();
+
+val integ_of_bin_add = integ_of_bin_add_lemma RS bspec;
+
+
+(*** bin_add: binary multiplication ***)
+
+val bin_mult_ss =
+ bin_ss addsimps (bin_recs bin_mult_def @
+ [integ_of_bin_minus, integ_of_bin_add]);
+
+
+val major::prems = goal Bin.thy
+ "[| v: bin; w: bin |] ==> \
+\ integ_of_bin(bin_mult(v,w)) = \
+\ integ_of_bin(v) $* integ_of_bin(w)";
+by (cut_facts_tac prems 1);
+by (bin_ind_tac "v" [major] 1);
+by (asm_simp_tac (bin_mult_ss addsimps [zmult_0]) 1);
+by (asm_simp_tac (bin_mult_ss addsimps [zmult_1,zmult_zminus]) 1);
+by (etac boolE 1);
+by (asm_simp_tac (bin_mult_ss addsimps [zadd_zmult_distrib]) 2);
+by (asm_simp_tac
+ (bin_mult_ss addsimps [zadd_zmult_distrib, zmult_1, zadd_assoc]) 1);
+by (REPEAT (ares_tac ([zadd_commute, zadd_assoc_swap_kill RS sym]@
+ typechecks) 1));
+val integ_of_bin_mult = result();
+
+(**** Computations ****)
+
+(** extra rules for bin_succ, bin_pred **)
+
+val [bin_succ_Plus, bin_succ_Minus, _] = bin_recs bin_succ_def;
+val [bin_pred_Plus, bin_pred_Minus, _] = bin_recs bin_pred_def;
+
+goal Bin.thy "bin_succ(w$$1) = bin_succ(w) $$ 0";
+by (simp_tac carry_ss 1);
+val bin_succ_Bcons1 = result();
+
+goal Bin.thy "bin_succ(w$$0) = w$$1";
+by (simp_tac carry_ss 1);
+val bin_succ_Bcons0 = result();
+
+goal Bin.thy "bin_pred(w$$1) = w$$0";
+by (simp_tac carry_ss 1);
+val bin_pred_Bcons1 = result();
+
+goal Bin.thy "bin_pred(w$$0) = bin_pred(w) $$ 1";
+by (simp_tac carry_ss 1);
+val bin_pred_Bcons0 = result();
+
+(** extra rules for bin_minus **)
+
+val [bin_minus_Plus, bin_minus_Minus, _] = bin_recs bin_minus_def;
+
+goal Bin.thy "bin_minus(w$$1) = bin_pred(bin_minus(w) $$ 0)";
+by (simp_tac bin_minus_ss 1);
+val bin_minus_Bcons1 = result();
+
+goal Bin.thy "bin_minus(w$$0) = bin_minus(w) $$ 0";
+by (simp_tac bin_minus_ss 1);
+val bin_minus_Bcons0 = result();
+
+(** extra rules for bin_add **)
+
+goal Bin.thy
+ "!!w. w: bin ==> bin_add(v$$1, w$$1) = bin_add(v, bin_succ(w)) $$ 0";
+by (asm_simp_tac bin_add_ss 1);
+val bin_add_Bcons_Bcons11 = result();
+
+goal Bin.thy
+ "!!w. w: bin ==> bin_add(v$$1, w$$0) = bin_add(v,w) $$ 1";
+by (asm_simp_tac bin_add_ss 1);
+val bin_add_Bcons_Bcons10 = result();
+
+goal Bin.thy
+ "!!w y.[| w: bin; y: bool |] ==> bin_add(v$$0, w$$y) = bin_add(v,w) $$ y";
+by (asm_simp_tac bin_add_ss 1);
+val bin_add_Bcons_Bcons0 = result();
+
+(** extra rules for bin_mult **)
+
+val [bin_mult_Plus, bin_mult_Minus, _] = bin_recs bin_mult_def;
+
+goal Bin.thy "bin_mult(v$$1, w) = bin_add(bin_mult(v,w)$$0, w)";
+by (simp_tac bin_mult_ss 1);
+val bin_mult_Bcons1 = result();
+
+goal Bin.thy "bin_mult(v$$0, w) = bin_mult(v,w)$$0";
+by (simp_tac bin_mult_ss 1);
+val bin_mult_Bcons0 = result();
+
+
+(*** The computation simpset ***)
+
+val bin_comp_ss = integ_ss
+ addsimps [bin_succ_Plus, bin_succ_Minus,
+ bin_succ_Bcons1, bin_succ_Bcons0,
+ bin_pred_Plus, bin_pred_Minus,
+ bin_pred_Bcons1, bin_pred_Bcons0,
+ bin_minus_Plus, bin_minus_Minus,
+ bin_minus_Bcons1, bin_minus_Bcons0,
+ bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus,
+ bin_add_Bcons_Minus, bin_add_Bcons_Bcons0,
+ bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11,
+ bin_mult_Plus, bin_mult_Minus,
+ bin_mult_Bcons1, bin_mult_Bcons0]
+ setsolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
+
+(*** Examples of performing binary arithmetic by simplification ***)
+
+proof_timing := true;
+(*All runtimes below are on a SPARCserver 10*)
+
+(* 13+19 = 32 *)
+goal Bin.thy
+ "bin_add(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = Plus$$1$$0$$0$$0$$0$$0";
+by (simp_tac bin_comp_ss 1); (*0.6 secs*)
+result();
+
+bin_add(binary_of_int 13, binary_of_int 19);
+
+(* 1234+5678 = 6912 *)
+goal Bin.thy
+ "bin_add(Plus$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0, \
+\ Plus$$1$$0$$1$$1$$0$$0$$0$$1$$0$$1$$1$$1$$0) = \
+\ Plus$$1$$1$$0$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0";
+by (simp_tac bin_comp_ss 1); (*2.6 secs*)
+result();
+
+bin_add(binary_of_int 1234, binary_of_int 5678);
+
+(* 1359-2468 = ~1109 *)
+goal Bin.thy
+ "bin_add(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, \
+\ Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = \
+\ Minus$$1$$0$$1$$1$$1$$0$$1$$0$$1$$0$$1$$1";
+by (simp_tac bin_comp_ss 1); (*2.3 secs*)
+result();
+
+bin_add(binary_of_int 1359, binary_of_int ~2468);
+
+(* 93746-46375 = 47371 *)
+goal Bin.thy
+ "bin_add(Plus$$1$$0$$1$$1$$0$$1$$1$$1$$0$$0$$0$$1$$1$$0$$0$$1$$0, \
+\ Minus$$0$$1$$0$$0$$1$$0$$1$$0$$1$$1$$0$$1$$1$$0$$0$$1) = \
+\ Plus$$0$$1$$0$$1$$1$$1$$0$$0$$1$$0$$0$$0$$0$$1$$0$$1$$1";
+by (simp_tac bin_comp_ss 1); (*3.9 secs*)
+result();
+
+bin_add(binary_of_int 93746, binary_of_int ~46375);
+
+(* negation of 65745 *)
+goal Bin.thy
+ "bin_minus(Plus$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1$$1$$0$$1$$0$$0$$0$$1) = \
+\ Minus$$0$$1$$1$$1$$1$$1$$1$$1$$1$$0$$0$$1$$0$$1$$1$$1$$1";
+by (simp_tac bin_comp_ss 1); (*0.6 secs*)
+result();
+
+bin_minus(binary_of_int 65745);
+
+(* negation of ~54321 *)
+goal Bin.thy
+ "bin_minus(Minus$$0$$0$$1$$0$$1$$0$$1$$1$$1$$1$$0$$0$$1$$1$$1$$1) = \
+\ Plus$$0$$1$$1$$0$$1$$0$$1$$0$$0$$0$$0$$1$$1$$0$$0$$0$$1";
+by (simp_tac bin_comp_ss 1); (*0.7 secs*)
+result();
+
+bin_minus(binary_of_int ~54321);
+
+(* 13*19 = 247 *)
+goal Bin.thy "bin_mult(Plus$$1$$1$$0$$1, Plus$$1$$0$$0$$1$$1) = \
+\ Plus$$1$$1$$1$$1$$0$$1$$1$$1";
+by (simp_tac bin_comp_ss 1); (*1.5 secs*)
+result();
+
+bin_mult(binary_of_int 13, binary_of_int 19);
+
+(* ~84 * 51 = ~4284 *)
+goal Bin.thy
+ "bin_mult(Minus$$0$$1$$0$$1$$1$$0$$0, Plus$$1$$1$$0$$0$$1$$1) = \
+\ Minus$$0$$1$$1$$1$$1$$0$$1$$0$$0$$0$$1$$0$$0";
+by (simp_tac bin_comp_ss 1); (*2.6 secs*)
+result();
+
+bin_mult(binary_of_int ~84, binary_of_int 51);
+
+(* 255*255 = 65025; the worst case for 8-bit operands *)
+goal Bin.thy
+ "bin_mult(Plus$$1$$1$$1$$1$$1$$1$$1$$1, \
+\ Plus$$1$$1$$1$$1$$1$$1$$1$$1) = \
+\ Plus$$1$$1$$1$$1$$1$$1$$1$$0$$0$$0$$0$$0$$0$$0$$0$$1";
+by (simp_tac bin_comp_ss 1); (*9.8 secs*)
+result();
+
+bin_mult(binary_of_int 255, binary_of_int 255);
+
+(* 1359 * ~2468 = ~3354012 *)
+goal Bin.thy
+ "bin_mult(Plus$$1$$0$$1$$0$$1$$0$$0$$1$$1$$1$$1, \
+\ Minus$$0$$1$$1$$0$$0$$1$$0$$1$$1$$1$$0$$0) = \
+\ Minus$$0$$0$$1$$1$$0$$0$$1$$1$$0$$1$$0$$0$$1$$0$$0$$1$$1$$0$$0$$1$$0$$0";
+by (simp_tac bin_comp_ss 1); (*13.7 secs*)
+result();
+
+bin_mult(binary_of_int 1359, binary_of_int ~2468);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Bin.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,60 @@
+(* Title: ZF/ex/Bin.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Arithmetic on binary integers.
+*)
+
+Bin = Integ + Univ +
+consts
+ bin_rec :: "[i, i, i, [i,i,i]=>i] => i"
+ integ_of_bin :: "i=>i"
+ bin_succ :: "i=>i"
+ bin_pred :: "i=>i"
+ bin_minus :: "i=>i"
+ bin_add,bin_mult :: "[i,i]=>i"
+
+ bin :: "i"
+
+datatype
+ "bin" = Plus
+ | Minus
+ | "$$" ("w: bin", "b: bool") (infixl 60)
+ type_intrs "[bool_into_univ]"
+
+rules
+
+ bin_rec_def
+ "bin_rec(z,a,b,h) == \
+\ Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
+
+ integ_of_bin_def
+ "integ_of_bin(w) == bin_rec(w, $#0, $~($#1), %w x r. $#x $+ r $+ r)"
+
+ bin_succ_def
+ "bin_succ(w0) == bin_rec(w0, Plus$$1, Plus, %w x r. cond(x, r$$0, w$$1))"
+
+ bin_pred_def
+ "bin_pred(w0) == \
+\ bin_rec(w0, Minus, Minus$$0, %w x r. cond(x, w$$0, r$$1))"
+
+ bin_minus_def
+ "bin_minus(w0) == \
+\ bin_rec(w0, Plus, Plus$$1, %w x r. cond(x, bin_pred(r$$0), r$$0))"
+
+ bin_add_def
+ "bin_add(v0,w0) == \
+\ bin_rec(v0, \
+\ lam w:bin. w, \
+\ lam w:bin. bin_pred(w), \
+\ %v x r. lam w1:bin. \
+\ bin_rec(w1, v$$x, bin_pred(v$$x), \
+\ %w y s. (r`cond(x and y, bin_succ(w), w)) \
+\ $$ (x xor y))) ` w0"
+
+ bin_mult_def
+ "bin_mult(v0,w) == \
+\ bin_rec(v0, Plus, bin_minus(w), \
+\ %v x r. cond(x, bin_add(r$$0,w), r$$0))"
+end
--- a/src/ZF/ex/Brouwer.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Brouwer.ML Fri Aug 12 12:28:46 1994 +0200
@@ -6,28 +6,16 @@
Datatype definition of the Brouwer ordinals -- demonstrates infinite branching
*)
-structure Brouwer = Datatype_Fun
- (val thy = InfDatatype.thy;
- val thy_name = "Brouwer";
- val rec_specs = [("brouwer", "Vfrom(0, csucc(nat))",
- [(["Zero"], "i", NoSyn),
- (["Suc","Lim"], "i=>i", NoSyn)])];
- val rec_styp = "i";
- val sintrs = ["Zero : brouwer",
- "b: brouwer ==> Suc(b): brouwer",
- "h: nat -> brouwer ==> Lim(h) : brouwer"];
- val monos = [Pi_mono];
- val type_intrs = inf_datatype_intrs;
- val type_elims = []);
-
-val [ZeroI, SucI, LimI] = Brouwer.intrs;
+open Brouwer;
goal Brouwer.thy "brouwer = {0} + brouwer + (nat -> brouwer)";
-by (rtac (Brouwer.unfold RS trans) 1);
-bws Brouwer.con_defs;
-by (fast_tac (sum_cs addIs ([equalityI] @ inf_datatype_intrs)
- addDs [Brouwer.dom_subset RS subsetD]
- addEs [A_into_Vfrom, fun_into_Vfrom_csucc]) 1);
+by (rtac (brouwer.unfold RS trans) 1);
+bws brouwer.con_defs;
+br equalityI 1;
+by (fast_tac sum_cs 1);
+by (fast_tac (sum_cs addIs inf_datatype_intrs
+ addDs [brouwer.dom_subset RS subsetD]
+ addEs [fun_into_Vcsucc]) 1);
val brouwer_unfold = result();
(*A nicer induction rule than the standard one*)
@@ -38,7 +26,7 @@
\ !!h. [| h: nat -> brouwer; ALL i:nat. P(h`i) \
\ |] ==> P(Lim(h)) \
\ |] ==> P(b)";
-by (rtac (major RS Brouwer.induct) 1);
+by (rtac (major RS brouwer.induct) 1);
by (REPEAT_SOME (ares_tac prems));
by (fast_tac (ZF_cs addEs [fun_weaken_type]) 1);
by (fast_tac (ZF_cs addDs [apply_type]) 1);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Brouwer.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,18 @@
+(* Title: ZF/ex/Brouwer.thy
+ ID: $ $
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Datatype definition of the Brouwer ordinals -- demonstrates infinite branching
+*)
+
+Brouwer = InfDatatype +
+consts
+ brouwer :: "i"
+
+datatype <= "Vfrom(0, csucc(nat))"
+ "brouwer" = Zero | Suc ("b: brouwer") | Lim ("h: nat -> brouwer")
+ monos "[Pi_mono]"
+ type_intrs "inf_datatype_intrs"
+
+end
--- a/src/ZF/ex/CoUnit.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/CoUnit.ML Fri Aug 12 12:28:46 1994 +0200
@@ -1,105 +1,75 @@
-(* Title: ZF/ex/counit.ML
+(* Title: ZF/ex/CoUnit.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
+ Copyright 1994 University of Cambridge
Trivial codatatype definitions, one of which goes wrong!
-Need to find sufficient conditions for codatatypes to work correctly!
+See discussion in
+ L C Paulson. A Concrete Final Coalgebra Theorem for ZF Set Theory.
+ Report 334, Cambridge University Computer Laboratory. 1994.
*)
-(*This degenerate definition does not work well because the one constructor's
- definition is trivial! The same thing occurs with Aczel's Special Final
- Coalgebra Theorem
-*)
-structure CoUnit = CoDatatype_Fun
- (val thy = QUniv.thy;
- val thy_name = "CoUnit";
- val rec_specs =
- [("counit", "quniv(0)",
- [(["Con"], "i=>i", NoSyn)])];
- val rec_styp = "i";
- val sintrs = ["x: counit ==> Con(x) : counit"];
- val monos = [];
- val type_intrs = codatatype_intrs
- val type_elims = codatatype_elims);
+open CoUnit;
-val [ConI] = CoUnit.intrs;
-
(*USELESS because folding on Con(?xa) == ?xa fails*)
-val ConE = CoUnit.mk_cases CoUnit.con_defs "Con(x) : counit";
+val ConE = counit.mk_cases counit.con_defs "Con(x) : counit";
(*Proving freeness results*)
-val Con_iff = CoUnit.mk_free "Con(x)=Con(y) <-> x=y";
+val Con_iff = counit.mk_free "Con(x)=Con(y) <-> x=y";
(*Should be a singleton, not everything!*)
goal CoUnit.thy "counit = quniv(0)";
-by (rtac (CoUnit.dom_subset RS equalityI) 1);
+by (rtac (counit.dom_subset RS equalityI) 1);
by (rtac subsetI 1);
-by (etac CoUnit.coinduct 1);
+by (etac counit.coinduct 1);
by (rtac subset_refl 1);
-by (rewrite_goals_tac CoUnit.con_defs);
+by (rewrite_goals_tac counit.con_defs);
by (fast_tac ZF_cs 1);
val counit_eq_univ = result();
-(*****************************************************************)
-
(*A similar example, but the constructor is non-degenerate and it works!
The resulting set is a singleton.
*)
-structure CoUnit2 = CoDatatype_Fun
- (val thy = QUniv.thy;
- val thy_name = "CoUnit2";
- val rec_specs =
- [("counit2", "quniv(0)",
- [(["Con2"], "[i,i]=>i", NoSyn)])];
- val rec_styp = "i";
- val sintrs = ["[| x: counit2; y: counit2 |] ==> Con2(x,y) : counit2"];
- val monos = [];
- val type_intrs = codatatype_intrs
- val type_elims = codatatype_elims);
-
-val [Con2I] = CoUnit2.intrs;
-
-val Con2E = CoUnit2.mk_cases CoUnit2.con_defs "Con2(x,y) : counit2";
+val Con2E = counit2.mk_cases counit2.con_defs "Con2(x,y) : counit2";
(*Proving freeness results*)
-val Con2_iff = CoUnit2.mk_free "Con2(x,y)=Con2(x',y') <-> x=x' & y=y'";
+val Con2_iff = counit2.mk_free "Con2(x,y)=Con2(x',y') <-> x=x' & y=y'";
-goalw CoUnit2.thy CoUnit2.con_defs "bnd_mono(univ(0), %x. Con2(x,x))";
+goalw CoUnit.thy counit2.con_defs "bnd_mono(univ(0), %x. Con2(x,x))";
by (rtac bnd_monoI 1);
by (REPEAT (ares_tac [subset_refl, QPair_subset_univ, QPair_mono] 1));
val Con2_bnd_mono = result();
-goal CoUnit2.thy "lfp(univ(0), %x. Con2(x,x)) : counit2";
-by (rtac (singletonI RS CoUnit2.coinduct) 1);
+goal CoUnit.thy "lfp(univ(0), %x. Con2(x,x)) : counit2";
+by (rtac (singletonI RS counit2.coinduct) 1);
by (rtac (qunivI RS singleton_subsetI) 1);
by (rtac ([lfp_subset, empty_subsetI RS univ_mono] MRS subset_trans) 1);
by (fast_tac (ZF_cs addSIs [Con2_bnd_mono RS lfp_Tarski]) 1);
val lfp_Con2_in_counit2 = result();
(*Lemma for proving finality. Borrowed from ex/llist_eq.ML!*)
-goal CoUnit2.thy
+goal CoUnit.thy
"!!i. Ord(i) ==> ALL x y. x: counit2 & y: counit2 --> x Int Vset(i) <= y";
by (etac trans_induct 1);
by (safe_tac subset_cs);
-by (etac CoUnit2.elim 1);
-by (etac CoUnit2.elim 1);
-by (rewrite_goals_tac CoUnit2.con_defs);
+by (etac counit2.elim 1);
+by (etac counit2.elim 1);
+by (rewrite_goals_tac counit2.con_defs);
by (fast_tac lleq_cs 1);
val counit2_Int_Vset_subset_lemma = result();
val counit2_Int_Vset_subset = standard
(counit2_Int_Vset_subset_lemma RS spec RS spec RS mp);
-goal CoUnit2.thy "!!x y. [| x: counit2; y: counit2 |] ==> x=y";
+goal CoUnit.thy "!!x y. [| x: counit2; y: counit2 |] ==> x=y";
by (rtac equalityI 1);
by (REPEAT (ares_tac [conjI, counit2_Int_Vset_subset RS Int_Vset_subset] 1));
val counit2_implies_equal = result();
-goal CoUnit2.thy "counit2 = {lfp(univ(0), %x. Con2(x,x))}";
+goal CoUnit.thy "counit2 = {lfp(univ(0), %x. Con2(x,x))}";
by (rtac equalityI 1);
by (rtac (lfp_Con2_in_counit2 RS singleton_subsetI) 2);
by (rtac subsetI 1);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/CoUnit.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,34 @@
+(* Title: ZF/ex/CoUnit.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Trivial codatatype definitions, one of which goes wrong!
+
+See discussion in
+ L C Paulson. A Concrete Final Coalgebra Theorem for ZF Set Theory.
+ Report 334, Cambridge University Computer Laboratory. 1994.
+*)
+
+CoUnit = QUniv + "Datatype" +
+
+(*This degenerate definition does not work well because the one constructor's
+ definition is trivial! The same thing occurs with Aczel's Special Final
+ Coalgebra Theorem
+*)
+consts
+ counit :: "i"
+codatatype
+ "counit" = Con ("x: counit")
+
+
+(*A similar example, but the constructor is non-degenerate and it works!
+ The resulting set is a singleton.
+*)
+
+consts
+ counit2 :: "i"
+codatatype
+ "counit2" = Con2 ("x: counit2", "y: counit2")
+
+end
--- a/src/ZF/ex/Comb.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Comb.ML Fri Aug 12 12:28:46 1994 +0200
@@ -3,32 +3,234 @@
Author: Lawrence C Paulson
Copyright 1993 University of Cambridge
-Datatype definition of combinators S and K
+Combinatory Logic example: the Church-Rosser Theorem
+Curiously, combinators do not include free variables.
+
+Example taken from
+ J. Camilleri and T. F. Melham.
+ Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
+ Report 265, University of Cambridge Computer Laboratory, 1992.
+
+HOL system proofs may be found in
+/usr/groups/theory/hvg-aftp/contrib/rule-induction/cl.ml
+*)
+
+open Comb;
+
+val [_,_,comb_Ap] = comb.intrs;
+val Ap_E = comb.mk_cases comb.con_defs "p#q : comb";
+
+
+(*** Results about Contraction ***)
+
+val contract_induct = standard
+ (contract.mutual_induct RS spec RS spec RSN (2,rev_mp));
+
+(*For type checking: replaces a-1->b by a,b:comb *)
+val contract_combE2 = contract.dom_subset RS subsetD RS SigmaE2;
+val contract_combD1 = contract.dom_subset RS subsetD RS SigmaD1;
+val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2;
+
+goal Comb.thy "field(contract) = comb";
+by (fast_tac (ZF_cs addIs [equalityI,contract.K] addSEs [contract_combE2]) 1);
+val field_contract_eq = result();
+
+val reduction_refl = standard
+ (field_contract_eq RS equalityD2 RS subsetD RS rtrancl_refl);
+
+val rtrancl_into_rtrancl2 = standard
+ (r_into_rtrancl RS (trans_rtrancl RS transD));
+
+val reduction_rls = [reduction_refl, contract.K, contract.S,
+ contract.K RS rtrancl_into_rtrancl2,
+ contract.S RS rtrancl_into_rtrancl2,
+ contract.Ap1 RS rtrancl_into_rtrancl2,
+ contract.Ap2 RS rtrancl_into_rtrancl2];
+
+(*Example only: not used*)
+goalw Comb.thy [I_def] "!!p. p:comb ==> I#p ---> p";
+by (REPEAT (ares_tac (comb.intrs @ reduction_rls) 1));
+val reduce_I = result();
+
+goalw Comb.thy [I_def] "I: comb";
+by (REPEAT (ares_tac comb.intrs 1));
+val comb_I = result();
+
+(** Non-contraction results **)
-J. Camilleri and T. F. Melham.
-Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
-Report 265, University of Cambridge Computer Laboratory, 1992.
-*)
+(*Derive a case for each combinator constructor*)
+val K_contractE = contract.mk_cases comb.con_defs "K -1-> r";
+val S_contractE = contract.mk_cases comb.con_defs "S -1-> r";
+val Ap_contractE = contract.mk_cases comb.con_defs "p#q -1-> r";
+
+val contract_cs =
+ ZF_cs addSIs comb.intrs
+ addIs contract.intrs
+ addSEs [contract_combD1,contract_combD2] (*type checking*)
+ addSEs [K_contractE, S_contractE, Ap_contractE]
+ addSEs comb.free_SEs;
+
+goalw Comb.thy [I_def] "!!r. I -1-> r ==> P";
+by (fast_tac contract_cs 1);
+val I_contract_E = result();
+
+goal Comb.thy "!!p r. K#p -1-> r ==> (EX q. r = K#q & p -1-> q)";
+by (fast_tac contract_cs 1);
+val K1_contractD = result();
+
+goal Comb.thy "!!p r. [| p ---> q; r: comb |] ==> p#r ---> q#r";
+by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
+by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
+by (etac rtrancl_induct 1);
+by (fast_tac (contract_cs addIs reduction_rls) 1);
+by (etac (trans_rtrancl RS transD) 1);
+by (fast_tac (contract_cs addIs reduction_rls) 1);
+val Ap_reduce1 = result();
+
+goal Comb.thy "!!p r. [| p ---> q; r: comb |] ==> r#p ---> r#q";
+by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
+by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
+by (etac rtrancl_induct 1);
+by (fast_tac (contract_cs addIs reduction_rls) 1);
+by (etac (trans_rtrancl RS transD) 1);
+by (fast_tac (contract_cs addIs reduction_rls) 1);
+val Ap_reduce2 = result();
+
+(** Counterexample to the diamond property for -1-> **)
+
+goal Comb.thy "K#I#(I#I) -1-> I";
+by (REPEAT (ares_tac [contract.K, comb_I, comb_Ap] 1));
+val KIII_contract1 = result();
+
+goalw Comb.thy [I_def] "K#I#(I#I) -1-> K#I#((K#I)#(K#I))";
+by (DEPTH_SOLVE (resolve_tac (comb.intrs @ contract.intrs) 1));
+val KIII_contract2 = result();
+
+goal Comb.thy "K#I#((K#I)#(K#I)) -1-> I";
+by (REPEAT (ares_tac (comb.intrs @ [contract.K, comb_I]) 1));
+val KIII_contract3 = result();
+
+goalw Comb.thy [diamond_def] "~ diamond(contract)";
+by (fast_tac (ZF_cs addIs [KIII_contract1,KIII_contract2,KIII_contract3]
+ addSEs [I_contract_E]) 1);
+val not_diamond_contract = result();
+
-(*Example of a datatype with mixfix syntax for some constructors*)
-structure Comb = Datatype_Fun
- (val thy = Univ.thy;
- val thy_name = "Comb";
- val rec_specs =
- [("comb", "univ(0)",
- [(["K","S"], "i", NoSyn),
- (["#"], "[i,i]=>i", Infixl 90)])];
- val rec_styp = "i";
- val sintrs =
- ["K : comb",
- "S : comb",
- "[| p: comb; q: comb |] ==> p#q : comb"];
- val monos = [];
- val type_intrs = datatype_intrs;
- val type_elims = []);
+(*** Results about Parallel Contraction ***)
+
+val parcontract_induct = standard
+ (parcontract.mutual_induct RS spec RS spec RSN (2,rev_mp));
+
+(*For type checking: replaces a=1=>b by a,b:comb *)
+val parcontract_combE2 = parcontract.dom_subset RS subsetD RS SigmaE2;
+val parcontract_combD1 = parcontract.dom_subset RS subsetD RS SigmaD1;
+val parcontract_combD2 = parcontract.dom_subset RS subsetD RS SigmaD2;
+
+goal Comb.thy "field(parcontract) = comb";
+by (fast_tac (ZF_cs addIs [equalityI, parcontract.K]
+ addSEs [parcontract_combE2]) 1);
+val field_parcontract_eq = result();
+
+(*Derive a case for each combinator constructor*)
+val K_parcontractE = parcontract.mk_cases comb.con_defs "K =1=> r";
+val S_parcontractE = parcontract.mk_cases comb.con_defs "S =1=> r";
+val Ap_parcontractE = parcontract.mk_cases comb.con_defs "p#q =1=> r";
+
+val parcontract_cs =
+ ZF_cs addSIs comb.intrs
+ addIs parcontract.intrs
+ addSEs [Ap_E, K_parcontractE, S_parcontractE,
+ Ap_parcontractE]
+ addSEs [parcontract_combD1, parcontract_combD2] (*type checking*)
+ addSEs comb.free_SEs;
+
+(*** Basic properties of parallel contraction ***)
+
+goal Comb.thy "!!p r. K#p =1=> r ==> (EX p'. r = K#p' & p =1=> p')";
+by (fast_tac parcontract_cs 1);
+val K1_parcontractD = result();
+
+goal Comb.thy "!!p r. S#p =1=> r ==> (EX p'. r = S#p' & p =1=> p')";
+by (fast_tac parcontract_cs 1);
+val S1_parcontractD = result();
+
+goal Comb.thy
+ "!!p q r. S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
+by (fast_tac (parcontract_cs addSDs [S1_parcontractD]) 1);
+val S2_parcontractD = result();
+
+(*Church-Rosser property for parallel contraction*)
+goalw Comb.thy [diamond_def] "diamond(parcontract)";
+by (rtac (impI RS allI RS allI) 1);
+by (etac parcontract_induct 1);
+by (ALLGOALS
+ (fast_tac (parcontract_cs addSDs [K1_parcontractD,S2_parcontractD])));
+val diamond_parcontract = result();
+
+(*** Transitive closure preserves the Church-Rosser property ***)
-val [K_comb,S_comb,Ap_comb] = Comb.intrs;
+goalw Comb.thy [diamond_def]
+ "!!x y r. [| diamond(r); <x,y>:r^+ |] ==> \
+\ ALL y'. <x,y'>:r --> (EX z. <y',z>: r^+ & <y,z>: r)";
+by (etac trancl_induct 1);
+by (fast_tac (ZF_cs addIs [r_into_trancl]) 1);
+by (slow_best_tac (ZF_cs addSDs [spec RS mp]
+ addIs [r_into_trancl, trans_trancl RS transD]) 1);
+val diamond_trancl_lemma = result();
+
+val diamond_lemmaE = diamond_trancl_lemma RS spec RS mp RS exE;
+
+val [major] = goal Comb.thy "diamond(r) ==> diamond(r^+)";
+bw diamond_def; (*unfold only in goal, not in premise!*)
+by (rtac (impI RS allI RS allI) 1);
+by (etac trancl_induct 1);
+by (ALLGOALS
+ (slow_best_tac (ZF_cs addIs [r_into_trancl, trans_trancl RS transD]
+ addEs [major RS diamond_lemmaE])));
+val diamond_trancl = result();
+
+
+(*** Equivalence of p--->q and p===>q ***)
+
+goal Comb.thy "!!p q. p-1->q ==> p=1=>q";
+by (etac contract_induct 1);
+by (ALLGOALS (fast_tac (parcontract_cs)));
+val contract_imp_parcontract = result();
-val Ap_E = Comb.mk_cases Comb.con_defs "p#q : comb";
+goal Comb.thy "!!p q. p--->q ==> p===>q";
+by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
+by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
+by (etac rtrancl_induct 1);
+by (fast_tac (parcontract_cs addIs [r_into_trancl]) 1);
+by (fast_tac (ZF_cs addIs [contract_imp_parcontract,
+ r_into_trancl, trans_trancl RS transD]) 1);
+val reduce_imp_parreduce = result();
+
+goal Comb.thy "!!p q. p=1=>q ==> p--->q";
+by (etac parcontract_induct 1);
+by (fast_tac (contract_cs addIs reduction_rls) 1);
+by (fast_tac (contract_cs addIs reduction_rls) 1);
+by (fast_tac (contract_cs addIs reduction_rls) 1);
+by (rtac (trans_rtrancl RS transD) 1);
+by (ALLGOALS
+ (fast_tac
+ (contract_cs addIs [Ap_reduce1, Ap_reduce2]
+ addSEs [parcontract_combD1,parcontract_combD2])));
+val parcontract_imp_reduce = result();
+
+goal Comb.thy "!!p q. p===>q ==> p--->q";
+by (forward_tac [trancl_type RS subsetD RS SigmaD1] 1);
+by (dtac (field_parcontract_eq RS equalityD1 RS subsetD) 1);
+by (etac trancl_induct 1);
+by (etac parcontract_imp_reduce 1);
+by (etac (trans_rtrancl RS transD) 1);
+by (etac parcontract_imp_reduce 1);
+val parreduce_imp_reduce = result();
+
+goal Comb.thy "p===>q <-> p--->q";
+by (REPEAT (ares_tac [iffI, parreduce_imp_reduce, reduce_imp_parreduce] 1));
+val parreduce_iff_reduce = result();
+
+writeln"Reached end of file.";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Comb.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,82 @@
+(* Title: ZF/ex/Comb.thy
+ ID: $Id$
+ Author: Lawrence C Paulson
+ Copyright 1994 University of Cambridge
+
+Combinatory Logic example: the Church-Rosser Theorem
+Curiously, combinators do not include free variables.
+
+Example taken from
+ J. Camilleri and T. F. Melham.
+ Reasoning with Inductively Defined Relations in the HOL Theorem Prover.
+ Report 265, University of Cambridge Computer Laboratory, 1992.
+*)
+
+
+Comb = Univ + "Datatype" +
+
+(** Datatype definition of combinators S and K, with infixed application **)
+consts comb :: "i"
+datatype (* <= "univ(0)" *)
+ "comb" = K
+ | S
+ | "#" ("p: comb", "q: comb") (infixl 90)
+
+(** Inductive definition of contractions, -1->
+ and (multi-step) reductions, --->
+**)
+consts
+ contract :: "i"
+ "-1->" :: "[i,i] => o" (infixl 50)
+ "--->" :: "[i,i] => o" (infixl 50)
+
+translations
+ "p -1-> q" == "<p,q> : contract"
+ "p ---> q" == "<p,q> : contract^*"
+
+inductive
+ domains "contract" <= "comb*comb"
+ intrs
+ K "[| p:comb; q:comb |] ==> K#p#q -1-> p"
+ S "[| p:comb; q:comb; r:comb |] ==> S#p#q#r -1-> (p#r)#(q#r)"
+ Ap1 "[| p-1->q; r:comb |] ==> p#r -1-> q#r"
+ Ap2 "[| p-1->q; r:comb |] ==> r#p -1-> r#q"
+ type_intrs "comb.intrs"
+
+
+(** Inductive definition of parallel contractions, =1=>
+ and (multi-step) parallel reductions, ===>
+**)
+consts
+ parcontract :: "i"
+ "=1=>" :: "[i,i] => o" (infixl 50)
+ "===>" :: "[i,i] => o" (infixl 50)
+
+translations
+ "p =1=> q" == "<p,q> : parcontract"
+ "p ===> q" == "<p,q> : parcontract^+"
+
+inductive
+ domains "parcontract" <= "comb*comb"
+ intrs
+ refl "[| p:comb |] ==> p =1=> p"
+ K "[| p:comb; q:comb |] ==> K#p#q =1=> p"
+ S "[| p:comb; q:comb; r:comb |] ==> S#p#q#r =1=> (p#r)#(q#r)"
+ Ap "[| p=1=>q; r=1=>s |] ==> p#r =1=> q#s"
+ type_intrs "comb.intrs"
+
+
+(*Misc definitions*)
+consts
+ diamond :: "i => o"
+ I :: "i"
+
+rules
+
+ diamond_def "diamond(r) == ALL x y. <x,y>:r --> \
+\ (ALL y'. <x,y'>:r --> \
+\ (EX z. <y,z>:r & <y',z> : r))"
+
+ I_def "I == S#K#K"
+
+end
--- a/src/ZF/ex/Data.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Data.ML Fri Aug 12 12:28:46 1994 +0200
@@ -1,4 +1,4 @@
-(* Title: ZF/ex/data.ML
+(* Title: ZF/ex/Data.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -7,34 +7,29 @@
It has four contructors, of arities 0-3, and two parameters A and B.
*)
-structure Data = Datatype_Fun
- (val thy = Univ.thy
- val thy_name = "Data"
- val rec_specs = [("data", "univ(A Un B)",
- [(["Con0"], "i", NoSyn),
- (["Con1"], "i=>i", NoSyn),
- (["Con2"], "[i,i]=>i", NoSyn),
- (["Con3"], "[i,i,i]=>i", NoSyn)])]
- val rec_styp = "[i,i]=>i"
- val sintrs =
- ["Con0 : data(A,B)",
- "[| a: A |] ==> Con1(a) : data(A,B)",
- "[| a: A; b: B |] ==> Con2(a,b) : data(A,B)",
- "[| a: A; b: B; d: data(A,B) |] ==> Con3(a,b,d) : data(A,B)"]
- val monos = []
- val type_intrs = datatype_intrs
- val type_elims = datatype_elims);
+open Data;
+goal Data.thy "data(A,B) = ({0} + A) + (A*B + A*B*data(A,B))";
+by (rtac (data.unfold RS trans) 1);
+bws data.con_defs;
+br equalityI 1;
+by (fast_tac sum_cs 1);
+(*for this direction, fast_tac is just too slow!*)
+by (safe_tac sum_cs);
+by (REPEAT_FIRST (swap_res_tac [refl, conjI, disjCI, exI]));
+by (REPEAT (fast_tac (sum_cs addIs datatype_intrs
+ addDs [data.dom_subset RS subsetD]) 1));
+val data_unfold = result();
(** Lemmas to justify using "data" in other recursive type definitions **)
-goalw Data.thy Data.defs "!!A B. [| A<=C; B<=D |] ==> data(A,B) <= data(C,D)";
+goalw Data.thy data.defs "!!A B. [| A<=C; B<=D |] ==> data(A,B) <= data(C,D)";
by (rtac lfp_mono 1);
-by (REPEAT (rtac Data.bnd_mono 1));
+by (REPEAT (rtac data.bnd_mono 1));
by (REPEAT (ares_tac (univ_mono::Un_mono::basic_monos) 1));
val data_mono = result();
-goalw Data.thy (Data.defs@Data.con_defs) "data(univ(A),univ(A)) <= univ(A)";
+goalw Data.thy (data.defs@data.con_defs) "data(univ(A),univ(A)) <= univ(A)";
by (rtac lfp_lowerbound 1);
by (rtac ([A_subset_univ, Un_upper1] MRS subset_trans RS univ_mono) 2);
by (fast_tac (ZF_cs addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Data.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,21 @@
+(* Title: ZF/ex/Data.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Sample datatype definition.
+It has four contructors, of arities 0-3, and two parameters A and B.
+*)
+
+Data = Univ +
+
+consts
+ data :: "[i,i] => i"
+
+datatype
+ "data(A,B)" = Con0
+ | Con1 ("a: A")
+ | Con2 ("a: A", "b: B")
+ | Con3 ("a: A", "b: B", "d: data(A,B)")
+
+end
--- a/src/ZF/ex/Enum.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Enum.ML Fri Aug 12 12:28:46 1994 +0200
@@ -1,4 +1,4 @@
-(* Title: ZF/ex/enum
+(* Title: ZF/ex/Enum
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -8,26 +8,9 @@
Can go up to at least 100 constructors, but it takes nearly 7 minutes...
*)
-
-(*An enumeration type with 60 contructors! -- takes about 150 seconds!*)
-fun mk_ids a 0 = []
- | mk_ids a n = a :: mk_ids (bump_string a) (n-1);
-
-val consts = mk_ids "con1" 60;
+open Enum;
-structure Enum = Datatype_Fun
- (val thy = Univ.thy;
- val thy_name = "Enum";
- val rec_specs =
- [("enum", "univ(0)",
- [(consts, "i", NoSyn)])];
- val rec_styp = "i";
- val sintrs = map (fn const => const ^ " : enum") consts;
- val monos = [];
- val type_intrs = datatype_intrs
- val type_elims = []);
-
-goal Enum.thy "con59 ~= con60";
-by (simp_tac (ZF_ss addsimps Enum.free_iffs) 1);
+goal Enum.thy "C00 ~= C01";
+by (simp_tac (ZF_ss addsimps enum.free_iffs) 1);
result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Enum.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,24 @@
+(* Title: ZF/ex/Enum
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1993 University of Cambridge
+
+Example of a BIG enumeration type
+
+Can go up to at least 100 constructors, but it takes nearly 7 minutes...
+*)
+
+Enum = Univ + "Datatype" +
+
+consts
+ enum :: "i"
+
+datatype
+ "enum" = C00 | C01 | C02 | C03 | C04 | C05 | C06 | C07 | C08 | C09
+ | C10 | C11 | C12 | C13 | C14 | C15 | C16 | C17 | C18 | C19
+ | C20 | C21 | C22 | C23 | C24 | C25 | C26 | C27 | C28 | C29
+ | C30 | C31 | C32 | C33 | C34 | C35 | C36 | C37 | C38 | C39
+ | C40 | C41 | C42 | C43 | C44 | C45 | C46 | C47 | C48 | C49
+ | C50 | C51 | C52 | C53 | C54 | C55 | C56 | C57 | C58 | C59
+
+end
--- a/src/ZF/ex/Equiv.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Equiv.ML Fri Aug 12 12:28:46 1994 +0200
@@ -46,14 +46,15 @@
(** Equivalence classes **)
(*Lemma for the next result*)
-goalw Equiv.thy [equiv_def,trans_def,sym_def]
- "!!A r. [| equiv(A,r); <a,b>: r |] ==> r``{a} <= r``{b}";
+goalw Equiv.thy [trans_def,sym_def]
+ "!!A r. [| sym(r); trans(r); <a,b>: r |] ==> r``{a} <= r``{b}";
by (fast_tac ZF_cs 1);
val equiv_class_subset = result();
-goal Equiv.thy "!!A r. [| equiv(A,r); <a,b>: r |] ==> r``{a} = r``{b}";
-by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
-by (rewrite_goals_tac [equiv_def,sym_def]);
+goalw Equiv.thy [equiv_def]
+ "!!A r. [| equiv(A,r); <a,b>: r |] ==> r``{a} = r``{b}";
+by (safe_tac (subset_cs addSIs [equalityI, equiv_class_subset]));
+by (rewrite_goals_tac [sym_def]);
by (fast_tac ZF_cs 1);
val equiv_class_eq = result();
--- a/src/ZF/ex/LList.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/LList.ML Fri Aug 12 12:28:46 1994 +0200
@@ -1,47 +1,35 @@
-(* Title: ZF/ex/llist.ML
+(* Title: ZF/ex/LList.ML
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
+ Copyright 1994 University of Cambridge
Codatatype definition of Lazy Lists
*)
-structure LList = CoDatatype_Fun
- (val thy = QUniv.thy
- val thy_name = "LList"
- val rec_specs = [("llist", "quniv(A)",
- [(["LNil"], "i", NoSyn),
- (["LCons"], "[i,i]=>i", NoSyn)])]
- val rec_styp = "i=>i"
- val sintrs = ["LNil : llist(A)",
- "[| a: A; l: llist(A) |] ==> LCons(a,l) : llist(A)"]
- val monos = []
- val type_intrs = codatatype_intrs
- val type_elims = codatatype_elims);
-
-val [LNilI, LConsI] = LList.intrs;
+open LList;
(*An elimination rule, for type-checking*)
-val LConsE = LList.mk_cases LList.con_defs "LCons(a,l) : llist(A)";
+val LConsE = llist.mk_cases llist.con_defs "LCons(a,l) : llist(A)";
(*Proving freeness results*)
-val LCons_iff = LList.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'";
-val LNil_LCons_iff = LList.mk_free "~ LNil=LCons(a,l)";
+val LCons_iff = llist.mk_free "LCons(a,l)=LCons(a',l') <-> a=a' & l=l'";
+val LNil_LCons_iff = llist.mk_free "~ LNil=LCons(a,l)";
goal LList.thy "llist(A) = {0} <+> (A <*> llist(A))";
-by (rtac (LList.unfold RS trans) 1);
-bws LList.con_defs;
-by (fast_tac (qsum_cs addIs ([equalityI] @ codatatype_intrs)
- addDs [LList.dom_subset RS subsetD]
- addEs [A_into_quniv]
- addSEs [QSigmaE]) 1);
+by (rtac (llist.unfold RS trans) 1);
+bws llist.con_defs;
+br equalityI 1;
+by (fast_tac qsum_cs 1);
+by (fast_tac (qsum_cs addIs codatatype_intrs
+ addDs [llist.dom_subset RS subsetD]
+ addSEs [QSigmaE]) 1);
val llist_unfold = result();
(*** Lemmas to justify using "llist" in other recursive type definitions ***)
-goalw LList.thy LList.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
+goalw LList.thy llist.defs "!!A B. A<=B ==> llist(A) <= llist(B)";
by (rtac gfp_mono 1);
-by (REPEAT (rtac LList.bnd_mono 1));
+by (REPEAT (rtac llist.bnd_mono 1));
by (REPEAT (ares_tac (quniv_mono::basic_monos) 1));
val llist_mono = result();
@@ -58,8 +46,8 @@
"!!i. Ord(i) ==> ALL l: llist(quniv(A)). l Int Vset(i) <= univ(eclose(A))";
by (etac trans_induct 1);
by (rtac ballI 1);
-by (etac LList.elim 1);
-by (rewrite_goals_tac ([QInl_def,QInr_def]@LList.con_defs));
+by (etac llist.elim 1);
+by (rewrite_goals_tac ([QInl_def,QInr_def]@llist.con_defs));
(*LNil case*)
by (fast_tac quniv_cs 1);
(*LCons case*)
@@ -76,5 +64,140 @@
val llist_subset_quniv = standard
(llist_mono RS (llist_quniv RSN (2,subset_trans)));
-(* Definition and use of LList_Eq has been moved to llist_eq.ML to allow
- automatic association between theory name and filename. *)
+
+(*** Lazy List Equality: lleq ***)
+
+val lleq_cs = subset_cs
+ addSIs [QPair_Int_Vset_subset_UN RS subset_trans, QPair_mono]
+ addSEs [Ord_in_Ord, Pair_inject];
+
+(*Lemma for proving finality. Unfold the lazy list; use induction hypothesis*)
+goal LList.thy
+ "!!i. Ord(i) ==> ALL l l'. <l,l'> : lleq(A) --> l Int Vset(i) <= l'";
+by (etac trans_induct 1);
+by (REPEAT (resolve_tac [allI, impI] 1));
+by (etac lleq.elim 1);
+by (rewrite_goals_tac (QInr_def::llist.con_defs));
+by (safe_tac lleq_cs);
+by (fast_tac (subset_cs addSEs [Ord_trans, make_elim bspec]) 1);
+val lleq_Int_Vset_subset_lemma = result();
+
+val lleq_Int_Vset_subset = standard
+ (lleq_Int_Vset_subset_lemma RS spec RS spec RS mp);
+
+
+(*lleq(A) is a symmetric relation because qconverse(lleq(A)) is a fixedpoint*)
+val [prem] = goal LList.thy "<l,l'> : lleq(A) ==> <l',l> : lleq(A)";
+by (rtac (prem RS converseI RS lleq.coinduct) 1);
+by (rtac (lleq.dom_subset RS converse_type) 1);
+by (safe_tac converse_cs);
+by (etac lleq.elim 1);
+by (ALLGOALS (fast_tac qconverse_cs));
+val lleq_symmetric = result();
+
+goal LList.thy "!!l l'. <l,l'> : lleq(A) ==> l=l'";
+by (rtac equalityI 1);
+by (REPEAT (ares_tac [lleq_Int_Vset_subset RS Int_Vset_subset] 1
+ ORELSE etac lleq_symmetric 1));
+val lleq_implies_equal = result();
+
+val [eqprem,lprem] = goal LList.thy
+ "[| l=l'; l: llist(A) |] ==> <l,l'> : lleq(A)";
+by (res_inst_tac [("X", "{<l,l>. l: llist(A)}")] lleq.coinduct 1);
+by (rtac (lprem RS RepFunI RS (eqprem RS subst)) 1);
+by (safe_tac qpair_cs);
+by (etac llist.elim 1);
+by (ALLGOALS (fast_tac pair_cs));
+val equal_llist_implies_leq = result();
+
+
+(*** Lazy List Functions ***)
+
+(*Examples of coinduction for type-checking and to prove llist equations*)
+
+(*** lconst -- defined directly using lfp, but equivalent to a LList_corec ***)
+
+goalw LList.thy llist.con_defs "bnd_mono(univ(a), %l. LCons(a,l))";
+by (rtac bnd_monoI 1);
+by (REPEAT (ares_tac [subset_refl, QInr_mono, QPair_mono] 2));
+by (REPEAT (ares_tac [subset_refl, A_subset_univ,
+ QInr_subset_univ, QPair_subset_univ] 1));
+val lconst_fun_bnd_mono = result();
+
+(* lconst(a) = LCons(a,lconst(a)) *)
+val lconst = standard
+ ([lconst_def, lconst_fun_bnd_mono] MRS def_lfp_Tarski);
+
+val lconst_subset = lconst_def RS def_lfp_subset;
+
+val member_subset_Union_eclose = standard (arg_into_eclose RS Union_upper);
+
+goal LList.thy "!!a A. a : A ==> lconst(a) : quniv(A)";
+by (rtac (lconst_subset RS subset_trans RS qunivI) 1);
+by (etac (arg_into_eclose RS eclose_subset RS univ_mono) 1);
+val lconst_in_quniv = result();
+
+goal LList.thy "!!a A. a:A ==> lconst(a): llist(A)";
+by (rtac (singletonI RS llist.coinduct) 1);
+by (fast_tac (ZF_cs addSIs [lconst_in_quniv]) 1);
+by (fast_tac (ZF_cs addSIs [lconst]) 1);
+val lconst_type = result();
+
+(*** flip --- equations merely assumed; certain consequences proved ***)
+
+val flip_ss = ZF_ss addsimps [flip_LNil, flip_LCons, not_type];
+
+goal QUniv.thy "!!b. b:bool ==> b Int X <= univ(eclose(A))";
+by (fast_tac (quniv_cs addSEs [boolE]) 1);
+val bool_Int_subset_univ = result();
+
+val flip_cs = quniv_cs addSIs [not_type]
+ addIs [bool_Int_subset_univ];
+
+(*Reasoning borrowed from lleq.ML; a similar proof works for all
+ "productive" functions -- cf Coquand's "Infinite Objects in Type Theory".*)
+goal LList.thy
+ "!!i. Ord(i) ==> ALL l: llist(bool). flip(l) Int Vset(i) <= \
+\ univ(eclose(bool))";
+by (etac trans_induct 1);
+by (rtac ballI 1);
+by (etac llist.elim 1);
+by (asm_simp_tac flip_ss 1);
+by (asm_simp_tac flip_ss 2);
+by (rewrite_goals_tac ([QInl_def,QInr_def]@llist.con_defs));
+(*LNil case*)
+by (fast_tac flip_cs 1);
+(*LCons case*)
+by (safe_tac flip_cs);
+by (ALLGOALS (fast_tac (flip_cs addSEs [Ord_trans, make_elim bspec])));
+val flip_llist_quniv_lemma = result();
+
+goal LList.thy "!!l. l: llist(bool) ==> flip(l) : quniv(bool)";
+by (rtac (flip_llist_quniv_lemma RS bspec RS Int_Vset_subset RS qunivI) 1);
+by (REPEAT (assume_tac 1));
+val flip_in_quniv = result();
+
+val [prem] = goal LList.thy "l : llist(bool) ==> flip(l): llist(bool)";
+by (res_inst_tac [("X", "{flip(l) . l:llist(bool)}")]
+ llist.coinduct 1);
+by (rtac (prem RS RepFunI) 1);
+by (fast_tac (ZF_cs addSIs [flip_in_quniv]) 1);
+by (etac RepFunE 1);
+by (etac llist.elim 1);
+by (asm_simp_tac flip_ss 1);
+by (asm_simp_tac flip_ss 1);
+by (fast_tac (ZF_cs addSIs [not_type]) 1);
+val flip_type = result();
+
+val [prem] = goal LList.thy
+ "l : llist(bool) ==> flip(flip(l)) = l";
+by (res_inst_tac [("X1", "{<flip(flip(l)),l> . l:llist(bool)}")]
+ (lleq.coinduct RS lleq_implies_equal) 1);
+by (rtac (prem RS RepFunI) 1);
+by (fast_tac (ZF_cs addSIs [flip_type]) 1);
+by (etac RepFunE 1);
+by (etac llist.elim 1);
+by (asm_simp_tac flip_ss 1);
+by (asm_simp_tac (flip_ss addsimps [flip_type, not_not]) 1);
+by (fast_tac (ZF_cs addSIs [not_type]) 1);
+val flip_flip = result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/LList.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,55 @@
+(* Title: ZF/ex/LList.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Codatatype definition of Lazy Lists
+
+Equality for llist(A) as a greatest fixed point
+
+Functions for Lazy Lists
+
+STILL NEEDS:
+co_recursion for defining lconst, flip, etc.
+a typing rule for it, based on some notion of "productivity..."
+*)
+
+LList = QUniv + "Datatype" +
+
+consts
+ llist :: "i=>i"
+
+codatatype
+ "llist(A)" = LNil | LCons ("a: A", "l: llist(A)")
+
+
+(*Coinductive definition of equality*)
+consts
+ lleq :: "i=>i"
+
+(*Previously used <*> in the domain and variant pairs as elements. But
+ standard pairs work just as well. To use variant pairs, must change prefix
+ a q/Q to the Sigma, Pair and converse rules.*)
+coinductive
+ domains "lleq(A)" <= "llist(A) * llist(A)"
+ intrs
+ LNil "<LNil, LNil> : lleq(A)"
+ LCons "[| a:A; <l,l'>: lleq(A) |] ==> <LCons(a,l), LCons(a,l')>: lleq(A)"
+ type_intrs "llist.intrs"
+
+
+(*Lazy list functions; flip is not definitional!*)
+consts
+ lconst :: "i => i"
+ flip :: "i => i"
+
+rules
+ lconst_def "lconst(a) == lfp(univ(a), %l. LCons(a,l))"
+
+ flip_LNil "flip(LNil) = LNil"
+
+ flip_LCons "[| x:bool; l: llist(bool) |] ==> \
+\ flip(LCons(x,l)) = LCons(not(x), flip(l))"
+
+end
+
--- a/src/ZF/ex/ListN.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/ListN.ML Fri Aug 12 12:28:46 1994 +0200
@@ -9,25 +9,15 @@
Research Report 92-49, LIP, ENS Lyon. Dec 1992.
*)
-structure ListN = Inductive_Fun
- (val thy = ListFn.thy |> add_consts [("listn","i=>i",NoSyn)]
- val thy_name = "ListN"
- val rec_doms = [("listn", "nat*list(A)")]
- val sintrs =
- ["<0,Nil> : listn(A)",
- "[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"]
- val monos = []
- val con_defs = []
- val type_intrs = nat_typechecks @ List.intrs
- val type_elims = []);
+open ListN;
val listn_induct = standard
- (ListN.mutual_induct RS spec RS spec RSN (2,rev_mp));
+ (listn.mutual_induct RS spec RS spec RSN (2,rev_mp));
goal ListN.thy "!!l. l:list(A) ==> <length(l),l> : listn(A)";
-by (etac List.induct 1);
+by (etac list.induct 1);
by (ALLGOALS (asm_simp_tac list_ss));
-by (REPEAT (ares_tac ListN.intrs 1));
+by (REPEAT (ares_tac listn.intrs 1));
val list_into_listn = result();
goal ListN.thy "<n,l> : listn(A) <-> l:list(A) & length(l)=n";
@@ -42,9 +32,9 @@
by (simp_tac (list_ss addsimps [listn_iff,separation,image_singleton_iff]) 1);
val listn_image_eq = result();
-goalw ListN.thy ListN.defs "!!A B. A<=B ==> listn(A) <= listn(B)";
+goalw ListN.thy listn.defs "!!A B. A<=B ==> listn(A) <= listn(B)";
by (rtac lfp_mono 1);
-by (REPEAT (rtac ListN.bnd_mono 1));
+by (REPEAT (rtac listn.bnd_mono 1));
by (REPEAT (ares_tac ([univ_mono,Sigma_mono,list_mono] @ basic_monos) 1));
val listn_mono = result();
@@ -52,11 +42,11 @@
"!!n l. [| <n,l> : listn(A); <n',l'> : listn(A) |] ==> \
\ <n#+n', l@l'> : listn(A)";
by (etac listn_induct 1);
-by (ALLGOALS (asm_simp_tac (list_ss addsimps ListN.intrs)));
+by (ALLGOALS (asm_simp_tac (list_ss addsimps listn.intrs)));
val listn_append = result();
-val Nil_listn_case = ListN.mk_cases List.con_defs "<i,Nil> : listn(A)"
-and Cons_listn_case = ListN.mk_cases List.con_defs "<i,Cons(x,l)> : listn(A)";
+val Nil_listn_case = listn.mk_cases list.con_defs "<i,Nil> : listn(A)"
+and Cons_listn_case = listn.mk_cases list.con_defs "<i,Cons(x,l)> : listn(A)";
-val zero_listn_case = ListN.mk_cases List.con_defs "<0,l> : listn(A)"
-and succ_listn_case = ListN.mk_cases List.con_defs "<succ(i),l> : listn(A)";
+val zero_listn_case = listn.mk_cases list.con_defs "<0,l> : listn(A)"
+and succ_listn_case = listn.mk_cases list.con_defs "<succ(i),l> : listn(A)";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/ListN.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,20 @@
+(* Title: ZF/ex/ListN
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Inductive definition of lists of n elements
+
+See Ch. Paulin-Mohring, Inductive Definitions in the System Coq.
+Research Report 92-49, LIP, ENS Lyon. Dec 1992.
+*)
+
+ListN = List +
+consts listn ::"i=>i"
+inductive
+ domains "listn(A)" <= "nat*list(A)"
+ intrs
+ NilI "<0,Nil> : listn(A)"
+ ConsI "[| a: A; <n,l> : listn(A) |] ==> <succ(n), Cons(a,l)> : listn(A)"
+ type_intrs "nat_typechecks @ list.intrs"
+end
--- a/src/ZF/ex/Ntree.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Ntree.ML Fri Aug 12 12:28:46 1994 +0200
@@ -9,27 +9,16 @@
Based upon ex/Term.ML
*)
-structure Ntree = Datatype_Fun
- (val thy = Univ.thy;
- val thy_name = "Ntree";
- val rec_specs =
- [("ntree", "univ(A)",
- [(["Branch"], "[i,i]=>i", NoSyn)])];
- val rec_styp = "i=>i";
- val sintrs =
- ["[| a: A; n: nat; h: n -> ntree(A) |] ==> Branch(a,h) : ntree(A)"];
- val monos = [Pi_mono];
- val type_intrs = (nat_fun_univ RS subsetD) :: datatype_intrs;
- val type_elims = []);
-
-val [BranchI] = Ntree.intrs;
+open Ntree;
goal Ntree.thy "ntree(A) = A * (UN n: nat. n -> ntree(A))";
-by (rtac (Ntree.unfold RS trans) 1);
-bws Ntree.con_defs;
-by (fast_tac (sum_cs addIs ([equalityI] @ datatype_intrs)
- addDs [Ntree.dom_subset RS subsetD]
- addEs [A_into_univ, nat_fun_into_univ]) 1);
+by (rtac (ntree.unfold RS trans) 1);
+bws ntree.con_defs;
+br equalityI 1;
+by (fast_tac sum_cs 1);
+by (fast_tac (sum_cs addIs datatype_intrs
+ addDs [ntree.dom_subset RS subsetD]
+ addEs [nat_fun_into_univ]) 1);
val ntree_unfold = result();
(*A nicer induction rule than the standard one*)
@@ -38,7 +27,8 @@
\ !!x n h. [| x: A; n: nat; h: n -> ntree(A); ALL i:n. P(h`i) \
\ |] ==> P(Branch(x,h)) \
\ |] ==> P(t)";
-by (rtac (major RS Ntree.induct) 1);
+by (rtac (major RS ntree.induct) 1);
+by (etac UN_E 1);
by (REPEAT_SOME (ares_tac prems));
by (fast_tac (ZF_cs addEs [fun_weaken_type]) 1);
by (fast_tac (ZF_cs addDs [apply_type]) 1);
@@ -60,14 +50,14 @@
(** Lemmas to justify using "Ntree" in other recursive type definitions **)
-goalw Ntree.thy Ntree.defs "!!A B. A<=B ==> ntree(A) <= ntree(B)";
+goalw Ntree.thy ntree.defs "!!A B. A<=B ==> ntree(A) <= ntree(B)";
by (rtac lfp_mono 1);
-by (REPEAT (rtac Ntree.bnd_mono 1));
+by (REPEAT (rtac ntree.bnd_mono 1));
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
val ntree_mono = result();
(*Easily provable by induction also*)
-goalw Ntree.thy (Ntree.defs@Ntree.con_defs) "ntree(univ(A)) <= univ(A)";
+goalw Ntree.thy (ntree.defs@ntree.con_defs) "ntree(univ(A)) <= univ(A)";
by (rtac lfp_lowerbound 1);
by (rtac (A_subset_univ RS univ_mono) 2);
by (safe_tac ZF_cs);
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Ntree.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,23 @@
+(* Title: ZF/ex/Ntree.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Datatype definition n-ary branching trees
+Demonstrates a simple use of function space in a datatype definition
+ and also "nested" monotonicity theorems
+
+Based upon ex/Term.thy
+*)
+
+Ntree = InfDatatype +
+consts
+ ntree :: "i=>i"
+
+datatype
+ "ntree(A)" = Branch ("a: A", "h: (UN n:nat. n -> ntree(A))")
+ monos "[[subset_refl, Pi_mono] MRS UN_mono]"
+ type_intrs "[nat_fun_univ RS subsetD]"
+ type_elims "[UN_E]"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Primrec.ML Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,379 @@
+(* Title: ZF/ex/Primrec
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Primitive Recursive Functions
+
+Proof adopted from
+Nora Szasz,
+A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
+In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
+
+See also E. Mendelson, Introduction to Mathematical Logic.
+(Van Nostrand, 1964), page 250, exercise 11.
+*)
+
+open Primrec;
+
+val pr_typechecks =
+ nat_typechecks @ list.intrs @
+ [lam_type, list_case_type, drop_type, map_type, apply_type, rec_type];
+
+(** Useful special cases of evaluation ***)
+
+val pr_ss = arith_ss
+ addsimps list.case_eqns
+ addsimps [list_rec_Nil, list_rec_Cons,
+ drop_0, drop_Nil, drop_succ_Cons,
+ map_Nil, map_Cons]
+ setsolver (type_auto_tac pr_typechecks);
+
+goalw Primrec.thy [SC_def]
+ "!!x l. [| x:nat; l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
+by (asm_simp_tac pr_ss 1);
+val SC = result();
+
+goalw Primrec.thy [CONST_def]
+ "!!l. [| l: list(nat) |] ==> CONST(k) ` l = k";
+by (asm_simp_tac pr_ss 1);
+val CONST = result();
+
+goalw Primrec.thy [PROJ_def]
+ "!!l. [| x: nat; l: list(nat) |] ==> PROJ(0) ` (Cons(x,l)) = x";
+by (asm_simp_tac pr_ss 1);
+val PROJ_0 = result();
+
+goalw Primrec.thy [COMP_def]
+ "!!l. [| l: list(nat) |] ==> COMP(g,[f]) ` l = g` [f`l]";
+by (asm_simp_tac pr_ss 1);
+val COMP_1 = result();
+
+goalw Primrec.thy [PREC_def]
+ "!!l. l: list(nat) ==> PREC(f,g) ` (Cons(0,l)) = f`l";
+by (asm_simp_tac pr_ss 1);
+val PREC_0 = result();
+
+goalw Primrec.thy [PREC_def]
+ "!!l. [| x:nat; l: list(nat) |] ==> \
+\ PREC(f,g) ` (Cons(succ(x),l)) = \
+\ g ` Cons(PREC(f,g)`(Cons(x,l)), Cons(x,l))";
+by (asm_simp_tac pr_ss 1);
+val PREC_succ = result();
+
+(*** Inductive definition of the PR functions ***)
+
+(* c: primrec ==> c: list(nat) -> nat *)
+val primrec_into_fun = primrec.dom_subset RS subsetD;
+
+val pr_ss = pr_ss
+ setsolver (type_auto_tac ([primrec_into_fun] @
+ pr_typechecks @ primrec.intrs));
+
+goalw Primrec.thy [ACK_def] "!!i. i:nat ==> ACK(i): primrec";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac pr_ss));
+val ACK_in_primrec = result();
+
+val ack_typechecks =
+ [ACK_in_primrec, primrec_into_fun RS apply_type,
+ add_type, list_add_type, nat_into_Ord] @
+ nat_typechecks @ list.intrs @ primrec.intrs;
+
+(*strict typechecking for the Ackermann proof; instantiates no vars*)
+fun tc_tac rls =
+ REPEAT
+ (SOMEGOAL (test_assume_tac ORELSE' match_tac (rls @ ack_typechecks)));
+
+goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j): nat";
+by (tc_tac []);
+val ack_type = result();
+
+(** Ackermann's function cases **)
+
+(*PROPERTY A 1*)
+goalw Primrec.thy [ACK_def] "!!j. j:nat ==> ack(0,j) = succ(j)";
+by (asm_simp_tac (pr_ss addsimps [SC]) 1);
+val ack_0 = result();
+
+(*PROPERTY A 2*)
+goalw Primrec.thy [ACK_def] "ack(succ(i), 0) = ack(i,1)";
+by (asm_simp_tac (pr_ss addsimps [CONST,PREC_0]) 1);
+val ack_succ_0 = result();
+
+(*PROPERTY A 3*)
+(*Could be proved in Primrec0, like the previous two cases, but using
+ primrec_into_fun makes type-checking easier!*)
+goalw Primrec.thy [ACK_def]
+ "!!i j. [| i:nat; j:nat |] ==> \
+\ ack(succ(i), succ(j)) = ack(i, ack(succ(i), j))";
+by (asm_simp_tac (pr_ss addsimps [CONST,PREC_succ,COMP_1,PROJ_0]) 1);
+val ack_succ_succ = result();
+
+val ack_ss =
+ pr_ss addsimps [ack_0, ack_succ_0, ack_succ_succ,
+ ack_type, nat_into_Ord];
+
+(*PROPERTY A 4*)
+goal Primrec.thy "!!i. i:nat ==> ALL j:nat. j < ack(i,j)";
+by (etac nat_induct 1);
+by (asm_simp_tac ack_ss 1);
+by (rtac ballI 1);
+by (eres_inst_tac [("n","j")] nat_induct 1);
+by (DO_GOAL [rtac (nat_0I RS nat_0_le RS lt_trans),
+ asm_simp_tac ack_ss] 1);
+by (DO_GOAL [etac (succ_leI RS lt_trans1),
+ asm_simp_tac ack_ss] 1);
+val lt_ack2_lemma = result();
+val lt_ack2 = standard (lt_ack2_lemma RS bspec);
+
+(*PROPERTY A 5-, the single-step lemma*)
+goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) < ack(i, succ(j))";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac (ack_ss addsimps [lt_ack2])));
+val ack_lt_ack_succ2 = result();
+
+(*PROPERTY A 5, monotonicity for < *)
+goal Primrec.thy "!!i j k. [| j<k; i:nat; k:nat |] ==> ack(i,j) < ack(i,k)";
+by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
+by (etac succ_lt_induct 1);
+by (assume_tac 1);
+by (rtac lt_trans 2);
+by (REPEAT (ares_tac ([ack_lt_ack_succ2, ack_type] @ pr_typechecks) 1));
+val ack_lt_mono2 = result();
+
+(*PROPERTY A 5', monotonicity for le *)
+goal Primrec.thy
+ "!!i j k. [| j le k; i: nat; k:nat |] ==> ack(i,j) le ack(i,k)";
+by (res_inst_tac [("f", "%j.ack(i,j)")] Ord_lt_mono_imp_le_mono 1);
+by (REPEAT (ares_tac [ack_lt_mono2, ack_type RS nat_into_Ord] 1));
+val ack_le_mono2 = result();
+
+(*PROPERTY A 6*)
+goal Primrec.thy
+ "!!i j. [| i:nat; j:nat |] ==> ack(i, succ(j)) le ack(succ(i), j)";
+by (nat_ind_tac "j" [] 1);
+by (ALLGOALS (asm_simp_tac ack_ss));
+by (rtac ack_le_mono2 1);
+by (rtac (lt_ack2 RS succ_leI RS le_trans) 1);
+by (REPEAT (ares_tac (ack_typechecks) 1));
+val ack2_le_ack1 = result();
+
+(*PROPERTY A 7-, the single-step lemma*)
+goal Primrec.thy "!!i j. [| i:nat; j:nat |] ==> ack(i,j) < ack(succ(i),j)";
+by (rtac (ack_lt_mono2 RS lt_trans2) 1);
+by (rtac ack2_le_ack1 4);
+by (REPEAT (ares_tac ([nat_le_refl, ack_type] @ pr_typechecks) 1));
+val ack_lt_ack_succ1 = result();
+
+(*PROPERTY A 7, monotonicity for < *)
+goal Primrec.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> ack(i,k) < ack(j,k)";
+by (forward_tac [lt_nat_in_nat] 1 THEN assume_tac 1);
+by (etac succ_lt_induct 1);
+by (assume_tac 1);
+by (rtac lt_trans 2);
+by (REPEAT (ares_tac ([ack_lt_ack_succ1, ack_type] @ pr_typechecks) 1));
+val ack_lt_mono1 = result();
+
+(*PROPERTY A 7', monotonicity for le *)
+goal Primrec.thy
+ "!!i j k. [| i le j; j:nat; k:nat |] ==> ack(i,k) le ack(j,k)";
+by (res_inst_tac [("f", "%j.ack(j,k)")] Ord_lt_mono_imp_le_mono 1);
+by (REPEAT (ares_tac [ack_lt_mono1, ack_type RS nat_into_Ord] 1));
+val ack_le_mono1 = result();
+
+(*PROPERTY A 8*)
+goal Primrec.thy "!!j. j:nat ==> ack(1,j) = succ(succ(j))";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac ack_ss));
+val ack_1 = result();
+
+(*PROPERTY A 9*)
+goal Primrec.thy "!!j. j:nat ==> ack(succ(1),j) = succ(succ(succ(j#+j)))";
+by (etac nat_induct 1);
+by (ALLGOALS (asm_simp_tac (ack_ss addsimps [ack_1, add_succ_right])));
+val ack_2 = result();
+
+(*PROPERTY A 10*)
+goal Primrec.thy
+ "!!i1 i2 j. [| i1:nat; i2:nat; j:nat |] ==> \
+\ ack(i1, ack(i2,j)) < ack(succ(succ(i1#+i2)), j)";
+by (rtac (ack2_le_ack1 RSN (2,lt_trans2)) 1);
+by (asm_simp_tac ack_ss 1);
+by (rtac (add_le_self RS ack_le_mono1 RS lt_trans1) 1);
+by (rtac (add_le_self2 RS ack_lt_mono1 RS ack_lt_mono2) 5);
+by (tc_tac []);
+val ack_nest_bound = result();
+
+(*PROPERTY A 11*)
+goal Primrec.thy
+ "!!i1 i2 j. [| i1:nat; i2:nat; j:nat |] ==> \
+\ ack(i1,j) #+ ack(i2,j) < ack(succ(succ(succ(succ(i1#+i2)))), j)";
+by (res_inst_tac [("j", "ack(succ(1), ack(i1 #+ i2, j))")] lt_trans 1);
+by (asm_simp_tac (ack_ss addsimps [ack_2]) 1);
+by (rtac (ack_nest_bound RS lt_trans2) 2);
+by (asm_simp_tac ack_ss 5);
+by (rtac (add_le_mono RS leI RS leI) 1);
+by (REPEAT (ares_tac ([add_le_self, add_le_self2, ack_le_mono1] @
+ ack_typechecks) 1));
+val ack_add_bound = result();
+
+(*PROPERTY A 12. Article uses existential quantifier but the ALF proof
+ used k#+4. Quantified version must be nested EX k'. ALL i,j... *)
+goal Primrec.thy
+ "!!i j k. [| i < ack(k,j); j:nat; k:nat |] ==> \
+\ i#+j < ack(succ(succ(succ(succ(k)))), j)";
+by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1);
+by (rtac (ack_add_bound RS lt_trans2) 2);
+by (asm_simp_tac (ack_ss addsimps [add_0_right]) 5);
+by (REPEAT (ares_tac ([add_lt_mono, lt_ack2] @ ack_typechecks) 1));
+val ack_add_bound2 = result();
+
+(*** MAIN RESULT ***)
+
+val ack2_ss =
+ ack_ss addsimps [list_add_Nil, list_add_Cons, list_add_type, nat_into_Ord];
+
+goalw Primrec.thy [SC_def]
+ "!!l. l: list(nat) ==> SC ` l < ack(1, list_add(l))";
+by (etac list.elim 1);
+by (asm_simp_tac (ack2_ss addsimps [succ_iff]) 1);
+by (asm_simp_tac (ack2_ss addsimps [ack_1, add_le_self]) 1);
+val SC_case = result();
+
+(*PROPERTY A 4'? Extra lemma needed for CONST case, constant functions*)
+goal Primrec.thy "!!j. [| i:nat; j:nat |] ==> i < ack(i,j)";
+by (etac nat_induct 1);
+by (asm_simp_tac (ack_ss addsimps [nat_0_le]) 1);
+by (etac ([succ_leI, ack_lt_ack_succ1] MRS lt_trans1) 1);
+by (tc_tac []);
+val lt_ack1 = result();
+
+goalw Primrec.thy [CONST_def]
+ "!!l. [| l: list(nat); k: nat |] ==> CONST(k) ` l < ack(k, list_add(l))";
+by (asm_simp_tac (ack2_ss addsimps [lt_ack1]) 1);
+val CONST_case = result();
+
+goalw Primrec.thy [PROJ_def]
+ "!!l. l: list(nat) ==> ALL i:nat. PROJ(i) ` l < ack(0, list_add(l))";
+by (asm_simp_tac ack2_ss 1);
+by (etac list.induct 1);
+by (asm_simp_tac (ack2_ss addsimps [nat_0_le]) 1);
+by (asm_simp_tac ack2_ss 1);
+by (rtac ballI 1);
+by (eres_inst_tac [("n","x")] natE 1);
+by (asm_simp_tac (ack2_ss addsimps [add_le_self]) 1);
+by (asm_simp_tac ack2_ss 1);
+by (etac (bspec RS lt_trans2) 1);
+by (rtac (add_le_self2 RS succ_leI) 2);
+by (tc_tac []);
+val PROJ_case_lemma = result();
+val PROJ_case = PROJ_case_lemma RS bspec;
+
+(** COMP case **)
+
+goal Primrec.thy
+ "!!fs. fs : list({f: primrec . \
+\ EX kf:nat. ALL l:list(nat). \
+\ f`l < ack(kf, list_add(l))}) \
+\ ==> EX k:nat. ALL l: list(nat). \
+\ list_add(map(%f. f ` l, fs)) < ack(k, list_add(l))";
+by (etac list.induct 1);
+by (DO_GOAL [res_inst_tac [("x","0")] bexI,
+ asm_simp_tac (ack2_ss addsimps [lt_ack1, nat_0_le]),
+ resolve_tac nat_typechecks] 1);
+by (safe_tac ZF_cs);
+by (asm_simp_tac ack2_ss 1);
+by (rtac (ballI RS bexI) 1);
+by (rtac (add_lt_mono RS lt_trans) 1);
+by (REPEAT (FIRSTGOAL (etac bspec)));
+by (rtac ack_add_bound 5);
+by (tc_tac []);
+val COMP_map_lemma = result();
+
+goalw Primrec.thy [COMP_def]
+ "!!g. [| g: primrec; kg: nat; \
+\ ALL l:list(nat). g`l < ack(kg, list_add(l)); \
+\ fs : list({f: primrec . \
+\ EX kf:nat. ALL l:list(nat). \
+\ f`l < ack(kf, list_add(l))}) \
+\ |] ==> EX k:nat. ALL l: list(nat). COMP(g,fs)`l < ack(k, list_add(l))";
+by (asm_simp_tac ZF_ss 1);
+by (forward_tac [list_CollectD] 1);
+by (etac (COMP_map_lemma RS bexE) 1);
+by (rtac (ballI RS bexI) 1);
+by (etac (bspec RS lt_trans) 1);
+by (rtac lt_trans 2);
+by (rtac ack_nest_bound 3);
+by (etac (bspec RS ack_lt_mono2) 2);
+by (tc_tac [map_type]);
+val COMP_case = result();
+
+(** PREC case **)
+
+goalw Primrec.thy [PREC_def]
+ "!!f g. [| ALL l:list(nat). f`l #+ list_add(l) < ack(kf, list_add(l)); \
+\ ALL l:list(nat). g`l #+ list_add(l) < ack(kg, list_add(l)); \
+\ f: primrec; kf: nat; \
+\ g: primrec; kg: nat; \
+\ l: list(nat) \
+\ |] ==> PREC(f,g)`l #+ list_add(l) < ack(succ(kf#+kg), list_add(l))";
+by (etac list.elim 1);
+by (asm_simp_tac (ack2_ss addsimps [[nat_le_refl, lt_ack2] MRS lt_trans]) 1);
+by (asm_simp_tac ack2_ss 1);
+by (etac ssubst 1); (*get rid of the needless assumption*)
+by (eres_inst_tac [("n","a")] nat_induct 1);
+(*base case*)
+by (DO_GOAL [asm_simp_tac ack2_ss, rtac lt_trans, etac bspec,
+ assume_tac, rtac (add_le_self RS ack_lt_mono1),
+ REPEAT o ares_tac (ack_typechecks)] 1);
+(*ind step*)
+by (asm_simp_tac (ack2_ss addsimps [add_succ_right]) 1);
+by (rtac (succ_leI RS lt_trans1) 1);
+by (res_inst_tac [("j", "g ` ?ll #+ ?mm")] lt_trans1 1);
+by (etac bspec 2);
+by (rtac (nat_le_refl RS add_le_mono) 1);
+by (tc_tac []);
+by (asm_simp_tac (ack2_ss addsimps [add_le_self2]) 1);
+(*final part of the simplification*)
+by (asm_simp_tac ack2_ss 1);
+by (rtac (add_le_self2 RS ack_le_mono1 RS lt_trans1) 1);
+by (etac ack_lt_mono2 5);
+by (tc_tac []);
+val PREC_case_lemma = result();
+
+goal Primrec.thy
+ "!!f g. [| f: primrec; kf: nat; \
+\ g: primrec; kg: nat; \
+\ ALL l:list(nat). f`l < ack(kf, list_add(l)); \
+\ ALL l:list(nat). g`l < ack(kg, list_add(l)) \
+\ |] ==> EX k:nat. ALL l: list(nat). \
+\ PREC(f,g)`l< ack(k, list_add(l))";
+by (rtac (ballI RS bexI) 1);
+by (rtac ([add_le_self, PREC_case_lemma] MRS lt_trans1) 1);
+by (REPEAT
+ (SOMEGOAL
+ (FIRST' [test_assume_tac,
+ match_tac (ack_typechecks),
+ rtac (ack_add_bound2 RS ballI) THEN' etac bspec])));
+val PREC_case = result();
+
+goal Primrec.thy
+ "!!f. f:primrec ==> EX k:nat. ALL l:list(nat). f`l < ack(k, list_add(l))";
+by (etac primrec.induct 1);
+by (safe_tac ZF_cs);
+by (DEPTH_SOLVE
+ (ares_tac ([SC_case, CONST_case, PROJ_case, COMP_case, PREC_case,
+ bexI, ballI] @ nat_typechecks) 1));
+val ack_bounds_primrec = result();
+
+goal Primrec.thy
+ "~ (lam l:list(nat). list_case(0, %x xs. ack(x,x), l)) : primrec";
+by (rtac notI 1);
+by (etac (ack_bounds_primrec RS bexE) 1);
+by (rtac lt_irrefl 1);
+by (dres_inst_tac [("x", "[x]")] bspec 1);
+by (asm_simp_tac ack2_ss 1);
+by (asm_full_simp_tac (ack2_ss addsimps [add_0_right]) 1);
+val ack_not_primrec = result();
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Primrec.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,64 @@
+(* Title: ZF/ex/Primrec.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Primitive Recursive Functions
+
+Proof adopted from
+Nora Szasz,
+A Machine Checked Proof that Ackermann's Function is not Primitive Recursive,
+In: Huet & Plotkin, eds., Logical Environments (CUP, 1993), 317-338.
+
+See also E. Mendelson, Introduction to Mathematical Logic.
+(Van Nostrand, 1964), page 250, exercise 11.
+*)
+
+Primrec = List +
+consts
+ primrec :: "i"
+ SC :: "i"
+ CONST :: "i=>i"
+ PROJ :: "i=>i"
+ COMP :: "[i,i]=>i"
+ PREC :: "[i,i]=>i"
+ ACK :: "i=>i"
+ ack :: "[i,i]=>i"
+
+translations
+ "ack(x,y)" == "ACK(x) ` [y]"
+
+rules
+
+ SC_def "SC == lam l:list(nat).list_case(0, %x xs.succ(x), l)"
+
+ CONST_def "CONST(k) == lam l:list(nat).k"
+
+ PROJ_def "PROJ(i) == lam l:list(nat). list_case(0, %x xs.x, drop(i,l))"
+
+ COMP_def "COMP(g,fs) == lam l:list(nat). g ` map(%f. f`l, fs)"
+
+ (*Note that g is applied first to PREC(f,g)`y and then to y!*)
+ PREC_def "PREC(f,g) == \
+\ lam l:list(nat). list_case(0, \
+\ %x xs. rec(x, f`xs, %y r. g ` Cons(r, Cons(y, xs))), l)"
+
+ ACK_def "ACK(i) == rec(i, SC, \
+\ %z r. PREC (CONST (r`[1]), COMP(r,[PROJ(0)])))"
+
+
+inductive
+ domains "primrec" <= "list(nat)->nat"
+ intrs
+ SC "SC : primrec"
+ CONST "k: nat ==> CONST(k) : primrec"
+ PROJ "i: nat ==> PROJ(i) : primrec"
+ COMP "[| g: primrec; fs: list(primrec) |] ==> COMP(g,fs): primrec"
+ PREC "[| f: primrec; g: primrec |] ==> PREC(f,g): primrec"
+ monos "[list_mono]"
+ con_defs "[SC_def,CONST_def,PROJ_def,COMP_def,PREC_def]"
+ type_intrs "nat_typechecks @ list.intrs @ \
+\ [lam_type, list_case_type, drop_type, map_type, \
+\ apply_type, rec_type]"
+
+end
--- a/src/ZF/ex/PropLog.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/PropLog.ML Fri Aug 12 12:28:46 1994 +0200
@@ -17,20 +17,20 @@
goal PropLog.thy "prop_rec(Fls,b,c,d) = b";
by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
-by (rewrite_goals_tac Prop.con_defs);
+by (rewrite_goals_tac prop.con_defs);
by (simp_tac rank_ss 1);
val prop_rec_Fls = result();
goal PropLog.thy "prop_rec(#v,b,c,d) = c(v)";
by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
-by (rewrite_goals_tac Prop.con_defs);
+by (rewrite_goals_tac prop.con_defs);
by (simp_tac rank_ss 1);
val prop_rec_Var = result();
goal PropLog.thy "prop_rec(p=>q,b,c,d) = \
\ d(p, q, prop_rec(p,b,c,d), prop_rec(q,b,c,d))";
by (rtac (prop_rec_def RS def_Vrec RS trans) 1);
-by (rewrite_goals_tac Prop.con_defs);
+by (rewrite_goals_tac prop.con_defs);
by (simp_tac rank_ss 1);
val prop_rec_Imp = result();
@@ -70,49 +70,34 @@
val hyps_Imp = result();
val prop_ss = prop_rec_ss
- addsimps Prop.intrs
+ addsimps prop.intrs
addsimps [is_true_Fls, is_true_Var, is_true_Imp,
hyps_Fls, hyps_Var, hyps_Imp];
(*** Proof theory of propositional logic ***)
-structure PropThms = Inductive_Fun
- (val thy = PropLog.thy;
- val thy_name = "PropThms";
- val rec_doms = [("thms","prop")];
- val sintrs =
- ["[| p:H; p:prop |] ==> H |- p",
- "[| p:prop; q:prop |] ==> H |- p=>q=>p",
- "[| p:prop; q:prop; r:prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r",
- "p:prop ==> H |- ((p=>Fls) => Fls) => p",
- "[| H |- p=>q; H |- p; p:prop; q:prop |] ==> H |- q"];
- val monos = [];
- val con_defs = [];
- val type_intrs = Prop.intrs;
- val type_elims = []);
-
-goalw PropThms.thy PropThms.defs "!!G H. G<=H ==> thms(G) <= thms(H)";
+goalw PropLog.thy thms.defs "!!G H. G<=H ==> thms(G) <= thms(H)";
by (rtac lfp_mono 1);
-by (REPEAT (rtac PropThms.bnd_mono 1));
+by (REPEAT (rtac thms.bnd_mono 1));
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
val thms_mono = result();
-val thms_in_pl = PropThms.dom_subset RS subsetD;
+val thms_in_pl = thms.dom_subset RS subsetD;
-val [thms_H, thms_K, thms_S, thms_DN, weak_thms_MP] = PropThms.intrs;
+val ImpE = prop.mk_cases prop.con_defs "p=>q : prop";
-(*Modus Ponens rule -- this stronger version avoids typecheck*)
-goal PropThms.thy "!!p q H. [| H |- p=>q; H |- p |] ==> H |- q";
-by (rtac weak_thms_MP 1);
+(*Stronger Modus Ponens rule: no typechecking!*)
+goal PropLog.thy "!!p q H. [| H |- p=>q; H |- p |] ==> H |- q";
+by (rtac thms.MP 1);
by (REPEAT (eresolve_tac [asm_rl, thms_in_pl, thms_in_pl RS ImpE] 1));
val thms_MP = result();
(*Rule is called I for Identity Combinator, not for Introduction*)
-goal PropThms.thy "!!p H. p:prop ==> H |- p=>p";
-by (rtac (thms_S RS thms_MP RS thms_MP) 1);
-by (rtac thms_K 5);
-by (rtac thms_K 4);
-by (REPEAT (ares_tac [ImpI] 1));
+goal PropLog.thy "!!p H. p:prop ==> H |- p=>p";
+by (rtac (thms.S RS thms_MP RS thms_MP) 1);
+by (rtac thms.K 5);
+by (rtac thms.K 4);
+by (REPEAT (ares_tac prop.intrs 1));
val thms_I = result();
(** Weakening, left and right **)
@@ -126,71 +111,71 @@
val weaken_left_Un1 = Un_upper1 RS weaken_left;
val weaken_left_Un2 = Un_upper2 RS weaken_left;
-goal PropThms.thy "!!H p q. [| H |- q; p:prop |] ==> H |- p=>q";
-by (rtac (thms_K RS thms_MP) 1);
+goal PropLog.thy "!!H p q. [| H |- q; p:prop |] ==> H |- p=>q";
+by (rtac (thms.K RS thms_MP) 1);
by (REPEAT (ares_tac [thms_in_pl] 1));
val weaken_right = result();
(*The deduction theorem*)
-goal PropThms.thy "!!p q H. [| cons(p,H) |- q; p:prop |] ==> H |- p=>q";
-by (etac PropThms.induct 1);
-by (fast_tac (ZF_cs addIs [thms_I, thms_H RS weaken_right]) 1);
-by (fast_tac (ZF_cs addIs [thms_K RS weaken_right]) 1);
-by (fast_tac (ZF_cs addIs [thms_S RS weaken_right]) 1);
-by (fast_tac (ZF_cs addIs [thms_DN RS weaken_right]) 1);
-by (fast_tac (ZF_cs addIs [thms_S RS thms_MP RS thms_MP]) 1);
+goal PropLog.thy "!!p q H. [| cons(p,H) |- q; p:prop |] ==> H |- p=>q";
+by (etac thms.induct 1);
+by (fast_tac (ZF_cs addIs [thms_I, thms.H RS weaken_right]) 1);
+by (fast_tac (ZF_cs addIs [thms.K RS weaken_right]) 1);
+by (fast_tac (ZF_cs addIs [thms.S RS weaken_right]) 1);
+by (fast_tac (ZF_cs addIs [thms.DN RS weaken_right]) 1);
+by (fast_tac (ZF_cs addIs [thms.S RS thms_MP RS thms_MP]) 1);
val deduction = result();
(*The cut rule*)
-goal PropThms.thy "!!H p q. [| H|-p; cons(p,H) |- q |] ==> H |- q";
+goal PropLog.thy "!!H p q. [| H|-p; cons(p,H) |- q |] ==> H |- q";
by (rtac (deduction RS thms_MP) 1);
by (REPEAT (ares_tac [thms_in_pl] 1));
val cut = result();
-goal PropThms.thy "!!H p. [| H |- Fls; p:prop |] ==> H |- p";
-by (rtac (thms_DN RS thms_MP) 1);
+goal PropLog.thy "!!H p. [| H |- Fls; p:prop |] ==> H |- p";
+by (rtac (thms.DN RS thms_MP) 1);
by (rtac weaken_right 2);
-by (REPEAT (ares_tac (Prop.intrs@[consI1]) 1));
+by (REPEAT (ares_tac (prop.intrs@[consI1]) 1));
val thms_FlsE = result();
(* [| H |- p=>Fls; H |- p; q: prop |] ==> H |- q *)
val thms_notE = standard (thms_MP RS thms_FlsE);
(*Soundness of the rules wrt truth-table semantics*)
-goalw PropThms.thy [logcon_def] "!!H. H |- p ==> H |= p";
-by (etac PropThms.induct 1);
+goalw PropLog.thy [logcon_def] "!!H. H |- p ==> H |= p";
+by (etac thms.induct 1);
by (fast_tac (ZF_cs addSDs [is_true_Imp RS iffD1 RS mp]) 5);
by (ALLGOALS (asm_simp_tac prop_ss));
val soundness = result();
(*** Towards the completeness proof ***)
-val [premf,premq] = goal PropThms.thy
+val [premf,premq] = goal PropLog.thy
"[| H |- p=>Fls; q: prop |] ==> H |- p=>q";
by (rtac (premf RS thms_in_pl RS ImpE) 1);
by (rtac deduction 1);
by (rtac (premf RS weaken_left_cons RS thms_notE) 1);
-by (REPEAT (ares_tac [premq, consI1, thms_H] 1));
+by (REPEAT (ares_tac [premq, consI1, thms.H] 1));
val Fls_Imp = result();
-val [premp,premq] = goal PropThms.thy
+val [premp,premq] = goal PropLog.thy
"[| H |- p; H |- q=>Fls |] ==> H |- (p=>q)=>Fls";
by (cut_facts_tac ([premp,premq] RL [thms_in_pl]) 1);
by (etac ImpE 1);
by (rtac deduction 1);
by (rtac (premq RS weaken_left_cons RS thms_MP) 1);
-by (rtac (consI1 RS thms_H RS thms_MP) 1);
+by (rtac (consI1 RS thms.H RS thms_MP) 1);
by (rtac (premp RS weaken_left_cons) 2);
-by (REPEAT (ares_tac Prop.intrs 1));
+by (REPEAT (ares_tac prop.intrs 1));
val Imp_Fls = result();
(*Typical example of strengthening the induction formula*)
-val [major] = goal PropThms.thy
+val [major] = goal PropLog.thy
"p: prop ==> hyps(p,t) |- if(is_true(p,t), p, p=>Fls)";
by (rtac (expand_if RS iffD2) 1);
-by (rtac (major RS Prop.induct) 1);
-by (ALLGOALS (asm_simp_tac (prop_ss addsimps [thms_I, thms_H])));
+by (rtac (major RS prop.induct) 1);
+by (ALLGOALS (asm_simp_tac (prop_ss addsimps [thms_I, thms.H])));
by (safe_tac (ZF_cs addSEs [Fls_Imp RS weaken_left_Un1,
Fls_Imp RS weaken_left_Un2]));
by (ALLGOALS (fast_tac (ZF_cs addIs [weaken_left_Un1, weaken_left_Un2,
@@ -198,7 +183,7 @@
val hyps_thms_if = result();
(*Key lemma for completeness; yields a set of assumptions satisfying p*)
-val [premp,sat] = goalw PropThms.thy [logcon_def]
+val [premp,sat] = goalw PropLog.thy [logcon_def]
"[| p: prop; 0 |= p |] ==> hyps(p,t) |- p";
by (rtac (sat RS spec RS mp RS if_P RS subst) 1 THEN
rtac (premp RS hyps_thms_if) 2);
@@ -207,46 +192,46 @@
(*For proving certain theorems in our new propositional logic*)
val thms_cs =
- ZF_cs addSIs [FlsI, VarI, ImpI, deduction]
- addIs [thms_in_pl, thms_H, thms_H RS thms_MP];
+ ZF_cs addSIs (prop.intrs @ [deduction])
+ addIs [thms_in_pl, thms.H, thms.H RS thms_MP];
(*The excluded middle in the form of an elimination rule*)
-val prems = goal PropThms.thy
+val prems = goal PropLog.thy
"[| p: prop; q: prop |] ==> H |- (p=>q) => ((p=>Fls)=>q) => q";
by (rtac (deduction RS deduction) 1);
-by (rtac (thms_DN RS thms_MP) 1);
+by (rtac (thms.DN RS thms_MP) 1);
by (ALLGOALS (best_tac (thms_cs addSIs prems)));
val thms_excluded_middle = result();
(*Hard to prove directly because it requires cuts*)
-val prems = goal PropThms.thy
+val prems = goal PropLog.thy
"[| cons(p,H) |- q; cons(p=>Fls,H) |- q; p: prop |] ==> H |- q";
by (rtac (thms_excluded_middle RS thms_MP RS thms_MP) 1);
-by (REPEAT (resolve_tac (prems@Prop.intrs@[deduction,thms_in_pl]) 1));
+by (REPEAT (resolve_tac (prems@prop.intrs@[deduction,thms_in_pl]) 1));
val thms_excluded_middle_rule = result();
(*** Completeness -- lemmas for reducing the set of assumptions ***)
(*For the case hyps(p,t)-cons(#v,Y) |- p;
we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
-val [major] = goal PropThms.thy
+val [major] = goal PropLog.thy
"p: prop ==> hyps(p, t-{v}) <= cons(#v=>Fls, hyps(p,t)-{#v})";
-by (rtac (major RS Prop.induct) 1);
+by (rtac (major RS prop.induct) 1);
by (simp_tac prop_ss 1);
by (asm_simp_tac (prop_ss setloop (split_tac [expand_if])) 1);
-by (fast_tac (ZF_cs addSEs Prop.free_SEs) 1);
+by (fast_tac (ZF_cs addSEs prop.free_SEs) 1);
by (asm_simp_tac prop_ss 1);
by (fast_tac ZF_cs 1);
val hyps_Diff = result();
(*For the case hyps(p,t)-cons(#v => Fls,Y) |- p;
we also have hyps(p,t)-{#v=>Fls} <= hyps(p, cons(v,t)) *)
-val [major] = goal PropThms.thy
+val [major] = goal PropLog.thy
"p: prop ==> hyps(p, cons(v,t)) <= cons(#v, hyps(p,t)-{#v=>Fls})";
-by (rtac (major RS Prop.induct) 1);
+by (rtac (major RS prop.induct) 1);
by (simp_tac prop_ss 1);
by (asm_simp_tac (prop_ss setloop (split_tac [expand_if])) 1);
-by (fast_tac (ZF_cs addSEs Prop.free_SEs) 1);
+by (fast_tac (ZF_cs addSEs prop.free_SEs) 1);
by (asm_simp_tac prop_ss 1);
by (fast_tac ZF_cs 1);
val hyps_cons = result();
@@ -263,26 +248,26 @@
(*The set hyps(p,t) is finite, and elements have the form #v or #v=>Fls;
could probably prove the stronger hyps(p,t) : Fin(hyps(p,0) Un hyps(p,nat))*)
-val [major] = goal PropThms.thy
+val [major] = goal PropLog.thy
"p: prop ==> hyps(p,t) : Fin(UN v:nat. {#v, #v=>Fls})";
-by (rtac (major RS Prop.induct) 1);
-by (asm_simp_tac (prop_ss addsimps [Fin_0I, Fin_consI, UN_I, cons_iff]
+by (rtac (major RS prop.induct) 1);
+by (asm_simp_tac (prop_ss addsimps (Fin.intrs @ [UN_I, cons_iff])
setloop (split_tac [expand_if])) 2);
-by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin_0I, Fin_UnI])));
+by (ALLGOALS (asm_simp_tac (prop_ss addsimps [Un_0, Fin.emptyI, Fin_UnI])));
val hyps_finite = result();
val Diff_weaken_left = subset_refl RSN (2, Diff_mono) RS weaken_left;
(*Induction on the finite set of assumptions hyps(p,t0).
We may repeatedly subtract assumptions until none are left!*)
-val [premp,sat] = goal PropThms.thy
+val [premp,sat] = goal PropLog.thy
"[| p: prop; 0 |= p |] ==> ALL t. hyps(p,t) - hyps(p,t0) |- p";
by (rtac (premp RS hyps_finite RS Fin_induct) 1);
by (simp_tac (prop_ss addsimps [premp, sat, logcon_thms_p, Diff_0]) 1);
by (safe_tac ZF_cs);
(*Case hyps(p,t)-cons(#v,Y) |- p *)
by (rtac thms_excluded_middle_rule 1);
-by (etac VarI 3);
+by (etac prop.Var_I 3);
by (rtac (cons_Diff_same RS weaken_left) 1);
by (etac spec 1);
by (rtac (cons_Diff_subset2 RS weaken_left) 1);
@@ -290,7 +275,7 @@
by (etac spec 1);
(*Case hyps(p,t)-cons(#v => Fls,Y) |- p *)
by (rtac thms_excluded_middle_rule 1);
-by (etac VarI 3);
+by (etac prop.Var_I 3);
by (rtac (cons_Diff_same RS weaken_left) 2);
by (etac spec 2);
by (rtac (cons_Diff_subset2 RS weaken_left) 1);
@@ -299,28 +284,28 @@
val completeness_0_lemma = result();
(*The base case for completeness*)
-val [premp,sat] = goal PropThms.thy "[| p: prop; 0 |= p |] ==> 0 |- p";
+val [premp,sat] = goal PropLog.thy "[| p: prop; 0 |= p |] ==> 0 |- p";
by (rtac (Diff_cancel RS subst) 1);
by (rtac (sat RS (premp RS completeness_0_lemma RS spec)) 1);
val completeness_0 = result();
(*A semantic analogue of the Deduction Theorem*)
-goalw PropThms.thy [logcon_def] "!!H p q. [| cons(p,H) |= q |] ==> H |= p=>q";
+goalw PropLog.thy [logcon_def] "!!H p q. [| cons(p,H) |= q |] ==> H |= p=>q";
by (simp_tac prop_ss 1);
by (fast_tac ZF_cs 1);
val logcon_Imp = result();
-goal PropThms.thy "!!H. H: Fin(prop) ==> ALL p:prop. H |= p --> H |- p";
+goal PropLog.thy "!!H. H: Fin(prop) ==> ALL p:prop. H |= p --> H |- p";
by (etac Fin_induct 1);
by (safe_tac (ZF_cs addSIs [completeness_0]));
by (rtac (weaken_left_cons RS thms_MP) 1);
-by (fast_tac (ZF_cs addSIs [logcon_Imp,ImpI]) 1);
+by (fast_tac (ZF_cs addSIs (logcon_Imp::prop.intrs)) 1);
by (fast_tac thms_cs 1);
val completeness_lemma = result();
val completeness = completeness_lemma RS bspec RS mp;
-val [finite] = goal PropThms.thy "H: Fin(prop) ==> H |- p <-> H |= p & p:prop";
+val [finite] = goal PropLog.thy "H: Fin(prop) ==> H |- p <-> H |= p & p:prop";
by (fast_tac (ZF_cs addSEs [soundness, finite RS completeness,
thms_in_pl]) 1);
val thms_iff = result();
--- a/src/ZF/ex/PropLog.thy Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/PropLog.thy Fri Aug 12 12:28:46 1994 +0200
@@ -1,26 +1,49 @@
-(* Title: ZF/ex/prop-log.thy
+(* Title: ZF/ex/PropLog.thy
ID: $Id$
Author: Tobias Nipkow & Lawrence C Paulson
Copyright 1993 University of Cambridge
-Inductive definition of propositional logic.
+Datatype definition of propositional logic formulae and inductive definition
+of the propositional tautologies.
*)
-PropLog = Prop + Fin +
+PropLog = Finite + Univ +
+
+(** The datatype of propositions; note mixfix syntax **)
consts
- (*semantics*)
- prop_rec :: "[i, i, i=>i, [i,i,i,i]=>i] => i"
- is_true :: "[i,i] => o"
- "|=" :: "[i,i] => o" (infixl 50)
- hyps :: "[i,i] => i"
+ prop :: "i"
- (*proof theory*)
+datatype
+ "prop" = Fls
+ | Var ("n: nat") ("#_" [100] 100)
+ | "=>" ("p: prop", "q: prop") (infixr 90)
+
+(** The proof system **)
+consts
thms :: "i => i"
"|-" :: "[i,i] => o" (infixl 50)
translations
"H |- p" == "p : thms(H)"
+inductive
+ domains "thms(H)" <= "prop"
+ intrs
+ H "[| p:H; p:prop |] ==> H |- p"
+ K "[| p:prop; q:prop |] ==> H |- p=>q=>p"
+ S "[| p:prop; q:prop; r:prop |] ==> H |- (p=>q=>r) => (p=>q) => p=>r"
+ DN "p:prop ==> H |- ((p=>Fls) => Fls) => p"
+ MP "[| H |- p=>q; H |- p; p:prop; q:prop |] ==> H |- q"
+ type_intrs "prop.intrs"
+
+
+(** The semantics **)
+consts
+ prop_rec :: "[i, i, i=>i, [i,i,i,i]=>i] => i"
+ is_true :: "[i,i] => o"
+ "|=" :: "[i,i] => o" (infixl 50)
+ hyps :: "[i,i] => i"
+
rules
prop_rec_def
--- a/src/ZF/ex/ROOT.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/ROOT.ML Fri Aug 12 12:28:46 1994 +0200
@@ -21,12 +21,12 @@
time_use_thy "ex/Integ";
(*Binary integer arithmetic*)
use "ex/twos_compl.ML";
-time_use_thy "ex/BinFn";
+time_use_thy "ex/Bin";
(** Datatypes **)
-time_use_thy "ex/BT_Fn"; (*binary trees*)
-time_use_thy "ex/TermFn"; (*terms: recursion over the list functor*)
-time_use_thy "ex/TF_Fn"; (*trees/forests: mutual recursion*)
+time_use_thy "ex/BT"; (*binary trees*)
+time_use_thy "ex/Term"; (*terms: recursion over the list functor*)
+time_use_thy "ex/TF"; (*trees/forests: mutual recursion*)
time_use_thy "ex/Ntree"; (*variable-branching trees; function demo*)
time_use_thy "ex/Brouwer"; (*Brouwer ordinals: infinite-branching trees*)
time_use_thy "ex/Data"; (*Sample datatype*)
@@ -35,16 +35,14 @@
(** Inductive definitions **)
time_use_thy "ex/Rmap"; (*mapping a relation over a list*)
time_use_thy "ex/PropLog"; (*completeness of propositional logic*)
-(*two Coq examples by Ch. Paulin-Mohring*)
+(*two Coq examples by Christine Paulin-Mohring*)
time_use_thy "ex/ListN";
time_use_thy "ex/Acc";
-time_use_thy "ex/Contract0"; (*Contraction relation for combinatory logic*)
-time_use_thy "ex/ParContract"; (*Diamond property for combinatory logic*)
-time_use_thy "ex/Primrec0";
+time_use_thy "ex/Comb"; (*Combinatory Logic example*)
+time_use_thy "ex/Primrec";
(** CoDatatypes **)
time_use_thy "ex/LList";
-time_use_thy "ex/LListFn";
time_use "ex/CoUnit.ML";
maketest"END: Root file for ZF Set Theory examples";
--- a/src/ZF/ex/Rmap.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Rmap.ML Fri Aug 12 12:28:46 1994 +0200
@@ -1,43 +1,31 @@
-(* Title: ZF/ex/rmap
+(* Title: ZF/ex/Rmap
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
+ Copyright 1994 University of Cambridge
Inductive definition of an operator to "map" a relation over a list
*)
-structure Rmap = Inductive_Fun
- (val thy = List.thy |> add_consts [("rmap","i=>i",NoSyn)];
- val thy_name = "Rmap";
- val rec_doms = [("rmap", "list(domain(r))*list(range(r))")];
- val sintrs =
- ["<Nil,Nil> : rmap(r)",
+open Rmap;
- "[| <x,y>: r; <xs,ys> : rmap(r) |] ==> \
-\ <Cons(x,xs), Cons(y,ys)> : rmap(r)"];
- val monos = [];
- val con_defs = [];
- val type_intrs = [domainI,rangeI] @ List.intrs
- val type_elims = []);
-
-goalw Rmap.thy Rmap.defs "!!r s. r<=s ==> rmap(r) <= rmap(s)";
+goalw Rmap.thy rmap.defs "!!r s. r<=s ==> rmap(r) <= rmap(s)";
by (rtac lfp_mono 1);
-by (REPEAT (rtac Rmap.bnd_mono 1));
+by (REPEAT (rtac rmap.bnd_mono 1));
by (REPEAT (ares_tac ([Sigma_mono, list_mono, domain_mono, range_mono] @
basic_monos) 1));
val rmap_mono = result();
val rmap_induct = standard
- (Rmap.mutual_induct RS spec RS spec RSN (2,rev_mp));
+ (rmap.mutual_induct RS spec RS spec RSN (2,rev_mp));
-val Nil_rmap_case = Rmap.mk_cases List.con_defs "<Nil,zs> : rmap(r)"
-and Cons_rmap_case = Rmap.mk_cases List.con_defs "<Cons(x,xs),zs> : rmap(r)";
+val Nil_rmap_case = rmap.mk_cases list.con_defs "<Nil,zs> : rmap(r)"
+and Cons_rmap_case = rmap.mk_cases list.con_defs "<Cons(x,xs),zs> : rmap(r)";
-val rmap_cs = ZF_cs addIs Rmap.intrs
+val rmap_cs = ZF_cs addIs rmap.intrs
addSEs [Nil_rmap_case, Cons_rmap_case];
goal Rmap.thy "!!r. r <= A*B ==> rmap(r) <= list(A)*list(B)";
-by (rtac (Rmap.dom_subset RS subset_trans) 1);
+by (rtac (rmap.dom_subset RS subset_trans) 1);
by (REPEAT (ares_tac [domain_rel_subset, range_rel_subset,
Sigma_mono, list_mono] 1));
val rmap_rel_type = result();
@@ -45,7 +33,7 @@
goal Rmap.thy
"!!r. [| ALL x:A. EX y. <x,y>: r; xs: list(A) |] ==> \
\ EX y. <xs, y> : rmap(r)";
-by (etac List.induct 1);
+by (etac list.induct 1);
by (ALLGOALS (fast_tac rmap_cs));
val rmap_total = result();
@@ -79,5 +67,5 @@
goal Rmap.thy "!!f. [| f: A->B; x: A; xs: list(A) |] ==> \
\ rmap(f) ` Cons(x,xs) = Cons(f`x, rmap(f)`xs)";
by (rtac apply_equality 1);
-by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ Rmap.intrs) 1));
+by (REPEAT (ares_tac ([apply_Pair, rmap_fun_type] @ rmap.intrs) 1));
val rmap_Cons = result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Rmap.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,25 @@
+(* Title: ZF/ex/Rmap
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Inductive definition of an operator to "map" a relation over a list
+*)
+
+Rmap = List +
+
+consts
+ rmap :: "i=>i"
+
+inductive
+ domains "rmap(r)" <= "list(domain(r))*list(range(r))"
+ intrs
+ NilI "<Nil,Nil> : rmap(r)"
+
+ ConsI "[| <x,y>: r; <xs,ys> : rmap(r) |] ==> \
+\ <Cons(x,xs), Cons(y,ys)> : rmap(r)"
+
+ type_intrs "[domainI,rangeI] @ list.intrs"
+
+end
+
--- a/src/ZF/ex/TF.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/TF.ML Fri Aug 12 12:28:46 1994 +0200
@@ -4,39 +4,29 @@
Copyright 1993 University of Cambridge
Trees & forests, a mutually recursive type definition.
+
+Still needs
+
+"TF_reflect == (%z. TF_rec(z, %x ts r. Tcons(x,r), 0,
+ %t ts r1 r2. TF_of_list(list_of_TF(r2) @ <r1,0>)))"
*)
-structure TF = Datatype_Fun
- (val thy = Univ.thy
- val thy_name = "TF"
- val rec_specs = [("tree", "univ(A)",
- [(["Tcons"], "[i,i]=>i", NoSyn)]),
- ("forest", "univ(A)",
- [(["Fnil"], "i", NoSyn),
- (["Fcons"], "[i,i]=>i", NoSyn)])]
- val rec_styp = "i=>i"
- val sintrs =
- ["[| a:A; f: forest(A) |] ==> Tcons(a,f) : tree(A)",
- "Fnil : forest(A)",
- "[| t: tree(A); f: forest(A) |] ==> Fcons(t,f) : forest(A)"]
- val monos = []
- val type_intrs = datatype_intrs
- val type_elims = datatype_elims);
+open TF;
-val [TconsI, FnilI, FconsI] = TF.intrs;
+val [TconsI, FnilI, FconsI] = tree_forest.intrs;
(** tree_forest(A) as the union of tree(A) and forest(A) **)
-goalw TF.thy (tl TF.defs) "tree(A) <= tree_forest(A)";
+goalw TF.thy (tl tree_forest.defs) "tree(A) <= tree_forest(A)";
by (rtac Part_subset 1);
val tree_subset_TF = result();
-goalw TF.thy (tl TF.defs) "forest(A) <= tree_forest(A)";
+goalw TF.thy (tl tree_forest.defs) "forest(A) <= tree_forest(A)";
by (rtac Part_subset 1);
val forest_subset_TF = result();
-goalw TF.thy (tl TF.defs) "tree(A) Un forest(A) = tree_forest(A)";
-by (rtac (TF.dom_subset RS Part_sum_equality) 1);
+goalw TF.thy (tl tree_forest.defs) "tree(A) Un forest(A) = tree_forest(A)";
+by (rtac (tree_forest.dom_subset RS Part_sum_equality) 1);
val TF_equals_Un = result();
(** NOT useful, but interesting... **)
@@ -44,30 +34,240 @@
(*The (refl RS conjI RS exI RS exI) avoids considerable search!*)
val unfold_cs = sum_cs addSIs [PartI, refl RS conjI RS exI RS exI]
addIs datatype_intrs
- addDs [TF.dom_subset RS subsetD]
- addSEs ([PartE] @ datatype_elims @ TF.free_SEs);
+ addDs [tree_forest.dom_subset RS subsetD]
+ addSEs ([PartE] @ datatype_elims @ tree_forest.free_SEs);
-goalw TF.thy (tl TF.defs)
+goalw TF.thy (tl tree_forest.defs)
"tree_forest(A) = (A*forest(A)) + ({0} + tree(A)*forest(A))";
-by (rtac (TF.unfold RS trans) 1);
-by (rewrite_goals_tac TF.con_defs);
+by (rtac (tree_forest.unfold RS trans) 1);
+by (rewrite_goals_tac tree_forest.con_defs);
by (rtac equalityI 1);
by (fast_tac unfold_cs 1);
by (fast_tac unfold_cs 1);
val tree_forest_unfold = result();
-val tree_forest_unfold' = rewrite_rule (tl TF.defs) tree_forest_unfold;
+val tree_forest_unfold' = rewrite_rule (tl tree_forest.defs) tree_forest_unfold;
-goalw TF.thy (tl TF.defs) "tree(A) = {Inl(x). x: A*forest(A)}";
+goalw TF.thy (tl tree_forest.defs)
+ "tree(A) = {Inl(x). x: A*forest(A)}";
by (rtac (Part_Inl RS subst) 1);
by (rtac (tree_forest_unfold' RS subst_context) 1);
val tree_unfold = result();
-goalw TF.thy (tl TF.defs) "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}";
+goalw TF.thy (tl tree_forest.defs)
+ "forest(A) = {Inr(x). x: {0} + tree(A)*forest(A)}";
by (rtac (Part_Inr RS subst) 1);
by (rtac (tree_forest_unfold' RS subst_context) 1);
val forest_unfold = result();
+(*** TF_rec -- by Vset recursion ***)
+(** conversion rules **)
+
+goal TF.thy "TF_rec(Tcons(a,f), b, c, d) = b(a, f, TF_rec(f,b,c,d))";
+by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac tree_forest.con_defs);
+by (simp_tac rank_ss 1);
+val TF_rec_Tcons = result();
+
+goal TF.thy "TF_rec(Fnil, b, c, d) = c";
+by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac tree_forest.con_defs);
+by (simp_tac rank_ss 1);
+val TF_rec_Fnil = result();
+
+goal TF.thy "TF_rec(Fcons(t,f), b, c, d) = \
+\ d(t, f, TF_rec(t, b, c, d), TF_rec(f, b, c, d))";
+by (rtac (TF_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac tree_forest.con_defs);
+by (simp_tac rank_ss 1);
+val TF_rec_Fcons = result();
+
+(*list_ss includes list operations as well as arith_ss*)
+val TF_rec_ss = list_ss addsimps
+ [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons, TconsI, FnilI, FconsI];
+
+(** Type checking **)
+
+val major::prems = goal TF.thy
+ "[| z: tree_forest(A); \
+\ !!x f r. [| x: A; f: forest(A); r: C(f) \
+\ |] ==> b(x,f,r): C(Tcons(x,f)); \
+\ c : C(Fnil); \
+\ !!t f r1 r2. [| t: tree(A); f: forest(A); r1: C(t); r2: C(f) \
+\ |] ==> d(t,f,r1,r2): C(Fcons(t,f)) \
+\ |] ==> TF_rec(z,b,c,d) : C(z)";
+by (rtac (major RS tree_forest.induct) 1);
+by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
+val TF_rec_type = result();
+
+(*Mutually recursive version*)
+val prems = goal TF.thy
+ "[| !!x f r. [| x: A; f: forest(A); r: D(f) \
+\ |] ==> b(x,f,r): C(Tcons(x,f)); \
+\ c : D(Fnil); \
+\ !!t f r1 r2. [| t: tree(A); f: forest(A); r1: C(t); r2: D(f) \
+\ |] ==> d(t,f,r1,r2): D(Fcons(t,f)) \
+\ |] ==> (ALL t:tree(A). TF_rec(t,b,c,d) : C(t)) & \
+\ (ALL f: forest(A). TF_rec(f,b,c,d) : D(f))";
+by (rewtac Ball_def);
+by (rtac tree_forest.mutual_induct 1);
+by (ALLGOALS (asm_simp_tac (TF_rec_ss addsimps prems)));
+val tree_forest_rec_type = result();
+
+
+(** Versions for use with definitions **)
+
+val [rew] = goal TF.thy
+ "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Tcons(a,f)) = b(a,f,j(f))";
+by (rewtac rew);
+by (rtac TF_rec_Tcons 1);
+val def_TF_rec_Tcons = result();
+
+val [rew] = goal TF.thy
+ "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fnil) = c";
+by (rewtac rew);
+by (rtac TF_rec_Fnil 1);
+val def_TF_rec_Fnil = result();
+
+val [rew] = goal TF.thy
+ "[| !!z. j(z)==TF_rec(z,b,c,d) |] ==> j(Fcons(t,f)) = d(t,f,j(t),j(f))";
+by (rewtac rew);
+by (rtac TF_rec_Fcons 1);
+val def_TF_rec_Fcons = result();
+
+fun TF_recs def = map standard
+ ([def] RL [def_TF_rec_Tcons, def_TF_rec_Fnil, def_TF_rec_Fcons]);
+
+
+(** list_of_TF and TF_of_list **)
+
+val [list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons] =
+ TF_recs list_of_TF_def;
+
+goalw TF.thy [list_of_TF_def]
+ "!!z A. z: tree_forest(A) ==> list_of_TF(z) : list(tree(A))";
+by (REPEAT (ares_tac ([TF_rec_type,TconsI] @ list_typechecks) 1));
+val list_of_TF_type = result();
+
+val [TF_of_list_Nil,TF_of_list_Cons] = list_recs TF_of_list_def;
+
+goalw TF.thy [TF_of_list_def]
+ "!!l A. l: list(tree(A)) ==> TF_of_list(l) : forest(A)";
+by (REPEAT (ares_tac [list_rec_type, FnilI, FconsI] 1));
+val TF_of_list_type = result();
+
+
+(** TF_map **)
+
+val [TF_map_Tcons, TF_map_Fnil, TF_map_Fcons] = TF_recs TF_map_def;
+
+val prems = goalw TF.thy [TF_map_def]
+ "[| !!x. x: A ==> h(x): B |] ==> \
+\ (ALL t:tree(A). TF_map(h,t) : tree(B)) & \
+\ (ALL f: forest(A). TF_map(h,f) : forest(B))";
+by (REPEAT
+ (ares_tac ([tree_forest_rec_type, TconsI, FnilI, FconsI] @ prems) 1));
+val TF_map_type = result();
+
+
+(** TF_size **)
+
+val [TF_size_Tcons, TF_size_Fnil, TF_size_Fcons] = TF_recs TF_size_def;
+
+goalw TF.thy [TF_size_def]
+ "!!z A. z: tree_forest(A) ==> TF_size(z) : nat";
+by (REPEAT (ares_tac [TF_rec_type, add_type, nat_0I, nat_succI] 1));
+val TF_size_type = result();
+
+
+(** TF_preorder **)
+
+val [TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons] =
+ TF_recs TF_preorder_def;
+
+goalw TF.thy [TF_preorder_def]
+ "!!z A. z: tree_forest(A) ==> TF_preorder(z) : list(A)";
+by (REPEAT (ares_tac ([TF_rec_type, app_type] @ list.intrs) 1));
+val TF_preorder_type = result();
+
+
+(** Term simplification **)
+
+val treeI = tree_subset_TF RS subsetD
+and forestI = forest_subset_TF RS subsetD;
+
+val TF_typechecks =
+ [TconsI, FnilI, FconsI, treeI, forestI,
+ list_of_TF_type, TF_map_type, TF_size_type, TF_preorder_type];
+
+val TF_rewrites =
+ [TF_rec_Tcons, TF_rec_Fnil, TF_rec_Fcons,
+ list_of_TF_Tcons, list_of_TF_Fnil, list_of_TF_Fcons,
+ TF_of_list_Nil,TF_of_list_Cons,
+ TF_map_Tcons, TF_map_Fnil, TF_map_Fcons,
+ TF_size_Tcons, TF_size_Fnil, TF_size_Fcons,
+ TF_preorder_Tcons, TF_preorder_Fnil, TF_preorder_Fcons];
+
+val TF_ss = list_ss addsimps TF_rewrites
+ setsolver type_auto_tac (list_typechecks@TF_typechecks);
+
+(** theorems about list_of_TF and TF_of_list **)
+
+(*essentially the same as list induction*)
+val major::prems = goal TF.thy
+ "[| f: forest(A); \
+\ R(Fnil); \
+\ !!t f. [| t: tree(A); f: forest(A); R(f) |] ==> R(Fcons(t,f)) \
+\ |] ==> R(f)";
+by (rtac (major RS (tree_forest.mutual_induct RS conjunct2 RS spec RSN (2,rev_mp))) 1);
+by (REPEAT (ares_tac (TrueI::prems) 1));
+val forest_induct = result();
+
+goal TF.thy "!!f A. f: forest(A) ==> TF_of_list(list_of_TF(f)) = f";
+by (etac forest_induct 1);
+by (ALLGOALS (asm_simp_tac TF_ss));
+val forest_iso = result();
+
+goal TF.thy
+ "!!ts. ts: list(tree(A)) ==> list_of_TF(TF_of_list(ts)) = ts";
+by (etac list.induct 1);
+by (ALLGOALS (asm_simp_tac TF_ss));
+val tree_list_iso = result();
+
+(** theorems about TF_map **)
+
+goal TF.thy "!!z A. z: tree_forest(A) ==> TF_map(%u.u, z) = z";
+by (etac tree_forest.induct 1);
+by (ALLGOALS (asm_simp_tac TF_ss));
+val TF_map_ident = result();
+
+goal TF.thy
+ "!!z A. z: tree_forest(A) ==> TF_map(h, TF_map(j,z)) = TF_map(%u.h(j(u)), z)";
+by (etac tree_forest.induct 1);
+by (ALLGOALS (asm_simp_tac TF_ss));
+val TF_map_compose = result();
+
+(** theorems about TF_size **)
+
+goal TF.thy
+ "!!z A. z: tree_forest(A) ==> TF_size(TF_map(h,z)) = TF_size(z)";
+by (etac tree_forest.induct 1);
+by (ALLGOALS (asm_simp_tac TF_ss));
+val TF_size_TF_map = result();
+
+goal TF.thy
+ "!!z A. z: tree_forest(A) ==> TF_size(z) = length(TF_preorder(z))";
+by (etac tree_forest.induct 1);
+by (ALLGOALS (asm_simp_tac (TF_ss addsimps [length_app])));
+val TF_size_length = result();
+
+(** theorems about TF_preorder **)
+
+goal TF.thy "!!z A. z: tree_forest(A) ==> \
+\ TF_preorder(TF_map(h,z)) = map(h, TF_preorder(z))";
+by (etac tree_forest.induct 1);
+by (ALLGOALS (asm_simp_tac (TF_ss addsimps [map_app_distrib])));
+val TF_preorder_TF_map = result();
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/TF.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,49 @@
+(* Title: ZF/ex/TF.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Trees & forests, a mutually recursive type definition.
+*)
+
+TF = List +
+consts
+ TF_rec :: "[i, [i,i,i]=>i, i, [i,i,i,i]=>i] => i"
+ TF_map :: "[i=>i, i] => i"
+ TF_size :: "i=>i"
+ TF_preorder :: "i=>i"
+ list_of_TF :: "i=>i"
+ TF_of_list :: "i=>i"
+
+ tree, forest, tree_forest :: "i=>i"
+
+datatype
+ "tree(A)" = "Tcons" ("a: A", "f: forest(A)")
+and
+ "forest(A)" = "Fnil" | "Fcons" ("t: tree(A)", "f: forest(A)")
+
+rules
+ TF_rec_def
+ "TF_rec(z,b,c,d) == Vrec(z, \
+\ %z r. tree_forest_case(%x f. b(x, f, r`f), \
+\ c, \
+\ %t f. d(t, f, r`t, r`f), z))"
+
+ list_of_TF_def
+ "list_of_TF(z) == TF_rec(z, %x f r. [Tcons(x,f)], [], \
+\ %t f r1 r2. Cons(t, r2))"
+
+ TF_of_list_def
+ "TF_of_list(f) == list_rec(f, Fnil, %t f r. Fcons(t,r))"
+
+ TF_map_def
+ "TF_map(h,z) == TF_rec(z, %x f r.Tcons(h(x),r), Fnil, \
+\ %t f r1 r2. Fcons(r1,r2))"
+
+ TF_size_def
+ "TF_size(z) == TF_rec(z, %x f r.succ(r), 0, %t f r1 r2. r1#+r2)"
+
+ TF_preorder_def
+ "TF_preorder(z) == TF_rec(z, %x f r.Cons(x,r), Nil, %t f r1 r2. r1@r2)"
+
+end
--- a/src/ZF/ex/Term.ML Fri Aug 12 11:13:23 1994 +0200
+++ b/src/ZF/ex/Term.ML Fri Aug 12 12:28:46 1994 +0200
@@ -7,26 +7,16 @@
Illustrates the list functor (essentially the same type as in Trees & Forests)
*)
-structure Term = Datatype_Fun
- (val thy = List.thy;
- val thy_name = "Term";
- val rec_specs =
- [("term", "univ(A)",
- [(["Apply"], "[i,i]=>i", NoSyn)])];
- val rec_styp = "i=>i";
- val sintrs = ["[| a: A; l: list(term(A)) |] ==> Apply(a,l) : term(A)"];
- val monos = [list_mono];
- val type_intrs = (list_univ RS subsetD) :: datatype_intrs;
- val type_elims = []);
-
-val [ApplyI] = Term.intrs;
+open Term;
goal Term.thy "term(A) = A * list(term(A))";
-by (rtac (Term.unfold RS trans) 1);
-bws Term.con_defs;
-by (fast_tac (sum_cs addIs ([equalityI] @ datatype_intrs)
- addDs [Term.dom_subset RS subsetD]
- addEs [A_into_univ, list_into_univ]) 1);
+by (rtac (term.unfold RS trans) 1);
+bws term.con_defs;
+br equalityI 1;
+by (fast_tac sum_cs 1);
+by (fast_tac (sum_cs addIs datatype_intrs
+ addDs [term.dom_subset RS subsetD]
+ addEs [list_into_univ]) 1);
val term_unfold = result();
(*Induction on term(A) followed by induction on List *)
@@ -36,33 +26,33 @@
\ !!x z zs. [| x: A; z: term(A); zs: list(term(A)); P(Apply(x,zs)) \
\ |] ==> P(Apply(x, Cons(z,zs))) \
\ |] ==> P(t)";
-by (rtac (major RS Term.induct) 1);
-by (etac List.induct 1);
+by (rtac (major RS term.induct) 1);
+by (etac list.induct 1);
by (etac CollectE 2);
by (REPEAT (ares_tac (prems@[list_CollectD]) 1));
val term_induct2 = result();
(*Induction on term(A) to prove an equation*)
-val major::prems = goal (merge_theories(Term.thy,ListFn.thy))
+val major::prems = goal Term.thy
"[| t: term(A); \
\ !!x zs. [| x: A; zs: list(term(A)); map(f,zs) = map(g,zs) |] ==> \
\ f(Apply(x,zs)) = g(Apply(x,zs)) \
\ |] ==> f(t)=g(t)";
-by (rtac (major RS Term.induct) 1);
+by (rtac (major RS term.induct) 1);
by (resolve_tac prems 1);
by (REPEAT (eresolve_tac [asm_rl, map_list_Collect, list_CollectD] 1));
val term_induct_eqn = result();
(** Lemmas to justify using "term" in other recursive type definitions **)
-goalw Term.thy Term.defs "!!A B. A<=B ==> term(A) <= term(B)";
+goalw Term.thy term.defs "!!A B. A<=B ==> term(A) <= term(B)";
by (rtac lfp_mono 1);
-by (REPEAT (rtac Term.bnd_mono 1));
+by (REPEAT (rtac term.bnd_mono 1));
by (REPEAT (ares_tac (univ_mono::basic_monos) 1));
val term_mono = result();
(*Easily provable by induction also*)
-goalw Term.thy (Term.defs@Term.con_defs) "term(univ(A)) <= univ(A)";
+goalw Term.thy (term.defs@term.con_defs) "term(univ(A)) <= univ(A)";
by (rtac lfp_lowerbound 1);
by (rtac (A_subset_univ RS univ_mono) 2);
by (safe_tac ZF_cs);
@@ -75,3 +65,178 @@
goal Term.thy "!!t A B. [| t: term(A); A <= univ(B) |] ==> t: univ(B)";
by (REPEAT (ares_tac [term_subset_univ RS subsetD] 1));
val term_into_univ = result();
+
+
+(*** term_rec -- by Vset recursion ***)
+
+(*Lemma: map works correctly on the underlying list of terms*)
+val [major,ordi] = goal list.thy
+ "[| l: list(A); Ord(i) |] ==> \
+\ rank(l)<i --> map(%z. (lam x:Vset(i).h(x)) ` z, l) = map(h,l)";
+by (rtac (major RS list.induct) 1);
+by (simp_tac list_ss 1);
+by (rtac impI 1);
+by (forward_tac [rank_Cons1 RS lt_trans] 1);
+by (dtac (rank_Cons2 RS lt_trans) 1);
+by (asm_simp_tac (list_ss addsimps [ordi, VsetI]) 1);
+val map_lemma = result();
+
+(*Typing premise is necessary to invoke map_lemma*)
+val [prem] = goal Term.thy
+ "ts: list(A) ==> \
+\ term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))";
+by (rtac (term_rec_def RS def_Vrec RS trans) 1);
+by (rewrite_goals_tac term.con_defs);
+val term_rec_ss = ZF_ss addsimps [Ord_rank, rank_pair2, prem RS map_lemma];
+by (simp_tac term_rec_ss 1);
+val term_rec = result();
+
+(*Slightly odd typing condition on r in the second premise!*)
+val major::prems = goal Term.thy
+ "[| t: term(A); \
+\ !!x zs r. [| x: A; zs: list(term(A)); \
+\ r: list(UN t:term(A). C(t)) |] \
+\ ==> d(x, zs, r): C(Apply(x,zs)) \
+\ |] ==> term_rec(t,d) : C(t)";
+by (rtac (major RS term.induct) 1);
+by (forward_tac [list_CollectD] 1);
+by (rtac (term_rec RS ssubst) 1);
+by (REPEAT (ares_tac prems 1));
+by (etac list.induct 1);
+by (ALLGOALS (asm_simp_tac (list_ss addsimps [term_rec])));
+by (etac CollectE 1);
+by (REPEAT (ares_tac [list.Cons_I, UN_I] 1));
+val term_rec_type = result();
+
+val [rew,tslist] = goal Term.thy
+ "[| !!t. j(t)==term_rec(t,d); ts: list(A) |] ==> \
+\ j(Apply(a,ts)) = d(a, ts, map(%Z.j(Z), ts))";
+by (rewtac rew);
+by (rtac (tslist RS term_rec) 1);
+val def_term_rec = result();
+
+val prems = goal Term.thy
+ "[| t: term(A); \
+\ !!x zs r. [| x: A; zs: list(term(A)); r: list(C) |] \
+\ ==> d(x, zs, r): C \
+\ |] ==> term_rec(t,d) : C";
+by (REPEAT (ares_tac (term_rec_type::prems) 1));
+by (etac (subset_refl RS UN_least RS list_mono RS subsetD) 1);
+val term_rec_simple_type = result();
+
+
+(** term_map **)
+
+val term_map = standard (term_map_def RS def_term_rec);
+
+val prems = goalw Term.thy [term_map_def]
+ "[| t: term(A); !!x. x: A ==> f(x): B |] ==> term_map(f,t) : term(B)";
+by (REPEAT (ares_tac ([term_rec_simple_type, term.Apply_I] @ prems) 1));
+val term_map_type = result();
+
+val [major] = goal Term.thy
+ "t: term(A) ==> term_map(f,t) : term({f(u). u:A})";
+by (rtac (major RS term_map_type) 1);
+by (etac RepFunI 1);
+val term_map_type2 = result();
+
+
+(** term_size **)
+
+val term_size = standard (term_size_def RS def_term_rec);
+
+goalw Term.thy [term_size_def] "!!t A. t: term(A) ==> term_size(t) : nat";
+by (REPEAT (ares_tac [term_rec_simple_type, list_add_type, nat_succI] 1));
+val term_size_type = result();
+
+
+(** reflect **)
+
+val reflect = standard (reflect_def RS def_term_rec);
+
+goalw Term.thy [reflect_def] "!!t A. t: term(A) ==> reflect(t) : term(A)";
+by (REPEAT (ares_tac [term_rec_simple_type, rev_type, term.Apply_I] 1));
+val reflect_type = result();
+
+(** preorder **)
+
+val preorder = standard (preorder_def RS def_term_rec);
+
+goalw Term.thy [preorder_def]
+ "!!t A. t: term(A) ==> preorder(t) : list(A)";
+by (REPEAT (ares_tac [term_rec_simple_type, list.Cons_I, flat_type] 1));
+val preorder_type = result();
+
+
+(** Term simplification **)
+
+val term_typechecks =
+ [term.Apply_I, term_map_type, term_map_type2, term_size_type,
+ reflect_type, preorder_type];
+
+(*map_type2 and term_map_type2 instantiate variables*)
+val term_ss = list_ss
+ addsimps [term_rec, term_map, term_size, reflect, preorder]
+ setsolver type_auto_tac (list_typechecks@term_typechecks);
+
+
+(** theorems about term_map **)
+
+goal Term.thy "!!t A. t: term(A) ==> term_map(%u.u, t) = t";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [map_ident]) 1);
+val term_map_ident = result();
+
+goal Term.thy
+ "!!t A. t: term(A) ==> term_map(f, term_map(g,t)) = term_map(%u.f(g(u)), t)";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
+val term_map_compose = result();
+
+goal Term.thy
+ "!!t A. t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose]) 1);
+val term_map_reflect = result();
+
+
+(** theorems about term_size **)
+
+goal Term.thy
+ "!!t A. t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [map_compose]) 1);
+val term_size_term_map = result();
+
+goal Term.thy "!!t A. t: term(A) ==> term_size(reflect(t)) = term_size(t)";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [rev_map_distrib RS sym, map_compose,
+ list_add_rev]) 1);
+val term_size_reflect = result();
+
+goal Term.thy "!!t A. t: term(A) ==> term_size(t) = length(preorder(t))";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [length_flat, map_compose]) 1);
+val term_size_length = result();
+
+
+(** theorems about reflect **)
+
+goal Term.thy "!!t A. t: term(A) ==> reflect(reflect(t)) = t";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [rev_map_distrib, map_compose,
+ map_ident, rev_rev_ident]) 1);
+val reflect_reflect_ident = result();
+
+
+(** theorems about preorder **)
+
+goal Term.thy
+ "!!t A. t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac (term_ss addsimps [map_compose, map_flat]) 1);
+val preorder_term_map = result();
+
+(** preorder(reflect(t)) = rev(postorder(t)) **)
+
+writeln"Reached end of file.";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ex/Term.thy Fri Aug 12 12:28:46 1994 +0200
@@ -0,0 +1,38 @@
+(* Title: ZF/ex/Term.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1994 University of Cambridge
+
+Terms over an alphabet.
+Illustrates the list functor (essentially the same type as in Trees & Forests)
+*)
+
+Term = List +
+consts
+ term_rec :: "[i, [i,i,i]=>i] => i"
+ term_map :: "[i=>i, i] => i"
+ term_size :: "i=>i"
+ reflect :: "i=>i"
+ preorder :: "i=>i"
+
+ term :: "i=>i"
+
+datatype
+ "term(A)" = Apply ("a: A", "l: list(term(A))")
+ monos "[list_mono]"
+ type_intrs "[list_univ RS subsetD]"
+
+rules
+ term_rec_def
+ "term_rec(t,d) == \
+\ Vrec(t, %t g. term_case(%x zs. d(x, zs, map(%z.g`z, zs)), t))"
+
+ term_map_def "term_map(f,t) == term_rec(t, %x zs rs. Apply(f(x), rs))"
+
+ term_size_def "term_size(t) == term_rec(t, %x zs rs. succ(list_add(rs)))"
+
+ reflect_def "reflect(t) == term_rec(t, %x zs rs. Apply(x, rev(rs)))"
+
+ preorder_def "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
+
+end