|
1 (* Title: Nominal2_Eqvt |
|
2 Author: Brian Huffman, |
|
3 Author: Christian Urban |
|
4 |
|
5 Test cases for perm_simp |
|
6 *) |
|
7 theory Eqvt |
|
8 imports Nominal2_Base |
|
9 begin |
|
10 |
|
11 |
|
12 declare [[trace_eqvt = false]] |
|
13 (* declare [[trace_eqvt = true]] *) |
|
14 |
|
15 lemma |
|
16 fixes B::"'a::pt" |
|
17 shows "p \<bullet> (B = C)" |
|
18 apply(perm_simp) |
|
19 oops |
|
20 |
|
21 lemma |
|
22 fixes B::"bool" |
|
23 shows "p \<bullet> (B = C)" |
|
24 apply(perm_simp) |
|
25 oops |
|
26 |
|
27 lemma |
|
28 fixes B::"bool" |
|
29 shows "p \<bullet> (A \<longrightarrow> B = C)" |
|
30 apply (perm_simp) |
|
31 oops |
|
32 |
|
33 lemma |
|
34 shows "p \<bullet> (\<lambda>(x::'a::pt). A \<longrightarrow> (B::'a \<Rightarrow> bool) x = C) = foo" |
|
35 apply(perm_simp) |
|
36 oops |
|
37 |
|
38 lemma |
|
39 shows "p \<bullet> (\<lambda>B::bool. A \<longrightarrow> (B = C)) = foo" |
|
40 apply (perm_simp) |
|
41 oops |
|
42 |
|
43 lemma |
|
44 shows "p \<bullet> (\<lambda>x y. \<exists>z. x = z \<and> x = y \<longrightarrow> z \<noteq> x) = foo" |
|
45 apply (perm_simp) |
|
46 oops |
|
47 |
|
48 lemma |
|
49 shows "p \<bullet> (\<lambda>f x. f (g (f x))) = foo" |
|
50 apply (perm_simp) |
|
51 oops |
|
52 |
|
53 lemma |
|
54 fixes p q::"perm" |
|
55 and x::"'a::pt" |
|
56 shows "p \<bullet> (q \<bullet> x) = foo" |
|
57 apply(perm_simp) |
|
58 oops |
|
59 |
|
60 lemma |
|
61 fixes p q r::"perm" |
|
62 and x::"'a::pt" |
|
63 shows "p \<bullet> (q \<bullet> r \<bullet> x) = foo" |
|
64 apply(perm_simp) |
|
65 oops |
|
66 |
|
67 lemma |
|
68 fixes p r::"perm" |
|
69 shows "p \<bullet> (\<lambda>q::perm. q \<bullet> (r \<bullet> x)) = foo" |
|
70 apply (perm_simp) |
|
71 oops |
|
72 |
|
73 lemma |
|
74 fixes C D::"bool" |
|
75 shows "B (p \<bullet> (C = D))" |
|
76 apply(perm_simp) |
|
77 oops |
|
78 |
|
79 declare [[trace_eqvt = false]] |
|
80 |
|
81 text {* there is no raw eqvt-rule for The *} |
|
82 lemma "p \<bullet> (THE x. P x) = foo" |
|
83 apply(perm_strict_simp exclude: The) |
|
84 apply(perm_simp exclude: The) |
|
85 oops |
|
86 |
|
87 lemma |
|
88 fixes P :: "(('b \<Rightarrow> bool) \<Rightarrow> ('b::pt)) \<Rightarrow> ('a::pt)" |
|
89 shows "p \<bullet> (P The) = foo" |
|
90 apply(perm_simp exclude: The) |
|
91 oops |
|
92 |
|
93 lemma |
|
94 fixes P :: "('a::pt) \<Rightarrow> ('b::pt) \<Rightarrow> bool" |
|
95 shows "p \<bullet> (\<lambda>(a, b). P a b) = (\<lambda>(a, b). (p \<bullet> P) a b)" |
|
96 apply(perm_simp) |
|
97 oops |
|
98 |
|
99 thm eqvts |
|
100 thm eqvts_raw |
|
101 |
|
102 ML {* Nominal_ThmDecls.is_eqvt @{context} @{term "supp"} *} |
|
103 |
|
104 |
|
105 end |