39 |
39 |
40 |
40 |
41 |
41 |
42 lemma test: |
42 lemma test: |
43 "(\<exists>p. (bs, x) \<approx>lst (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))" |
43 "(\<exists>p. (bs, x) \<approx>lst (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))" |
44 oops |
44 sorry |
45 |
45 |
46 lemma Abs_eq_iff: |
46 lemma Abs_eq_iff: |
47 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
47 shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
48 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
48 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))" |
49 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
49 and "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))" |
50 by (lifting alphas_abs) |
50 by (lifting alphas_abs) |
51 |
51 |
52 (* |
|
53 lemma supp_fv: |
52 lemma supp_fv: |
54 "supp t = fv_trm t \<and> supp b = fv_bn b" |
53 "supp t = fv_trm t \<and> supp b = fv_bn b" |
55 apply(rule single_let.induct) |
54 apply(rule single_let.induct) |
56 apply(simp_all only: single_let.fv_defs)[2] |
55 apply(simp_all only: single_let.fv_defs)[2] |
57 apply(simp_all only: supp_def)[2] |
56 apply(simp_all only: supp_def)[2] |
63 apply(simp_all only: de_Morgan_conj)[2] |
62 apply(simp_all only: de_Morgan_conj)[2] |
64 apply(simp_all only: Collect_disj_eq)[2] |
63 apply(simp_all only: Collect_disj_eq)[2] |
65 apply(subgoal_tac "supp (Lam name trm) = supp (Abs_lst [atom name] trm)") |
64 apply(subgoal_tac "supp (Lam name trm) = supp (Abs_lst [atom name] trm)") |
66 apply(simp only: single_let.fv_defs) |
65 apply(simp only: single_let.fv_defs) |
67 apply(simp only: supp_abs) |
66 apply(simp only: supp_abs) |
|
67 apply(simp) |
68 apply(simp (no_asm) only: supp_def) |
68 apply(simp (no_asm) only: supp_def) |
69 apply(simp only: single_let.perm_simps) |
69 apply(simp only: single_let.perm_simps) |
70 apply(simp only: single_let.eq_iff) |
70 apply(simp only: single_let.eq_iff) |
|
71 apply(simp only: permute_abs atom_eqvt permute_list.simps) |
|
72 apply(simp only: Abs_eq_iff) |
71 apply(subst test) |
73 apply(subst test) |
72 apply(simp only: Abs_eq_iff[symmetric]) |
74 apply(rule refl) |
73 apply(simp only: alphas_abs[symmetric]) |
|
74 apply(simp only: eqvts) |
|
75 thm Abs_eq_iff |
|
76 apply(simp only: alphas) |
|
77 sorry |
75 sorry |
78 *) |
76 |
79 (* |
77 (* |
80 |
|
81 consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm" |
78 consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm" |
82 consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg" |
79 consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg" |
83 |
80 |
84 lemma y: |
81 lemma y: |
85 "perm_bn_trm p (Var x) = (Var x)" |
82 "perm_bn_trm p (Var x) = (Var x)" |