1.1 --- a/src/HOL/Tools/rewrite_hol_proof.ML Thu Jun 03 23:17:57 2010 +0200
1.2 +++ b/src/HOL/Tools/rewrite_hol_proof.ML Thu Jun 03 23:56:05 2010 +0200
1.3 @@ -13,8 +13,6 @@
1.4 structure RewriteHOLProof : REWRITE_HOL_PROOF =
1.5 struct
1.6
1.7 -open Proofterm;
1.8 -
1.9 val rews = map (pairself (Proof_Syntax.proof_of_term @{theory} true) o
1.10 Logic.dest_equals o Logic.varify_global o Proof_Syntax.read_term @{theory} true propT)
1.11
1.12 @@ -311,14 +309,14 @@
1.13 | strip_cong ps (PThm (_, (("HOL.refl", _, _), _)) % SOME f %% _) = SOME (f, ps)
1.14 | strip_cong _ _ = NONE;
1.15
1.16 -val subst_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of subst))));
1.17 -val sym_prf = fst (strip_combt (fst (strip_combP (Thm.proof_of sym))));
1.18 +val subst_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of subst))));
1.19 +val sym_prf = fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of sym))));
1.20
1.21 fun make_subst Ts prf xs (_, []) = prf
1.22 | make_subst Ts prf xs (f, ((x, y), (prf', clprf)) :: ps) =
1.23 let val T = fastype_of1 (Ts, x)
1.24 in if x aconv y then make_subst Ts prf (xs @ [x]) (f, ps)
1.25 - else change_type (SOME [T]) subst_prf %> x %> y %>
1.26 + else Proofterm.change_type (SOME [T]) subst_prf %> x %> y %>
1.27 Abs ("z", T, list_comb (incr_boundvars 1 f,
1.28 map (incr_boundvars 1) xs @ Bound 0 ::
1.29 map (incr_boundvars 1 o snd o fst) ps)) %% clprf %% prf' %%
1.30 @@ -326,7 +324,8 @@
1.31 end;
1.32
1.33 fun make_sym Ts ((x, y), (prf, clprf)) =
1.34 - ((y, x), (change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
1.35 + ((y, x),
1.36 + (Proofterm.change_type (SOME [fastype_of1 (Ts, x)]) sym_prf %> x %> y %% clprf %% prf, clprf));
1.37
1.38 fun mk_AbsP P t = AbsP ("H", Option.map HOLogic.mk_Trueprop P, t);
1.39
1.40 @@ -334,15 +333,15 @@
1.41 Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
1.42 | elim_cong_aux Ts (PThm (_, (("HOL.iffD1", _, _), _)) % P % _ %% prf) =
1.43 Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
1.44 - (strip_cong [] (incr_pboundvars 1 0 prf))
1.45 + (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf))
1.46 | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % _ %% prf1 %% prf2) =
1.47 Option.map (make_subst Ts prf2 [] o
1.48 apsnd (map (make_sym Ts))) (strip_cong [] prf1)
1.49 | elim_cong_aux Ts (PThm (_, (("HOL.iffD2", _, _), _)) % _ % P %% prf) =
1.50 Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
1.51 - apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
1.52 + apsnd (map (make_sym Ts))) (strip_cong [] (Proofterm.incr_pboundvars 1 0 prf))
1.53 | elim_cong_aux _ _ = NONE;
1.54
1.55 -fun elim_cong Ts hs prf = Option.map (rpair no_skel) (elim_cong_aux Ts prf);
1.56 +fun elim_cong Ts hs prf = Option.map (rpair Proofterm.no_skel) (elim_cong_aux Ts prf);
1.57
1.58 end;
2.1 --- a/src/Pure/Proof/extraction.ML Thu Jun 03 23:17:57 2010 +0200
2.2 +++ b/src/Pure/Proof/extraction.ML Thu Jun 03 23:56:05 2010 +0200
2.3 @@ -30,8 +30,6 @@
2.4 structure Extraction : EXTRACTION =
2.5 struct
2.6
2.7 -open Proofterm;
2.8 -
2.9 (**** tools ****)
2.10
2.11 fun add_syntax thy =
2.12 @@ -116,7 +114,7 @@
2.13
2.14 in rew end;
2.15
2.16 -val chtype = change_type o SOME;
2.17 +val chtype = Proofterm.change_type o SOME;
2.18
2.19 fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
2.20 fun corr_name s vs = extr_name s vs ^ "_correctness";
2.21 @@ -135,7 +133,7 @@
2.22 | strip_abs n (Abs (_, _, t)) = strip_abs (n-1) t
2.23 | strip_abs _ _ = error "strip_abs: not an abstraction";
2.24
2.25 -val prf_subst_TVars = map_proof_types o typ_subst_TVars;
2.26 +val prf_subst_TVars = Proofterm.map_proof_types o typ_subst_TVars;
2.27
2.28 fun relevant_vars types prop = List.foldr (fn
2.29 (Var ((a, _), T), vs) => (case strip_type T of
2.30 @@ -371,10 +369,10 @@
2.31 val xs' = map (map_types typ_map) xs
2.32 in
2.33 prf |>
2.34 - Same.commit (map_proof_same (map_types typ_map) typ_map mk_hyp) |>
2.35 - fold_rev implies_intr_proof' (map snd constraints) |>
2.36 - fold_rev forall_intr_proof' xs' |>
2.37 - fold_rev implies_intr_proof' constraints'
2.38 + Same.commit (Proofterm.map_proof_same (map_types typ_map) typ_map mk_hyp) |>
2.39 + fold_rev Proofterm.implies_intr_proof' (map snd constraints) |>
2.40 + fold_rev Proofterm.forall_intr_proof' xs' |>
2.41 + fold_rev Proofterm.implies_intr_proof' constraints'
2.42 end;
2.43
2.44 (** expanding theorems / definitions **)
2.45 @@ -521,7 +519,7 @@
2.46
2.47 | corr d defs vs ts Ts hs cs (Abst (s, SOME T, prf)) (Abst (_, _, prf')) t =
2.48 let val (defs', corr_prf) = corr d defs vs [] (T :: Ts)
2.49 - (dummyt :: hs) cs prf (incr_pboundvars 1 0 prf')
2.50 + (dummyt :: hs) cs prf (Proofterm.incr_pboundvars 1 0 prf')
2.51 (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE)
2.52 in (defs', Abst (s, SOME T, corr_prf)) end
2.53
2.54 @@ -531,13 +529,15 @@
2.55 val u = if T = nullT then
2.56 (case t of SOME u => SOME (incr_boundvars 1 u) | NONE => NONE)
2.57 else (case t of SOME (Abs (_, _, u)) => SOME u | _ => NONE);
2.58 - val (defs', corr_prf) = corr d defs vs [] (T :: Ts) (prop :: hs)
2.59 - (prop :: cs) (incr_pboundvars 0 1 prf) (incr_pboundvars 0 1 prf') u;
2.60 + val (defs', corr_prf) =
2.61 + corr d defs vs [] (T :: Ts) (prop :: hs)
2.62 + (prop :: cs) (Proofterm.incr_pboundvars 0 1 prf)
2.63 + (Proofterm.incr_pboundvars 0 1 prf') u;
2.64 val rlz = Const ("realizes", T --> propT --> propT)
2.65 in (defs',
2.66 if T = nullT then AbsP ("R",
2.67 SOME (app_rlz_rews Ts vs (rlz $ nullt $ prop)),
2.68 - prf_subst_bounds [nullt] corr_prf)
2.69 + Proofterm.prf_subst_bounds [nullt] corr_prf)
2.70 else Abst (s, SOME T, AbsP ("R",
2.71 SOME (app_rlz_rews (T :: Ts) vs
2.72 (rlz $ Bound 0 $ incr_boundvars 1 prop)), corr_prf)))
2.73 @@ -581,7 +581,7 @@
2.74
2.75 | corr d defs vs ts Ts hs cs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
2.76 let
2.77 - val prf = join_proof body;
2.78 + val prf = Proofterm.join_proof body;
2.79 val (vs', tye) = find_inst prop Ts ts vs;
2.80 val shyps = mk_shyps tye;
2.81 val sprfs = mk_sprfs cs tye;
2.82 @@ -605,23 +605,26 @@
2.83 val corr_prf = mkabsp shyps corr_prf0;
2.84 val corr_prop = Reconstruct.prop_of corr_prf;
2.85 val corr_prf' =
2.86 - proof_combP (proof_combt
2.87 + Proofterm.proof_combP (Proofterm.proof_combt
2.88 (PThm (serial (),
2.89 ((corr_name name vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
2.90 - Future.value (approximate_proof_body corr_prf))), vfs_of corr_prop),
2.91 + Future.value (Proofterm.approximate_proof_body corr_prf))),
2.92 + vfs_of corr_prop),
2.93 map PBound (length shyps - 1 downto 0)) |>
2.94 - fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
2.95 + fold_rev Proofterm.forall_intr_proof'
2.96 + (map (get_var_type corr_prop) (vfs_of prop)) |>
2.97 mkabsp shyps
2.98 in
2.99 ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
2.100 - proof_combP (prf_subst_TVars tye' corr_prf', sprfs))
2.101 + Proofterm.proof_combP (prf_subst_TVars tye' corr_prf', sprfs))
2.102 end
2.103 - | SOME (_, (_, prf')) => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs)))
2.104 + | SOME (_, (_, prf')) =>
2.105 + (defs', Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs)))
2.106 | SOME rs => (case find vs' rs of
2.107 - SOME (_, prf') => (defs', proof_combP (prf_subst_TVars tye' prf', sprfs))
2.108 + SOME (_, prf') => (defs', Proofterm.proof_combP (prf_subst_TVars tye' prf', sprfs))
2.109 | NONE => error ("corr: no realizer for instance of theorem " ^
2.110 quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
2.111 - (Reconstruct.prop_of (proof_combt (prf0, ts))))))
2.112 + (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))))
2.113 end
2.114
2.115 | corr d defs vs ts Ts hs cs (prf0 as PAxm (s, prop, SOME Ts')) _ _ =
2.116 @@ -633,10 +636,10 @@
2.117 realizes_null vs' prop aconv prop then (defs, prf0)
2.118 else case find vs' (Symtab.lookup_list realizers s) of
2.119 SOME (_, prf) => (defs,
2.120 - proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye))
2.121 + Proofterm.proof_combP (prf_subst_TVars tye' prf, mk_sprfs cs tye))
2.122 | NONE => error ("corr: no realizer for instance of axiom " ^
2.123 quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
2.124 - (Reconstruct.prop_of (proof_combt (prf0, ts)))))
2.125 + (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))
2.126 end
2.127
2.128 | corr d defs vs ts Ts hs _ _ _ _ = error "corr: bad proof"
2.129 @@ -645,14 +648,14 @@
2.130
2.131 | extr d defs vs ts Ts hs (Abst (s, SOME T, prf)) =
2.132 let val (defs', t) = extr d defs vs []
2.133 - (T :: Ts) (dummyt :: hs) (incr_pboundvars 1 0 prf)
2.134 + (T :: Ts) (dummyt :: hs) (Proofterm.incr_pboundvars 1 0 prf)
2.135 in (defs', Abs (s, T, t)) end
2.136
2.137 | extr d defs vs ts Ts hs (AbsP (s, SOME t, prf)) =
2.138 let
2.139 val T = etype_of thy' vs Ts t;
2.140 - val (defs', t) = extr d defs vs [] (T :: Ts) (t :: hs)
2.141 - (incr_pboundvars 0 1 prf)
2.142 + val (defs', t) =
2.143 + extr d defs vs [] (T :: Ts) (t :: hs) (Proofterm.incr_pboundvars 0 1 prf)
2.144 in (defs',
2.145 if T = nullT then subst_bound (nullt, t) else Abs (s, T, t))
2.146 end
2.147 @@ -677,7 +680,7 @@
2.148
2.149 | extr d defs vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) =
2.150 let
2.151 - val prf = join_proof body;
2.152 + val prf = Proofterm.join_proof body;
2.153 val (vs', tye) = find_inst prop Ts ts vs;
2.154 val shyps = mk_shyps tye;
2.155 val tye' = (map fst (Term.add_tvars prop [] |> rev) ~~ Ts') @ tye
2.156 @@ -712,20 +715,22 @@
2.157 (Abs ("x", T, rlz $ list_comb (Bound 0, args') $ prop));
2.158
2.159 val corr_prf' = mkabsp shyps
2.160 - (chtype [] equal_elim_axm %> lhs %> rhs %%
2.161 - (chtype [propT] symmetric_axm %> rhs %> lhs %%
2.162 - (chtype [T, propT] combination_axm %> f %> f %> c %> t' %%
2.163 - (chtype [T --> propT] reflexive_axm %> f) %%
2.164 + (chtype [] Proofterm.equal_elim_axm %> lhs %> rhs %%
2.165 + (chtype [propT] Proofterm.symmetric_axm %> rhs %> lhs %%
2.166 + (chtype [T, propT] Proofterm.combination_axm %> f %> f %> c %> t' %%
2.167 + (chtype [T --> propT] Proofterm.reflexive_axm %> f) %%
2.168 PAxm (cname ^ "_def", eqn,
2.169 SOME (map TVar (Term.add_tvars eqn [] |> rev))))) %% corr_prf);
2.170 val corr_prop = Reconstruct.prop_of corr_prf';
2.171 val corr_prf'' =
2.172 - proof_combP (proof_combt
2.173 + Proofterm.proof_combP (Proofterm.proof_combt
2.174 (PThm (serial (),
2.175 ((corr_name s vs', corr_prop, SOME (map TVar (Term.add_tvars corr_prop [] |> rev))),
2.176 - Future.value (approximate_proof_body corr_prf'))), vfs_of corr_prop),
2.177 + Future.value (Proofterm.approximate_proof_body corr_prf'))),
2.178 + vfs_of corr_prop),
2.179 map PBound (length shyps - 1 downto 0)) |>
2.180 - fold_rev forall_intr_proof' (map (get_var_type corr_prop) (vfs_of prop)) |>
2.181 + fold_rev Proofterm.forall_intr_proof'
2.182 + (map (get_var_type corr_prop) (vfs_of prop)) |>
2.183 mkabsp shyps
2.184 in
2.185 ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
2.186 @@ -736,7 +741,7 @@
2.187 SOME (t, _) => (defs, subst_TVars tye' t)
2.188 | NONE => error ("extr: no realizer for instance of theorem " ^
2.189 quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
2.190 - (Reconstruct.prop_of (proof_combt (prf0, ts))))))
2.191 + (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts))))))
2.192 end
2.193
2.194 | extr d defs vs ts Ts hs (prf0 as PAxm (s, prop, SOME Ts')) =
2.195 @@ -748,7 +753,7 @@
2.196 SOME (t, _) => (defs, subst_TVars tye' t)
2.197 | NONE => error ("extr: no realizer for instance of axiom " ^
2.198 quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
2.199 - (Reconstruct.prop_of (proof_combt (prf0, ts)))))
2.200 + (Reconstruct.prop_of (Proofterm.proof_combt (prf0, ts)))))
2.201 end
2.202
2.203 | extr d defs vs ts Ts hs _ = error "extr: bad proof";
3.1 --- a/src/Pure/Proof/proof_rewrite_rules.ML Thu Jun 03 23:17:57 2010 +0200
3.2 +++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu Jun 03 23:56:05 2010 +0200
3.3 @@ -22,8 +22,6 @@
3.4 structure ProofRewriteRules : PROOF_REWRITE_RULES =
3.5 struct
3.6
3.7 -open Proofterm;
3.8 -
3.9 fun rew b _ _ =
3.10 let
3.11 fun ?? x = if b then SOME x else NONE;
3.12 @@ -33,9 +31,9 @@
3.13 let val Type (_, [Type (_, [U, _]), _]) = T
3.14 in SOME U end
3.15 else NONE;
3.16 - val equal_intr_axm = ax equal_intr_axm [];
3.17 - val equal_elim_axm = ax equal_elim_axm [];
3.18 - val symmetric_axm = ax symmetric_axm [propT];
3.19 + val equal_intr_axm = ax Proofterm.equal_intr_axm [];
3.20 + val equal_elim_axm = ax Proofterm.equal_elim_axm [];
3.21 + val symmetric_axm = ax Proofterm.symmetric_axm [propT];
3.22
3.23 fun rew' (PThm (_, (("Pure.protectD", _, _), _)) % _ %%
3.24 (PThm (_, (("Pure.protectI", _, _), _)) % _ %% prf)) = SOME prf
3.25 @@ -71,9 +69,10 @@
3.26 val _ $ A $ C = Envir.beta_norm X;
3.27 val _ $ B $ D = Envir.beta_norm Y
3.28 in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? B,
3.29 - equal_elim_axm %> C %> D %% incr_pboundvars 2 0 prf2 %%
3.30 + Proofterm.equal_elim_axm %> C %> D %% Proofterm.incr_pboundvars 2 0 prf2 %%
3.31 (PBound 1 %% (equal_elim_axm %> B %> A %%
3.32 - (symmetric_axm % ?? A % ?? B %% incr_pboundvars 2 0 prf1) %% PBound 0)))))
3.33 + (Proofterm.symmetric_axm % ?? A % ?? B %% Proofterm.incr_pboundvars 2 0 prf1) %%
3.34 + PBound 0)))))
3.35 end
3.36
3.37 | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
3.38 @@ -86,8 +85,9 @@
3.39 val _ $ B $ D = Envir.beta_norm X
3.40 in SOME (AbsP ("H1", ?? X, AbsP ("H2", ?? A,
3.41 equal_elim_axm %> D %> C %%
3.42 - (symmetric_axm % ?? C % ?? D %% incr_pboundvars 2 0 prf2)
3.43 - %% (PBound 1 %% (equal_elim_axm %> A %> B %% incr_pboundvars 2 0 prf1 %% PBound 0)))))
3.44 + (symmetric_axm % ?? C % ?? D %% Proofterm.incr_pboundvars 2 0 prf2) %%
3.45 + (PBound 1 %%
3.46 + (equal_elim_axm %> A %> B %% Proofterm.incr_pboundvars 2 0 prf1 %% PBound 0)))))
3.47 end
3.48
3.49 | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
3.50 @@ -99,7 +99,7 @@
3.51 val _ $ Q = Envir.beta_norm Y;
3.52 in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
3.53 equal_elim_axm %> incr_boundvars 1 P $ Bound 0 %> incr_boundvars 1 Q $ Bound 0 %%
3.54 - (incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
3.55 + (Proofterm.incr_pboundvars 1 1 prf %> Bound 0) %% (PBound 0 %> Bound 0))))
3.56 end
3.57
3.58 | rew' (PAxm ("Pure.equal_elim", _, _) % SOME X % SOME Y %%
3.59 @@ -114,7 +114,7 @@
3.60 val u = incr_boundvars 1 Q $ Bound 0
3.61 in SOME (AbsP ("H", ?? X, Abst ("x", ty T,
3.62 equal_elim_axm %> t %> u %%
3.63 - (symmetric_axm % ?? u % ?? t %% (incr_pboundvars 1 1 prf %> Bound 0))
3.64 + (symmetric_axm % ?? u % ?? t %% (Proofterm.incr_pboundvars 1 1 prf %> Bound 0))
3.65 %% (PBound 0 %> Bound 0))))
3.66 end
3.67
3.68 @@ -182,12 +182,12 @@
3.69 (PAxm ("Pure.reflexive", _, _) % _)) =
3.70 let val (U, V) = (case T of
3.71 Type (_, [U, V]) => (U, V) | _ => (dummyT, dummyT))
3.72 - in SOME (prf %% (ax combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %%
3.73 - (ax reflexive_axm [T] % ?? eq) %% (ax reflexive_axm [U] % ?? t)))
3.74 + in SOME (prf %% (ax Proofterm.combination_axm [U, V] %> eq % ?? eq % ?? t % ?? t %%
3.75 + (ax Proofterm.reflexive_axm [T] % ?? eq) %% (ax Proofterm.reflexive_axm [U] % ?? t)))
3.76 end
3.77
3.78 | rew' _ = NONE;
3.79 - in rew' #> Option.map (rpair no_skel) end;
3.80 + in rew' #> Option.map (rpair Proofterm.no_skel) end;
3.81
3.82 fun rprocs b = [rew b];
3.83 val _ = Context.>> (Context.map_theory (fold Proofterm.add_prf_rproc (rprocs false)));
3.84 @@ -231,7 +231,8 @@
3.85 (Abst (s, SOME T, fst (insert_refl defs (T :: Ts) prf)), false)
3.86 | insert_refl defs Ts (AbsP (s, t, prf)) =
3.87 (AbsP (s, t, fst (insert_refl defs Ts prf)), false)
3.88 - | insert_refl defs Ts prf = (case strip_combt prf of
3.89 + | insert_refl defs Ts prf =
3.90 + (case Proofterm.strip_combt prf of
3.91 (PThm (_, ((s, prop, SOME Ts), _)), ts) =>
3.92 if member (op =) defs s then
3.93 let
3.94 @@ -242,11 +243,12 @@
3.95 (fold_rev (fn x => fn b => Abs ("", dummyT, abstract_over (x, b))) vs rhs),
3.96 map the ts);
3.97 in
3.98 - (change_type (SOME [fastype_of1 (Ts, rhs')]) reflexive_axm %> rhs', true)
3.99 + (Proofterm.change_type (SOME [fastype_of1 (Ts, rhs')])
3.100 + Proofterm.reflexive_axm %> rhs', true)
3.101 end
3.102 else (prf, false)
3.103 | (_, []) => (prf, false)
3.104 - | (prf', ts) => (proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
3.105 + | (prf', ts) => (Proofterm.proof_combt' (fst (insert_refl defs Ts prf'), ts), false));
3.106
3.107 fun elim_defs thy r defs prf =
3.108 let
3.109 @@ -256,7 +258,7 @@
3.110 val f = if not r then I else
3.111 let
3.112 val cnames = map (fst o dest_Const o fst) defs';
3.113 - val thms = fold_proof_atoms true
3.114 + val thms = Proofterm.fold_proof_atoms true
3.115 (fn PThm (_, ((name, prop, _), _)) =>
3.116 if member (op =) defnames name orelse
3.117 not (exists_Const (member (op =) cnames o #1) prop)
3.118 @@ -291,7 +293,7 @@
3.119 | elim_varst (t as Var (xi, T)) = if member (op =) tv (xi, T) then t else mk_default' T
3.120 | elim_varst t = t;
3.121 in
3.122 - map_proof_terms (fn t =>
3.123 + Proofterm.map_proof_terms (fn t =>
3.124 if Term.exists_subterm hidden_variable t then Envir.beta_norm (elim_varst t) else t) I prf
3.125 end;
3.126
3.127 @@ -354,16 +356,16 @@
3.128 fun reconstruct prf prop = prf |>
3.129 Reconstruct.reconstruct_proof thy prop |>
3.130 Reconstruct.expand_proof thy [("", NONE)] |>
3.131 - Same.commit (map_proof_same Same.same Same.same hyp)
3.132 + Same.commit (Proofterm.map_proof_same Same.same Same.same hyp)
3.133 in
3.134 map2 reconstruct
3.135 - (of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S))
3.136 + (Proofterm.of_sort_proof thy (OfClass o apfst Type.strip_sorts) (subst T, S))
3.137 (Logic.mk_of_sort (T, S))
3.138 end;
3.139
3.140 fun expand_of_class thy Ts hs (OfClass (T, c)) =
3.141 mk_of_sort_proof thy hs (T, [c]) |>
3.142 - hd |> rpair no_skel |> SOME
3.143 + hd |> rpair Proofterm.no_skel |> SOME
3.144 | expand_of_class thy Ts hs _ = NONE;
3.145
3.146 end;
4.1 --- a/src/Pure/Proof/proof_syntax.ML Thu Jun 03 23:17:57 2010 +0200
4.2 +++ b/src/Pure/Proof/proof_syntax.ML Thu Jun 03 23:56:05 2010 +0200
4.3 @@ -23,8 +23,6 @@
4.4 structure Proof_Syntax : PROOF_SYNTAX =
4.5 struct
4.6
4.7 -open Proofterm;
4.8 -
4.9 (**** add special syntax for embedding proof terms ****)
4.10
4.11 val proofT = Type ("proof", []);
4.12 @@ -98,7 +96,7 @@
4.13
4.14 fun prf_of [] (Bound i) = PBound i
4.15 | prf_of Ts (Const (s, Type ("proof", _))) =
4.16 - change_type (if ty then SOME Ts else NONE)
4.17 + Proofterm.change_type (if ty then SOME Ts else NONE)
4.18 (case Long_Name.explode s of
4.19 "axm" :: xs =>
4.20 let
4.21 @@ -110,14 +108,15 @@
4.22 | "thm" :: xs =>
4.23 let val name = Long_Name.implode xs;
4.24 in (case AList.lookup (op =) thms name of
4.25 - SOME thm => fst (strip_combt (fst (strip_combP (Thm.proof_of thm))))
4.26 + SOME thm =>
4.27 + fst (Proofterm.strip_combt (fst (Proofterm.strip_combP (Thm.proof_of thm))))
4.28 | NONE => error ("Unknown theorem " ^ quote name))
4.29 end
4.30 | _ => error ("Illegal proof constant name: " ^ quote s))
4.31 | prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) =
4.32 (case try Logic.class_of_const c_class of
4.33 SOME c =>
4.34 - change_type (if ty then SOME Ts else NONE)
4.35 + Proofterm.change_type (if ty then SOME Ts else NONE)
4.36 (OfClass (TVar ((Name.aT, 0), []), c))
4.37 | NONE => error ("Bad class constant: " ^ quote c_class))
4.38 | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop
4.39 @@ -126,13 +125,13 @@
4.40 if T = proofT then
4.41 error ("Term variable abstraction may not bind proof variable " ^ quote s)
4.42 else Abst (s, if ty then SOME T else NONE,
4.43 - incr_pboundvars (~1) 0 (prf_of [] prf))
4.44 + Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf))
4.45 | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
4.46 AbsP (s, case t of
4.47 Const ("dummy_pattern", _) => NONE
4.48 | _ $ Const ("dummy_pattern", _) => NONE
4.49 | _ => SOME (mk_term t),
4.50 - incr_pboundvars 0 (~1) (prf_of [] prf))
4.51 + Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
4.52 | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
4.53 prf_of [] prf1 %% prf_of [] prf2
4.54 | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =
4.55 @@ -168,11 +167,11 @@
4.56 | term_of Ts (Abst (s, opT, prf)) =
4.57 let val T = the_default dummyT opT
4.58 in Const ("Abst", (T --> proofT) --> proofT) $
4.59 - Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
4.60 + Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf))
4.61 end
4.62 | term_of Ts (AbsP (s, t, prf)) =
4.63 AbsPt $ the_default (Term.dummy_pattern propT) t $
4.64 - Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
4.65 + Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf))
4.66 | term_of Ts (prf1 %% prf2) =
4.67 AppPt $ term_of Ts prf1 $ term_of Ts prf2
4.68 | term_of Ts (prf % opt) =
4.69 @@ -233,10 +232,10 @@
4.70
4.71 fun proof_syntax prf =
4.72 let
4.73 - val thm_names = Symtab.keys (fold_proof_atoms true
4.74 + val thm_names = Symtab.keys (Proofterm.fold_proof_atoms true
4.75 (fn PThm (_, ((name, _, _), _)) => if name <> "" then Symtab.update (name, ()) else I
4.76 | _ => I) [prf] Symtab.empty);
4.77 - val axm_names = Symtab.keys (fold_proof_atoms true
4.78 + val axm_names = Symtab.keys (Proofterm.fold_proof_atoms true
4.79 (fn PAxm (name, _, _) => Symtab.update (name, ()) | _ => I) [prf] Symtab.empty);
4.80 in
4.81 add_proof_syntax #>
4.82 @@ -249,8 +248,10 @@
4.83 val thy = Thm.theory_of_thm thm;
4.84 val prop = Thm.full_prop_of thm;
4.85 val prf = Thm.proof_of thm;
4.86 - val prf' = (case strip_combt (fst (strip_combP prf)) of
4.87 - (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then join_proof body else prf
4.88 + val prf' =
4.89 + (case Proofterm.strip_combt (fst (Proofterm.strip_combP prf)) of
4.90 + (PThm (_, ((_, prop', _), body)), _) =>
4.91 + if prop = prop' then Proofterm.join_proof body else prf
4.92 | _ => prf)
4.93 in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end;
4.94
5.1 --- a/src/Pure/Proof/proofchecker.ML Thu Jun 03 23:17:57 2010 +0200
5.2 +++ b/src/Pure/Proof/proofchecker.ML Thu Jun 03 23:56:05 2010 +0200
5.3 @@ -13,8 +13,6 @@
5.4 structure ProofChecker : PROOF_CHECKER =
5.5 struct
5.6
5.7 -open Proofterm;
5.8 -
5.9 (***** construct a theorem out of a proof term *****)
5.10
5.11 fun lookup_thm thy =
5.12 @@ -39,8 +37,8 @@
5.13 end;
5.14
5.15 fun pretty_prf thy vs Hs prf =
5.16 - let val prf' = prf |> prf_subst_bounds (map Free vs) |>
5.17 - prf_subst_pbounds (map (Hyp o prop_of) Hs)
5.18 + let val prf' = prf |> Proofterm.prf_subst_bounds (map Free vs) |>
5.19 + Proofterm.prf_subst_pbounds (map (Hyp o prop_of) Hs)
5.20 in
5.21 (Proof_Syntax.pretty_proof (Syntax.init_pretty_global thy) prf',
5.22 Syntax.pretty_term_global thy (Reconstruct.prop_of prf'))
6.1 --- a/src/Pure/Proof/reconstruct.ML Thu Jun 03 23:17:57 2010 +0200
6.2 +++ b/src/Pure/Proof/reconstruct.ML Thu Jun 03 23:56:05 2010 +0200
6.3 @@ -17,8 +17,6 @@
6.4 structure Reconstruct : RECONSTRUCT =
6.5 struct
6.6
6.7 -open Proofterm;
6.8 -
6.9 val quiet_mode = Unsynchronized.ref true;
6.10 fun message s = if !quiet_mode then () else writeln s;
6.11
6.12 @@ -28,7 +26,7 @@
6.13 fun forall_intr_vfs prop = fold_rev Logic.all
6.14 (vars_of prop @ frees_of prop) prop;
6.15
6.16 -fun forall_intr_vfs_prf prop prf = fold_rev forall_intr_proof'
6.17 +fun forall_intr_vfs_prf prop prf = fold_rev Proofterm.forall_intr_proof'
6.18 (vars_of prop @ frees_of prop) prf;
6.19
6.20
6.21 @@ -140,8 +138,8 @@
6.22 | SOME Ts => (Ts, env));
6.23 val prop' = subst_atomic_types (map TVar tvars @ map TFree tfrees ~~ Ts)
6.24 (forall_intr_vfs prop) handle Library.UnequalLengths =>
6.25 - error ("Wrong number of type arguments for " ^ quote (guess_name prf))
6.26 - in (prop', change_type (SOME Ts) prf, [], env', vTs) end;
6.27 + error ("Wrong number of type arguments for " ^ quote (Proofterm.guess_name prf))
6.28 + in (prop', Proofterm.change_type (SOME Ts) prf, [], env', vTs) end;
6.29
6.30 fun head_norm (prop, prf, cnstrts, env, vTs) =
6.31 (Envir.head_norm env prop, prf, cnstrts, env, vTs);
6.32 @@ -285,17 +283,17 @@
6.33
6.34 fun reconstruct_proof thy prop cprf =
6.35 let
6.36 - val (cprf' % SOME prop', thawf) = freeze_thaw_prf (cprf % SOME prop);
6.37 + val (cprf' % SOME prop', thawf) = Proofterm.freeze_thaw_prf (cprf % SOME prop);
6.38 val _ = message "Collecting constraints...";
6.39 val (t, prf, cs, env, _) = make_constraints_cprf thy
6.40 - (Envir.empty (maxidx_proof cprf ~1)) cprf';
6.41 + (Envir.empty (Proofterm.maxidx_proof cprf ~1)) cprf';
6.42 val cs' = map (fn p => (true, p, uncurry (union (op =))
6.43 (pairself (map (fst o dest_Var) o OldTerm.term_vars) p)))
6.44 (map (pairself (Envir.norm_term env)) ((t, prop')::cs));
6.45 val _ = message ("Solving remaining constraints (" ^ string_of_int (length cs') ^ ") ...");
6.46 val env' = solve thy cs' env
6.47 in
6.48 - thawf (norm_proof env' prf)
6.49 + thawf (Proofterm.norm_proof env' prf)
6.50 end;
6.51
6.52 fun prop_of_atom prop Ts = subst_atomic_types
6.53 @@ -357,24 +355,24 @@
6.54 val _ = message ("Reconstructing proof of " ^ a);
6.55 val _ = message (Syntax.string_of_term_global thy prop);
6.56 val prf' = forall_intr_vfs_prf prop
6.57 - (reconstruct_proof thy prop (join_proof body));
6.58 + (reconstruct_proof thy prop (Proofterm.join_proof body));
6.59 val (maxidx', prfs', prf) = expand
6.60 - (maxidx_proof prf' ~1) prfs prf'
6.61 - in (maxidx' + maxidx + 1, incr_indexes (maxidx + 1) prf,
6.62 + (Proofterm.maxidx_proof prf' ~1) prfs prf'
6.63 + in (maxidx' + maxidx + 1, Proofterm.incr_indexes (maxidx + 1) prf,
6.64 ((a, prop), (maxidx', prf)) :: prfs')
6.65 end
6.66 | SOME (maxidx', prf) => (maxidx' + maxidx + 1,
6.67 - incr_indexes (maxidx + 1) prf, prfs));
6.68 + Proofterm.incr_indexes (maxidx + 1) prf, prfs));
6.69 val tfrees = Term.add_tfrees prop [] |> rev;
6.70 val tye = map (fn ((s, j), _) => (s, maxidx + 1 + j))
6.71 (Term.add_tvars prop [] |> rev) @ map (rpair ~1 o fst) tfrees ~~ Ts;
6.72 val varify = map_type_tfree (fn p as (a, S) =>
6.73 if member (op =) tfrees p then TVar ((a, ~1), S) else TFree p)
6.74 in
6.75 - (maxidx', prfs', map_proof_types (typ_subst_TVars tye o varify) prf)
6.76 + (maxidx', prfs', Proofterm.map_proof_types (typ_subst_TVars tye o varify) prf)
6.77 end
6.78 | expand maxidx prfs prf = (maxidx, prfs, prf);
6.79
6.80 - in #3 (expand (maxidx_proof prf ~1) [] prf) end;
6.81 + in #3 (expand (Proofterm.maxidx_proof prf ~1) [] prf) end;
6.82
6.83 end;