equal
deleted
inserted
replaced
1 theory SingleLet |
1 theory SingleLet |
2 imports "../Nominal2" "../Abs" |
2 imports "../Nominal2" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 declare [[STEPS = 100]] |
7 declare [[STEPS = 100]] |
22 "bn (As x y t) = [atom x]" |
22 "bn (As x y t) = [atom x]" |
23 |
23 |
24 |
24 |
25 thm single_let.distinct |
25 thm single_let.distinct |
26 thm single_let.induct |
26 thm single_let.induct |
|
27 thm single_let.inducts |
27 thm single_let.exhaust |
28 thm single_let.exhaust |
28 thm single_let.fv_defs |
29 thm single_let.fv_defs |
29 thm single_let.bn_defs |
30 thm single_let.bn_defs |
30 thm single_let.perm_simps |
31 thm single_let.perm_simps |
31 thm single_let.eq_iff |
32 thm single_let.eq_iff |
43 apply(rule assms) |
44 apply(rule assms) |
44 done |
45 done |
45 |
46 |
46 |
47 |
47 lemma supp_fv: |
48 lemma supp_fv: |
48 "fv_trm t = supp t \<and> fv_assg as = supp as \<and> fv_bn as = supp_rel alpha_bn as" |
49 "fv_trm t = supp t" "fv_assg as = supp as" "fv_bn as = supp_rel alpha_bn as" |
49 apply(rule single_let.induct) |
50 apply(induct t and as rule: single_let.inducts) |
50 -- " 0A " |
51 -- " 0A " |
51 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
52 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
52 apply(simp only: supp_abs(3)[symmetric])? |
53 apply(simp only: supp_abs(3)[symmetric])? |
53 apply(simp (no_asm) only: supp_def) |
54 apply(simp (no_asm) only: supp_def) |
54 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
55 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
68 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
69 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
69 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
70 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
70 apply(drule test2) |
71 apply(drule test2) |
71 apply(simp only:) |
72 apply(simp only:) |
72 -- " 2 " |
73 -- " 2 " |
73 apply(erule conjE)+ |
|
74 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
74 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
75 apply(simp only: supp_abs(3)[symmetric]) |
75 apply(simp only: supp_abs(3)[symmetric]) |
76 apply(simp (no_asm) only: supp_def supp_rel_def) |
76 apply(simp (no_asm) only: supp_def supp_rel_def) |
77 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
77 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
78 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
78 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
107 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
107 apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject) |
108 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
108 apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un) |
109 apply(drule test2)+ |
109 apply(drule test2)+ |
110 apply(simp only: supp_Pair Un_assoc conj_assoc) |
110 apply(simp only: supp_Pair Un_assoc conj_assoc) |
111 -- "last" |
111 -- "last" |
112 apply(rule conjI) |
|
113 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
112 apply(simp only: single_let.fv_defs supp_Pair[symmetric]) |
114 apply(simp only: supp_abs(3)[symmetric]) |
113 apply(simp only: supp_abs(3)[symmetric]) |
115 apply(simp (no_asm) only: supp_def supp_rel_def) |
114 apply(simp (no_asm) only: supp_def supp_rel_def) |
116 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
115 apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt) |
117 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |
116 apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff) |