| author | nipkow |
| Wed, 13 Feb 2019 07:48:42 +0100 | |
| changeset 69801 | a99a0f5474c5 |
| parent 69605 | a96320074298 |
| child 77811 | ae9e6218443d |
| permissions | -rw-r--r-- |
|
69567
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
1 |
(* Author: Pascal Stoop, ETH Zurich |
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
2 |
Author: Andreas Lochbihler, Digital Asset *) |
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
3 |
|
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
4 |
theory Case_Converter |
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
5 |
imports Main |
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
6 |
begin |
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
7 |
|
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
8 |
subsection \<open>Eliminating pattern matches\<close> |
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
9 |
|
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
10 |
definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where |
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
11 |
[code del]: "missing_pattern_match m f = f ()" |
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
12 |
|
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
13 |
lemma missing_pattern_match_cong [cong]: |
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
14 |
"m = m' \<Longrightarrow> missing_pattern_match m f = missing_pattern_match m' f" |
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
15 |
by(rule arg_cong) |
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
16 |
|
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
17 |
lemma missing_pattern_match_code [code_unfold]: |
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
18 |
"missing_pattern_match = Code.abort" |
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
19 |
unfolding missing_pattern_match_def Code.abort_def .. |
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
20 |
|
| 69605 | 21 |
ML_file \<open>case_converter.ML\<close> |
|
69567
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
22 |
|
|
6b4c41037649
separate case converter into a separate theory
Andreas Lochbihler
parents:
diff
changeset
|
23 |
end |