# HG changeset patch # User wenzelm # Date 1204377015 -3600 # Node ID 9808cca5c54dbe3dd72b793d7a0f3290463e65d4 # Parent 9cb1b484fe9639c62b1cb6229574620cc52923b3 misc cleanup of embedded ML code; use more antiquotations; tuned; diff -r 9cb1b484fe96 -r 9808cca5c54d src/ZF/Inductive_ZF.thy --- 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} diff -r 9cb1b484fe96 -r 9808cca5c54d src/ZF/Tools/cartprod.ML --- 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, diff -r 9cb1b484fe96 -r 9808cca5c54d src/ZF/Tools/datatype_package.ML --- 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; diff -r 9cb1b484fe96 -r 9808cca5c54d src/ZF/Tools/inductive_package.ML --- 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 diff -r 9cb1b484fe96 -r 9808cca5c54d src/ZF/ind_syntax.ML --- 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;