separate case converter into a separate theory
authorAndreas Lochbihler
Sun Dec 30 10:30:41 2018 +0100 (6 months ago)
changeset 695676b4c41037649
parent 69544 5aa5a8d6e5b5
child 69568 de09a7261120
separate case converter into a separate theory
src/HOL/Library/Case_Converter.thy
src/HOL/Library/Code_Lazy.thy
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Case_Converter.thy	Sun Dec 30 10:30:41 2018 +0100
     1.3 @@ -0,0 +1,23 @@
     1.4 +(* Author: Pascal Stoop, ETH Zurich
     1.5 +   Author: Andreas Lochbihler, Digital Asset *)
     1.6 +
     1.7 +theory Case_Converter
     1.8 +  imports Main
     1.9 +begin
    1.10 +
    1.11 +subsection \<open>Eliminating pattern matches\<close>
    1.12 +
    1.13 +definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
    1.14 +  [code del]: "missing_pattern_match m f = f ()"
    1.15 +
    1.16 +lemma missing_pattern_match_cong [cong]:
    1.17 +  "m = m' \<Longrightarrow> missing_pattern_match m f = missing_pattern_match m' f"
    1.18 +  by(rule arg_cong)
    1.19 +
    1.20 +lemma missing_pattern_match_code [code_unfold]:
    1.21 +  "missing_pattern_match = Code.abort"
    1.22 +  unfolding missing_pattern_match_def Code.abort_def ..
    1.23 +
    1.24 +ML_file "case_converter.ML"
    1.25 +
    1.26 +end
     2.1 --- a/src/HOL/Library/Code_Lazy.thy	Sat Dec 29 20:32:09 2018 +0100
     2.2 +++ b/src/HOL/Library/Code_Lazy.thy	Sun Dec 30 10:30:41 2018 +0100
     2.3 @@ -4,7 +4,7 @@
     2.4  section \<open>Lazy types in generated code\<close>
     2.5  
     2.6  theory Code_Lazy
     2.7 -imports Main
     2.8 +imports Case_Converter
     2.9  keywords
    2.10    "code_lazy_type"
    2.11    "activate_lazy_type"
    2.12 @@ -24,22 +24,6 @@
    2.13    and thus eligible for lazification.
    2.14  \<close>
    2.15  
    2.16 -subsection \<open>Eliminating pattern matches\<close>
    2.17 -
    2.18 -definition missing_pattern_match :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a" where
    2.19 -  [code del]: "missing_pattern_match m f = f ()"
    2.20 -
    2.21 -lemma missing_pattern_match_cong [cong]:
    2.22 -  "m = m' \<Longrightarrow> missing_pattern_match m f = missing_pattern_match m' f"
    2.23 -  by(rule arg_cong)
    2.24 -
    2.25 -lemma missing_pattern_match_code [code_unfold]:
    2.26 -  "missing_pattern_match = Code.abort"
    2.27 -  unfolding missing_pattern_match_def Code.abort_def ..
    2.28 -
    2.29 -ML_file "case_converter.ML"
    2.30 -
    2.31 -
    2.32  subsection \<open>The type \<open>lazy\<close>\<close>
    2.33  
    2.34  typedef 'a lazy = "UNIV :: 'a set" ..