Theory Datatype_Simproc_Tests

(*  Title:      HOL/Datatype_Examples/Simproc_Tests.thy
    Author:     Manuel Eberl, TU München
*)

section ‹Tests of datatype-specific simprocs›

theory Datatype_Simproc_Tests
imports Main
begin

(* datatype without parameters *)

datatype foo = X | Y foo foo

lemma "x ≠ Y x y" "x ≠ Y y x" "Y x y ≠ x" "Y y x ≠ x"
  by simp_all


(* datatype with parameters *)

datatype 'a mytree = A 'a | B "'a mytree" "'a mytree"

lemma "B l r ≠ l" and "B l r ≠ r" and "l ≠ B l r" and "r ≠ B l r"
  by simp_all

notepad
begin
  fix a b c d e f :: "nat mytree"
  define t where [simp]: "t = B (B (B a b) (B c d)) (B e f)"
  have "∀x∈{a,b,c,d,e,f}. t ≠ x"
    by simp
  have "∀x∈{a,b,c,d,e,f}. x ≠ t"
    by simp
end


(* mutual recursion *)

datatype 'a myty1 = A1 'a | B1 "'a myty1" "'a myty2"
     and 'a myty2 = A2 'a | B2 "'a myty2" "'a myty1"

lemma "B1 a (B2 b c) ≠ a" and "B1 a (B2 b c) ≠ c"
  by simp_all

lemma "B2 a (B1 b c) ≠ a" and "B2 a (B1 b c) ≠ c"
  by simp_all

end