added 'datatype_compat' examples/tests
authorblanchet
Tue Apr 08 18:06:21 2014 +0200 (2014-04-08)
changeset 56454e9e82384e5a1
parent 56453 00548d372f02
child 56455 1ff66e72628b
added 'datatype_compat' examples/tests
src/HOL/BNF_Examples/Compat.thy
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/BNF_Examples/Compat.thy	Tue Apr 08 18:06:21 2014 +0200
     1.3 @@ -0,0 +1,79 @@
     1.4 +theory Compat
     1.5 +imports Main
     1.6 +begin
     1.7 +
     1.8 +
     1.9 +datatype_new 'a lst = Nl | Cns 'a "'a lst"
    1.10 +datatype_compat lst
    1.11 +
    1.12 +datatype_new 'b w = W | W' "'b w * 'b list"
    1.13 +(* no support for sums of products
    1.14 +datatype_compat w
    1.15 +*)
    1.16 +
    1.17 +datatype_new ('c, 'b) s = L 'c | R 'b
    1.18 +datatype_new 'd x = X | X' "('d x lst, 'd list) s"
    1.19 +datatype_compat s
    1.20 +datatype_compat x
    1.21 +
    1.22 +datatype_new 'a tttre = TTTre 'a "'a tttre lst lst lst"
    1.23 +datatype_compat tttre
    1.24 +
    1.25 +datatype_new 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst"
    1.26 +datatype_compat ftre
    1.27 +
    1.28 +datatype_new 'a btre = BTre 'a "'a btre lst" "'a btre lst"
    1.29 +datatype_compat btre
    1.30 +
    1.31 +datatype_new 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo"
    1.32 +datatype_compat foo bar
    1.33 +
    1.34 +datatype_new 'a tre = Tre 'a "'a tre lst"
    1.35 +datatype_compat tre
    1.36 +
    1.37 +fun f_tre and f_tres where
    1.38 +  "f_tre (Tre a ts) = {a} \<union> f_tres ts"
    1.39 +| "f_tres Nl = {}"
    1.40 +| "f_tres (Cns t ts) = f_tres ts"
    1.41 +
    1.42 +datatype_new 'a f = F 'a and 'a g = G 'a
    1.43 +datatype_new h = H "h f" | H'
    1.44 +datatype_compat f g
    1.45 +datatype_compat h
    1.46 +
    1.47 +datatype_new myunit = MyUnity
    1.48 +datatype_compat myunit
    1.49 +
    1.50 +datatype_new mylist = MyNil | MyCons nat mylist
    1.51 +datatype_compat mylist
    1.52 +
    1.53 +fun f_mylist where
    1.54 +  "f_mylist MyNil = 0"
    1.55 +| "f_mylist (MyCons _ xs) = Suc (f_mylist xs)"
    1.56 +
    1.57 +datatype_new foo' = FooNil | FooCons bar' foo' and bar' = Bar
    1.58 +(* FIXME
    1.59 +datatype_compat bar' foo'
    1.60 +
    1.61 +fun f_foo and f_bar where
    1.62 +  "f_foo FooNil = 0"
    1.63 +| "f_foo (FooCons bar foo) = Suc (f_foo foo) + f_bar bar"
    1.64 +| "f_bar Bar = Suc 0"
    1.65 +*)
    1.66 +
    1.67 +locale opt begin
    1.68 +
    1.69 +datatype_new 'a opt = Non | Som 'a
    1.70 +datatype_compat opt
    1.71 +
    1.72 +end
    1.73 +
    1.74 +datatype funky = Funky "funky tre" | Funky'
    1.75 +datatype fnky = Fnky "nat tre"
    1.76 +
    1.77 +datatype_new tree = Tree "tree foo"
    1.78 +datatype_compat tree
    1.79 +
    1.80 +ML {* Datatype_Data.get_info @{theory} @{type_name tree} *}
    1.81 +
    1.82 +end
     2.1 --- a/src/HOL/ROOT	Tue Apr 08 17:49:03 2014 +0200
     2.2 +++ b/src/HOL/ROOT	Tue Apr 08 18:06:21 2014 +0200
     2.3 @@ -720,6 +720,7 @@
     2.4    *}
     2.5    options [document = false]
     2.6    theories
     2.7 +    Compat
     2.8      Lambda_Term
     2.9      Process
    2.10      TreeFsetI