(*  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