src/HOLCF/Tools/pcpodef_package.ML
author haftmann
Tue, 02 Sep 2008 12:07:34 +0200
changeset 28073 5e9f00f4f209
parent 27691 ce171cbd4b93
child 28083 103d9282a946
permissions -rw-r--r--
adapted to class instantiation compliance
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     1
(*  Title:      HOLCF/Tools/pcpodef_package.ML
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     3
    Author:     Brian Huffman
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     4
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     5
Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     6
typedef.
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     7
*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     8
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
     9
signature PCPODEF_PACKAGE =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    10
sig
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    11
  val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * string
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    12
    * (string * string) option -> theory -> Proof.state
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    13
  val pcpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    14
    * (string * string) option -> theory -> Proof.state
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    15
  val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * string
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    16
    * (string * string) option -> theory -> Proof.state
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    17
  val cpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    18
    * (string * string) option -> theory -> Proof.state
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    19
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    20
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    21
structure PcpodefPackage: PCPODEF_PACKAGE =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    22
struct
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    23
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    24
(** theory context references **)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    25
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    26
val typedef_po = thm "typedef_po";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    27
val typedef_cpo = thm "typedef_cpo";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    28
val typedef_pcpo = thm "typedef_pcpo";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    29
val typedef_lub = thm "typedef_lub";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    30
val typedef_thelub = thm "typedef_thelub";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    31
val typedef_compact = thm "typedef_compact";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    32
val cont_Rep = thm "typedef_cont_Rep";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    33
val cont_Abs = thm "typedef_cont_Abs";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    34
val Rep_strict = thm "typedef_Rep_strict";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    35
val Abs_strict = thm "typedef_Abs_strict";
25926
aa0eca1ccb19 pcpodef generates strict_iff lemmas
huffman
parents: 25723
diff changeset
    36
val Rep_strict_iff = thm "typedef_Rep_strict_iff";
aa0eca1ccb19 pcpodef generates strict_iff lemmas
huffman
parents: 25723
diff changeset
    37
val Abs_strict_iff = thm "typedef_Abs_strict_iff";
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    38
val Rep_defined = thm "typedef_Rep_defined";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    39
val Abs_defined = thm "typedef_Abs_defined";
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    40
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    41
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    42
(** type definitions **)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    43
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    44
(* prepare_cpodef *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    45
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    46
fun err_in_cpodef msg name =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    47
  cat_error msg ("The error(s) above occurred in cpodef " ^ quote name);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    48
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    49
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    50
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    51
fun adm_const T = Const ("Adm.adm", (T --> HOLogic.boolT) --> HOLogic.boolT);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    52
fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    53
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    54
fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    55
  let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    56
    val ctxt = ProofContext.init thy;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    57
    val full = Sign.full_name thy;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    58
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    59
    (*rhs*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    60
    val full_name = full name;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    61
    val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    62
    val setT = Term.fastype_of set;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    63
    val rhs_tfrees = term_tfrees set;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    64
    val oldT = HOLogic.dest_setT setT handle TYPE _ =>
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24867
diff changeset
    65
      error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    66
    fun mk_nonempty A =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    67
      HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    68
    fun mk_admissible A =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    69
      mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
25723
80c06e4d4db6 move bottom-related stuff back into Pcpo.thy
huffman
parents: 25701
diff changeset
    70
    fun mk_UU_mem A = HOLogic.mk_mem (Const ("Pcpo.UU", oldT), A);
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    71
    val goal = if pcpo
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    72
      then HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_UU_mem set, mk_admissible set))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    73
      else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    74
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    75
    (*lhs*)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    76
    val defS = Sign.defaultS thy;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    77
    val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    78
    val lhs_sorts = map snd lhs_tfrees;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    79
    val tname = Syntax.type_name t mx;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    80
    val full_tname = full tname;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    81
    val newT = Type (full_tname, map TFree lhs_tfrees);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    82
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    83
    val (Rep_name, Abs_name) = the_default ("Rep_" ^ name, "Abs_" ^ name) opt_morphs;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    84
    val RepC = Const (full Rep_name, newT --> oldT);
23284
07ae93e58fea use new-style class for sq_ord; rename op << to sq_le
huffman
parents: 23152
diff changeset
    85
    fun lessC T = Const (@{const_name Porder.sq_le}, T --> T --> HOLogic.boolT);
28073
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
    86
    val less_def = Logic.mk_equals (lessC newT,
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
    87
      Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
    88
28073
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
    89
    fun make_po tac thy1 =
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
    90
      let
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
    91
        val ((_, {type_definition, set_def, ...}), thy2) = thy1
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
    92
          |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac;
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
    93
        val lthy3 = thy2
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
    94
          |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort "Porder.po"});
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
    95
        val less_def' = Syntax.check_term lthy3 less_def;
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
    96
        val ((_, (_, less_definition')), lthy4) = lthy3
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
    97
          |> Specification.definition (NONE, (("less_" ^ name ^ "_def", []), less_def'));
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
    98
        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
    99
        val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
   100
        val thy5 = lthy4
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
   101
          |> Class.prove_instantiation_instance
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
   102
              (K (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1))
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
   103
          |> LocalTheory.exit
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
   104
          |> ProofContext.theory_of;
5e9f00f4f209 adapted to class instantiation compliance
haftmann
parents: 27691
diff changeset
   105
      in ((type_definition, less_definition, set_def), thy5) end;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   106
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   107
    fun make_cpo admissible (type_def, less_def, set_def) theory =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   108
      let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   109
        val admissible' = fold_rule (the_list set_def) admissible;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   110
        val cpo_thms = [type_def, less_def, admissible'];
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   111
      in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   112
        theory
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   113
        |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.cpo"])
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   114
          (Tactic.rtac (typedef_cpo OF cpo_thms) 1)
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24509
diff changeset
   115
        |> Sign.add_path name
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   116
        |> PureThy.add_thms
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   117
            ([(("adm_" ^ name, admissible'), []),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   118
              (("cont_" ^ Rep_name, cont_Rep OF cpo_thms), []),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   119
              (("cont_" ^ Abs_name, cont_Abs OF cpo_thms), []),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   120
              (("lub_"     ^ name, typedef_lub     OF cpo_thms), []),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   121
              (("thelub_"  ^ name, typedef_thelub  OF cpo_thms), []),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   122
              (("compact_" ^ name, typedef_compact OF cpo_thms), [])])
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   123
        |> snd
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24509
diff changeset
   124
        |> Sign.parent_path
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   125
      end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   126
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   127
    fun make_pcpo UUmem (type_def, less_def, set_def) theory =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   128
      let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   129
        val UUmem' = fold_rule (the_list set_def) UUmem;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   130
        val pcpo_thms = [type_def, less_def, UUmem'];
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   131
      in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   132
        theory
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   133
        |> AxClass.prove_arity (full_tname, lhs_sorts, ["Pcpo.pcpo"])
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   134
          (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1)
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24509
diff changeset
   135
        |> Sign.add_path name
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   136
        |> PureThy.add_thms
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   137
            ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   138
              ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []),
25926
aa0eca1ccb19 pcpodef generates strict_iff lemmas
huffman
parents: 25723
diff changeset
   139
              ((Rep_name ^ "_strict_iff", Rep_strict_iff OF pcpo_thms), []),
aa0eca1ccb19 pcpodef generates strict_iff lemmas
huffman
parents: 25723
diff changeset
   140
              ((Abs_name ^ "_strict_iff", Abs_strict_iff OF pcpo_thms), []),
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   141
              ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []),
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   142
              ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), [])
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   143
              ])
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   144
        |> snd
24712
64ed05609568 proper Sign operations instead of Theory aliases;
wenzelm
parents: 24509
diff changeset
   145
        |> Sign.parent_path
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   146
      end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   147
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   148
    fun pcpodef_result UUmem_admissible theory =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   149
      let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   150
        val UUmem = UUmem_admissible RS conjunct1;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   151
        val admissible = UUmem_admissible RS conjunct2;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   152
      in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   153
        theory
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   154
        |> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   155
        |-> (fn defs => make_cpo admissible defs #> make_pcpo UUmem defs)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   156
      end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   157
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   158
    fun cpodef_result nonempty_admissible theory =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   159
      let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   160
        val nonempty = nonempty_admissible RS conjunct1;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   161
        val admissible = nonempty_admissible RS conjunct2;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   162
      in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   163
        theory
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   164
        |> make_po (Tactic.rtac nonempty 1)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   165
        |-> make_cpo admissible
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   166
      end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   167
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   168
  in (goal, if pcpo then pcpodef_result else cpodef_result) end
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   169
  handle ERROR msg => err_in_cpodef msg name;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   170
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   171
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   172
(* cpodef_proof interface *)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   173
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   174
fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   175
  let
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   176
    val (goal, pcpodef_result) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   177
      prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   178
    fun after_qed [[th]] = ProofContext.theory (pcpodef_result th);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   179
  in Proof.theorem_i NONE after_qed [[(goal, [])]] (ProofContext.init thy) end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   180
24509
23ee6b7788c2 replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents: 24218
diff changeset
   181
fun pcpodef_proof x = gen_pcpodef_proof Syntax.read_term true x;
23ee6b7788c2 replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents: 24218
diff changeset
   182
fun pcpodef_proof_i x = gen_pcpodef_proof Syntax.check_term true x;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   183
24509
23ee6b7788c2 replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents: 24218
diff changeset
   184
fun cpodef_proof x = gen_pcpodef_proof Syntax.read_term false x;
23ee6b7788c2 replaced ProofContext.read_term/prop by general Syntax.read_term/prop;
wenzelm
parents: 24218
diff changeset
   185
fun cpodef_proof_i x = gen_pcpodef_proof Syntax.check_term false x;
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   186
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   187
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   188
(** outer syntax **)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   189
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   190
local structure P = OuterParse and K = OuterKeyword in
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   191
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24712
diff changeset
   192
(* cf. HOL/Tools/typedef_package.ML *)
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   193
val typedef_proof_decl =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   194
  Scan.optional (P.$$$ "(" |--
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   195
      ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   196
        --| P.$$$ ")") (true, NONE) --
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   197
    (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   198
    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   199
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   200
fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   201
  (if pcpo then pcpodef_proof else cpodef_proof)
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   202
    ((def, the_default (Syntax.type_name t mx) opt_name), (t, vs, mx), A, morphs);
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   203
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24712
diff changeset
   204
val _ =
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   205
  OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   206
    (typedef_proof_decl >>
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   207
      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   208
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24712
diff changeset
   209
val _ =
23152
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   210
  OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   211
    (typedef_proof_decl >>
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   212
      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   213
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   214
end;
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   215
9497234a2743 moved HOLCF tools to canonical place;
wenzelm
parents:
diff changeset
   216
end;