isabelle: src/HOL/Ctr_Sugar.thy@62fb5af93fe2 (annotated)

54397 f4b4fa25ce56 tuned headers blanchet parents: 54396 diff changeset	1	(* Title: HOL/Ctr_Sugar.thy
49486 64cc57c0d0fe generate "expand" property blanchet parents: 49312 diff changeset	2	Author: Jasmin Blanchette, TU Muenchen
54397 f4b4fa25ce56 tuned headers blanchet parents: 54396 diff changeset	3	Copyright 2012, 2013
49075 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
54006 9fe1bd54d437 renamed theory file blanchet parents: 52969 diff changeset	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 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	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 0504e286d66d renamed "wrap_data" to "wrap_free_constructors" blanchet parents: 49633 diff changeset	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 5b5450bc544c compatibility option to use "rep_datatype" blanchet parents: 49510 diff changeset	16	"rep_compat"
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	17	begin
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	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 c874ff5658dc moved theorems closer to where they are used blanchet parents: 49309 diff changeset	33	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	34	by (erule iffI) (erule contrapos_pn)
c874ff5658dc moved theorems closer to where they are used blanchet parents: 49309 diff changeset	35
49486 64cc57c0d0fe generate "expand" property blanchet parents: 49312 diff changeset	36	lemma iff_contradict:
64cc57c0d0fe generate "expand" property blanchet parents: 49312 diff changeset	37	"\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
64cc57c0d0fe generate "expand" property blanchet parents: 49312 diff changeset	38	"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
64cc57c0d0fe generate "expand" property blanchet parents: 49312 diff changeset	39	by blast+
64cc57c0d0fe generate "expand" property blanchet parents: 49312 diff changeset	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 07028b08045f renamed ML files blanchet parents: 54006 diff changeset	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 07028b08045f renamed ML files blanchet parents: 54006 diff changeset	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 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	46	end

author	blanchet
	Mon, 02 Dec 2013 20:31:54 +0100
changeset 54615	62fb5af93fe2
parent 54398	100c0eaf63d5
child 54626	8a5e82425e55
permissions	-rw-r--r--