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