1.1 --- a/src/HOLCF/Cfun.thy Thu Dec 11 16:30:35 2008 +0100
1.2 +++ b/src/HOLCF/Cfun.thy Thu Dec 11 16:50:18 2008 +0100
1.3 @@ -23,7 +23,7 @@
1.4 by (rule admI, rule cont_lub_fun)
1.5
1.6 cpodef (CFun) ('a, 'b) "->" (infixr "->" 0) = "{f::'a => 'b. cont f}"
1.7 -by (simp add: Ex_cont adm_cont)
1.8 +by (simp_all add: Ex_cont adm_cont)
1.9
1.10 syntax (xsymbols)
1.11 "->" :: "[type, type] => type" ("(_ \<rightarrow>/ _)" [1,0]0)
2.1 --- a/src/HOLCF/Fixrec.thy Thu Dec 11 16:30:35 2008 +0100
2.2 +++ b/src/HOLCF/Fixrec.thy Thu Dec 11 16:50:18 2008 +0100
2.3 @@ -15,7 +15,7 @@
2.4 defaultsort cpo
2.5
2.6 pcpodef (open) 'a maybe = "UNIV::(one ++ 'a u) set"
2.7 -by simp
2.8 +by simp_all
2.9
2.10 constdefs
2.11 fail :: "'a maybe"
3.1 --- a/src/HOLCF/Lift.thy Thu Dec 11 16:30:35 2008 +0100
3.2 +++ b/src/HOLCF/Lift.thy Thu Dec 11 16:50:18 2008 +0100
3.3 @@ -12,7 +12,7 @@
3.4 defaultsort type
3.5
3.6 pcpodef 'a lift = "UNIV :: 'a discr u set"
3.7 -by simp
3.8 +by simp_all
3.9
3.10 instance lift :: (finite) finite_po
3.11 by (rule typedef_finite_po [OF type_definition_lift])
4.1 --- a/src/HOLCF/Sprod.thy Thu Dec 11 16:30:35 2008 +0100
4.2 +++ b/src/HOLCF/Sprod.thy Thu Dec 11 16:50:18 2008 +0100
4.3 @@ -17,7 +17,7 @@
4.4
4.5 pcpodef (Sprod) ('a, 'b) "**" (infixr "**" 20) =
4.6 "{p::'a \<times> 'b. p = \<bottom> \<or> (cfst\<cdot>p \<noteq> \<bottom> \<and> csnd\<cdot>p \<noteq> \<bottom>)}"
4.7 -by simp
4.8 +by simp_all
4.9
4.10 instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
4.11 by (rule typedef_finite_po [OF type_definition_Sprod])
5.1 --- a/src/HOLCF/Ssum.thy Thu Dec 11 16:30:35 2008 +0100
5.2 +++ b/src/HOLCF/Ssum.thy Thu Dec 11 16:50:18 2008 +0100
5.3 @@ -19,7 +19,7 @@
5.4 "{p :: tr \<times> ('a \<times> 'b).
5.5 (cfst\<cdot>p \<sqsubseteq> TT \<longleftrightarrow> csnd\<cdot>(csnd\<cdot>p) = \<bottom>) \<and>
5.6 (cfst\<cdot>p \<sqsubseteq> FF \<longleftrightarrow> cfst\<cdot>(csnd\<cdot>p) = \<bottom>)}"
5.7 -by simp
5.8 +by simp_all
5.9
5.10 instance "++" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
5.11 by (rule typedef_finite_po [OF type_definition_Ssum])
6.1 --- a/src/HOLCF/Tools/pcpodef_package.ML Thu Dec 11 16:30:35 2008 +0100
6.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML Thu Dec 11 16:50:18 2008 +0100
6.3 @@ -47,11 +47,11 @@
6.4 error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
6.5
6.6 (*goal*)
6.7 - val goal_UU_mem = HOLogic.mk_mem (Const (@{const_name UU}, oldT), set);
6.8 - val goal_nonempty = HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set));
6.9 - val goal_admissible = mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set));
6.10 - val goal = HOLogic.mk_Trueprop
6.11 - (HOLogic.mk_conj (if pcpo then goal_UU_mem else goal_nonempty, goal_admissible));
6.12 + val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
6.13 + val goal_nonempty =
6.14 + HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
6.15 + val goal_admissible =
6.16 + HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
6.17
6.18 (*lhs*)
6.19 val defS = Sign.defaultS thy;
6.20 @@ -107,10 +107,10 @@
6.21 |> Sign.parent_path
6.22 end;
6.23
6.24 - fun make_pcpo UUmem (type_def, less_def, set_def) theory =
6.25 + fun make_pcpo UU_mem (type_def, less_def, set_def) theory =
6.26 let
6.27 - val UUmem' = fold_rule (the_list set_def) UUmem;
6.28 - val pcpo_thms = map (Thm.transfer theory) [type_def, less_def, UUmem'];
6.29 + val UU_mem' = fold_rule (the_list set_def) UU_mem;
6.30 + val pcpo_thms = map (Thm.transfer theory) [type_def, less_def, UU_mem'];
6.31 val theory' = theory
6.32 |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
6.33 (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
6.34 @@ -130,27 +130,18 @@
6.35 |> Sign.parent_path
6.36 end;
6.37
6.38 - fun pcpodef_result UUmem_admissible theory =
6.39 - let
6.40 - val UUmem = UUmem_admissible RS conjunct1;
6.41 - val admissible = UUmem_admissible RS conjunct2;
6.42 - in
6.43 - theory
6.44 - |> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1)
6.45 - |-> (fn defs => make_cpo admissible defs #> make_pcpo UUmem defs)
6.46 - end;
6.47 + fun pcpodef_result UU_mem admissible =
6.48 + make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1)
6.49 + #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs);
6.50
6.51 - fun cpodef_result nonempty_admissible theory =
6.52 - let
6.53 - val nonempty = nonempty_admissible RS conjunct1;
6.54 - val admissible = nonempty_admissible RS conjunct2;
6.55 - in
6.56 - theory
6.57 - |> make_po (Tactic.rtac nonempty 1)
6.58 - |-> make_cpo admissible
6.59 - end;
6.60 -
6.61 - in (goal, if pcpo then pcpodef_result else cpodef_result) end
6.62 + fun cpodef_result nonempty admissible =
6.63 + make_po (Tactic.rtac nonempty 1)
6.64 + #-> make_cpo admissible;
6.65 + in
6.66 + if pcpo
6.67 + then (goal_UU_mem, goal_admissible, pcpodef_result)
6.68 + else (goal_nonempty, goal_admissible, cpodef_result)
6.69 + end
6.70 handle ERROR msg => err_in_cpodef msg name;
6.71
6.72
6.73 @@ -160,10 +151,10 @@
6.74
6.75 fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
6.76 let
6.77 - val (goal, pcpodef_result) =
6.78 + val (goal1, goal2, make_result) =
6.79 prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
6.80 - fun after_qed [[th]] = ProofContext.theory (pcpodef_result th);
6.81 - in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end;
6.82 + fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2);
6.83 + in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
6.84
6.85 in
6.86