stripped legacy ML bindings
authorhaftmann
Wed Sep 23 12:03:47 2009 +0200 (2009-09-23)
changeset 326523175e23b79f3
parent 32647 e54f47f9e28b
child 32653 7feb35deb6f6
stripped legacy ML bindings
src/HOL/Inductive.thy
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Inductive.thy	Wed Sep 23 11:33:52 2009 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Wed Sep 23 12:03:47 2009 +0200
     1.3 @@ -267,26 +267,6 @@
     1.4    Ball_def Bex_def
     1.5    induct_rulify_fallback
     1.6  
     1.7 -ML {*
     1.8 -val def_lfp_unfold = @{thm def_lfp_unfold}
     1.9 -val def_gfp_unfold = @{thm def_gfp_unfold}
    1.10 -val def_lfp_induct = @{thm def_lfp_induct}
    1.11 -val def_coinduct = @{thm def_coinduct}
    1.12 -val inf_bool_eq = @{thm inf_bool_eq} RS @{thm eq_reflection}
    1.13 -val inf_fun_eq = @{thm inf_fun_eq} RS @{thm eq_reflection}
    1.14 -val sup_bool_eq = @{thm sup_bool_eq} RS @{thm eq_reflection}
    1.15 -val sup_fun_eq = @{thm sup_fun_eq} RS @{thm eq_reflection}
    1.16 -val le_boolI = @{thm le_boolI}
    1.17 -val le_boolI' = @{thm le_boolI'}
    1.18 -val le_funI = @{thm le_funI}
    1.19 -val le_boolE = @{thm le_boolE}
    1.20 -val le_funE = @{thm le_funE}
    1.21 -val le_boolD = @{thm le_boolD}
    1.22 -val le_funD = @{thm le_funD}
    1.23 -val le_bool_def = @{thm le_bool_def} RS @{thm eq_reflection}
    1.24 -val le_fun_def = @{thm le_fun_def} RS @{thm eq_reflection}
    1.25 -*}
    1.26 -
    1.27  use "Tools/inductive.ML"
    1.28  setup Inductive.setup
    1.29  
     2.1 --- a/src/HOL/Tools/inductive.ML	Wed Sep 23 11:33:52 2009 +0200
     2.2 +++ b/src/HOL/Tools/inductive.ML	Wed Sep 23 12:03:47 2009 +0200
     2.3 @@ -103,7 +103,10 @@
     2.4        "(P & True) = P" "(True & P) = P"
     2.5      by (fact simp_thms)+};
     2.6  
     2.7 -val simp_thms'' = inf_fun_eq :: inf_bool_eq :: simp_thms';
     2.8 +val simp_thms'' = map mk_meta_eq [@{thm inf_fun_eq}, @{thm inf_bool_eq}] @ simp_thms';
     2.9 +
    2.10 +val simp_thms''' = map mk_meta_eq
    2.11 +  [@{thm le_fun_def}, @{thm le_bool_def}, @{thm sup_fun_eq}, @{thm sup_bool_eq}];
    2.12  
    2.13  
    2.14  (** context data **)
    2.15 @@ -171,15 +174,15 @@
    2.16        (case concl of
    2.17            (_ $ (_ $ (Const ("Not", _) $ _) $ _)) => []
    2.18          | _ => [thm' RS (thm' RS eq_to_mono2)]);
    2.19 -    fun dest_less_concl thm = dest_less_concl (thm RS le_funD)
    2.20 -      handle THM _ => thm RS le_boolD
    2.21 +    fun dest_less_concl thm = dest_less_concl (thm RS @{thm le_funD})
    2.22 +      handle THM _ => thm RS @{thm le_boolD}
    2.23    in
    2.24      case concl of
    2.25        Const ("==", _) $ _ $ _ => eq2mono (thm RS meta_eq_to_obj_eq)
    2.26      | _ $ (Const ("op =", _) $ _ $ _) => eq2mono thm
    2.27      | _ $ (Const (@{const_name HOL.less_eq}, _) $ _ $ _) =>
    2.28        [dest_less_concl (Seq.hd (REPEAT (FIRSTGOAL
    2.29 -         (resolve_tac [le_funI, le_boolI'])) thm))]
    2.30 +         (resolve_tac [@{thm le_funI}, @{thm le_boolI'}])) thm))]
    2.31      | _ => [thm]
    2.32    end handle THM _ =>
    2.33      error ("Bad monotonicity theorem:\n" ^ Display.string_of_thm_without_context thm);
    2.34 @@ -323,11 +326,11 @@
    2.35      (HOLogic.mk_Trueprop
    2.36        (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
    2.37      (fn _ => EVERY [rtac @{thm monoI} 1,
    2.38 -      REPEAT (resolve_tac [le_funI, le_boolI'] 1),
    2.39 +      REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
    2.40        REPEAT (FIRST
    2.41          [atac 1,
    2.42           resolve_tac (List.concat (map mk_mono monos) @ get_monos ctxt) 1,
    2.43 -         etac le_funE 1, dtac le_boolD 1])]));
    2.44 +         etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
    2.45  
    2.46  
    2.47  (* prove introduction rules *)
    2.48 @@ -338,7 +341,7 @@
    2.49  
    2.50      val unfold = funpow k (fn th => th RS fun_cong)
    2.51        (mono RS (fp_def RS
    2.52 -        (if coind then def_gfp_unfold else def_lfp_unfold)));
    2.53 +        (if coind then @{thm def_gfp_unfold} else @{thm def_lfp_unfold})));
    2.54  
    2.55      fun select_disj 1 1 = []
    2.56        | select_disj _ 1 = [rtac disjI1]
    2.57 @@ -553,13 +556,13 @@
    2.58      val ind_concl = HOLogic.mk_Trueprop
    2.59        (HOLogic.mk_binrel "HOL.ord_class.less_eq" (rec_const, ind_pred));
    2.60  
    2.61 -    val raw_fp_induct = (mono RS (fp_def RS def_lfp_induct));
    2.62 +    val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
    2.63  
    2.64      val induct = SkipProof.prove ctxt'' [] ind_prems ind_concl
    2.65        (fn {prems, ...} => EVERY
    2.66          [rewrite_goals_tac [inductive_conj_def],
    2.67           DETERM (rtac raw_fp_induct 1),
    2.68 -         REPEAT (resolve_tac [le_funI, le_boolI] 1),
    2.69 +         REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
    2.70           rewrite_goals_tac simp_thms'',
    2.71           (*This disjE separates out the introduction rules*)
    2.72           REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
    2.73 @@ -577,7 +580,7 @@
    2.74          [rewrite_goals_tac rec_preds_defs,
    2.75           REPEAT (EVERY
    2.76             [REPEAT (resolve_tac [conjI, impI] 1),
    2.77 -            REPEAT (eresolve_tac [le_funE, le_boolE] 1),
    2.78 +            REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
    2.79              atac 1,
    2.80              rewrite_goals_tac simp_thms',
    2.81              atac 1])])
    2.82 @@ -763,8 +766,8 @@
    2.83             (snd (Variable.add_fixes (map (fst o dest_Free) params) ctxt1)) ctxt1)
    2.84             (rotate_prems ~1 (ObjectLogic.rulify
    2.85               (fold_rule rec_preds_defs
    2.86 -               (rewrite_rule [le_fun_def, le_bool_def, sup_fun_eq, sup_bool_eq]
    2.87 -                (mono RS (fp_def RS def_coinduct))))))
    2.88 +               (rewrite_rule simp_thms'''
    2.89 +                (mono RS (fp_def RS @{thm def_coinduct}))))))
    2.90         else
    2.91           prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono fp_def
    2.92             rec_preds_defs ctxt1);