isabelle: src/HOL/BNF/BNF_Ctr_Sugar.thy@182454c06a80 (annotated)

51797 182454c06a80 tuned ML and thy file names blanchet parents: 51781 diff changeset	1	(* Title: HOL/BNF/BNF_Ctr_Sugar.thy
49486 64cc57c0d0fe generate "expand" property blanchet parents: 49312 diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	3	Copyright 2012
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	4
51797 182454c06a80 tuned ML and thy file names blanchet parents: 51781 diff changeset	5	Wrapping existing freely generated type's constructors.
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	6	*)
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	7
51797 182454c06a80 tuned ML and thy file names blanchet parents: 51781 diff changeset	8	header {* Wrapping Existing Freely Generated Type's Constructors *}
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	9
51797 182454c06a80 tuned ML and thy file names blanchet parents: 51781 diff changeset	10	theory BNF_Ctr_Sugar
49283 97809ae5f7bb move "bnf_util.ML" to "BNF_Util.thy" blanchet parents: 49278 diff changeset	11	imports BNF_Util
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	12	keywords
51781 0504e286d66d renamed "wrap_data" to "wrap_free_constructors" blanchet parents: 49633 diff changeset	13	"wrap_free_constructors" :: thy_goal and
49633 5b5450bc544c compatibility option to use "rep_datatype" blanchet parents: 49510 diff changeset	14	"no_dests" and
5b5450bc544c compatibility option to use "rep_datatype" blanchet parents: 49510 diff changeset	15	"rep_compat"
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	16	begin
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	17
49312 c874ff5658dc moved theorems closer to where they are used blanchet parents: 49309 diff changeset	18	lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
c874ff5658dc moved theorems closer to where they are used blanchet parents: 49309 diff changeset	19	by (erule iffI) (erule contrapos_pn)
c874ff5658dc moved theorems closer to where they are used blanchet parents: 49309 diff changeset	20
49486 64cc57c0d0fe generate "expand" property blanchet parents: 49312 diff changeset	21	lemma iff_contradict:
64cc57c0d0fe generate "expand" property blanchet parents: 49312 diff changeset	22	"\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
64cc57c0d0fe generate "expand" property blanchet parents: 49312 diff changeset	23	"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
64cc57c0d0fe generate "expand" property blanchet parents: 49312 diff changeset	24	by blast+
64cc57c0d0fe generate "expand" property blanchet parents: 49312 diff changeset	25
51797 182454c06a80 tuned ML and thy file names blanchet parents: 51781 diff changeset	26	ML_file "Tools/bnf_ctr_sugar_tactics.ML"
182454c06a80 tuned ML and thy file names blanchet parents: 51781 diff changeset	27	ML_file "Tools/bnf_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	28
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	29	end

author	blanchet
	Sat, 27 Apr 2013 11:37:50 +0200
changeset 51797	182454c06a80
parent 51781	src/HOL/BNF/BNF_Wrap.thy@0504e286d66d
child 52969	f2df0730f8ac
permissions	-rw-r--r--