src/Tools/induct.ML
changeset 37524 a9e38cdbfe07
parent 37523 40c352510065
child 37525 a5ac274798fc
     1.1 --- a/src/Tools/induct.ML	Thu Jun 24 11:28:34 2010 +0200
     1.2 +++ b/src/Tools/induct.ML	Thu Jun 24 12:16:39 2010 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  Proof by cases, induction, and coinduction.
     1.5  *)
     1.6  
     1.7 -signature INDUCT_DATA =
     1.8 +signature INDUCT_ARGS =
     1.9  sig
    1.10    val cases_default: thm
    1.11    val atomize: thm list
    1.12 @@ -82,7 +82,7 @@
    1.13    val setup: theory -> theory
    1.14  end;
    1.15  
    1.16 -functor Induct(Data: INDUCT_DATA): INDUCT =
    1.17 +functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
    1.18  struct
    1.19  
    1.20  (** variables -- ordered left-to-right, preferring right **)
    1.21 @@ -135,7 +135,7 @@
    1.22      val l = length (Logic.strip_params t);
    1.23      val Hs = Logic.strip_assums_hyp t;
    1.24      fun find (i, t) =
    1.25 -      case Data.dest_def (drop_judgment ctxt t) of
    1.26 +      case Induct_Args.dest_def (drop_judgment ctxt t) of
    1.27          SOME (Bound j, _) => SOME (i, j)
    1.28        | SOME (_, Bound j) => SOME (i, j)
    1.29        | _ => NONE
    1.30 @@ -168,13 +168,13 @@
    1.31  (* rulify operators around definition *)
    1.32  
    1.33  fun rulify_defs_conv ctxt ct =
    1.34 -  if exists_subterm (is_some o Data.dest_def) (term_of ct) andalso
    1.35 -    not (is_some (Data.dest_def (drop_judgment ctxt (term_of ct))))
    1.36 +  if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) andalso
    1.37 +    not (is_some (Induct_Args.dest_def (drop_judgment ctxt (term_of ct))))
    1.38    then
    1.39      (Conv.forall_conv (rulify_defs_conv o snd) ctxt else_conv
    1.40       Conv.implies_conv (Conv.try_conv (rulify_defs_conv ctxt))
    1.41         (Conv.try_conv (rulify_defs_conv ctxt)) else_conv
    1.42 -     Conv.first_conv (map Conv.rewr_conv Data.rulify) then_conv
    1.43 +     Conv.first_conv (map Conv.rewr_conv Induct_Args.rulify) then_conv
    1.44         Conv.try_conv (rulify_defs_conv ctxt)) ct
    1.45    else Conv.no_conv ct;
    1.46  
    1.47 @@ -203,7 +203,7 @@
    1.48  
    1.49  (* context data *)
    1.50  
    1.51 -structure InductData = Generic_Data
    1.52 +structure Data = Generic_Data
    1.53  (
    1.54    type T = (rules * rules) * (rules * rules) * (rules * rules) * simpset;
    1.55    val empty =
    1.56 @@ -220,7 +220,7 @@
    1.57       merge_ss (simpset1, simpset2));
    1.58  );
    1.59  
    1.60 -val get_local = InductData.get o Context.Proof;
    1.61 +val get_local = Data.get o Context.Proof;
    1.62  
    1.63  fun dest_rules ctxt =
    1.64    let val ((casesT, casesP), (inductT, inductP), (coinductT, coinductP), _) = get_local ctxt in
    1.65 @@ -276,9 +276,9 @@
    1.66  local
    1.67  
    1.68  fun mk_att f g name arg =
    1.69 -  let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end;
    1.70 +  let val (x, thm) = g arg in (Data.map (f (name, thm)) x, thm) end;
    1.71  
    1.72 -fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs =>
    1.73 +fun del_att which = Thm.declaration_attribute (fn th => Data.map (which (pairself (fn rs =>
    1.74    fold Item_Net.remove (filter_rules rs th) rs))));
    1.75  
    1.76  fun map1 f (x, y, z, s) = (f x, y, z, s);
    1.77 @@ -310,7 +310,7 @@
    1.78  val coinduct_pred = mk_att add_coinductP consumes1;
    1.79  val coinduct_del = del_att map3;
    1.80  
    1.81 -fun map_simpset f = InductData.map (map4 f);
    1.82 +fun map_simpset f = Data.map (map4 f);
    1.83  
    1.84  fun induct_simp f =
    1.85    Thm.declaration_attribute (fn thm => fn context =>
    1.86 @@ -410,14 +410,14 @@
    1.87  
    1.88  (* mark equality constraints in cases rule *)
    1.89  
    1.90 -val equal_def' = Thm.symmetric Data.equal_def;
    1.91 +val equal_def' = Thm.symmetric Induct_Args.equal_def;
    1.92  
    1.93  fun mark_constraints n ctxt = Conv.fconv_rule
    1.94    (Conv.prems_conv (~1) (Conv.params_conv ~1 (K (Conv.prems_conv n
    1.95       (MetaSimplifier.rewrite false [equal_def']))) ctxt));
    1.96  
    1.97  val unmark_constraints = Conv.fconv_rule
    1.98 -  (MetaSimplifier.rewrite true [Data.equal_def]);
    1.99 +  (MetaSimplifier.rewrite true [Induct_Args.equal_def]);
   1.100  
   1.101  (* simplify *)
   1.102  
   1.103 @@ -425,7 +425,7 @@
   1.104    Simplifier.full_rewrite (Simplifier.context ctxt (#4 (get_local ctxt)));
   1.105  
   1.106  fun simplify_conv ctxt ct =
   1.107 -  if exists_subterm (is_some o Data.dest_def) (term_of ct) then
   1.108 +  if exists_subterm (is_some o Induct_Args.dest_def) (term_of ct) then
   1.109      (Conv.try_conv (rulify_defs_conv ctxt) then_conv simplify_conv' ctxt) ct
   1.110    else Conv.all_conv ct;
   1.111  
   1.112 @@ -437,7 +437,7 @@
   1.113  
   1.114  fun simplify_tac ctxt = CONVERSION (simplify_conv ctxt);
   1.115  
   1.116 -val trivial_tac = Data.trivial_tac;
   1.117 +val trivial_tac = Induct_Args.trivial_tac;
   1.118  
   1.119  
   1.120  
   1.121 @@ -477,7 +477,7 @@
   1.122        (case opt_rule of
   1.123          SOME r => Seq.single (inst_rule r)
   1.124        | NONE =>
   1.125 -          (get_casesP ctxt facts @ get_casesT ctxt insts @ [Data.cases_default])
   1.126 +          (get_casesP ctxt facts @ get_casesT ctxt insts @ [Induct_Args.cases_default])
   1.127            |> tap (trace_rules ctxt casesN)
   1.128            |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
   1.129    in
   1.130 @@ -507,12 +507,12 @@
   1.131  (* atomize *)
   1.132  
   1.133  fun atomize_term thy =
   1.134 -  MetaSimplifier.rewrite_term thy Data.atomize []
   1.135 +  MetaSimplifier.rewrite_term thy Induct_Args.atomize []
   1.136    #> Object_Logic.drop_judgment thy;
   1.137  
   1.138 -val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
   1.139 +val atomize_cterm = MetaSimplifier.rewrite true Induct_Args.atomize;
   1.140  
   1.141 -val atomize_tac = Simplifier.rewrite_goal_tac Data.atomize;
   1.142 +val atomize_tac = Simplifier.rewrite_goal_tac Induct_Args.atomize;
   1.143  
   1.144  val inner_atomize_tac =
   1.145    Simplifier.rewrite_goal_tac (map Thm.symmetric conjunction_congs) THEN' atomize_tac;
   1.146 @@ -521,8 +521,8 @@
   1.147  (* rulify *)
   1.148  
   1.149  fun rulify_term thy =
   1.150 -  MetaSimplifier.rewrite_term thy (Data.rulify @ conjunction_congs) [] #>
   1.151 -  MetaSimplifier.rewrite_term thy Data.rulify_fallback [];
   1.152 +  MetaSimplifier.rewrite_term thy (Induct_Args.rulify @ conjunction_congs) [] #>
   1.153 +  MetaSimplifier.rewrite_term thy Induct_Args.rulify_fallback [];
   1.154  
   1.155  fun rulified_term thm =
   1.156    let
   1.157 @@ -532,8 +532,8 @@
   1.158    in (thy, Logic.list_implies (map rulify As, rulify B)) end;
   1.159  
   1.160  val rulify_tac =
   1.161 -  Simplifier.rewrite_goal_tac (Data.rulify @ conjunction_congs) THEN'
   1.162 -  Simplifier.rewrite_goal_tac Data.rulify_fallback THEN'
   1.163 +  Simplifier.rewrite_goal_tac (Induct_Args.rulify @ conjunction_congs) THEN'
   1.164 +  Simplifier.rewrite_goal_tac Induct_Args.rulify_fallback THEN'
   1.165    Goal.conjunction_tac THEN_ALL_NEW
   1.166    (Simplifier.rewrite_goal_tac [@{thm Pure.conjunction_imp}] THEN' Goal.norm_hhf_tac);
   1.167