author | wenzelm |
Mon, 24 Oct 2016 11:42:39 +0200 | |
changeset 64367 | a424f2737646 |
parent 63167 | 0909deb8059b |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
58309
a09ec6daaa19
renamed 'BNF_Examples' to 'Datatype_Examples' (cf. 'datatypes.pdf')
blanchet
parents:
58228
diff
changeset
|
1 |
(* Title: HOL/Datatype_Examples/Misc_Codatatype.thy |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Author: Andrei Popescu, TU Muenchen |
52323 | 4 |
Author: Jasmin Blanchette, TU Muenchen |
5 |
Copyright 2012, 2013 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
|
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52323
diff
changeset
|
7 |
Miscellaneous codatatype definitions. |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
8 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
63167 | 10 |
section \<open>Miscellaneous Codatatype Definitions\<close> |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
11 |
|
53122
bc87b7af4767
renamed theory files to be closer to (new) command names
blanchet
parents:
52323
diff
changeset
|
12 |
theory Misc_Codatatype |
55129
26bd1cba3ab5
killed 'More_BNFs' by moving its various bits where they (now) belong
blanchet
parents:
55076
diff
changeset
|
13 |
imports "~~/src/HOL/Library/FSet" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
15 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
16 |
codatatype simple = X1 | X2 | X3 | X4 |
49158 | 17 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
18 |
codatatype simple' = X1' unit | X2' unit | X3' unit | X4' unit |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
19 |
|
52323 | 20 |
codatatype simple'' = X1'' nat int | X2'' |
21 |
||
54193 | 22 |
codatatype 'a stream = Stream (shd: 'a) (stl: "'a stream") |
49158 | 23 |
|
54193 | 24 |
codatatype 'a mylist = MyNil | MyCons (myhd: 'a) (mytl: "'a mylist") |
49158 | 25 |
|
58228 | 26 |
codatatype ('b, 'c :: ord, 'd, 'e) some_passive = |
49158 | 27 |
SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
|
58417
fa50722ad6cb
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
desharna
parents:
58332
diff
changeset
|
29 |
codatatype 'a multi_live_direct1 = MultiLiveDirect1 'a |
fa50722ad6cb
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
desharna
parents:
58332
diff
changeset
|
30 |
codatatype 'a multi_live_direct2 = MultiLiveDirect2 'a 'a |
fa50722ad6cb
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
desharna
parents:
58332
diff
changeset
|
31 |
codatatype 'a multi_live_direct3 = MultiLiveDirect3 'a 'a 'a |
fa50722ad6cb
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
desharna
parents:
58332
diff
changeset
|
32 |
codatatype 'a multi_live_direct4 = MultiLiveDirect4 'a 'a 'a 'a |
fa50722ad6cb
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
desharna
parents:
58332
diff
changeset
|
33 |
codatatype 'a multi_live_direct5 = MultiLiveDirect5 'a 'a 'a 'a 'a |
fa50722ad6cb
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
desharna
parents:
58332
diff
changeset
|
34 |
codatatype 'a multi_live_direct6 = MultiLiveDirect6 'a 'a 'a 'a 'a 'a |
fa50722ad6cb
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
desharna
parents:
58332
diff
changeset
|
35 |
codatatype 'a multi_live_direct7 = MultiLiveDirect7 'a 'a 'a 'a 'a 'a 'a |
fa50722ad6cb
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
desharna
parents:
58332
diff
changeset
|
36 |
codatatype 'a multi_live_direct8 = MultiLiveDirect8 'a 'a 'a 'a 'a 'a 'a 'a |
fa50722ad6cb
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
desharna
parents:
58332
diff
changeset
|
37 |
codatatype 'a multi_live_direct9 = MultiLiveDirect9 'a 'a 'a 'a 'a 'a 'a 'a 'a |
fa50722ad6cb
make 'set_induct0' tactic more robust w.r.t multiple arguments constructors
desharna
parents:
58332
diff
changeset
|
38 |
|
58455 | 39 |
datatype 'a live_and_fun = LiveAndFun nat "nat \<Rightarrow> 'a" |
40 |
||
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
41 |
codatatype lambda = |
49158 | 42 |
Var string | |
43 |
App lambda lambda | |
|
44 |
Abs string lambda | |
|
45 |
Let "(string \<times> lambda) fset" lambda |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
46 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
47 |
codatatype 'a par_lambda = |
49158 | 48 |
PVar 'a | |
49 |
PApp "'a par_lambda" "'a par_lambda" | |
|
50 |
PAbs 'a "'a par_lambda" | |
|
51 |
PLet "('a \<times> 'a par_lambda) fset" "'a par_lambda" |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
52 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
53 |
(* |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
54 |
('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
55 |
('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
56 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
57 |
|
53591 | 58 |
codatatype 'a p = P "'a + 'a p" |
59 |
||
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
60 |
codatatype 'a J1 = J11 'a "'a J1" | J12 'a "'a J2" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
61 |
and 'a J2 = J21 | J22 "'a J1" "'a J2" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
62 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
63 |
codatatype 'a tree = TEmpty | TNode 'a "'a forest" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
64 |
and 'a forest = FNil | FCons "'a tree" "'a forest" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
65 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
66 |
codatatype 'a tree' = TEmpty' | TNode' "'a branch" "'a branch" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
67 |
and 'a branch = Branch 'a "'a tree'" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
68 |
|
55484 | 69 |
codatatype 'a bin_rose_tree = BRTree 'a "'a bin_rose_tree mylist" "'a bin_rose_tree mylist" |
70 |
||
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
71 |
codatatype ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
72 |
and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
73 |
and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
74 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
75 |
codatatype ('a, 'b, 'c) some_killing = |
49158 | 76 |
SK "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" |
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
77 |
and ('a, 'b, 'c) in_here = |
49158 | 78 |
IH1 'b 'a | IH2 'c |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
79 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
80 |
codatatype ('a, 'b, 'c) some_killing' = |
49617 | 81 |
SK' "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b, 'c) some_killing' + ('a, 'b, 'c) in_here'" |
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
82 |
and ('a, 'b, 'c) in_here' = |
49617 | 83 |
IH1' 'b | IH2' 'c |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
84 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
85 |
codatatype ('a, 'b, 'c) some_killing'' = |
49617 | 86 |
SK'' "'a \<Rightarrow> ('a, 'b, 'c) in_here''" |
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
87 |
and ('a, 'b, 'c) in_here'' = |
49617 | 88 |
IH1'' 'b 'a | IH2'' 'c |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
89 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
90 |
codatatype ('b, 'c) less_killing = LK "'b \<Rightarrow> 'c" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
91 |
|
53588
11a77e4aa98b
more robust tactic to cover another corner case (added as example);
traytel
parents:
53122
diff
changeset
|
92 |
codatatype 'b poly_unit = U "'b \<Rightarrow> 'b poly_unit" |
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
93 |
codatatype 'b cps = CPS1 'b | CPS2 "'b \<Rightarrow> 'b cps" |
49158 | 94 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
95 |
codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs = |
49158 | 96 |
FR "'b1 \<Rightarrow> 'b2 \<Rightarrow> 'b3 \<Rightarrow> 'b4 \<Rightarrow> 'b5 \<Rightarrow> 'b6 \<Rightarrow> 'b7 \<Rightarrow> 'b8 \<Rightarrow> 'b9 \<Rightarrow> |
97 |
('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs" |
|
49102
ce2ef34eb828
added examples for testing of coinductive witnesses
traytel
parents:
49074
diff
changeset
|
98 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
99 |
codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17, |
49158 | 100 |
'b18, 'b19, 'b20) fun_rhs' = |
101 |
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> |
|
102 |
'b15 \<Rightarrow> 'b16 \<Rightarrow> 'b17 \<Rightarrow> 'b18 \<Rightarrow> 'b19 \<Rightarrow> 'b20 \<Rightarrow> |
|
103 |
('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17, |
|
104 |
'b18, 'b19, 'b20) fun_rhs'" |
|
105 |
||
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
106 |
codatatype ('a, 'b, 'c) wit3_F1 = W1 'a "('a, 'b, 'c) wit3_F1" "('a, 'b, 'c) wit3_F2" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
107 |
and ('a, 'b, 'c) wit3_F2 = W2 'b "('a, 'b, 'c) wit3_F2" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
108 |
and ('a, 'b, 'c) wit3_F3 = W31 'a 'b "('a, 'b, 'c) wit3_F1" | W32 'c 'a 'b "('a, 'b, 'c) wit3_F1" |
49158 | 109 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
110 |
codatatype ('c, 'e, 'g) coind_wit1 = |
49158 | 111 |
CW1 'c "('c, 'e, 'g) coind_wit1" "('c, 'e, 'g) ind_wit" "('c, 'e, 'g) coind_wit2" |
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
112 |
and ('c, 'e, 'g) coind_wit2 = |
49158 | 113 |
CW21 "('c, 'e, 'g) coind_wit2" 'e | CW22 'c 'g |
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
114 |
and ('c, 'e, 'g) ind_wit = |
49158 | 115 |
IW1 | IW2 'c |
49102
ce2ef34eb828
added examples for testing of coinductive witnesses
traytel
parents:
49074
diff
changeset
|
116 |
|
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
117 |
codatatype ('b, 'a) bar = BAR "'a \<Rightarrow> 'b" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
118 |
codatatype ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a" |
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49158
diff
changeset
|
119 |
|
58332 | 120 |
codatatype (dead 'a) dead_foo = A |
121 |
codatatype ('a, 'b) use_dead_foo = Y 'a "'b dead_foo" |
|
122 |
||
123 |
codatatype 'a phantom = A |
|
124 |
codatatype 'a use_phantom = Y 'a "'a use_phantom phantom" |
|
49185
073d7d1b7488
respect order of/additional type variables supplied by the user in fixed point constructions;
traytel
parents:
49158
diff
changeset
|
125 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
126 |
(* SLOW, MEMORY-HUNGRY |
51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
127 |
codatatype ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
128 |
and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
129 |
and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
130 |
and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
131 |
and ('a, 'c) D5 = A5 "('a, 'c) D6" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
132 |
and ('a, 'c) D6 = A6 "('a, 'c) D7" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
133 |
and ('a, 'c) D7 = A7 "('a, 'c) D8" |
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
49617
diff
changeset
|
134 |
and ('a, 'c) D8 = A8 "('a, 'c) D1 list" |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
135 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
136 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
137 |
end |