equal
deleted
inserted
replaced
|
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 "case_converter.ML" |
|
22 |
|
23 end |