src/HOL/Ctr_Sugar.thy
author blanchet
Mon Dec 09 09:44:57 2013 +0100 (2013-12-09)
changeset 54701 4ed7454aebde
parent 54626 8a5e82425e55
child 55160 2d69438b1b0c
permissions -rw-r--r--
tuning -- moved ML files to subdirectory
     1 (*  Title:      HOL/Ctr_Sugar.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2012, 2013
     4 
     5 Wrapping existing freely generated type's constructors.
     6 *)
     7 
     8 header {* Wrapping Existing Freely Generated Type's Constructors *}
     9 
    10 theory Ctr_Sugar
    11 imports HOL
    12 keywords
    13   "print_case_translations" :: diag and
    14   "wrap_free_constructors" :: thy_goal
    15 begin
    16 
    17 consts
    18   case_guard :: "bool \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
    19   case_nil :: "'a \<Rightarrow> 'b"
    20   case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    21   case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
    22   case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
    23 declare [[coercion_args case_guard - + -]]
    24 declare [[coercion_args case_cons - -]]
    25 declare [[coercion_args case_abs -]]
    26 declare [[coercion_args case_elem - +]]
    27 
    28 ML_file "Tools/Ctr_Sugar/case_translation.ML"
    29 setup Case_Translation.setup
    30 
    31 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    32 by (erule iffI) (erule contrapos_pn)
    33 
    34 lemma iff_contradict:
    35 "\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
    36 "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
    37 by blast+
    38 
    39 ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML"
    40 ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML"
    41 ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML"
    42 ML_file "Tools/Ctr_Sugar/ctr_sugar.ML"
    43 
    44 end