--- a/src/HOL/Tools/function_package/fundef_core.ML Tue Apr 15 16:12:01 2008 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML Tue Apr 15 16:12:05 2008 +0200
@@ -416,7 +416,7 @@
Abs ("y", ranT, G $ Bound 1 $ Bound 0)))
|> cterm_of thy
- val ihyp_thm = assume ihyp |> forall_elim_vars 0
+ val ihyp_thm = assume ihyp |> Thm.forall_elim_vars 0
val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
|> instantiate' [] [NONE, SOME (cterm_of thy h)]
@@ -430,7 +430,7 @@
val _ = Output.debug (K "Proving: Graph is a function")
val graph_is_function = complete
- |> forall_elim_vars 0
+ |> Thm.forall_elim_vars 0
|> fold (curry op COMP) ex1s
|> implies_intr (ihyp)
|> implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x)))
@@ -652,7 +652,7 @@
val (cases, steps) = split_list (map prove_case clauses)
val istep = complete_thm
- |> forall_elim_vars 0
+ |> Thm.forall_elim_vars 0
|> fold (curry op COMP) cases (* P x *)
|> implies_intr ihyp
|> implies_intr (cprop_of x_D)
@@ -700,7 +700,7 @@
in
Goal.init goal
|> (SINGLE (resolve_tac [accI] 1)) |> the
- |> (SINGLE (eresolve_tac [forall_elim_vars 0 R_cases] 1)) |> the
+ |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the
|> (SINGLE (CLASIMPSET auto_tac)) |> the
|> Goal.conclude
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
@@ -778,7 +778,7 @@
$ HOLogic.mk_Trueprop (acc_R $ Bound 0))
|> cterm_of thy
- val ihyp_a = assume ihyp |> forall_elim_vars 0
+ val ihyp_a = assume ihyp |> Thm.forall_elim_vars 0
val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x))
@@ -821,7 +821,7 @@
let
val Globals {domT, ranT, fvar, ...} = globals
- val R_cases = forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
+ val R_cases = Thm.forall_elim_vars 0 R_cases (* FIXME: Should be already in standard form. *)
val graph_implies_dom = (* "G ?x ?y ==> dom ?x" *)
Goal.prove octxt ["x", "y"] [HOLogic.mk_Trueprop (G $ Free ("x", domT) $ Free ("y", ranT))]
@@ -847,7 +847,7 @@
Goal.prove ctxt [] [] trsimp
(fn _ =>
rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
- THEN (rtac (forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
+ THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
THEN (SIMPSET' simp_default_tac 1)
THEN (etac not_acc_down 1)
THEN ((etac R_cases) THEN_ALL_NEW (SIMPSET' simp_default_tac)) 1)
@@ -921,7 +921,7 @@
val (graph_is_function, complete_thm) =
provedgoal
|> Conjunction.elim
- |> apfst (forall_elim_vars 0)
+ |> apfst (Thm.forall_elim_vars 0)
val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff)
--- a/src/HOL/Tools/function_package/induction_scheme.ML Tue Apr 15 16:12:01 2008 +0200
+++ b/src/HOL/Tools/function_package/induction_scheme.ML Tue Apr 15 16:12:05 2008 +0200
@@ -262,13 +262,13 @@
val res = Conjunction.intr_balanced (map_index project concls)
|> fold_rev (implies_intr o cprop_of) acases
- |> forall_elim_vars 0
+ |> Thm.forall_elim_vars 0
in
(fn st =>
Drule.compose_single (res, i, st)
|> fold_rev (implies_intr o cprop_of) (complete :: wf_thm :: flat ineqss)
|> forall_intr (cert R)
- |> forall_elim_vars 0
+ |> Thm.forall_elim_vars 0
|> Seq.single
)
end))
--- a/src/HOL/Tools/function_package/mutual.ML Tue Apr 15 16:12:01 2008 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML Tue Apr 15 16:12:05 2008 +0200
@@ -222,7 +222,7 @@
fold (fn x => fn thm => combination thm (reflexive x)) xs thm
|> Conv.fconv_rule (Thm.beta_conversion true)
|> fold_rev forall_intr xs
- |> forall_elim_vars 0
+ |> Thm.forall_elim_vars 0
end
--- a/src/HOL/Tools/res_axioms.ML Tue Apr 15 16:12:01 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML Tue Apr 15 16:12:05 2008 +0200
@@ -282,7 +282,7 @@
fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1
in Goal.prove_internal [ex_tm] conc tacf
|> forall_intr_list frees
- |> forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
+ |> Thm.forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
|> Thm.varifyT
end;
--- a/src/Pure/Proof/extraction.ML Tue Apr 15 16:12:01 2008 +0200
+++ b/src/Pure/Proof/extraction.ML Tue Apr 15 16:12:05 2008 +0200
@@ -739,7 +739,7 @@
thy'
|> PureThy.store_thm (corr_name s vs,
Thm.varifyT (funpow (length (term_vars corr_prop))
- (forall_elim_var 0) (forall_intr_frees
+ (Thm.forall_elim_var 0) (forall_intr_frees
(ProofChecker.thm_of_proof thy'
(fst (Proofterm.freeze_thaw_prf prf))))))
|> snd
--- a/src/Pure/conjunction.ML Tue Apr 15 16:12:01 2008 +0200
+++ b/src/Pure/conjunction.ML Tue Apr 15 16:12:05 2008 +0200
@@ -74,7 +74,7 @@
fun conjunctionD which =
Drule.implies_intr_list [A, B] (Thm.assume (which (A, B))) COMP
- Drule.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B));
+ Thm.forall_elim_vars 0 (Thm.equal_elim conjunction_def (Thm.assume A_B));
in
@@ -130,7 +130,7 @@
fun comp_rule th rule =
Thm.adjust_maxidx_thm ~1 (th COMP
- (rule |> Drule.forall_intr_frees |> Drule.forall_elim_vars (Thm.maxidx_of th + 1)));
+ (rule |> Drule.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
in
--- a/src/Pure/drule.ML Tue Apr 15 16:12:01 2008 +0200
+++ b/src/Pure/drule.ML Tue Apr 15 16:12:05 2008 +0200
@@ -25,8 +25,6 @@
val forall_intr_frees: thm -> thm
val forall_intr_vars: thm -> thm
val forall_elim_list: cterm list -> thm -> thm
- val forall_elim_var: int -> thm -> thm
- val forall_elim_vars: int -> thm -> thm
val gen_all: thm -> thm
val lift_all: cterm -> thm -> thm
val freeze_thaw: thm -> thm * (thm -> thm)
@@ -290,9 +288,6 @@
fold forall_intr
(map (Thm.cterm_of (Thm.theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th [])) th;
-val forall_elim_var = PureThy.forall_elim_var;
-val forall_elim_vars = PureThy.forall_elim_vars;
-
fun outer_params t =
let val vs = Term.strip_all_vars t
in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
@@ -373,7 +368,7 @@
#> forall_intr_frees
#> `Thm.maxidx_of
#-> (fn maxidx =>
- forall_elim_vars (maxidx + 1)
+ Thm.forall_elim_vars (maxidx + 1)
#> Thm.strip_shyps
#> zero_var_indexes
#> Thm.varifyT);
--- a/src/Pure/more_thm.ML Tue Apr 15 16:12:01 2008 +0200
+++ b/src/Pure/more_thm.ML Tue Apr 15 16:12:05 2008 +0200
@@ -52,6 +52,8 @@
-> cterm list * (indexname * typ)list
val read_cterm: theory -> string * typ -> cterm
val elim_implies: thm -> thm -> thm
+ val forall_elim_var: int -> thm -> thm
+ val forall_elim_vars: int -> thm -> thm
val unvarify: thm -> thm
val close_derivation: thm -> thm
val add_axiom: term list -> bstring * term -> theory -> thm * theory
@@ -129,7 +131,7 @@
fun eq_thm ths =
Context.joinable (pairself Thm.theory_of_thm ths) andalso
- thm_ord ths = EQUAL;
+ is_equal (thm_ord ths);
val eq_thms = eq_list eq_thm;
@@ -233,7 +235,36 @@
*)
fun elim_implies thA thAB = Thm.implies_elim thAB thA;
-(*global schematic variables*)
+
+(* forall_elim_var(s) *)
+
+local
+
+fun forall_elim_vars_aux strip_vars i th =
+ let
+ val thy = Thm.theory_of_thm th;
+ val {tpairs, prop, ...} = Thm.rep_thm th;
+ val add_used = Term.fold_aterms
+ (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I);
+ val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []);
+ val vars = strip_vars prop;
+ val cvars = (Name.variant_list used (map #1 vars), vars)
+ |> ListPair.map (fn (x, (_, T)) => Thm.cterm_of thy (Var ((x, i), T)));
+ in fold Thm.forall_elim cvars th end;
+
+in
+
+val forall_elim_vars = forall_elim_vars_aux Term.strip_all_vars;
+
+fun forall_elim_var i th = forall_elim_vars_aux
+ (fn Const ("all", _) $ Abs (a, T, _) => [(a, T)]
+ | _ => raise THM ("forall_elim_vars", i, [th])) i th;
+
+end;
+
+
+(* unvarify: global schematic variables *)
+
fun unvarify th =
let
val thy = Thm.theory_of_thm th;
@@ -251,6 +282,9 @@
in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
in Thm.instantiate (instT, inst) th end;
+
+(* close_derivation *)
+
fun close_derivation thm =
if Thm.get_name thm = "" then Thm.put_name "" thm
else thm;
--- a/src/Pure/old_goals.ML Tue Apr 15 16:12:01 2008 +0200
+++ b/src/Pure/old_goals.ML Tue Apr 15 16:12:05 2008 +0200
@@ -159,7 +159,7 @@
forall (fn t => not (can Logic.dest_implies t orelse can Logic.dest_all t)) As;
val (As,B) = if atoms then ([],horn) else (As,B);
val cAs = map (cterm_of thy) As;
- val prems = map (rewrite_rule rths o forall_elim_vars 0 o Thm.assume) cAs;
+ val prems = map (rewrite_rule rths o Thm.forall_elim_vars 0 o Thm.assume) cAs;
val cB = cterm_of thy B;
val st0 = let val st = Goal.init cB |> fold Thm.weaken cAs
in rewrite_goals_rule rths st end
--- a/src/Pure/simplifier.ML Tue Apr 15 16:12:01 2008 +0200
+++ b/src/Pure/simplifier.ML Tue Apr 15 16:12:05 2008 +0200
@@ -417,7 +417,7 @@
if can Logic.dest_equals (Thm.concl_of thm) then [thm]
else [thm RS reflect] handle THM _ => [];
- fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
+ fun mksimps thm = mk_eq (Thm.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
in
empty_ss setsubgoaler asm_simp_tac
setSSolver safe_solver
--- a/src/Pure/tctical.ML Tue Apr 15 16:12:01 2008 +0200
+++ b/src/Pure/tctical.ML Tue Apr 15 16:12:05 2008 +0200
@@ -429,7 +429,7 @@
val cterm = Thm.cterm_of (Thm.theory_of_thm state)
val chyps = map cterm hyps
val hypths = map assume chyps
- val subprems = map (forall_elim_vars 0) hypths
+ val subprems = map (Thm.forall_elim_vars 0) hypths
val fparams = map Free params
val cparams = map cterm fparams
fun swap_ctpair (t,u) = (cterm u, cterm t)
@@ -481,7 +481,7 @@
let val prem = Logic.nth_prem (i, Thm.prop_of state)
and cterm = cterm_of (Thm.theory_of_thm state)
val (_,_,hyps,_) = metahyps_split_prem prem
- in SOME (map (forall_elim_vars 0 o assume o cterm) hyps) end
+ in SOME (map (Thm.forall_elim_vars 0 o Thm.assume o cterm) hyps) end
handle TERM ("nth_prem", [A]) => NONE;
local
--- a/src/Tools/IsaPlanner/isand.ML Tue Apr 15 16:12:01 2008 +0200
+++ b/src/Tools/IsaPlanner/isand.ML Tue Apr 15 16:12:05 2008 +0200
@@ -181,7 +181,7 @@
val ct = ctermify allified_term;
val typ_allified_ct = ctermify (allify_term_typs tyvs allified_term);
in (typ_allified_ct,
- Drule.forall_elim_vars 0 (Thm.assume ct)) end;
+ Thm.forall_elim_vars 0 (Thm.assume ct)) end;
(* change type-vars to fresh type frees *)
@@ -271,7 +271,7 @@
(* make free vars into schematic vars with index zero *)
fun unfix_frees frees =
- apply (map (K (Drule.forall_elim_var 0)) frees)
+ apply (map (K (Thm.forall_elim_var 0)) frees)
o Drule.forall_intr_list frees;
(* fix term and type variables *)