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