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
     1 (* Author: Pascal Stoop, ETH Zurich
     2    Author: Andreas Lochbihler, Digital Asset *)
     3 
     4 theory Case_Converter
     5   imports Main
     6 begin
     7 
     8 subsection \<open>Eliminating pattern matches\<close>
     9 
    10 definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
    11   [code del]: "missing_pattern_match m f = f ()"
    12 
    13 lemma missing_pattern_match_cong [cong]:
    14   "m = m' \<Longrightarrow> missing_pattern_match m f = missing_pattern_match m' f"
    15   by(rule arg_cong)
    16 
    17 lemma missing_pattern_match_code [code_unfold]:
    18   "missing_pattern_match = Code.abort"
    19   unfolding missing_pattern_match_def Code.abort_def ..
    20 
    21 ML_file \<open>case_converter.ML\<close>
    22 
    23 end