src/HOLCF/Tools/pcpodef.ML
changeset 33645 562635ab559b
parent 33553 35f2b30593a8
child 33646 d2f3104ca3d2
     1.1 --- a/src/HOLCF/Tools/pcpodef.ML	Wed Nov 11 17:27:48 2009 +0100
     1.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Wed Nov 11 10:15:32 2009 -0800
     1.3 @@ -7,6 +7,10 @@
     1.4  
     1.5  signature PCPODEF =
     1.6  sig
     1.7 +  val add_pcpodef: bool -> binding option -> binding * string list * mixfix ->
     1.8 +    term -> (binding * binding) option -> tactic -> theory -> theory
     1.9 +  val add_cpodef: bool -> binding option -> binding * string list * mixfix ->
    1.10 +    term -> (binding * binding) option -> tactic -> theory -> theory
    1.11    val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
    1.12      * (binding * binding) option -> theory -> Proof.state
    1.13    val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
    1.14 @@ -97,16 +101,17 @@
    1.15            |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
    1.16              (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
    1.17          val cpo_thms' = map (Thm.transfer theory') cpo_thms;
    1.18 +        fun make thm = Drule.standard (thm OF cpo_thms');
    1.19        in
    1.20          theory'
    1.21          |> Sign.add_path (Binding.name_of name)
    1.22          |> PureThy.add_thms
    1.23            ([((Binding.prefix_name "adm_" name, admissible'), []),
    1.24 -            ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
    1.25 -            ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
    1.26 -            ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []),
    1.27 -            ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []),
    1.28 -            ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])])
    1.29 +            ((Binding.prefix_name "cont_" Rep_name, make @{thm typedef_cont_Rep}), []),
    1.30 +            ((Binding.prefix_name "cont_" Abs_name, make @{thm typedef_cont_Abs}), []),
    1.31 +            ((Binding.prefix_name "lub_" name, make @{thm typedef_lub}), []),
    1.32 +            ((Binding.prefix_name "thelub_" name, make @{thm typedef_thelub}), []),
    1.33 +            ((Binding.prefix_name "compact_" name, make @{thm typedef_compact}), [])])
    1.34          |> snd
    1.35          |> Sign.parent_path
    1.36        end;
    1.37 @@ -120,16 +125,17 @@
    1.38            |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
    1.39              (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
    1.40          val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
    1.41 +        fun make thm = Drule.standard (thm OF pcpo_thms');
    1.42        in
    1.43          theory'
    1.44          |> Sign.add_path (Binding.name_of name)
    1.45          |> PureThy.add_thms
    1.46 -          ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []),
    1.47 -            ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []),
    1.48 -            ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
    1.49 -            ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
    1.50 -            ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []),
    1.51 -            ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])])
    1.52 +          ([((Binding.suffix_name "_strict" Rep_name, make @{thm typedef_Rep_strict}), []),
    1.53 +            ((Binding.suffix_name "_strict" Abs_name, make @{thm typedef_Abs_strict}), []),
    1.54 +            ((Binding.suffix_name "_strict_iff" Rep_name, make @{thm typedef_Rep_strict_iff}), []),
    1.55 +            ((Binding.suffix_name "_strict_iff" Abs_name, make @{thm typedef_Abs_strict_iff}), []),
    1.56 +            ((Binding.suffix_name "_defined" Rep_name, make @{thm typedef_Rep_defined}), []),
    1.57 +            ((Binding.suffix_name "_defined" Abs_name, make @{thm typedef_Abs_defined}), [])])
    1.58          |> snd
    1.59          |> Sign.parent_path
    1.60        end;
    1.61 @@ -150,6 +156,30 @@
    1.62      cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
    1.63  
    1.64  
    1.65 +(* tactic interface *)
    1.66 +
    1.67 +local
    1.68 +
    1.69 +fun gen_add_pcpodef pcpo def opt_name typ set opt_morphs tac thy =
    1.70 +  let
    1.71 +    val name = the_default (#1 typ) opt_name;
    1.72 +    val (goal1, goal2, pcpodef_result) =
    1.73 +      prepare_pcpodef Syntax.check_term pcpo def name typ set opt_morphs thy;
    1.74 +    val thm1 = Goal.prove_global thy [] [] goal1 (K tac)
    1.75 +      handle ERROR msg => cat_error msg
    1.76 +        ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
    1.77 +    val thm2 = Goal.prove_global thy [] [] goal2 (K tac)
    1.78 +      handle ERROR msg => cat_error msg
    1.79 +        ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
    1.80 +  in pcpodef_result thm1 thm2 thy end;
    1.81 +
    1.82 +in
    1.83 +
    1.84 +val add_pcpodef = gen_add_pcpodef true;
    1.85 +val add_cpodef = gen_add_pcpodef false;
    1.86 +
    1.87 +end;
    1.88 +
    1.89  (* proof interface *)
    1.90  
    1.91  local