# HG changeset patch # User huffman # Date 1258065089 28800 # Node ID 053ac8080c11aebc72e35cfad691e42bf6ce9a21 # Parent d2f3104ca3d20669b2e90161418d3362aebbc766# Parent af07d9cd86cef5a947a90536bab01ddacb4b8d8c merged diff -r af07d9cd86ce -r 053ac8080c11 src/HOLCF/Tools/pcpodef.ML --- a/src/HOLCF/Tools/pcpodef.ML Thu Nov 12 20:33:26 2009 +0100 +++ b/src/HOLCF/Tools/pcpodef.ML Thu Nov 12 14:31:29 2009 -0800 @@ -7,14 +7,31 @@ signature PCPODEF = sig + type cpo_info = + { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm, + lub: thm, thelub: thm, compact: thm } + type pcpo_info = + { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm, + Rep_defined: thm, Abs_defined: thm } + + val add_podef: bool -> binding option -> binding * string list * mixfix -> + term -> (binding * binding) option -> tactic -> theory -> + (Typedef.info * thm) * theory + val add_cpodef: bool -> binding option -> binding * string list * mixfix -> + term -> (binding * binding) option -> tactic * tactic -> theory -> + (Typedef.info * cpo_info) * theory + val add_pcpodef: bool -> binding option -> binding * string list * mixfix -> + term -> (binding * binding) option -> tactic * tactic -> theory -> + (Typedef.info * cpo_info * pcpo_info) * theory + + val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term + * (binding * binding) option -> theory -> Proof.state + val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string + * (binding * binding) option -> theory -> Proof.state val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term * (binding * binding) option -> theory -> Proof.state val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string * (binding * binding) option -> theory -> Proof.state - val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term - * (binding * binding) option -> theory -> Proof.state - val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string - * (binding * binding) option -> theory -> Proof.state end; structure Pcpodef :> PCPODEF = @@ -22,22 +39,124 @@ (** type definitions **) -(* prepare_cpodef *) +type cpo_info = + { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm, + lub: thm, thelub: thm, compact: thm } -fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); +type pcpo_info = + { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm, + Rep_defined: thm, Abs_defined: thm } + +(* building terms *) fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT); fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P); -fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy = +fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT); + +(* manipulating theorems *) + +fun fold_adm_mem thm NONE = thm + | fold_adm_mem thm (SOME set_def) = + let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp} + in rule OF [set_def, thm] end; + +fun fold_UU_mem thm NONE = thm + | fold_UU_mem thm (SOME set_def) = + let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp} + in rule OF [set_def, thm] end; + +(* proving class instances *) + +fun prove_cpo + (name: binding) + (newT: typ) + (Rep_name: binding, Abs_name: binding) + (type_definition: thm) (* type_definition Rep Abs A *) + (set_def: thm option) (* A == set *) + (below_def: thm) (* op << == %x y. Rep x << Rep y *) + (admissible: thm) (* adm (%x. x : set) *) + (thy: theory) + = + let + val admissible' = fold_adm_mem admissible set_def; + val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible']; + val (full_tname, Ts) = dest_Type newT; + val lhs_sorts = map (snd o dest_TFree) Ts; + val thy2 = + thy + |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) + (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1); + val cpo_thms' = map (Thm.transfer thy2) cpo_thms; + fun make thm = Drule.standard (thm OF cpo_thms'); + val ([adm, cont_Rep, cont_Abs, lub, thelub, compact], thy3) = + thy2 + |> Sign.add_path (Binding.name_of name) + |> PureThy.add_thms + ([((Binding.prefix_name "adm_" name, admissible'), []), + ((Binding.prefix_name "cont_" Rep_name, make @{thm typedef_cont_Rep}), []), + ((Binding.prefix_name "cont_" Abs_name, make @{thm typedef_cont_Abs}), []), + ((Binding.prefix_name "lub_" name, make @{thm typedef_lub}), []), + ((Binding.prefix_name "thelub_" name, make @{thm typedef_thelub}), []), + ((Binding.prefix_name "compact_" name, make @{thm typedef_compact}), [])]) + ||> Sign.parent_path; + val cpo_info : cpo_info = + { below_def = below_def, adm = admissible', cont_Rep = cont_Rep, + cont_Abs = cont_Abs, lub = lub, thelub = thelub, compact = compact }; + in + (cpo_info, thy3) + end; + +fun prove_pcpo + (name: binding) + (newT: typ) + (Rep_name: binding, Abs_name: binding) + (type_definition: thm) (* type_definition Rep Abs A *) + (set_def: thm option) (* A == set *) + (below_def: thm) (* op << == %x y. Rep x << Rep y *) + (UU_mem: thm) (* UU : set *) + (thy: theory) + = + let + val UU_mem' = fold_UU_mem UU_mem set_def; + val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem']; + val (full_tname, Ts) = dest_Type newT; + val lhs_sorts = map (snd o dest_TFree) Ts; + val thy2 = thy + |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) + (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1); + val pcpo_thms' = map (Thm.transfer thy2) pcpo_thms; + fun make thm = Drule.standard (thm OF pcpo_thms'); + val ([Rep_strict, Abs_strict, Rep_strict_iff, Abs_strict_iff, + Rep_defined, Abs_defined], thy3) = + thy2 + |> Sign.add_path (Binding.name_of name) + |> PureThy.add_thms + ([((Binding.suffix_name "_strict" Rep_name, make @{thm typedef_Rep_strict}), []), + ((Binding.suffix_name "_strict" Abs_name, make @{thm typedef_Abs_strict}), []), + ((Binding.suffix_name "_strict_iff" Rep_name, make @{thm typedef_Rep_strict_iff}), []), + ((Binding.suffix_name "_strict_iff" Abs_name, make @{thm typedef_Abs_strict_iff}), []), + ((Binding.suffix_name "_defined" Rep_name, make @{thm typedef_Rep_defined}), []), + ((Binding.suffix_name "_defined" Abs_name, make @{thm typedef_Abs_defined}), [])]) + ||> Sign.parent_path; + val pcpo_info = + { Rep_strict = Rep_strict, Abs_strict = Abs_strict, + Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff, + Rep_defined = Rep_defined, Abs_defined = Abs_defined }; + in + (pcpo_info, thy3) + end; + +(* prepare_cpodef *) + +fun declare_type_name a = + Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS))); + +fun prepare prep_term _ name (t, vs, mx) raw_set opt_morphs thy = let val _ = Theory.requires thy "Pcpodef" "pcpodefs"; val ctxt = ProofContext.init thy; - val full = Sign.full_name thy; - val full_name = full name; - val bname = Binding.name_of name; - (*rhs*) val set = prep_term (ctxt |> fold declare_type_name vs) raw_set; val setT = Term.fastype_of set; @@ -45,129 +164,171 @@ val oldT = HOLogic.dest_setT setT handle TYPE _ => error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT)); - (*goal*) - val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set)); + (*lhs*) + val defS = Sign.defaultS thy; + val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; + val lhs_sorts = map snd lhs_tfrees; + val tname = Binding.map_name (Syntax.type_name mx) t; + val full_tname = Sign.full_name thy tname; + val newT = Type (full_tname, map TFree lhs_tfrees); + + val morphs = opt_morphs + |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name); + in + (newT, oldT, set, morphs, lhs_sorts) + end + +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 {type_definition, set_def, Rep_name, ...}), thy2) = thy + |> Typedef.add_typedef def opt_name typ set opt_morphs tac; + val oldT = #rep_type info; + val newT = #abs_type info; + val lhs_tfrees = map dest_TFree (snd (dest_Type newT)); + + val RepC = Const (Rep_name, newT --> oldT); + val below_def = Logic.mk_equals (below_const newT, + Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))); + val lthy3 = thy2 + |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po}); + val below_def' = Syntax.check_term lthy3 below_def; + val ((_, (_, below_definition')), lthy4) = lthy3 + |> Specification.definition (NONE, + ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def')); + val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4); + val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition'; + val thy5 = lthy4 + |> Class.prove_instantiation_instance + (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1)) + |> LocalTheory.exit_global; + in ((info, below_definition), thy5) end; + +fun prepare_cpodef + (prep_term: Proof.context -> 'a -> term) + (def: bool) + (name: binding) + (typ: binding * string list * mixfix) + (raw_set: 'a) + (opt_morphs: (binding * binding) option) + (thy: theory) + : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) = + let + val (newT, oldT, set, morphs as (Rep_name, Abs_name), lhs_sorts) = + prepare prep_term def name typ raw_set opt_morphs thy; + 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; - val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs; - val lhs_sorts = map snd lhs_tfrees; - - val tname = Binding.map_name (Syntax.type_name mx) t; - val full_tname = full tname; - val newT = Type (full_tname, map TFree lhs_tfrees); - - val (Rep_name, Abs_name) = - (case opt_morphs of - NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name) - | SOME morphs => morphs); - val RepC = Const (full Rep_name, newT --> oldT); - fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT); - val below_def = Logic.mk_equals (belowC newT, - Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))); - - fun make_po tac thy1 = + fun cpodef_result nonempty admissible thy = let - val ((_, {type_definition, set_def, ...}), thy2) = thy1 - |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac; - val lthy3 = thy2 - |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po}); - val below_def' = Syntax.check_term lthy3 below_def; - val ((_, (_, below_definition')), lthy4) = lthy3 - |> Specification.definition (NONE, - ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def')); - val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4); - val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition'; - val thy5 = lthy4 - |> Class.prove_instantiation_instance - (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1)) - |> LocalTheory.exit_global; - in ((type_definition, below_definition, set_def), thy5) end; - - fun make_cpo admissible (type_def, below_def, set_def) theory = - let - (* FIXME fold_rule might fold user input inintentionally *) - val admissible' = fold_rule (the_list set_def) admissible; - val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible']; - val theory' = theory - |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) - (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1); - val cpo_thms' = map (Thm.transfer theory') cpo_thms; + val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy + |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1); + val (cpo_info, thy3) = thy2 + |> prove_cpo name newT morphs type_definition set_def below_def admissible; in - theory' - |> Sign.add_path (Binding.name_of name) - |> PureThy.add_thms - ([((Binding.prefix_name "adm_" name, admissible'), []), - ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []), - ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []), - ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []), - ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []), - ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])]) - |> snd - |> Sign.parent_path + ((info, cpo_info), thy3) end; - - fun make_pcpo UU_mem (type_def, below_def, set_def) theory = - let - (* FIXME fold_rule might fold user input inintentionally *) - val UU_mem' = fold_rule (the_list set_def) UU_mem; - val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem']; - val theory' = theory - |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) - (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1); - val pcpo_thms' = map (Thm.transfer theory') pcpo_thms; - in - theory' - |> Sign.add_path (Binding.name_of name) - |> PureThy.add_thms - ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []), - ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []), - ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []), - ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []), - ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []), - ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])]) - |> snd - |> Sign.parent_path - 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 = - 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) + (goal_nonempty, goal_admissible, cpodef_result) end handle ERROR msg => cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name)); +fun prepare_pcpodef + (prep_term: Proof.context -> 'a -> term) + (def: bool) + (name: binding) + (typ: binding * string 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 (newT, oldT, set, morphs as (Rep_name, Abs_name), lhs_sorts) = + prepare prep_term def name typ raw_set opt_morphs thy; + + val goal_UU_mem = + HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set)); + + val goal_admissible = + HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set))); + + 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 + |> add_podef def (SOME name) typ set opt_morphs tac; + val (cpo_info, thy3) = thy2 + |> prove_cpo name newT morphs type_definition set_def below_def admissible; + val (pcpo_info, thy4) = thy3 + |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem; + in + ((info, cpo_info, pcpo_info), thy4) + end; + in + (goal_UU_mem, goal_admissible, pcpodef_result) + end + handle ERROR msg => + cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name)); + + +(* tactic interface *) + +fun add_cpodef def opt_name 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; + 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)); + val thm2 = Goal.prove_global thy [] [] goal2 (K tac2) + handle ERROR msg => cat_error msg + ("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 = + 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; + 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)); + val thm2 = Goal.prove_global thy [] [] goal2 (K tac2) + handle ERROR msg => cat_error msg + ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set)); + in pcpodef_result thm1 thm2 thy end; + (* proof interface *) local -fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy = +fun gen_cpodef_proof prep_term ((def, name), typ, set, opt_morphs) thy = let val (goal1, goal2, make_result) = - prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy; - fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2); + prepare_cpodef prep_term def name typ set opt_morphs thy; + fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2); + in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end; + +fun gen_pcpodef_proof prep_term ((def, name), typ, set, opt_morphs) thy = + let + val (goal1, goal2, make_result) = + prepare_pcpodef prep_term def name typ set opt_morphs thy; + fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2); in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end; in -fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x; -fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x; +fun cpodef_proof x = gen_cpodef_proof Syntax.check_term x; +fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term x; -fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x; -fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x; +fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term x; +fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term x; end;