# HG changeset patch # User haftmann # Date 1256019047 -7200 # Node ID b0ff69f0a24859a512f4a154f3b3488c74b4a1aa # Parent 82382652e5e7ed8700a5ef6141ab3f0e93205be8# Parent 94108ea8c568d884e4f9c639f880524417090584 merged diff -r 82382652e5e7 -r b0ff69f0a248 CONTRIBUTORS --- a/CONTRIBUTORS Mon Oct 19 16:47:21 2009 +0200 +++ b/CONTRIBUTORS Tue Oct 20 08:10:47 2009 +0200 @@ -7,6 +7,12 @@ Contributions to this Isabelle version -------------------------------------- +* Oktober 2009: Florian Haftmann, TUM + Refinement of parts of the HOL datatype package + +* Oktober 2009: Florian Haftmann, TUM + Generic term styles for term antiquotations + * September 2009: Thomas Sewell, NICTA More efficient HOL/record implementation @@ -14,7 +20,7 @@ SMT method using external SMT solvers * September 2009: Florian Haftmann, TUM - Refinement of Sets and Lattices + Refinement of sets and lattices * July 2009: Jeremy Avigad and Amine Chaieb New number theory diff -r 82382652e5e7 -r b0ff69f0a248 src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Oct 19 16:47:21 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Oct 20 08:10:47 2009 +0200 @@ -7,8 +7,6 @@ signature DATATYPE_CODEGEN = sig val find_shortest_path: Datatype.descr -> int -> (string * int) option - val mk_eq_eqns: theory -> string -> (thm * bool) list - val mk_case_cert: theory -> string -> thm val setup: theory -> theory end; @@ -386,7 +384,7 @@ (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms))); fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset))) |> Simpdata.mk_eq; - in map (rpair true o prove) (triv_injects @ injects @ distincts) @ [(prove refl, false)] end; + in (map prove (triv_injects @ injects @ distincts), prove refl) end; fun add_equality vs dtcos thy = let @@ -405,14 +403,12 @@ in (thm', lthy') end; fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (ProofContext.fact_tac thms); - fun add_eq_thms dtco thy = - let - val const = AxClass.param_of_inst thy (@{const_name eq_class.eq}, dtco); - val thy_ref = Theory.check_thy thy; - fun mk_thms () = rev ((mk_eq_eqns (Theory.deref thy_ref) dtco)); - in - Code.add_eqnl (const, Lazy.lazy mk_thms) thy - end; + fun add_eq_thms dtco = + Theory.checkpoint + #> `(fn thy => mk_eq_eqns thy dtco) + #-> (fn (thms, thm) => + Code.add_nbe_eqn thm + #> fold_rev Code.add_eqn thms); in thy |> TheoryTarget.instantiation (dtcos, vs, [HOLogic.class_eq]) diff -r 82382652e5e7 -r b0ff69f0a248 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Mon Oct 19 16:47:21 2009 +0200 +++ b/src/Pure/Isar/code.ML Tue Oct 20 08:10:47 2009 +0200 @@ -37,7 +37,6 @@ (string * ((string * sort) list * (string * typ list) list) -> theory -> theory) -> theory -> theory val add_eqn: thm -> theory -> theory - val add_eqnl: string * (thm * bool) list lazy -> theory -> theory val add_nbe_eqn: thm -> theory -> theory val add_default_eqn: thm -> theory -> theory val add_default_eqn_attribute: attribute @@ -119,19 +118,8 @@ (* code equations *) -type eqns = bool * (thm * bool) list lazy; - (*default flag, theorems with proper flag (perhaps lazy)*) - -fun pretty_lthms ctxt r = case Lazy.peek r - of SOME thms => map (Display.pretty_thm ctxt o fst) (Exn.release thms) - | NONE => [Pretty.str "[...]"]; - -fun certificate thy f r = - case Lazy.peek r - of SOME thms => (Lazy.value o f thy) (Exn.release thms) - | NONE => let - val thy_ref = Theory.check_thy thy; - in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end; +type eqns = bool * (thm * bool) list; + (*default flag, theorems with proper flag *) fun add_drop_redundant thy (thm, proper) thms = let @@ -148,13 +136,11 @@ else false; in (thm, proper) :: filter_out drop thms end; -fun add_thm thy _ thm (false, thms) = (false, Lazy.map_force (add_drop_redundant thy thm) thms) - | add_thm thy true thm (true, thms) = (true, Lazy.map_force (fn thms => thms @ [thm]) thms) - | add_thm thy false thm (true, thms) = (false, Lazy.value [thm]); +fun add_thm thy _ thm (false, thms) = (false, add_drop_redundant thy thm thms) + | add_thm thy true thm (true, thms) = (true, thms @ [thm]) + | add_thm thy false thm (true, thms) = (false, [thm]); -fun add_lthms lthms _ = (false, lthms); - -fun del_thm thm = (apsnd o Lazy.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true)); +fun del_thm thm = apsnd (remove (eq_fst Thm.eq_thm_prop) (thm, true)); (* executable code data *) @@ -285,17 +271,17 @@ val purge_data = (Code_Data.map o apsnd) (K (Unsynchronized.ref empty_data)); fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns - o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), []))) + o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, [])), []))) o apfst) (fn (_, eqns) => (true, f eqns)); -fun del_eqns c = change_eqns true c (K (false, Lazy.value [])); +fun del_eqns c = change_eqns true c (K (false, [])); (* tackling equation history *) fun get_eqns thy c = Symtab.lookup ((the_eqns o the_exec) thy) c - |> Option.map (Lazy.force o snd o snd o fst) + |> Option.map (snd o snd o fst) |> these; fun continue_history thy = if (history_concluded o the_exec) thy @@ -550,7 +536,7 @@ fun all_eqns thy = Symtab.dest ((the_eqns o the_exec) thy) - |> maps (Lazy.force o snd o snd o fst o snd); + |> maps (snd o snd o fst o snd); (* cases *) @@ -606,9 +592,9 @@ let val ctxt = ProofContext.init thy; val exec = the_exec thy; - fun pretty_eqn (s, (_, lthms)) = + fun pretty_eqns (s, (_, eqns)) = (Pretty.block o Pretty.fbreaks) ( - Pretty.str s :: pretty_lthms ctxt lthms + Pretty.str s :: map (Display.pretty_thm ctxt o fst) eqns ); fun pretty_dtyp (s, []) = Pretty.str s @@ -638,7 +624,7 @@ Pretty.block ( Pretty.str "code equations:" :: Pretty.fbrk - :: (Pretty.fbreaks o map pretty_eqn) eqns + :: (Pretty.fbreaks o map pretty_eqns) eqns ), Pretty.block ( Pretty.str "datatypes:" @@ -704,11 +690,6 @@ fun add_nbe_eqn thm thy = gen_add_eqn false (mk_eqn thy (thm, false)) thy; -fun add_eqnl (c, lthms) thy = - let - val lthms' = certificate thy (fn thy => assert_eqns_const thy c) lthms; - in change_eqns false c (add_lthms lthms') thy end; - val add_default_eqn_attribute = Thm.declaration_attribute (fn thm => Context.mapping (add_default_eqn thm) I); val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);