diff options
Diffstat (limited to 'spartan/core')
| -rw-r--r-- | spartan/core/Spartan.thy | 25 | ||||
| -rw-r--r-- | spartan/core/goals.ML | 9 |
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 |