diff options
| -rw-r--r-- | spartan/core/Spartan.thy | 25 | ||||
| -rw-r--r-- | spartan/core/goals.ML | 9 | ||||
| -rw-r--r-- | spartan/lib/List.thy | 18 | ||||
| -rw-r--r-- | spartan/lib/Maybe.thy | 2 | ||||
| -rw-r--r-- | spartan/lib/More_Types.thy | 50 |
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 |