aboutsummaryrefslogtreecommitdiff
path: root/spartan/core
diff options
context:
space:
mode:
Diffstat (limited to 'spartan/core')
-rw-r--r--spartan/core/Spartan.thy25
-rw-r--r--spartan/core/goals.ML9
2 files changed, 21 insertions, 13 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index 0a5fe4c..ed21934 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -6,7 +6,7 @@ imports
"HOL-Eisbach.Eisbach"
"HOL-Eisbach.Eisbach_Tools"
keywords
- "Theorem" "Lemma" "Corollary" "Proposition" :: thy_goal_stmt and
+ "Theorem" "Lemma" "Corollary" "Proposition" "Definition" :: thy_goal_stmt and
"focus" "\<guillemotright>" "\<^item>" "\<^enum>" "~" :: prf_script_goal % "proof" and
"congruence" "print_coercions" :: thy_decl and
"rhs" "derive" "prems" "vars" :: quasi_command
@@ -150,28 +150,29 @@ axiomatization where
\<rbrakk> \<Longrightarrow> \<Sum>x: A. B x \<equiv> \<Sum>x: A. B' x"
-section \<open>Proof commands\<close>
+section \<open>Infrastructure\<close>
+
+ML_file \<open>lib.ML\<close>
+ML_file \<open>types.ML\<close>
+
+subsection \<open>Proof commands\<close>
named_theorems typechk
-ML_file \<open>lib.ML\<close>
ML_file \<open>goals.ML\<close>
ML_file \<open>focus.ML\<close>
-ML_file \<open>types.ML\<close>
-
-section \<open>Congruence automation\<close>
+subsection \<open>Congruence automation\<close>
consts "rhs" :: \<open>'a\<close> ("..")
ML_file \<open>congruence.ML\<close>
-
-section \<open>Methods\<close>
-
ML_file \<open>elimination.ML\<close> \<comment> \<open>elimination rules\<close>
ML_file \<open>cases.ML\<close> \<comment> \<open>case reasoning rules\<close>
+subsection \<open>Methods\<close>
+
named_theorems intros and comps
lemmas
[intros] = PiF PiI SigF SigI and
@@ -275,8 +276,7 @@ setup \<open>map_theory_simpset (fn ctxt => ctxt addSolver (mk_solver "" typechk
method reduce uses add = (simp add: comps add | subst comps)+
-
-section \<open>Implicit notations\<close>
+subsection \<open>Implicits\<close>
text \<open>
\<open>?\<close> is used to mark implicit arguments in definitions, while \<open>{}\<close> is expanded
@@ -301,8 +301,7 @@ text \<open>Automatically insert inhabitation judgments where needed:\<close>
syntax inhabited :: \<open>o \<Rightarrow> prop\<close> ("(_)")
translations "inhabited A" \<rightharpoonup> "CONST has_type {} A"
-
-section \<open>Lambda coercion\<close>
+subsection \<open>Lambda coercion\<close>
\<comment> \<open>Coerce object lambdas to meta-lambdas\<close>
abbreviation (input) lambda :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close>
diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML
index 9f394f0..4b53a7f 100644
--- a/spartan/core/goals.ML
+++ b/spartan/core/goals.ML
@@ -204,11 +204,20 @@ fun theorem spec descr =
schematic_theorem_cmd
(case opt_derive of SOME "derive" => true | _ => false)
long descr NONE (K I) binding includes elems concl))
+
+fun definition spec descr =
+ Outer_Syntax.local_theory_to_proof' spec "definition via proof"
+ ((long_statement || short_statement) >>
+ (fn (long, binding, includes, elems, concl) => schematic_theorem_cmd
+ true long descr NONE (K I) binding includes elems concl))
+
+
in
val _ = theorem \<^command_keyword>\<open>Theorem\<close> "Theorem"
val _ = theorem \<^command_keyword>\<open>Lemma\<close> "Lemma"
val _ = theorem \<^command_keyword>\<open>Corollary\<close> "Corollary"
val _ = theorem \<^command_keyword>\<open>Proposition\<close> "Proposition"
+val _ = definition \<^command_keyword>\<open>Definition\<close> "Definition"
end