# HG changeset patch # User blanchet # Date 1277395471 -7200 # Node ID 8db1e5d4b93f9564b0e0e6df3299835556a53e79 # Parent a76ace919f1cba65b053b5b1fd2a1a83fa577c07# Parent 8a9a34be09e0407e70a0512346e9f08920a25ff1 merge diff -r a76ace919f1c -r 8db1e5d4b93f Admin/CHECKLIST --- a/Admin/CHECKLIST Thu Jun 24 17:57:36 2010 +0200 +++ b/Admin/CHECKLIST Thu Jun 24 18:04:31 2010 +0200 @@ -29,3 +29,17 @@ build lib/html/library_index_content.template + +Packaging +========= + +- makedist -r DISTNAME + +- makebin (multiplatform); + +- makebin -l on fast machine; + +- makebundle (multiplatform); + +- hdiutil create -srcfolder DIR DMG (Mac OS); + diff -r a76ace919f1c -r 8db1e5d4b93f src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Jun 24 17:57:36 2010 +0200 +++ b/src/HOL/IsaMakefile Thu Jun 24 18:04:31 2010 +0200 @@ -1093,6 +1093,7 @@ $(OUT)/HOL-Multivariate_Analysis: $(OUT)/HOL \ Multivariate_Analysis/Brouwer_Fixpoint.thy \ + Multivariate_Analysis/Cartesian_Euclidean_Space.thy \ Multivariate_Analysis/Convex_Euclidean_Space.thy \ Multivariate_Analysis/Derivative.thy \ Multivariate_Analysis/Determinants.thy \ diff -r a76ace919f1c -r 8db1e5d4b93f src/HOL/Tools/Quotient/quotient_def.ML --- a/src/HOL/Tools/Quotient/quotient_def.ML Thu Jun 24 17:57:36 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_def.ML Thu Jun 24 18:04:31 2010 +0200 @@ -7,13 +7,13 @@ signature QUOTIENT_DEF = sig val quotient_def: (binding option * mixfix) * (Attrib.binding * (term * term)) -> - local_theory -> (term * thm) * local_theory + local_theory -> Quotient_Info.qconsts_info * local_theory val quotdef_cmd: (binding option * mixfix) * (Attrib.binding * (string * string)) -> - local_theory -> (term * thm) * local_theory + local_theory -> Quotient_Info.qconsts_info * local_theory - val quotient_lift_const: typ list -> string * term -> local_theory -> - (term * thm) * local_theory + val lift_raw_const: typ list -> string * term -> local_theory -> + Quotient_Info.qconsts_info * local_theory end; structure Quotient_Def: QUOTIENT_DEF = @@ -32,12 +32,10 @@ - the new constant as term - the rhs of the definition as term - It returns the defined constant and its definition - theorem; stores the data in the qconsts data slot. + It stores the qconst_info in the qconsts data slot. - Restriction: At the moment the right-hand side of the - definition must be a constant. Similarly the left-hand - side must be a constant. + Restriction: At the moment the left- and right-hand + side of the definition must be a constant. *) fun error_msg bind str = let @@ -45,7 +43,7 @@ val pos = Position.str_of (Binding.pos_of bind) in error ("Head of quotient_definition " ^ - (quote str) ^ " differs from declaration " ^ name ^ pos) + quote str ^ " differs from declaration " ^ name ^ pos) end fun quotient_def ((optbind, mx), (attr, (lhs, rhs))) lthy = @@ -69,12 +67,14 @@ val ((trm, (_ , thm)), lthy') = Local_Theory.define ((qconst_bname, mx), (attr, newrhs)) lthy (* data storage *) - fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm} + val qconst_data = {qconst = trm, rconst = rhs, def = thm} + + fun qcinfo phi = transform_qconsts phi qconst_data fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi) val lthy'' = Local_Theory.declaration true (fn phi => qconsts_update_gen (trans_name phi) (qcinfo phi)) lthy' in - ((trm, thm), lthy'') + (qconst_data, lthy'') end fun quotdef_cmd (decl, (attr, (lhs_str, rhs_str))) lthy = @@ -87,10 +87,17 @@ quotient_def (decl, (attr, (lhs, rhs))) lthy'' end -fun quotient_lift_const qtys (b, t) ctxt = +(* a wrapper for automatically lifting a raw constant *) +fun lift_raw_const qtys (qconst_name, rconst) ctxt = +let + val rty = fastype_of rconst + val qty = derive_qtyp qtys rty ctxt +in quotient_def ((NONE, NoSyn), (Attrib.empty_binding, - (Quotient_Term.quotient_lift_const qtys (b, t) ctxt, t))) ctxt + (Free (qconst_name, qty), rconst))) ctxt +end +(* parser and command *) val quotdef_decl = (Parse.binding >> SOME) -- Parse.opt_mixfix' --| Parse.$$$ "where" val quotdef_parser = diff -r a76ace919f1c -r 8db1e5d4b93f src/HOL/Tools/Quotient/quotient_term.ML --- a/src/HOL/Tools/Quotient/quotient_term.ML Thu Jun 24 17:57:36 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_term.ML Thu Jun 24 18:04:31 2010 +0200 @@ -26,7 +26,7 @@ val inj_repabs_trm: Proof.context -> term * term -> term val inj_repabs_trm_chk: Proof.context -> term * term -> term - val quotient_lift_const: typ list -> string * term -> local_theory -> term + val derive_qtyp: typ list -> typ -> Proof.context -> typ val quotient_lift_all: typ list -> Proof.context -> term -> term end; @@ -84,7 +84,7 @@ *) fun mk_mapfun ctxt vs rty = let - val vs' = map (mk_Free) vs + val vs' = map mk_Free vs fun mk_mapfun_aux rty = case rty of @@ -103,7 +103,7 @@ let val thy = ProofContext.theory_of ctxt val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.") - val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn + val qdata = quotdata_lookup thy s handle Quotient_Info.NotFound => raise exn in (#rtyp qdata, #qtyp qdata) end @@ -738,14 +738,12 @@ (ty_substs, filter valid_trm_subst all_trm_substs) end -fun quotient_lift_const qtys (b, t) ctxt = +fun derive_qtyp qtys rty ctxt = let val thy = ProofContext.theory_of ctxt - val (ty_substs, _) = get_ty_trm_substs qtys ctxt; - val (_, ty) = dest_Const t; - val nty = subst_tys thy ty_substs ty; + val (ty_substs, _) = get_ty_trm_substs qtys ctxt in - Free(b, nty) + subst_tys thy ty_substs rty end (* diff -r a76ace919f1c -r 8db1e5d4b93f src/HOL/Tools/Quotient/quotient_typ.ML --- a/src/HOL/Tools/Quotient/quotient_typ.ML Thu Jun 24 17:57:36 2010 +0200 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML Thu Jun 24 18:04:31 2010 +0200 @@ -8,7 +8,7 @@ signature QUOTIENT_TYPE = sig val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm - -> Proof.context -> (thm * thm) * local_theory + -> Proof.context -> Quotient_Info.quotdata_info * local_theory val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list -> Proof.context -> Proof.state @@ -32,11 +32,8 @@ end fun note (name, thm, attrs) lthy = -let - val ((_,[thm']), lthy') = Local_Theory.note ((name, attrs), [thm]) lthy -in - (thm', lthy') -end + Local_Theory.note ((name, attrs), [thm]) lthy |> snd + fun intern_attr at = Attrib.internal (K at) @@ -64,7 +61,7 @@ |> map Free in lambda c (HOLogic.exists_const rty $ - lambda x (HOLogic.mk_conj ((rel $ x $ x), (HOLogic.mk_eq (c, (rel $ x)))))) + lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x)))) end @@ -139,7 +136,10 @@ (* main function for constructing a quotient type *) fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy = let - val part_equiv = if partial then equiv_thm else equiv_thm RS @{thm equivp_implies_part_equivp} + val part_equiv = + if partial + then equiv_thm + else equiv_thm RS @{thm equivp_implies_part_equivp} (* generates the typedef *) val ((qty_full_name, typedef_info), lthy1) = typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy @@ -173,15 +173,17 @@ (* name equivalence theorem *) val equiv_thm_name = Binding.suffix_name "_equivp" qty_name - (* storing the quot-info *) - fun qinfo phi = transform_quotdata phi - {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm} - val lthy4 = Local_Theory.declaration true - (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) lthy3 + (* storing the quotdata *) + val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm} + + fun qinfo phi = transform_quotdata phi quotdata + + val lthy4 = lthy3 + |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi)) + |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add]) + |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) in - lthy4 - |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add]) - ||>> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add]) + (quotdata, lthy4) end @@ -253,6 +255,7 @@ - its free type variables (first argument) - its mixfix annotation - the type to be quotient + - the partial flag (a boolean) - the relation according to which the type is quotient it opens a proof-state in which one has to show that the @@ -268,7 +271,8 @@ fun mk_goal (rty, rel, partial) = let val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool} - val const = if partial then @{const_name part_equivp} else @{const_name equivp} + val const = + if partial then @{const_name part_equivp} else @{const_name equivp} in HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel) end diff -r a76ace919f1c -r 8db1e5d4b93f src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Thu Jun 24 17:57:36 2010 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Thu Jun 24 18:04:31 2010 +0200 @@ -334,10 +334,10 @@ in Pretty.block ([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @ - (Pretty.block ((if eqs=[] then [] else str "if " :: + (Pretty.block ((if null eqs then [] else str "if " :: [Pretty.block eqs, Pretty.brk 1, str "then "]) @ (success_p :: - (if eqs=[] then [] else [Pretty.brk 1, str "else DSeq.empty"]))) :: + (if null eqs then [] else [Pretty.brk 1, str "else DSeq.empty"]))) :: (if can_fail then [Pretty.brk 1, str "| _ => DSeq.empty)"] else [str ")"]))) diff -r a76ace919f1c -r 8db1e5d4b93f src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Thu Jun 24 17:57:36 2010 +0200 +++ b/src/Pure/General/pretty.ML Thu Jun 24 18:04:31 2010 +0200 @@ -102,10 +102,11 @@ (** printing items: compound phrases, strings, and breaks **) -datatype T = +abstype T = Block of (output * output) * T list * int * int | (*markup output, body, indentation, length*) String of output * int | (*text, length*) - Break of bool * int; (*mandatory flag, width if not taken*) + Break of bool * int (*mandatory flag, width if not taken*) +with fun length (Block (_, _, _, len)) = len | length (String (_, len)) = len @@ -323,6 +324,8 @@ | from_ML (ML_Pretty.String s) = String s | from_ML (ML_Pretty.Break b) = Break b; +end; + (** abstract pretty printing context **) diff -r a76ace919f1c -r 8db1e5d4b93f src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Thu Jun 24 17:57:36 2010 +0200 +++ b/src/Pure/Isar/code.ML Thu Jun 24 18:04:31 2010 +0200 @@ -1132,7 +1132,7 @@ fun mk_prem z = Free (z, T_cong); fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts); val (prem, concl) = pairself Logic.mk_equals (pairself mk_prem (x, y), pairself mk_concl (x, y)); - fun tac { prems, ... } = Simplifier.rewrite_goals_tac prems + fun tac { context, prems } = Simplifier.rewrite_goals_tac prems THEN ALLGOALS (ProofContext.fact_tac [Drule.reflexive_thm]); in Skip_Proof.prove_global thy (x :: y :: zs) [prem] concl tac end; diff -r a76ace919f1c -r 8db1e5d4b93f src/Pure/net.ML --- a/src/Pure/net.ML Thu Jun 24 17:57:36 2010 +0200 +++ b/src/Pure/net.ML Thu Jun 24 18:04:31 2010 +0200 @@ -17,6 +17,7 @@ sig type key val key_of_term: term -> key list + val encode_type: typ -> term type 'a net val empty: 'a net exception INSERT @@ -62,6 +63,11 @@ (*convert a term to a list of keys*) fun key_of_term t = add_key_of_terms (t, []); +(*encode_type -- for indexing purposes*) +fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts) + | encode_type (TFree (a, _)) = Free (a, dummyT) + | encode_type (TVar (a, _)) = Var (a, dummyT); + (*Trees indexed by key lists: each arc is labelled by a key. Each node contains a list of items, and arcs to children. diff -r a76ace919f1c -r 8db1e5d4b93f src/Pure/pure_setup.ML --- a/src/Pure/pure_setup.ML Thu Jun 24 17:57:36 2010 +0200 +++ b/src/Pure/pure_setup.ML Thu Jun 24 18:04:31 2010 +0200 @@ -18,6 +18,7 @@ (* ML toplevel pretty printing *) +toplevel_pp ["Pretty", "T"] "(fn _: Pretty.T => Pretty.str \"\")"; toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task"; toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group"; toplevel_pp ["Position", "T"] "Pretty.position"; diff -r a76ace919f1c -r 8db1e5d4b93f src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Thu Jun 24 17:57:36 2010 +0200 +++ b/src/Tools/Code/code_target.ML Thu Jun 24 18:04:31 2010 +0200 @@ -142,9 +142,9 @@ name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) = if serial1 = serial2 orelse not strict then make_target ((serial1, serializer), - ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)), + ((merge (op =) (reserved1, reserved2), Symtab.merge (K true) (includes1, includes2)), (merge_name_syntax_table (name_syntax_table1, name_syntax_table2), - Symtab.join (K snd) (module_alias1, module_alias2)) + Symtab.join (K fst) (module_alias1, module_alias2)) )) else error ("Incompatible serializers: " ^ quote target); diff -r a76ace919f1c -r 8db1e5d4b93f src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Jun 24 17:57:36 2010 +0200 +++ b/src/Tools/induct.ML Thu Jun 24 18:04:31 2010 +0200 @@ -4,7 +4,7 @@ Proof by cases, induction, and coinduction. *) -signature INDUCT_DATA = +signature INDUCT_ARGS = sig val cases_default: thm val atomize: thm list @@ -82,27 +82,17 @@ val setup: theory -> theory end; -functor Induct(Data: INDUCT_DATA): INDUCT = +functor Induct(Induct_Args: INDUCT_ARGS): INDUCT = struct - -(** misc utils **) - -(* encode_type -- for indexing purposes *) - -fun encode_type (Type (c, Ts)) = Term.list_comb (Const (c, dummyT), map encode_type Ts) - | encode_type (TFree (a, _)) = Free (a, dummyT) - | encode_type (TVar (a, _)) = Var (a, dummyT); - - -(* variables -- ordered left-to-right, preferring right *) +(** variables -- ordered left-to-right, preferring right **) fun vars_of tm = rev (distinct (op =) (Term.fold_aterms (fn (t as Var _) => cons t | _ => I) tm [])); local -val mk_var = encode_type o #2 o Term.dest_Var; +val mk_var = Net.encode_type o #2 o Term.dest_Var; fun concl_var which thm = mk_var (which (vars_of (Thm.concl_of thm))) handle Empty => raise THM ("No variables in conclusion of rule", 0, [thm]); @@ -128,14 +118,14 @@ fun conv1 0 ctxt = Conv.forall_conv (cv o snd) ctxt | conv1 k ctxt = Conv.rewr_conv @{thm swap_params} then_conv - Conv.forall_conv (conv1 (k-1) o snd) ctxt + Conv.forall_conv (conv1 (k - 1) o snd) ctxt fun conv2 0 ctxt = conv1 j ctxt - | conv2 k ctxt = Conv.forall_conv (conv2 (k-1) o snd) ctxt + | conv2 k ctxt = Conv.forall_conv (conv2 (k - 1) o snd) ctxt in conv2 i ctxt end; fun swap_prems_conv 0 = Conv.all_conv | swap_prems_conv i = - Conv.implies_concl_conv (swap_prems_conv (i-1)) then_conv + Conv.implies_concl_conv (swap_prems_conv (i - 1)) then_conv Conv.rewr_conv Drule.swap_prems_eq fun drop_judgment ctxt = Object_Logic.drop_judgment (ProofContext.theory_of ctxt); @@ -145,46 +135,51 @@ val l = length (Logic.strip_params t); val Hs = Logic.strip_assums_hyp t; fun find (i, t) = - case Data.dest_def (drop_judgment ctxt t) of + (case Induct_Args.dest_def (drop_judgment ctxt t) of SOME (Bound j, _) => SOME (i, j) | SOME (_, Bound j) => SOME (i, j) - | _ => NONE + | _ => NONE); in - case get_first find (map_index I Hs) of + (case get_first find (map_index I Hs) of NONE => NONE | SOME (0, 0) => NONE - | SOME (i, j) => SOME (i, l-j-1, j) + | SOME (i, j) => SOME (i, l - j - 1, j)) end; -fun mk_swap_rrule ctxt ct = case find_eq ctxt (term_of ct) of +fun mk_swap_rrule ctxt ct = + (case find_eq ctxt (term_of ct) of NONE => NONE - | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct); + | SOME (i, k, j) => SOME (swap_params_conv ctxt k j (K (swap_prems_conv i)) ct)); -val rearrange_eqs_simproc = Simplifier.simproc - (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"] - (fn thy => fn ss => fn t => - mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t)) +val rearrange_eqs_simproc = + Simplifier.simproc + (Thm.theory_of_thm Drule.swap_prems_eq) "rearrange_eqs" ["all t"] + (fn thy => fn ss => fn t => + mk_swap_rrule (Simplifier.the_context ss) (cterm_of thy t)); + (* rotate k premises to the left by j, skipping over first j premises *) fun rotate_conv 0 j 0 = Conv.all_conv - | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k-1) - | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i-1) j k); + | rotate_conv 0 j k = swap_prems_conv j then_conv rotate_conv 1 j (k - 1) + | rotate_conv i j k = Conv.implies_concl_conv (rotate_conv (i - 1) j k); fun rotate_tac j 0 = K all_tac - | rotate_tac j k = SUBGOAL (fn (goal, i) => CONVERSION (rotate_conv - j (length (Logic.strip_assums_hyp goal) - j - k) k) i); + | rotate_tac j k = SUBGOAL (fn (goal, i) => + CONVERSION (rotate_conv + j (length (Logic.strip_assums_hyp goal) - j - k) k) i); + (* rulify operators around definition *) fun rulify_defs_conv ctxt ct = - if exists_subterm (is_some o Data.dest_def) (term_of ct) andalso - not (is_some (Data.dest_def (drop_judgment ctxt (term_of ct)))) + if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) andalso + not (is_some (Induct_Args.dest_def (drop_judgment ctxt (term_of ct)))) then (Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt)) (Conv.try_conv (rulify_defs_conv ctxt)) else_conv - Conv.first_conv (map Conv.rewr_conv Data.rulify) then_conv + Conv.first_conv (map Conv.rewr_conv Induct_Args.rulify) then_conv Conv.try_conv (rulify_defs_conv ctxt)) ct else Conv.no_conv ct; @@ -213,7 +208,7 @@ (* context data *) -structure InductData = Generic_Data +structure Data = Generic_Data ( type T = (rules * rules) * (rules * rules) * (rules * rules) * simpset; val empty = @@ -230,7 +225,7 @@ merge_ss (simpset1, simpset2)); ); -val get_local = InductData.get o Context.Proof; +val get_local = Data.get o Context.Proof; fun dest_rules ctxt = let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in @@ -272,11 +267,11 @@ fun find_rules which how ctxt x = map snd (Item_Net.retrieve (which (get_local ctxt)) (how x)); -val find_casesT = find_rules (#1 o #1) encode_type; +val find_casesT = find_rules (#1 o #1) Net.encode_type; val find_casesP = find_rules (#2 o #1) I; -val find_inductT = find_rules (#1 o #2) encode_type; +val find_inductT = find_rules (#1 o #2) Net.encode_type; val find_inductP = find_rules (#2 o #2) I; -val find_coinductT = find_rules (#1 o #3) encode_type; +val find_coinductT = find_rules (#1 o #3) Net.encode_type; val find_coinductP = find_rules (#2 o #3) I; @@ -286,10 +281,11 @@ local fun mk_att f g name arg = - let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end; + let val (x, thm) = g arg in (Data.map (f (name, thm)) x, thm) end; -fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs => - fold Item_Net.remove (filter_rules rs th) rs)))); +fun del_att which = + Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs => + fold Item_Net.remove (filter_rules rs th) rs)))); fun map1 f (x, y, z, s) = (f x, y, z, s); fun map2 f (x, y, z, s) = (x, f y, z, s); @@ -320,12 +316,12 @@ val coinduct_pred = mk_att add_coinductP consumes1; val coinduct_del = del_att map3; -fun map_simpset f = InductData.map (map4 f); +fun map_simpset f = Data.map (map4 f); fun induct_simp f = Thm.declaration_attribute (fn thm => fn context => - (map_simpset - (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context)); + map_simpset + (Simplifier.with_context (Context.proof_of context) (fn ss => f (ss, [thm]))) context); val induct_simp_add = induct_simp (op addsimps); val induct_simp_del = induct_simp (op delsimps); @@ -420,14 +416,15 @@ (* mark equality constraints in cases rule *) -val equal_def' = Thm.symmetric Data.equal_def; +val equal_def' = Thm.symmetric Induct_Args.equal_def; fun mark_constraints n ctxt = Conv.fconv_rule (Conv.prems_conv (~1) (Conv.params_conv ~1 (K (Conv.prems_conv n (MetaSimplifier.rewrite false [equal_def']))) ctxt)); val unmark_constraints = Conv.fconv_rule - (MetaSimplifier.rewrite true [Data.equal_def]); + (MetaSimplifier.rewrite true [Induct_Args.equal_def]); + (* simplify *) @@ -435,7 +432,7 @@ Simplifier.full_rewrite (Simplifier.context ctxt (#4 (get_local ctxt))); fun simplify_conv ctxt ct = - if exists_subterm (is_some o Data.dest_def) (term_of ct) then + if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) then (Conv.try_conv (rulify_defs_conv ctxt) then_conv simplify_conv' ctxt) ct else Conv.all_conv ct; @@ -447,7 +444,7 @@ fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt); -val trivial_tac = Data.trivial_tac; +val trivial_tac = Induct_Args.trivial_tac; @@ -487,7 +484,7 @@ (case opt_rule of SOME r => Seq.single (inst_rule r) | NONE => - (get_casesP ctxt facts @ get_casesT ctxt insts @ [Data.cases_default]) + (get_casesP ctxt facts @ get_casesT ctxt insts @ [Induct_Args.cases_default]) |> tap (trace_rules ctxt casesN) |> Seq.of_list |> Seq.maps (Seq.try inst_rule)); in @@ -517,12 +514,12 @@ (* atomize *) fun atomize_term thy = - MetaSimplifier.rewrite_term thy Data.atomize [] + MetaSimplifier.rewrite_term thy Induct_Args.atomize [] #> Object_Logic.drop_judgment thy; -val atomize_cterm = MetaSimplifier.rewrite true Data.atomize; +val atomize_cterm = MetaSimplifier.rewrite true Induct_Args.atomize; -val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize; +val atomize_tac = Simplifier.rewrite_goal_tac Induct_Args.atomize; val inner_atomize_tac = Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac; @@ -531,8 +528,8 @@ (* rulify *) fun rulify_term thy = - MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #> - MetaSimplifier.rewrite_term thy Data.rulify_fallback []; + MetaSimplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #> + MetaSimplifier.rewrite_term thy Induct_Args.rulify_fallback []; fun rulified_term thm = let @@ -542,8 +539,8 @@ in (thy, Logic.list_implies (map rulify As, rulify B)) end; val rulify_tac = - Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN' - Simplifier.rewrite_goal_tac Data.rulify_fallback THEN' + Simplifier.rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN' + Simplifier.rewrite_goal_tac Induct_Args.rulify_fallback THEN' Goal.conjunction_tac THEN_ALL_NEW (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);