1(* Title: HOL/Ctr_Sugar.thy 2 Author: Jasmin Blanchette, TU Muenchen 3 Author: Dmitriy Traytel, TU Muenchen 4 Copyright 2012, 2013 5 6Wrapping existing freely generated type's constructors. 7*) 8 9section \<open>Wrapping Existing Freely Generated Type's Constructors\<close> 10 11theory Ctr_Sugar 12imports HOL 13keywords 14 "print_case_translations" :: diag and 15 "free_constructors" :: thy_goal 16begin 17 18consts 19 case_guard :: "bool \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" 20 case_nil :: "'a \<Rightarrow> 'b" 21 case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" 22 case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b" 23 case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b" 24 25declare [[coercion_args case_guard - + -]] 26declare [[coercion_args case_cons - -]] 27declare [[coercion_args case_abs -]] 28declare [[coercion_args case_elem - +]] 29 30ML_file "Tools/Ctr_Sugar/case_translation.ML" 31 32lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y" 33 by (erule iffI) (erule contrapos_pn) 34 35lemma iff_contradict: 36 "\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R" 37 "\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R" 38 by blast+ 39 40ML_file "Tools/Ctr_Sugar/ctr_sugar_util.ML" 41ML_file "Tools/Ctr_Sugar/ctr_sugar_tactics.ML" 42ML_file "Tools/Ctr_Sugar/ctr_sugar_code.ML" 43ML_file "Tools/Ctr_Sugar/ctr_sugar.ML" 44 45text \<open>Coinduction method that avoids some boilerplate compared with coinduct.\<close> 46 47ML_file "Tools/coinduction.ML" 48 49end 50