(* Title: HOL/Corec_Examples/Tests/TLList_Friends.thy Author: Aymeric Bouzy, Ecole polytechnique Author: Jasmin Blanchette, Inria, LORIA, MPII Copyright 2015, 2016 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