Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Quotient_Examples/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 3 kB

Quelle Lifting_Code_Dt_Test.thy Sprache: Isabelle

(*  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

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.