|
1 header {* Utilities for defining constants and functions *} |
|
2 theory Utils imports Lambda begin |
|
3 |
|
4 lemma beta_app: |
|
5 "(\<integral> x. M) \<cdot> V x \<approx> M" |
|
6 by (rule b3, rule bI) |
|
7 (simp add: b1) |
|
8 |
|
9 lemma lam1_fast_app: |
|
10 assumes leq: "\<And>a. (L = \<integral> a. (F (V a)))" |
|
11 and su: "\<And>x. atom x \<sharp> A \<Longrightarrow> F (V x) [x ::= A] = F A" |
|
12 shows "L \<cdot> A \<approx> F A" |
|
13 proof - |
|
14 obtain x :: var where a: "atom x \<sharp> A" using obtain_fresh by blast |
|
15 show ?thesis |
|
16 by (simp add: leq[of x], rule b3, rule bI, simp add: su b1 a) |
|
17 qed |
|
18 |
|
19 lemma lam2_fast_app: |
|
20 assumes leq: "\<And>a b. a \<noteq> b \<Longrightarrow> L = \<integral> a. \<integral> b. (F (V a) (V b))" |
|
21 and su: "\<And>x y. atom x \<sharp> A \<Longrightarrow> atom y \<sharp> A \<Longrightarrow> atom x \<sharp> B \<Longrightarrow> atom y \<sharp> B \<Longrightarrow> |
|
22 x \<noteq> y \<Longrightarrow> F (V x) (V y) [x ::= A] [y ::= B] = F A B" |
|
23 shows "L \<cdot> A \<cdot> B \<approx> F A B" |
|
24 proof - |
|
25 obtain x :: var where a: "atom x \<sharp> (A, B)" using obtain_fresh by blast |
|
26 obtain y :: var where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast |
|
27 obtain z :: var where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast |
|
28 have *: "x \<noteq> y" "x \<noteq> z" "y \<noteq> z" |
|
29 using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+ |
|
30 have ** : "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x" |
|
31 "atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y" |
|
32 "atom x \<sharp> A" "atom y \<sharp> A" "atom z \<sharp> A" |
|
33 "atom x \<sharp> B" "atom y \<sharp> B" "atom z \<sharp> B" |
|
34 using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+ |
|
35 show ?thesis |
|
36 apply (simp add: leq[OF *(1)]) |
|
37 apply (rule b3) apply (rule b5) apply (rule bI) |
|
38 apply (simp add: ** fresh_Pair) |
|
39 apply (rule b3) apply (rule bI) apply (simp add: su b1 ** *) |
|
40 done |
|
41 qed |
|
42 |
|
43 lemma lam3_fast_app: |
|
44 assumes leq: "\<And>a b c. a \<noteq> b \<Longrightarrow> b \<noteq> c \<Longrightarrow> c \<noteq> a \<Longrightarrow> |
|
45 L = \<integral> a. \<integral> b. \<integral> c. (F (V a) (V b) (V c))" |
|
46 and su: "\<And>x y z. atom x \<sharp> A \<Longrightarrow> atom y \<sharp> A \<Longrightarrow> atom z \<sharp> A \<Longrightarrow> |
|
47 atom x \<sharp> B \<Longrightarrow> atom y \<sharp> B \<Longrightarrow> atom z \<sharp> B \<Longrightarrow> |
|
48 atom y \<sharp> B \<Longrightarrow> atom y \<sharp> B \<Longrightarrow> atom z \<sharp> B \<Longrightarrow> |
|
49 x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> z \<noteq> x \<Longrightarrow> |
|
50 ((F (V x) (V y) (V z))[x ::= A] [y ::= B] [z ::= C] = F A B C)" |
|
51 shows "L \<cdot> A \<cdot> B \<cdot> C \<approx> F A B C" |
|
52 proof - |
|
53 obtain x :: var where a: "atom x \<sharp> (A, B, C)" using obtain_fresh by blast |
|
54 obtain y :: var where b: "atom y \<sharp> (x, A, B, C)" using obtain_fresh by blast |
|
55 obtain z :: var where c: "atom z \<sharp> (x, y, A, B, C)" using obtain_fresh by blast |
|
56 have *: "x \<noteq> y" "y \<noteq> z" "z \<noteq> x" |
|
57 using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+ |
|
58 have ** : "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x" |
|
59 "atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y" |
|
60 "atom x \<sharp> A" "atom y \<sharp> A" "atom z \<sharp> A" |
|
61 "atom x \<sharp> B" "atom y \<sharp> B" "atom z \<sharp> B" |
|
62 "atom x \<sharp> C" "atom y \<sharp> C" "atom z \<sharp> C" |
|
63 using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+ |
|
64 show ?thesis |
|
65 apply (simp add: leq[OF *(1) *(2) *(3)]) |
|
66 apply (rule b3) apply (rule b5) apply (rule b5) apply (rule bI) |
|
67 apply (simp add: ** fresh_Pair) |
|
68 apply (rule b3) apply (rule b5) apply (rule bI) |
|
69 apply (simp add: ** fresh_Pair) |
|
70 apply (rule b3) apply (rule bI) apply (simp add: su b1 ** *) |
|
71 done |
|
72 qed |
|
73 |
|
74 definition cn :: "nat \<Rightarrow> var" where "cn n \<equiv> Abs_var (Atom (Sort ''Lambda.var'' []) n)" |
|
75 |
|
76 lemma cnd[simp]: "m \<noteq> n \<Longrightarrow> cn m \<noteq> cn n" |
|
77 unfolding cn_def using Abs_var_inject by simp |
|
78 |
|
79 definition cx :: var where "cx \<equiv> cn 0" |
|
80 definition cy :: var where "cy \<equiv> cn 1" |
|
81 definition cz :: var where "cz \<equiv> cn 2" |
|
82 |
|
83 lemma cx_cy_cz[simp]: |
|
84 "cx \<noteq> cy" "cx \<noteq> cz" "cz \<noteq> cy" |
|
85 unfolding cx_def cy_def cz_def |
|
86 by simp_all |
|
87 |
|
88 lemma noteq_fresh: "atom x \<sharp> y = (x \<noteq> y)" |
|
89 by (simp add: fresh_at_base(2)) |
|
90 |
|
91 lemma fresh_fun_eqvt_app2: |
|
92 assumes a: "eqvt f" |
|
93 and b: "a \<sharp> x" "a \<sharp> y" |
|
94 shows "a \<sharp> f x y" |
|
95 using fresh_fun_eqvt_app[OF a b(1)] a b |
|
96 by (metis fresh_fun_app) |
|
97 |
|
98 end |
|
99 |
|
100 |
|
101 |