10 lemma lam1_fast_app: |
10 lemma lam1_fast_app: |
11 assumes leq: "\<And>a. (L = \<integral> a. (F (V a)))" |
11 assumes leq: "\<And>a. (L = \<integral> a. (F (V a)))" |
12 and su: "\<And>x. atom x \<sharp> A \<Longrightarrow> F (V x) [x ::= A] = F A" |
12 and su: "\<And>x. atom x \<sharp> A \<Longrightarrow> F (V x) [x ::= A] = F A" |
13 shows "L \<cdot> A \<approx> F A" |
13 shows "L \<cdot> A \<approx> F A" |
14 proof - |
14 proof - |
15 obtain x :: var where a: "atom x \<sharp> A" using obtain_fresh by blast |
15 obtain x :: name where a: "atom x \<sharp> A" using obtain_fresh by blast |
16 show ?thesis |
16 show ?thesis |
17 by (simp add: leq[of x], rule b3, rule bI, simp add: su b1 a) |
17 by (simp add: leq[of x], rule b3, rule bI, simp add: su b1 a) |
18 qed |
18 qed |
19 |
19 |
20 lemma lam2_fast_app: |
20 lemma lam2_fast_app: |
21 assumes leq: "\<And>a b. a \<noteq> b \<Longrightarrow> L = \<integral> a. \<integral> b. (F (V a) (V b))" |
21 assumes leq: "\<And>a b. a \<noteq> b \<Longrightarrow> L = \<integral> a. \<integral> b. (F (V a) (V b))" |
22 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 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> |
23 x \<noteq> y \<Longrightarrow> F (V x) (V y) [x ::= A] [y ::= B] = F A B" |
23 x \<noteq> y \<Longrightarrow> F (V x) (V y) [x ::= A] [y ::= B] = F A B" |
24 shows "L \<cdot> A \<cdot> B \<approx> F A B" |
24 shows "L \<cdot> A \<cdot> B \<approx> F A B" |
25 proof - |
25 proof - |
26 obtain x :: var where a: "atom x \<sharp> (A, B)" using obtain_fresh by blast |
26 obtain x :: name where a: "atom x \<sharp> (A, B)" using obtain_fresh by blast |
27 obtain y :: var where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast |
27 obtain y :: name where b: "atom y \<sharp> (x, A, B)" using obtain_fresh by blast |
28 obtain z :: var where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast |
28 obtain z :: name where c: "atom z \<sharp> (x, y, A, B)" using obtain_fresh by blast |
29 have *: "x \<noteq> y" "x \<noteq> z" "y \<noteq> z" |
29 have *: "x \<noteq> y" "x \<noteq> z" "y \<noteq> z" |
30 using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+ |
30 using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+ |
31 have ** : "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x" |
31 have ** : "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x" |
32 "atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y" |
32 "atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y" |
33 "atom x \<sharp> A" "atom y \<sharp> A" "atom z \<sharp> A" |
33 "atom x \<sharp> A" "atom y \<sharp> A" "atom z \<sharp> A" |
49 atom y \<sharp> B \<Longrightarrow> atom y \<sharp> B \<Longrightarrow> atom z \<sharp> B \<Longrightarrow> |
49 atom y \<sharp> B \<Longrightarrow> atom y \<sharp> B \<Longrightarrow> atom z \<sharp> B \<Longrightarrow> |
50 x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> z \<noteq> x \<Longrightarrow> |
50 x \<noteq> y \<Longrightarrow> y \<noteq> z \<Longrightarrow> z \<noteq> x \<Longrightarrow> |
51 ((F (V x) (V y) (V z))[x ::= A] [y ::= B] [z ::= C] = F A B C)" |
51 ((F (V x) (V y) (V z))[x ::= A] [y ::= B] [z ::= C] = F A B C)" |
52 shows "L \<cdot> A \<cdot> B \<cdot> C \<approx> F A B C" |
52 shows "L \<cdot> A \<cdot> B \<cdot> C \<approx> F A B C" |
53 proof - |
53 proof - |
54 obtain x :: var where a: "atom x \<sharp> (A, B, C)" using obtain_fresh by blast |
54 obtain x :: name where a: "atom x \<sharp> (A, B, C)" using obtain_fresh by blast |
55 obtain y :: var where b: "atom y \<sharp> (x, A, B, C)" using obtain_fresh by blast |
55 obtain y :: name where b: "atom y \<sharp> (x, A, B, C)" using obtain_fresh by blast |
56 obtain z :: var where c: "atom z \<sharp> (x, y, A, B, C)" using obtain_fresh by blast |
56 obtain z :: name where c: "atom z \<sharp> (x, y, A, B, C)" using obtain_fresh by blast |
57 have *: "x \<noteq> y" "y \<noteq> z" "z \<noteq> x" |
57 have *: "x \<noteq> y" "y \<noteq> z" "z \<noteq> x" |
58 using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+ |
58 using a b c by (simp_all add: fresh_Pair fresh_at_base) blast+ |
59 have ** : "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x" |
59 have ** : "atom y \<sharp> z" "atom x \<sharp> z" "atom y \<sharp> x" |
60 "atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y" |
60 "atom z \<sharp> y" "atom z \<sharp> x" "atom x \<sharp> y" |
61 "atom x \<sharp> A" "atom y \<sharp> A" "atom z \<sharp> A" |
61 "atom x \<sharp> A" "atom y \<sharp> A" "atom z \<sharp> A" |
70 apply (simp add: ** fresh_Pair) |
70 apply (simp add: ** fresh_Pair) |
71 apply (rule b3) apply (rule bI) apply (simp add: su b1 ** *) |
71 apply (rule b3) apply (rule bI) apply (simp add: su b1 ** *) |
72 done |
72 done |
73 qed |
73 qed |
74 |
74 |
75 definition cn :: "nat \<Rightarrow> var" where "cn n \<equiv> Abs_var (Atom (Sort ''LambdaTerms.var'' []) n)" |
75 definition cn :: "nat \<Rightarrow> name" where "cn n \<equiv> Abs_name (Atom (Sort ''LambdaTerms.name'' []) n)" |
76 |
76 |
77 lemma cnd[simp]: "m \<noteq> n \<Longrightarrow> cn m \<noteq> cn n" |
77 lemma cnd[simp]: "m \<noteq> n \<Longrightarrow> cn m \<noteq> cn n" |
78 unfolding cn_def using Abs_var_inject by simp |
78 unfolding cn_def using Abs_name_inject by simp |
79 |
79 |
80 definition cx :: var where "cx \<equiv> cn 0" |
80 definition cx :: name where "cx \<equiv> cn 0" |
81 definition cy :: var where "cy \<equiv> cn 1" |
81 definition cy :: name where "cy \<equiv> cn 1" |
82 definition cz :: var where "cz \<equiv> cn 2" |
82 definition cz :: name where "cz \<equiv> cn 2" |
83 |
83 |
84 lemma cx_cy_cz[simp]: |
84 lemma cx_cy_cz[simp]: |
85 "cx \<noteq> cy" "cx \<noteq> cz" "cz \<noteq> cy" |
85 "cx \<noteq> cy" "cx \<noteq> cz" "cz \<noteq> cy" |
86 unfolding cx_def cy_def cz_def |
86 unfolding cx_def cy_def cz_def |
87 by simp_all |
87 by simp_all |