34 shows "finite (set (bn l))" |
34 shows "finite (set (bn l))" |
35 apply(induct l rule: trm_assn.inducts(2)) |
35 apply(induct l rule: trm_assn.inducts(2)) |
36 apply(simp_all) |
36 apply(simp_all) |
37 done |
37 done |
38 |
38 |
|
39 primrec |
|
40 permute_bn_raw |
|
41 where |
|
42 "permute_bn_raw p (ANil_raw) = ANil_raw" |
|
43 | "permute_bn_raw p (ACons_raw a t l) = ACons_raw (p \<bullet> a) t (permute_bn_raw p l)" |
|
44 |
|
45 quotient_definition |
|
46 "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn" |
|
47 is |
|
48 "permute_bn_raw" |
|
49 |
|
50 lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw" |
|
51 apply simp |
|
52 apply clarify |
|
53 apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts) |
|
54 apply (rule TrueI)+ |
|
55 apply simp_all |
|
56 apply (rule_tac [!] alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros) |
|
57 apply simp_all |
|
58 done |
|
59 |
|
60 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
|
61 |
|
62 lemma uu: |
|
63 shows "alpha_bn (permute_bn p as) as" |
|
64 apply(induct as rule: trm_assn.inducts(2)) |
|
65 apply(auto)[4] |
|
66 apply(simp add: permute_bn) |
|
67 apply(simp add: trm_assn.eq_iff) |
|
68 apply(simp add: permute_bn) |
|
69 apply(simp add: trm_assn.eq_iff) |
|
70 done |
|
71 |
|
72 lemma tt: |
|
73 shows "(p \<bullet> bn as) = bn (permute_bn p as)" |
|
74 apply(induct as rule: trm_assn.inducts(2)) |
|
75 apply(auto)[4] |
|
76 apply(simp add: permute_bn trm_assn.bn_defs) |
|
77 apply(simp add: permute_bn trm_assn.bn_defs) |
|
78 apply(simp add: atom_eqvt) |
|
79 done |
|
80 |
|
81 thm trm_assn.supp |
|
82 |
|
83 lemma "as \<sharp>* x \<longleftrightarrow> (\<forall>a\<in>as. a \<sharp> x)" |
|
84 apply(simp add: fresh_def) |
|
85 apply(simp add: fresh_star_def) |
|
86 oops |
39 |
87 |
40 inductive |
88 inductive |
41 test_trm :: "trm \<Rightarrow> bool" |
89 test_trm :: "trm \<Rightarrow> bool" |
42 and test_assn :: "assn \<Rightarrow> bool" |
90 and test_assn :: "assn \<Rightarrow> bool" |
43 where |
91 where |
49 | "\<lbrakk>test_trm t; test_assn as\<rbrakk> \<Longrightarrow> test_assn (ACons x t as)" |
97 | "\<lbrakk>test_trm t; test_assn as\<rbrakk> \<Longrightarrow> test_assn (ACons x t as)" |
50 |
98 |
51 declare trm_assn.fv_bn_eqvt[eqvt] |
99 declare trm_assn.fv_bn_eqvt[eqvt] |
52 equivariance test_trm |
100 equivariance test_trm |
53 |
101 |
54 (* |
|
55 lemma |
102 lemma |
56 fixes p::"perm" |
103 fixes p::"perm" |
57 shows "test_trm (p \<bullet> t)" and "test_assn (p \<bullet> as)" |
104 shows "test_trm (p \<bullet> t)" and "test_assn (p \<bullet> as)" |
58 apply(induct t and as arbitrary: p and p rule: trm_assn.inducts) |
105 apply(induct t and as arbitrary: p and p rule: trm_assn.inducts) |
59 apply(simp) |
106 apply(simp) |
72 apply(rule test_trm_test_assn.intros) |
119 apply(rule test_trm_test_assn.intros) |
73 apply(simp) |
120 apply(simp) |
74 apply(rule test_trm_test_assn.intros) |
121 apply(rule test_trm_test_assn.intros) |
75 apply(assumption) |
122 apply(assumption) |
76 apply(assumption) |
123 apply(assumption) |
77 apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst) |
124 apply(subgoal_tac "finite (set (bn (p \<bullet> assn)))") |
|
125 apply(subgoal_tac "set (bn (p \<bullet> assn)) \<sharp>* (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm))") |
|
126 apply(drule_tac c="()" in at_set_avoiding2) |
|
127 apply(simp add: supp_Unit) |
|
128 prefer 2 |
|
129 apply(assumption) |
|
130 apply(simp add: finite_supp) |
|
131 apply(erule exE) |
|
132 apply(erule conjE) |
|
133 apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" and |
|
134 s = "Let (permute_bn pa (p \<bullet> assn)) (pa \<bullet> (p \<bullet> trm))" in subst) |
78 apply(rule trm_assn.eq_iff(4)[THEN iffD2]) |
135 apply(rule trm_assn.eq_iff(4)[THEN iffD2]) |
|
136 apply(simp add: uu) |
|
137 apply(drule supp_perm_eq) |
|
138 apply(simp add: tt) |
|
139 apply(rule test_trm_test_assn.intros(4)) |
79 defer |
140 defer |
80 apply(rule test_trm_test_assn.intros) |
141 apply(subst permute_plus[symmetric]) |
81 prefer 3 |
142 apply(blast) |
82 apply(simp add: fresh_star_def trm_assn.fresh) |
143 oops |
83 thm freshs |
144 |
84 --"HERE" |
145 |
85 |
146 (* |
86 thm supps |
|
87 apply(rule test_trm_test_assn.intros) |
|
88 apply(assumption) |
|
89 |
|
90 apply(assumption) |
|
91 |
|
92 |
|
93 |
|
94 lemma |
147 lemma |
95 fixes t::trm |
148 fixes t::trm |
96 and as::assn |
149 and as::assn |
97 and c::"'a::fs" |
150 and c::"'a::fs" |
98 assumes a1: "\<And>x c. P1 c (Var x)" |
151 assumes a1: "\<And>x c. P1 c (Var x)" |