src/HOL/Corec_Examples/Tests/TLList_Friends.thy
changeset 62696 7325d8573fb8
child 62726 5b2a7caa855b
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Corec_Examples/Tests/TLList_Friends.thy	Tue Mar 22 12:39:37 2016 +0100
     1.3 @@ -0,0 +1,126 @@
     1.4 +(*  Title:      HOL/Corec_Examples/Tests/TLList_Friends.thy
     1.5 +    Author:     Aymeric Bouzy, Ecole polytechnique
     1.6 +    Author:     Jasmin Blanchette, Inria, LORIA, MPII
     1.7 +    Copyright   2015, 2016
     1.8 +
     1.9 +Terminated lists examples
    1.10 +*)
    1.11 +
    1.12 +section {* Small Concrete Examples *}
    1.13 +
    1.14 +theory TLList_Friends
    1.15 +imports "~~/src/HOL/Library/BNF_Corec"
    1.16 +begin
    1.17 +
    1.18 +codatatype ('a, 'b) tllist =
    1.19 +  TLNil (trm: 'b)
    1.20 +| TLCons (tlhd: 'a) (tltl: "('a, 'b) tllist")
    1.21 +
    1.22 +corec pls :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
    1.23 +  "pls s s' = TLCons (tlhd s + tlhd s') (pls (tltl s) (tltl s'))"
    1.24 +
    1.25 +friend_of_corec pls where
    1.26 +  "pls s s' = TLCons (tlhd s + tlhd s') (pls (tltl s) (tltl s'))"
    1.27 +  sorry
    1.28 +
    1.29 +corec prd :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
    1.30 +  "prd xs ys = TLCons (tlhd xs * tlhd ys) (pls (prd xs (tltl ys)) (prd (tltl xs) ys))"
    1.31 +
    1.32 +friend_of_corec prd where
    1.33 +  "prd xs ys = TLCons (tlhd xs * tlhd ys) (pls (prd xs (tltl ys)) (prd (tltl xs) ys))"
    1.34 +  sorry
    1.35 +
    1.36 +corec onetwo :: "(nat, 'b) tllist" where
    1.37 +  "onetwo = TLCons 1 (TLCons 2 onetwo)"
    1.38 +
    1.39 +corec Exp :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
    1.40 +  "Exp xs = TLCons (2 ^^ tlhd xs) (prd (tltl xs) (Exp xs))"
    1.41 +
    1.42 +friend_of_corec Exp where
    1.43 +  "Exp xs = TLCons (2 ^^ tlhd xs) (prd (tltl xs) (Exp xs))"
    1.44 +  sorry
    1.45 +
    1.46 +corec prd2 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
    1.47 +  "prd2 xs ys = TLCons (tlhd xs * tlhd ys) (pls (prd xs (tltl ys)) (prd2 (tltl xs) ys))"
    1.48 +
    1.49 +text {* Outer if: *}
    1.50 +
    1.51 +corec takeUntilOdd :: "(int, int) tllist \<Rightarrow> (int, int) tllist" where
    1.52 +  "takeUntilOdd xs =
    1.53 +     (if is_TLNil xs then TLNil (trm xs)
    1.54 +      else if tlhd xs mod 2 = 0 then TLCons (tlhd xs) (takeUntilOdd (tltl xs))
    1.55 +      else TLNil (tlhd xs))"
    1.56 +
    1.57 +friend_of_corec takeUntilOdd where
    1.58 +  "takeUntilOdd xs =
    1.59 +     (if is_TLNil xs then TLNil (trm xs)
    1.60 +      else if tlhd xs mod 2 = 0 then TLCons (tlhd xs) (takeUntilOdd (tltl xs))
    1.61 +      else TLNil (tlhd xs))"
    1.62 +      sorry
    1.63 +
    1.64 +corec takeUntilEven :: "(int, int) tllist \<Rightarrow> (int, int) tllist" where
    1.65 +  "takeUntilEven xs =
    1.66 +     (case xs of
    1.67 +        TLNil y \<Rightarrow> TLNil y
    1.68 +      | TLCons y ys \<Rightarrow>
    1.69 +        if y mod 2 = 1 then TLCons y (takeUntilEven ys)
    1.70 +        else TLNil y)"
    1.71 +
    1.72 +friend_of_corec takeUntilEven where
    1.73 +  "takeUntilEven xs =
    1.74 +     (case xs of
    1.75 +        TLNil y \<Rightarrow> TLNil y
    1.76 +      | TLCons y ys \<Rightarrow>
    1.77 +        if y mod 2 = 1 then TLCons y (takeUntilEven ys)
    1.78 +        else TLNil y)"
    1.79 +        sorry
    1.80 +
    1.81 +text {* If inside the constructor: *}
    1.82 +
    1.83 +corec prd3 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
    1.84 +  "prd3 xs ys = TLCons (tlhd xs * tlhd ys)
    1.85 +     (if undefined then pls (prd xs (tltl ys)) (prd (tltl xs) ys)
    1.86 +      else prd3 (tltl xs) (tltl ys))"
    1.87 +
    1.88 +friend_of_corec prd3 where
    1.89 +  "prd3 xs ys = TLCons (tlhd xs * tlhd ys)
    1.90 +     (if undefined then pls (prd xs (tltl ys)) (prd (tltl xs) ys)
    1.91 +      else prd3 (tltl xs) (tltl ys))"
    1.92 + sorry
    1.93 +
    1.94 +text {* If inside the inner friendly operation: *}
    1.95 +
    1.96 +corec prd4 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
    1.97 +  "prd4 xs ys = TLCons (tlhd xs * tlhd ys)
    1.98 +     (pls (if undefined then prd xs (tltl ys) else xs) (prd (tltl xs) ys))"
    1.99 +
   1.100 +friend_of_corec prd4 :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
   1.101 +  "prd4 xs ys = TLCons (tlhd xs * tlhd ys)
   1.102 +     (pls (if undefined then prd xs (tltl ys) else xs) (prd (tltl xs) ys))"
   1.103 +  sorry
   1.104 +
   1.105 +text {* Lots of if's: *}
   1.106 +
   1.107 +corec iffy :: "(nat, 'b) tllist \<Rightarrow> (nat, 'b) tllist" where
   1.108 +  "iffy xs =
   1.109 +   (if undefined (0::nat) then
   1.110 +      TLNil undefined
   1.111 +    else
   1.112 +      Exp (if undefined (1::nat) then
   1.113 +             Exp undefined
   1.114 +           else
   1.115 +             TLCons undefined
   1.116 +               (if undefined (2::nat) then
   1.117 +                  Exp (if undefined (3::nat) then
   1.118 +                         Exp (if undefined (4::nat) then
   1.119 +                                iffy (tltl xs)
   1.120 +                              else if undefined (5::nat) then
   1.121 +                                iffy xs
   1.122 +                              else
   1.123 +                                xs)
   1.124 +                       else
   1.125 +                         xs)
   1.126 +                else
   1.127 +                  undefined)))"
   1.128 +
   1.129 +end