add testing file for code_dt extension of lifting
authorkuncar
Sat May 02 13:58:06 2015 +0200 (2015-05-02)
changeset 60237d47387d4a3c6
parent 60236 865741686926
child 60238 52d02564242a
add testing file for code_dt extension of lifting
src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy
src/HOL/ROOT
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy	Sat May 02 13:58:06 2015 +0200
     1.3 @@ -0,0 +1,101 @@
     1.4 +(*  Title:      HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy
     1.5 +    Author:     Ondrej Kuncar, TU Muenchen
     1.6 +    Copyright   2015
     1.7 +
     1.8 +Miscellaneous lift_definition(code_dt) definitions (for testing purposes).
     1.9 +*)
    1.10 +
    1.11 +theory Lifting_Code_Dt_Test
    1.12 +imports Main
    1.13 +begin
    1.14 +
    1.15 +(* basic examples *)
    1.16 +
    1.17 +typedef bool2 = "{x. x}" by auto
    1.18 +
    1.19 +setup_lifting type_definition_bool2
    1.20 +
    1.21 +lift_definition(code_dt) f1 :: "bool2 option" is "Some True" by simp
    1.22 +
    1.23 +lift_definition(code_dt) f2 :: "bool2 list" is "[True]" by simp
    1.24 +
    1.25 +lift_definition(code_dt) f3 :: "bool2 \<times> int" is "(True, 42)" by simp
    1.26 +
    1.27 +lift_definition(code_dt) f4 :: "int + bool2" is "Inr True" by simp
    1.28 +
    1.29 +lift_definition(code_dt) f5 :: "'a \<Rightarrow> (bool2 \<times> 'a) option" is "\<lambda>x. Some (True, x)" by simp
    1.30 +
    1.31 +(* ugly (i.e., sensitive to rewriting done in my tactics) definition of T *)
    1.32 +
    1.33 +typedef 'a T = "{ x::'a. \<forall>(y::'a) z::'a. \<exists>(w::'a). (z = z) \<and> eq_onp top y y 
    1.34 +  \<or> rel_prod (eq_onp top) (eq_onp top) (x, y) (x, y) \<longrightarrow> pred_prod top top (w, w) }"
    1.35 +  by auto
    1.36 +
    1.37 +setup_lifting type_definition_T
    1.38 +
    1.39 +lift_definition(code_dt) f6 :: "bool T option" is "Some True" by simp
    1.40 +
    1.41 +lift_definition(code_dt) f7 :: "(bool T \<times> int) option" is "Some (True, 42)" by simp
    1.42 +
    1.43 +lift_definition(code_dt) f8 :: "bool T \<Rightarrow> int \<Rightarrow> (bool T \<times> int) option" 
    1.44 +  is "\<lambda>x y. if x then Some (x, y) else None" by simp
    1.45 +
    1.46 +lift_definition(code_dt) f9 :: "nat \<Rightarrow> ((bool T \<times> int) option) list \<times> nat" 
    1.47 +  is "\<lambda>x. ([Some (True, 42)], x)" by simp
    1.48 +
    1.49 +(* complicated nested datatypes *)
    1.50 +
    1.51 +(* stolen from Datatype_Examples *)
    1.52 +datatype 'a tree = Empty | Node 'a "'a tree list"
    1.53 +
    1.54 +datatype 'a ttree = TEmpty | TNode 'a "'a ttree list tree"
    1.55 +
    1.56 +datatype 'a tttree = TEmpty | TNode 'a "'a tttree list ttree list tree"
    1.57 +
    1.58 +lift_definition(code_dt) f10 :: "int \<Rightarrow> int T tree" is "\<lambda>i. Node i [Node i Nil, Empty]" by simp
    1.59 +
    1.60 +lift_definition(code_dt) f11 :: "int \<Rightarrow> int T ttree" 
    1.61 +  is "\<lambda>i. ttree.TNode i (Node [ttree.TNode i Empty] [])" by simp
    1.62 +
    1.63 +lift_definition(code_dt) f12 :: "int \<Rightarrow> int T tttree" is "\<lambda>i. tttree.TNode i Empty" by simp
    1.64 +
    1.65 +(* Phantom type variables *)
    1.66 +
    1.67 +datatype 'a phantom = PH1 | PH2 
    1.68 +
    1.69 +datatype ('a, 'b) phantom2 = PH21 'a | PH22 "'a option"
    1.70 +
    1.71 +lift_definition(code_dt) f13 :: "int \<Rightarrow> int T phantom" is "\<lambda>i. PH1" by auto
    1.72 +
    1.73 +lift_definition(code_dt) f14 :: "int \<Rightarrow> (int T, nat T) phantom2" is "\<lambda>i. PH22 (Some i)" by auto
    1.74 +
    1.75 +(* Mutual datatypes *)
    1.76 +
    1.77 +datatype 'a M1 = Empty 'a | CM "'a M2"
    1.78 +and 'a M2 = CM2 "'a M1"
    1.79 +
    1.80 +lift_definition(code_dt) f15 :: "int \<Rightarrow> int T M1" is "\<lambda>i. Empty i" by auto
    1.81 +
    1.82 +(* Codatatypes *)
    1.83 +
    1.84 +codatatype 'a stream = S 'a "'a stream"
    1.85 +
    1.86 +primcorec 
    1.87 +  sconst :: "'a \<Rightarrow> 'a stream" where
    1.88 +  "sconst a = S a (sconst a)"
    1.89 +
    1.90 +lift_definition(code_dt) f16 :: "int \<Rightarrow> int T stream" is "\<lambda>i. sconst i"  unfolding pred_stream_def
    1.91 +by auto
    1.92 +
    1.93 +(* Sort constraints *)
    1.94 +
    1.95 +datatype ('a::finite, 'b::finite) F = F 'a | F2 'b
    1.96 +
    1.97 +instance T :: (finite) finite by (default, transfer, auto)
    1.98 +
    1.99 +lift_definition(code_dt) f17 :: "bool \<Rightarrow> (bool T, 'b::finite) F" is "\<lambda>b. F b" by auto
   1.100 +
   1.101 +export_code f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 
   1.102 +  checking SML OCaml? Haskell? Scala? 
   1.103 +
   1.104 +end
     2.1 --- a/src/HOL/ROOT	Sat May 02 13:58:06 2015 +0200
     2.2 +++ b/src/HOL/ROOT	Sat May 02 13:58:06 2015 +0200
     2.3 @@ -962,6 +962,7 @@
     2.4      Quotient_Rat
     2.5      Lift_DList
     2.6      Int_Pow
     2.7 +    Lifting_Code_Dt_Test
     2.8  
     2.9  session "HOL-Predicate_Compile_Examples" in Predicate_Compile_Examples = HOL +
    2.10    options [document = false]