src/HOL/BNF_Examples/Compat.thy
author blanchet
Tue, 08 Apr 2014 18:06:21 +0200
changeset 56454 e9e82384e5a1
child 56455 1ff66e72628b
permissions -rw-r--r--
added 'datatype_compat' examples/tests
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56454
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
     1
theory Compat
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
     2
imports Main
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
     3
begin
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
     4
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
     5
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
     6
datatype_new 'a lst = Nl | Cns 'a "'a lst"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
     7
datatype_compat lst
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
     8
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
     9
datatype_new 'b w = W | W' "'b w * 'b list"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    10
(* no support for sums of products
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    11
datatype_compat w
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    12
*)
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    13
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    14
datatype_new ('c, 'b) s = L 'c | R 'b
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    15
datatype_new 'd x = X | X' "('d x lst, 'd list) s"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    16
datatype_compat s
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    17
datatype_compat x
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    18
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    19
datatype_new 'a tttre = TTTre 'a "'a tttre lst lst lst"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    20
datatype_compat tttre
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    21
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    22
datatype_new 'a ftre = FEmp | FTre "'a \<Rightarrow> 'a ftre lst"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    23
datatype_compat ftre
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    24
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    25
datatype_new 'a btre = BTre 'a "'a btre lst" "'a btre lst"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    26
datatype_compat btre
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    27
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    28
datatype_new 'a foo = Foo | Foo' 'a "'a bar" and 'a bar = Bar | Bar' 'a "'a foo"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    29
datatype_compat foo bar
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    30
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    31
datatype_new 'a tre = Tre 'a "'a tre lst"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    32
datatype_compat tre
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    33
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    34
fun f_tre and f_tres where
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    35
  "f_tre (Tre a ts) = {a} \<union> f_tres ts"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    36
| "f_tres Nl = {}"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    37
| "f_tres (Cns t ts) = f_tres ts"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    38
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    39
datatype_new 'a f = F 'a and 'a g = G 'a
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    40
datatype_new h = H "h f" | H'
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    41
datatype_compat f g
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    42
datatype_compat h
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    43
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    44
datatype_new myunit = MyUnity
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    45
datatype_compat myunit
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    46
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    47
datatype_new mylist = MyNil | MyCons nat mylist
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    48
datatype_compat mylist
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    49
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    50
fun f_mylist where
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    51
  "f_mylist MyNil = 0"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    52
| "f_mylist (MyCons _ xs) = Suc (f_mylist xs)"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    53
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    54
datatype_new foo' = FooNil | FooCons bar' foo' and bar' = Bar
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    55
(* FIXME
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    56
datatype_compat bar' foo'
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    57
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    58
fun f_foo and f_bar where
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    59
  "f_foo FooNil = 0"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    60
| "f_foo (FooCons bar foo) = Suc (f_foo foo) + f_bar bar"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    61
| "f_bar Bar = Suc 0"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    62
*)
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    63
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    64
locale opt begin
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    65
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    66
datatype_new 'a opt = Non | Som 'a
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    67
datatype_compat opt
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    68
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    69
end
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    70
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    71
datatype funky = Funky "funky tre" | Funky'
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    72
datatype fnky = Fnky "nat tre"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    73
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    74
datatype_new tree = Tree "tree foo"
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    75
datatype_compat tree
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    76
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    77
ML {* Datatype_Data.get_info @{theory} @{type_name tree} *}
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    78
e9e82384e5a1 added 'datatype_compat' examples/tests
blanchet
parents:
diff changeset
    79
end