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