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