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/More_Types.thy | 150 ---------------------------------------------
 1 file changed, 150 deletions(-)
 delete mode 100644 spartan/lib/More_Types.thy

(limited to 'spartan/lib/More_Types.thy')

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