|
(* Title: HOL/Quotient_Examples/Lifting_Code_Dt_Test.thy
Author: Ondrej Kuncar, TU Muenchen
Copyright 2015
Miscellaneous lift_definition(code_dt) definitions (for testing purposes).
*)
theory Lifting_Code_Dt_Test
imports Main
begin
(* basic examples *)
typedef bool2 = "{x. x}" by auto
setup_lifting type_definition_bool2
lift_definition(code_dt) f1 :: "bool2 option" is "Some True" by simp
lift_definition(code_dt) f2 :: "bool2 list" is "[True]" by simp
lift_definition(code_dt) f3 :: "bool2 \ int" is "(True, 42)" by simp
lift_definition(code_dt) f4 :: "int + bool2" is "Inr True" by simp
lift_definition(code_dt) f5 :: "'a \ (bool2 \ 'a) option" is "\x. Some (True, x)" by simp
(* ugly (i.e., sensitive to rewriting done in my tactics) definition of T *)
typedef 'a T = "{ x::'a. \<forall>(y::'a) z::'a. \<exists>(w::'a). (z = z) \<and> eq_onp top y y
\<or> rel_prod (eq_onp top) (eq_onp top) (x, y) (x, y) \<longrightarrow> pred_prod top top (w, w) }"
by auto
setup_lifting type_definition_T
lift_definition(code_dt) f6 :: "bool T option" is "Some True" by simp
lift_definition(code_dt) f7 :: "(bool T \ int) option" is "Some (True, 42)" by simp
lift_definition(code_dt) f8 :: "bool T \ int \ (bool T \ int) option"
is "\x y. if x then Some (x, y) else None" by simp
lift_definition(code_dt) f9 :: "nat \ ((bool T \ int) option) list \ nat"
is "\x. ([Some (True, 42)], x)" by simp
(* complicated nested datatypes *)
(* stolen from Datatype_Examples *)
datatype 'a tree = Empty | Node 'a "'a tree list"
datatype 'a ttree = TEmpty | TNode 'a "'a ttree list tree"
datatype 'a tttree = TEmpty | TNode 'a "'a tttree list ttree list tree"
lift_definition(code_dt) f10 :: "int \ int T tree" is "\i. Node i [Node i Nil, Empty]" by simp
lift_definition(code_dt) f11 :: "int \ int T ttree"
is "\i. ttree.TNode i (Node [ttree.TNode i Empty] [])" by simp
lift_definition(code_dt) f12 :: "int \ int T tttree" is "\i. tttree.TNode i Empty" by simp
(* Phantom type variables *)
datatype 'a phantom = PH1 | PH2
datatype ('a, 'b) phantom2 = PH21 'a | PH22 "'a option"
lift_definition(code_dt) f13 :: "int \ int T phantom" is "\i. PH1" by auto
lift_definition(code_dt) f14 :: "int \ (int T, nat T) phantom2" is "\i. PH22 (Some i)" by auto
(* Mutual datatypes *)
datatype 'a M1 = Empty 'a | CM "'a M2"
and 'a M2 = CM2 "'a M1"
lift_definition(code_dt) f15 :: "int \ int T M1" is "\i. Empty i" by auto
(* Codatatypes *)
codatatype 'a stream = S 'a "'a stream"
primcorec
sconst :: "'a \ 'a stream" where
"sconst a = S a (sconst a)"
lift_definition(code_dt) f16 :: "int \ int T stream" is "\i. sconst i" unfolding pred_stream_def
by auto
(* Sort constraints *)
datatype ('a::finite, 'b::finite) F = F 'a | F2 'b
instance T :: (finite) finite by standard (transfer, auto)
lift_definition(code_dt) f17 :: "bool \ (bool T, 'b::finite) F" is "\b. F b" by auto
export_code f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17
checking SML OCaml? Haskell? Scala?
end
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
