equal
deleted
inserted
replaced
16 bn |
16 bn |
17 where |
17 where |
18 "bn ANil = []" |
18 "bn ANil = []" |
19 | "bn (ACons x t as) = (atom x) # (bn as)" |
19 | "bn (ACons x t as) = (atom x) # (bn as)" |
20 |
20 |
21 thm permute_bn_raw.simps |
|
22 |
|
23 thm at_set_avoiding2 |
21 thm at_set_avoiding2 |
24 thm trm_assn.fv_defs |
22 thm trm_assn.fv_defs |
25 thm trm_assn.eq_iff |
23 thm trm_assn.eq_iff |
26 thm trm_assn.bn_defs |
24 thm trm_assn.bn_defs |
27 thm trm_assn.perm_simps |
25 thm trm_assn.perm_simps |
29 thm trm_assn.inducts |
27 thm trm_assn.inducts |
30 thm trm_assn.distinct |
28 thm trm_assn.distinct |
31 thm trm_assn.supp |
29 thm trm_assn.supp |
32 thm trm_assn.fresh |
30 thm trm_assn.fresh |
33 thm trm_assn.exhaust[where y="t", no_vars] |
31 thm trm_assn.exhaust[where y="t", no_vars] |
34 |
|
35 quotient_definition |
|
36 "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn" |
|
37 is |
|
38 "permute_bn_raw" |
|
39 |
32 |
40 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
33 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
41 |
34 |
42 lemma uu: |
35 lemma uu: |
43 shows "alpha_bn as (permute_bn p as)" |
36 shows "alpha_bn as (permute_bn p as)" |