From 12eed8685674b7d5ff7bc45a44a061e01f99ce5f Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Tue, 21 Jul 2020 02:09:44 +0200
Subject: 1. Type-checking/inference now more principled, and the
 implementation is better. 2. Changed most tactics to context tactics.

---
 spartan/lib/List.thy       | 13 +++++++------
 spartan/lib/Maybe.thy      |  7 ++++---
 spartan/lib/More_Types.thy | 30 +++++++++++++++++-------------
 3 files changed, 28 insertions(+), 22 deletions(-)

(limited to 'spartan/lib')

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>
 
-- 
cgit v1.2.3