|
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 (default, 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 |