# HG changeset patch
# User haftmann
# Date 1253706173 -7200
# Node ID 7feb35deb6f647013174809d70f61bde741d8d70
# Parent  3175e23b79f3b5ce41c9d004e11c4277f1e496c6# Parent  af55ccf865a49f059f4709840bbf823f6cc43af7
merged

diff -r af55ccf865a4 -r 7feb35deb6f6 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Wed Sep 23 13:31:38 2009 +0200
+++ b/src/HOL/Inductive.thy	Wed Sep 23 13:42:53 2009 +0200
@@ -267,26 +267,6 @@
   Ball_def Bex_def
   induct_rulify_fallback
 
-ML {*
-val def_lfp_unfold = @{thm def_lfp_unfold}
-val def_gfp_unfold = @{thm def_gfp_unfold}
-val def_lfp_induct = @{thm def_lfp_induct}
-val def_coinduct = @{thm def_coinduct}
-val inf_bool_eq = @{thm inf_bool_eq} RS @{thm eq_reflection}
-val inf_fun_eq = @{thm inf_fun_eq} RS @{thm eq_reflection}
-val sup_bool_eq = @{thm sup_bool_eq} RS @{thm eq_reflection}
-val sup_fun_eq = @{thm sup_fun_eq} RS @{thm eq_reflection}
-val le_boolI = @{thm le_boolI}
-val le_boolI' = @{thm le_boolI'}
-val le_funI = @{thm le_funI}
-val le_boolE = @{thm le_boolE}
-val le_funE = @{thm le_funE}
-val le_boolD = @{thm le_boolD}
-val le_funD = @{thm le_funD}
-val le_bool_def = @{thm le_bool_def} RS @{thm eq_reflection}
-val le_fun_def = @{thm le_fun_def} RS @{thm eq_reflection}
-*}
-
 use "Tools/inductive.ML"
 setup Inductive.setup
 
diff -r af55ccf865a4 -r 7feb35deb6f6 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Wed Sep 23 13:31:38 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Wed Sep 23 13:42:53 2009 +0200
@@ -103,7 +103,10 @@
       "(P & True) = P" "(True & P) = P"
     by (fact simp_thms)+};
 
-val simp_thms'' = inf_fun_eq :: inf_bool_eq :: simp_thms';
+val simp_thms'' = map mk_meta_eq [@{thm inf_fun_eq}, @{thm inf_bool_eq}] @ simp_thms';
+
+val simp_thms''' = map mk_meta_eq
+  [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_eq}, @{thm sup_bool_eq}];
 
 
 (** context data **)
@@ -171,15 +174,15 @@
       (case concl of
           (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
         | _ => [thm' RS (thm' RS eq_to_mono2)]);
-    fun dest_less_concl thm = dest_less_concl (thm RS le_funD)
-      handle THM _ => thm RS le_boolD
+    fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
+      handle THM _ => thm RS @{thm le_boolD}
   in
     case concl of
       Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
     | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
     | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) =>
       [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
-         (resolve_tac [le_funI, le_boolI'])) thm))]
+         (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))]
     | _ => [thm]
   end handle THM _ =>
     error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
@@ -323,11 +326,11 @@
     (HOLogic.mk_Trueprop
       (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
     (fn _ => EVERY [rtac @{thm monoI} 1,
-      REPEAT (resolve_tac [le_funI, le_boolI'] 1),
+      REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
       REPEAT (FIRST
         [atac 1,
          resolve_tac (List.concat (map mk_mono monos) @ get_monos ctxt) 1,
-         etac le_funE 1, dtac le_boolD 1])]));
+         etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
 
 
 (* prove introduction rules *)
@@ -338,7 +341,7 @@
 
     val unfold = funpow k (fn th => th RS fun_cong)
       (mono RS (fp_def RS
-        (if coind then def_gfp_unfold else def_lfp_unfold)));
+        (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold})));
 
     fun select_disj 1 1 = []
       | select_disj _ 1 = [rtac disjI1]
@@ -553,13 +556,13 @@
     val ind_concl = HOLogic.mk_Trueprop
       (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
 
-    val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
+    val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
 
     val induct = SkipProof.prove ctxt'' [] ind_prems ind_concl
       (fn {prems, ...} => EVERY
         [rewrite_goals_tac [inductive_conj_def],
          DETERM (rtac raw_fp_induct 1),
-         REPEAT (resolve_tac [le_funI, le_boolI] 1),
+         REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
          rewrite_goals_tac simp_thms'',
          (*This disjE separates out the introduction rules*)
          REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
@@ -577,7 +580,7 @@
         [rewrite_goals_tac rec_preds_defs,
          REPEAT (EVERY
            [REPEAT (resolve_tac [conjI, impI] 1),
-            REPEAT (eresolve_tac [le_funE, le_boolE] 1),
+            REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
             atac 1,
             rewrite_goals_tac simp_thms',
             atac 1])])
@@ -763,8 +766,8 @@
            (snd (Variable.add_fixes (map (fst o dest_Free) params) ctxt1)) ctxt1)
            (rotate_prems ~1 (ObjectLogic.rulify
              (fold_rule rec_preds_defs
-               (rewrite_rule [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq]
-                (mono RS (fp_def RS def_coinduct))))))
+               (rewrite_rule simp_thms'''
+                (mono RS (fp_def RS @{thm def_coinduct}))))))
        else
          prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
            rec_preds_defs ctxt1);