--- a/src/ZF/Inductive_ZF.thy Sat Mar 01 14:10:14 2008 +0100
+++ b/src/ZF/Inductive_ZF.thy Sat Mar 01 14:10:15 2008 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/Inductive.thy
+(* Title: ZF/Inductive_ZF.thy
ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
@@ -12,14 +12,31 @@
header{*Inductive and Coinductive Definitions*}
-theory Inductive_ZF imports Fixedpt QPair Nat_ZF
- uses
- "ind_syntax.ML"
- "Tools/cartprod.ML"
- "Tools/ind_cases.ML"
- "Tools/inductive_package.ML"
- "Tools/induct_tacs.ML"
- "Tools/primrec_package.ML" begin
+theory Inductive_ZF
+imports Fixedpt QPair Nat_ZF
+uses
+ ("ind_syntax.ML")
+ ("Tools/cartprod.ML")
+ ("Tools/ind_cases.ML")
+ ("Tools/inductive_package.ML")
+ ("Tools/induct_tacs.ML")
+ ("Tools/primrec_package.ML")
+begin
+
+lemma def_swap_iff: "a == b ==> a = c <-> c = b"
+ by blast
+
+lemma def_trans: "f == g ==> g(a) = b ==> f(a) = b"
+ by simp
+
+lemma refl_thin: "!!P. a = a ==> P ==> P" .
+
+use "ind_syntax.ML"
+use "Tools/cartprod.ML"
+use "Tools/ind_cases.ML"
+use "Tools/inductive_package.ML"
+use "Tools/induct_tacs.ML"
+use "Tools/primrec_package.ML"
setup IndCases.setup
setup DatatypeTactics.setup
@@ -30,8 +47,8 @@
structure Lfp =
struct
- val oper = Const("Fixedpt.lfp", [iT,iT-->iT]--->iT)
- val bnd_mono = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
+ val oper = @{const lfp}
+ val bnd_mono = @{const bnd_mono}
val bnd_monoI = @{thm bnd_monoI}
val subs = @{thm def_lfp_subset}
val Tarski = @{thm def_lfp_unfold}
@@ -40,9 +57,9 @@
structure Standard_Prod =
struct
- val sigma = Const("Sigma", [iT, iT-->iT]--->iT)
- val pair = Const("Pair", [iT,iT]--->iT)
- val split_name = "split"
+ val sigma = @{const Sigma}
+ val pair = @{const Pair}
+ val split_name = @{const_name split}
val pair_iff = @{thm Pair_iff}
val split_eq = @{thm split}
val fsplitI = @{thm splitI}
@@ -54,10 +71,10 @@
structure Standard_Sum =
struct
- val sum = Const(@{const_name sum}, [iT,iT]--->iT)
- val inl = Const("Inl", iT-->iT)
- val inr = Const("Inr", iT-->iT)
- val elim = Const("case", [iT-->iT, iT-->iT, iT]--->iT)
+ val sum = @{const sum}
+ val inl = @{const Inl}
+ val inr = @{const Inr}
+ val elim = @{const case}
val case_inl = @{thm case_Inl}
val case_inr = @{thm case_Inr}
val inl_iff = @{thm Inl_iff}
@@ -77,8 +94,8 @@
structure Gfp =
struct
- val oper = Const("Fixedpt.gfp", [iT,iT-->iT]--->iT)
- val bnd_mono = Const("Fixedpt.bnd_mono", [iT,iT-->iT]--->oT)
+ val oper = @{const gfp}
+ val bnd_mono = @{const bnd_mono}
val bnd_monoI = @{thm bnd_monoI}
val subs = @{thm def_gfp_subset}
val Tarski = @{thm def_gfp_unfold}
@@ -87,9 +104,9 @@
structure Quine_Prod =
struct
- val sigma = Const("QPair.QSigma", [iT, iT-->iT]--->iT)
- val pair = Const("QPair.QPair", [iT,iT]--->iT)
- val split_name = "QPair.qsplit"
+ val sigma = @{const QSigma}
+ val pair = @{const QPair}
+ val split_name = @{const_name qsplit}
val pair_iff = @{thm QPair_iff}
val split_eq = @{thm qsplit}
val fsplitI = @{thm qsplitI}
@@ -101,10 +118,10 @@
structure Quine_Sum =
struct
- val sum = Const("QPair.op <+>", [iT,iT]--->iT)
- val inl = Const("QPair.QInl", iT-->iT)
- val inr = Const("QPair.QInr", iT-->iT)
- val elim = Const("QPair.qcase", [iT-->iT, iT-->iT, iT]--->iT)
+ val sum = @{const qsum}
+ val inl = @{const QInl}
+ val inr = @{const QInr}
+ val elim = @{const qcase}
val case_inl = @{thm qcase_QInl}
val case_inr = @{thm qcase_QInr}
val inl_iff = @{thm QInl_iff}
--- a/src/ZF/Tools/cartprod.ML Sat Mar 01 14:10:14 2008 +0100
+++ b/src/ZF/Tools/cartprod.ML Sat Mar 01 14:10:15 2008 +0100
@@ -69,13 +69,14 @@
(*Bogus product type underlying a (possibly nested) Sigma.
Lets us share HOL code*)
fun pseudo_type (t $ A $ Abs(_,_,B)) =
- if t = Pr.sigma then mk_prod(pseudo_type A, pseudo_type B)
- else Ind_Syntax.iT
- | pseudo_type _ = Ind_Syntax.iT;
+ if t = Pr.sigma
+ then mk_prod(pseudo_type A, pseudo_type B)
+ else @{typ i}
+ | pseudo_type _ = @{typ i};
(*Maps the type T1*...*Tn to [T1,...,Tn], however nested*)
-fun factors (Type("*", [T1,T2])) = factors T1 @ factors T2
- | factors T = [T];
+fun factors (Type("*", [T1, T2])) = factors T1 @ factors T2
+ | factors T = [T];
(*Make a well-typed instance of "split"*)
fun split_const T = Const(Pr.split_name,
--- a/src/ZF/Tools/datatype_package.ML Sat Mar 01 14:10:14 2008 +0100
+++ b/src/ZF/Tools/datatype_package.ML Sat Mar 01 14:10:15 2008 +0100
@@ -46,6 +46,23 @@
(*con_ty_lists specifies the constructors in the form (name, prems, mixfix) *)
+(*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_hds = map head_of rec_tms
+ val dummy = assert_all is_Const rec_hds
+ (fn t => "Datatype set not previously declared as constant: " ^
+ Sign.string_of_term @{theory IFOL} t);
+ val rec_names = (*nat doesn't have to be added*)
+ @{const_name nat} :: map (#1 o dest_Const) rec_hds
+ val u = if co then @{const QUniv.quniv} else @{const Univ.univ}
+ val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
+ (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t
+ | _ => I)) con_ty_lists [];
+ in u $ Ind_Syntax.union_params (hd rec_tms, cs) end;
+
fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy =
let
val dummy = (*has essential ancestors?*)
@@ -149,7 +166,7 @@
Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
(*a recursive call for x is the application rec`x *)
- val rec_call = Ind_Syntax.apply_const $ Free ("rec", iT);
+ val rec_call = @{const apply} $ Free ("rec", iT);
(*look back down the "case args" (which have been reversed) to
determine the de Bruijn index*)
@@ -220,7 +237,7 @@
val recursor_def =
PrimitiveDefs.mk_defpair
(recursor_tm,
- Ind_Syntax.Vrecursor_const $
+ @{const Univ.Vrecursor} $
absfree ("rec", iT, list_comb (case_const, recursor_cases)));
(* Build the new theory *)
@@ -267,8 +284,8 @@
args)),
list_comb (case_free, args)));
- val case_trans = hd con_defs RS Ind_Syntax.def_trans
- and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
+ val case_trans = hd con_defs RS @{thm def_trans}
+ and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS @{thm trans};
fun prove_case_eqn (arg, con_def) =
Goal.prove_global thy1 [] []
@@ -279,7 +296,7 @@
rtac case_trans 1,
REPEAT (resolve_tac [refl, split_trans, Su.case_inl RS trans, Su.case_inr RS trans] 1)]);
- val free_iffs = map standard (con_defs RL [Ind_Syntax.def_swap_iff]);
+ val free_iffs = map standard (con_defs RL [@{thm def_swap_iff}]);
val case_eqns =
map prove_case_eqn
@@ -393,7 +410,7 @@
val rec_tms = map read_i srec_tms;
val con_ty_lists = Ind_Syntax.read_constructs thy scon_ty_lists;
val dom_sum =
- if sdom = "" then Ind_Syntax.data_domain coind (rec_tms, con_ty_lists)
+ if sdom = "" then data_domain coind (rec_tms, con_ty_lists)
else read_i sdom;
val monos = Attrib.eval_thms ctxt raw_monos;
val type_intrs = Attrib.eval_thms ctxt raw_type_intrs;
--- a/src/ZF/Tools/inductive_package.ML Sat Mar 01 14:10:14 2008 +0100
+++ b/src/ZF/Tools/inductive_package.ML Sat Mar 01 14:10:15 2008 +0100
@@ -65,6 +65,7 @@
intr_specs (monos, con_defs, type_intrs, type_elims) thy =
let
val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
+ val ctxt = ProofContext.init thy;
val (intr_names, intr_tms) = split_list (map fst intr_specs);
val case_names = RuleCases.case_names intr_names;
@@ -74,7 +75,7 @@
val dummy = assert_all is_Const rec_hds
(fn t => "Recursive set not previously declared as constant: " ^
- Sign.string_of_term thy t);
+ Syntax.string_of_term ctxt t);
(*Now we know they are all Consts, so get their names, type and params*)
val rec_names = map (#1 o dest_Const) rec_hds
@@ -91,12 +92,12 @@
in
val dummy = assert_all intr_ok intr_sets
(fn t => "Conclusion of rule does not name a recursive set: " ^
- Sign.string_of_term thy t);
+ Syntax.string_of_term ctxt t);
end;
val dummy = assert_all is_Free rec_params
(fn t => "Param in recursion term not a free variable: " ^
- Sign.string_of_term thy t);
+ Syntax.string_of_term ctxt t);
(*** Construct the fixedpoint definition ***)
val mk_variant = Name.variant (foldr add_term_names [] intr_tms);
@@ -105,7 +106,7 @@
fun dest_tprop (Const("Trueprop",_) $ P) = P
| dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
- Sign.string_of_term thy Q);
+ Syntax.string_of_term ctxt Q);
(*Makes a disjunct from an introduction rule*)
fun fp_part intr = (*quantify over rule's free vars except parameters*)
@@ -119,7 +120,7 @@
(*The Part(A,h) terms -- compose injections to make h*)
fun mk_Part (Bound 0) = Free(X',iT) (*no mutual rec, no Part needed*)
- | mk_Part h = Part_const $ Free(X',iT) $ Abs(w',iT,h);
+ | mk_Part h = @{const Part} $ Free(X',iT) $ Abs(w',iT,h);
(*Access to balanced disjoint sums via injections*)
val parts = map mk_Part
@@ -166,14 +167,16 @@
(*tracing: print the fixedpoint definition*)
val dummy = if !Ind_Syntax.trace then
- List.app (writeln o Sign.string_of_term thy o #2) axpairs
+ writeln (cat_lines (map (Syntax.string_of_term ctxt o #2) axpairs))
else ()
(*add definitions of the inductive sets*)
val (_, thy1) =
thy
|> Sign.add_path big_rec_base_name
- |> PureThy.add_defs_i false (map Thm.no_attributes axpairs)
+ |> PureThy.add_defs_i false (map Thm.no_attributes axpairs);
+
+ val ctxt1 = ProofContext.init thy1;
(*fetch fp definitions from the theory*)
@@ -224,7 +227,7 @@
DEPTH_SOLVE_1 (resolve_tac [refl,exI,conjI] 2 APPEND assume_tac 2),
(*Now solve the equations like Tcons(a,f) = Inl(?b4)*)
rewrite_goals_tac con_defs,
- REPEAT (rtac refl 2),
+ REPEAT (rtac @{thm refl} 2),
(*Typechecking; this can fail*)
if !Ind_Syntax.trace then print_tac "The type-checking subgoal:"
else all_tac,
@@ -238,7 +241,9 @@
(*combines disjI1 and disjI2 to get the corresponding nested disjunct...*)
val mk_disj_rls = BalancedTree.accesses
- {left = fn rl => rl RS disjI1, right = fn rl => rl RS disjI2, init = asm_rl};
+ {left = fn rl => rl RS @{thm disjI1},
+ right = fn rl => rl RS @{thm disjI2},
+ init = @{thm asm_rl}};
val intrs =
(intr_tms, map intro_tacsf (mk_disj_rls (length intr_tms)))
@@ -285,13 +290,13 @@
(*Used to make induction rules;
ind_alist = [(rec_tm1,pred1),...] associates predicates with rec ops
prem is a premise of an intr rule*)
- fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $
- (Const(@{const_name mem},_)$t$X), iprems) =
+ fun add_induct_prem ind_alist (prem as Const (@{const_name Trueprop}, _) $
+ (Const (@{const_name mem}, _) $ t $ X), iprems) =
(case AList.lookup (op aconv) ind_alist X of
SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
| NONE => (*possibly membership in M(rec_tm), for M monotone*)
let fun mk_sb (rec_tm,pred) =
- (rec_tm, Ind_Syntax.Collect_const$rec_tm$pred)
+ (rec_tm, @{const Collect} $ rec_tm $ pred)
in subst_free (map mk_sb ind_alist) prem :: iprems end)
| add_induct_prem ind_alist (prem,iprems) = prem :: iprems;
@@ -319,7 +324,7 @@
val dummy = if !Ind_Syntax.trace then
(writeln "ind_prems = ";
- List.app (writeln o Sign.string_of_term thy1) ind_prems;
+ List.app (writeln o Syntax.string_of_term ctxt1) ind_prems;
writeln "raw_induct = "; print_thm raw_induct)
else ();
@@ -338,15 +343,15 @@
(FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
(fn prems => EVERY
[rewrite_goals_tac part_rec_defs,
- rtac (impI RS allI) 1,
+ rtac (@{thm impI} RS @{thm allI}) 1,
DETERM (etac raw_induct 1),
(*Push Part inside Collect*)
full_simp_tac (min_ss addsimps [@{thm Part_Collect}]) 1,
(*This CollectE and disjE separates out the introduction rules*)
- REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, disjE])),
+ REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, @{thm disjE}])),
(*Now break down the individual cases. No disjE here in case
some premise involves disjunction.*)
- REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, exE, conjE]
+ REPEAT (FIRSTGOAL (eresolve_tac [@{thm CollectE}, @{thm exE}, @{thm conjE}]
ORELSE' bound_hyp_subst_tac)),
ind_tac (rev (map (rewrite_rule part_rec_defs) prems)) (length prems)]);
@@ -377,7 +382,7 @@
val qconcl =
foldr FOLogic.mk_all
(FOLogic.imp $
- (Ind_Syntax.mem_const $ elem_tuple $ rec_tm)
+ (@{const mem} $ elem_tuple $ rec_tm)
$ (list_comb (pfree, elem_frees))) elem_frees
in (CP.ap_split elem_type FOLogic.oT pfree,
qconcl)
@@ -387,7 +392,7 @@
(*Used to form simultaneous induction lemma*)
fun mk_rec_imp (rec_tm,pred) =
- FOLogic.imp $ (Ind_Syntax.mem_const $ Bound 0 $ rec_tm) $
+ FOLogic.imp $ (@{const mem} $ Bound 0 $ rec_tm) $
(pred $ Bound 0);
(*To instantiate the main induction rule*)
@@ -403,15 +408,15 @@
val dummy = if !Ind_Syntax.trace then
(writeln ("induct_concl = " ^
- Sign.string_of_term thy1 induct_concl);
+ Syntax.string_of_term ctxt1 induct_concl);
writeln ("mutual_induct_concl = " ^
- Sign.string_of_term thy1 mutual_induct_concl))
+ Syntax.string_of_term ctxt1 mutual_induct_concl))
else ();
- val lemma_tac = FIRST' [eresolve_tac [asm_rl, conjE, @{thm PartE}, mp],
- resolve_tac [allI, impI, conjI, @{thm Part_eqI}],
- dresolve_tac [spec, mp, Pr.fsplitD]];
+ val lemma_tac = FIRST' [eresolve_tac [@{thm asm_rl}, @{thm conjE}, @{thm PartE}, @{thm mp}],
+ resolve_tac [@{thm allI}, @{thm impI}, @{thm conjI}, @{thm Part_eqI}],
+ dresolve_tac [@{thm spec}, @{thm mp}, Pr.fsplitD]];
val need_mutual = length rec_names > 1;
@@ -423,7 +428,7 @@
(fn _ => EVERY
[rewrite_goals_tac part_rec_defs,
REPEAT (rewrite_goals_tac [Pr.split_eq] THEN lemma_tac 1)]))
- else (writeln " [ No mutual induction rule needed ]"; TrueI);
+ else (writeln " [ No mutual induction rule needed ]"; @{thm TrueI});
val dummy = if !Ind_Syntax.trace then
(writeln "lemma = "; print_thm lemma)
@@ -495,9 +500,9 @@
cterm_of thy1 elem_tuple)]);
(*strip quantifier and the implication*)
- val induct0 = inst (quant_induct RS spec RSN (2,rev_mp));
+ val induct0 = inst (quant_induct RS spec RSN (2, @{thm rev_mp}));
- val Const ("Trueprop", _) $ (pred_var $ _) = concl_of induct0
+ val Const (@{const_name Trueprop}, _) $ (pred_var $ _) = concl_of induct0
val induct = CP.split_rule_var(pred_var, elem_type-->FOLogic.oT, induct0)
|> standard
--- a/src/ZF/ind_syntax.ML Sat Mar 01 14:10:14 2008 +0100
+++ b/src/ZF/ind_syntax.ML Sat Mar 01 14:10:15 2008 +0100
@@ -6,16 +6,13 @@
Abstract Syntax functions for Inductive Definitions.
*)
-(*The structure protects these items from redeclaration (somewhat!). The
- datatype definitions in theory files refer to these items by name!
-*)
structure Ind_Syntax =
struct
(*Print tracing messages during processing of "inductive" theory sections*)
val trace = ref false;
-fun traceIt msg thy t =
+fun traceIt msg thy t =
if !trace then (tracing (msg ^ Sign.string_of_term thy t); t)
else t;
@@ -24,45 +21,36 @@
val iT = Type("i",[]);
-val mem_const = @{term mem};
-
(*Creates All(%v.v:A --> P(v)) rather than Ball(A,P) *)
-fun mk_all_imp (A,P) =
- FOLogic.all_const iT $
- Abs("v", iT, FOLogic.imp $ (mem_const $ Bound 0 $ A) $
+fun mk_all_imp (A,P) =
+ FOLogic.all_const iT $
+ Abs("v", iT, FOLogic.imp $ (@{const mem} $ Bound 0 $ A) $
Term.betapply(P, Bound 0));
-val Part_const = Const("Part", [iT,iT-->iT]--->iT);
-
-val apply_const = @{term apply};
-
-val Vrecursor_const = Const("Univ.Vrecursor", [[iT,iT]--->iT, iT]--->iT);
-
-val Collect_const = Const("Collect", [iT, iT-->FOLogic.oT] ---> iT);
-fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t);
+fun mk_Collect (a, D, t) = @{const Collect} $ D $ absfree (a, iT, t);
(*simple error-checking in the premises of an inductive definition*)
-fun chk_prem rec_hd (Const("op &",_) $ _ $ _) =
+fun chk_prem rec_hd (Const (@{const_name "op &"}, _) $ _ $ _) =
error"Premises may not be conjuctive"
- | chk_prem rec_hd (Const(@{const_name mem},_) $ t $ X) =
+ | chk_prem rec_hd (Const (@{const_name mem}, _) $ t $ X) =
(Logic.occs(rec_hd,t) andalso error "Recursion term on left of member symbol"; ())
- | chk_prem rec_hd t =
+ | chk_prem rec_hd t =
(Logic.occs(rec_hd,t) andalso error "Recursion term in side formula"; ());
(*Return the conclusion of a rule, of the form t:X*)
-fun rule_concl rl =
- let val Const("Trueprop",_) $ (Const(@{const_name mem},_) $ t $ X) =
+fun rule_concl rl =
+ let val Const (@{const_name Trueprop}, _) $ (Const (@{const_name mem}, _) $ t $ X) =
Logic.strip_imp_concl rl
in (t,X) end;
(*As above, but return error message if bad*)
fun rule_concl_msg sign rl = rule_concl rl
- handle Bind => error ("Ill-formed conclusion of introduction rule: " ^
+ handle Bind => error ("Ill-formed conclusion of introduction rule: " ^
Sign.string_of_term sign rl);
(*For deriving cases rules. CollectD2 discards the domain, which is redundant;
read_instantiate replaces a propositional variable by a formula variable*)
-val equals_CollectD =
+val equals_CollectD =
read_instantiate [("W","?Q")]
(make_elim (@{thm equalityD1} RS @{thm subsetD} RS @{thm CollectD2}));
@@ -71,10 +59,10 @@
(*Constructor name, type, mixfix info;
internal name from mixfix, datatype sets, full premises*)
-type constructor_spec =
- ((string * typ * mixfix) * string * term list * term list);
+type constructor_spec =
+ (string * typ * mixfix) * string * term list * term list;
-fun dest_mem (Const(@{const_name mem},_) $ x $ A) = (x,A)
+fun dest_mem (Const (@{const_name mem}, _) $ x $ A) = (x, A)
| dest_mem _ = error "Constructor specifications must have the form x:A";
(*read a constructor specification*)
@@ -82,7 +70,7 @@
let val prems = map (Sign.simple_read_term sign FOLogic.oT) sprems
val args = map (#1 o dest_mem) prems
val T = (map (#2 o dest_Free) args) ---> iT
- handle TERM _ => error
+ handle TERM _ => error
"Bad variable in constructor specification"
val name = Syntax.const_name id syn (*handle infix constructors*)
in ((id,T,syn), name, args, prems) end;
@@ -96,75 +84,40 @@
Logic.list_implies
(map FOLogic.mk_Trueprop prems,
FOLogic.mk_Trueprop
- (mem_const $ list_comb (Const (Sign.full_name sg name, T), args)
+ (@{const mem} $ list_comb (Const (Sign.full_name sg name, T), args)
$ rec_tm))
in map mk_intr constructs end;
fun mk_all_intr_tms sg arg = List.concat (ListPair.map (mk_intr_tms sg) arg);
-fun mk_Un (t1, t2) = Const(@{const_name Un}, [iT,iT]--->iT) $ t1 $ t2;
-
-val empty = Const("0", iT)
-and univ = Const("Univ.univ", iT-->iT)
-and quniv = Const("QUniv.quniv", iT-->iT);
+fun mk_Un (t1, t2) = @{const Un} $ t1 $ t2;
(*Make a datatype's domain: form the union of its set parameters*)
fun union_params (rec_tm, cs) =
let val (_,args) = strip_comb rec_tm
fun is_ind arg = (type_of arg = iT)
in case List.filter is_ind (args @ cs) of
- [] => empty
+ [] => @{const 0}
| u_args => BalancedTree.make mk_Un u_args
end;
-(*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_hds = map head_of rec_tms
- val dummy = assert_all is_Const rec_hds
- (fn t => "Datatype set not previously declared as constant: " ^
- Sign.string_of_term @{theory IFOL} t);
- val rec_names = (*nat doesn't have to be added*)
- @{const_name "nat"} :: map (#1 o dest_Const) rec_hds
- val u = if co then quniv else univ
- val cs = (fold o fold) (fn (_, _, _, prems) => prems |> (fold o fold_aterms)
- (fn t as Const (a, _) => if a mem_string rec_names then I else insert (op =) t
- | _ => I)) 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 (the_context ()) "a==b ==> a=c <-> c=b"
- (fn [def] => [(rewtac def), (rtac iffI 1), (REPEAT (etac sym 1))]);
-
-val def_trans = prove_goal (the_context ()) "[| f==g; g(a)=b |] ==> f(a)=b"
- (fn [rew,prem] => [ rewtac rew, rtac prem 1 ]);
-
-(*Delete needless equality assumptions*)
-val refl_thin = prove_goal (the_context ()) "!!P. [| a=a; P |] ==> P"
- (fn _ => [assume_tac 1]);
(*Includes rules for succ and Pair since they are common constructions*)
-val elim_rls = [asm_rl, FalseE, thm "succ_neq_0", sym RS thm "succ_neq_0",
- thm "Pair_neq_0", sym RS thm "Pair_neq_0", thm "Pair_inject",
- make_elim (thm "succ_inject"),
- refl_thin, conjE, exE, disjE];
+val elim_rls =
+ [@{thm asm_rl}, @{thm FalseE}, @{thm succ_neq_0}, @{thm sym} RS @{thm succ_neq_0},
+ @{thm Pair_neq_0}, @{thm sym} RS @{thm Pair_neq_0}, @{thm Pair_inject},
+ make_elim @{thm succ_inject}, @{thm refl_thin}, @{thm conjE}, @{thm exE}, @{thm disjE}];
(*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*)
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
| tryres (th, []) = raise THM("tryres", 0, [th]);
-fun gen_make_elim elim_rls rl =
+fun gen_make_elim elim_rls rl =
standard (tryres (rl, elim_rls @ [revcut_rl]));
(*Turns iff rules into safe elimination rules*)
-fun mk_free_SEs iffs = map (gen_make_elim [conjE,FalseE]) (iffs RL [iffD1]);
+fun mk_free_SEs iffs = map (gen_make_elim [@{thm conjE}, @{thm FalseE}]) (iffs RL [@{thm iffD1}]);
end;
-
-(*For convenient access by the user*)
-val trace_induct = Ind_Syntax.trace;