src/HOL/Library/Case_Converter.thy
author haftmann
Fri Mar 22 19:18:08 2019 +0000 (4 months ago)
changeset 69946 494934c30f38
parent 69605 a96320074298
permissions -rw-r--r--
improved code equations taken over from AFP
Andreas@69567
     1
(* Author: Pascal Stoop, ETH Zurich
Andreas@69567
     2
   Author: Andreas Lochbihler, Digital Asset *)
Andreas@69567
     3
Andreas@69567
     4
theory Case_Converter
Andreas@69567
     5
  imports Main
Andreas@69567
     6
begin
Andreas@69567
     7
Andreas@69567
     8
subsection \<open>Eliminating pattern matches\<close>
Andreas@69567
     9
Andreas@69567
    10
definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
Andreas@69567
    11
  [code del]: "missing_pattern_match m f = f ()"
Andreas@69567
    12
Andreas@69567
    13
lemma missing_pattern_match_cong [cong]:
Andreas@69567
    14
  "m = m' \<Longrightarrow> missing_pattern_match m f = missing_pattern_match m' f"
Andreas@69567
    15
  by(rule arg_cong)
Andreas@69567
    16
Andreas@69567
    17
lemma missing_pattern_match_code [code_unfold]:
Andreas@69567
    18
  "missing_pattern_match = Code.abort"
Andreas@69567
    19
  unfolding missing_pattern_match_def Code.abort_def ..
Andreas@69567
    20
wenzelm@69605
    21
ML_file \<open>case_converter.ML\<close>
Andreas@69567
    22
Andreas@69567
    23
end