# HG changeset patch # User huffman # Date 1291317524 28800 # Node ID 29a45797e269952ff778e1cd950651df6e782246 # Parent 0317c902dbfa6c7d62d4afb008b2c2dca1af81f9# Parent ee8d0548c14899b8c4c9e42540bd60d8d5c625a3 merged diff -r ee8d0548c148 -r 29a45797e269 src/HOL/HOLCF/Algebraic.thy --- a/src/HOL/HOLCF/Algebraic.thy Thu Dec 02 16:45:28 2010 +0100 +++ b/src/HOL/HOLCF/Algebraic.thy Thu Dec 02 11:18:44 2010 -0800 @@ -73,7 +73,7 @@ subsection {* Defining algebraic deflations by ideal completion *} typedef (open) defl = "{S::fin_defl set. below.ideal S}" -by (fast intro: below.ideal_principal) +by (rule below.ex_ideal) instantiation defl :: below begin diff -r ee8d0548c148 -r 29a45797e269 src/HOL/HOLCF/Completion.thy --- a/src/HOL/HOLCF/Completion.thy Thu Dec 02 16:45:28 2010 +0100 +++ b/src/HOL/HOLCF/Completion.thy Thu Dec 02 11:18:44 2010 -0800 @@ -49,8 +49,8 @@ apply (fast intro: r_trans) done -lemma ex_ideal: "\A. ideal A" -by (rule exI, rule ideal_principal) +lemma ex_ideal: "\A. A \ {A. ideal A}" +by (fast intro: ideal_principal) lemma lub_image_principal: assumes f: "\x y. x \ y \ f x \ f y" diff -r ee8d0548c148 -r 29a45797e269 src/HOL/HOLCF/ConvexPD.thy --- a/src/HOL/HOLCF/ConvexPD.thy Thu Dec 02 16:45:28 2010 +0100 +++ b/src/HOL/HOLCF/ConvexPD.thy Thu Dec 02 11:18:44 2010 -0800 @@ -121,7 +121,7 @@ typedef (open) 'a convex_pd = "{S::'a pd_basis set. convex_le.ideal S}" -by (fast intro: convex_le.ideal_principal) +by (rule convex_le.ex_ideal) instantiation convex_pd :: ("domain") below begin diff -r ee8d0548c148 -r 29a45797e269 src/HOL/HOLCF/LowerPD.thy --- a/src/HOL/HOLCF/LowerPD.thy Thu Dec 02 16:45:28 2010 +0100 +++ b/src/HOL/HOLCF/LowerPD.thy Thu Dec 02 11:18:44 2010 -0800 @@ -76,7 +76,7 @@ typedef (open) 'a lower_pd = "{S::'a pd_basis set. lower_le.ideal S}" -by (fast intro: lower_le.ideal_principal) +by (rule lower_le.ex_ideal) instantiation lower_pd :: ("domain") below begin diff -r ee8d0548c148 -r 29a45797e269 src/HOL/HOLCF/Tools/cpodef.ML --- a/src/HOL/HOLCF/Tools/cpodef.ML Thu Dec 02 16:45:28 2010 +0100 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Thu Dec 02 11:18:44 2010 -0800 @@ -193,7 +193,7 @@ fun add_podef def opt_name typ set opt_morphs tac thy = let val name = the_default (#1 typ) opt_name - val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy2) = thy + val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy) = thy |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac val oldT = #rep_type (#1 info) val newT = #abs_type (#1 info) @@ -202,18 +202,16 @@ val RepC = Const (Rep_name, newT --> oldT) val below_eqn = Logic.mk_equals (below_const newT, Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))) - val lthy3 = thy2 + val ((_, (_, below_ldef)), lthy) = thy |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po}) - val ((_, (_, below_ldef)), lthy4) = lthy3 |> Specification.definition (NONE, ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn)) - val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy4) - val below_def = singleton (ProofContext.export lthy4 ctxt_thy) below_ldef - val thy5 = lthy4 - |> Class.prove_instantiation_instance + val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy) + val below_def = singleton (ProofContext.export lthy ctxt_thy) below_ldef + val thy = lthy + |> Class.prove_instantiation_exit (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_def]) 1)) - |> Local_Theory.exit_global - in ((info, below_def), thy5) end + in ((info, below_def), thy) end fun prepare_cpodef (prep_term: Proof.context -> 'a -> term) @@ -235,12 +233,12 @@ fun cpodef_result nonempty admissible thy = let - val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy + val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1) - val (cpo_info, thy3) = thy2 + val (cpo_info, thy) = thy |> prove_cpo name newT morphs type_definition set_def below_def admissible in - ((info, cpo_info), thy3) + ((info, cpo_info), thy) end in (goal_nonempty, goal_admissible, cpodef_result) @@ -270,14 +268,14 @@ fun pcpodef_result UU_mem admissible thy = let val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1 - val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy + val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy |> add_podef def (SOME name) typ set opt_morphs tac - val (cpo_info, thy3) = thy2 + val (cpo_info, thy) = thy |> prove_cpo name newT morphs type_definition set_def below_def admissible - val (pcpo_info, thy4) = thy3 + val (pcpo_info, thy) = thy |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem in - ((info, cpo_info, pcpo_info), thy4) + ((info, cpo_info, pcpo_info), thy) end in (goal_UU_mem, goal_admissible, pcpodef_result) diff -r ee8d0548c148 -r 29a45797e269 src/HOL/HOLCF/Universal.thy --- a/src/HOL/HOLCF/Universal.thy Thu Dec 02 16:45:28 2010 +0100 +++ b/src/HOL/HOLCF/Universal.thy Thu Dec 02 11:18:44 2010 -0800 @@ -199,7 +199,7 @@ subsection {* Defining the universal domain by ideal completion *} typedef (open) udom = "{S. udom.ideal S}" -by (fast intro: udom.ideal_principal) +by (rule udom.ex_ideal) instantiation udom :: below begin diff -r ee8d0548c148 -r 29a45797e269 src/HOL/HOLCF/UpperPD.thy --- a/src/HOL/HOLCF/UpperPD.thy Thu Dec 02 16:45:28 2010 +0100 +++ b/src/HOL/HOLCF/UpperPD.thy Thu Dec 02 11:18:44 2010 -0800 @@ -74,7 +74,7 @@ typedef (open) 'a upper_pd = "{S::'a pd_basis set. upper_le.ideal S}" -by (fast intro: upper_le.ideal_principal) +by (rule upper_le.ex_ideal) instantiation upper_pd :: ("domain") below begin