src/HOL/Ctr_Sugar.thy
author blanchet
Tue Nov 12 13:47:24 2013 +0100 (2013-11-12)
changeset 54398 100c0eaf63d5
parent 54397 f4b4fa25ce56
child 54615 62fb5af93fe2
permissions -rw-r--r--
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
     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 and
    15   "no_discs_sels" and
    16   "rep_compat"
    17 begin
    18 
    19 consts
    20   case_guard :: "bool \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b"
    21   case_nil :: "'a \<Rightarrow> 'b"
    22   case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
    23   case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b"
    24   case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
    25 declare [[coercion_args case_guard - + -]]
    26 declare [[coercion_args case_cons - -]]
    27 declare [[coercion_args case_abs -]]
    28 declare [[coercion_args case_elem - +]]
    29 
    30 ML_file "Tools/case_translation.ML"
    31 setup Case_Translation.setup
    32 
    33 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    34 by (erule iffI) (erule contrapos_pn)
    35 
    36 lemma iff_contradict:
    37 "\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
    38 "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
    39 by blast+
    40 
    41 ML_file "Tools/ctr_sugar_util.ML"
    42 ML_file "Tools/ctr_sugar_tactics.ML"
    43 ML_file "Tools/ctr_sugar.ML"
    44 
    45 end