1. Initial `Definition` keyword. 2. ifelse.

1 files changed, 46 insertions, 4 deletions

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