# HG changeset patch # User wenzelm # Date 1277374599 -7200 # Node ID a9e38cdbfe07391915727e98283503fce35fd12b # Parent 40c352510065b102295ab5ddf92f01ea03376d00 tuned auxiliary structures; diff -r 40c352510065 -r a9e38cdbfe07 src/Tools/induct.ML --- a/src/Tools/induct.ML Thu Jun 24 11:28:34 2010 +0200 +++ b/src/Tools/induct.ML Thu Jun 24 12:16:39 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,7 +82,7 @@ val setup: theory -> theory end; -functor Induct(Data: INDUCT_DATA): INDUCT = +functor Induct(Induct_Args: INDUCT_ARGS): INDUCT = struct (** variables -- ordered left-to-right, preferring right **) @@ -135,7 +135,7 @@ 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 @@ -168,13 +168,13 @@ (* 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; @@ -203,7 +203,7 @@ (* context data *) -structure InductData = Generic_Data +structure Data = Generic_Data ( type T = (rules * rules) * (rules * rules) * (rules * rules) * simpset; val empty = @@ -220,7 +220,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 @@ -276,9 +276,9 @@ 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 => +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); @@ -310,7 +310,7 @@ 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 => @@ -410,14 +410,14 @@ (* 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 *) @@ -425,7 +425,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; @@ -437,7 +437,7 @@ fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt); -val trivial_tac = Data.trivial_tac; +val trivial_tac = Induct_Args.trivial_tac; @@ -477,7 +477,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 @@ -507,12 +507,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; @@ -521,8 +521,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 @@ -532,8 +532,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);