# HG changeset patch # User blanchet # Date 1377069940 -7200 # Node ID bc87b7af476740c98a31f1e80dd23a8c38bb6285 # Parent 5f727525b1acad420ab150626446f01471a7c319 renamed theory files to be closer to (new) command names diff -r 5f727525b1ac -r bc87b7af4767 src/HOL/BNF/Examples/Misc_Codata.thy --- a/src/HOL/BNF/Examples/Misc_Codata.thy Wed Aug 21 09:25:40 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,117 +0,0 @@ -(* Title: HOL/BNF/Examples/Misc_Codata.thy - Author: Dmitriy Traytel, TU Muenchen - Author: Andrei Popescu, TU Muenchen - Author: Jasmin Blanchette, TU Muenchen - Copyright 2012, 2013 - -Miscellaneous codatatype declarations. -*) - -header {* Miscellaneous Codatatype Declarations *} - -theory Misc_Codata -imports "../BNF" -begin - -codatatype simple = X1 | X2 | X3 | X4 - -codatatype simple' = X1' unit | X2' unit | X3' unit | X4' unit - -codatatype simple'' = X1'' nat int | X2'' - -codatatype 'a stream = Stream 'a "'a stream" - -codatatype 'a mylist = MyNil | MyCons 'a "'a mylist" - -codatatype ('b, 'c, 'd, 'e) some_passive = - SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e - -codatatype lambda = - Var string | - App lambda lambda | - Abs string lambda | - Let "(string \ lambda) fset" lambda - -codatatype 'a par_lambda = - PVar 'a | - PApp "'a par_lambda" "'a par_lambda" | - PAbs 'a "'a par_lambda" | - PLet "('a \ 'a par_lambda) fset" "'a par_lambda" - -(* - ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2 - ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 -*) - -codatatype 'a J1 = J11 'a "'a J1" | J12 'a "'a J2" -and 'a J2 = J21 | J22 "'a J1" "'a J2" - -codatatype 'a tree = TEmpty | TNode 'a "'a forest" -and 'a forest = FNil | FCons "'a tree" "'a forest" - -codatatype 'a tree' = TEmpty' | TNode' "'a branch" "'a branch" -and 'a branch = Branch 'a "'a tree'" - -codatatype ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" -and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" -and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" - -codatatype ('a, 'b, 'c) some_killing = - SK "'a \ 'b \ ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" -and ('a, 'b, 'c) in_here = - IH1 'b 'a | IH2 'c - -codatatype ('a, 'b, 'c) some_killing' = - SK' "'a \ 'b \ ('a, 'b, 'c) some_killing' + ('a, 'b, 'c) in_here'" -and ('a, 'b, 'c) in_here' = - IH1' 'b | IH2' 'c - -codatatype ('a, 'b, 'c) some_killing'' = - SK'' "'a \ ('a, 'b, 'c) in_here''" -and ('a, 'b, 'c) in_here'' = - IH1'' 'b 'a | IH2'' 'c - -codatatype ('b, 'c) less_killing = LK "'b \ 'c" - -codatatype 'b cps = CPS1 'b | CPS2 "'b \ 'b cps" - -codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs = - FR "'b1 \ 'b2 \ 'b3 \ 'b4 \ 'b5 \ 'b6 \ 'b7 \ 'b8 \ 'b9 \ - ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs" - -codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17, - 'b18, 'b19, 'b20) fun_rhs' = - FR' "'b1 \ 'b2 \ 'b3 \ 'b4 \ 'b5 \ 'b6 \ 'b7 \ 'b8 \ 'b9 \ 'b10 \ 'b11 \ 'b12 \ 'b13 \ 'b14 \ - 'b15 \ 'b16 \ 'b17 \ 'b18 \ 'b19 \ 'b20 \ - ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17, - 'b18, 'b19, 'b20) fun_rhs'" - -codatatype ('a, 'b, 'c) wit3_F1 = W1 'a "('a, 'b, 'c) wit3_F1" "('a, 'b, 'c) wit3_F2" -and ('a, 'b, 'c) wit3_F2 = W2 'b "('a, 'b, 'c) wit3_F2" -and ('a, 'b, 'c) wit3_F3 = W31 'a 'b "('a, 'b, 'c) wit3_F1" | W32 'c 'a 'b "('a, 'b, 'c) wit3_F1" - -codatatype ('c, 'e, 'g) coind_wit1 = - CW1 'c "('c, 'e, 'g) coind_wit1" "('c, 'e, 'g) ind_wit" "('c, 'e, 'g) coind_wit2" -and ('c, 'e, 'g) coind_wit2 = - CW21 "('c, 'e, 'g) coind_wit2" 'e | CW22 'c 'g -and ('c, 'e, 'g) ind_wit = - IW1 | IW2 'c - -codatatype ('b, 'a) bar = BAR "'a \ 'b" -codatatype ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \ 'c + 'a" - -codatatype 'a dead_foo = A -codatatype ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" - -(* SLOW, MEMORY-HUNGRY -codatatype ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" -and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" -and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" -and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" -and ('a, 'c) D5 = A5 "('a, 'c) D6" -and ('a, 'c) D6 = A6 "('a, 'c) D7" -and ('a, 'c) D7 = A7 "('a, 'c) D8" -and ('a, 'c) D8 = A8 "('a, 'c) D1 list" -*) - -end diff -r 5f727525b1ac -r bc87b7af4767 src/HOL/BNF/Examples/Misc_Codatatype.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BNF/Examples/Misc_Codatatype.thy Wed Aug 21 09:25:40 2013 +0200 @@ -0,0 +1,117 @@ +(* Title: HOL/BNF/Examples/Misc_Codatatype.thy + Author: Dmitriy Traytel, TU Muenchen + Author: Andrei Popescu, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012, 2013 + +Miscellaneous codatatype definitions. +*) + +header {* Miscellaneous Codatatype Definitions *} + +theory Misc_Codatatype +imports "../BNF" +begin + +codatatype simple = X1 | X2 | X3 | X4 + +codatatype simple' = X1' unit | X2' unit | X3' unit | X4' unit + +codatatype simple'' = X1'' nat int | X2'' + +codatatype 'a stream = Stream 'a "'a stream" + +codatatype 'a mylist = MyNil | MyCons 'a "'a mylist" + +codatatype ('b, 'c, 'd, 'e) some_passive = + SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e + +codatatype lambda = + Var string | + App lambda lambda | + Abs string lambda | + Let "(string \ lambda) fset" lambda + +codatatype 'a par_lambda = + PVar 'a | + PApp "'a par_lambda" "'a par_lambda" | + PAbs 'a "'a par_lambda" | + PLet "('a \ 'a par_lambda) fset" "'a par_lambda" + +(* + ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2 + ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 +*) + +codatatype 'a J1 = J11 'a "'a J1" | J12 'a "'a J2" +and 'a J2 = J21 | J22 "'a J1" "'a J2" + +codatatype 'a tree = TEmpty | TNode 'a "'a forest" +and 'a forest = FNil | FCons "'a tree" "'a forest" + +codatatype 'a tree' = TEmpty' | TNode' "'a branch" "'a branch" +and 'a branch = Branch 'a "'a tree'" + +codatatype ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" +and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" +and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" + +codatatype ('a, 'b, 'c) some_killing = + SK "'a \ 'b \ ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" +and ('a, 'b, 'c) in_here = + IH1 'b 'a | IH2 'c + +codatatype ('a, 'b, 'c) some_killing' = + SK' "'a \ 'b \ ('a, 'b, 'c) some_killing' + ('a, 'b, 'c) in_here'" +and ('a, 'b, 'c) in_here' = + IH1' 'b | IH2' 'c + +codatatype ('a, 'b, 'c) some_killing'' = + SK'' "'a \ ('a, 'b, 'c) in_here''" +and ('a, 'b, 'c) in_here'' = + IH1'' 'b 'a | IH2'' 'c + +codatatype ('b, 'c) less_killing = LK "'b \ 'c" + +codatatype 'b cps = CPS1 'b | CPS2 "'b \ 'b cps" + +codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs = + FR "'b1 \ 'b2 \ 'b3 \ 'b4 \ 'b5 \ 'b6 \ 'b7 \ 'b8 \ 'b9 \ + ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9) fun_rhs" + +codatatype ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17, + 'b18, 'b19, 'b20) fun_rhs' = + FR' "'b1 \ 'b2 \ 'b3 \ 'b4 \ 'b5 \ 'b6 \ 'b7 \ 'b8 \ 'b9 \ 'b10 \ 'b11 \ 'b12 \ 'b13 \ 'b14 \ + 'b15 \ 'b16 \ 'b17 \ 'b18 \ 'b19 \ 'b20 \ + ('b1, 'b2, 'b3, 'b4, 'b5, 'b6, 'b7, 'b8, 'b9, 'b10, 'b11, 'b12, 'b13, 'b14, 'b15, 'b16, 'b17, + 'b18, 'b19, 'b20) fun_rhs'" + +codatatype ('a, 'b, 'c) wit3_F1 = W1 'a "('a, 'b, 'c) wit3_F1" "('a, 'b, 'c) wit3_F2" +and ('a, 'b, 'c) wit3_F2 = W2 'b "('a, 'b, 'c) wit3_F2" +and ('a, 'b, 'c) wit3_F3 = W31 'a 'b "('a, 'b, 'c) wit3_F1" | W32 'c 'a 'b "('a, 'b, 'c) wit3_F1" + +codatatype ('c, 'e, 'g) coind_wit1 = + CW1 'c "('c, 'e, 'g) coind_wit1" "('c, 'e, 'g) ind_wit" "('c, 'e, 'g) coind_wit2" +and ('c, 'e, 'g) coind_wit2 = + CW21 "('c, 'e, 'g) coind_wit2" 'e | CW22 'c 'g +and ('c, 'e, 'g) ind_wit = + IW1 | IW2 'c + +codatatype ('b, 'a) bar = BAR "'a \ 'b" +codatatype ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \ 'c + 'a" + +codatatype 'a dead_foo = A +codatatype ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" + +(* SLOW, MEMORY-HUNGRY +codatatype ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" +and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" +and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" +and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" +and ('a, 'c) D5 = A5 "('a, 'c) D6" +and ('a, 'c) D6 = A6 "('a, 'c) D7" +and ('a, 'c) D7 = A7 "('a, 'c) D8" +and ('a, 'c) D8 = A8 "('a, 'c) D1 list" +*) + +end diff -r 5f727525b1ac -r bc87b7af4767 src/HOL/BNF/Examples/Misc_Data.thy --- a/src/HOL/BNF/Examples/Misc_Data.thy Wed Aug 21 09:25:40 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,183 +0,0 @@ -(* Title: HOL/BNF/Examples/Misc_Data.thy - Author: Dmitriy Traytel, TU Muenchen - Author: Andrei Popescu, TU Muenchen - Author: Jasmin Blanchette, TU Muenchen - Copyright 2012, 2013 - -Miscellaneous datatype declarations. -*) - -header {* Miscellaneous Datatype Declarations *} - -theory Misc_Data -imports "../BNF" -begin - -datatype_new simple = X1 | X2 | X3 | X4 - -datatype_new simple' = X1' unit | X2' unit | X3' unit | X4' unit - -datatype_new simple'' = X1'' nat int | X2'' - -datatype_new 'a mylist = MyNil | MyCons 'a "'a mylist" - -datatype_new ('b, 'c, 'd, 'e) some_passive = - SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e - -datatype_new hfset = HFset "hfset fset" - -datatype_new lambda = - Var string | - App lambda lambda | - Abs string lambda | - Let "(string \ lambda) fset" lambda - -datatype_new 'a par_lambda = - PVar 'a | - PApp "'a par_lambda" "'a par_lambda" | - PAbs 'a "'a par_lambda" | - PLet "('a \ 'a par_lambda) fset" "'a par_lambda" - -(* - ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2 - ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 -*) - -datatype_new 'a I1 = I11 'a "'a I1" | I12 'a "'a I2" -and 'a I2 = I21 | I22 "'a I1" "'a I2" - -datatype_new 'a tree = TEmpty | TNode 'a "'a forest" -and 'a forest = FNil | FCons "'a tree" "'a forest" - -datatype_new 'a tree' = TEmpty' | TNode' "'a branch" "'a branch" -and 'a branch = Branch 'a "'a tree'" - -datatype_new ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" -and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" -and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" - -datatype_new ('a, 'b, 'c) some_killing = - SK "'a \ 'b \ ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" -and ('a, 'b, 'c) in_here = - IH1 'b 'a | IH2 'c - -datatype_new 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b -datatype_new 'b nofail2 = NF2 "('b nofail2 \ 'b \ 'b nofail2 \ 'b) list" -datatype_new 'b nofail3 = NF3 'b "('b nofail3 \ 'b \ 'b nofail3 \ 'b) fset" -datatype_new 'b nofail4 = NF4 "('b nofail4 \ ('b nofail4 \ 'b \ 'b nofail4 \ 'b) fset) list" - -(* -datatype_new 'b fail = F "'b fail" 'b "'b fail" "'b list" -datatype_new 'b fail = F "'b fail" 'b "'b fail" 'b -datatype_new 'b fail = F1 "'b fail" 'b | F2 "'b fail" -datatype_new 'b fail = F "'b fail" 'b -*) - -datatype_new l1 = L1 "l2 list" -and l2 = L21 "l1 fset" | L22 l2 - -datatype_new kk1 = KK1 kk2 -and kk2 = KK2 kk3 -and kk3 = KK3 "kk1 list" - -datatype_new t1 = T11 t3 | T12 t2 -and t2 = T2 t1 -and t3 = T3 - -datatype_new t1' = T11' t2' | T12' t3' -and t2' = T2' t1' -and t3' = T3' - -(* -datatype_new fail1 = F1 fail2 -and fail2 = F2 fail3 -and fail3 = F3 fail1 - -datatype_new fail1 = F1 "fail2 list" fail2 -and fail2 = F2 "fail2 fset" fail3 -and fail3 = F3 fail1 - -datatype_new fail1 = F1 "fail2 list" fail2 -and fail2 = F2 "fail1 fset" fail1 -*) - -(* SLOW -datatype_new ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" -and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" -and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" -and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" -and ('a, 'c) D5 = A5 "('a, 'c) D6" -and ('a, 'c) D6 = A6 "('a, 'c) D7" -and ('a, 'c) D7 = A7 "('a, 'c) D8" -and ('a, 'c) D8 = A8 "('a, 'c) D1 list" - -(*time comparison*) -datatype ('a, 'c) D1' = A1' "('a, 'c) D2'" | B1' "'a list" - and ('a, 'c) D2' = A2' "('a, 'c) D3'" | B2' "'c list" - and ('a, 'c) D3' = A3' "('a, 'c) D3'" | B3' "('a, 'c) D4'" | C3' "('a, 'c) D4'" "('a, 'c) D5'" - and ('a, 'c) D4' = A4' "('a, 'c) D5'" | B4' "'a list list list" - and ('a, 'c) D5' = A5' "('a, 'c) D6'" - and ('a, 'c) D6' = A6' "('a, 'c) D7'" - and ('a, 'c) D7' = A7' "('a, 'c) D8'" - and ('a, 'c) D8' = A8' "('a, 'c) D1' list" -*) - -(* fail: -datatype_new tt1 = TT11 tt2 tt3 | TT12 tt2 tt4 -and tt2 = TT2 -and tt3 = TT3 tt4 -and tt4 = TT4 tt1 -*) - -datatype_new k1 = K11 k2 k3 | K12 k2 k4 -and k2 = K2 -and k3 = K3 k4 -and k4 = K4 - -datatype_new tt1 = TT11 tt3 tt2 | TT12 tt2 tt4 -and tt2 = TT2 -and tt3 = TT3 tt1 -and tt4 = TT4 - -(* SLOW -datatype_new s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2 -and s2 = S21 s7 s5 | S22 s5 s4 s6 -and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5 -and s4 = S4 s5 -and s5 = S5 -and s6 = S61 s6 | S62 s1 s2 | S63 s6 -and s7 = S71 s8 | S72 s5 -and s8 = S8 nat -*) - -datatype_new 'a deadbar = DeadBar "'a \ 'a" -datatype_new 'a deadbar_option = DeadBarOption "'a option \ 'a option" -datatype_new ('a, 'b) bar = Bar "'b \ 'a" -datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \ 'c + 'a" -datatype_new 'a deadfoo = C "'a \ 'a + 'a" - -datatype_new 'a dead_foo = A -datatype_new ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" - -datatype_new d1 = D -datatype_new d1' = is_D: D - -datatype_new d2 = D nat -datatype_new d2' = is_D: D nat - -datatype_new d3 = D | E -datatype_new d3' = D | is_E: E -datatype_new d3'' = is_D: D | E -datatype_new d3''' = is_D: D | is_E: E - -datatype_new d4 = D nat | E -datatype_new d4' = D nat | is_E: E -datatype_new d4'' = is_D: D nat | E -datatype_new d4''' = is_D: D nat | is_E: E - -datatype_new d5 = D nat | E int -datatype_new d5' = D nat | is_E: E int -datatype_new d5'' = is_D: D nat | E int -datatype_new d5''' = is_D: D nat | is_E: E int - -end diff -r 5f727525b1ac -r bc87b7af4767 src/HOL/BNF/Examples/Misc_Datatype.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/BNF/Examples/Misc_Datatype.thy Wed Aug 21 09:25:40 2013 +0200 @@ -0,0 +1,183 @@ +(* Title: HOL/BNF/Examples/Misc_Datatype.thy + Author: Dmitriy Traytel, TU Muenchen + Author: Andrei Popescu, TU Muenchen + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012, 2013 + +Miscellaneous datatype definitions. +*) + +header {* Miscellaneous Datatype Definitions *} + +theory Misc_Datatype +imports "../BNF" +begin + +datatype_new simple = X1 | X2 | X3 | X4 + +datatype_new simple' = X1' unit | X2' unit | X3' unit | X4' unit + +datatype_new simple'' = X1'' nat int | X2'' + +datatype_new 'a mylist = MyNil | MyCons 'a "'a mylist" + +datatype_new ('b, 'c, 'd, 'e) some_passive = + SP1 "('b, 'c, 'd, 'e) some_passive" | SP2 'b | SP3 'c | SP4 'd | SP5 'e + +datatype_new hfset = HFset "hfset fset" + +datatype_new lambda = + Var string | + App lambda lambda | + Abs string lambda | + Let "(string \ lambda) fset" lambda + +datatype_new 'a par_lambda = + PVar 'a | + PApp "'a par_lambda" "'a par_lambda" | + PAbs 'a "'a par_lambda" | + PLet "('a \ 'a par_lambda) fset" "'a par_lambda" + +(* + ('a, 'b1, 'b2) F1 = 'a * 'b1 + 'a * 'b2 + ('a, 'b1, 'b2) F2 = unit + 'b1 * 'b2 +*) + +datatype_new 'a I1 = I11 'a "'a I1" | I12 'a "'a I2" +and 'a I2 = I21 | I22 "'a I1" "'a I2" + +datatype_new 'a tree = TEmpty | TNode 'a "'a forest" +and 'a forest = FNil | FCons "'a tree" "'a forest" + +datatype_new 'a tree' = TEmpty' | TNode' "'a branch" "'a branch" +and 'a branch = Branch 'a "'a tree'" + +datatype_new ('a, 'b) exp = Term "('a, 'b) trm" | Sum "('a, 'b) trm" "('a, 'b) exp" +and ('a, 'b) trm = Factor "('a, 'b) factor" | Prod "('a, 'b) factor" "('a, 'b) trm" +and ('a, 'b) factor = C 'a | V 'b | Paren "('a, 'b) exp" + +datatype_new ('a, 'b, 'c) some_killing = + SK "'a \ 'b \ ('a, 'b, 'c) some_killing + ('a, 'b, 'c) in_here" +and ('a, 'b, 'c) in_here = + IH1 'b 'a | IH2 'c + +datatype_new 'b nofail1 = NF11 "'b nofail1" 'b | NF12 'b +datatype_new 'b nofail2 = NF2 "('b nofail2 \ 'b \ 'b nofail2 \ 'b) list" +datatype_new 'b nofail3 = NF3 'b "('b nofail3 \ 'b \ 'b nofail3 \ 'b) fset" +datatype_new 'b nofail4 = NF4 "('b nofail4 \ ('b nofail4 \ 'b \ 'b nofail4 \ 'b) fset) list" + +(* +datatype_new 'b fail = F "'b fail" 'b "'b fail" "'b list" +datatype_new 'b fail = F "'b fail" 'b "'b fail" 'b +datatype_new 'b fail = F1 "'b fail" 'b | F2 "'b fail" +datatype_new 'b fail = F "'b fail" 'b +*) + +datatype_new l1 = L1 "l2 list" +and l2 = L21 "l1 fset" | L22 l2 + +datatype_new kk1 = KK1 kk2 +and kk2 = KK2 kk3 +and kk3 = KK3 "kk1 list" + +datatype_new t1 = T11 t3 | T12 t2 +and t2 = T2 t1 +and t3 = T3 + +datatype_new t1' = T11' t2' | T12' t3' +and t2' = T2' t1' +and t3' = T3' + +(* +datatype_new fail1 = F1 fail2 +and fail2 = F2 fail3 +and fail3 = F3 fail1 + +datatype_new fail1 = F1 "fail2 list" fail2 +and fail2 = F2 "fail2 fset" fail3 +and fail3 = F3 fail1 + +datatype_new fail1 = F1 "fail2 list" fail2 +and fail2 = F2 "fail1 fset" fail1 +*) + +(* SLOW +datatype_new ('a, 'c) D1 = A1 "('a, 'c) D2" | B1 "'a list" +and ('a, 'c) D2 = A2 "('a, 'c) D3" | B2 "'c list" +and ('a, 'c) D3 = A3 "('a, 'c) D3" | B3 "('a, 'c) D4" | C3 "('a, 'c) D4" "('a, 'c) D5" +and ('a, 'c) D4 = A4 "('a, 'c) D5" | B4 "'a list list list" +and ('a, 'c) D5 = A5 "('a, 'c) D6" +and ('a, 'c) D6 = A6 "('a, 'c) D7" +and ('a, 'c) D7 = A7 "('a, 'c) D8" +and ('a, 'c) D8 = A8 "('a, 'c) D1 list" + +(*time comparison*) +datatype ('a, 'c) D1' = A1' "('a, 'c) D2'" | B1' "'a list" + and ('a, 'c) D2' = A2' "('a, 'c) D3'" | B2' "'c list" + and ('a, 'c) D3' = A3' "('a, 'c) D3'" | B3' "('a, 'c) D4'" | C3' "('a, 'c) D4'" "('a, 'c) D5'" + and ('a, 'c) D4' = A4' "('a, 'c) D5'" | B4' "'a list list list" + and ('a, 'c) D5' = A5' "('a, 'c) D6'" + and ('a, 'c) D6' = A6' "('a, 'c) D7'" + and ('a, 'c) D7' = A7' "('a, 'c) D8'" + and ('a, 'c) D8' = A8' "('a, 'c) D1' list" +*) + +(* fail: +datatype_new tt1 = TT11 tt2 tt3 | TT12 tt2 tt4 +and tt2 = TT2 +and tt3 = TT3 tt4 +and tt4 = TT4 tt1 +*) + +datatype_new k1 = K11 k2 k3 | K12 k2 k4 +and k2 = K2 +and k3 = K3 k4 +and k4 = K4 + +datatype_new tt1 = TT11 tt3 tt2 | TT12 tt2 tt4 +and tt2 = TT2 +and tt3 = TT3 tt1 +and tt4 = TT4 + +(* SLOW +datatype_new s1 = S11 s2 s3 s4 | S12 s3 | S13 s2 s6 | S14 s4 s2 | S15 s2 s2 +and s2 = S21 s7 s5 | S22 s5 s4 s6 +and s3 = S31 s1 s7 s2 | S32 s3 s3 | S33 s4 s5 +and s4 = S4 s5 +and s5 = S5 +and s6 = S61 s6 | S62 s1 s2 | S63 s6 +and s7 = S71 s8 | S72 s5 +and s8 = S8 nat +*) + +datatype_new 'a deadbar = DeadBar "'a \ 'a" +datatype_new 'a deadbar_option = DeadBarOption "'a option \ 'a option" +datatype_new ('a, 'b) bar = Bar "'b \ 'a" +datatype_new ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \ 'c + 'a" +datatype_new 'a deadfoo = C "'a \ 'a + 'a" + +datatype_new 'a dead_foo = A +datatype_new ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo" + +datatype_new d1 = D +datatype_new d1' = is_D: D + +datatype_new d2 = D nat +datatype_new d2' = is_D: D nat + +datatype_new d3 = D | E +datatype_new d3' = D | is_E: E +datatype_new d3'' = is_D: D | E +datatype_new d3''' = is_D: D | is_E: E + +datatype_new d4 = D nat | E +datatype_new d4' = D nat | is_E: E +datatype_new d4'' = is_D: D nat | E +datatype_new d4''' = is_D: D nat | is_E: E + +datatype_new d5 = D nat | E int +datatype_new d5' = D nat | is_E: E int +datatype_new d5'' = is_D: D nat | E int +datatype_new d5''' = is_D: D nat | is_E: E int + +end diff -r 5f727525b1ac -r bc87b7af4767 src/HOL/ROOT --- a/src/HOL/ROOT Wed Aug 21 09:25:40 2013 +0200 +++ b/src/HOL/ROOT Wed Aug 21 09:25:40 2013 +0200 @@ -729,8 +729,8 @@ "Derivation_Trees/Parallel" Koenig theories [condition = ISABELLE_FULL_TEST] - Misc_Codata - Misc_Data + Misc_Codatatype + Misc_Datatype session "HOL-Word" (main) in Word = HOL + options [document_graph]