--- a/src/HOL/Library/Eval.thy Thu Dec 06 15:10:12 2007 +0100
+++ b/src/HOL/Library/Eval.thy Thu Dec 06 16:36:19 2007 +0100
@@ -102,7 +102,7 @@
(fn (v, ty) => term_term_of ty $ Free (v, ty))
(Pure_term.mk_typ (fn (v, sort) => TypOf.mk (TFree (v, sort)))) c
in
- HOLogic.mk_eq (lhs, rhs)
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
end;
in map mk_eq cs end;
fun mk_term_of t =
@@ -140,19 +140,26 @@
val vs = map fst vs_proto ~~ sorts;
val css = map (prep_dtyp thy vs) tycos;
val defs = map (TermOf.mk_terms_of_defs vs) css;
- val defs' = (map (pair ("", []) o ObjectLogic.ensure_propT thy) o flat) defs;
in if forall (fn tyco => can (Sign.arity_sorts thy tyco) @{sort term_of}) dep_tycos
andalso not (tycos = [@{type_name typ}])
- then SOME (sorts, defs')
+ then SOME (sorts, defs)
else NONE
end;
+ fun prep' ctxt proto_eqs =
+ let
+ val eqs as eq :: _ = map (Class.prep_spec ctxt) proto_eqs;
+ val (Free (v, ty), _) =
+ (strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) eq;
+ in ((v, SOME ty, NoSyn), map (pair ("", [])) eqs) end;
+ fun primrec primrecs ctxt =
+ let
+ val (fixes, eqnss) = split_list (map (prep' ctxt) primrecs);
+ in PrimrecPackage.add_primrec fixes (flat eqnss) ctxt end;
fun interpretator tycos thy = case prep thy tycos
of SOME (sorts, defs) =>
thy
|> Instance.instantiate (tycos, sorts, @{sort term_of})
- (pair ()) ((K o K) (Class.intro_classes_tac []))
- |> OldPrimrecPackage.gen_primrec thy_note thy_def "" defs
- |> snd
+ (primrec defs) ((K o K) (Class.intro_classes_tac []))
| NONE => thy;
in DatatypePackage.interpretation interpretator end
*}
@@ -184,7 +191,7 @@
text {* Adaption for @{typ message_string}s *}
-lemmas [code func, code func del] = term_of_message_string_def
+lemmas [code func del] = term_of_messagestring.simps
subsection {* Evaluation infrastructure *}
--- a/src/HOL/List.thy Thu Dec 06 15:10:12 2007 +0100
+++ b/src/HOL/List.thy Thu Dec 06 16:36:19 2007 +0100
@@ -104,11 +104,11 @@
"map f [] = []"
"map f (x#xs) = f(x)#map f xs"
-setup {* snd o Sign.declare_const [] (*authentic syntax*)
- ("append", @{typ "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"}, InfixrName ("@", 65)) *}
primrec
- append_Nil:"[]@ys = ys"
- append_Cons: "(x#xs)@ys = x#(xs@ys)"
+ append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "@" 65)
+where
+ append_Nil:"[] @ ys = ys"
+ | append_Cons: "(x#xs) @ ys = x # xs @ ys"
primrec
"rev([]) = []"
@@ -222,11 +222,11 @@
"sorted [x] \<longleftrightarrow> True" |
"sorted (x#y#zs) \<longleftrightarrow> x <= y \<and> sorted (y#zs)"
-fun insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+primrec insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
"insort x [] = [x]" |
"insort x (y#ys) = (if x <= y then (x#y#ys) else y#(insort x ys))"
-fun sort :: "'a list \<Rightarrow> 'a list" where
+primrec sort :: "'a list \<Rightarrow> 'a list" where
"sort [] = []" |
"sort (x#xs) = insort x (sort xs)"
@@ -3172,11 +3172,11 @@
filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list"
-setup {* snd o Sign.declare_const [] (*authentic syntax*)
- ("member", @{typ "'a \<Rightarrow> 'a list \<Rightarrow> bool"}, InfixlName ("mem", 55)) *}
primrec
- "x mem [] = False"
- "x mem (y#ys) = (if y=x then True else x mem ys)"
+ member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
+where
+ "x mem [] \<longleftrightarrow> False"
+ | "x mem (y#ys) \<longleftrightarrow> (if y = x then True else x mem ys)"
primrec
"null [] = True"
--- a/src/HOL/Nat.thy Thu Dec 06 15:10:12 2007 +0100
+++ b/src/HOL/Nat.thy Thu Dec 06 16:36:19 2007 +0100
@@ -1157,13 +1157,11 @@
context semiring_1
begin
-definition
- of_nat_def: "of_nat = nat_rec 0 (\<lambda>_. (op +) 1)"
-
-lemma of_nat_simps [simp, code]:
- shows of_nat_0: "of_nat 0 = 0"
- and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
- unfolding of_nat_def by simp_all
+primrec
+ of_nat :: "nat \<Rightarrow> 'a"
+where
+ of_nat_0: "of_nat 0 = 0"
+ | of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
lemma of_nat_1 [simp]: "of_nat 1 = 1"
by simp
@@ -1454,11 +1452,6 @@
notation (xsymbols)
Nats ("\<nat>")
-end
-
-context semiring_1
-begin
-
lemma of_nat_in_Nats [simp]: "of_nat n \<in> \<nat>"
by (simp add: Nats_def)
@@ -1491,11 +1484,19 @@
text {* the lattice order on @{typ nat} *}
-instance nat :: distrib_lattice
+instantiation nat :: distrib_lattice
+begin
+
+definition
"(inf \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = min"
+
+definition
"(sup \<Colon> nat \<Rightarrow> nat \<Rightarrow> nat) = max"
- by intro_classes
- (simp_all add: inf_nat_def sup_nat_def)
+
+instance by intro_classes
+ (simp_all add: inf_nat_def sup_nat_def)
+
+end
subsection {* legacy bindings *}
--- a/src/HOL/Tools/primrec_package.ML Thu Dec 06 15:10:12 2007 +0100
+++ b/src/HOL/Tools/primrec_package.ML Thu Dec 06 16:36:19 2007 +0100
@@ -27,10 +27,11 @@
(* preprocessing of equations *)
-fun process_eqn is_fixed is_const spec rec_fns =
+fun process_eqn is_fixed spec rec_fns =
let
val vars = strip_qnt_vars "all" spec;
val body = strip_qnt_body "all" spec;
+ (*FIXME not necessarily correct*)
val eqn = curry subst_bounds (map Free (rev vars)) body;
val (lhs, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eqn)
handle TERM _ => primrec_error "not a proper equation";
@@ -64,7 +65,7 @@
(check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
check_vars "extra variables on rhs: "
(map dest_Free (term_frees rhs) |> subtract (op =) lfrees
- |> filter_out (is_const o fst) |> filter_out (is_fixed o fst));
+ |> filter_out (is_fixed o fst));
case AList.lookup (op =) rec_fns fname of
NONE =>
(fname, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eqn))]))::rec_fns
@@ -222,8 +223,9 @@
fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
let
- val ((fixes, spec), _) = prep_spec raw_fixes [(map o apsnd) single raw_spec] ctxt
- in (fixes, (map o apsnd) the_single spec) end;
+ val ((fixes, spec), _) = prep_spec
+ raw_fixes (map (single o apsnd single) raw_spec) ctxt
+ in (fixes, map (apsnd the_single) spec) end;
fun prove_spec ctxt rec_rewrites defs =
let
@@ -235,8 +237,8 @@
fun gen_primrec prep_spec raw_fixes raw_spec lthy =
let
val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
- val eqns = fold_rev (process_eqn (member (op =) (map (fst o fst) fixes))
- (Variable.is_const lthy) o snd) spec [];
+ val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
+ orelse exists (fn ((w, _), _) => v = w) fixes) o snd) spec [];
val tnames = distinct (op =) (map (#1 o snd) eqns);
val dts = find_dts (DatatypePackage.get_datatypes
(ProofContext.theory_of lthy)) tnames tnames;
@@ -255,8 +257,7 @@
"\nare not mutually recursive");
val qualify = NameSpace.qualified
(space_implode "_" (map (Sign.base_name o #1) defs));
- val simp_atts = [Attrib.internal (K Simplifier.simp_add),
- Code.add_default_func_attr (*FIXME*)];
+ val simp_atts = map (Attrib.internal o K) [Simplifier.simp_add, RecfunCodegen.add NONE];
in
lthy
|> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs