--- 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 "(\<not> True) = False"
and "(\<not> 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 = {*
--- 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 \<Rightarrow> bool" where
- is_none_none [normal post, symmetric]: "is_none x \<longleftrightarrow> x = None"
-
-lemmas [code inline] = is_none_none
+ is_none_none [normal post, symmetric, code inline]: "is_none x \<longleftrightarrow> x = None"
lemma is_none_code [code]:
shows "is_none None \<longleftrightarrow> True"
--- 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
--- 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 "\<And>P\<Colon>bool. P"
- then show "False" ..
+ then show False ..
qed
lemma not_eq_False:
assumes not_eq: "x \<noteq> y"
- and eq: "x == y"
+ and eq: "x \<equiv> 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"
--- 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 \<le> Q \<equiv> P \<longrightarrow> Q"
less_bool_def: "P < Q \<equiv> P \<le> Q \<and> P \<noteq> 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
--- 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 \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c \<times> 'b"
where
- "upd_fst f = prod_fun f id"
+ [code func del]: "upd_fst f = prod_fun f id"
definition
upd_snd :: "('b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'a \<times> '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
*}