Quelle Ctr_Sugar.thy Sprache: Isabelle

(*  Title:      HOL/Ctr_Sugar.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Author:     Dmitriy Traytel, TU Muenchen
    Copyright   2012, 2013

Wrapping existing freely generated type's constructors.
*)

section \<open>Wrapping Existing Freely Generated Type's Constructors\<close>

theory Ctr_Sugar
imports HOL
keywords
  "print_case_translations" :: diag and
  "free_constructors" :: thy_goal
begin

consts
  case_guard :: "bool \ 'a \ ('a \ 'b) \ 'b"
  case_nil :: "'a \ 'b"
  case_cons :: "('a \ 'b) \ ('a \ 'b) \ 'a \ 'b"
  case_elem :: "'a \ 'b \ 'a \ 'b"
  case_abs :: "('c \ 'b) \ 'b"

declare [[coercion_args case_guard - + -]]
declare [[coercion_args case_cons - -]]
declare [[coercion_args case_abs -]]
declare [[coercion_args case_elem - +]]

ML_file \<open>Tools/Ctr_Sugar/case_translation.ML\<close>

lemma iffI_np: "\x \ \ y; \ x \ y\ \ \ x \ y"
  by (erule iffI) (erule contrapos_pn)

lemma iff_contradict:
  "\ P \ P \ Q \ Q \ R"
  "\ Q \ P \ Q \ P \ R"
  by blast+

ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_util.ML\<close>
ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_tactics.ML\<close>
ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_code.ML\<close>
ML_file \<open>Tools/Ctr_Sugar/ctr_sugar.ML\<close>

text \<open>Coinduction method that avoids some boilerplate compared with coinduct.\<close>

ML_file \<open>Tools/coinduction.ML\<close>

end

quality100%

¤ Dauer der Verarbeitung: 0.1 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.