# Theory TLList_Friends

theory TLList_Friends
imports BNF_Corec
```(*  Title:      HOL/Corec_Examples/Tests/TLList_Friends.thy
Author:     Aymeric Bouzy, Ecole polytechnique
Author:     Jasmin Blanchette, Inria, LORIA, MPII

Friendly functions on terminated lists.
*)

section ‹Friendly Functions on Terminated Lists›

theory TLList_Friends
imports "HOL-Library.BNF_Corec"
begin

codatatype ('a, 'b) tllist =
TLNil (trm: 'b)
| TLCons (tlhd: 'a) (tltl: "('a, 'b) tllist")

corec pls :: "(nat, 'b) tllist ⇒ (nat, 'b) tllist ⇒ (nat, 'b) tllist" where
"pls s s' = TLCons (tlhd s + tlhd s') (pls (tltl s) (tltl s'))"

friend_of_corec pls where
"pls s s' = TLCons (tlhd s + tlhd s') (pls (tltl s) (tltl s'))"
sorry

corec prd :: "(nat, 'b) tllist ⇒ (nat, 'b) tllist ⇒ (nat, 'b) tllist" where
"prd xs ys = TLCons (tlhd xs * tlhd ys) (pls (prd xs (tltl ys)) (prd (tltl xs) ys))"

friend_of_corec prd where
"prd xs ys = TLCons (tlhd xs * tlhd ys) (pls (prd xs (tltl ys)) (prd (tltl xs) ys))"
sorry

corec onetwo :: "(nat, 'b) tllist" where
"onetwo = TLCons 1 (TLCons 2 onetwo)"

corec Exp :: "(nat, 'b) tllist ⇒ (nat, 'b) tllist" where
"Exp xs = TLCons (2 ^^ tlhd xs) (prd (tltl xs) (Exp xs))"

friend_of_corec Exp where
"Exp xs = TLCons (2 ^^ tlhd xs) (prd (tltl xs) (Exp xs))"
sorry

corec prd2 :: "(nat, 'b) tllist ⇒ (nat, 'b) tllist ⇒ (nat, 'b) tllist" where
"prd2 xs ys = TLCons (tlhd xs * tlhd ys) (pls (prd xs (tltl ys)) (prd2 (tltl xs) ys))"

text ‹Outer if:›

corec takeUntilOdd :: "(int, int) tllist ⇒ (int, int) tllist" where
"takeUntilOdd xs =
(if is_TLNil xs then TLNil (trm xs)
else if tlhd xs mod 2 = 0 then TLCons (tlhd xs) (takeUntilOdd (tltl xs))
else TLNil (tlhd xs))"

friend_of_corec takeUntilOdd where
"takeUntilOdd xs =
(if is_TLNil xs then TLNil (trm xs)
else if tlhd xs mod 2 = 0 then TLCons (tlhd xs) (takeUntilOdd (tltl xs))
else TLNil (tlhd xs))"
sorry

corec takeUntilEven :: "(int, int) tllist ⇒ (int, int) tllist" where
"takeUntilEven xs =
(case xs of
TLNil y ⇒ TLNil y
| TLCons y ys ⇒
if y mod 2 = 1 then TLCons y (takeUntilEven ys)
else TLNil y)"

friend_of_corec takeUntilEven where
"takeUntilEven xs =
(case xs of
TLNil y ⇒ TLNil y
| TLCons y ys ⇒
if y mod 2 = 1 then TLCons y (takeUntilEven ys)
else TLNil y)"
sorry

text ‹If inside the constructor:›

corec prd3 :: "(nat, 'b) tllist ⇒ (nat, 'b) tllist ⇒ (nat, 'b) tllist" where
"prd3 xs ys = TLCons (tlhd xs * tlhd ys)
(if undefined then pls (prd xs (tltl ys)) (prd (tltl xs) ys)
else prd3 (tltl xs) (tltl ys))"

friend_of_corec prd3 where
"prd3 xs ys = TLCons (tlhd xs * tlhd ys)
(if undefined then pls (prd xs (tltl ys)) (prd (tltl xs) ys)
else prd3 (tltl xs) (tltl ys))"
sorry

text ‹If inside the inner friendly operation:›

corec prd4 :: "(nat, 'b) tllist ⇒ (nat, 'b) tllist ⇒ (nat, 'b) tllist" where
"prd4 xs ys = TLCons (tlhd xs * tlhd ys)
(pls (if undefined then prd xs (tltl ys) else xs) (prd (tltl xs) ys))"

friend_of_corec prd4 :: "(nat, 'b) tllist ⇒ (nat, 'b) tllist ⇒ (nat, 'b) tllist" where
"prd4 xs ys = TLCons (tlhd xs * tlhd ys)
(pls (if undefined then prd xs (tltl ys) else xs) (prd (tltl xs) ys))"
sorry

text ‹Lots of if's:›

corec iffy :: "(nat, 'b) tllist ⇒ (nat, 'b) tllist" where
"iffy xs =
(if undefined (0::nat) then
TLNil undefined
else
Exp (if undefined (1::nat) then
Exp undefined
else
TLCons undefined
(if undefined (2::nat) then
Exp (if undefined (3::nat) then
Exp (if undefined (4::nat) then
iffy (tltl xs)
else if undefined (5::nat) then
iffy xs
else
xs)
else
xs)
else
undefined)))"

end
```