# Theory Eqvt

```(*  Title:      Nominal2_Eqvt
Author:     Brian Huffman,
Author:     Christian Urban

Test cases for perm_simp
*)
theory Eqvt
imports Nominal2_Base
begin

declare [[trace_eqvt = false]]
(* declare [[trace_eqvt = true]] *)

lemma
fixes B::"'a::pt"
shows "p ∙ (B = C)"
apply(perm_simp)
oops

lemma
fixes B::"bool"
shows "p ∙ (B = C)"
apply(perm_simp)
oops

lemma
fixes B::"bool"
shows "p ∙ (A ⟶ B = C)"
apply (perm_simp)
oops

lemma
shows "p ∙ (λ(x::'a::pt). A ⟶ (B::'a ⇒ bool) x = C) = foo"
apply(perm_simp)
oops

lemma
shows "p ∙ (λB::bool. A ⟶ (B = C)) = foo"
apply (perm_simp)
oops

lemma
shows "p ∙ (λx y. ∃z. x = z ∧ x = y ⟶ z ≠ x) = foo"
apply (perm_simp)
oops

lemma
shows "p ∙ (λf x. f (g (f x))) = foo"
apply (perm_simp)
oops

lemma
fixes p q::"perm"
and   x::"'a::pt"
shows "p ∙ (q ∙ x) = foo"
apply(perm_simp)
oops

lemma
fixes p q r::"perm"
and   x::"'a::pt"
shows "p ∙ (q ∙ r ∙ x) = foo"
apply(perm_simp)
oops

lemma
fixes p r::"perm"
shows "p ∙ (λq::perm. q ∙ (r ∙ x)) = foo"
apply (perm_simp)
oops

lemma
fixes C D::"bool"
shows "B (p ∙ (C = D))"
apply(perm_simp)
oops

declare [[trace_eqvt = false]]

text ‹there is no raw eqvt-rule for The›
lemma "p ∙ (THE x. P x) = foo"
apply(perm_strict_simp exclude: The)
apply(perm_simp exclude: The)
oops

lemma
fixes P :: "(('b ⇒ bool) ⇒ ('b::pt)) ⇒ ('a::pt)"
shows "p ∙ (P The) = foo"
apply(perm_simp exclude: The)
oops

lemma
fixes  P :: "('a::pt) ⇒ ('b::pt) ⇒ bool"
shows "p ∙ (λ(a, b). P a b) = (λ(a, b). (p ∙ P) a b)"
apply(perm_simp)
oops

thm eqvts
thm eqvts_raw

ML ‹Nominal_ThmDecls.is_eqvt @{context} @{term "supp"}›

end
```