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