isabelle: src/HOL/Ctr_Sugar.thy@0604d3051eee (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
55160 2d69438b1b0c added Dmitriy, since he did the case syntax blanchet parents: 54701 diff changeset	3	Author: Dmitriy Traytel, TU Muenchen
54397 f4b4fa25ce56 tuned headers blanchet parents: 54396 diff changeset	4	Copyright 2012, 2013
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	5
51797 182454c06a80 tuned ML and thy file names blanchet parents: 51781 diff changeset	6	Wrapping existing freely generated type's constructors.
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	7	*)
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	8
60758 d8d85a8172b5 isabelle update_cartouches; wenzelm parents: 58889 diff changeset	9	section \<open>Wrapping Existing Freely Generated Type's Constructors\<close>
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	10
54006 9fe1bd54d437 renamed theory file blanchet parents: 52969 diff changeset	11	theory Ctr_Sugar
54398 100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it blanchet parents: 54397 diff changeset	12	imports HOL
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	13	keywords
54398 100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it blanchet parents: 54397 diff changeset	14	"print_case_translations" :: diag and
55468 98b25c51e9e5 renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.) blanchet parents: 55160 diff changeset	15	"free_constructors" :: thy_goal
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	16	begin
ed769978dc8d rearrange dependencies blanchet parents: diff changeset	17
54398 100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it blanchet parents: 54397 diff changeset	18	consts
100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it blanchet parents: 54397 diff changeset	19	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	20	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	21	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	22	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	23	case_abs :: "('c \<Rightarrow> 'b) \<Rightarrow> 'b"
57631 959caab43a3d use the noted theorem whenever possible, also in 'BNF_Def' blanchet parents: 55971 diff changeset	24
54398 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
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 64430 diff changeset	30	ML_file \<open>Tools/Ctr_Sugar/case_translation.ML\<close>
54398 100c0eaf63d5 moved 'Ctr_Sugar' further up the theory hierarchy, so that 'Datatype' can use it blanchet parents: 54397 diff changeset	31
49312 c874ff5658dc moved theorems closer to where they are used blanchet parents: 49309 diff changeset	32	lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
58188 cc71d2be4f0a introduced mechanism to filter interpretations blanchet parents: 58177 diff changeset	33	by (erule iffI) (erule contrapos_pn)
49312 c874ff5658dc moved theorems closer to where they are used blanchet parents: 49309 diff changeset	34
49486 64cc57c0d0fe generate "expand" property blanchet parents: 49312 diff changeset	35	lemma iff_contradict:
58188 cc71d2be4f0a introduced mechanism to filter interpretations blanchet parents: 58177 diff changeset	36	"\<not> P \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> Q \<Longrightarrow> R"
cc71d2be4f0a introduced mechanism to filter interpretations blanchet parents: 58177 diff changeset	37	"\<not> Q \<Longrightarrow> P \<longleftrightarrow> Q \<Longrightarrow> P \<Longrightarrow> R"
cc71d2be4f0a introduced mechanism to filter interpretations blanchet parents: 58177 diff changeset	38	by blast+
49486 64cc57c0d0fe generate "expand" property blanchet parents: 49312 diff changeset	39
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 64430 diff changeset	40	ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_util.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 64430 diff changeset	41	ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_tactics.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 64430 diff changeset	42	ML_file \<open>Tools/Ctr_Sugar/ctr_sugar_code.ML\<close>
a96320074298 isabelle update -u path_cartouches; wenzelm parents: 64430 diff changeset	43	ML_file \<open>Tools/Ctr_Sugar/ctr_sugar.ML\<close>
49309 f20b24214ac2 split basic BNFs into really basic ones and others, and added Andreas Lochbihler's "option" BNF blanchet parents: 49286 diff changeset	44
64430 1d85ac286c72 avoid code generator warnings when deleting equations in BNF commands (e.g., datatype) in locales with assumptions and similar blanchet parents: 63655 diff changeset	45	text \<open>Coinduction method that avoids some boilerplate compared with coinduct.\<close>
63655 d31650b377c4 simplified theory hierarchy; wenzelm parents: 60758 diff changeset	46
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 64430 diff changeset	47	ML_file \<open>Tools/coinduction.ML\<close>
63655 d31650b377c4 simplified theory hierarchy; wenzelm parents: 60758 diff changeset	48
49075 ed769978dc8d rearrange dependencies blanchet parents: diff changeset	49	end

author	nipkow
	Wed, 29 May 2024 18:13:05 +0200
changeset 80208	0604d3051eee
parent 69605	a96320074298
permissions	-rw-r--r--