aboutsummaryrefslogtreecommitdiff
path: root/spartan/lib
diff options
context:
space:
mode:
authorJosh Chen2020-07-21 02:16:14 +0200
committerGitHub2020-07-21 02:16:14 +0200
commitdfd241b2d85fc5a4ad4d7ddd64adf0138b05f083 (patch)
treeb4c4280b1bc4426059ddd184a2258d15d20a0bab /spartan/lib
parent6aaf4d5b28a5284b3b02fa5c410d2d83a711840b (diff)
parent12eed8685674b7d5ff7bc45a44a061e01f99ce5f (diff)
Merge pull request #8 from jaycech3n/dev
Merge big diff on dev
Diffstat (limited to 'spartan/lib')
-rw-r--r--spartan/lib/List.thy13
-rw-r--r--spartan/lib/Maybe.thy7
-rw-r--r--spartan/lib/More_Types.thy30
3 files changed, 28 insertions, 22 deletions
diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index a755859..be86b63 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -44,9 +44,10 @@ where
f x xs (ListInd A (fn xs. C xs) c\<^sub>0 (fn x xs rec. f x xs rec) xs)"
lemmas
- [intros] = ListF List_nil List_cons and
- [elims "?xs"] = ListE and
- [comps] = List_comp_nil List_comp_cons
+ [form] = ListF and
+ [intro, intros] = List_nil List_cons and
+ [elim "?xs"] = ListE and
+ [comp] = List_comp_nil List_comp_cons
abbreviation "ListRec A C \<equiv> ListInd A (fn _. C)"
@@ -110,7 +111,7 @@ Lemma head_type [typechk]:
shows "head xs: Maybe A"
unfolding head_def by typechk
-Lemma head_of_cons [comps]:
+Lemma head_of_cons [comp]:
assumes "A: U i" "x: A" "xs: List A"
shows "head (x # xs) \<equiv> some x"
unfolding head_def by reduce
@@ -120,7 +121,7 @@ Lemma tail_type [typechk]:
shows "tail xs: List A"
unfolding tail_def by typechk
-Lemma tail_of_cons [comps]:
+Lemma tail_of_cons [comp]:
assumes "A: U i" "x: A" "xs: List A"
shows "tail (x # xs) \<equiv> xs"
unfolding tail_def by reduce
@@ -181,7 +182,7 @@ Lemma rev_type [typechk]:
shows "rev xs: List A"
unfolding rev_def by typechk
-Lemma rev_nil [comps]:
+Lemma rev_nil [comp]:
assumes "A: U i"
shows "rev (nil A) \<equiv> nil A"
unfolding rev_def by reduce
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index d821920..0ce534c 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -54,9 +54,10 @@ Lemma Maybe_comp_some:
unfolding MaybeInd_def some_def by (reduce add: Maybe_def)
lemmas
- [intros] = MaybeF Maybe_none Maybe_some and
- [comps] = Maybe_comp_none Maybe_comp_some and
- MaybeE [elims "?m"] = MaybeInd[rotated 4]
+ [form] = MaybeF and
+ [intro, intros] = Maybe_none Maybe_some and
+ [comp] = Maybe_comp_none Maybe_comp_some and
+ MaybeE [elim "?m"] = MaybeInd[rotated 4]
lemmas
Maybe_cases [cases] = MaybeE
diff --git a/spartan/lib/More_Types.thy b/spartan/lib/More_Types.thy
index 0d7096f..55e6554 100644
--- a/spartan/lib/More_Types.thy
+++ b/spartan/lib/More_Types.thy
@@ -16,9 +16,9 @@ notation Sum (infixl "\<or>" 50)
axiomatization where
SumF: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A \<or> B: U i" and
- Sum_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl A B a: A \<or> B" and
+ Sum_inl: "\<lbrakk>B: U i; a: A\<rbrakk> \<Longrightarrow> inl A B a: A \<or> B" and
- Sum_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr A B b: A \<or> B" and
+ Sum_inr: "\<lbrakk>A: U i; b: B\<rbrakk> \<Longrightarrow> inr A B b: A \<or> B" and
SumE: "\<lbrakk>
s: A \<or> B;
@@ -42,9 +42,11 @@ axiomatization where
\<rbrakk> \<Longrightarrow> SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) (inr A B b) \<equiv> d b"
lemmas
- [intros] = SumF Sum_inl Sum_inr and
- [elims ?s] = SumE and
- [comps] = Sum_comp_inl Sum_comp_inr
+ [form] = SumF and
+ [intro] = Sum_inl Sum_inr and
+ [intros] = Sum_inl[rotated] Sum_inr[rotated] and
+ [elim ?s] = SumE and
+ [comp] = Sum_comp_inl Sum_comp_inr
method left = rule Sum_inl
method right = rule Sum_inr
@@ -76,10 +78,11 @@ and
BotE: "\<lbrakk>x: \<bottom>; \<And>x. x: \<bottom> \<Longrightarrow> C x: U i\<rbrakk> \<Longrightarrow> BotInd (fn x. C x) x: C x"
lemmas
- [intros] = TopF TopI BotF and
- [elims ?a] = TopE and
- [elims ?x] = BotE and
- [comps] = Top_comp
+ [form] = TopF BotF and
+ [intro, intros] = TopI and
+ [elim ?a] = TopE and
+ [elim ?x] = BotE and
+ [comp] = Top_comp
section \<open>Booleans\<close>
@@ -125,9 +128,10 @@ Lemma if_false:
by reduce
lemmas
- [intros] = BoolF Bool_true Bool_false and
- [comps] = if_true if_false and
- [elims ?x] = ifelse
+ [form] = BoolF and
+ [intro, intros] = Bool_true Bool_false and
+ [comp] = if_true if_false and
+ [elim ?x] = ifelse
lemmas
BoolE = ifelse
@@ -136,7 +140,7 @@ 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"
+translations "if x then a else b" \<leftharpoondown> "CONST ifelse C x a b"
subsection \<open>Logical connectives\<close>