(* 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. \<open>Wrapping Existing Freely Generated Type's Constructors\<close> theory Ctr_Sugarimports HOL"print_case_translations" :: diag and "free_constructors" :: thy_goalbegin consts "bool \ 'a \ ('a \ 'b) \ 'b" "'a \ 'b" "('a \ 'b) \ ('a \ 'b) \ 'a \ 'b" "'a \ 'b \ 'a \ 'b" "('c \ 'b) \ 'b" declare [[coercion_args case_guard - + -]]declare [[coercion_args case_cons - -]]declare [[coercion_args case_abs -]]declare [[coercion_args case_elem - +]]\<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+\<open>Tools/Ctr_Sugar/ctr_sugar_util.ML\<close> \<open>Tools/Ctr_Sugar/ctr_sugar_tactics.ML\<close> \<open>Tools/Ctr_Sugar/ctr_sugar_code.ML\<close> \<open>Tools/Ctr_Sugar/ctr_sugar.ML\<close> text \<open>Coinduction method that avoids some boilerplate compared with coinduct.\<close> \<open>Tools/coinduction.ML\<close> end quality 100%
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
