1.1 --- a/src/HOL/Codatatype/Examples/Misc_Codata.thy	Wed Sep 05 15:40:13 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Examples/Misc_Codata.thy	Wed Sep 05 15:40:26 2012 +0200
     1.3 @@ -12,56 +12,57 @@
     1.4  imports "../Codatatype"
     1.5  begin
     1.6  
     1.7 -codata_raw simple: 'a = "unit + unit + unit + unit"
     1.8 +codata simple = X1 | X2 | X3 | X4
     1.9  
    1.10 -codata_raw stream: 's = "'a \<times> 's"
    1.11 +codata simple' = X1' unit | X2' unit | X3' unit | X4' unit
    1.12  
    1.13 -codata_raw llist: 'llist = "unit + 'a \<times> 'llist"
    1.14 +codata 'a stream = Stream 'a "'a stream"
    1.15  
    1.16 -codata_raw some_passive: 'a = "'a + 'b + 'c + 'd + 'e"
    1.17 +codata 'a mylist = MyNil | MyCons 'a "'a mylist"
    1.18 +
    1.19 +codata ('b, 'c, 'd, 'e) some_passive =
    1.20 +  SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e
    1.21 +
    1.22 +codata lambda =
    1.23 +  Var string |
    1.24 +  App lambda lambda |
    1.25 +  Abs string lambda |
    1.26 +  Let "(string \<times> lambda) fset" lambda
    1.27 +
    1.28 +codata 'a par_lambda =
    1.29 +  PVar 'a |
    1.30 +  PApp "'a par_lambda" "'a par_lambda" |
    1.31 +  PAbs 'a "'a par_lambda" |
    1.32 +  PLet "('a \<times> 'a par_lambda) fset" "'a par_lambda"
    1.33  
    1.34  (*
    1.35    ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2
    1.36    ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2
    1.37  *)
    1.38  
    1.39 -codata_raw F1: 'b1 = "'a \<times> 'b1 + 'a \<times> 'b2"
    1.40 -and F2: 'b2 = "unit + 'b1 * 'b2"
    1.41 +codata 'a J1 = J11 'a "'a J1" | J12 'a "'a J2"
    1.42 +   and 'a J2 = J21 | J22 "'a J1" "'a J2"
    1.43  
    1.44 -codata_raw EXPR:   'E = "'T + 'T \<times> 'E"
    1.45 -and TERM:   'T = "'F + 'F \<times> 'T"
    1.46 -and FACTOR: 'F = "'a + 'b + 'E"
    1.47 +codata 'a tree = TEmpty | TNode 'a "'a forest"
    1.48 +   and 'a forest = FNil | FCons "'a tree" "'a forest"
    1.49  
    1.50 -codata_raw llambda:
    1.51 -  'trm = "string +
    1.52 -          'trm \<times> 'trm +
    1.53 -          string \<times> 'trm +
    1.54 -          (string \<times> 'trm) fset \<times> 'trm"
    1.55 +codata 'a tree' = TEmpty' | TNode' "'a branch" "'a branch"
    1.56 +   and 'a branch = Branch 'a "'a tree'"
    1.57  
    1.58 -codata_raw par_llambda:
    1.59 -  'trm = "'a +
    1.60 -          'trm \<times> 'trm +
    1.61 -          'a \<times> 'trm +
    1.62 -          ('a \<times> 'trm) fset \<times> 'trm"
    1.63 +codata ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp"
    1.64 +   and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm"
    1.65 +   and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
    1.66  
    1.67 -(*
    1.68 -  'a tree = Empty | Node of 'a * 'a forest      ('b = unit + 'a * 'c)
    1.69 -  'a forest = Nil | Cons of 'a tree * 'a forest ('c = unit + 'b * 'c)
    1.70 +codata_raw some_killing: 'A = "'a \<Rightarrow> 'b \<Rightarrow> ('A + 'B)"
    1.71 +       and in_here: 'B = "'b \<times> 'a + 'c"
    1.72 +
    1.73 +(* FIXME
    1.74 +codata ('a, 'b, 'c) some_killing =
    1.75 +  SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here"
    1.76 + and ('a, 'b, 'c) in_here =
    1.77 +  IH1 'b 'a | IH2 'c
    1.78  *)
    1.79  
    1.80 -codata_raw tree:     'tree = "unit + 'a \<times> 'forest"
    1.81 -and forest: 'forest = "unit + 'tree \<times> 'forest"
    1.82 -
    1.83 -codata_raw CPS: 'a = "'b + 'b \<Rightarrow> 'a"
    1.84 -
    1.85 -codata_raw fun_rhs: 'a = "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'a"
    1.86 -
    1.87 -codata_raw fun_rhs': 'a = "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'b10 \<Rightarrow>
    1.88 -                    'b11 \<Rightarrow> 'b12 \<Rightarrow> 'b13 \<Rightarrow> 'b14 \<Rightarrow> 'b15 \<Rightarrow> 'b16 \<Rightarrow> 'b17 \<Rightarrow> 'b18 \<Rightarrow> 'b19 \<Rightarrow> 'b20 \<Rightarrow> 'a"
    1.89 -
    1.90 -codata_raw some_killing: 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
    1.91 -and in_here: 'c = "'d \<times> 'b + 'e"
    1.92 -
    1.93  codata_raw some_killing': 'a = "'b \<Rightarrow> 'd \<Rightarrow> ('a + 'c)"
    1.94  and in_here': 'c = "'d + 'e"
    1.95  
    1.96 @@ -70,25 +71,39 @@
    1.97  
    1.98  codata_raw less_killing: 'a = "'b \<Rightarrow> 'c"
    1.99  
   1.100 -codata_raw
   1.101 -    wit3_F1: 'b1 = "'a1 \<times> 'b1 \<times> 'b2"
   1.102 -and wit3_F2: 'b2 = "'a2 \<times> 'b2"
   1.103 -and wit3_F3: 'b3 = "'a1 \<times> 'a2 \<times> 'b1 + 'a3 \<times> 'a1 \<times> 'a2 \<times> 'b1"
   1.104 +codata 'b cps = CPS1 'b | CPS2 "'b \<Rightarrow> 'b cps"
   1.105  
   1.106 -codata_raw
   1.107 -    coind_wit1: 'a = "'c \<times> 'a \<times> 'b \<times> 'd"
   1.108 -and coind_wit2: 'd = "'d \<times> 'e + 'c \<times> 'g"
   1.109 -and ind_wit:    'b = "unit + 'c"
   1.110 +codata ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs =
   1.111 +  FR "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow>
   1.112 +      ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs"
   1.113 +
   1.114 +codata ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17,
   1.115 +        'b18, 'b19, 'b20) fun_rhs' =
   1.116 +  FR' "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> 'b10 \<Rightarrow> 'b11 \<Rightarrow> 'b12 \<Rightarrow> 'b13 \<Rightarrow> 'b14 \<Rightarrow>
   1.117 +       'b15 \<Rightarrow> 'b16 \<Rightarrow> 'b17 \<Rightarrow> 'b18 \<Rightarrow> 'b19 \<Rightarrow> 'b20 \<Rightarrow>
   1.118 +       ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17,
   1.119 +        'b18, 'b19, 'b20) fun_rhs'"
   1.120 +
   1.121 +codata ('a, 'b, 'c) wit3_F1 = W1 'a "('a, 'b, 'c) wit3_F1" "('a, 'b, 'c) wit3_F2"
   1.122 +   and ('a, 'b, 'c) wit3_F2 = W2 'b "('a, 'b, 'c) wit3_F2"
   1.123 +   and ('a, 'b, 'c) wit3_F3 = W31 'a 'b "('a, 'b, 'c) wit3_F1" | W32 'c 'a 'b "('a, 'b, 'c) wit3_F1"
   1.124 +
   1.125 +codata ('c, 'e, 'g) coind_wit1 =
   1.126 +       CW1 'c "('c, 'e, 'g) coind_wit1" "('c, 'e, 'g) ind_wit" "('c, 'e, 'g) coind_wit2"
   1.127 +   and ('c, 'e, 'g) coind_wit2 =
   1.128 +       CW21 "('c, 'e, 'g) coind_wit2" 'e | CW22 'c 'g
   1.129 +   and ('c, 'e, 'g) ind_wit =
   1.130 +       IW1 | IW2 'c
   1.131  
   1.132  (* SLOW, MEMORY-HUNGRY
   1.133 -codata_raw K1': 'K1 = "'K2 + 'a list"
   1.134 -and K2': 'K2 = "'K3 + 'c fset"
   1.135 -and K3': 'K3 = "'K3 + 'K4 + 'K4 \<times> 'K5"
   1.136 -and K4': 'K4 = "'K5 + 'a list list list"
   1.137 -and K5': 'K5 = "'K6"
   1.138 -and K6': 'K6 = "'K7"
   1.139 -and K7': 'K7 = "'K8"
   1.140 -and K8': 'K8 = "'K1 list"
   1.141 +codata ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list"
   1.142 +   and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list"
   1.143 +   and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5"
   1.144 +   and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list"
   1.145 +   and ('a, 'c) D5 = A5 "('a, 'c) D6"
   1.146 +   and ('a, 'c) D6 = A6 "('a, 'c) D7"
   1.147 +   and ('a, 'c) D7 = A7 "('a, 'c) D8"
   1.148 +   and ('a, 'c) D8 = A8 "('a, 'c) D1 list"
   1.149  *)
   1.150  
   1.151  end

     2.1 --- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Wed Sep 05 15:40:13 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Wed Sep 05 15:40:26 2012 +0200
     2.3 @@ -52,7 +52,7 @@
     2.4   and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp"
     2.5  
     2.6  data_raw some_killing: 'A = "'a \<Rightarrow> 'b \<Rightarrow> ('A + 'B)"
     2.7 -and in_here: 'B = "'b \<times> 'a + 'c"
     2.8 +     and in_here: 'B = "'b \<times> 'a + 'c"
     2.9  
    2.10  (* FIXME
    2.11  data ('a, 'b, 'c) some_killing =