# HG changeset patch # User wenzelm # Date 1229010618 -3600 # Node ID 7619f0561cd7d7ab17d35423170ac2a0beac4043 # Parent 6f8a100325b6b8c6d99e71e7db57f09eaa3a4fed pcpodef package: state two goals, instead of encoded conjunction; diff -r 6f8a100325b6 -r 7619f0561cd7 src/HOLCF/Cfun.thy --- a/src/HOLCF/Cfun.thy Thu Dec 11 16:30:35 2008 +0100 +++ b/src/HOLCF/Cfun.thy Thu Dec 11 16:50:18 2008 +0100 @@ -23,7 +23,7 @@ by (rule admI, rule cont_lub_fun) cpodef (CFun) ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}" -by (simp add: Ex_cont adm_cont) +by (simp_all add: Ex_cont adm_cont) syntax (xsymbols) "->" :: "[type, type] => type" ("(_ \/ _)" [1,0]0) diff -r 6f8a100325b6 -r 7619f0561cd7 src/HOLCF/Fixrec.thy --- a/src/HOLCF/Fixrec.thy Thu Dec 11 16:30:35 2008 +0100 +++ b/src/HOLCF/Fixrec.thy Thu Dec 11 16:50:18 2008 +0100 @@ -15,7 +15,7 @@ defaultsort cpo pcpodef (open) 'a maybe = "UNIV::(one ++ 'a u) set" -by simp +by simp_all constdefs fail :: "'a maybe" diff -r 6f8a100325b6 -r 7619f0561cd7 src/HOLCF/Lift.thy --- a/src/HOLCF/Lift.thy Thu Dec 11 16:30:35 2008 +0100 +++ b/src/HOLCF/Lift.thy Thu Dec 11 16:50:18 2008 +0100 @@ -12,7 +12,7 @@ defaultsort type pcpodef 'a lift = "UNIV :: 'a discr u set" -by simp +by simp_all instance lift :: (finite) finite_po by (rule typedef_finite_po [OF type_definition_lift]) diff -r 6f8a100325b6 -r 7619f0561cd7 src/HOLCF/Sprod.thy --- a/src/HOLCF/Sprod.thy Thu Dec 11 16:30:35 2008 +0100 +++ b/src/HOLCF/Sprod.thy Thu Dec 11 16:50:18 2008 +0100 @@ -17,7 +17,7 @@ pcpodef (Sprod) ('a, 'b) "**" (infixr "**" 20) = "{p::'a \ 'b. p = \ \ (cfst\p \ \ \ csnd\p \ \)}" -by simp +by simp_all instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po by (rule typedef_finite_po [OF type_definition_Sprod]) diff -r 6f8a100325b6 -r 7619f0561cd7 src/HOLCF/Ssum.thy --- a/src/HOLCF/Ssum.thy Thu Dec 11 16:30:35 2008 +0100 +++ b/src/HOLCF/Ssum.thy Thu Dec 11 16:50:18 2008 +0100 @@ -19,7 +19,7 @@ "{p :: tr \ ('a \ 'b). (cfst\p \ TT \ csnd\(csnd\p) = \) \ (cfst\p \ FF \ cfst\(csnd\p) = \)}" -by simp +by simp_all instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po by (rule typedef_finite_po [OF type_definition_Ssum]) diff -r 6f8a100325b6 -r 7619f0561cd7 src/HOLCF/Tools/pcpodef_package.ML --- a/src/HOLCF/Tools/pcpodef_package.ML Thu Dec 11 16:30:35 2008 +0100 +++ b/src/HOLCF/Tools/pcpodef_package.ML Thu Dec 11 16:50:18 2008 +0100 @@ -47,11 +47,11 @@ error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT)); (*goal*) - val goal_UU_mem = HOLogic.mk_mem (Const (@{const_name UU}, oldT), set); - val goal_nonempty = HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)); - val goal_admissible = mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)); - val goal = HOLogic.mk_Trueprop - (HOLogic.mk_conj (if pcpo then goal_UU_mem else goal_nonempty, goal_admissible)); + val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set)); + val goal_nonempty = + HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); + val goal_admissible = + HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); (*lhs*) val defS = Sign.defaultS thy; @@ -107,10 +107,10 @@ |> Sign.parent_path end; - fun make_pcpo UUmem (type_def, less_def, set_def) theory = + fun make_pcpo UU_mem (type_def, less_def, set_def) theory = let - val UUmem' = fold_rule (the_list set_def) UUmem; - val pcpo_thms = map (Thm.transfer theory) [type_def, less_def, UUmem']; + val UU_mem' = fold_rule (the_list set_def) UU_mem; + val pcpo_thms = map (Thm.transfer theory) [type_def, less_def, UU_mem']; val theory' = theory |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1); @@ -130,27 +130,18 @@ |> Sign.parent_path end; - fun pcpodef_result UUmem_admissible theory = - let - val UUmem = UUmem_admissible RS conjunct1; - val admissible = UUmem_admissible RS conjunct2; - in - theory - |> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1) - |-> (fn defs => make_cpo admissible defs #> make_pcpo UUmem defs) - end; + fun pcpodef_result UU_mem admissible = + make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1) + #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs); - fun cpodef_result nonempty_admissible theory = - let - val nonempty = nonempty_admissible RS conjunct1; - val admissible = nonempty_admissible RS conjunct2; - in - theory - |> make_po (Tactic.rtac nonempty 1) - |-> make_cpo admissible - end; - - in (goal, if pcpo then pcpodef_result else cpodef_result) end + fun cpodef_result nonempty admissible = + make_po (Tactic.rtac nonempty 1) + #-> make_cpo admissible; + in + if pcpo + then (goal_UU_mem, goal_admissible, pcpodef_result) + else (goal_nonempty, goal_admissible, cpodef_result) + end handle ERROR msg => err_in_cpodef msg name; @@ -160,10 +151,10 @@ fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy = let - val (goal, pcpodef_result) = + val (goal1, goal2, make_result) = prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy; - fun after_qed [[th]] = ProofContext.theory (pcpodef_result th); - in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end; + fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2); + in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end; in