aboutsummaryrefslogtreecommitdiff
path: root/spartan/lib/Prelude.thy
blob: 6adbce86c97d4e2227f198cda8008a4ab52aaf5b (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
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
  [intr] = Sum_inl Sum_inr and
  [intro] = 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
  [intr, intro] = 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
  [intr, intro] = 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