src/HOLCF/pcpodef_package.ML
author wenzelm
Sat Jan 21 23:02:14 2006 +0100 (2006-01-21)
changeset 18728 6790126ab5f6
parent 18678 dd0c569fa43d
child 18799 f137c5e971f5
permissions -rw-r--r--
simplified type attribute;
huffman@16696
     1
(*  Title:      HOLCF/pcpodef_package.ML
huffman@16696
     2
    ID:         $Id$
huffman@16696
     3
    Author:     Brian Huffman
huffman@16696
     4
huffman@16696
     5
Gordon/HOL-style type definitions for HOLCF.
huffman@16696
     6
*)
huffman@16696
     7
huffman@16696
     8
signature PCPODEF_PACKAGE =
huffman@16696
     9
sig
huffman@16696
    10
  val quiet_mode: bool ref
huffman@16696
    11
  val pcpodef_proof: (bool * string) * (bstring * string list * mixfix) * string
wenzelm@17336
    12
    * (string * string) option -> theory -> Proof.state
huffman@16696
    13
  val pcpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
wenzelm@17336
    14
    * (string * string) option -> theory -> Proof.state
huffman@16696
    15
  val cpodef_proof: (bool * string) * (bstring * string list * mixfix) * string
wenzelm@17336
    16
    * (string * string) option -> theory -> Proof.state
huffman@16696
    17
  val cpodef_proof_i: (bool * string) * (bstring * string list * mixfix) * term
wenzelm@17336
    18
    * (string * string) option -> theory -> Proof.state
huffman@16696
    19
end;
huffman@16696
    20
huffman@16696
    21
structure PcpodefPackage: PCPODEF_PACKAGE =
huffman@16696
    22
struct
huffman@16696
    23
huffman@16696
    24
huffman@16696
    25
(** theory context references **)
huffman@16696
    26
huffman@16696
    27
val typedef_po = thm "typedef_po";
huffman@16696
    28
val typedef_cpo = thm "typedef_cpo";
huffman@16919
    29
val typedef_pcpo = thm "typedef_pcpo";
huffman@16919
    30
val typedef_lub = thm "typedef_lub";
huffman@16919
    31
val typedef_thelub = thm "typedef_thelub";
huffman@17833
    32
val typedef_compact = thm "typedef_compact";
huffman@16696
    33
val cont_Rep = thm "typedef_cont_Rep";
huffman@16696
    34
val cont_Abs = thm "typedef_cont_Abs";
huffman@16696
    35
val Rep_strict = thm "typedef_Rep_strict";
huffman@16696
    36
val Abs_strict = thm "typedef_Abs_strict";
huffman@16696
    37
val Rep_defined = thm "typedef_Rep_defined";
huffman@16696
    38
val Abs_defined = thm "typedef_Abs_defined";
huffman@16696
    39
huffman@16696
    40
huffman@16696
    41
(** type definitions **)
huffman@16696
    42
huffman@16696
    43
(* messages *)
huffman@16696
    44
huffman@16696
    45
val quiet_mode = ref false;
huffman@16696
    46
fun message s = if ! quiet_mode then () else writeln s;
huffman@16696
    47
huffman@16696
    48
huffman@16696
    49
(* prepare_cpodef *)
huffman@16696
    50
huffman@16696
    51
fun read_term thy used s =
huffman@16696
    52
  #1 (Thm.read_def_cterm (thy, K NONE, K NONE) used true (s, HOLogic.typeT));
huffman@16696
    53
huffman@16696
    54
fun cert_term thy _ t = Thm.cterm_of thy t handle TERM (msg, _) => error msg;
huffman@16696
    55
wenzelm@18678
    56
fun err_in_cpodef msg name =
wenzelm@18678
    57
  cat_error msg ("The error(s) above occurred in cpodef " ^ quote name);
huffman@16696
    58
huffman@16696
    59
fun adm_const T = Const ("Adm.adm", (T --> HOLogic.boolT) --> HOLogic.boolT);
huffman@16696
    60
fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
huffman@16696
    61
huffman@16696
    62
fun gen_prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
huffman@16696
    63
  let
huffman@16696
    64
    val full = Sign.full_name thy;
huffman@16696
    65
huffman@16696
    66
    (*rhs*)
huffman@16696
    67
    val full_name = full name;
huffman@16696
    68
    val cset = prep_term thy vs raw_set;
huffman@16696
    69
    val {T = setT, t = set, ...} = Thm.rep_cterm cset;
huffman@16696
    70
    val rhs_tfrees = term_tfrees set;
huffman@16696
    71
    val oldT = HOLogic.dest_setT setT handle TYPE _ =>
huffman@16696
    72
      error ("Not a set type: " ^ quote (Sign.string_of_typ thy setT));
huffman@16696
    73
    fun mk_nonempty A =
huffman@16696
    74
      HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
huffman@16696
    75
    fun mk_admissible A =
huffman@16696
    76
      mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
huffman@16696
    77
    fun mk_UU_mem A = HOLogic.mk_mem (Const ("Pcpo.UU", oldT), A);
huffman@16696
    78
    val goal = if pcpo
huffman@16696
    79
      then HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_UU_mem set, mk_admissible set))
huffman@16696
    80
      else HOLogic.mk_Trueprop (HOLogic.mk_conj (mk_nonempty set, mk_admissible set));
huffman@16696
    81
  
huffman@16696
    82
    (*lhs*)
haftmann@17325
    83
    val lhs_tfrees = map (fn v => (v, AList.lookup (op =) rhs_tfrees v |> the_default HOLogic.typeS)) vs;
huffman@16696
    84
    val lhs_sorts = map snd lhs_tfrees;
huffman@16696
    85
    val tname = Syntax.type_name t mx;
huffman@16696
    86
    val full_tname = full tname;
huffman@16696
    87
    val newT = Type (full_tname, map TFree lhs_tfrees);
huffman@16696
    88
huffman@16696
    89
    val (Rep_name, Abs_name) = getOpt (opt_morphs, ("Rep_" ^ name, "Abs_" ^ name));
huffman@16696
    90
    val RepC = Const (full Rep_name, newT --> oldT);
huffman@17810
    91
    fun lessC T = Const ("Porder.<<", T --> T --> HOLogic.boolT);
huffman@16696
    92
    val less_def = ("less_" ^ name ^ "_def", Logic.mk_equals (lessC newT,
huffman@16696
    93
      Abs ("x", newT, Abs ("y", newT, lessC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0)))));
huffman@16696
    94
huffman@16696
    95
    fun option_fold_rule NONE = I
huffman@16696
    96
      | option_fold_rule (SOME def) = fold_rule [def];
huffman@16696
    97
    
haftmann@18358
    98
    fun make_po tac thy =
haftmann@18358
    99
      thy
huffman@16696
   100
      |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac
huffman@16696
   101
      |>> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Porder.sq_ord"])
haftmann@18358
   102
           (AxClass.intro_classes_tac [])
haftmann@18358
   103
      |>>> (PureThy.add_defs_i true [Thm.no_attributes less_def] #> Library.swap)
haftmann@18358
   104
      |> (fn (thy', ({type_definition, set_def, ...}, [less_definition])) =>
haftmann@18358
   105
           thy'
haftmann@18358
   106
           |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Porder.po"])
haftmann@18358
   107
             (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1)
haftmann@18358
   108
           |> rpair (type_definition, less_definition, set_def));
huffman@16696
   109
    
huffman@16919
   110
    fun make_cpo admissible (theory, defs as (type_def, less_def, set_def)) =
huffman@16919
   111
      let
huffman@16919
   112
        val admissible' = option_fold_rule set_def admissible;
huffman@16919
   113
        val cpo_thms = [type_def, less_def, admissible'];
haftmann@18377
   114
        val (_, theory') =
huffman@16919
   115
          theory
huffman@16919
   116
          |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.cpo"])
huffman@16919
   117
            (Tactic.rtac (typedef_cpo OF cpo_thms) 1)
huffman@16919
   118
          |> Theory.add_path name
huffman@16919
   119
          |> PureThy.add_thms
huffman@16919
   120
            ([(("adm_" ^ name, admissible'), []),
huffman@16919
   121
              (("cont_" ^ Rep_name, cont_Rep OF cpo_thms), []),
huffman@16919
   122
              (("cont_" ^ Abs_name, cont_Abs OF cpo_thms), []),
huffman@17833
   123
              (("lub_"     ^ name, typedef_lub     OF cpo_thms), []),
huffman@17833
   124
              (("thelub_"  ^ name, typedef_thelub  OF cpo_thms), []),
huffman@17833
   125
              (("compact_" ^ name, typedef_compact OF cpo_thms), [])])
haftmann@18377
   126
          ||> Theory.parent_path;
huffman@16919
   127
      in (theory', defs) end;
huffman@16919
   128
huffman@16919
   129
    fun make_pcpo UUmem (theory, defs as (type_def, less_def, set_def)) =
huffman@16919
   130
      let
huffman@16919
   131
        val UUmem' = option_fold_rule set_def UUmem;
huffman@16919
   132
        val pcpo_thms = [type_def, less_def, UUmem'];
haftmann@18377
   133
        val (_, theory') =
huffman@16919
   134
          theory
huffman@16919
   135
          |> AxClass.add_inst_arity_i (full_tname, lhs_sorts, ["Pcpo.pcpo"])
huffman@16919
   136
            (Tactic.rtac (typedef_pcpo OF pcpo_thms) 1)
huffman@16919
   137
          |> Theory.add_path name
huffman@16919
   138
          |> PureThy.add_thms
huffman@16919
   139
            ([((Rep_name ^ "_strict", Rep_strict OF pcpo_thms), []),
huffman@16919
   140
              ((Abs_name ^ "_strict", Abs_strict OF pcpo_thms), []),
huffman@16919
   141
              ((Rep_name ^ "_defined", Rep_defined OF pcpo_thms), []),
huffman@16919
   142
              ((Abs_name ^ "_defined", Abs_defined OF pcpo_thms), [])
huffman@16919
   143
              ])
haftmann@18377
   144
          ||> Theory.parent_path;
huffman@16919
   145
      in (theory', defs) end;
huffman@16919
   146
    
wenzelm@18728
   147
    fun pcpodef_result (context, UUmem_admissible) =
huffman@16696
   148
      let
wenzelm@18728
   149
        val theory = Context.the_theory context;
huffman@16696
   150
        val UUmem = UUmem_admissible RS conjunct1;
huffman@16696
   151
        val admissible = UUmem_admissible RS conjunct2;
huffman@16696
   152
      in
huffman@16696
   153
        theory
huffman@16696
   154
        |> make_po (Tactic.rtac exI 1 THEN Tactic.rtac UUmem 1)
huffman@16919
   155
        |> make_cpo admissible
huffman@16919
   156
        |> make_pcpo UUmem
wenzelm@18728
   157
        |> (fn (theory', (type_def, _, _)) => (Context.Theory theory', type_def))
huffman@16696
   158
      end;
huffman@16696
   159
  
wenzelm@18728
   160
    fun cpodef_result (context, nonempty_admissible) =
huffman@16696
   161
      let
wenzelm@18728
   162
        val theory = Context.the_theory context;
huffman@16696
   163
        val nonempty = nonempty_admissible RS conjunct1;
huffman@16696
   164
        val admissible = nonempty_admissible RS conjunct2;
huffman@16696
   165
      in
huffman@16696
   166
        theory
huffman@16696
   167
        |> make_po (Tactic.rtac nonempty 1)
huffman@16919
   168
        |> make_cpo admissible
wenzelm@18728
   169
        |> (fn (theory', (type_def, _, _)) => (Context.Theory theory', type_def))
huffman@16696
   170
      end;
huffman@16696
   171
  
huffman@16696
   172
  in (goal, if pcpo then pcpodef_result else cpodef_result) end
wenzelm@18678
   173
  handle ERROR msg => err_in_cpodef msg name;
huffman@16696
   174
huffman@16696
   175
(* cpodef_proof interface *)
huffman@16696
   176
wenzelm@17336
   177
fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
huffman@16696
   178
  let
huffman@16696
   179
    val (goal, att) =
huffman@16696
   180
      gen_prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
wenzelm@17336
   181
  in IsarThy.theorem_i Drule.internalK ("", [att]) (goal, ([], [])) thy end;
huffman@16696
   182
haftmann@18358
   183
fun pcpodef_proof x = gen_pcpodef_proof read_term true x;
haftmann@18358
   184
fun pcpodef_proof_i x = gen_pcpodef_proof cert_term true x;
huffman@16696
   185
haftmann@18358
   186
fun cpodef_proof x = gen_pcpodef_proof read_term false x;
haftmann@18358
   187
fun cpodef_proof_i x = gen_pcpodef_proof cert_term false x;
huffman@16696
   188
huffman@16696
   189
huffman@16696
   190
(** outer syntax **)
huffman@16696
   191
wenzelm@17057
   192
local structure P = OuterParse and K = OuterKeyword in
huffman@16696
   193
huffman@16696
   194
(* copied from HOL/Tools/typedef_package.ML *)
huffman@16696
   195
val typedef_proof_decl =
huffman@16696
   196
  Scan.optional (P.$$$ "(" |--
huffman@16696
   197
      ((P.$$$ "open" >> K false) -- Scan.option P.name || P.name >> (fn s => (true, SOME s)))
huffman@16696
   198
        --| P.$$$ ")") (true, NONE) --
huffman@16696
   199
    (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
huffman@16696
   200
    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.name -- P.name));
huffman@16696
   201
huffman@16696
   202
fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
huffman@16696
   203
  (if pcpo then pcpodef_proof else cpodef_proof)
huffman@16696
   204
    ((def, getOpt (opt_name, Syntax.type_name t mx)), (t, vs, mx), A, morphs);
huffman@16696
   205
huffman@16696
   206
val pcpodefP =
huffman@16696
   207
  OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
huffman@16696
   208
    (typedef_proof_decl >>
huffman@16696
   209
      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
huffman@16696
   210
huffman@16696
   211
val cpodefP =
huffman@16696
   212
  OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
huffman@16696
   213
    (typedef_proof_decl >>
huffman@16696
   214
      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
huffman@16696
   215
huffman@16696
   216
val _ = OuterSyntax.add_parsers [pcpodefP, cpodefP];
huffman@16696
   217
huffman@16696
   218
end;
huffman@16696
   219
huffman@16696
   220
end;