global declaration of abstract syntax for proof terms, with qualified names;
clarified modules;
--- a/src/HOL/Tools/rewrite_hol_proof.ML Sun Jul 21 12:28:02 2019 +0200
+++ b/src/HOL/Tools/rewrite_hol_proof.ML Sun Jul 21 15:19:07 2019 +0200
@@ -34,9 +34,9 @@
\<open>(meta_eq_to_obj_eq \<cdot> TYPE('U) \<cdot> x1 \<cdot> x2 \<bullet> prfU \<bullet>
(combination \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<cdot> x \<cdot> y \<bullet> prf1 \<bullet> prf2)) \<equiv>
(cong \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<cdot> x \<cdot> y \<bullet>
- (OfClass type_class \<cdot> TYPE('T)) \<bullet> prfU \<bullet>
- (meta_eq_to_obj_eq \<cdot> TYPE('T \<Rightarrow> 'U) \<cdot> f \<cdot> g \<bullet> (OfClass type_class \<cdot> TYPE('T \<Rightarrow> 'U)) \<bullet> prf1) \<bullet>
- (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> (OfClass type_class \<cdot> TYPE('T)) \<bullet> prf2))\<close>,
+ (Pure.OfClass type_class \<cdot> TYPE('T)) \<bullet> prfU \<bullet>
+ (meta_eq_to_obj_eq \<cdot> TYPE('T \<Rightarrow> 'U) \<cdot> f \<cdot> g \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T \<Rightarrow> 'U)) \<bullet> prf1) \<bullet>
+ (meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T)) \<bullet> prf2))\<close>,
\<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x1 \<cdot> x2 \<bullet> prfT \<bullet>
(axm.transitive \<cdot> TYPE('T) \<cdot> x \<cdot> y \<cdot> z \<bullet> prf1 \<bullet> prf2)) \<equiv>
@@ -54,9 +54,9 @@
\<open>(meta_eq_to_obj_eq \<cdot> TYPE('T \<Rightarrow> 'U) \<cdot> x1 \<cdot> x2 \<bullet> prfTU \<bullet>
(abstract_rule \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<bullet> prf)) \<equiv>
(ext \<cdot> TYPE('T) \<cdot> TYPE('U) \<cdot> f \<cdot> g \<bullet>
- (OfClass type_class \<cdot> TYPE('T)) \<bullet> (OfClass type_class \<cdot> TYPE('U)) \<bullet>
+ (Pure.OfClass type_class \<cdot> TYPE('T)) \<bullet> (Pure.OfClass type_class \<cdot> TYPE('U)) \<bullet>
(\<^bold>\<lambda>(x::'T). meta_eq_to_obj_eq \<cdot> TYPE('U) \<cdot> f x \<cdot> g x \<bullet>
- (OfClass type_class \<cdot> TYPE('U)) \<bullet> (prf \<cdot> x)))\<close>,
+ (Pure.OfClass type_class \<cdot> TYPE('U)) \<bullet> (prf \<cdot> x)))\<close>,
\<open>(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet>
(eq_reflection \<cdot> TYPE('T) \<cdot> x \<cdot> y \<bullet> prfT \<bullet> prf)) \<equiv> prf\<close>,
@@ -70,9 +70,9 @@
prfT \<bullet> arity_type_bool \<bullet>
(cong \<cdot> TYPE('T) \<cdot> TYPE('T\<Rightarrow>bool) \<cdot>
((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> A \<cdot> B \<bullet>
- prfT \<bullet> (OfClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
+ prfT \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
(HOL.refl \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<bullet>
- (OfClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
+ (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> B \<bullet> prfT \<bullet> prf1)) \<bullet>
(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> C \<cdot> D \<bullet> prfT \<bullet> prf2)) \<bullet>
(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> C \<bullet> prfT \<bullet> prf3))\<close>,
@@ -87,9 +87,9 @@
prfT \<bullet> arity_type_bool \<bullet>
(cong \<cdot> TYPE('T) \<cdot> TYPE('T\<Rightarrow>bool) \<cdot>
((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> A \<cdot> B \<bullet>
- prfT \<bullet> (OfClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
+ prfT \<bullet> (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>bool)) \<bullet>
(HOL.refl \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool) \<cdot> ((=) :: 'T\<Rightarrow>'T\<Rightarrow>bool) \<bullet>
- (OfClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
+ (Pure.OfClass type_class \<cdot> TYPE('T\<Rightarrow>'T\<Rightarrow>bool))) \<bullet>
(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> A \<cdot> B \<bullet> prfT \<bullet> prf1)) \<bullet>
(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> C \<cdot> D \<bullet> prfT \<bullet> prf2)) \<bullet>
(meta_eq_to_obj_eq \<cdot> TYPE('T) \<cdot> B \<cdot> D \<bullet> prfT \<bullet> prf3))\<close>,
@@ -155,7 +155,7 @@
((\<and>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<and>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
prfb \<bullet> prfbb \<bullet>
(HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<and>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
- (OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
+ (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
(HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
(* \<or> *)
@@ -181,7 +181,7 @@
((\<or>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<or>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
prfb \<bullet> prfbb \<bullet>
(HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<or>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
- (OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
+ (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
(HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
(* \<longrightarrow> *)
@@ -205,7 +205,7 @@
((\<longrightarrow>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<longrightarrow>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
prfb \<bullet> prfbb \<bullet>
(HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((\<longrightarrow>) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
- (OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
+ (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
(HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
(* \<not> *)
@@ -257,7 +257,7 @@
((=) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((=) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> A \<cdot> A \<bullet>
prfb \<bullet> prfbb \<bullet>
(HOL.refl \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool) \<cdot> ((=) :: bool\<Rightarrow>bool\<Rightarrow>bool) \<bullet>
- (OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
+ (Pure.OfClass type_class \<cdot> TYPE(bool\<Rightarrow>bool\<Rightarrow>bool))) \<bullet>
(HOL.refl \<cdot> TYPE(bool) \<cdot> A \<bullet> prfb)))\<close>,
(** transitivity, reflexivity, and symmetry **)
--- a/src/Pure/Proof/proof_syntax.ML Sun Jul 21 12:28:02 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Sun Jul 21 15:19:07 2019 +0200
@@ -6,10 +6,8 @@
signature PROOF_SYNTAX =
sig
- val proofT: typ
val add_proof_syntax: theory -> theory
val proof_of_term: theory -> bool -> term -> Proofterm.proof
- val term_of_proof: Proofterm.proof -> term
val cterm_of_proof: theory -> Proofterm.proof -> cterm * (cterm -> Proofterm.proof)
val read_term: theory -> bool -> typ -> string -> term
val read_proof: theory -> bool -> bool -> string -> Proofterm.proof
@@ -24,40 +22,23 @@
(**** add special syntax for embedding proof terms ****)
-val proofT = Type ("proof", []);
+val proofT = Proofterm.proofT;
+
+local
+
val paramT = Type ("param", []);
val paramsT = Type ("params", []);
val idtT = Type ("idt", []);
val aT = Term.aT [];
-
-(** constants for theorems and axioms **)
+fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);
-fun add_proof_atom_consts names thy =
- thy
- |> Sign.root_path
- |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
-
-
-(** constants for application and abstraction **)
-
-fun mixfix (sy, ps, p) = Mixfix (Input.string sy, ps, p, Position.no_range);
+in
fun add_proof_syntax thy =
thy
|> Sign.root_path
|> Sign.set_defsort []
- |> Sign.add_types_global
- [(Binding.make ("proof", \<^here>), 0, NoSyn)]
- |> fold (snd oo Sign.declare_const_global)
- [((Binding.make ("Appt", \<^here>), [proofT, aT] ---> proofT), mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
- ((Binding.make ("AppP", \<^here>), [proofT, proofT] ---> proofT), mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
- ((Binding.make ("Abst", \<^here>), (aT --> proofT) --> proofT), NoSyn),
- ((Binding.make ("AbsP", \<^here>), [propT, proofT --> proofT] ---> proofT), NoSyn),
- ((Binding.make ("Hyp", \<^here>), propT --> proofT), NoSyn),
- ((Binding.make ("Oracle", \<^here>), propT --> proofT), NoSyn),
- ((Binding.make ("OfClass", \<^here>), (Term.a_itselfT --> propT) --> proofT), NoSyn),
- ((Binding.make ("MinProof", \<^here>), proofT), Mixfix.mixfix "?")]
|> Sign.add_nonterminals_global
[Binding.make ("param", \<^here>),
Binding.make ("params", \<^here>)]
@@ -68,11 +49,14 @@
("_Lam1", [idtT, propT] ---> paramT, mixfix ("_: _", [0, 0], 0)),
("", paramT --> paramT, Mixfix.mixfix "'(_')"),
("", idtT --> paramsT, Mixfix.mixfix "_"),
- ("", paramT --> paramsT, Mixfix.mixfix "_")]
+ ("", paramT --> paramsT, Mixfix.mixfix "_"),
+ (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
+ (Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ \<bullet>/ _)", [4, 5], 4)),
+ (Lexicon.mark_const "Pure.MinProof", proofT, Mixfix.mixfix "?")]
|> Sign.add_syntax (Print_Mode.ASCII, true)
[("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1Lam _./ _)", [0, 3], 3)),
- (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)),
- (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ %%/ _)", [4, 5], 4))]
+ (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ %/ _)", [4, 5], 4)),
+ (Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ %%/ _)", [4, 5], 4))]
|> Sign.add_trrules (map Syntax.Parse_Print_Rule
[(Ast.mk_appl (Ast.Constant "_Lam")
[Ast.mk_appl (Ast.Constant "_Lam0")
@@ -83,12 +67,22 @@
(Ast.mk_appl (Ast.Constant "_Lam")
[Ast.mk_appl (Ast.Constant "_Lam1")
[Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"],
- Ast.mk_appl (Ast.Constant (Lexicon.mark_const "AbsP")) [Ast.Variable "A",
+ Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.AbsP")) [Ast.Variable "A",
(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]),
(Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"],
- Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Abst"))
+ Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Pure.Abst"))
[(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]);
+end;
+
+
+(** constants for theorems and axioms **)
+
+fun add_proof_atom_consts names thy =
+ thy
+ |> Sign.root_path
+ |> Sign.add_consts (map (fn name => (Binding.qualified_name name, proofT, NoSyn)) names);
+
(**** translation between proof terms and pure terms ****)
@@ -101,7 +95,7 @@
(Term.no_dummy_patterns t);
fun prf_of [] (Bound i) = PBound i
- | prf_of Ts (Const (s, Type ("proof", _))) =
+ | prf_of Ts (Const (s, Type ("Pure.proof", _))) =
Proofterm.change_type (if ty then SOME Ts else NONE)
(case Long_Name.explode s of
"axm" :: xs =>
@@ -119,30 +113,30 @@
| NONE => error ("Unknown theorem " ^ quote name))
end
| _ => error ("Illegal proof constant name: " ^ quote s))
- | prf_of Ts (Const ("OfClass", _) $ Const (c_class, _)) =
+ | prf_of Ts (Const ("Pure.OfClass", _) $ Const (c_class, _)) =
(case try Logic.class_of_const c_class of
SOME c =>
Proofterm.change_type (if ty then SOME Ts else NONE)
(OfClass (TVar ((Name.aT, 0), []), c))
| NONE => error ("Bad class constant: " ^ quote c_class))
- | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop
- | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
- | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) =
+ | prf_of Ts (Const ("Pure.Hyp", _) $ prop) = Hyp prop
+ | prf_of Ts (v as Var ((_, Type ("Pure.proof", _)))) = Hyp v
+ | prf_of [] (Const ("Pure.Abst", _) $ Abs (s, T, prf)) =
if T = proofT then
error ("Term variable abstraction may not bind proof variable " ^ quote s)
else Abst (s, if ty then SOME T else NONE,
Proofterm.incr_pboundvars (~1) 0 (prf_of [] prf))
- | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
+ | prf_of [] (Const ("Pure.AbsP", _) $ t $ Abs (s, _, prf)) =
AbsP (s, case t of
Const ("Pure.dummy_pattern", _) => NONE
| _ $ Const ("Pure.dummy_pattern", _) => NONE
| _ => SOME (mk_term t),
Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
- | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
+ | prf_of [] (Const ("Pure.AppP", _) $ prf1 $ prf2) =
prf_of [] prf1 %% prf_of [] prf2
- | prf_of Ts (Const ("Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) =
+ | prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) =
prf_of (T::Ts) prf
- | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
+ | prf_of [] (Const ("Pure.Appt", _) $ prf $ t) = prf_of [] prf %
(case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t))
| prf_of _ t = error ("Not a proof term:\n" ^
Syntax.string_of_term_global thy t)
@@ -150,48 +144,6 @@
in prf_of [] end;
-val AbsPt = Const ("AbsP", [propT, proofT --> proofT] ---> proofT);
-val AppPt = Const ("AppP", [proofT, proofT] ---> proofT);
-val Hypt = Const ("Hyp", propT --> proofT);
-val Oraclet = Const ("Oracle", propT --> proofT);
-val OfClasst = Const ("OfClass", (Term.itselfT dummyT --> propT) --> proofT);
-val MinProoft = Const ("MinProof", proofT);
-
-val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
- [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
-
-fun term_of _ (PThm (_, ((name, _, NONE), _))) =
- Const (Long_Name.append "thm" name, proofT)
- | term_of _ (PThm (_, ((name, _, SOME Ts), _))) =
- mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT))
- | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT)
- | term_of _ (PAxm (name, _, SOME Ts)) =
- mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT))
- | term_of _ (OfClass (T, c)) =
- mk_tyapp [T] (OfClasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT))
- | term_of _ (PBound i) = Bound i
- | term_of Ts (Abst (s, opT, prf)) =
- let val T = the_default dummyT opT
- in Const ("Abst", (T --> proofT) --> proofT) $
- Abs (s, T, term_of (T::Ts) (Proofterm.incr_pboundvars 1 0 prf))
- end
- | term_of Ts (AbsP (s, t, prf)) =
- AbsPt $ the_default Term.dummy_prop t $
- Abs (s, proofT, term_of (proofT::Ts) (Proofterm.incr_pboundvars 0 1 prf))
- | term_of Ts (prf1 %% prf2) =
- AppPt $ term_of Ts prf1 $ term_of Ts prf2
- | term_of Ts (prf % opt) =
- let val t = the_default Term.dummy opt
- in Const ("Appt",
- [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
- term_of Ts prf $ t
- end
- | term_of Ts (Hyp t) = Hypt $ t
- | term_of Ts (Oracle (_, t, _)) = Oraclet $ t
- | term_of Ts MinProof = MinProoft;
-
-val term_of_proof = term_of [];
-
fun cterm_of_proof thy prf =
let
val thm_names = map fst (Global_Theory.all_thms_of thy true);
@@ -201,7 +153,7 @@
|> add_proof_atom_consts
(map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names);
in
- (Thm.global_cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
+ (Thm.global_cterm_of thy' (Proofterm.term_of_proof prf), proof_of_term thy true o Thm.term_of)
end;
fun read_term thy topsort =
@@ -257,7 +209,7 @@
fun pretty_proof ctxt prf =
Proof_Context.pretty_term_abbrev
(Proof_Context.transfer (proof_syntax prf (Proof_Context.theory_of ctxt)) ctxt)
- (term_of_proof prf);
+ (Proofterm.term_of_proof prf);
fun pretty_clean_proof_of ctxt full thm =
pretty_proof ctxt (Reconstruct.clean_proof_of ctxt full thm);
--- a/src/Pure/proofterm.ML Sun Jul 21 12:28:02 2019 +0200
+++ b/src/Pure/proofterm.ML Sun Jul 21 15:19:07 2019 +0200
@@ -91,6 +91,8 @@
val prf_subst_bounds: term list -> proof -> proof
val prf_subst_pbounds: proof list -> proof -> proof
val freeze_thaw_prf: proof -> proof * (proof -> proof)
+ val proofT: typ
+ val term_of_proof: proof -> term
(** proof terms for specific inference rules **)
val implies_intr_proof: term -> proof -> proof
@@ -755,6 +757,59 @@
end;
+(**** proof terms as pure terms ****)
+
+val proofT = Type ("Pure.proof", []);
+
+local
+
+val AbsPt = Const ("Pure.AbsP", [propT, proofT --> proofT] ---> proofT);
+val AppPt = Const ("Pure.AppP", [proofT, proofT] ---> proofT);
+val Hypt = Const ("Pure.Hyp", propT --> proofT);
+val Oraclet = Const ("Pure.Oracle", propT --> proofT);
+val OfClasst = Const ("Pure.OfClass", (Term.itselfT dummyT --> propT) --> proofT);
+val MinProoft = Const ("Pure.MinProof", proofT);
+
+val mk_tyapp = fold (fn T => fn prf => Const ("Pure.Appt",
+ [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
+
+fun term_of _ (PThm (_, ((name, _, NONE), _))) =
+ Const (Long_Name.append "thm" name, proofT)
+ | term_of _ (PThm (_, ((name, _, SOME Ts), _))) =
+ mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT))
+ | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT)
+ | term_of _ (PAxm (name, _, SOME Ts)) =
+ mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT))
+ | term_of _ (OfClass (T, c)) =
+ mk_tyapp [T] (OfClasst $ Const (Logic.const_of_class c, Term.itselfT dummyT --> propT))
+ | term_of _ (PBound i) = Bound i
+ | term_of Ts (Abst (s, opT, prf)) =
+ let val T = the_default dummyT opT
+ in Const ("Pure.Abst", (T --> proofT) --> proofT) $
+ Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
+ end
+ | term_of Ts (AbsP (s, t, prf)) =
+ AbsPt $ the_default Term.dummy_prop t $
+ Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
+ | term_of Ts (prf1 %% prf2) =
+ AppPt $ term_of Ts prf1 $ term_of Ts prf2
+ | term_of Ts (prf % opt) =
+ let val t = the_default Term.dummy opt
+ in Const ("Pure.Appt",
+ [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
+ term_of Ts prf $ t
+ end
+ | term_of Ts (Hyp t) = Hypt $ t
+ | term_of Ts (Oracle (_, t, _)) = Oraclet $ t
+ | term_of Ts MinProof = MinProoft;
+
+in
+
+val term_of_proof = term_of [];
+
+end;
+
+
(***** implication introduction *****)
fun gen_implies_intr_proof f h prf =
--- a/src/Pure/pure_thy.ML Sun Jul 21 12:28:02 2019 +0200
+++ b/src/Pure/pure_thy.ML Sun Jul 21 15:19:07 2019 +0200
@@ -14,6 +14,8 @@
structure Pure_Thy: PURE_THY =
struct
+(* auxiliary *)
+
val typ = Simple_Syntax.read_typ;
val prop = Simple_Syntax.read_prop;
@@ -27,6 +29,18 @@
fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range);
fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range);
+fun add_deps_type c thy =
+ let
+ val n = Sign.arity_number thy c;
+ val typargs = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
+ in thy |> Theory.add_deps_global "" ((Defs.Type, c), typargs) [] end
+
+fun add_deps_const c thy =
+ let
+ val T = Logic.unvarifyT_global (Sign.the_const_type thy c);
+ val typargs = Sign.const_typargs thy (c, T);
+ in thy |> Theory.add_deps_global "" ((Defs.Const, c), typargs) [] end;
+
(* application syntax variants *)
@@ -70,11 +84,13 @@
[(Binding.make ("fun", \<^here>), 2, NoSyn),
(Binding.make ("prop", \<^here>), 0, NoSyn),
(Binding.make ("itself", \<^here>), 1, NoSyn),
- (Binding.make ("dummy", \<^here>), 0, NoSyn)]
- #> Theory.add_deps_global "fun" ((Defs.Type, "fun"), [typ "'a", typ "'b"]) []
- #> Theory.add_deps_global "prop" ((Defs.Type, "prop"), []) []
- #> Theory.add_deps_global "itself" ((Defs.Type, "itself"), [typ "'a"]) []
- #> Theory.add_deps_global "dummy" ((Defs.Type, "dummy"), []) []
+ (Binding.make ("dummy", \<^here>), 0, NoSyn),
+ (qualify (Binding.make ("proof", \<^here>)), 0, NoSyn)]
+ #> add_deps_type "fun"
+ #> add_deps_type "prop"
+ #> add_deps_type "itself"
+ #> add_deps_type "dummy"
+ #> add_deps_type "Pure.proof"
#> Sign.add_nonterminals_global
(map (fn name => Binding.make (name, \<^here>))
(Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
@@ -200,12 +216,20 @@
(qualify (Binding.make ("all", \<^here>)), typ "('a \<Rightarrow> prop) \<Rightarrow> prop", binder ("\<And>", 0, 0)),
(qualify (Binding.make ("prop", \<^here>)), typ "prop \<Rightarrow> prop", NoSyn),
(qualify (Binding.make ("type", \<^here>)), typ "'a itself", NoSyn),
- (qualify (Binding.make ("dummy_pattern", \<^here>)), typ "'a", Mixfix.mixfix "'_")]
- #> Theory.add_deps_global "Pure.eq" ((Defs.Const, "Pure.eq"), [typ "'a"]) []
- #> Theory.add_deps_global "Pure.imp" ((Defs.Const, "Pure.imp"), []) []
- #> Theory.add_deps_global "Pure.all" ((Defs.Const, "Pure.all"), [typ "'a"]) []
- #> Theory.add_deps_global "Pure.type" ((Defs.Const, "Pure.type"), [typ "'a"]) []
- #> Theory.add_deps_global "Pure.dummy_pattern" ((Defs.Const, "Pure.dummy_pattern"), [typ "'a"]) []
+ (qualify (Binding.make ("dummy_pattern", \<^here>)), typ "'a", Mixfix.mixfix "'_"),
+ (qualify (Binding.make ("Appt", \<^here>)), typ "Pure.proof \<Rightarrow> 'a \<Rightarrow> Pure.proof", NoSyn),
+ (qualify (Binding.make ("AppP", \<^here>)), typ "Pure.proof \<Rightarrow> Pure.proof \<Rightarrow> Pure.proof", NoSyn),
+ (qualify (Binding.make ("Abst", \<^here>)), typ "('a \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn),
+ (qualify (Binding.make ("AbsP", \<^here>)), typ "prop \<Rightarrow> (Pure.proof \<Rightarrow> Pure.proof) \<Rightarrow> Pure.proof", NoSyn),
+ (qualify (Binding.make ("Hyp", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
+ (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
+ (qualify (Binding.make ("OfClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn),
+ (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", Mixfix.mixfix "?")]
+ #> add_deps_const "Pure.eq"
+ #> add_deps_const "Pure.imp"
+ #> add_deps_const "Pure.all"
+ #> add_deps_const "Pure.type"
+ #> add_deps_const "Pure.dummy_pattern"
#> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
#> Sign.parse_translation Syntax_Trans.pure_parse_translation
#> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
--- a/src/Pure/pure_thy.scala Sun Jul 21 12:28:02 2019 +0200
+++ b/src/Pure/pure_thy.scala Sun Jul 21 15:19:07 2019 +0200
@@ -22,16 +22,16 @@
val TYPE: String = "Pure.type"
- /* proof terms (abstract syntax) */
+ /* abstract syntax for proof terms */
- val PROOF: String = "proof"
+ val PROOF: String = "Pure.proof"
- val APPT: String = "Appt"
- val APPP: String = "AppP"
- val ABST: String = "Abst"
- val ABSP: String = "AbsP"
- val HYP: String = "Hyp"
- val ORACLE: String = "Oracle"
- val OFCLASS: String = "OfClass"
- val MINPROOF: String = "MinProof"
+ val APPT: String = "Pure.Appt"
+ val APPP: String = "Pure.AppP"
+ val ABST: String = "Pure.Abst"
+ val ABSP: String = "Pure.AbsP"
+ val HYP: String = "Pure.Hyp"
+ val ORACLE: String = "Pure.Oracle"
+ val OFCLASS: String = "Pure.OfClass"
+ val MINPROOF: String = "Pure.MinProof"
}