src/HOL/BNF/Ctr_Sugar.thy
author blanchet
Tue Oct 01 14:05:25 2013 +0200 (2013-10-01)
changeset 54007 07028b08045f
parent 54006 9fe1bd54d437
child 54008 b15cfc2864de
permissions -rw-r--r--
renamed ML files
     1 (*  Title:      HOL/BNF/Ctr_Sugar.thy
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2012
     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 BNF_Util
    12 keywords
    13   "wrap_free_constructors" :: thy_goal and
    14   "no_discs_sels" and
    15   "rep_compat"
    16 begin
    17 
    18 lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
    19 by (erule iffI) (erule contrapos_pn)
    20 
    21 lemma iff_contradict:
    22 "\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
    23 "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
    24 by blast+
    25 
    26 ML_file "Tools/ctr_sugar_tactics.ML"
    27 ML_file "Tools/ctr_sugar.ML"
    28 
    29 end