author | blanchet |
Mon, 02 Dec 2013 20:31:54 +0100 | |
changeset 54615 | 62fb5af93fe2 |
parent 54398 | 100c0eaf63d5 |
child 54626 | 8a5e82425e55 |
permissions | -rw-r--r-- |
54397 | 1 |
(* Title: HOL/Ctr_Sugar.thy |
49486 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
54397 | 3 |
Copyright 2012, 2013 |
49075 | 4 |
|
51797 | 5 |
Wrapping existing freely generated type's constructors. |
49075 | 6 |
*) |
7 |
||
51797 | 8 |
header {* Wrapping Existing Freely Generated Type's Constructors *} |
49075 | 9 |
|
54006 | 10 |
theory Ctr_Sugar |
54398
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
11 |
imports HOL |
49075 | 12 |
keywords |
54398
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
13 |
"print_case_translations" :: diag and |
51781 | 14 |
"wrap_free_constructors" :: thy_goal and |
52969
f2df0730f8ac
clarified option name (since case/fold/rec are also destructors)
blanchet
parents:
51797
diff
changeset
|
15 |
"no_discs_sels" and |
49633 | 16 |
"rep_compat" |
49075 | 17 |
begin |
18 |
||
54398
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
19 |
consts |
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
20 |
case_guard :: "bool \<Rightarrow> 'a \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b" |
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
21 |
case_nil :: "'a \<Rightarrow> 'b" |
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
22 |
case_cons :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
23 |
case_elem :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b" |
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
24 |
case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b" |
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
25 |
declare [[coercion_args case_guard - + -]] |
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
26 |
declare [[coercion_args case_cons - -]] |
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
27 |
declare [[coercion_args case_abs -]] |
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
28 |
declare [[coercion_args case_elem - +]] |
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
29 |
|
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
30 |
ML_file "Tools/case_translation.ML" |
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
31 |
setup Case_Translation.setup |
100c0eaf63d5
moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it
blanchet
parents:
54397
diff
changeset
|
32 |
|
49312 | 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 |
||
49486 | 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 |
||
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
41 |
ML_file "Tools/ctr_sugar_util.ML" |
54007 | 42 |
ML_file "Tools/ctr_sugar_tactics.ML" |
54615
62fb5af93fe2
generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local)
blanchet
parents:
54398
diff
changeset
|
43 |
ML_file "Tools/ctr_sugar_code.ML" |
54007 | 44 |
ML_file "Tools/ctr_sugar.ML" |
49309
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49286
diff
changeset
|
45 |
|
49075 | 46 |
end |