isabelle: src/HOL/Library/Case_Converter.thy@a2d22d519bf2 (annotated)

69567 6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	1	(* Author: Pascal Stoop, ETH Zurich
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	2	Author: Andreas Lochbihler, Digital Asset *)
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	3
77811 ae9e6218443d proper section headings haftmann parents: 69605 diff changeset	4	section \<open>Eliminating pattern matches\<close>
ae9e6218443d proper section headings haftmann parents: 69605 diff changeset	5
69567 6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	6	theory Case_Converter
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	7	imports Main
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	8	begin
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	9
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	10	definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	11	[code del]: "missing_pattern_match m f = f ()"
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	12
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	13	lemma missing_pattern_match_cong [cong]:
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	14	"m = m' \<Longrightarrow> missing_pattern_match m f = missing_pattern_match m' f"
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	15	by(rule arg_cong)
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	16
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	17	lemma missing_pattern_match_code [code_unfold]:
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	18	"missing_pattern_match = Code.abort"
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	19	unfolding missing_pattern_match_def Code.abort_def ..
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	20
69605 a96320074298 isabelle update -u path_cartouches; wenzelm parents: 69567 diff changeset	21	ML_file \<open>case_converter.ML\<close>
69567 6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	22
6b4c41037649 separate case converter into a separate theory Andreas Lochbihler parents: diff changeset	23	end

author	wenzelm
	Tue, 18 Jul 2023 12:55:43 +0200
changeset 78393	a2d22d519bf2
parent 77811	ae9e6218443d
permissions	-rw-r--r--