# HG changeset patch # User haftmann # Date 1178689986 -7200 # Node ID cdff6ef76009ee348510a2dbc233327bf532f3aa # Parent ebde66a71ab0cdca39792b812da465e5f131f8be moved recfun_codegen.ML to Code_Generator.thy diff -r ebde66a71ab0 -r cdff6ef76009 src/HOL/Code_Generator.thy --- a/src/HOL/Code_Generator.thy Wed May 09 07:53:04 2007 +0200 +++ b/src/HOL/Code_Generator.thy Wed May 09 07:53:06 2007 +0200 @@ -6,8 +6,16 @@ theory Code_Generator imports HOL +uses "~~/src/HOL/Tools/recfun_codegen.ML" begin +ML {* +structure HOL = +struct + val thy = theory "HOL"; +end; +*} -- "belongs to theory HOL" + subsection {* SML code generator setup *} types_code @@ -55,6 +63,7 @@ in Codegen.add_codegen "eq_codegen" eq_codegen +#> RecfunCodegen.setup end *} @@ -107,7 +116,7 @@ shows "(\ True) = False" and "(\ False) = True" by (rule HOL.simp_thms)+ -lemmas [code func] = imp_conv_disj +lemmas [code] = imp_conv_disj lemmas [code func] = if_True if_False @@ -174,7 +183,7 @@ oracle eval_oracle ("term") = {* fn thy => fn t => if CodegenPackage.satisfies thy (HOLogic.dest_Trueprop t) [] then t - else HOLogic.Trueprop $ (HOLogic.true_const) (*dummy*) + else HOLogic.Trueprop $ HOLogic.true_const (*dummy*) *} method_setup eval = {* diff -r ebde66a71ab0 -r cdff6ef76009 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Wed May 09 07:53:04 2007 +0200 +++ b/src/HOL/Datatype.thy Wed May 09 07:53:06 2007 +0200 @@ -102,7 +102,7 @@ (** apfst -- can be used in similar type definitions **) -lemma apfst_conv [simp, code func]: "apfst f (a, b) = (f a, b)" +lemma apfst_conv [simp, code]: "apfst f (a, b) = (f a, b)" by (simp add: apfst_def) @@ -715,12 +715,12 @@ constdefs option_map :: "('a => 'b) => ('a option => 'b option)" - "option_map == %f y. case y of None => None | Some x => Some (f x)" + [code func del]: "option_map == %f y. case y of None => None | Some x => Some (f x)" -lemma option_map_None [simp, code func]: "option_map f None = None" +lemma option_map_None [simp, code]: "option_map f None = None" by (simp add: option_map_def) -lemma option_map_Some [simp, code func]: "option_map f (Some x) = Some (f x)" +lemma option_map_Some [simp, code]: "option_map f (Some x) = Some (f x)" by (simp add: option_map_def) lemma option_map_is_None [iff]: @@ -742,13 +742,9 @@ subsubsection {* Code generator setup *} -lemmas [code] = fst_conv snd_conv imp_conv_disj - definition is_none :: "'a option \ bool" where - is_none_none [normal post, symmetric]: "is_none x \ x = None" - -lemmas [code inline] = is_none_none + is_none_none [normal post, symmetric, code inline]: "is_none x \ x = None" lemma is_none_code [code]: shows "is_none None \ True" diff -r ebde66a71ab0 -r cdff6ef76009 src/HOL/Fun.thy --- a/src/HOL/Fun.thy Wed May 09 07:53:04 2007 +0200 +++ b/src/HOL/Fun.thy Wed May 09 07:53:06 2007 +0200 @@ -7,12 +7,12 @@ header {* Notions about functions *} theory Fun -imports Set Code_Generator +imports Set begin constdefs fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" - [code func]: "fun_upd f a b == % x. if x=a then b else f x" + "fun_upd f a b == % x. if x=a then b else f x" nonterminals updbinds updbind diff -r ebde66a71ab0 -r cdff6ef76009 src/HOL/Inductive.thy --- a/src/HOL/Inductive.thy Wed May 09 07:53:04 2007 +0200 +++ b/src/HOL/Inductive.thy Wed May 09 07:53:06 2007 +0200 @@ -21,7 +21,6 @@ ("Tools/datatype_case.ML") ("Tools/datatype_package.ML") ("Tools/datatype_codegen.ML") - ("Tools/recfun_codegen.ML") ("Tools/primrec_package.ML") begin @@ -61,7 +60,7 @@ text {* Package setup. *} -use "Tools/old_inductive_package.ML" +ML {* setmp tolerate_legacy_features true use "Tools/old_inductive_package.ML" *} setup OldInductivePackage.setup theorems basic_monos [mono] = @@ -90,12 +89,12 @@ then show P .. next assume "\P\bool. P" - then show "False" .. + then show False .. qed lemma not_eq_False: assumes not_eq: "x \ y" - and eq: "x == y" + and eq: "x \ y" shows False using not_eq eq by auto @@ -107,9 +106,6 @@ text {* Package setup. *} -use "Tools/recfun_codegen.ML" -setup RecfunCodegen.setup - use "Tools/datatype_aux.ML" use "Tools/datatype_prop.ML" use "Tools/datatype_rep_proofs.ML" diff -r ebde66a71ab0 -r cdff6ef76009 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Wed May 09 07:53:04 2007 +0200 +++ b/src/HOL/Orderings.thy Wed May 09 07:53:06 2007 +0200 @@ -6,7 +6,7 @@ header {* Syntactic and abstract orders *} theory Orderings -imports HOL +imports Code_Generator begin subsection {* Order syntax *} @@ -798,7 +798,7 @@ subsection {* Order on bool *} -instance bool :: linorder +instance bool :: order le_bool_def: "P \ Q \ P \ Q" less_bool_def: "P < Q \ P \ Q \ P \ Q" by default (auto simp add: le_bool_def less_bool_def) @@ -892,11 +892,6 @@ ML {* val monoI = @{thm monoI}; - -structure HOL = -struct - val thy = theory "HOL"; -end; -*} -- "belongs to theory HOL" +*} end diff -r ebde66a71ab0 -r cdff6ef76009 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Wed May 09 07:53:04 2007 +0200 +++ b/src/HOL/Product_Type.thy Wed May 09 07:53:06 2007 +0200 @@ -231,10 +231,10 @@ lemma Pair_eq [iff]: "((a, b) = (a', b')) = (a = a' & b = b')" by (blast elim!: Pair_inject) -lemma fst_conv [simp]: "fst (a, b) = a" +lemma fst_conv [simp, code]: "fst (a, b) = a" unfolding fst_def by blast -lemma snd_conv [simp]: "snd (a, b) = b" +lemma snd_conv [simp, code]: "snd (a, b) = b" unfolding snd_def by blast lemma fst_eqD: "fst (x, y) = a ==> x = a" @@ -602,18 +602,18 @@ definition upd_fst :: "('a \ 'c) \ 'a \ 'b \ 'c \ 'b" where - "upd_fst f = prod_fun f id" + [code func del]: "upd_fst f = prod_fun f id" definition upd_snd :: "('b \ 'c) \ 'a \ 'b \ 'a \ 'c" where - "upd_snd f = prod_fun id f" + [code func del]: "upd_snd f = prod_fun id f" -lemma upd_fst_conv [simp, code func]: +lemma upd_fst_conv [simp, code]: "upd_fst f (x, y) = (f x, y)" by (simp add: upd_fst_def) -lemma upd_snd_conv [simp, code func]: +lemma upd_snd_conv [simp, code]: "upd_snd f (x, y) = (x, f y)" by (simp add: upd_snd_def) @@ -776,8 +776,6 @@ subsection {* Code generator setup *} -lemmas [code func] = fst_conv snd_conv - instance unit :: eq .. lemma [code func]: @@ -910,8 +908,7 @@ Codegen.add_codegen "let_codegen" let_codegen #> Codegen.add_codegen "split_codegen" split_codegen - #> CodegenPackage.add_appconst - ("Let", CodegenPackage.appgen_let) + #> CodegenPackage.add_appconst ("Let", CodegenPackage.appgen_let) end *}