author | blanchet |
Tue, 01 Oct 2013 14:05:25 +0200 | |
changeset 54008 | b15cfc2864de |
parent 54007 | 07028b08045f |
permissions | -rw-r--r-- |
54006 | 1 |
(* Title: HOL/BNF/Ctr_Sugar.thy |
49486 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
49075 | 3 |
Copyright 2012 |
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 |
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
11 |
imports Main |
49075 | 12 |
keywords |
51781 | 13 |
"wrap_free_constructors" :: thy_goal and |
52969
f2df0730f8ac
clarified option name (since case/fold/rec are also destructors)
blanchet
parents:
51797
diff
changeset
|
14 |
"no_discs_sels" and |
49633 | 15 |
"rep_compat" |
49075 | 16 |
begin |
17 |
||
49312 | 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 |
||
49486 | 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 |
||
54008
b15cfc2864de
refactoring -- splitting between constructor sugar dependencies and true BNF dependencies
blanchet
parents:
54007
diff
changeset
|
26 |
ML_file "Tools/ctr_sugar_util.ML" |
54007 | 27 |
ML_file "Tools/ctr_sugar_tactics.ML" |
28 |
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
|
29 |
|
49075 | 30 |
end |