--- a/src/HOL/Tools/record.ML Fri Dec 30 12:12:16 2011 +0100
+++ b/src/HOL/Tools/record.ML Fri Dec 30 12:54:55 2011 +0100
@@ -1477,8 +1477,7 @@
val params = Logic.strip_params g;
val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl g);
val rule' = Thm.lift_rule cgoal rule;
- val (P, ys) = strip_comb (HOLogic.dest_Trueprop
- (Logic.strip_assums_concl (prop_of rule')));
+ val (P, ys) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_assums_concl (prop_of rule')));
(*ca indicates if rule is a case analysis or induction rule*)
val (x, ca) =
(case rev (drop (length params) ys) of
@@ -1688,27 +1687,6 @@
fold_rev (fn (parent, Ts) => fn T => Type (parent, subst_last T Ts)) extT;
-fun obj_to_meta_all thm =
- let
- fun E thm = (* FIXME proper name *)
- (case SOME (spec OF [thm]) handle THM _ => NONE of
- SOME thm' => E thm'
- | NONE => thm);
- val th1 = E thm;
- val th2 = Drule.forall_intr_vars th1;
- in th2 end;
-
-fun meta_to_obj_all thm =
- let
- val thy = Thm.theory_of_thm thm;
- val prop = Thm.prop_of thm;
- val params = Logic.strip_params prop;
- val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl prop);
- val ct = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.list_all (params, concl)));
- val thm' = Seq.hd (REPEAT (rtac allI 1) (Thm.trivial ct));
- in Thm.implies_elim thm' thm end;
-
-
(* code generation *)
fun mk_random_eq tyco vs extN Ts =
@@ -2201,31 +2179,12 @@
rtac (@{thm prop_subst} OF [surjective]),
REPEAT o etac @{thm meta_allE}, atac]));
- fun split_object_prf () =
- let
- val cPI = cterm_of defs_thy (lambda r0 (Trueprop (P $ r0)));
- val _ $ Abs (_, _, P $ _) = fst (Logic.dest_equals (concl_of split_meta));
- val cP = cterm_of defs_thy P;
- val split_meta' = cterm_instantiate [(cP, cPI)] split_meta;
- val (l, r) = HOLogic.dest_eq (HOLogic.dest_Trueprop split_object_prop);
- val cl = cterm_of defs_thy (HOLogic.mk_Trueprop l);
- val cr = cterm_of defs_thy (HOLogic.mk_Trueprop r);
- val thl =
- Thm.assume cl (*All r. P r*) (* 1 *)
- |> obj_to_meta_all (*!!r. P r*)
- |> Thm.equal_elim split_meta' (*!!n m more. P (ext n m more)*)
- |> meta_to_obj_all (*All n m more. P (ext n m more)*) (* 2*)
- |> Thm.implies_intr cl (* 1 ==> 2 *)
- val thr =
- Thm.assume cr (*All n m more. P (ext n m more)*)
- |> obj_to_meta_all (*!!n m more. P (ext n m more)*)
- |> Thm.equal_elim (Thm.symmetric split_meta') (*!!r. P r*)
- |> meta_to_obj_all (*All r. P r*)
- |> Thm.implies_intr cr (* 2 ==> 1 *)
- in thr COMP (thl COMP iffI) end;
-
val split_object = timeit_msg ctxt "record split_object proof:" (fn () =>
- future_forward_prf defs_thy split_object_prf split_object_prop);
+ Skip_Proof.prove_global defs_thy [] [] split_object_prop
+ (fn _ =>
+ rtac @{lemma "Trueprop A == Trueprop B ==> A = B" by (rule iffI) unfold} 1 THEN
+ rewrite_goals_tac @{thms atomize_all [symmetric]} THEN
+ rtac split_meta 1));
val split_ex = timeit_msg ctxt "record split_ex proof:" (fn () =>
let