# HG changeset patch # User wenzelm # Date 1208268725 -7200 # Node ID 60e0cf6bef896440826b01b71a927b3ea7156142 # Parent 43310f3721a51cc44e952de9e18b5a02cbb9d180 Thm.forall_elim_var(s); diff -r 43310f3721a5 -r 60e0cf6bef89 src/HOL/Tools/function_package/fundef_core.ML --- 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) diff -r 43310f3721a5 -r 60e0cf6bef89 src/HOL/Tools/function_package/induction_scheme.ML --- 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)) diff -r 43310f3721a5 -r 60e0cf6bef89 src/HOL/Tools/function_package/mutual.ML --- 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 diff -r 43310f3721a5 -r 60e0cf6bef89 src/HOL/Tools/res_axioms.ML --- 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; diff -r 43310f3721a5 -r 60e0cf6bef89 src/Pure/Proof/extraction.ML --- 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 diff -r 43310f3721a5 -r 60e0cf6bef89 src/Pure/conjunction.ML --- 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 diff -r 43310f3721a5 -r 60e0cf6bef89 src/Pure/drule.ML --- 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); diff -r 43310f3721a5 -r 60e0cf6bef89 src/Pure/more_thm.ML --- 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; diff -r 43310f3721a5 -r 60e0cf6bef89 src/Pure/old_goals.ML --- 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 diff -r 43310f3721a5 -r 60e0cf6bef89 src/Pure/simplifier.ML --- 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 diff -r 43310f3721a5 -r 60e0cf6bef89 src/Pure/tctical.ML --- 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 diff -r 43310f3721a5 -r 60e0cf6bef89 src/Tools/IsaPlanner/isand.ML --- 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 *)