27 abbreviation "BP \<equiv> BP_raw" |
27 abbreviation "BP \<equiv> BP_raw" |
28 abbreviation "bi \<equiv> bi_raw" |
28 abbreviation "bi \<equiv> bi_raw" |
29 |
29 |
30 (* non-recursive case *) |
30 (* non-recursive case *) |
31 |
31 |
|
32 fun |
|
33 fv_lam |
|
34 and fv_bi |
|
35 and fv_bp |
|
36 where |
|
37 "fv_lam (VAR name) = {atom name}" |
|
38 | "fv_lam (APP lam1 lam2) = fv_lam lam1 \<union> fv_lam lam2" |
|
39 | "fv_lam (LET bp lam) = (fv_bi bp) \<union> (fv_lam lam - bi bp)" |
|
40 | "fv_bi (BP name lam) = fv_lam lam" |
|
41 | "fv_bp (BP name lam) = {atom name} \<union> fv_lam lam" |
|
42 |
32 inductive |
43 inductive |
33 alpha_lam :: "lam_raw \<Rightarrow> lam_raw \<Rightarrow> bool" and |
44 alpha_lam :: "lam_raw \<Rightarrow> lam_raw \<Rightarrow> bool" and |
34 alpha_bp :: "bp_raw \<Rightarrow> bp_raw \<Rightarrow> bool" and |
45 alpha_bp :: "bp_raw \<Rightarrow> bp_raw \<Rightarrow> bool" and |
35 compat_bp :: "bp_raw \<Rightarrow> perm \<Rightarrow> bp_raw \<Rightarrow> bool" |
46 alpha_bi :: "bp_raw \<Rightarrow> perm \<Rightarrow> bp_raw \<Rightarrow> bool" |
36 where |
47 where |
37 "x = y \<Longrightarrow> alpha_lam (VAR x) (VAR y)" |
48 "x = y \<Longrightarrow> alpha_lam (VAR x) (VAR y)" |
38 | "alpha_lam l1 s1 \<and> alpha_lam l2 s2 \<Longrightarrow> alpha_lam (APP l1 l2) (APP s1 s2)" |
49 | "alpha_lam l1 s1 \<and> alpha_lam l2 s2 \<Longrightarrow> alpha_lam (APP l1 l2) (APP s1 s2)" |
39 | "\<exists>pi. (bi bp, lam) \<approx>gen alpha_lam fv_lam_raw pi (bi bp', lam') \<and> (pi \<bullet> (bi bp)) = bi bp' |
50 | "\<exists>pi. (bi bp, lam) \<approx>gen alpha_lam fv_lam_raw pi (bi bp', lam') \<and> (pi \<bullet> (bi bp)) = bi bp' |
40 \<and> compat_bp bp pi bp' |
51 \<and> alpha_bi bp pi bp' |
41 \<Longrightarrow> alpha_lam (LET bp lam) (LET bp' lam')" |
52 \<Longrightarrow> alpha_lam (LET bp lam) (LET bp' lam')" |
42 | "alpha_lam lam lam' \<and> name = name' \<Longrightarrow> alpha_bp (BP name lam) (BP name' lam')" |
53 | "alpha_lam lam lam' \<and> name = name' \<Longrightarrow> alpha_bp (BP name lam) (BP name' lam')" |
43 | "alpha_lam t t' \<Longrightarrow> compat_bp (BP x t) pi (BP x' t')" |
54 | "alpha_lam t t' \<Longrightarrow> alpha_bi (BP x t) pi (BP x' t')" |
44 |
55 |
45 lemma test1: |
56 lemma test1: |
46 assumes "distinct [x, y]" |
57 assumes "distinct [x, y]" |
47 shows "alpha_lam (LET (BP x (VAR x)) (VAR x)) |
58 shows "alpha_lam (LET (BP x (VAR x)) (VAR x)) |
48 (LET (BP y (VAR x)) (VAR y))" |
59 (LET (BP y (VAR x)) (VAR y))" |
49 apply(rule alpha_lam_alpha_bp_compat_bp.intros) |
60 apply(rule alpha_lam_alpha_bp_alpha_bi.intros) |
50 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
61 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
51 apply(simp add: alpha_gen fresh_star_def) |
62 apply(simp add: alpha_gen fresh_star_def) |
52 apply(simp add: alpha_lam_alpha_bp_compat_bp.intros(1)) |
63 apply(simp add: alpha_lam_alpha_bp_alpha_bi.intros(1)) |
53 apply(rule conjI) |
64 apply(rule conjI) |
54 defer |
65 defer |
55 apply(rule alpha_lam_alpha_bp_compat_bp.intros) |
66 apply(rule alpha_lam_alpha_bp_alpha_bi.intros) |
56 apply(simp add: alpha_lam_alpha_bp_compat_bp.intros(1)) |
67 apply(simp add: alpha_lam_alpha_bp_alpha_bi.intros(1)) |
57 apply(simp add: permute_set_eq atom_eqvt) |
68 apply(simp add: permute_set_eq atom_eqvt) |
58 done |
69 done |
59 |
70 |
60 lemma test2: |
71 lemma test2: |
61 assumes asm: "distinct [x, y]" |
72 assumes asm: "distinct [x, y]" |
90 | "\<exists>pi. (bi bp, lam) \<approx>gen Alpha_lam fv_lam_raw pi (bi bp', lam') \<and> Compat_bp bp pi bp' |
101 | "\<exists>pi. (bi bp, lam) \<approx>gen Alpha_lam fv_lam_raw pi (bi bp', lam') \<and> Compat_bp bp pi bp' |
91 \<and> (pi \<bullet> (bi bp)) = bi bp' |
102 \<and> (pi \<bullet> (bi bp)) = bi bp' |
92 \<Longrightarrow> Alpha_lam (LET bp lam) (LET bp' lam')" |
103 \<Longrightarrow> Alpha_lam (LET bp lam) (LET bp' lam')" |
93 | "Alpha_lam lam lam' \<and> name = name' \<Longrightarrow> Alpha_bp (BP name lam) (BP name' lam')" |
104 | "Alpha_lam lam lam' \<and> name = name' \<Longrightarrow> Alpha_bp (BP name lam) (BP name' lam')" |
94 | "Alpha_lam (pi \<bullet> t) t' \<Longrightarrow> Compat_bp (BP x t) pi (BP x' t')" |
105 | "Alpha_lam (pi \<bullet> t) t' \<Longrightarrow> Compat_bp (BP x t) pi (BP x' t')" |
|
106 |
|
107 |
95 |
108 |
96 lemma Test1: |
109 lemma Test1: |
97 assumes "distinct [x, y]" |
110 assumes "distinct [x, y]" |
98 shows "Alpha_lam (LET (BP x (VAR x)) (VAR x)) |
111 shows "Alpha_lam (LET (BP x (VAR x)) (VAR x)) |
99 (LET (BP y (VAR y)) (VAR y))" |
112 (LET (BP y (VAR y)) (VAR y))" |