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 |
21 thm at_set_avoiding2 |
23 thm at_set_avoiding2 |
22 thm trm_assn.fv_defs |
24 thm trm_assn.fv_defs |
23 thm trm_assn.eq_iff |
25 thm trm_assn.eq_iff |
24 thm trm_assn.bn_defs |
26 thm trm_assn.bn_defs |
25 thm trm_assn.perm_simps |
27 thm trm_assn.perm_simps |
27 thm trm_assn.inducts |
29 thm trm_assn.inducts |
28 thm trm_assn.distinct |
30 thm trm_assn.distinct |
29 thm trm_assn.supp |
31 thm trm_assn.supp |
30 thm trm_assn.fresh |
32 thm trm_assn.fresh |
31 thm trm_assn.exhaust[where y="t", no_vars] |
33 thm trm_assn.exhaust[where y="t", no_vars] |
32 |
|
33 primrec |
|
34 permute_bn_raw |
|
35 where |
|
36 "permute_bn_raw p (ANil_raw) = ANil_raw" |
|
37 | "permute_bn_raw p (ACons_raw a t l) = ACons_raw (p \<bullet> a) t (permute_bn_raw p l)" |
|
38 |
34 |
39 quotient_definition |
35 quotient_definition |
40 "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn" |
36 "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn" |
41 is |
37 is |
42 "permute_bn_raw" |
38 "permute_bn_raw" |