theory TypesInductifs
imports Main

begin

datatype nat =  Z | S nat
datatype 'a list = nil  | cons 'a "'a list"
datatype 'a tree = leaf  | node 'a "'a tree" "'a tree"
datatype ('a,'b) itree =
    ileaf  | inode 'a "'b => ('a,'b) itree"
(* datatype E = C E *)

(*
TypesInductifs.nat.induct: ?P Z \<Longrightarrow> (\<And>x. ?P x \<Longrightarrow> ?P (S x)) \<Longrightarrow> ?P ?nat
TypesInductifs.list.induct:
    ?P nil \<Longrightarrow> (\<And>x1 x2. ?P x2 \<Longrightarrow> ?P (cons x1 x2)) \<Longrightarrow> ?P ?list
TypesInductifs.tree.induct:
    ?P leaf \<Longrightarrow> (\<And>x1 x2 x3. ?P x2 \<Longrightarrow> ?P x3 \<Longrightarrow> ?P (node x1 x2 x3)) \<Longrightarrow> ?P ?tree
TypesInductifs.itree.induct:
    ?P ileaf \<Longrightarrow>
    (\<And>x1 x2.
        (\<And>x2a. x2a \<in> range x2 \<Longrightarrow> ?P x2a) \<Longrightarrow> ?P (inode x1 x2 x3)) \<Longrightarrow>
    ?P ?itree
*)

fun natR (* :: "'x \<Rightarrow> (nat \<Rightarrow> 'x \<Rightarrow> 'x) \<Rightarrow> nat \<Rightarrow> 'x" *)
where 
   "natR f g Z = f" 
 | "natR f g (S p) =  g p (natR f g p)"

fun listR where 
   "listR f g nil = f"
 | "listR f g (cons a p) = g a p (listR f g p)"

fun treeR where 
   "treeR f g leaf = f"
 | "treeR f g (node a l r) = g a l r (treeR f g l) (treeR f g r)"

(* pas accepté avec fun *)
primrec itreeR where
    "itreeR f g ileaf = f" 
  | "itreeR f g (inode a F) = g a F (\<lambda> x. itreeR f g (F x))"

term itreeR

end