--- a/src/ZF/AC/AC16_WO4.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/AC/AC16_WO4.ML Wed Jan 13 11:57:09 1999 +0100
@@ -328,11 +328,10 @@
by (res_inst_tac
[("f3", "lam b:y-a. THE c. c: s(u) & a <= c & b:c")]
(exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
-by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1);
-by (rtac CollectI 1);
+by (simp_tac (simpset() addsimps [inj_def]) 1);
+by (rtac conjI 1);
by (rtac lam_type 1);
-by (forward_tac [ex1_superset_a RS theI] 1
- THEN REPEAT (Fast_tac 1));
+by (forward_tac [ex1_superset_a RS theI] 1 THEN REPEAT (Fast_tac 1));
by (Asm_simp_tac 1);
by (Clarify_tac 1);
by (rtac cons_eqE 1);
@@ -387,17 +386,16 @@
\ ==> {v:s(u). a <= v} lepoll {v:Pow(x). v eqpoll m}";
by (res_inst_tac [("f3","lam w:{v:s(u). a <= v}. w Int (x - {u})")]
(exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1);
-by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1);
-by (rtac CollectI 1);
+by (simp_tac (simpset() addsimps [inj_def]) 1);
+by (rtac conjI 1);
by (rtac lam_type 1);
by (rtac CollectI 1);
by (Fast_tac 1);
by (rtac w_Int_eqpoll_m 1 THEN REPEAT (assume_tac 1));
-by (simp_tac (simpset() delsimps ball_simps) 1);
by (REPEAT (resolve_tac [ballI, impI] 1));
-(** LEVEL 9 **)
-by (resolve_tac [w_Int_eqpoll_m RS eqpoll_m_not_empty RS not_emptyE] 1
- THEN REPEAT (assume_tac 1));
+(** LEVEL 8 **)
+by (resolve_tac [w_Int_eqpoll_m RS eqpoll_m_not_empty RS not_emptyE] 1);
+by (EVERY (map Blast_tac [4,3,2,1]));
by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1));
by (forward_tac [cons_cons_in] 1 THEN REPEAT (assume_tac 1));
by (etac ex1_two_eq 1);
--- a/src/ZF/AC/WO1_AC.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/AC/WO1_AC.ML Wed Jan 13 11:57:09 1999 +0100
@@ -56,9 +56,9 @@
by (fast_tac (claset() addSEs [well_ord_cardinal_eqpoll]) 2);
by (resolve_tac [eqpoll_sym RS eqpoll_trans] 1);
by (fast_tac (claset() addSEs [well_ord_cardinal_eqpoll]) 1);
-by (resolve_tac [cadd_def RS def_imp_eq RS subst] 1);
+by (fold_tac [cadd_def]);
by (resolve_tac [Card_cardinal RSN (2, Inf_Card_is_InfCard) RS
- InfCard_cdouble_eq RS ssubst] 1);
+ InfCard_cdouble_eq RS ssubst] 1);
by (rtac eqpoll_refl 2);
by (rtac notI 1);
by (etac notE 1);
--- a/src/ZF/Cardinal.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Cardinal.ML Wed Jan 13 11:57:09 1999 +0100
@@ -8,8 +8,6 @@
This theory does NOT assume the Axiom of Choice
*)
-open Cardinal;
-
(*** The Schroeder-Bernstein Theorem -- see Davey & Priestly, page 106 ***)
(** Lemma: Banach's Decomposition Theorem **)
@@ -457,11 +455,9 @@
by (rtac ballI 1);
by (eres_inst_tac [("n","n")] natE 1);
by (asm_simp_tac (simpset() addsimps [lepoll_def, inj_def,
- succI1 RS Pi_empty2]) 1);
+ succI1 RS Pi_empty2]) 1);
by (blast_tac (claset() addSIs [succ_leI] addSDs [succ_lepoll_succD]) 1);
-qed "nat_lepoll_imp_le_lemma";
-
-bind_thm ("nat_lepoll_imp_le", nat_lepoll_imp_le_lemma RS bspec RS mp);
+qed_spec_mp "nat_lepoll_imp_le";
Goal "[| m:nat; n: nat |] ==> m eqpoll n <-> m = n";
by (rtac iffI 1);
--- a/src/ZF/Coind/Language.thy Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Coind/Language.thy Wed Jan 13 11:57:09 1999 +0100
@@ -18,11 +18,12 @@
consts
Exp :: i (* Datatype of expressions *)
ExVar :: i (* Abstract type of variables *)
-datatype <= "univ(Const Un ExVar)"
- "Exp" = e_const("c:Const")
- | e_var("x:ExVar")
- | e_fn("x:ExVar","e:Exp")
- | e_fix("x1:ExVar","x2:ExVar","e:Exp")
- | e_app("e1:Exp","e2:Exp")
+
+datatype
+ "Exp" = e_const ("c:Const")
+ | e_var ("x:ExVar")
+ | e_fn ("x:ExVar","e:Exp")
+ | e_fix ("x1:ExVar","x2:ExVar","e:Exp")
+ | e_app ("e1:Exp","e2:Exp")
end
--- a/src/ZF/Coind/Types.thy Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Coind/Types.thy Wed Jan 13 11:57:09 1999 +0100
@@ -9,18 +9,20 @@
consts
Ty :: i (* Datatype of types *)
TyConst :: i (* Abstract type of type constants *)
-datatype <= "univ(TyConst)"
- "Ty" = t_const("tc:TyConst")
- | t_fun("t1:Ty","t2:Ty")
+
+datatype
+ "Ty" = t_const ("tc:TyConst")
+ | t_fun ("t1:Ty","t2:Ty")
(* Definition of type environments and associated operators *)
consts
TyEnv :: i
-datatype <= "univ(Ty Un ExVar)"
+
+datatype
"TyEnv" = te_emp
- | te_owr("te:TyEnv","x:ExVar","t:Ty")
+ | te_owr ("te:TyEnv","x:ExVar","t:Ty")
consts
te_dom :: i => i
--- a/src/ZF/Coind/Values.thy Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Coind/Values.thy Wed Jan 13 11:57:09 1999 +0100
@@ -10,11 +10,12 @@
consts
Val, ValEnv, Val_ValEnv :: i
-codatatype <= "quniv(Const Un ExVar Un Exp)"
- "Val" = v_const("c:Const")
- | v_clos("x:ExVar","e:Exp","ve:ValEnv")
+
+codatatype
+ "Val" = v_const ("c:Const")
+ | v_clos ("x:ExVar","e:Exp","ve:ValEnv")
and
- "ValEnv" = ve_mk("m:PMap(ExVar,Val)")
+ "ValEnv" = ve_mk ("m:PMap(ExVar,Val)")
monos "[map_mono]"
type_intrs "[A_into_univ, mapQU]"
--- a/src/ZF/Datatype.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Datatype.ML Wed Jan 13 11:57:09 1999 +0100
@@ -15,8 +15,9 @@
Pair_in_univ, Inl_in_univ, Inr_in_univ,
zero_in_univ, A_into_univ, nat_into_univ, UnCI];
- (*Needed for mutual recursion*)
- val elims = [make_elim InlD, make_elim InrD];
+
+ val elims = [make_elim InlD, make_elim InrD, (*for mutual recursion*)
+ SigmaE, sumE]; (*allows * and + in spec*)
end;
@@ -36,7 +37,8 @@
QPair_in_quniv, QInl_in_quniv, QInr_in_quniv,
zero_in_quniv, A_into_quniv, nat_into_quniv, UnCI];
- val elims = [make_elim QInlD, make_elim QInrD];
+ val elims = [make_elim QInlD, make_elim QInrD, (*for mutual recursion*)
+ QSigmaE, qsumE]; (*allows * and + in spec*)
end;
structure CoData_Package =
--- a/src/ZF/IMP/Com.thy Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/IMP/Com.thy Wed Jan 13 11:57:09 1999 +0100
@@ -78,7 +78,7 @@
(** Commands **)
consts com :: i
-datatype <= "univ(loc Un aexp Un bexp)"
+datatype
"com" = skip
| asgt ("x:loc", "a:aexp") (infixl 60)
| semic ("c0:com", "c1:com") ("_; _" [60, 60] 10)
--- a/src/ZF/Integ/Bin.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Integ/Bin.ML Wed Jan 13 11:57:09 1999 +0100
@@ -77,7 +77,7 @@
by (rename_tac "w'" 3);
by (induct_tac "w'" 3);
by Auto_tac;
-bind_thm ("bin_add_type", result() RS bspec);
+qed_spec_mp "bin_add_type";
Addsimps [bin_add_type];
Goal "[| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
@@ -169,8 +169,7 @@
by (rtac ballI 1);
by (induct_tac "wa" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE))));
-bind_thm("integ_of_add", result() RS bspec);
-
+qed_spec_mp "integ_of_add";
Addsimps [integ_of_add];
--- a/src/ZF/List.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/List.ML Wed Jan 13 11:57:09 1999 +0100
@@ -34,11 +34,11 @@
by (rtac lfp_lowerbound 1);
by (rtac (A_subset_univ RS univ_mono) 2);
by (blast_tac (claset() addSIs [zero_in_univ, Inl_in_univ, Inr_in_univ,
- Pair_in_univ]) 1);
+ Pair_in_univ]) 1);
qed "list_univ";
(*These two theorems justify datatypes involving list(nat), list(A), ...*)
-bind_thm ("list_subset_univ", ([list_mono, list_univ] MRS subset_trans));
+bind_thm ("list_subset_univ", [list_mono, list_univ] MRS subset_trans);
Goal "[| l: list(A); A <= univ(B) |] ==> l: univ(B)";
by (REPEAT (ares_tac [list_subset_univ RS subsetD] 1));
@@ -177,6 +177,7 @@
by (induct_tac "l" 1);
by (ALLGOALS Asm_simp_tac);
qed "map_ident";
+Addsimps [map_ident];
Goal "l: list(A) ==> map(h, map(j,l)) = map(%u. h(j(u)), l)";
by (induct_tac "l" 1);
@@ -203,7 +204,7 @@
(** theorems about list(Collect(A,P)) -- used in ex/term.ML **)
(* c : list(Collect(B,P)) ==> c : list(B) *)
-bind_thm ("list_CollectD", (Collect_subset RS list_mono RS subsetD));
+bind_thm ("list_CollectD", Collect_subset RS list_mono RS subsetD);
Goal "l: list({x:A. h(x)=j(x)}) ==> map(h,l) = map(j,l)";
by (induct_tac "l" 1);
@@ -222,13 +223,9 @@
by (ALLGOALS Asm_simp_tac);
qed "length_app";
-(* [| m: nat; n: nat |] ==> m #+ succ(n) = succ(n) #+ m
- Used for rewriting below*)
-val add_commute_succ = nat_succI RSN (2,add_commute);
-
Goal "xs: list(A) ==> length(rev(xs)) = length(xs)";
by (induct_tac "xs" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app, add_commute_succ])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [length_app])));
qed "length_rev";
Goal "ls: list(list(A)) ==> length(flat(ls)) = list_add(map(length,ls))";
@@ -244,22 +241,19 @@
by (etac list.induct 1);
by (ALLGOALS Asm_simp_tac);
by (Blast_tac 1);
-qed "drop_length_Cons_lemma";
-bind_thm ("drop_length_Cons", (drop_length_Cons_lemma RS spec));
+qed_spec_mp "drop_length_Cons";
-Goal "l: list(A) ==> ALL i: length(l). EX z zs. drop(i,l) = Cons(z,zs)";
+Goal "l: list(A) ==> ALL i:length(l). (EX z zs. drop(i,l) = Cons(z,zs))";
by (etac list.induct 1);
by (ALLGOALS Asm_simp_tac);
-by (rtac conjI 1);
+by Safe_tac;
by (etac drop_length_Cons 1);
-by (rtac ballI 1);
by (rtac natE 1);
by (etac ([asm_rl, length_type, Ord_nat] MRS Ord_trans) 1);
by (assume_tac 1);
by (ALLGOALS Asm_simp_tac);
by (ALLGOALS (blast_tac (claset() addIs [succ_in_naturalD, length_type])));
-qed "drop_length_lemma";
-bind_thm ("drop_length", (drop_length_lemma RS bspec));
+qed_spec_mp "drop_length";
(*** theorems about app ***)
@@ -268,6 +262,7 @@
by (etac list.induct 1);
by (ALLGOALS Asm_simp_tac);
qed "app_right_Nil";
+Addsimps [app_right_Nil];
Goal "xs: list(A) ==> (xs@ys)@zs = xs@(ys@zs)";
by (induct_tac "xs" 1);
@@ -292,18 +287,20 @@
*)
Goal "[| xs: list(A); ys: list(A) |] ==> rev(xs@ys) = rev(ys)@rev(xs)";
by (etac list.induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_right_Nil,app_assoc])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [app_assoc])));
qed "rev_app_distrib";
Goal "l: list(A) ==> rev(rev(l))=l";
by (induct_tac "l" 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [rev_app_distrib])));
qed "rev_rev_ident";
+Addsimps [rev_rev_ident];
Goal "ls: list(list(A)) ==> rev(flat(ls)) = flat(map(rev,rev(ls)))";
by (induct_tac "ls" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps
- [map_app_distrib, flat_app_distrib, rev_app_distrib, app_right_Nil])));
+by (ALLGOALS
+ (asm_simp_tac (simpset() addsimps
+ [map_app_distrib, flat_app_distrib, rev_app_distrib])));
qed "rev_flat";
--- a/src/ZF/OrdQuant.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/OrdQuant.ML Wed Jan 13 11:57:09 1999 +0100
@@ -5,8 +5,6 @@
Quantifiers and union operator for ordinals.
*)
-open OrdQuant;
-
(*** universal quantifier for ordinals ***)
qed_goalw "oallI" thy [oall_def]
--- a/src/ZF/QPair.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/QPair.ML Wed Jan 13 11:57:09 1999 +0100
@@ -122,11 +122,9 @@
(*** Eliminator - qsplit ***)
(*A META-equality, so that it applies to higher types as well...*)
-qed_goalw "qsplit" thy [qsplit_def]
- "qsplit(%x y. c(x,y), <a;b>) == c(a,b)"
- (fn _ => [ (Simp_tac 1),
- (rtac reflexive_thm 1) ]);
-
+Goalw [qsplit_def] "qsplit(%x y. c(x,y), <a;b>) == c(a,b)";
+by (Simp_tac 1);
+qed "qsplit";
Addsimps [qsplit];
qed_goal "qsplit_type" thy
--- a/src/ZF/QUniv.thy Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/QUniv.thy Wed Jan 13 11:57:09 1999 +0100
@@ -8,8 +8,20 @@
QUniv = Univ + QPair + mono + equalities +
+(*Disjoint sums as a datatype*)
+rep_datatype
+ elim sumE
+ induct TrueI
+ case_eqns case_Inl, case_Inr
+
+(*Variant disjoint sums as a datatype*)
+rep_datatype
+ elim qsumE
+ induct TrueI
+ case_eqns qcase_QInl, qcase_QInr
+
constdefs
quniv :: i => i
- "quniv(A) == Pow(univ(eclose(A)))"
+ "quniv(A) == Pow(univ(eclose(A)))"
end
--- a/src/ZF/ROOT.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ROOT.ML Wed Jan 13 11:57:09 1999 +0100
@@ -28,10 +28,10 @@
use_thy "Fixedpt";
use "Tools/inductive_package";
use_thy "Inductive";
-use "Tools/induct_tacs";
-use "Tools/primrec_package";
+use "Tools/induct_tacs";
+use "Tools/primrec_package";
use_thy "QUniv";
-use "Tools/datatype_package";
+use "Tools/datatype_package";
use_thy "Datatype";
use_thy "InfDatatype";
use_thy "List";
--- a/src/ZF/Resid/Redex.thy Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Resid/Redex.thy Wed Jan 13 11:57:09 1999 +0100
@@ -13,8 +13,6 @@
"redexes" = Var ("n: nat")
| Fun ("t: redexes")
| App ("b:bool" ,"f:redexes" , "a:redexes")
- type_intrs "[bool_into_univ]"
-
consts
--- a/src/ZF/Resid/Substitution.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Resid/Substitution.ML Wed Jan 13 11:57:09 1999 +0100
@@ -107,13 +107,13 @@
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [lift_rec_Var,
lift_rec_Fun, lift_rec_App])));
-bind_thm ("lift_rec_type", result() RS bspec);
+qed_spec_mp "lift_rec_type";
Goal "v:redexes ==> ALL n:nat. ALL u:redexes. subst_rec(u,v,n):redexes";
by (etac redexes.induct 1);
by (ALLGOALS(asm_simp_tac
(simpset() addsimps [subst_Var, lift_rec_type])));
-bind_thm ("subst_type", result() RS bspec RS bspec);
+qed_spec_mp "subst_type";
Addsimps [subst_eq, subst_gt, subst_lt, subst_type,
--- a/src/ZF/Resid/Terms.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Resid/Terms.ML Wed Jan 13 11:57:09 1999 +0100
@@ -30,13 +30,12 @@
Goal "v:lambda ==> ALL k:nat. lift_rec(v,k):lambda";
by (etac lambda.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [lift_rec_Var])));
-bind_thm ("liftL_type", result() RS bspec);
+qed_spec_mp "liftL_type";
Goal "v:lambda ==> ALL n:nat. ALL u:lambda. subst_rec(u,v,n):lambda";
by (etac lambda.induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [liftL_type,subst_Var])));
-qed "substL_typea";
-bind_thm ("substL_type", result() RS bspec RS bspec);
+qed_spec_mp "substL_type";
(* ------------------------------------------------------------------------- *)
--- a/src/ZF/Tools/datatype_package.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Tools/datatype_package.ML Wed Jan 13 11:57:09 1999 +0100
@@ -19,7 +19,7 @@
recursor_eqns : thm list, (*equations for the recursor*)
free_iffs : thm list, (*freeness rewrite rules*)
free_SEs : thm list, (*freeness destruct rules*)
- mk_free : string -> thm}; (*makes freeness theorems*)
+ mk_free : string -> thm}; (*function to make freeness theorems*)
signature DATATYPE_ARG =
@@ -302,7 +302,7 @@
(cterm_of (sign_of thy1) (mk_case_eqn arg)))
(case_tacsf con_def);
- val con_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
+ val free_iffs = con_defs RL [Ind_Syntax.def_swap_iff];
val case_eqns =
map prove_case_eqn
@@ -353,10 +353,7 @@
val constructors =
map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
- val free_iffs = con_iffs @
- [Su.distinct, Su.distinct', Su.inl_iff, Su.inr_iff, Pr.pair_iff];
-
- val free_SEs = Ind_Syntax.mk_free_SEs con_iffs @ Su.free_SEs;
+ val free_SEs = Ind_Syntax.mk_free_SEs free_iffs;
val {elim, induct, mutual_induct, ...} = ind_result
@@ -366,7 +363,7 @@
prove_goalw (theory_of_thm elim) (*Don't use thy1: it will be stale*)
con_defs s
(fn prems => [cut_facts_tac prems 1,
- fast_tac (ZF_cs addSEs free_SEs) 1]);
+ fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]);
val simps = case_eqns @ recursor_eqns;
@@ -413,11 +410,12 @@
monos, type_intrs, type_elims) thy =
let val sign = sign_of thy
val rec_tms = map (readtm sign Ind_Syntax.iT) srec_tms
+ val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists
val dom_sum =
if sdom = "" then
- Ind_Syntax.data_domain (#1 (dest_Const Fp.oper) <> "Fixedpt.lfp") rec_tms
+ Ind_Syntax.data_domain (#1(dest_Const Fp.oper) <> "Fixedpt.lfp")
+ (rec_tms, con_ty_lists)
else readtm sign Ind_Syntax.iT sdom
- and con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists
in
add_datatype_i (dom_sum, rec_tms, con_ty_lists,
monos, type_intrs, type_elims) thy
--- a/src/ZF/Tools/induct_tacs.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Wed Jan 13 11:57:09 1999 +0100
@@ -111,7 +111,9 @@
if exh then #exhaustion (datatype_info_sg sign tn)
else #induct (datatype_info_sg sign tn)
val (Const("op :",_) $ Var(ixn,_) $ _) =
- FOLogic.dest_Trueprop (hd (prems_of rule))
+ (case prems_of rule of
+ [] => error "induction is not available for this datatype"
+ | major::_ => FOLogic.dest_Trueprop major)
val ind_vname = Syntax.string_of_vname ixn
val vname' = (*delete leading question mark*)
String.substring (ind_vname, 1, size ind_vname-1)
@@ -139,9 +141,11 @@
map (head_of o const_of o FOLogic.dest_Trueprop o
#prop o rep_thm) case_eqns;
- val Const ("op :", _) $ _ $ Const(big_rec_name, _) =
+ val Const ("op :", _) $ _ $ data =
FOLogic.dest_Trueprop (hd (prems_of elim));
+ val Const(big_rec_name, _) = head_of data;
+
val simps = case_eqns @ recursor_eqns;
val dt_info =
--- a/src/ZF/Tools/typechk.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/Tools/typechk.ML Wed Jan 13 11:57:09 1999 +0100
@@ -29,5 +29,6 @@
drawback: does not simplify conjunctions*)
fun type_auto_tac tyrls hyps = SELECT_GOAL
(DEPTH_SOLVE (typechk_step_tac (tyrls@hyps)
- ORELSE ares_tac [TrueI,refl,iff_refl,ballI,allI,conjI,impI] 1));
+ ORELSE ares_tac [TrueI,refl,reflexive_thm,iff_refl,
+ ballI,allI,conjI,impI] 1));
--- a/src/ZF/WF.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/WF.ML Wed Jan 13 11:57:09 1999 +0100
@@ -203,8 +203,8 @@
(** r-``{a} is the set of everything under a in r **)
-bind_thm ("underI", (vimage_singleton_iff RS iffD2));
-bind_thm ("underD", (vimage_singleton_iff RS iffD1));
+bind_thm ("underI", vimage_singleton_iff RS iffD2);
+bind_thm ("underD", vimage_singleton_iff RS iffD1);
(** is_recfun **)
@@ -223,7 +223,7 @@
(*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE
spec RS mp instantiates induction hypotheses*)
fun indhyp_tac hyps =
- resolve_tac (TrueI::refl::hyps) ORELSE'
+ resolve_tac (TrueI::refl::reflexive_thm::hyps) ORELSE'
(cut_facts_tac hyps THEN'
DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE'
eresolve_tac [underD, transD, spec RS mp]));
@@ -238,8 +238,7 @@
by (REPEAT (rtac impI 1 ORELSE etac ssubst 1));
by (rewtac restrict_def);
by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1);
-qed "is_recfun_equal_lemma";
-bind_thm ("is_recfun_equal", (is_recfun_equal_lemma RS mp RS mp));
+qed_spec_mp "is_recfun_equal";
val prems as [wfr,transr,recf,recg,_] = goal WF.thy
"[| wf(r); trans(r); \
--- a/src/ZF/ex/BT.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/BT.ML Wed Jan 13 11:57:09 1999 +0100
@@ -8,6 +8,17 @@
Addsimps bt.intrs;
+Goal "l : bt(A) ==> ALL x r. Br(x,l,r) ~= l";
+by (induct_tac "l" 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps bt.free_iffs)));
+qed_spec_mp "Br_neq_left";
+
+(*Proving a freeness theorem*)
+val Br_iff = bt.mk_free "Br(a,l,r) = Br(a',l',r') <-> a=a' & l=l' & r=r'";
+
+(*An elimination rule, for type-checking*)
+val BrE = bt.mk_cases bt.con_defs "Br(a,l,r) : bt(A)";
+
(** Lemmas to justify using "bt" in other recursive type definitions **)
Goalw bt.defs "A<=B ==> bt(A) <= bt(B)";
@@ -26,7 +37,7 @@
bind_thm ("bt_subset_univ", [bt_mono, bt_univ] MRS subset_trans);
-(*Type checking -- proved by induction, as usual*)
+(*Type checking for recursor -- example only; not really needed*)
val major::prems = goal BT.thy
"[| t: bt(A); \
\ c: C(Lf); \
@@ -58,14 +69,13 @@
Goal "t: bt(A) ==> bt_reflect(t) : bt(A)";
by (induct_tac "t" 1);
by Auto_tac;
-by (REPEAT (ares_tac (bt.intrs @ [bt_rec_type]) 1));
qed "bt_reflect_type";
(** BT simplification **)
-Addsimps [bt_rec_type, n_nodes_type, n_leaves_type, bt_reflect_type];
+Addsimps [n_nodes_type, n_leaves_type, bt_reflect_type];
(*** theorems about n_leaves ***)
--- a/src/ZF/ex/BT.thy Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/BT.thy Wed Jan 13 11:57:09 1999 +0100
@@ -6,18 +6,18 @@
Binary trees
*)
-BT = Datatype +
+BT = Main +
+consts
+ bt :: i=>i
+
+datatype
+ "bt(A)" = Lf | Br ("a: A", "t1: bt(A)", "t2: bt(A)")
+
consts
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)")
-
-
primrec
"n_nodes(Lf) = 0"
"n_nodes(Br(a,l,r)) = succ(n_nodes(l) #+ n_nodes(r))"
--- a/src/ZF/ex/Ntree.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/Ntree.ML Wed Jan 13 11:57:09 1999 +0100
@@ -9,8 +9,6 @@
Based upon ex/Term.ML
*)
-open Ntree;
-
(** ntree **)
Goal "ntree(A) = A * (UN n: nat. n -> ntree(A))";
--- a/src/ZF/ex/Primrec.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/Primrec.ML Wed Jan 13 11:57:09 1999 +0100
@@ -70,8 +70,7 @@
by (etac (succ_leI RS lt_trans1) 2);
by (rtac (nat_0I RS nat_0_le RS lt_trans) 1);
by Auto_tac;
-qed "lt_ack2_lemma";
-bind_thm ("lt_ack2", (lt_ack2_lemma RS bspec));
+qed_spec_mp "lt_ack2";
(*PROPERTY A 5-, the single-step lemma*)
Goal "[| i:nat; j:nat |] ==> ack(i,j) < ack(i, succ(j))";
--- a/src/ZF/ex/Ramsey.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/Ramsey.ML Wed Jan 13 11:57:09 1999 +0100
@@ -103,11 +103,7 @@
(*proving the condition*)
by (Asm_simp_tac 1);
by (etac Atleast_superset 1 THEN Fast_tac 1);
-qed "pigeon2_lemma";
-
-(* [| m:nat; n:nat; Atleast(m #+ n #- succ(0), A Un B) |] ==>
- Atleast(m,A) | Atleast(n,B) *)
-bind_thm ("pigeon2", (pigeon2_lemma RS bspec RS spec RS spec RS mp));
+qed_spec_mp "pigeon2";
(**** Ramsey's Theorem ****)
--- a/src/ZF/ex/TF.thy Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/TF.thy Wed Jan 13 11:57:09 1999 +0100
@@ -8,6 +8,15 @@
TF = List +
consts
+ 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)")
+
+
+consts
map :: [i=>i, i] => i
size :: i=>i
preorder :: i=>i
@@ -15,13 +24,6 @@
of_list :: i=>i
reflect :: 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)")
-
primrec
"list_of_TF (Tcons(x,f)) = [Tcons(x,f)]"
"list_of_TF (Fnil) = []"
--- a/src/ZF/ex/Term.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/Term.ML Wed Jan 13 11:57:09 1999 +0100
@@ -7,8 +7,6 @@
Illustrates the list functor (essentially the same type as in Trees & Forests)
*)
-open Term;
-
Goal "term(A) = A * list(term(A))";
let open term; val rew = rewrite_rule con_defs in
by (fast_tac (claset() addSIs (map rew intrs) addEs [rew elim]) 1)
@@ -121,7 +119,7 @@
(** term_map **)
-bind_thm ("term_map", (term_map_def RS def_term_rec));
+bind_thm ("term_map", term_map_def RS def_term_rec);
val prems = Goalw [term_map_def]
"[| t: term(A); !!x. x: A ==> f(x): B |] ==> term_map(f,t) : term(B)";
@@ -136,7 +134,7 @@
(** term_size **)
-bind_thm ("term_size", (term_size_def RS def_term_rec));
+bind_thm ("term_size", term_size_def RS def_term_rec);
Goalw [term_size_def] "t: term(A) ==> term_size(t) : nat";
by (REPEAT (ares_tac [term_rec_simple_type, list_add_type, nat_succI] 1));
@@ -145,7 +143,7 @@
(** reflect **)
-bind_thm ("reflect", (reflect_def RS def_term_rec));
+bind_thm ("reflect", reflect_def RS def_term_rec);
Goalw [reflect_def] "t: term(A) ==> reflect(t) : term(A)";
by (REPEAT (ares_tac [term_rec_simple_type, rev_type, term.Apply_I] 1));
@@ -153,41 +151,53 @@
(** preorder **)
-bind_thm ("preorder", (preorder_def RS def_term_rec));
+bind_thm ("preorder", preorder_def RS def_term_rec);
Goalw [preorder_def]
"t: term(A) ==> preorder(t) : list(A)";
by (REPEAT (ares_tac [term_rec_simple_type, list.Cons_I, flat_type] 1));
qed "preorder_type";
+(** postorder **)
+
+bind_thm ("postorder", postorder_def RS def_term_rec);
+
+Goalw [postorder_def]
+ "t: term(A) ==> postorder(t) : list(A)";
+by (REPEAT (ares_tac [term_rec_simple_type] 1));
+by (Asm_simp_tac 1);
+qed "postorder_type";
+
(** Term simplification **)
val term_typechecks =
[term.Apply_I, term_map_type, term_map_type2, term_size_type,
- reflect_type, preorder_type];
+ reflect_type, preorder_type, postorder_type];
(*map_type2 and term_map_type2 instantiate variables*)
simpset_ref() := simpset()
- addsimps [term_rec, term_map, term_size, reflect, preorder]
+ addsimps [term_rec, term_map, term_size, reflect, preorder, postorder]
setSolver type_auto_tac (list_typechecks@term_typechecks);
(** theorems about term_map **)
+Addsimps [thm "List.map_compose"]; (*there is also TF.map_compose*)
+
Goal "t: term(A) ==> term_map(%u. u, t) = t";
by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [map_ident]) 1);
+by (Asm_simp_tac 1);
qed "term_map_ident";
Goal "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 (simpset() addsimps [map_compose]) 1);
+by (asm_simp_tac (simpset() addsimps []) 1);
qed "term_map_compose";
Goal "t: term(A) ==> term_map(f, reflect(t)) = reflect(term_map(f,t))";
by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym, map_compose]) 1);
+by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym]) 1);
qed "term_map_reflect";
@@ -195,18 +205,17 @@
Goal "t: term(A) ==> term_size(term_map(f,t)) = term_size(t)";
by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [map_compose]) 1);
+by (asm_simp_tac (simpset() addsimps []) 1);
qed "term_size_term_map";
Goal "t: term(A) ==> term_size(reflect(t)) = term_size(t)";
by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [rev_map_distrib RS sym, map_compose,
- list_add_rev]) 1);
+by (asm_simp_tac(simpset() addsimps [rev_map_distrib RS sym, list_add_rev]) 1);
qed "term_size_reflect";
Goal "t: term(A) ==> term_size(t) = length(preorder(t))";
by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [length_flat, map_compose]) 1);
+by (asm_simp_tac (simpset() addsimps [length_flat]) 1);
qed "term_size_length";
@@ -214,8 +223,7 @@
Goal "t: term(A) ==> reflect(reflect(t)) = t";
by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [rev_map_distrib, map_compose,
- map_ident, rev_rev_ident]) 1);
+by (asm_simp_tac (simpset() addsimps [rev_map_distrib]) 1);
qed "reflect_reflect_ident";
@@ -223,9 +231,14 @@
Goal "t: term(A) ==> preorder(term_map(f,t)) = map(f, preorder(t))";
by (etac term_induct_eqn 1);
-by (asm_simp_tac (simpset() addsimps [map_compose, map_flat]) 1);
+by (asm_simp_tac (simpset() addsimps [map_flat]) 1);
qed "preorder_term_map";
-(** preorder(reflect(t)) = rev(postorder(t)) **)
+Goal "t: term(A) ==> preorder(reflect(t)) = rev(postorder(t))";
+by (etac term_induct_eqn 1);
+by (asm_simp_tac(simpset() addsimps [rev_app_distrib, rev_flat,
+ rev_map_distrib RS sym]) 1);
+qed "preorder_reflect_eq_rev_postorder";
+
writeln"Reached end of file.";
--- a/src/ZF/ex/Term.thy Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ex/Term.thy Wed Jan 13 11:57:09 1999 +0100
@@ -9,12 +9,6 @@
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
@@ -26,6 +20,14 @@
type_intrs "[list_univ RS subsetD]"
*)
+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
+ postorder :: i=>i
+
defs
term_rec_def
"term_rec(t,d) ==
@@ -39,4 +41,6 @@
preorder_def "preorder(t) == term_rec(t, %x zs rs. Cons(x, flat(rs)))"
+ postorder_def "postorder(t) == term_rec(t, %x zs rs. flat(rs) @ [x])"
+
end
--- a/src/ZF/ind_syntax.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/ind_syntax.ML Wed Jan 13 11:57:09 1999 +0100
@@ -107,17 +107,32 @@
and quniv = Const("QUniv.quniv", iT-->iT);
(*Make a datatype's domain: form the union of its set parameters*)
-fun union_params rec_tm =
+fun union_params (rec_tm, cs) =
let val (_,args) = strip_comb rec_tm
- in case (filter (fn arg => type_of arg = iT) args) of
- [] => empty
- | iargs => fold_bal (app Un) iargs
+ fun is_ind arg = (type_of arg = iT)
+ in case filter is_ind (args @ cs) of
+ [] => empty
+ | u_args => fold_bal (app Un) u_args
end;
-(*Previously these both did replicate (length rec_tms); however now
- [q]univ itself constitutes the sum domain for mutual recursion!*)
-fun data_domain false rec_tms = univ $ union_params (hd rec_tms)
- | data_domain true rec_tms = quniv $ union_params (hd rec_tms);
+(*univ or quniv constitutes the sum domain for mutual recursion;
+ it is applied to the datatype parameters and to Consts occurring in the
+ definition other than Nat.nat and the datatype sets themselves.
+ FIXME: could insert all constant set expressions, e.g. nat->nat.*)
+fun data_domain co (rec_tms, con_ty_lists) =
+ let val rec_names = (*nat doesn't have to be added*)
+ "Nat.nat" :: map (#1 o dest_Const o head_of) rec_tms
+ val u = if co then quniv else univ
+ fun is_OK (Const(a,T)) = not (a mem_string rec_names)
+ | is_OK _ = false
+ val add_term_consts_2 =
+ foldl_aterms (fn (cs, Const c) => Const c ins cs | (cs, _) => cs);
+ fun fourth (_, name, args, prems) = prems
+ fun add_consts_in_cts cts =
+ foldl (foldl add_term_consts_2) ([], map fourth (flat cts));
+ val cs = filter is_OK (add_consts_in_cts con_ty_lists)
+ in u $ union_params (hd rec_tms, cs) end;
+
(*Could go to FOL, but it's hardly general*)
val def_swap_iff = prove_goal IFOL.thy "a==b ==> a=c <-> c=b"
@@ -141,3 +156,6 @@
end;
+
+(*For convenient access by the user*)
+val trace_induct = Ind_Syntax.trace;
--- a/src/ZF/pair.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/pair.ML Wed Jan 13 11:57:09 1999 +0100
@@ -135,10 +135,9 @@
(*** Eliminator - split ***)
(*A META-equality, so that it applies to higher types as well...*)
-qed_goalw "split" thy [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)"
- (fn _ => [ (Simp_tac 1),
- (rtac reflexive_thm 1) ]);
-
+Goalw [split_def] "split(%x y. c(x,y), <a,b>) == c(a,b)";
+by (Simp_tac 1);
+qed "split";
Addsimps [split];
qed_goal "split_type" thy
--- a/src/ZF/thy_syntax.ML Wed Jan 13 11:56:28 1999 +0100
+++ b/src/ZF/thy_syntax.ML Wed Jan 13 11:57:09 1999 +0100
@@ -140,7 +140,7 @@
(("elim" $$-- ident) --
("induct" $$-- ident) --
("case_eqns" $$-- list1 ident) --
- ("recursor_eqns" $$-- list1 ident)) >> mk_rep_dt_string;
+ optional ("recursor_eqns" $$-- list1 ident) []) >> mk_rep_dt_string;
(** primrec **)