author | wenzelm |
Tue, 09 Apr 2013 21:39:55 +0200 | |
changeset 51667 | 354c23ef2784 |
parent 49633 | 5b5450bc544c |
child 51781 | 0504e286d66d |
permissions | -rw-r--r-- |
49509
163914705f8d
renamed top-level theory from "Codatatype" to "BNF"
blanchet
parents:
49486
diff
changeset
|
1 |
(* Title: HOL/BNF/BNF_Wrap.thy |
49486 | 2 |
Author: Jasmin Blanchette, TU Muenchen |
49075 | 3 |
Copyright 2012 |
4 |
||
5 |
Wrapping datatypes. |
|
6 |
*) |
|
7 |
||
8 |
header {* Wrapping Datatypes *} |
|
9 |
||
10 |
theory BNF_Wrap |
|
49283 | 11 |
imports BNF_Util |
49075 | 12 |
keywords |
49286 | 13 |
"wrap_data" :: thy_goal and |
49633 | 14 |
"no_dests" and |
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 |
||
49309
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49286
diff
changeset
|
26 |
ML_file "Tools/bnf_wrap_tactics.ML" |
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49286
diff
changeset
|
27 |
ML_file "Tools/bnf_wrap.ML" |
f20b24214ac2
split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF
blanchet
parents:
49286
diff
changeset
|
28 |
|
49075 | 29 |
end |