src/HOLCF/Tools/pcpodef.ML
author wenzelm
Tue Nov 10 16:04:57 2009 +0100 (2009-11-10)
changeset 33553 35f2b30593a8
parent 33226 9a2911232c1b
child 33645 562635ab559b
permissions -rw-r--r--
modernized structure Theory_Target;
haftmann@31738
     1
(*  Title:      HOLCF/Tools/pcpodef.ML
wenzelm@23152
     2
    Author:     Brian Huffman
wenzelm@23152
     3
wenzelm@23152
     4
Primitive domain definitions for HOLCF, similar to Gordon/HOL-style
haftmann@31738
     5
typedef (see also ~~/src/HOL/Tools/typedef.ML).
wenzelm@23152
     6
*)
wenzelm@23152
     7
haftmann@31738
     8
signature PCPODEF =
wenzelm@23152
     9
sig
wenzelm@30345
    10
  val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
wenzelm@30345
    11
    * (binding * binding) option -> theory -> Proof.state
wenzelm@30345
    12
  val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
wenzelm@30345
    13
    * (binding * binding) option -> theory -> Proof.state
wenzelm@30345
    14
  val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
wenzelm@30345
    15
    * (binding * binding) option -> theory -> Proof.state
wenzelm@30345
    16
  val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
wenzelm@30345
    17
    * (binding * binding) option -> theory -> Proof.state
wenzelm@23152
    18
end;
wenzelm@23152
    19
haftmann@31738
    20
structure Pcpodef :> PCPODEF =
wenzelm@23152
    21
struct
wenzelm@23152
    22
wenzelm@23152
    23
(** type definitions **)
wenzelm@23152
    24
wenzelm@23152
    25
(* prepare_cpodef *)
wenzelm@23152
    26
wenzelm@23152
    27
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
wenzelm@23152
    28
wenzelm@29060
    29
fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
wenzelm@23152
    30
fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
wenzelm@23152
    31
wenzelm@23152
    32
fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
wenzelm@23152
    33
  let
wenzelm@29060
    34
    val _ = Theory.requires thy "Pcpodef" "pcpodefs";
wenzelm@23152
    35
    val ctxt = ProofContext.init thy;
wenzelm@30345
    36
wenzelm@30345
    37
    val full = Sign.full_name thy;
wenzelm@30345
    38
    val full_name = full name;
wenzelm@30345
    39
    val bname = Binding.name_of name;
wenzelm@23152
    40
wenzelm@23152
    41
    (*rhs*)
wenzelm@23152
    42
    val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
wenzelm@23152
    43
    val setT = Term.fastype_of set;
wenzelm@29060
    44
    val rhs_tfrees = Term.add_tfrees set [];
wenzelm@23152
    45
    val oldT = HOLogic.dest_setT setT handle TYPE _ =>
wenzelm@24920
    46
      error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
wenzelm@29060
    47
wenzelm@29060
    48
    (*goal*)
wenzelm@29063
    49
    val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
wenzelm@29063
    50
    val goal_nonempty =
wenzelm@29063
    51
      HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
wenzelm@29063
    52
    val goal_admissible =
wenzelm@29063
    53
      HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
wenzelm@23152
    54
wenzelm@23152
    55
    (*lhs*)
wenzelm@23152
    56
    val defS = Sign.defaultS thy;
wenzelm@23152
    57
    val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
wenzelm@23152
    58
    val lhs_sorts = map snd lhs_tfrees;
wenzelm@29060
    59
wenzelm@30345
    60
    val tname = Binding.map_name (Syntax.type_name mx) t;
wenzelm@23152
    61
    val full_tname = full tname;
wenzelm@23152
    62
    val newT = Type (full_tname, map TFree lhs_tfrees);
wenzelm@23152
    63
wenzelm@30345
    64
    val (Rep_name, Abs_name) =
wenzelm@30345
    65
      (case opt_morphs of
wenzelm@30345
    66
        NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
wenzelm@30345
    67
      | SOME morphs => morphs);
wenzelm@23152
    68
    val RepC = Const (full Rep_name, newT --> oldT);
huffman@31076
    69
    fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
huffman@31076
    70
    val below_def = Logic.mk_equals (belowC newT,
huffman@31076
    71
      Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
wenzelm@23152
    72
haftmann@28073
    73
    fun make_po tac thy1 =
haftmann@28073
    74
      let
haftmann@28073
    75
        val ((_, {type_definition, set_def, ...}), thy2) = thy1
haftmann@31725
    76
          |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
haftmann@28073
    77
        val lthy3 = thy2
wenzelm@33553
    78
          |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
huffman@31076
    79
        val below_def' = Syntax.check_term lthy3 below_def;
huffman@31076
    80
        val ((_, (_, below_definition')), lthy4) = lthy3
wenzelm@30345
    81
          |> Specification.definition (NONE,
huffman@31076
    82
              ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
haftmann@28073
    83
        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
huffman@31076
    84
        val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
haftmann@28073
    85
        val thy5 = lthy4
haftmann@28073
    86
          |> Class.prove_instantiation_instance
huffman@31076
    87
              (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
wenzelm@28394
    88
          |> LocalTheory.exit_global;
huffman@31076
    89
      in ((type_definition, below_definition, set_def), thy5) end;
wenzelm@23152
    90
huffman@31076
    91
    fun make_cpo admissible (type_def, below_def, set_def) theory =
wenzelm@23152
    92
      let
wenzelm@33226
    93
        (* FIXME fold_rule might fold user input inintentionally *)
wenzelm@23152
    94
        val admissible' = fold_rule (the_list set_def) admissible;
huffman@31076
    95
        val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
wenzelm@28377
    96
        val theory' = theory
wenzelm@29060
    97
          |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
wenzelm@29060
    98
            (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
wenzelm@28377
    99
        val cpo_thms' = map (Thm.transfer theory') cpo_thms;
wenzelm@23152
   100
      in
wenzelm@28377
   101
        theory'
wenzelm@30345
   102
        |> Sign.add_path (Binding.name_of name)
wenzelm@23152
   103
        |> PureThy.add_thms
wenzelm@30345
   104
          ([((Binding.prefix_name "adm_" name, admissible'), []),
wenzelm@30345
   105
            ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
wenzelm@30345
   106
            ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
wenzelm@30345
   107
            ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []),
wenzelm@30345
   108
            ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []),
wenzelm@30345
   109
            ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])])
wenzelm@23152
   110
        |> snd
wenzelm@24712
   111
        |> Sign.parent_path
wenzelm@23152
   112
      end;
wenzelm@23152
   113
huffman@31076
   114
    fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
wenzelm@23152
   115
      let
wenzelm@33226
   116
        (* FIXME fold_rule might fold user input inintentionally *)
wenzelm@29063
   117
        val UU_mem' = fold_rule (the_list set_def) UU_mem;
huffman@31076
   118
        val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
wenzelm@28377
   119
        val theory' = theory
wenzelm@29060
   120
          |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
wenzelm@29060
   121
            (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
wenzelm@28377
   122
        val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
wenzelm@23152
   123
      in
wenzelm@28377
   124
        theory'
wenzelm@30345
   125
        |> Sign.add_path (Binding.name_of name)
wenzelm@23152
   126
        |> PureThy.add_thms
wenzelm@30345
   127
          ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []),
wenzelm@30345
   128
            ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []),
wenzelm@30345
   129
            ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
wenzelm@30345
   130
            ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
wenzelm@30345
   131
            ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []),
wenzelm@30345
   132
            ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])])
wenzelm@23152
   133
        |> snd
wenzelm@24712
   134
        |> Sign.parent_path
wenzelm@23152
   135
      end;
wenzelm@23152
   136
wenzelm@29063
   137
    fun pcpodef_result UU_mem admissible =
wenzelm@29063
   138
      make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1)
wenzelm@29063
   139
      #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs);
wenzelm@23152
   140
wenzelm@29063
   141
    fun cpodef_result nonempty admissible =
wenzelm@29063
   142
      make_po (Tactic.rtac nonempty 1)
wenzelm@29063
   143
      #-> make_cpo admissible;
wenzelm@29063
   144
  in
wenzelm@29063
   145
    if pcpo
wenzelm@29063
   146
    then (goal_UU_mem, goal_admissible, pcpodef_result)
wenzelm@29063
   147
    else (goal_nonempty, goal_admissible, cpodef_result)
wenzelm@29063
   148
  end
wenzelm@30345
   149
  handle ERROR msg =>
wenzelm@30345
   150
    cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
wenzelm@23152
   151
wenzelm@23152
   152
wenzelm@29060
   153
(* proof interface *)
wenzelm@29060
   154
wenzelm@29060
   155
local
wenzelm@23152
   156
wenzelm@23152
   157
fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
wenzelm@23152
   158
  let
wenzelm@29063
   159
    val (goal1, goal2, make_result) =
wenzelm@23152
   160
      prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
wenzelm@29063
   161
    fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2);
wenzelm@29063
   162
  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
wenzelm@23152
   163
wenzelm@29060
   164
in
wenzelm@29060
   165
wenzelm@29060
   166
fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x;
wenzelm@29060
   167
fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x;
wenzelm@23152
   168
wenzelm@29060
   169
fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x;
wenzelm@29060
   170
fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x;
wenzelm@29060
   171
wenzelm@29060
   172
end;
wenzelm@29060
   173
wenzelm@23152
   174
wenzelm@23152
   175
wenzelm@23152
   176
(** outer syntax **)
wenzelm@23152
   177
wenzelm@23152
   178
local structure P = OuterParse and K = OuterKeyword in
wenzelm@23152
   179
wenzelm@23152
   180
val typedef_proof_decl =
wenzelm@23152
   181
  Scan.optional (P.$$$ "(" |--
wenzelm@30345
   182
      ((P.$$$ "open" >> K false) -- Scan.option P.binding || P.binding >> (fn s => (true, SOME s)))
wenzelm@23152
   183
        --| P.$$$ ")") (true, NONE) --
wenzelm@30345
   184
    (P.type_args -- P.binding) -- P.opt_infix -- (P.$$$ "=" |-- P.term) --
wenzelm@30345
   185
    Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding));
wenzelm@23152
   186
wenzelm@23152
   187
fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
wenzelm@29060
   188
  (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
wenzelm@30345
   189
    ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
wenzelm@23152
   190
wenzelm@24867
   191
val _ =
wenzelm@23152
   192
  OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
wenzelm@23152
   193
    (typedef_proof_decl >>
wenzelm@23152
   194
      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)));
wenzelm@23152
   195
wenzelm@24867
   196
val _ =
wenzelm@23152
   197
  OuterSyntax.command "cpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal
wenzelm@23152
   198
    (typedef_proof_decl >>
wenzelm@23152
   199
      (Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)));
wenzelm@23152
   200
wenzelm@23152
   201
end;
wenzelm@23152
   202
wenzelm@23152
   203
end;