18 bi::"bp \<Rightarrow> atom set" |
18 bi::"bp \<Rightarrow> atom set" |
19 where |
19 where |
20 "bi (BP x t) = {atom x}" |
20 "bi (BP x t) = {atom x}" |
21 |
21 |
22 thm alpha_lam_raw_alpha_bp_raw.intros[no_vars] |
22 thm alpha_lam_raw_alpha_bp_raw.intros[no_vars] |
|
23 thm fv_lam_raw_fv_bp_raw.simps[no_vars] |
23 |
24 |
24 abbreviation "VAR \<equiv> VAR_raw" |
25 abbreviation "VAR \<equiv> VAR_raw" |
25 abbreviation "APP \<equiv> APP_raw" |
26 abbreviation "APP \<equiv> APP_raw" |
26 abbreviation "LET \<equiv> LET_raw" |
27 abbreviation "LET \<equiv> LET_raw" |
27 abbreviation "BP \<equiv> BP_raw" |
28 abbreviation "BP \<equiv> BP_raw" |
28 abbreviation "bi \<equiv> bi_raw" |
29 abbreviation "bi \<equiv> bi_raw" |
29 |
30 |
30 (* non-recursive case *) |
31 (* non-recursive case *) |
|
32 primrec |
|
33 fv_lam :: "lam_raw \<Rightarrow> atom set" |
|
34 and fv_compat :: "bp_raw \<Rightarrow> atom set" |
|
35 where |
|
36 "fv_lam (VAR name) = {atom name}" |
|
37 | "fv_lam (APP lam1 lam2) = fv_lam lam1 \<union> fv_lam lam2" |
|
38 | "fv_lam (LET bp lam) = (fv_compat bp) \<union> (fv_lam lam - bi bp)" |
|
39 | "fv_compat (BP name lam) = fv_lam lam" |
|
40 |
|
41 primrec |
|
42 fv_bp :: "bp_raw \<Rightarrow> atom set" |
|
43 where |
|
44 "fv_bp (BP name lam) = {atom name} \<union> fv_lam lam" |
|
45 |
31 |
46 |
32 inductive |
47 inductive |
33 alpha_lam :: "lam_raw \<Rightarrow> lam_raw \<Rightarrow> bool" and |
48 alpha_lam :: "lam_raw \<Rightarrow> lam_raw \<Rightarrow> bool" and |
34 alpha_bp :: "bp_raw \<Rightarrow> bp_raw \<Rightarrow> bool" and |
49 alpha_bp :: "bp_raw \<Rightarrow> bp_raw \<Rightarrow> bool" and |
35 compat_bp :: "bp_raw \<Rightarrow> perm \<Rightarrow> bp_raw \<Rightarrow> bool" |
50 compat_bp :: "bp_raw \<Rightarrow> perm \<Rightarrow> bp_raw \<Rightarrow> bool" |
40 \<Longrightarrow> alpha_lam (LET bp lam) (LET bp' lam')" |
55 \<Longrightarrow> alpha_lam (LET bp lam) (LET bp' lam')" |
41 | "alpha_lam lam lam' \<and> name = name' \<Longrightarrow> alpha_bp (BP name lam) (BP name' lam')" |
56 | "alpha_lam lam lam' \<and> name = name' \<Longrightarrow> alpha_bp (BP name lam) (BP name' lam')" |
42 | "alpha_lam t t' \<and> pi \<bullet> x = x' \<Longrightarrow> compat_bp (BP x t) pi (BP x' t')" |
57 | "alpha_lam t t' \<and> pi \<bullet> x = x' \<Longrightarrow> compat_bp (BP x t) pi (BP x' t')" |
43 |
58 |
44 lemma test1: |
59 lemma test1: |
45 assumes "distinct [x, y]" |
|
46 shows "alpha_lam (LET (BP x (VAR x)) (VAR x)) |
60 shows "alpha_lam (LET (BP x (VAR x)) (VAR x)) |
47 (LET (BP y (VAR x)) (VAR y))" |
61 (LET (BP y (VAR x)) (VAR y))" |
48 apply(rule alpha_lam_alpha_bp_compat_bp.intros) |
62 apply(rule alpha_lam_alpha_bp_compat_bp.intros) |
49 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
63 apply(rule_tac x="(x \<leftrightarrow> y)" in exI) |
50 apply(simp add: alpha_gen fresh_star_def) |
64 apply(simp add: alpha_gen fresh_star_def) |