1(* Title: HOL/Corec_Examples/Tests/TLList_Friends.thy 2 Author: Aymeric Bouzy, Ecole polytechnique 3 Author: Jasmin Blanchette, Inria, LORIA, MPII 4 Copyright 2015, 2016 5 6Friendly functions on terminated lists. 7*) 8 9section \<open>Friendly Functions on Terminated Lists\<close> 10 11theory TLList_Friends 12imports "HOL-Library.BNF_Corec" 13begin 14 15codatatype ('a, 'b) tllist = 16 TLNil (trm: 'b) 17| TLCons (tlhd: 'a) (tltl: "('a, 'b) tllist") 18 19corec pls :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where 20 "pls s s' = TLCons (tlhd s + tlhd s') (pls (tltl s) (tltl s'))" 21 22friend_of_corec pls where 23 "pls s s' = TLCons (tlhd s + tlhd s') (pls (tltl s) (tltl s'))" 24 sorry 25 26corec prd :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where 27 "prd xs ys = TLCons (tlhd xs * tlhd ys) (pls (prd xs (tltl ys)) (prd (tltl xs) ys))" 28 29friend_of_corec prd where 30 "prd xs ys = TLCons (tlhd xs * tlhd ys) (pls (prd xs (tltl ys)) (prd (tltl xs) ys))" 31 sorry 32 33corec onetwo :: "(nat, 'b) tllist" where 34 "onetwo = TLCons 1 (TLCons 2 onetwo)" 35 36corec Exp :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where 37 "Exp xs = TLCons (2 ^^ tlhd xs) (prd (tltl xs) (Exp xs))" 38 39friend_of_corec Exp where 40 "Exp xs = TLCons (2 ^^ tlhd xs) (prd (tltl xs) (Exp xs))" 41 sorry 42 43corec prd2 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where 44 "prd2 xs ys = TLCons (tlhd xs * tlhd ys) (pls (prd xs (tltl ys)) (prd2 (tltl xs) ys))" 45 46text \<open>Outer if:\<close> 47 48corec takeUntilOdd :: "(int, int) tllist \<Rightarrow> (int, int) tllist" where 49 "takeUntilOdd xs = 50 (if is_TLNil xs then TLNil (trm xs) 51 else if tlhd xs mod 2 = 0 then TLCons (tlhd xs) (takeUntilOdd (tltl xs)) 52 else TLNil (tlhd xs))" 53 54friend_of_corec takeUntilOdd where 55 "takeUntilOdd xs = 56 (if is_TLNil xs then TLNil (trm xs) 57 else if tlhd xs mod 2 = 0 then TLCons (tlhd xs) (takeUntilOdd (tltl xs)) 58 else TLNil (tlhd xs))" 59 sorry 60 61corec takeUntilEven :: "(int, int) tllist \<Rightarrow> (int, int) tllist" where 62 "takeUntilEven xs = 63 (case xs of 64 TLNil y \<Rightarrow> TLNil y 65 | TLCons y ys \<Rightarrow> 66 if y mod 2 = 1 then TLCons y (takeUntilEven ys) 67 else TLNil y)" 68 69friend_of_corec takeUntilEven where 70 "takeUntilEven xs = 71 (case xs of 72 TLNil y \<Rightarrow> TLNil y 73 | TLCons y ys \<Rightarrow> 74 if y mod 2 = 1 then TLCons y (takeUntilEven ys) 75 else TLNil y)" 76 sorry 77 78text \<open>If inside the constructor:\<close> 79 80corec prd3 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where 81 "prd3 xs ys = TLCons (tlhd xs * tlhd ys) 82 (if undefined then pls (prd xs (tltl ys)) (prd (tltl xs) ys) 83 else prd3 (tltl xs) (tltl ys))" 84 85friend_of_corec prd3 where 86 "prd3 xs ys = TLCons (tlhd xs * tlhd ys) 87 (if undefined then pls (prd xs (tltl ys)) (prd (tltl xs) ys) 88 else prd3 (tltl xs) (tltl ys))" 89 sorry 90 91text \<open>If inside the inner friendly operation:\<close> 92 93corec prd4 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where 94 "prd4 xs ys = TLCons (tlhd xs * tlhd ys) 95 (pls (if undefined then prd xs (tltl ys) else xs) (prd (tltl xs) ys))" 96 97friend_of_corec prd4 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where 98 "prd4 xs ys = TLCons (tlhd xs * tlhd ys) 99 (pls (if undefined then prd xs (tltl ys) else xs) (prd (tltl xs) ys))" 100 sorry 101 102text \<open>Lots of if's:\<close> 103 104corec iffy :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where 105 "iffy xs = 106 (if undefined (0::nat) then 107 TLNil undefined 108 else 109 Exp (if undefined (1::nat) then 110 Exp undefined 111 else 112 TLCons undefined 113 (if undefined (2::nat) then 114 Exp (if undefined (3::nat) then 115 Exp (if undefined (4::nat) then 116 iffy (tltl xs) 117 else if undefined (5::nat) then 118 iffy xs 119 else 120 xs) 121 else 122 xs) 123 else 124 undefined)))" 125 126end 127