Theory Misc_N2M

(*  Title:      Benchmarks/Datatype_Benchmark/Misc_N2M.thy
    Author:     Dmitriy Traytel, TU Muenchen
    Copyright   2014

Miscellaneous tests for the nested-to-mutual reduction.
*)

section ‹Miscellaneous Tests for the Nested-to-Mutual Reduction›

theory Misc_N2M
imports "HOL-Library.BNF_Axiomatization"
begin

declare [[typedef_overloaded]]


locale misc
begin

datatype 'a li = Ni | Co 'a "'a li"
datatype 'a tr = Tr "'a ⇒ 'a tr li"

primrec (nonexhaustive)
  f_tl :: "'a ⇒ 'a tr li ⇒ nat" and
  f_t :: "'a ⇒ 'a tr ⇒ nat"
where
  "f_tl _ Ni = 0" |
  "f_t a (Tr ts) = 1 + f_tl a (ts a)"

datatype ('a, 'b) l = N | C 'a 'b "('a, 'b) l"
datatype ('a, 'b) t = T "(('a, 'b) t, 'a) l" "(('a, 'b) t, 'b) l"

primrec (nonexhaustive)
  f_tl2 :: "(('a, 'a) t, 'a) l ⇒ nat" and
  f_t2 :: "('a, 'a) t ⇒ nat"
where
  "f_tl2 N = 0" |
  "f_t2 (T ts us) = f_tl2 ts + f_tl2 us"

primrec  (nonexhaustive)
  g_tla :: "(('a, 'b) t, 'a) l ⇒ nat" and
  g_tlb :: "(('a, 'b) t, 'b) l ⇒ nat" and
  g_t :: "('a, 'b) t ⇒ nat"
where
  "g_tla N = 0" |
  "g_tlb N = 1" |
  "g_t (T ts us) = g_tla ts + g_tlb us"


datatype
  'a l1 = N1 | C1 'a "'a l1"

datatype
  ('a, 'b) t1 = T1 'a 'b "('a, 'b) t1 l1" "(nat × ('a, 'b) t1) l1" and
  ('a, 'b) t2 = T2 "('a, 'b) t1"

primrec
  h1_tl1 :: "(nat, 'a) t1 l1 ⇒ nat" and
  h1_natl1 :: "(nat × (nat, 'a) t1) l1 ⇒ nat" and
  h1_t1 :: "(nat, 'a) t1 ⇒ nat"
where
  "h1_tl1 N1 = 0" |
  "h1_tl1 (C1 t ts) = h1_t1 t + h1_tl1 ts" |
  "h1_natl1 N1 = Suc 0" |
  "h1_natl1 (C1 n ts) = fst n + h1_natl1 ts" |
  "h1_t1 (T1 n _ ts _) = n + h1_tl1 ts"

end


bnf_axiomatization ('a, 'b) M0 [wits: "('a, 'b) M0"]
bnf_axiomatization ('a, 'b) N0 [wits: "('a, 'b) N0"]
bnf_axiomatization ('a, 'b) K0 [wits: "('a, 'b) K0"]
bnf_axiomatization ('a, 'b) L0 [wits: "('a, 'b) L0"]
bnf_axiomatization ('a, 'b, 'c) G0 [wits: "('a, 'b, 'c) G0"]

locale (*co*)mplicated
begin

datatype 'a M = CM "('a, 'a M) M0"
datatype 'a N = CN "('a N, 'a) N0"
datatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0"
         and ('a, 'b) L = CL "('b, ('a, 'b) K) L0"
datatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0"

primrec
    fG :: "'a G ⇒ 'a G"
and fK :: "('a G, 'a G N) K ⇒ ('a G, 'a G N) K"
and fL :: "('a G, 'a G N) L ⇒ ('a G, 'a G N) L"
and fM :: "'a G M ⇒ 'a G M" where
  "fG (CG x) = CG (map_G0 id fK (map_L fM fG) x)"
| "fK (CK y) = CK (map_K0 fG fL y)"
| "fL (CL z) = CL (map_L0 (map_N fG) fK z)"
| "fM (CM w) = CM (map_M0 fG fM w)"
thm fG_def fK_def fL_def fM_def fG.simps fK.simps fL.simps fM.simps

end

locale complicated
begin

codatatype 'a M = CM "('a, 'a M) M0"
codatatype 'a N = CN "('a N, 'a) N0"
codatatype ('a, 'b) K = CK "('a, ('a, 'b) L) K0"
       and ('a, 'b) L = CL "('b, ('a, 'b) K) L0"
codatatype 'a G = CG "('a, ('a G, 'a G N) K, ('a G M, 'a G) L) G0"

primcorec
    fG :: "'a G ⇒ 'a G"
and fK :: "('a G, 'a G N) K ⇒ ('a G, 'a G N) K"
and fL :: "('a G, 'a G N) L ⇒ ('a G, 'a G N) L"
and fM :: "'a G M ⇒ 'a G M" where
  "fG x = CG (map_G0 id fK (map_L fM fG) (un_CG x))"
| "fK y = CK (map_K0 fG fL (un_CK y))"
| "fL z = CL (map_L0 (map_N fG) fK (un_CL z))"
| "fM w = CM (map_M0 fG fM (un_CM w))"
thm fG_def fK_def fL_def fM_def fG.simps fK.simps fL.simps fM.simps

end

datatype ('a, 'b) F1 = F1 'a 'b
datatype F2 = F2 "((unit, nat) F1, F2) F1" | F2'
datatype 'a kk1 = K1 'a | K2 "'a kk2" and 'a kk2 = K3 "'a kk1"
datatype 'a ll1 = L1 'a | L2 "'a ll2 kk2" and 'a ll2 = L3 "'a ll1"

datatype_compat F1
datatype_compat F2
datatype_compat kk1 kk2
datatype_compat ll1 ll2


subsection ‹Deep Nesting›

datatype