diff -r 38ce84c83738 -r 96e2b9a6f074 src/Pure/Proof/proof_rewrite_rules.ML --- a/src/Pure/Proof/proof_rewrite_rules.ML Thu Jun 03 23:17:57 2010 +0200 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu Jun 03 23:56:05 2010 +0200 @@ -22,8 +22,6 @@ structure ProofRewriteRules : PROOF_REWRITE_RULES = struct -open Proofterm; - fun rew b _ _ = let fun ?? x = if b then SOME x else NONE; @@ -33,9 +31,9 @@ let val Type (_, [Type (_, [U, _]), _]) = T in SOME U end else NONE; - val equal_intr_axm = ax equal_intr_axm []; - val equal_elim_axm = ax equal_elim_axm []; - val symmetric_axm = ax symmetric_axm [propT]; + val equal_intr_axm = ax Proofterm.equal_intr_axm []; + val equal_elim_axm = ax Proofterm.equal_elim_axm []; + val symmetric_axm = ax Proofterm.symmetric_axm [propT]; fun rew' (PThm (_, (("Pure.protectD", _, _), _)) % _ %% (PThm (_, (("Pure.protectI", _, _), _)) % _ %% prf)) = SOME prf @@ -71,9 +69,10 @@ val _ $ A $ C = Envir.beta_norm X; val _ $ B $ D = Envir.beta_norm Y in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? B, - equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %% + Proofterm.equal_elim_axm %> C %> D %% Proofterm.incr_pboundvars 2 0 prf2 %% (PBound 1 %% (equal_elim_axm %> B %> A %% - (symmetric_axm % ?? A % ?? B %% incr_pboundvars 2 0 prf1) %% PBound 0))))) + (Proofterm.symmetric_axm % ?? A % ?? B %% Proofterm.incr_pboundvars 2 0 prf1) %% + PBound 0))))) end | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %% @@ -86,8 +85,9 @@ val _ $ B $ D = Envir.beta_norm X in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? A, equal_elim_axm %> D %> C %% - (symmetric_axm % ?? C % ?? D %% incr_pboundvars 2 0 prf2) - %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0))))) + (symmetric_axm % ?? C % ?? D %% Proofterm.incr_pboundvars 2 0 prf2) %% + (PBound 1 %% + (equal_elim_axm %> A %> B %% Proofterm.incr_pboundvars 2 0 prf1 %% PBound 0))))) end | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %% @@ -99,7 +99,7 @@ val _ $ Q = Envir.beta_norm Y; in SOME (AbsP ("H", ?? X, Abst ("x", ty T, equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %% - (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0)))) + (Proofterm.incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0)))) end | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %% @@ -114,7 +114,7 @@ val u = incr_boundvars 1 Q $ Bound 0 in SOME (AbsP ("H", ?? X, Abst ("x", ty T, equal_elim_axm %> t %> u %% - (symmetric_axm % ?? u % ?? t %% (incr_pboundvars 1 1 prf %> Bound 0)) + (symmetric_axm % ?? u % ?? t %% (Proofterm.incr_pboundvars 1 1 prf %> Bound 0)) %% (PBound 0 %> Bound 0)))) end @@ -182,12 +182,12 @@ (PAxm ("Pure.reflexive", _, _) % _)) = let val (U, V) = (case T of Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT)) - in SOME (prf %% (ax combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %% - (ax reflexive_axm [T] % ?? eq) %% (ax reflexive_axm [U] % ?? t))) + in SOME (prf %% (ax Proofterm.combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %% + (ax Proofterm.reflexive_axm [T] % ?? eq) %% (ax Proofterm.reflexive_axm [U] % ?? t))) end | rew' _ = NONE; - in rew' #> Option.map (rpair no_skel) end; + in rew' #> Option.map (rpair Proofterm.no_skel) end; fun rprocs b = [rew b]; val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false))); @@ -231,7 +231,8 @@ (Abst (s, SOME T, fst (insert_refl defs (T :: Ts) prf)), false) | insert_refl defs Ts (AbsP (s, t, prf)) = (AbsP (s, t, fst (insert_refl defs Ts prf)), false) - | insert_refl defs Ts prf = (case strip_combt prf of + | insert_refl defs Ts prf = + (case Proofterm.strip_combt prf of (PThm (_, ((s, prop, SOME Ts), _)), ts) => if member (op =) defs s then let @@ -242,11 +243,12 @@ (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs), map the ts); in - (change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs', true) + (Proofterm.change_type (SOME [fastype_of1 (Ts, rhs')]) + Proofterm.reflexive_axm %> rhs', true) end else (prf, false) | (_, []) => (prf, false) - | (prf', ts) => (proof_combt' (fst (insert_refl defs Ts prf'), ts), false)); + | (prf', ts) => (Proofterm.proof_combt' (fst (insert_refl defs Ts prf'), ts), false)); fun elim_defs thy r defs prf = let @@ -256,7 +258,7 @@ val f = if not r then I else let val cnames = map (fst o dest_Const o fst) defs'; - val thms = fold_proof_atoms true + val thms = Proofterm.fold_proof_atoms true (fn PThm (_, ((name, prop, _), _)) => if member (op =) defnames name orelse not (exists_Const (member (op =) cnames o #1) prop) @@ -291,7 +293,7 @@ | elim_varst (t as Var (xi, T)) = if member (op =) tv (xi, T) then t else mk_default' T | elim_varst t = t; in - map_proof_terms (fn t => + Proofterm.map_proof_terms (fn t => if Term.exists_subterm hidden_variable t then Envir.beta_norm (elim_varst t) else t) I prf end; @@ -354,16 +356,16 @@ fun reconstruct prf prop = prf |> Reconstruct.reconstruct_proof thy prop |> Reconstruct.expand_proof thy [("", NONE)] |> - Same.commit (map_proof_same Same.same Same.same hyp) + Same.commit (Proofterm.map_proof_same Same.same Same.same hyp) in map2 reconstruct - (of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S)) + (Proofterm.of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S)) (Logic.mk_of_sort (T, S)) end; fun expand_of_class thy Ts hs (OfClass (T, c)) = mk_of_sort_proof thy hs (T, [c]) |> - hd |> rpair no_skel |> SOME + hd |> rpair Proofterm.no_skel |> SOME | expand_of_class thy Ts hs _ = NONE; end;