|
(* Title: HOL/Corec_Examples/Tests/Simple_Nesting.thy
Author: Aymeric Bouzy, Ecole polytechnique
Author: Jasmin Blanchette, Inria, LORIA, MPII
Copyright 2015, 2016
Tests "corec"'s parsing of map functions.
*)
section \<open>Tests "corec"'s Parsing of Map Functions\<close>
theory Simple_Nesting
imports "HOL-Library.BNF_Corec"
begin
subsection \<open>Corecursion via Map Functions\<close>
consts
g :: 'a
g' :: 'a
g'' :: 'a
h :: 'a
h' :: 'a
q :: 'a
q' :: 'a
codatatype tree =
Node nat "tree list"
(* a direct, intuitive way to define a function *)
corec k0 where
"k0 x = Node (g x) (map (\y. if q y then g' y else k0 (h' y :: 'a)) (h (x :: 'a) :: nat list))"
(* another way -- this one is perhaps less intuitive but more systematic *)
corec k0' where
"k0' x = Node (g x) (map (\z. case z of Inl t \ t | Inr (x' :: 'a) \ k0' x')
(map (\<lambda>y. if q y then Inl (g' y) else Inr (h' y)) (h (x :: 'a) :: nat list)))"
(* more examples, same story *)
corec k1 :: "nat \ tree" where
"k1 x = Node (g x) (map (\y. k1 (h' y)) (h x :: nat list))"
corec k1' :: "nat \ tree" where
"k1' x = Node (g x) (map (\z. case z of Inl t \ t | Inr x' \ k1' x')
(map (\<lambda>y. Inr (h' y)) (h x :: nat list)))"
corec k2 :: "nat \ tree" where
"k2 x = Node (g x) (map g' (h x :: nat list))"
corec k2' :: "nat \ tree" where
"k2' x = Node (g x) (map (\z. case z of Inl t \ t | Inr (x' :: nat) \ k2' x')
(map (\<lambda>y. Inl (g' y)) (h x :: nat list)))"
corec k3 :: "nat \ tree" where
"k3 x = Node (g x) (h x)"
corec k3' :: "nat \ tree" where
"k3' x = Node (g x) (map (\z. case z of Inl t \ t | Inr (x' :: nat) \ k3' x')
(map Inl (h x)))"
subsection \<open>Constructors instead of Maps\<close>
codatatype 'a y = Y 'a "'a y list"
corec hh where
"hh a = Y a (map hh [a])"
corec k where
"k a = Y a [k a, k undefined, k (a + a), undefined, k a]"
codatatype 'a x = X 'a "'a x option"
corec f where
"f a = X a (map_option f (Some a))"
corec gg where
"gg a = X a (Some (gg a))"
subsection \<open>Some Friends\<close>
codatatype u =
U (lab: nat) (sub: "u list")
definition u_id :: "u \ u" where "u_id u = u"
friend_of_corec u_id where
"u_id u = U (lab u) (sub u)"
by (simp add: u_id_def) transfer_prover
corec u_id_f :: "u \ u" where
"u_id_f u = u_id (U (lab u) (map u_id_f (sub u)))"
corec (friend) u_id_g :: "u \ u" where
"u_id_g u = U (lab u) (map (\u'. u_id (u_id_g u')) (sub u))"
corec (friend) u_id_g' :: "u \ u" where
"u_id_g' u = U (lab u) (map (u_id o u_id_g') (sub u))"
corec (friend) u_id_g'' :: "u \ u" where
"u_id_g'' u = U (lab u) (map ((\u'. u_id u') o u_id_g'') (sub u))"
corec u_id_h :: "u \ u" where
"u_id_h u = u_id (u_id (U (lab u) (map (\u'. (u_id o u_id) (u_id (u_id (u_id_h u')))) (sub u))))"
corec u_id_h' :: "u \ u" where
"u_id_h' u = u_id (u_id (U (lab u) (map (u_id o u_id o u_id_h') (sub u))))"
corec u_id_h'' :: "u \ u" where
"u_id_h'' u = u_id (u_id (U (lab u) (map (u_id o (u_id o (\u'. u_id u')) o u_id_h'') (sub u))))"
definition u_K :: "u \ u \ u" where "u_K u v = u"
friend_of_corec u_K where
"u_K u v = U (lab u) (sub u)"
by (simp add: u_K_def) transfer_prover
corec u_K_f :: "u \ u" where
"u_K_f u = u_K (U (lab u) (map u_K_f (sub u))) undefined"
corec (friend) u_K_g :: "u \ u" where
"u_K_g u = U (lab u) (map (\u'. u_K (u_K_g u') undefined) (sub u))"
corec (friend) u_K_g' :: "u \ u" where
"u_K_g' u = U (lab u) (map ((\u'. u_K u' undefined) o u_K_g') (sub u))"
corec (friend) u_K_g'' :: "u \ u" where
"u_K_g'' u = U (lab u) (map (u_K undefined o u_K_g'') (sub u))"
end
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
