2893
+ − 1
header {* Constant definitions *}
2898
+ − 2
+ − 3
theory Consts imports Utils begin
2893
+ − 4
+ − 5
fun Umn :: "nat \<Rightarrow> nat \<Rightarrow> lam"
+ − 6
where
+ − 7
[simp del]: "Umn 0 n = \<integral>(cn 0). V (cn n)"
+ − 8
| [simp del]: "Umn (Suc m) n = \<integral>(cn (Suc m)). Umn m n"
+ − 9
+ − 10
lemma [simp]: "2 = Suc 1"
+ − 11
by auto
+ − 12
+ − 13
lemma Lam_U:
+ − 14
"x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> z \<Longrightarrow> Umn 2 0 = \<integral>x. \<integral>y. \<integral>z. V z"
+ − 15
"x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> z \<Longrightarrow> Umn 2 1 = \<integral>x. \<integral>y. \<integral>z. V y"
+ − 16
"x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> z \<Longrightarrow> Umn 2 2 = \<integral>x. \<integral>y. \<integral>z. V x"
+ − 17
apply (simp_all add: Umn.simps Abs1_eq_iff lam.fresh fresh_at_base flip_def[symmetric] Umn.simps)
+ − 18
apply (smt Zero_not_Suc cnd flip_at_base_simps flip_at_simps)+
+ − 19
done
+ − 20
+ − 21
lemma a: "n \<le> m \<Longrightarrow> atom (cn n) \<notin> supp (Umn m n)"
+ − 22
apply (induct m)
+ − 23
apply (auto simp add: lam.supp supp_at_base Umn.simps)
+ − 24
by smt
+ − 25
+ − 26
lemma b: "supp (Umn m n) \<subseteq> {atom (cn n)}"
+ − 27
by (induct m) (auto simp add: lam.supp supp_at_base Umn.simps)
+ − 28
+ − 29
lemma supp_U[simp]: "n \<le> m \<Longrightarrow> supp (Umn m n) = {}"
+ − 30
using a b
+ − 31
by blast
+ − 32
+ − 33
lemma U_eqvt:
+ − 34
"n \<le> m \<Longrightarrow> p \<bullet> (Umn m n) = Umn m n"
+ − 35
by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def)
+ − 36
+ − 37
definition Var where "Var \<equiv> \<integral>cx. \<integral>cy. (V cy \<cdot> (Umn 2 2) \<cdot> V cx \<cdot> V cy)"
+ − 38
definition "App \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. (V cz \<cdot> Umn 2 1 \<cdot> V cx \<cdot> V cy \<cdot> V cz)"
+ − 39
definition "Abs \<equiv> \<integral>cx. \<integral>cy. (V cy \<cdot> Umn 2 0 \<cdot> V cx \<cdot> V cy)"
+ − 40
+ − 41
lemma Var_App_Abs:
+ − 42
"x \<noteq> e \<Longrightarrow> Var = \<integral>x. \<integral>e. (V e \<cdot> Umn 2 2 \<cdot> V x \<cdot> V e)"
+ − 43
"e \<noteq> x \<Longrightarrow> e \<noteq> y \<Longrightarrow> x \<noteq> y \<Longrightarrow> App = \<integral>x. \<integral>y. \<integral>e. (V e \<cdot> Umn 2 1 \<cdot> V x \<cdot> V y \<cdot> V e)"
+ − 44
"x \<noteq> e \<Longrightarrow> Abs = \<integral>x. \<integral>e. (V e \<cdot> Umn 2 0 \<cdot> V x \<cdot> V e)"
+ − 45
unfolding Var_def App_def Abs_def
+ − 46
by (simp_all add: Abs1_eq_iff lam.fresh flip_def[symmetric] U_eqvt fresh_def lam.supp supp_at_base)
+ − 47
(smt cx_cy_cz permute_flip_at Zero_not_Suc cnd flip_at_base_simps flip_at_simps)+
+ − 48
+ − 49
lemma Var_app:
+ − 50
"Var \<cdot> x \<cdot> e \<approx> e \<cdot> Umn 2 2 \<cdot> x \<cdot> e"
+ − 51
by (rule lam2_fast_app) (simp_all add: Var_App_Abs)
+ − 52
+ − 53
lemma App_app:
+ − 54
"App \<cdot> x \<cdot> y \<cdot> e \<approx> e \<cdot> Umn 2 1 \<cdot> x \<cdot> y \<cdot> e"
+ − 55
by (rule lam3_fast_app[OF Var_App_Abs(2)]) (simp_all)
+ − 56
+ − 57
lemma Abs_app:
+ − 58
"Abs \<cdot> x \<cdot> e \<approx> e \<cdot> Umn 2 0 \<cdot> x \<cdot> e"
+ − 59
by (rule lam2_fast_app) (simp_all add: Var_App_Abs)
+ − 60
+ − 61
lemma supp_Var_App_Abs[simp]:
+ − 62
"supp Var = {}" "supp App = {}" "supp Abs = {}"
+ − 63
by (simp_all add: Var_def App_def Abs_def lam.supp supp_at_base) blast+
+ − 64
+ − 65
lemma Var_App_Abs_eqvt[eqvt]:
+ − 66
"p \<bullet> Var = Var" "p \<bullet> App = App" "p \<bullet> Abs = Abs"
+ − 67
by (rule_tac [!] perm_supp_eq) (simp_all add: fresh_star_def fresh_def)
+ − 68
+ − 69
nominal_primrec
+ − 70
Numeral :: "lam \<Rightarrow> lam" ("\<lbrace>_\<rbrace>" 1000)
+ − 71
where
+ − 72
"\<lbrace>V x\<rbrace> = Var \<cdot> (V x)"
+ − 73
| Ap: "\<lbrace>M \<cdot> N\<rbrace> = App \<cdot> \<lbrace>M\<rbrace> \<cdot> \<lbrace>N\<rbrace>"
+ − 74
| "\<lbrace>\<integral>x. M\<rbrace> = Abs \<cdot> (\<integral>x. \<lbrace>M\<rbrace>)"
+ − 75
proof auto
+ − 76
fix x :: lam and P
+ − 77
assume "\<And>xa. x = V xa \<Longrightarrow> P" "\<And>M N. x = M \<cdot> N \<Longrightarrow> P" "\<And>xa M. x = \<integral> xa. M \<Longrightarrow> P"
+ − 78
then show "P"
+ − 79
by (rule_tac y="x" and c="0 :: perm" in lam.strong_exhaust)
+ − 80
(auto simp add: Abs1_eq_iff fresh_star_def)[3]
+ − 81
next
+ − 82
fix x :: var and M and xa :: var and Ma
+ − 83
assume "[[atom x]]lst. M = [[atom xa]]lst. Ma"
+ − 84
"eqvt_at Numeral_sumC M"
+ − 85
then show "[[atom x]]lst. Numeral_sumC M = [[atom xa]]lst. Numeral_sumC Ma"
+ − 86
apply -
+ − 87
apply (erule Abs_lst1_fcb)
+ − 88
apply (simp_all add: Abs_fresh_iff)
+ − 89
apply (erule fresh_eqvt_at)
+ − 90
apply (simp_all add: finite_supp Abs1_eq_iff eqvt_at_def)
+ − 91
done
+ − 92
next
+ − 93
show "eqvt Numeral_graph" unfolding eqvt_def Numeral_graph_def
+ − 94
by (rule, perm_simp, rule)
+ − 95
qed
+ − 96
+ − 97
termination
+ − 98
by (relation "measure (\<lambda>(t). size t)")
+ − 99
(simp_all add: lam.size)
+ − 100
+ − 101
lemma numeral_eqvt[eqvt]: "p \<bullet> \<lbrace>x\<rbrace> = \<lbrace>p \<bullet> x\<rbrace>"
+ − 102
by (induct x rule: lam.induct)
+ − 103
(simp_all add: Var_App_Abs_eqvt)
+ − 104
+ − 105
lemma supp_numeral[simp]:
+ − 106
"supp \<lbrace>x\<rbrace> = supp x"
+ − 107
by (induct x rule: lam.induct)
+ − 108
(simp_all add: lam.supp)
+ − 109
+ − 110
lemma fresh_numeral[simp]:
+ − 111
"x \<sharp> \<lbrace>y\<rbrace> = x \<sharp> y"
+ − 112
unfolding fresh_def by simp
+ − 113
+ − 114
fun app_lst :: "var \<Rightarrow> lam list \<Rightarrow> lam" where
+ − 115
"app_lst n [] = V n"
+ − 116
| "app_lst n (h # t) = Ap (app_lst n t) h"
+ − 117
+ − 118
lemma app_lst_eqvt[eqvt]: "p \<bullet> (app_lst t ts) = app_lst (p \<bullet> t) (p \<bullet> ts)"
+ − 119
by (induct ts arbitrary: t p) (simp_all add: eqvts)
+ − 120
+ − 121
lemma supp_app_lst: "supp (app_lst x l) = {atom x} \<union> supp l"
+ − 122
apply (induct l)
+ − 123
apply (simp_all add: supp_Nil lam.supp supp_at_base supp_Cons)
+ − 124
by blast
+ − 125
+ − 126
lemma app_lst_eq_iff: "app_lst n M = app_lst n N \<Longrightarrow> M = N"
+ − 127
by (induct M N rule: list_induct2') simp_all
+ − 128
+ − 129
lemma app_lst_rev_eq_iff: "app_lst n (rev M) = app_lst n (rev N) \<Longrightarrow> M = N"
+ − 130
by (drule app_lst_eq_iff) simp
+ − 131
+ − 132
nominal_primrec
+ − 133
Ltgt :: "lam list \<Rightarrow> lam" ("\<guillemotleft>_\<guillemotright>" 1000)
+ − 134
where
+ − 135
[simp del]: "atom x \<sharp> l \<Longrightarrow> \<guillemotleft>l\<guillemotright> = \<integral>x. (app_lst x (rev l))"
+ − 136
unfolding eqvt_def Ltgt_graph_def
+ − 137
apply (rule, perm_simp, rule, rule)
+ − 138
apply (rule_tac x="x" and ?'a="var" in obtain_fresh)
+ − 139
apply (simp_all add: Abs1_eq_iff lam.fresh swap_fresh_fresh fresh_at_base)
+ − 140
apply (simp add: eqvts swap_fresh_fresh)
+ − 141
apply (case_tac "x = xa")
+ − 142
apply simp_all
+ − 143
apply (subgoal_tac "eqvt app_lst")
+ − 144
apply (erule fresh_fun_eqvt_app2)
+ − 145
apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev)
+ − 146
done
+ − 147
+ − 148
termination
+ − 149
by (relation "measure (\<lambda>t. size t)")
+ − 150
(simp_all add: lam.size)
+ − 151
+ − 152
lemma ltgt_eqvt[eqvt]:
+ − 153
"p \<bullet> \<guillemotleft>t\<guillemotright> = \<guillemotleft>p \<bullet> t\<guillemotright>"
+ − 154
proof -
+ − 155
obtain x :: var where "atom x \<sharp> (t, p \<bullet> t)" using obtain_fresh by auto
+ − 156
then have *: "atom x \<sharp> t" "atom x \<sharp> (p \<bullet> t)" using fresh_Pair by simp_all
+ − 157
then show ?thesis using *[unfolded fresh_def]
+ − 158
apply (simp add: Abs1_eq_iff lam.fresh app_lst_eqvt Ltgt.simps)
+ − 159
apply (case_tac "p \<bullet> x = x")
+ − 160
apply (simp_all add: eqvts)
+ − 161
apply rule
+ − 162
apply (subst swap_fresh_fresh)
+ − 163
apply (simp_all add: fresh_at_base_permute_iff fresh_def[symmetric] fresh_at_base)
+ − 164
apply (subgoal_tac "eqvt app_lst")
+ − 165
apply (erule fresh_fun_eqvt_app2)
+ − 166
apply (simp_all add: fresh_at_base lam.fresh eqvt_def eqvts_raw fresh_rev)
+ − 167
done
+ − 168
qed
+ − 169
+ − 170
lemma ltgt_eq_iff[simp]:
+ − 171
"\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright> \<longleftrightarrow> M = N"
+ − 172
proof auto
+ − 173
obtain x :: var where "atom x \<sharp> (M, N)" using obtain_fresh by auto
+ − 174
then have *: "atom x \<sharp> M" "atom x \<sharp> N" using fresh_Pair by simp_all
+ − 175
then show "(\<guillemotleft>M\<guillemotright> = \<guillemotleft>N\<guillemotright>) \<Longrightarrow> (M = N)" by (simp add: Abs1_eq_iff app_lst_rev_eq_iff Ltgt.simps)
+ − 176
qed
+ − 177
+ − 178
lemma Ltgt1_app: "\<guillemotleft>[M]\<guillemotright> \<cdot> N \<approx> N \<cdot> M"
+ − 179
proof -
+ − 180
obtain x :: var where "atom x \<sharp> (M, N)" using obtain_fresh by auto
+ − 181
then have "atom x \<sharp> M" "atom x \<sharp> N" using fresh_Pair by simp_all
+ − 182
then show ?thesis
+ − 183
apply (subst Ltgt.simps)
+ − 184
apply (simp add: fresh_Cons fresh_Nil)
+ − 185
apply (rule b3, rule bI, simp add: b1)
+ − 186
done
+ − 187
qed
+ − 188
+ − 189
lemma Ltgt3_app: "\<guillemotleft>[M,N,P]\<guillemotright> \<cdot> R \<approx> R \<cdot> M \<cdot> N \<cdot> P"
+ − 190
proof -
+ − 191
obtain x :: var where "atom x \<sharp> (M, N, P, R)" using obtain_fresh by auto
+ − 192
then have *: "atom x \<sharp> (M,N,P)" "atom x \<sharp> R" using fresh_Pair by simp_all
+ − 193
then have s: "V x \<cdot> M \<cdot> N \<cdot> P [x ::= R] \<approx> R \<cdot> M \<cdot> N \<cdot> P" using b1 by simp
+ − 194
show ?thesis using *
+ − 195
apply (subst Ltgt.simps)
+ − 196
apply (simp add: fresh_Cons fresh_Nil fresh_Pair_elim)
+ − 197
apply auto[1]
+ − 198
apply (rule b3, rule bI, simp add: b1)
+ − 199
done
+ − 200
qed
+ − 201
+ − 202
lemma supp_ltgt[simp]:
+ − 203
"supp \<guillemotleft>t\<guillemotright> = supp t"
+ − 204
proof -
+ − 205
obtain x :: var where *:"atom x \<sharp> t" using obtain_fresh by auto
+ − 206
show ?thesis using *
+ − 207
by (simp_all add: Ltgt.simps lam.supp supp_at_base supp_Nil supp_app_lst supp_rev fresh_def)
+ − 208
qed
+ − 209
+ − 210
lemma fresh_ltgt[simp]:
+ − 211
"x \<sharp> \<guillemotleft>[y]\<guillemotright> = x \<sharp> y"
+ − 212
"x \<sharp> \<guillemotleft>[t,r,s]\<guillemotright> = x \<sharp> (t,r,s)"
+ − 213
by (simp_all add: fresh_def supp_Cons supp_Nil supp_Pair)
+ − 214
+ − 215
lemma Ltgt1_subst[simp]:
+ − 216
"\<guillemotleft>[M]\<guillemotright> [y ::= A] = \<guillemotleft>[M [y ::= A]]\<guillemotright>"
+ − 217
proof -
+ − 218
obtain x :: var where a: "atom x \<sharp> (M, A, y, M [y ::= A])" using obtain_fresh by blast
+ − 219
have "x \<noteq> y" using a[simplified fresh_Pair fresh_at_base] by simp
+ − 220
then show ?thesis
+ − 221
apply (subst Ltgt.simps)
+ − 222
using a apply (simp add: fresh_Nil fresh_Cons fresh_Pair_elim)
+ − 223
apply (subst Ltgt.simps)
+ − 224
using a apply (simp add: fresh_Pair_elim fresh_Nil fresh_Cons)
+ − 225
apply (simp add: a)
+ − 226
done
+ − 227
qed
+ − 228
+ − 229
lemma U_app:
+ − 230
"\<guillemotleft>[A,B,C]\<guillemotright> \<cdot> Umn 2 2 \<approx> A" "\<guillemotleft>[A,B,C]\<guillemotright> \<cdot> Umn 2 1 \<approx> B" "\<guillemotleft>[A,B,C]\<guillemotright> \<cdot> Umn 2 0 \<approx> C"
+ − 231
by (rule b3, rule Ltgt3_app, rule lam3_fast_app, rule Lam_U, simp_all)
+ − 232
(rule b3, rule Ltgt3_app, rule lam3_fast_app, rule Lam_U[simplified], simp_all)+
+ − 233
+ − 234
definition "F1 \<equiv> \<integral>cx. (App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V cx))"
+ − 235
definition "F2 \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. ((App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (V cz \<cdot> V cx))) \<cdot> (V cz \<cdot> V cy))"
+ − 236
definition "F3 \<equiv> \<integral>cx. \<integral>cy. (App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>cz. (V cy \<cdot> (V cx \<cdot> V cz)))))"
+ − 237
+ − 238
+ − 239
lemma Lam_F:
+ − 240
"F1 = \<integral>x. (App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> V x))"
+ − 241
"a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> F2 = \<integral>a. \<integral>b. \<integral>c. ((App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (V c \<cdot> V a))) \<cdot> (V c \<cdot> V b))"
+ − 242
"a \<noteq> b \<Longrightarrow> a \<noteq> x \<Longrightarrow> x \<noteq> b \<Longrightarrow> F3 = \<integral>a. \<integral>b. (App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (V b \<cdot> (V a \<cdot> V x)))))"
+ − 243
apply (simp_all add: F1_def F2_def F3_def Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt numeral_eqvt flip_def[symmetric] fresh_at_base)
+ − 244
apply (smt cx_cy_cz permute_flip_at)+
+ − 245
done
+ − 246
+ − 247
lemma supp_F[simp]:
+ − 248
"supp F1 = {}" "supp F2 = {}" "supp F3 = {}"
+ − 249
by (simp_all add: F1_def F2_def F3_def lam.supp supp_at_base)
+ − 250
blast+
+ − 251
+ − 252
lemma F_eqvt[eqvt]:
+ − 253
"p \<bullet> F1 = F1" "p \<bullet> F2 = F2" "p \<bullet> F3 = F3"
+ − 254
by (rule_tac [!] perm_supp_eq)
+ − 255
(simp_all add: fresh_star_def fresh_def)
+ − 256
+ − 257
lemma F_app:
+ − 258
"F1 \<cdot> A \<approx> App \<cdot> \<lbrace>Var\<rbrace> \<cdot> (Var \<cdot> A)"
+ − 259
"F2 \<cdot> A \<cdot> B \<cdot> C \<approx> (App \<cdot> (App \<cdot> \<lbrace>App\<rbrace> \<cdot> (C \<cdot> A))) \<cdot> (C \<cdot> B)"
+ − 260
by (rule lam1_fast_app, rule Lam_F, simp_all)
+ − 261
(rule lam3_fast_app, rule Lam_F, simp_all)
+ − 262
+ − 263
lemma F3_app:
+ − 264
assumes f: "atom x \<sharp> A" "atom x \<sharp> B" (* or A and B have empty support *)
+ − 265
shows "F3 \<cdot> A \<cdot> B \<approx> App \<cdot> \<lbrace>Abs\<rbrace> \<cdot> (Abs \<cdot> (\<integral>x. (B \<cdot> (A \<cdot> V x))))"
+ − 266
proof -
+ − 267
obtain y :: var where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast
+ − 268
obtain z :: var where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast
+ − 269
have *: "x \<noteq> z" "x \<noteq> y" "y \<noteq> z"
+ − 270
using b c by (simp_all add: fresh_Pair fresh_at_base) blast+
+ − 271
have **:
+ − 272
"atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x"
+ − 273
"atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y"
+ − 274
"atom x \<sharp> A" "atom y \<sharp> A" "atom z \<sharp> A"
+ − 275
"atom x \<sharp> B" "atom y \<sharp> B" "atom z \<sharp> B"
+ − 276
using b c f by (simp_all add: fresh_Pair fresh_at_base) blast+
+ − 277
show ?thesis
+ − 278
apply (simp add: Lam_F(3)[of y z x] * *[symmetric])
+ − 279
apply (rule b3) apply (rule b5) apply (rule bI)
+ − 280
apply (simp add: ** fresh_Pair * *[symmetric])
+ − 281
apply (rule b3) apply (rule bI)
+ − 282
apply (simp add: ** fresh_Pair * *[symmetric])
+ − 283
apply (rule b1)
+ − 284
done
+ − 285
qed
+ − 286
+ − 287
definition Lam_A1_pre : "A1 \<equiv> \<integral>cx. \<integral>cy. (F1 \<cdot> V cx)"
+ − 288
definition Lam_A2_pre : "A2 \<equiv> \<integral>cx. \<integral>cy. \<integral>cz. (F2 \<cdot> V cx \<cdot> V cy \<cdot> \<guillemotleft>[V cz]\<guillemotright>)"
+ − 289
definition Lam_A3_pre : "A3 \<equiv> \<integral>cx. \<integral>cy. (F3 \<cdot> V cx \<cdot> \<guillemotleft>[V cy]\<guillemotright>)"
+ − 290
lemma Lam_A:
+ − 291
"x \<noteq> y \<Longrightarrow> A1 = \<integral>x. \<integral>y. (F1 \<cdot> V x)"
+ − 292
"a \<noteq> b \<Longrightarrow> a \<noteq> c \<Longrightarrow> c \<noteq> b \<Longrightarrow> A2 = \<integral>a. \<integral>b. \<integral>c. (F2 \<cdot> V a \<cdot> V b \<cdot> \<guillemotleft>[V c]\<guillemotright>)"
+ − 293
"a \<noteq> b \<Longrightarrow> A3 = \<integral>a. \<integral>b. (F3 \<cdot> V a \<cdot> \<guillemotleft>[V b]\<guillemotright>)"
+ − 294
apply (simp_all add: Lam_A1_pre Lam_A2_pre Lam_A3_pre Abs1_eq_iff lam.fresh supp_at_base Var_App_Abs_eqvt numeral_eqvt flip_def[symmetric] fresh_at_base F_eqvt ltgt_eqvt)
+ − 295
apply (smt cx_cy_cz permute_flip_at)+
+ − 296
done
+ − 297
+ − 298
lemma supp_A[simp]:
+ − 299
"supp A1 = {}" "supp A2 = {}" "supp A3 = {}"
+ − 300
by (auto simp add: Lam_A1_pre Lam_A2_pre Lam_A3_pre lam.supp supp_at_base supp_Cons supp_Nil)
+ − 301
+ − 302
lemma A_app:
+ − 303
"A1 \<cdot> A \<cdot> B \<approx> F1 \<cdot> A"
+ − 304
"A2 \<cdot> A \<cdot> B \<cdot> C \<approx> F2 \<cdot> A \<cdot> B \<cdot> \<guillemotleft>[C]\<guillemotright>"
+ − 305
"A3 \<cdot> A \<cdot> B \<approx> F3 \<cdot> A \<cdot> \<guillemotleft>[B]\<guillemotright>"
+ − 306
apply (rule lam2_fast_app, rule Lam_A, simp_all)
+ − 307
apply (rule lam3_fast_app, rule Lam_A, simp_all)
+ − 308
apply (rule lam2_fast_app, rule Lam_A, simp_all)
+ − 309
done
+ − 310
+ − 311
definition "Num \<equiv> \<guillemotleft>[\<guillemotleft>[A1,A2,A3]\<guillemotright>]\<guillemotright>"
+ − 312
+ − 313
lemma supp_Num[simp]:
+ − 314
"supp Num = {}"
+ − 315
by (auto simp only: Num_def supp_ltgt supp_Pair supp_A supp_Cons supp_Nil)
+ − 316
+ − 317
end