src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy
 author haftmann Sun Oct 08 22:28:22 2017 +0200 (23 months ago) changeset 66816 212a3334e7da parent 61169 4de9ff3ea29a permissions -rw-r--r--
more fundamental definition of div and mod on int
```     1 (*  Title:      HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy
```
```     2     Author:     Ondrej Kuncar, TU Muenchen
```
```     3     Copyright   2015
```
```     4
```
```     5 Miscellaneous lift_definition(code_dt) definitions (for testing purposes).
```
```     6 *)
```
```     7
```
```     8 theory Lifting_Code_Dt_Test
```
```     9 imports Main
```
```    10 begin
```
```    11
```
```    12 (* basic examples *)
```
```    13
```
```    14 typedef bool2 = "{x. x}" by auto
```
```    15
```
```    16 setup_lifting type_definition_bool2
```
```    17
```
```    18 lift_definition(code_dt) f1 :: "bool2 option" is "Some True" by simp
```
```    19
```
```    20 lift_definition(code_dt) f2 :: "bool2 list" is "[True]" by simp
```
```    21
```
```    22 lift_definition(code_dt) f3 :: "bool2 \<times> int" is "(True, 42)" by simp
```
```    23
```
```    24 lift_definition(code_dt) f4 :: "int + bool2" is "Inr True" by simp
```
```    25
```
```    26 lift_definition(code_dt) f5 :: "'a \<Rightarrow> (bool2 \<times> 'a) option" is "\<lambda>x. Some (True, x)" by simp
```
```    27
```
```    28 (* ugly (i.e., sensitive to rewriting done in my tactics) definition of T *)
```
```    29
```
```    30 typedef 'a T = "{ x::'a. \<forall>(y::'a) z::'a. \<exists>(w::'a). (z = z) \<and> eq_onp top y y
```
```    31   \<or> rel_prod (eq_onp top) (eq_onp top) (x, y) (x, y) \<longrightarrow> pred_prod top top (w, w) }"
```
```    32   by auto
```
```    33
```
```    34 setup_lifting type_definition_T
```
```    35
```
```    36 lift_definition(code_dt) f6 :: "bool T option" is "Some True" by simp
```
```    37
```
```    38 lift_definition(code_dt) f7 :: "(bool T \<times> int) option" is "Some (True, 42)" by simp
```
```    39
```
```    40 lift_definition(code_dt) f8 :: "bool T \<Rightarrow> int \<Rightarrow> (bool T \<times> int) option"
```
```    41   is "\<lambda>x y. if x then Some (x, y) else None" by simp
```
```    42
```
```    43 lift_definition(code_dt) f9 :: "nat \<Rightarrow> ((bool T \<times> int) option) list \<times> nat"
```
```    44   is "\<lambda>x. ([Some (True, 42)], x)" by simp
```
```    45
```
```    46 (* complicated nested datatypes *)
```
```    47
```
```    48 (* stolen from Datatype_Examples *)
```
```    49 datatype 'a tree = Empty | Node 'a "'a tree list"
```
```    50
```
```    51 datatype 'a ttree = TEmpty | TNode 'a "'a ttree list tree"
```
```    52
```
```    53 datatype 'a tttree = TEmpty | TNode 'a "'a tttree list ttree list tree"
```
```    54
```
```    55 lift_definition(code_dt) f10 :: "int \<Rightarrow> int T tree" is "\<lambda>i. Node i [Node i Nil, Empty]" by simp
```
```    56
```
```    57 lift_definition(code_dt) f11 :: "int \<Rightarrow> int T ttree"
```
```    58   is "\<lambda>i. ttree.TNode i (Node [ttree.TNode i Empty] [])" by simp
```
```    59
```
```    60 lift_definition(code_dt) f12 :: "int \<Rightarrow> int T tttree" is "\<lambda>i. tttree.TNode i Empty" by simp
```
```    61
```
```    62 (* Phantom type variables *)
```
```    63
```
```    64 datatype 'a phantom = PH1 | PH2
```
```    65
```
```    66 datatype ('a, 'b) phantom2 = PH21 'a | PH22 "'a option"
```
```    67
```
```    68 lift_definition(code_dt) f13 :: "int \<Rightarrow> int T phantom" is "\<lambda>i. PH1" by auto
```
```    69
```
```    70 lift_definition(code_dt) f14 :: "int \<Rightarrow> (int T, nat T) phantom2" is "\<lambda>i. PH22 (Some i)" by auto
```
```    71
```
```    72 (* Mutual datatypes *)
```
```    73
```
```    74 datatype 'a M1 = Empty 'a | CM "'a M2"
```
```    75 and 'a M2 = CM2 "'a M1"
```
```    76
```
```    77 lift_definition(code_dt) f15 :: "int \<Rightarrow> int T M1" is "\<lambda>i. Empty i" by auto
```
```    78
```
```    79 (* Codatatypes *)
```
```    80
```
```    81 codatatype 'a stream = S 'a "'a stream"
```
```    82
```
```    83 primcorec
```
```    84   sconst :: "'a \<Rightarrow> 'a stream" where
```
```    85   "sconst a = S a (sconst a)"
```
```    86
```
```    87 lift_definition(code_dt) f16 :: "int \<Rightarrow> int T stream" is "\<lambda>i. sconst i"  unfolding pred_stream_def
```
```    88 by auto
```
```    89
```
```    90 (* Sort constraints *)
```
```    91
```
```    92 datatype ('a::finite, 'b::finite) F = F 'a | F2 'b
```
```    93
```
```    94 instance T :: (finite) finite by standard (transfer, auto)
```
```    95
```
```    96 lift_definition(code_dt) f17 :: "bool \<Rightarrow> (bool T, 'b::finite) F" is "\<lambda>b. F b" by auto
```
```    97
```
```    98 export_code f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17
```
```    99   checking SML OCaml? Haskell? Scala?
```
```   100
```
```   101 end
```