Theory HOL-Library.Case_Converter

(* Author: Pascal Stoop, ETH Zurich
   Author: Andreas Lochbihler, Digital Asset *)

section ‹Eliminating pattern matches›

theory Case_Converter
  imports Main
begin

definition missing_pattern_match :: "String.literal ⇒ (unit ⇒ 'a) ⇒ 'a" where
  [code del]: "missing_pattern_match m f = f ()"

lemma missing_pattern_match_cong [cong]:
  "m = m' ⟹ missing_pattern_match m f = missing_pattern_match m' f"
  by(rule arg_cong)

lemma missing_pattern_match_code [code_unfold]:
  "missing_pattern_match = Code.abort"
  unfolding missing_pattern_match_def Code.abort_def ..

ML_file ‹case_converter.ML›

end