15 lemma eqvtI: |
15 lemma eqvtI: |
16 "(\<And>p. p \<bullet> x \<equiv> x) \<Longrightarrow> eqvt x" |
16 "(\<And>p. p \<bullet> x \<equiv> x) \<Longrightarrow> eqvt x" |
17 apply(auto simp add: eqvt_def) |
17 apply(auto simp add: eqvt_def) |
18 done |
18 done |
19 |
19 |
|
20 term THE_default |
20 |
21 |
21 lemma the_default_eqvt: |
22 lemma the_default_eqvt: |
22 assumes unique: "\<exists>!x. P x" |
23 assumes unique: "\<exists>!x. P x" |
23 shows "(p \<bullet> (THE_default d P)) = (THE_default (p \<bullet> d) (p \<bullet> P))" |
24 shows "(p \<bullet> (THE_default d P)) = (THE_default d (p \<bullet> P))" |
24 apply(rule THE_default1_equality [symmetric]) |
25 apply(rule THE_default1_equality [symmetric]) |
25 apply(rule_tac p="-p" in permute_boolE) |
26 apply(rule_tac p="-p" in permute_boolE) |
26 apply(perm_simp add: permute_minus_cancel) |
27 apply(perm_simp add: permute_minus_cancel) |
27 apply(rule unique) |
28 apply(rule unique) |
28 apply(rule_tac p="-p" in permute_boolE) |
29 apply(rule_tac p="-p" in permute_boolE) |
29 apply(perm_simp add: permute_minus_cancel) |
30 apply(perm_simp add: permute_minus_cancel) |
30 apply(rule THE_defaultI'[OF unique]) |
31 apply(rule THE_defaultI'[OF unique]) |
31 done |
32 done |
|
33 |
|
34 lemma fundef_ex1_eqvt: |
|
35 fixes x::"'a::pt" |
|
36 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
|
37 assumes ex1: "\<exists>!y. G x y" |
|
38 assumes eqvt: "eqvt G" |
|
39 shows "(p \<bullet> (f x)) = f (p \<bullet> x)" |
|
40 apply (simp only: f_def) |
|
41 apply(subst the_default_eqvt) |
|
42 apply (rule ex1) |
|
43 apply(perm_simp) |
|
44 using eqvt |
|
45 apply(simp add: eqvt_def) |
|
46 done |
|
47 |
32 |
48 |
33 |
49 |
34 ML {* |
50 ML {* |
35 |
51 |
36 |
52 |