aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--spartan/core/Spartan.thy25
-rw-r--r--spartan/core/goals.ML9
-rw-r--r--spartan/lib/List.thy18
-rw-r--r--spartan/lib/Maybe.thy2
-rw-r--r--spartan/lib/More_Types.thy50
5 files changed, 76 insertions, 28 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
diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index 1798a23..11b8406 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -50,7 +50,7 @@ lemmas
abbreviation "ListRec A C \<equiv> ListInd A (\<lambda>_. C)"
-Lemma (derive) ListCase:
+Lemma list_cases [cases]:
assumes
"xs: List A" and
nil_case: "c\<^sub>0: C (nil A)" and
@@ -59,8 +59,6 @@ Lemma (derive) ListCase:
shows "?List_cases A (\<lambda>xs. C xs) c\<^sub>0 (\<lambda>x xs. f x xs) xs: C xs"
by (elim xs) (fact nil_case, rule cons_case)
-lemmas List_cases [cases] = ListCase[unfolded ListCase_def]
-
section \<open>Notation\<close>
@@ -84,7 +82,7 @@ section \<open>Standard functions\<close>
subsection \<open>Head and tail\<close>
-Lemma (derive) head:
+Definition head:
assumes "A: U i" "xs: List A"
shows "Maybe A"
proof (cases xs)
@@ -92,7 +90,7 @@ proof (cases xs)
show "\<And>x. x: A \<Longrightarrow> some x: Maybe A" by intro
qed
-Lemma (derive) tail:
+Definition tail:
assumes "A: U i" "xs: List A"
shows "List A"
proof (cases xs)
@@ -115,7 +113,7 @@ Lemma head_type [typechk]:
Lemma head_of_cons [comps]:
assumes "A: U i" "x: A" "xs: List A"
shows "head (x # xs) \<equiv> some x"
- unfolding head_def ListCase_def by reduce
+ unfolding head_def by reduce
Lemma tail_type [typechk]:
assumes "A: U i" "xs: List A"
@@ -125,11 +123,11 @@ Lemma tail_type [typechk]:
Lemma tail_of_cons [comps]:
assumes "A: U i" "x: A" "xs: List A"
shows "tail (x # xs) \<equiv> xs"
- unfolding tail_def ListCase_def by reduce
+ unfolding tail_def by reduce
subsection \<open>Append\<close>
-Lemma (derive) app:
+Definition app:
assumes "A: U i" "xs: List A" "ys: List A"
shows "List A"
apply (elim xs)
@@ -144,7 +142,7 @@ translations "app" \<leftharpoondown> "CONST List.app A"
subsection \<open>Map\<close>
-Lemma (derive) map:
+Definition map:
assumes "A: U i" "B: U i" "f: A \<rightarrow> B" "xs: List A"
shows "List B"
proof (elim xs)
@@ -166,7 +164,7 @@ Lemma map_type [typechk]:
subsection \<open>Reverse\<close>
-Lemma (derive) rev:
+Definition rev:
assumes "A: U i" "xs: List A"
shows "List A"
apply (elim xs)
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index 1efbb95..6729812 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -17,7 +17,7 @@ lemma
Maybe_some: "a: A \<Longrightarrow> some A a: Maybe A"
unfolding Maybe_def none_def some_def by typechk+
-Lemma (derive) MaybeInd:
+Definition MaybeInd:
assumes
"A: U i"
"\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
diff --git a/spartan/lib/More_Types.thy b/spartan/lib/More_Types.thy
index 1d7abb9..38ba2aa 100644
--- a/spartan/lib/More_Types.thy
+++ b/spartan/lib/More_Types.thy
@@ -1,5 +1,3 @@
-chapter \<open>Some standard types\<close>
-
theory More_Types
imports Spartan
@@ -96,9 +94,53 @@ Lemma
Bool_false: "false: Bool"
unfolding Bool_def true_def false_def by typechk+
-lemmas [intros] = BoolF Bool_true Bool_false
+\<comment> \<open>Definitions like these should be handled by a future function package\<close>
+Definition ifelse [rotated 1]:
+ assumes *[unfolded Bool_def true_def false_def]:
+ "\<And>x. x: Bool \<Longrightarrow> C x: U i"
+ "x: Bool"
+ "a: C true"
+ "b: C false"
+ shows "C x"
+ by (elim x) (elim, rule *)+
+
+Lemma if_true:
+ assumes
+ "\<And>x. x: Bool \<Longrightarrow> C x: U i"
+ "a: C true"
+ "b: C false"
+ shows "ifelse C true a b \<equiv> a"
+ unfolding ifelse_def true_def
+ supply assms[unfolded Bool_def true_def false_def]
+ by reduce
+
+Lemma if_false:
+ assumes
+ "\<And>x. x: Bool \<Longrightarrow> C x: U i"
+ "a: C true"
+ "b: C false"
+ shows "ifelse C false a b \<equiv> b"
+ unfolding ifelse_def false_def
+ supply assms[unfolded Bool_def true_def false_def]
+ by reduce
+
+lemmas
+ [intros] = BoolF Bool_true Bool_false and
+ [comps] = if_true if_false and
+ [elims ?x] = ifelse
+lemmas
+ BoolE = ifelse
+
+subsection \<open>Notation\<close>
+
+definition ifelse_i ("if _ then _ else _")
+ where [implicit]: "if x then a else b \<equiv> ifelse ? x a b"
+
+no_translations "if x then a else b" \<leftharpoondown> "CONST ifelse C x a b"
+
+subsection \<open>Logical connectives\<close>
-\<comment> \<open>Can define if-then-else etc.\<close>
+definition not ("!_") where "not x \<equiv> ifelse (K Bool) x false true"
end