Quelle  Case_Converter.thy   Sprache: Isabelle

(* 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