src/HOL/Tools/inductive.ML
changeset 45649 2d995773da1a
parent 45648 7654f750fb43
child 45651 172aa230ce69
     1.1 --- a/src/HOL/Tools/inductive.ML	Sun Nov 27 14:26:57 2011 +0100
     1.2 +++ b/src/HOL/Tools/inductive.ML	Sun Nov 27 14:40:08 2011 +0100
     1.3 @@ -99,16 +99,18 @@
     1.4  val inductive_rulify = @{thms induct_rulify};
     1.5  val inductive_rulify_fallback = @{thms induct_rulify_fallback};
     1.6  
     1.7 -val simp_thms' = map mk_meta_eq
     1.8 -  @{lemma "(~True) = False" "(~False) = True"
     1.9 -      "(True --> P) = P" "(False --> P) = True"
    1.10 -      "(P & True) = P" "(True & P) = P"
    1.11 -    by (fact simp_thms)+};
    1.12 +val simp_thms1 =
    1.13 +  map mk_meta_eq
    1.14 +    @{lemma "(~ True) = False" "(~ False) = True"
    1.15 +        "(True --> P) = P" "(False --> P) = True"
    1.16 +        "(P & True) = P" "(True & P) = P"
    1.17 +      by (fact simp_thms)+};
    1.18  
    1.19 -val simp_thms'' = map mk_meta_eq [@{thm inf_fun_def}, @{thm inf_bool_def}] @ simp_thms';
    1.20 +val simp_thms2 =
    1.21 +  map mk_meta_eq [@{thm inf_fun_def}, @{thm inf_bool_def}] @ simp_thms1;
    1.22  
    1.23 -val simp_thms''' = map mk_meta_eq
    1.24 -  [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_def}, @{thm sup_bool_def}];
    1.25 +val simp_thms3 =
    1.26 +  map mk_meta_eq [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_def}, @{thm sup_bool_def}];
    1.27  
    1.28  
    1.29  
    1.30 @@ -201,12 +203,14 @@
    1.31  (
    1.32    type T = thm Item_Net.T;
    1.33    val empty = Item_Net.init (op aconv o pairself Thm.prop_of)
    1.34 -    (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);
    1.35 +    (single o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of);  (* FIXME fragile wrt. morphisms *)
    1.36    val extend = I;
    1.37    val merge = Item_Net.merge;
    1.38  );
    1.39  
    1.40 -val add_equation = Thm.declaration_attribute (Equation_Data.map o Item_Net.update)
    1.41 +val add_equation = Thm.declaration_attribute (Equation_Data.map o Item_Net.update);
    1.42 +
    1.43 +val get_equations = Equation_Data.get o Context.Proof;
    1.44  
    1.45  
    1.46  
    1.47 @@ -579,7 +583,7 @@
    1.48      val ctxt' = Variable.auto_fixes prop ctxt;
    1.49      val lhs_of = fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of;
    1.50      val substs =
    1.51 -      Item_Net.retrieve (Equation_Data.get (Context.Proof ctxt)) (HOLogic.dest_Trueprop prop)
    1.52 +      Item_Net.retrieve (get_equations ctxt) (HOLogic.dest_Trueprop prop)
    1.53        |> map_filter
    1.54          (fn eq => SOME (Pattern.match thy (lhs_of eq, HOLogic.dest_Trueprop prop)
    1.55              (Vartab.empty, Vartab.empty), eq)
    1.56 @@ -696,7 +700,7 @@
    1.57          [rewrite_goals_tac [inductive_conj_def],
    1.58           DETERM (rtac raw_fp_induct 1),
    1.59           REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
    1.60 -         rewrite_goals_tac simp_thms'',
    1.61 +         rewrite_goals_tac simp_thms2,
    1.62           (*This disjE separates out the introduction rules*)
    1.63           REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
    1.64           (*Now break down the individual cases.  No disjE here in case
    1.65 @@ -705,7 +709,7 @@
    1.66           REPEAT (FIRSTGOAL
    1.67             (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
    1.68           EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule
    1.69 -             (inductive_conj_def :: rec_preds_defs @ simp_thms'') prem,
    1.70 +             (inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
    1.71             conjI, refl] 1)) prems)]);
    1.72  
    1.73      val lemma = Skip_Proof.prove ctxt'' [] []
    1.74 @@ -715,7 +719,7 @@
    1.75             [REPEAT (resolve_tac [conjI, impI] 1),
    1.76              REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
    1.77              atac 1,
    1.78 -            rewrite_goals_tac simp_thms',
    1.79 +            rewrite_goals_tac simp_thms1,
    1.80              atac 1])]);
    1.81  
    1.82    in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
    1.83 @@ -926,7 +930,7 @@
    1.84           singleton (Proof_Context.export lthy2 lthy1)
    1.85             (rotate_prems ~1 (Object_Logic.rulify
    1.86               (fold_rule rec_preds_defs
    1.87 -               (rewrite_rule simp_thms'''
    1.88 +               (rewrite_rule simp_thms3
    1.89                  (mono RS (fp_def RS @{thm def_coinduct}))))))
    1.90         else
    1.91           prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def