From ff5454812f9e2720bd90c3a5437505644f63b487 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 31 Jul 2020 14:56:24 +0200
Subject: (FEAT) Term elaboration of assumption and goal statements.   .
 spartan/core/goals.ML   . spartan/core/elaboration.ML   .
 spartan/core/elaborated_statement.ML

(FEAT) More context tacticals and search tacticals.
  . spartan/core/context_tactical.ML

(FEAT) Improved subgoal focus.
  Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY).
  . spartan/core/focus.ML

(FIX) Normalize facts in order to be able to resolve properly.
  . spartan/core/typechecking.ML

(MAIN) New definitions.
(MAIN) Renamed theories and theorems.
(MAIN) Refactor theories to fit new features.
---
 spartan/lib/List.thy       |  10 +--
 spartan/lib/Maybe.thy      |  19 +++---
 spartan/lib/More_Types.thy | 150 ---------------------------------------------
 spartan/lib/Prelude.thy    | 150 +++++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 165 insertions(+), 164 deletions(-)
 delete mode 100644 spartan/lib/More_Types.thy
 create mode 100644 spartan/lib/Prelude.thy

(limited to 'spartan/lib')

diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy
index be86b63..34873e4 100644
--- a/spartan/lib/List.thy
+++ b/spartan/lib/List.thy
@@ -132,9 +132,9 @@ Definition app:
   assumes "A: U i" "xs: List A" "ys: List A"
   shows "List A"
   apply (elim xs)
-  \<guillemotright> by (fact \<open>ys:_\<close>)
-  \<guillemotright> prems vars x _ rec
-    proof - show "x # rec: List A" by typechk qed
+    \<^item> by (fact \<open>ys:_\<close>)
+    \<^item> vars x _ rec
+      proof - show "x # rec: List A" by typechk qed
   done
 
 definition app_i ("app") where [implicit]: "app xs ys \<equiv> List.app ? xs ys"
@@ -169,8 +169,8 @@ Definition rev:
   assumes "A: U i" "xs: List A"
   shows "List A"
   apply (elim xs)
-  \<guillemotright> by (rule List_nil)
-  \<guillemotright> prems vars x _ rec proof - show "app rec [x]: List A" by typechk qed
+    \<^item> by (rule List_nil)
+    \<^item> vars x _ rec proof - show "app rec [x]: List A" by typechk qed
   done
 
 definition rev_i ("rev") where [implicit]: "rev \<equiv> List.rev ?"
diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy
index 0ce534c..a2e1638 100644
--- a/spartan/lib/Maybe.thy
+++ b/spartan/lib/Maybe.thy
@@ -1,7 +1,7 @@
 chapter \<open>Maybe type\<close>
 
 theory Maybe
-imports More_Types
+imports Prelude
 
 begin
 
@@ -25,11 +25,10 @@ Definition MaybeInd:
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "m: Maybe A"
   shows "C m"
-  supply assms[unfolded Maybe_def none_def some_def]
+  using assms[unfolded Maybe_def none_def some_def]
   apply (elim m)
-  \<guillemotright> unfolding Maybe_def .
-  \<guillemotright> by (rule \<open>_ \<Longrightarrow> _: C (inl _ _ _)\<close>)
-  \<guillemotright> by elim (rule \<open>_: C (inr _ _ _)\<close>)
+    apply (rule \<open>_ \<Longrightarrow> _: C (inl _ _ _)\<close>)
+    apply (elim, rule \<open>_: C (inr _ _ _)\<close>)
   done
 
 Lemma Maybe_comp_none:
@@ -39,8 +38,9 @@ Lemma Maybe_comp_none:
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
   shows "MaybeInd A C c\<^sub>0 f (none A) \<equiv> c\<^sub>0"
-  supply assms[unfolded Maybe_def some_def none_def]
-  unfolding MaybeInd_def none_def by reduce
+  using assms
+  unfolding Maybe_def MaybeInd_def none_def some_def
+  by reduce
 
 Lemma Maybe_comp_some:
   assumes
@@ -50,8 +50,9 @@ Lemma Maybe_comp_some:
     "\<And>a. a: A \<Longrightarrow> f a: C (some A a)"
     "\<And>m. m: Maybe A \<Longrightarrow> C m: U i"
   shows "MaybeInd A C c\<^sub>0 f (some A a) \<equiv> f a"
-  supply assms[unfolded Maybe_def some_def none_def]
-  unfolding MaybeInd_def some_def by (reduce add: Maybe_def)
+  using assms
+  unfolding Maybe_def MaybeInd_def none_def some_def
+  by reduce
 
 lemmas
   [form] = MaybeF and
diff --git a/spartan/lib/More_Types.thy b/spartan/lib/More_Types.thy
deleted file mode 100644
index 55e6554..0000000
--- a/spartan/lib/More_Types.thy
+++ /dev/null
@@ -1,150 +0,0 @@
-theory More_Types
-imports Spartan
-
-begin
-
-section \<open>Sum type\<close>
-
-axiomatization
-  Sum    :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> and
-  inl    :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> and
-  inr    :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> and
-  SumInd :: \<open>o \<Rightarrow> o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o\<close>
-
-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>B: U i; a: A\<rbrakk> \<Longrightarrow> inl A B a: 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;
-    \<And>s. s: A \<or> B \<Longrightarrow> C s: U i;
-    \<And>a. a: A \<Longrightarrow> c a: C (inl A B a);
-    \<And>b. b: B \<Longrightarrow> d b: C (inr A B b)
-    \<rbrakk> \<Longrightarrow> SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) s: C s" and
-
-  Sum_comp_inl: "\<lbrakk>
-    a: A;
-    \<And>s. s: A \<or> B \<Longrightarrow> C s: U i;
-    \<And>a. a: A \<Longrightarrow> c a: C (inl A B a);
-    \<And>b. b: B \<Longrightarrow> d b: C (inr A B b)
-    \<rbrakk> \<Longrightarrow> SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) (inl A B a) \<equiv> c a" and
-
-  Sum_comp_inr: "\<lbrakk>
-    b: B;
-    \<And>s. s: A \<or> B \<Longrightarrow> C s: U i;
-    \<And>a. a: A \<Longrightarrow> c a: C (inl A B a);
-    \<And>b. b: B \<Longrightarrow> d b: C (inr A B b)
-    \<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
-  [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
-
-
-section \<open>Empty and unit types\<close>
-
-axiomatization
-  Top    :: \<open>o\<close> and
-  tt     :: \<open>o\<close> and
-  TopInd :: \<open>(o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close>
-and
-  Bot    :: \<open>o\<close> and
-  BotInd :: \<open>(o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o\<close>
-
-notation Top ("\<top>") and Bot ("\<bottom>")
-
-axiomatization where
-  TopF: "\<top>: U i" and
-
-  TopI: "tt: \<top>" and
-
-  TopE: "\<lbrakk>a: \<top>; \<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (fn x. C x) c a: C a" and
-
-  Top_comp: "\<lbrakk>\<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (fn x. C x) c tt \<equiv> c"
-and
-  BotF: "\<bottom>: U i" 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
-  [form] = TopF BotF and
-  [intro, intros] = TopI and
-  [elim ?a] = TopE and
-  [elim ?x] = BotE and
-  [comp] = Top_comp
-
-
-section \<open>Booleans\<close>
-
-definition "Bool \<equiv> \<top> \<or> \<top>"
-definition "true \<equiv> inl \<top> \<top> tt"
-definition "false \<equiv> inr \<top> \<top> tt"
-
-Lemma
-  BoolF: "Bool: U i" and
-  Bool_true: "true: Bool" and
-  Bool_false: "false: Bool"
-  unfolding Bool_def true_def false_def by typechk+
-
-\<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
-  [form] = BoolF and
-  [intro, intros] = Bool_true Bool_false and
-  [comp] = if_true if_false and
-  [elim ?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"
-
-translations "if x then a else b" \<leftharpoondown> "CONST ifelse C x a b"
-
-subsection \<open>Logical connectives\<close>
-
-definition not ("!_") where "not x \<equiv> ifelse (K Bool) x false true"
-
-
-end
diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy
new file mode 100644
index 0000000..36f12d2
--- /dev/null
+++ b/spartan/lib/Prelude.thy
@@ -0,0 +1,150 @@
+theory Prelude
+imports Spartan
+
+begin
+
+section \<open>Sum type\<close>
+
+axiomatization
+  Sum    :: \<open>o \<Rightarrow> o \<Rightarrow> o\<close> and
+  inl    :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> and
+  inr    :: \<open>o \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close> and
+  SumInd :: \<open>o \<Rightarrow> o \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> (o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o\<close>
+
+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>B: U i; a: A\<rbrakk> \<Longrightarrow> inl A B a: 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;
+    \<And>s. s: A \<or> B \<Longrightarrow> C s: U i;
+    \<And>a. a: A \<Longrightarrow> c a: C (inl A B a);
+    \<And>b. b: B \<Longrightarrow> d b: C (inr A B b)
+    \<rbrakk> \<Longrightarrow> SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) s: C s" and
+
+  Sum_comp_inl: "\<lbrakk>
+    a: A;
+    \<And>s. s: A \<or> B \<Longrightarrow> C s: U i;
+    \<And>a. a: A \<Longrightarrow> c a: C (inl A B a);
+    \<And>b. b: B \<Longrightarrow> d b: C (inr A B b)
+    \<rbrakk> \<Longrightarrow> SumInd A B (fn s. C s) (fn a. c a) (fn b. d b) (inl A B a) \<equiv> c a" and
+
+  Sum_comp_inr: "\<lbrakk>
+    b: B;
+    \<And>s. s: A \<or> B \<Longrightarrow> C s: U i;
+    \<And>a. a: A \<Longrightarrow> c a: C (inl A B a);
+    \<And>b. b: B \<Longrightarrow> d b: C (inr A B b)
+    \<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
+  [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
+
+
+section \<open>Empty and unit types\<close>
+
+axiomatization
+  Top    :: \<open>o\<close> and
+  tt     :: \<open>o\<close> and
+  TopInd :: \<open>(o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o \<Rightarrow> o\<close>
+and
+  Bot    :: \<open>o\<close> and
+  BotInd :: \<open>(o \<Rightarrow> o) \<Rightarrow> o \<Rightarrow> o\<close>
+
+notation Top ("\<top>") and Bot ("\<bottom>")
+
+axiomatization where
+  TopF: "\<top>: U i" and
+
+  TopI: "tt: \<top>" and
+
+  TopE: "\<lbrakk>a: \<top>; \<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (fn x. C x) c a: C a" and
+
+  Top_comp: "\<lbrakk>\<And>x. x: \<top> \<Longrightarrow> C x: U i; c: C tt\<rbrakk> \<Longrightarrow> TopInd (fn x. C x) c tt \<equiv> c"
+and
+  BotF: "\<bottom>: U i" 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
+  [form] = TopF BotF and
+  [intro, intros] = TopI and
+  [elim ?a] = TopE and
+  [elim ?x] = BotE and
+  [comp] = Top_comp
+
+
+section \<open>Booleans\<close>
+
+definition "Bool \<equiv> \<top> \<or> \<top>"
+definition "true \<equiv> inl \<top> \<top> tt"
+definition "false \<equiv> inr \<top> \<top> tt"
+
+Lemma
+  BoolF: "Bool: U i" and
+  Bool_true: "true: Bool" and
+  Bool_false: "false: Bool"
+  unfolding Bool_def true_def false_def by typechk+
+
+\<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
+  using assms unfolding 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
+  using assms unfolding Bool_def true_def false_def
+  by reduce
+
+lemmas
+  [form] = BoolF and
+  [intro, intros] = Bool_true Bool_false and
+  [comp] = if_true if_false and
+  [elim ?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"
+
+translations "if x then a else b" \<leftharpoondown> "CONST ifelse C x a b"
+
+subsection \<open>Logical connectives\<close>
+
+definition not ("!_") where "not x \<equiv> ifelse (K Bool) x false true"
+
+
+end
-- 
cgit v1.2.3