--- a/NEWS Tue Oct 07 16:07:30 2008 +0200
+++ b/NEWS Tue Oct 07 16:07:33 2008 +0200
@@ -91,6 +91,11 @@
*** HOL ***
+* Unified theorem tables of both code code generators. Thus [code]
+and [code func] behave identically. INCOMPATIBILITY.
+
+* "undefined" replaces "arbitrary" in most occurences.
+
* Wrapper script for remote SystemOnTPTP service allows to use
sledgehammer without local ATP installation (Vampire etc.). See also
ISABELLE_HOME/contrib/SystemOnTPTP and the VAMPIRE_HOME setting
--- a/src/HOL/Library/Efficient_Nat.thy Tue Oct 07 16:07:30 2008 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Tue Oct 07 16:07:33 2008 +0200
@@ -27,12 +27,12 @@
code_datatype number_nat_inst.number_of_nat
-lemma zero_nat_code [code, code unfold]:
+lemma zero_nat_code [code, code inline]:
"0 = (Numeral0 :: nat)"
by simp
lemmas [code post] = zero_nat_code [symmetric]
-lemma one_nat_code [code, code unfold]:
+lemma one_nat_code [code, code inline]:
"1 = (Numeral1 :: nat)"
by simp
lemmas [code post] = one_nat_code [symmetric]
@@ -59,9 +59,9 @@
definition
divmod_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat"
where
- [code func del]: "divmod_aux = divmod"
+ [code del]: "divmod_aux = divmod"
-lemma [code func]:
+lemma [code]:
"divmod n m = (if m = 0 then (0, n) else divmod_aux n m)"
unfolding divmod_aux_def divmod_div_mod by simp
@@ -92,7 +92,7 @@
expression:
*}
-lemma [code func, code unfold]:
+lemma [code, code unfold]:
"nat_case = (\<lambda>f g n. if n = 0 then f else g (n - 1))"
by (auto simp add: expand_fun_eq dest!: gr0_implies_Suc)
@@ -221,8 +221,7 @@
fun lift f thy eqns1 =
let
- val eqns2 = ((map o apfst) (AxClass.overload thy)
- o burrow_fst Drule.zero_var_indexes_list) eqns1;
+ val eqns2 = burrow_fst Drule.zero_var_indexes_list eqns1;
val thms3 = try (map fst
#> map (fn thm => thm RS @{thm meta_eq_to_obj_eq})
#> f thy
@@ -232,7 +231,8 @@
in case thms4
of NONE => NONE
| SOME thms4 => if Thm.eq_thms (map fst eqns2, thms4)
- then NONE else SOME (map (Code_Unit.mk_eqn thy) thms4)
+ then NONE else SOME (map (apfst (AxClass.overload thy) o Code_Unit.mk_eqn thy) thms4)
+ (*FIXME*)
end
in
@@ -423,7 +423,8 @@
(Haskell infix 4 "<")
consts_code
- 0 ("0")
+ "0::nat" ("0")
+ "1::nat" ("1")
Suc ("(_ +/ 1)")
"op + \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" ("(_ +/ _)")
"op * \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat" ("(_ */ _)")
--- a/src/HOL/Library/Executable_Set.thy Tue Oct 07 16:07:30 2008 +0200
+++ b/src/HOL/Library/Executable_Set.thy Tue Oct 07 16:07:33 2008 +0200
@@ -11,11 +11,22 @@
subsection {* Definitional rewrites *}
-lemma [code target: Set]:
- "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
- by blast
+definition subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+ "subset = op \<le>"
+
+declare subset_def [symmetric, code unfold]
+
+lemma "subset A B \<longleftrightarrow> (\<forall>x\<in>A. x \<in> B)"
+ unfolding subset_def subset_eq ..
-declare subset_eq [code]
+definition is_empty :: "'a set \<Rightarrow> bool" where
+ "is_empty A \<longleftrightarrow> A = {}"
+
+definition eq_set :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
+ [code del]: "eq_set = op ="
+
+lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
+ unfolding eq_set_def by auto
lemma [code]:
"a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
@@ -247,6 +258,7 @@
consts_code
"{}" ("{*[]*}")
insert ("{*insertl*}")
+ is_empty ("{*null*}")
"op \<union>" ("{*unionl*}")
"op \<inter>" ("{*intersect*}")
"op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" ("{* flip subtract *}")
--- a/src/HOL/Tools/recfun_codegen.ML Tue Oct 07 16:07:30 2008 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Tue Oct 07 16:07:33 2008 +0200
@@ -18,57 +18,73 @@
open Codegen;
-structure RecCodegenData = TheoryDataFun
+structure ModuleData = TheoryDataFun
(
- type T = (thm * string option) list Symtab.table;
+ type T = string Symtab.table;
val empty = Symtab.empty;
val copy = I;
val extend = I;
- fun merge _ = Symtab.merge_list (Thm.eq_thm_prop o pairself fst);
+ fun merge _ = Symtab.merge (K true);
);
-val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
-val lhs_of = fst o dest_eqn o prop_of;
-val const_of = dest_Const o head_of o fst o dest_eqn;
-
-fun warn thm = warning ("RecfunCodegen: Not a proper equation:\n" ^
- Display.string_of_thm thm);
-
-fun add_thm opt_module thm =
- (if Pattern.pattern (lhs_of thm) then
- RecCodegenData.map
- (Symtab.cons_list ((fst o const_of o prop_of) thm, (thm, opt_module)))
- else tap (fn _ => warn thm))
- handle TERM _ => tap (fn _ => warn thm);
+fun add_thm add NONE thm thy = add thm thy
+ | add_thm add (SOME module_name) thm thy =
+ case Code_Unit.warning_thm (Code_Unit.mk_eqn thy) thm
+ of SOME (thm', _) => let val c = Code_Unit.const_eqn thm'
+ in thy
+ |> ModuleData.map (Symtab.update (c, module_name))
+ |> add thm'
+ end
+ | NONE => add thm thy;
fun add opt_module = Thm.declaration_attribute (fn thm => Context.mapping
- (add_thm opt_module thm #> Code.add_liberal_eqn thm) I);
+ (add_thm Code.add_eqn opt_module thm) I);
val add_default = Thm.declaration_attribute (fn thm => Context.mapping
- (add_thm NONE thm #> Code.add_default_eqn thm) I);
+ (add_thm Code.add_default_eqn NONE thm) I);
+
+val del = Thm.declaration_attribute (fn thm => Context.mapping
+ (Code.del_eqn thm) I);
-fun del_thm thm = case try const_of (prop_of thm)
- of SOME (s, _) => RecCodegenData.map
- (Symtab.map_entry s (remove (Thm.eq_thm o apsnd fst) thm))
- | NONE => tap (fn _ => warn thm);
+fun meta_eq_to_obj_eq thy thm =
+ let
+ val T = (fastype_of o fst o Logic.dest_equals o Thm.prop_of) thm;
+ in if Sign.of_sort thy (T, @{sort type})
+ then SOME (Conv.fconv_rule Drule.beta_eta_conversion (@{thm meta_eq_to_obj_eq} OF [thm]))
+ else NONE
+ end;
-val del = Thm.declaration_attribute
- (fn thm => Context.mapping (del_thm thm #> Code.del_eqn thm) I)
+fun expand_eta thy [] = []
+ | expand_eta thy (thms as thm :: _) =
+ let
+ val (_, ty) = Code_Unit.const_typ_eqn thm;
+ in if (null o Term.typ_tvars) ty orelse (null o fst o strip_type) ty
+ then thms
+ else map (Code_Unit.expand_eta thy 1) thms
+ end;
-fun del_redundant thy eqs [] = eqs
- | del_redundant thy eqs (eq :: eqs') =
- let
- val matches = curry
- (Pattern.matches thy o pairself (lhs_of o fst))
- in del_redundant thy (eq :: eqs) (filter_out (matches eq) eqs') end;
+fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else
+ let
+ val c' = AxClass.unoverload_const thy (c, T);
+ val opt_name = Symtab.lookup (ModuleData.get thy) c';
+ val thms = Code.these_raw_eqns thy c'
+ |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
+ |> expand_eta thy
+ |> map (AxClass.overload thy)
+ |> map_filter (meta_eq_to_obj_eq thy)
+ |> Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var
+ |> map (rpair opt_name)
+ in if null thms then NONE else SOME thms end;
+
+val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
+val const_of = dest_Const o head_of o fst o dest_eqn;
fun get_equations thy defs (s, T) =
- (case Symtab.lookup (RecCodegenData.get thy) s of
+ (case retrieve_equations thy (s, T) of
NONE => ([], "")
| SOME thms =>
- let val thms' = del_redundant thy []
- (filter (fn (thm, _) => is_instance T
- (snd (const_of (prop_of thm)))) thms)
+ let val thms' = filter (fn (thm, _) => is_instance T
+ (snd (const_of (prop_of thm)))) thms
in if null thms' then ([], "")
else (preprocess thy (map fst thms'),
case snd (snd (split_last thms')) of
@@ -166,7 +182,6 @@
end)
| _ => NONE);
-
val setup =
add_codegen "recfun" recfun_codegen
#> Code.add_attribute ("", Args.del |-- Scan.succeed del