# HG changeset patch # User huffman # Date 1349796826 -7200 # Node ID ecf1d5d87e5ef9f5d964a039fcccfaf1e7bb1351 # Parent 718f10c8bbfcd40dc9314dec017b82300c62f465 removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands; removed '(open)', '(set_name)' and '(open set_name)' options diff -r 718f10c8bbfc -r ecf1d5d87e5e src/HOL/HOLCF/Cfun.thy --- a/src/HOL/HOLCF/Cfun.thy Tue Oct 09 16:58:36 2012 +0200 +++ b/src/HOL/HOLCF/Cfun.thy Tue Oct 09 17:33:46 2012 +0200 @@ -15,7 +15,7 @@ definition "cfun = {f::'a => 'b. cont f}" -cpodef (open) ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set" +cpodef ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set" unfolding cfun_def by (auto intro: cont_const adm_cont) type_notation (xsymbols) diff -r 718f10c8bbfc -r ecf1d5d87e5e src/HOL/HOLCF/Fixrec.thy --- a/src/HOL/HOLCF/Fixrec.thy Tue Oct 09 16:58:36 2012 +0200 +++ b/src/HOL/HOLCF/Fixrec.thy Tue Oct 09 17:33:46 2012 +0200 @@ -13,7 +13,7 @@ default_sort cpo -pcpodef (open) 'a match = "UNIV::(one ++ 'a u) set" +pcpodef 'a match = "UNIV::(one ++ 'a u) set" by simp_all definition diff -r 718f10c8bbfc -r ecf1d5d87e5e src/HOL/HOLCF/Lift.thy --- a/src/HOL/HOLCF/Lift.thy Tue Oct 09 16:58:36 2012 +0200 +++ b/src/HOL/HOLCF/Lift.thy Tue Oct 09 17:33:46 2012 +0200 @@ -10,7 +10,7 @@ default_sort type -pcpodef (open) 'a lift = "UNIV :: 'a discr u set" +pcpodef 'a lift = "UNIV :: 'a discr u set" by simp_all lemmas inst_lift_pcpo = Abs_lift_strict [symmetric] diff -r 718f10c8bbfc -r ecf1d5d87e5e src/HOL/HOLCF/Sfun.thy --- a/src/HOL/HOLCF/Sfun.thy Tue Oct 09 16:58:36 2012 +0200 +++ b/src/HOL/HOLCF/Sfun.thy Tue Oct 09 17:33:46 2012 +0200 @@ -8,7 +8,7 @@ imports Cfun begin -pcpodef (open) ('a, 'b) sfun (infixr "->!" 0) +pcpodef ('a, 'b) sfun (infixr "->!" 0) = "{f :: 'a \ 'b. f\\ = \}" by simp_all diff -r 718f10c8bbfc -r ecf1d5d87e5e src/HOL/HOLCF/Sprod.thy --- a/src/HOL/HOLCF/Sprod.thy Tue Oct 09 16:58:36 2012 +0200 +++ b/src/HOL/HOLCF/Sprod.thy Tue Oct 09 17:33:46 2012 +0200 @@ -15,7 +15,7 @@ definition "sprod = {p::'a \ 'b. p = \ \ (fst p \ \ \ snd p \ \)}" -pcpodef (open) ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \ 'b) set" +pcpodef ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \ 'b) set" unfolding sprod_def by simp_all instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin diff -r 718f10c8bbfc -r ecf1d5d87e5e src/HOL/HOLCF/Ssum.thy --- a/src/HOL/HOLCF/Ssum.thy Tue Oct 09 16:58:36 2012 +0200 +++ b/src/HOL/HOLCF/Ssum.thy Tue Oct 09 17:33:46 2012 +0200 @@ -19,7 +19,7 @@ (fst p = TT \ fst (snd p) \ \ \ snd (snd p) = \) \ (fst p = FF \ fst (snd p) = \ \ snd (snd p) \ \)}" -pcpodef (open) ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \ 'a \ 'b) set" +pcpodef ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \ 'a \ 'b) set" unfolding ssum_def by simp_all instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin diff -r 718f10c8bbfc -r ecf1d5d87e5e src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Oct 09 16:58:36 2012 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Tue Oct 09 17:33:46 2012 +0200 @@ -519,7 +519,7 @@ let val spec = (tbind, map (rpair dummyS) vs, mx) val ((_, _, _, {DEFL, ...}), thy) = - Domaindef.add_domaindef false NONE spec defl NONE thy + Domaindef.add_domaindef spec defl NONE thy (* declare domain_defl_simps rules *) val thy = Context.theory_map (RepData.add_thm DEFL) thy in diff -r 718f10c8bbfc -r ecf1d5d87e5e src/HOL/HOLCF/Tools/cpodef.ML --- a/src/HOL/HOLCF/Tools/cpodef.ML Tue Oct 09 16:58:36 2012 +0200 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Tue Oct 09 17:33:46 2012 +0200 @@ -14,27 +14,27 @@ { Rep_strict: thm, Abs_strict: thm, Rep_bottom_iff: thm, Abs_bottom_iff: thm } - val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix -> + val add_podef: binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic -> theory -> (Typedef.info * thm) * theory - val add_cpodef: bool -> binding option -> binding * (string * sort) list * mixfix -> + val add_cpodef: binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic * tactic -> theory -> (Typedef.info * cpo_info) * theory - val add_pcpodef: bool -> binding option -> binding * (string * sort) list * mixfix -> + val add_pcpodef: binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic * tactic -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory - val cpodef_proof: (bool * binding) - * (binding * (string * sort) list * mixfix) * term + val cpodef_proof: + (binding * (string * sort) list * mixfix) * term * (binding * binding) option -> theory -> Proof.state - val cpodef_proof_cmd: (bool * binding) - * (binding * (string * string option) list * mixfix) * string + val cpodef_proof_cmd: + (binding * (string * string option) list * mixfix) * string * (binding * binding) option -> theory -> Proof.state - val pcpodef_proof: (bool * binding) - * (binding * (string * sort) list * mixfix) * term + val pcpodef_proof: + (binding * (string * sort) list * mixfix) * term * (binding * binding) option -> theory -> Proof.state - val pcpodef_proof_cmd: (bool * binding) - * (binding * (string * string option) list * mixfix) * string + val pcpodef_proof_cmd: + (binding * (string * string option) list * mixfix) * string * (binding * binding) option -> theory -> Proof.state end @@ -180,11 +180,11 @@ (newT, oldT, set, morphs) end -fun add_podef def opt_name typ set opt_morphs tac thy = +fun add_podef typ set opt_morphs tac thy = let - val name = the_default (#1 typ) opt_name + val name = #1 typ val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy - |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac + |> Typedef.add_typedef_global false NONE typ set opt_morphs tac val oldT = #rep_type (#1 info) val newT = #abs_type (#1 info) val lhs_tfrees = map dest_TFree (snd (dest_Type newT)) @@ -205,14 +205,13 @@ fun prepare_cpodef (prep_term: Proof.context -> 'a -> term) - (def: bool) - (name: binding) (typ: binding * (string * sort) list * mixfix) (raw_set: 'a) (opt_morphs: (binding * binding) option) (thy: theory) : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) = let + val name = #1 typ val (newT, oldT, set, morphs) = prepare prep_term name typ raw_set opt_morphs thy @@ -224,7 +223,7 @@ fun cpodef_result nonempty admissible thy = let val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy - |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1) + |> add_podef typ set opt_morphs (Tactic.rtac nonempty 1) val (cpo_info, thy) = thy |> prove_cpo name newT morphs type_definition set_def below_def admissible in @@ -234,18 +233,17 @@ (goal_nonempty, goal_admissible, cpodef_result) end handle ERROR msg => - cat_error msg ("The error(s) above occurred in cpodef " ^ Binding.print name) + cat_error msg ("The error(s) above occurred in cpodef " ^ Binding.print (#1 typ)) fun prepare_pcpodef (prep_term: Proof.context -> 'a -> term) - (def: bool) - (name: binding) (typ: binding * (string * sort) list * mixfix) (raw_set: 'a) (opt_morphs: (binding * binding) option) (thy: theory) : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) = let + val name = #1 typ val (newT, oldT, set, morphs) = prepare prep_term name typ raw_set opt_morphs thy @@ -259,7 +257,7 @@ let val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1 val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy - |> add_podef def (SOME name) typ set opt_morphs tac + |> add_podef typ set opt_morphs tac val (cpo_info, thy) = thy |> prove_cpo name newT morphs type_definition set_def below_def admissible val (pcpo_info, thy) = thy @@ -271,16 +269,15 @@ (goal_bottom_mem, goal_admissible, pcpodef_result) end handle ERROR msg => - cat_error msg ("The error(s) above occurred in pcpodef " ^ Binding.print name) + cat_error msg ("The error(s) above occurred in pcpodef " ^ Binding.print (#1 typ)) (* tactic interface *) -fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy = +fun add_cpodef typ set opt_morphs (tac1, tac2) thy = let - val name = the_default (#1 typ) opt_name val (goal1, goal2, cpodef_result) = - prepare_cpodef Syntax.check_term def name typ set opt_morphs thy + prepare_cpodef Syntax.check_term typ set opt_morphs thy val thm1 = Goal.prove_global thy [] [] goal1 (K tac1) handle ERROR msg => cat_error msg ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) @@ -289,11 +286,10 @@ ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)) in cpodef_result thm1 thm2 thy end -fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy = +fun add_pcpodef typ set opt_morphs (tac1, tac2) thy = let - val name = the_default (#1 typ) opt_name val (goal1, goal2, pcpodef_result) = - prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy + prepare_pcpodef Syntax.check_term typ set opt_morphs thy val thm1 = Goal.prove_global thy [] [] goal1 (K tac1) handle ERROR msg => cat_error msg ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set)) @@ -308,23 +304,23 @@ local fun gen_cpodef_proof prep_term prep_constraint - ((def, name), (b, raw_args, mx), set, opt_morphs) thy = + ((b, raw_args, mx), set, opt_morphs) thy = let val ctxt = Proof_Context.init_global thy val args = map (apsnd (prep_constraint ctxt)) raw_args val (goal1, goal2, make_result) = - prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy + prepare_cpodef prep_term (b, args, mx) set opt_morphs thy fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2) | after_qed _ = raise Fail "cpodef_proof" in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end fun gen_pcpodef_proof prep_term prep_constraint - ((def, name), (b, raw_args, mx), set, opt_morphs) thy = + ((b, raw_args, mx), set, opt_morphs) thy = let val ctxt = Proof_Context.init_global thy val args = map (apsnd (prep_constraint ctxt)) raw_args val (goal1, goal2, make_result) = - prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy + prepare_pcpodef prep_term (b, args, mx) set opt_morphs thy fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2) | after_qed _ = raise Fail "pcpodef_proof" in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end @@ -344,17 +340,14 @@ (** outer syntax **) val typedef_proof_decl = - Scan.optional (@{keyword "("} |-- - ((@{keyword "open"} >> K false) -- Scan.option Parse.binding || - Parse.binding >> (fn s => (true, SOME s))) - --| @{keyword ")"}) (true, NONE) -- - (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix -- - (@{keyword "="} |-- Parse.term) -- - Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) + (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix -- + (@{keyword "="} |-- Parse.term) -- + Scan.option + (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) -fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) = +fun mk_pcpodef_proof pcpo ((((args, t), mx), A), morphs) = (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd) - ((def, the_default t opt_name), (t, args, mx), A, morphs) + ((t, args, mx), A, morphs) val _ = Outer_Syntax.command @{command_spec "pcpodef"} diff -r 718f10c8bbfc -r ecf1d5d87e5e src/HOL/HOLCF/Tools/domaindef.ML --- a/src/HOL/HOLCF/Tools/domaindef.ML Tue Oct 09 16:58:36 2012 +0200 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Tue Oct 09 17:33:46 2012 +0200 @@ -17,11 +17,11 @@ DEFL : thm } - val add_domaindef: bool -> binding option -> binding * (string * sort) list * mixfix -> + val add_domaindef: binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> theory -> (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory - val domaindef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string + val domaindef_cmd: (binding * (string * string option) list * mixfix) * string * (binding * binding) option -> theory -> theory end @@ -78,8 +78,6 @@ fun gen_add_domaindef (prep_term: Proof.context -> 'a -> term) - (def: bool) - (name: binding) (typ as (tname, raw_args, _) : binding * (string * sort) list * mixfix) (raw_defl: 'a) (opt_morphs: (binding * binding) option) @@ -106,7 +104,7 @@ (*morphisms*) val morphs = opt_morphs - |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name) + |> the_default (Binding.prefix_name "Rep_" tname, Binding.prefix_name "Abs_" tname) (*set*) val set = @{term "defl_set :: udom defl => udom set"} $ defl @@ -115,7 +113,7 @@ val tac1 = rtac @{thm defl_set_bottom} 1 val tac2 = rtac @{thm adm_defl_set} 1 val ((info, cpo_info, pcpo_info), thy) = thy - |> Cpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2) + |> Cpodef.add_pcpodef typ set (SOME morphs) (tac1, tac2) (*definitions*) val Rep_const = Const (#Rep_name (#1 info), newT --> udomT) @@ -134,7 +132,7 @@ Abs ("t", Term.itselfT newT, mk_capply (@{const liftdefl_of}, defl_const newT $ Logic.mk_type newT))) - val name_def = Thm.def_binding name + val name_def = Thm.def_binding tname val emb_bind = (Binding.prefix_name "emb_" name_def, []) val prj_bind = (Binding.prefix_name "prj_" name_def, []) val defl_bind = (Binding.prefix_name "defl_" name_def, []) @@ -179,9 +177,9 @@ (*other theorems*) val defl_thm' = Thm.transfer thy defl_def val (DEFL_thm, thy) = thy - |> Sign.add_path (Binding.name_of name) + |> Sign.add_path (Binding.name_of tname) |> Global_Theory.add_thm - ((Binding.prefix_name "DEFL_" name, + ((Binding.prefix_name "DEFL_" tname, Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), []) ||> Sign.restore_naming thy @@ -193,35 +191,28 @@ ((info, cpo_info, pcpo_info, rep_info), thy) end handle ERROR msg => - cat_error msg ("The error(s) above occurred in domaindef " ^ Binding.print name) + cat_error msg ("The error(s) above occurred in domaindef " ^ Binding.print tname) -fun add_domaindef def opt_name typ defl opt_morphs thy = - let - val name = the_default (#1 typ) opt_name - in - gen_add_domaindef Syntax.check_term def name typ defl opt_morphs thy - end +fun add_domaindef typ defl opt_morphs thy = + gen_add_domaindef Syntax.check_term typ defl opt_morphs thy -fun domaindef_cmd ((def, name), (b, raw_args, mx), A, morphs) thy = +fun domaindef_cmd ((b, raw_args, mx), A, morphs) thy = let val ctxt = Proof_Context.init_global thy val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args - in snd (gen_add_domaindef Syntax.read_term def name (b, args, mx) A morphs thy) end + in snd (gen_add_domaindef Syntax.read_term (b, args, mx) A morphs thy) end (** outer syntax **) val domaindef_decl = - Scan.optional (@{keyword "("} |-- - ((@{keyword "open"} >> K false) -- Scan.option Parse.binding || - Parse.binding >> (fn s => (true, SOME s))) - --| @{keyword ")"}) (true, NONE) -- - (Parse.type_args_constrained -- Parse.binding) -- - Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) -- - Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) + (Parse.type_args_constrained -- Parse.binding) -- + Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) -- + Scan.option + (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)) -fun mk_domaindef ((((((def, opt_name), (args, t)), mx), A), morphs)) = - domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs) +fun mk_domaindef (((((args, t)), mx), A), morphs) = + domaindef_cmd ((t, args, mx), A, morphs) val _ = Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations" diff -r 718f10c8bbfc -r ecf1d5d87e5e src/HOL/HOLCF/ex/Domain_Proofs.thy --- a/src/HOL/HOLCF/ex/Domain_Proofs.thy Tue Oct 09 16:58:36 2012 +0200 +++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy Tue Oct 09 17:33:46 2012 +0200 @@ -80,13 +80,13 @@ text {* Use @{text pcpodef} with the appropriate type combinator. *} -pcpodef (open) 'a foo = "defl_set (foo_defl\DEFL('a))" +pcpodef 'a foo = "defl_set (foo_defl\DEFL('a))" by (rule defl_set_bottom, rule adm_defl_set) -pcpodef (open) 'a bar = "defl_set (bar_defl\DEFL('a))" +pcpodef 'a bar = "defl_set (bar_defl\DEFL('a))" by (rule defl_set_bottom, rule adm_defl_set) -pcpodef (open) 'a baz = "defl_set (baz_defl\DEFL('a))" +pcpodef 'a baz = "defl_set (baz_defl\DEFL('a))" by (rule defl_set_bottom, rule adm_defl_set) text {* Prove rep instance using lemma @{text typedef_rep_class}. *}