# HG changeset patch # User haftmann # Date 1196955379 -3600 # Node ID f14305fb698c41c2ad9b9400d3c4c6763bac408b # Parent 5c317e8f5673f11924c38936275864903ff8cbe0 authentic primrec diff -r 5c317e8f5673 -r f14305fb698c src/HOL/Library/Eval.thy --- 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 *} diff -r 5c317e8f5673 -r f14305fb698c src/HOL/List.thy --- 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 \ 'a list \ 'a list"}, InfixrName ("@", 65)) *} primrec - append_Nil:"[]@ys = ys" - append_Cons: "(x#xs)@ys = x#(xs@ys)" + append :: "'a list \ 'a list \ '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] \ True" | "sorted (x#y#zs) \ x <= y \ sorted (y#zs)" -fun insort :: "'a \ 'a list \ 'a list" where +primrec insort :: "'a \ 'a list \ '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 \ 'a list" where +primrec sort :: "'a list \ 'a list" where "sort [] = []" | "sort (x#xs) = insort x (sort xs)" @@ -3172,11 +3172,11 @@ filtermap :: "('a \ 'b option) \ 'a list \ 'b list" map_filter :: "('a \ 'b) \ ('a \ bool) \ 'a list \ 'b list" -setup {* snd o Sign.declare_const [] (*authentic syntax*) - ("member", @{typ "'a \ 'a list \ bool"}, InfixlName ("mem", 55)) *} primrec - "x mem [] = False" - "x mem (y#ys) = (if y=x then True else x mem ys)" + member :: "'a \ 'a list \ bool" (infixl "mem" 55) +where + "x mem [] \ False" + | "x mem (y#ys) \ (if y = x then True else x mem ys)" primrec "null [] = True" diff -r 5c317e8f5673 -r f14305fb698c src/HOL/Nat.thy --- 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 (\_. (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 \ '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 ("\") -end - -context semiring_1 -begin - lemma of_nat_in_Nats [simp]: "of_nat n \ \" 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 \ nat \ nat \ nat) = min" + +definition "(sup \ nat \ nat \ 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 *} diff -r 5c317e8f5673 -r f14305fb698c src/HOL/Tools/primrec_package.ML --- 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