src/HOL/Tools/Quotient/quotient_info.ML
author wenzelm
Thu Mar 06 13:44:01 2014 +0100 (2014-03-06)
changeset 55954 a29aefc88c8d
parent 55952 2f85cc6c27d4
child 57960 ee1ba4848896
permissions -rw-r--r--
more uniform check_const/read_const;
haftmann@37744
     1
(*  Title:      HOL/Tools/Quotient/quotient_info.ML
kaliszyk@35222
     2
    Author:     Cezary Kaliszyk and Christian Urban
kaliszyk@35222
     3
wenzelm@45279
     4
Context data for the quotient package.
kaliszyk@35222
     5
*)
kaliszyk@35222
     6
kaliszyk@35222
     7
signature QUOTIENT_INFO =
kaliszyk@35222
     8
sig
kuncar@47094
     9
  type quotmaps = {relmap: string, quot_thm: thm}
wenzelm@45280
    10
  val lookup_quotmaps: Proof.context -> string -> quotmaps option
wenzelm@45340
    11
  val lookup_quotmaps_global: theory -> string -> quotmaps option
wenzelm@45279
    12
  val print_quotmaps: Proof.context -> unit
kaliszyk@35222
    13
bulwahn@45534
    14
  type abs_rep = {abs : term, rep : term}
bulwahn@45534
    15
  val transform_abs_rep: morphism -> abs_rep -> abs_rep
bulwahn@45534
    16
  val lookup_abs_rep: Proof.context -> string -> abs_rep option
bulwahn@45534
    17
  val lookup_abs_rep_global: theory -> string -> abs_rep option
bulwahn@45534
    18
  val update_abs_rep: string -> abs_rep -> Context.generic -> Context.generic
bulwahn@45534
    19
  val print_abs_rep: Proof.context -> unit
bulwahn@45534
    20
  
kuncar@47093
    21
  type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
wenzelm@45279
    22
  val transform_quotients: morphism -> quotients -> quotients
wenzelm@45280
    23
  val lookup_quotients: Proof.context -> string -> quotients option
wenzelm@45340
    24
  val lookup_quotients_global: theory -> string -> quotients option
wenzelm@45279
    25
  val update_quotients: string -> quotients -> Context.generic -> Context.generic
wenzelm@45279
    26
  val dest_quotients: Proof.context -> quotients list
wenzelm@45279
    27
  val print_quotients: Proof.context -> unit
kaliszyk@35222
    28
wenzelm@45279
    29
  type quotconsts = {qconst: term, rconst: term, def: thm}
wenzelm@45279
    30
  val transform_quotconsts: morphism -> quotconsts -> quotconsts
wenzelm@45340
    31
  val lookup_quotconsts_global: theory -> term -> quotconsts option
wenzelm@45279
    32
  val update_quotconsts: string -> quotconsts -> Context.generic -> Context.generic
urbanc@45350
    33
  val dest_quotconsts_global: theory -> quotconsts list
wenzelm@45279
    34
  val dest_quotconsts: Proof.context -> quotconsts list
wenzelm@45279
    35
  val print_quotconsts: Proof.context -> unit
kaliszyk@35222
    36
wenzelm@45279
    37
  val equiv_rules: Proof.context -> thm list
kaliszyk@35222
    38
  val equiv_rules_add: attribute
wenzelm@45279
    39
  val rsp_rules: Proof.context -> thm list
kaliszyk@35314
    40
  val rsp_rules_add: attribute
wenzelm@45279
    41
  val prs_rules: Proof.context -> thm list
kaliszyk@35314
    42
  val prs_rules_add: attribute
wenzelm@45279
    43
  val id_simps: Proof.context -> thm list
wenzelm@45279
    44
  val quotient_rules: Proof.context -> thm list
kaliszyk@35222
    45
  val quotient_rules_add: attribute
wenzelm@41452
    46
  val setup: theory -> theory
kaliszyk@35222
    47
end;
kaliszyk@35222
    48
kaliszyk@35222
    49
structure Quotient_Info: QUOTIENT_INFO =
kaliszyk@35222
    50
struct
kaliszyk@35222
    51
kaliszyk@35222
    52
(** data containers **)
kaliszyk@35222
    53
wenzelm@41472
    54
(* FIXME just one data slot (record) per program unit *)
wenzelm@41472
    55
kaliszyk@35222
    56
(* info about map- and rel-functions for a type *)
kuncar@47094
    57
type quotmaps = {relmap: string, quot_thm: thm}
kaliszyk@35222
    58
wenzelm@45280
    59
structure Quotmaps = Generic_Data
wenzelm@38759
    60
(
wenzelm@45279
    61
  type T = quotmaps Symtab.table
wenzelm@38759
    62
  val empty = Symtab.empty
wenzelm@38759
    63
  val extend = I
wenzelm@38759
    64
  fun merge data = Symtab.merge (K true) data
wenzelm@38759
    65
)
kaliszyk@35222
    66
wenzelm@45280
    67
val lookup_quotmaps = Symtab.lookup o Quotmaps.get o Context.Proof
wenzelm@45340
    68
val lookup_quotmaps_global = Symtab.lookup o Quotmaps.get o Context.Theory
kaliszyk@35222
    69
wenzelm@45281
    70
(* FIXME export proper internal update operation!? *)
kaliszyk@35222
    71
wenzelm@45281
    72
val quotmaps_attribute_setup =
kuncar@47308
    73
  Attrib.setup @{binding mapQ3}
wenzelm@55952
    74
    ((Args.type_name {proper = true, strict = true} --| Scan.lift @{keyword "="}) --
wenzelm@55954
    75
      (Scan.lift @{keyword "("} |--
wenzelm@55954
    76
        Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
wenzelm@47110
    77
        Attrib.thm --| Scan.lift @{keyword ")"}) >>
kuncar@47094
    78
      (fn (tyname, (relname, qthm)) =>
kuncar@47094
    79
        let val minfo = {relmap = relname, quot_thm = qthm}
wenzelm@45281
    80
        in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
wenzelm@45281
    81
    "declaration of map information"
kaliszyk@35222
    82
wenzelm@45279
    83
fun print_quotmaps ctxt =
wenzelm@41444
    84
  let
kuncar@47094
    85
    fun prt_map (ty_name, {relmap, quot_thm}) =
wenzelm@41445
    86
      Pretty.block (separate (Pretty.brk 2)
kuncar@47094
    87
         [Pretty.str "type:", 
kuncar@47094
    88
          Pretty.str ty_name,
kuncar@47094
    89
          Pretty.str "relation map:", 
kuncar@47094
    90
          Pretty.str relmap,
kuncar@47094
    91
          Pretty.str "quot. theorem:", 
kuncar@47094
    92
          Syntax.pretty_term ctxt (prop_of quot_thm)])
wenzelm@41444
    93
  in
wenzelm@45280
    94
    map prt_map (Symtab.dest (Quotmaps.get (Context.Proof ctxt)))
wenzelm@41444
    95
    |> Pretty.big_list "maps for type constructors:"
wenzelm@41444
    96
    |> Pretty.writeln
wenzelm@41444
    97
  end
kaliszyk@35222
    98
bulwahn@45534
    99
(* info about abs/rep terms *)
bulwahn@45534
   100
type abs_rep = {abs : term, rep : term}
bulwahn@45534
   101
bulwahn@45534
   102
structure Abs_Rep = Generic_Data
bulwahn@45534
   103
(
bulwahn@45534
   104
  type T = abs_rep Symtab.table
bulwahn@45534
   105
  val empty = Symtab.empty
bulwahn@45534
   106
  val extend = I
bulwahn@45534
   107
  fun merge data = Symtab.merge (K true) data
bulwahn@45534
   108
)
bulwahn@45534
   109
bulwahn@45534
   110
fun transform_abs_rep phi {abs, rep} = {abs = Morphism.term phi abs, rep = Morphism.term phi rep}
bulwahn@45534
   111
bulwahn@45534
   112
val lookup_abs_rep = Symtab.lookup o Abs_Rep.get o Context.Proof
bulwahn@45534
   113
val lookup_abs_rep_global = Symtab.lookup o Abs_Rep.get o Context.Theory
bulwahn@45534
   114
bulwahn@45534
   115
fun update_abs_rep str data = Abs_Rep.map (Symtab.update (str, data))
bulwahn@45534
   116
bulwahn@45534
   117
fun print_abs_rep ctxt =
bulwahn@45534
   118
  let
bulwahn@45534
   119
    fun prt_abs_rep (s, {abs, rep}) =
bulwahn@45534
   120
      Pretty.block (separate (Pretty.brk 2)
bulwahn@45534
   121
       [Pretty.str "type constructor:",
bulwahn@45534
   122
        Pretty.str s,
bulwahn@45534
   123
        Pretty.str "abs term:",
bulwahn@45534
   124
        Syntax.pretty_term ctxt abs,
bulwahn@45534
   125
        Pretty.str "rep term:",
bulwahn@45534
   126
        Syntax.pretty_term ctxt rep])
bulwahn@45534
   127
  in
bulwahn@45534
   128
    map prt_abs_rep (Symtab.dest (Abs_Rep.get (Context.Proof ctxt)))
bulwahn@45534
   129
    |> Pretty.big_list "abs/rep terms:"
bulwahn@45534
   130
    |> Pretty.writeln
bulwahn@45534
   131
  end
kaliszyk@35222
   132
kaliszyk@35222
   133
(* info about quotient types *)
kuncar@47093
   134
type quotients = {qtyp: typ, rtyp: typ, equiv_rel: term, equiv_thm: thm, quot_thm: thm}
kaliszyk@35222
   135
wenzelm@45280
   136
structure Quotients = Generic_Data
wenzelm@38759
   137
(
wenzelm@45279
   138
  type T = quotients Symtab.table
wenzelm@38759
   139
  val empty = Symtab.empty
wenzelm@38759
   140
  val extend = I
wenzelm@38759
   141
  fun merge data = Symtab.merge (K true) data
wenzelm@38759
   142
)
kaliszyk@35222
   143
kuncar@47093
   144
fun transform_quotients phi {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
kaliszyk@35222
   145
  {qtyp = Morphism.typ phi qtyp,
kaliszyk@35222
   146
   rtyp = Morphism.typ phi rtyp,
kaliszyk@35222
   147
   equiv_rel = Morphism.term phi equiv_rel,
kuncar@47093
   148
   equiv_thm = Morphism.thm phi equiv_thm,
kuncar@47093
   149
   quot_thm = Morphism.thm phi quot_thm}
kaliszyk@35222
   150
wenzelm@45280
   151
val lookup_quotients = Symtab.lookup o Quotients.get o Context.Proof
wenzelm@45340
   152
val lookup_quotients_global = Symtab.lookup o Quotients.get o Context.Theory
kaliszyk@35222
   153
wenzelm@45280
   154
fun update_quotients str qinfo = Quotients.map (Symtab.update (str, qinfo))
kaliszyk@35222
   155
wenzelm@45280
   156
fun dest_quotients ctxt =  (* FIXME slightly expensive way to retrieve data *)
wenzelm@45280
   157
  map snd (Symtab.dest (Quotients.get (Context.Proof ctxt)))
kaliszyk@35222
   158
wenzelm@45279
   159
fun print_quotients ctxt =
wenzelm@41444
   160
  let
kuncar@47093
   161
    fun prt_quot {qtyp, rtyp, equiv_rel, equiv_thm, quot_thm} =
wenzelm@41445
   162
      Pretty.block (separate (Pretty.brk 2)
wenzelm@41444
   163
       [Pretty.str "quotient type:",
wenzelm@41444
   164
        Syntax.pretty_typ ctxt qtyp,
wenzelm@41444
   165
        Pretty.str "raw type:",
wenzelm@41444
   166
        Syntax.pretty_typ ctxt rtyp,
wenzelm@41444
   167
        Pretty.str "relation:",
wenzelm@41444
   168
        Syntax.pretty_term ctxt equiv_rel,
wenzelm@41444
   169
        Pretty.str "equiv. thm:",
kuncar@47093
   170
        Syntax.pretty_term ctxt (prop_of equiv_thm),
kuncar@47093
   171
        Pretty.str "quot. thm:",
kuncar@47093
   172
        Syntax.pretty_term ctxt (prop_of quot_thm)])
wenzelm@41444
   173
  in
wenzelm@45280
   174
    map (prt_quot o snd) (Symtab.dest (Quotients.get (Context.Proof ctxt)))
wenzelm@41444
   175
    |> Pretty.big_list "quotients:"
wenzelm@41444
   176
    |> Pretty.writeln
wenzelm@41444
   177
  end
kaliszyk@35222
   178
kaliszyk@35222
   179
kaliszyk@35222
   180
(* info about quotient constants *)
wenzelm@45279
   181
type quotconsts = {qconst: term, rconst: term, def: thm}
kaliszyk@35222
   182
wenzelm@45279
   183
fun eq_quotconsts (x : quotconsts, y : quotconsts) = #qconst x = #qconst y
kaliszyk@35222
   184
kaliszyk@35222
   185
(* We need to be able to lookup instances of lifted constants,
kaliszyk@35222
   186
   for example given "nat fset" we need to find "'a fset";
kaliszyk@35222
   187
   but overloaded constants share the same name *)
wenzelm@45280
   188
structure Quotconsts = Generic_Data
wenzelm@38759
   189
(
wenzelm@45279
   190
  type T = quotconsts list Symtab.table
wenzelm@38759
   191
  val empty = Symtab.empty
wenzelm@38759
   192
  val extend = I
wenzelm@45279
   193
  val merge = Symtab.merge_list eq_quotconsts
wenzelm@38759
   194
)
kaliszyk@35222
   195
wenzelm@45279
   196
fun transform_quotconsts phi {qconst, rconst, def} =
kaliszyk@35222
   197
  {qconst = Morphism.term phi qconst,
kaliszyk@35222
   198
   rconst = Morphism.term phi rconst,
kaliszyk@35222
   199
   def = Morphism.thm phi def}
kaliszyk@35222
   200
wenzelm@45280
   201
fun update_quotconsts name qcinfo = Quotconsts.map (Symtab.cons_list (name, qcinfo))
wenzelm@45280
   202
wenzelm@45280
   203
fun dest_quotconsts ctxt =
wenzelm@45280
   204
  flat (map snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
kaliszyk@35222
   205
urbanc@45350
   206
fun dest_quotconsts_global thy =
urbanc@45350
   207
  flat (map snd (Symtab.dest (Quotconsts.get (Context.Theory thy))))
urbanc@45350
   208
urbanc@45350
   209
urbanc@45350
   210
wenzelm@45340
   211
fun lookup_quotconsts_global thy t =
wenzelm@45280
   212
  let
kaliszyk@35222
   213
    val (name, qty) = dest_Const t
wenzelm@45279
   214
    fun matches (x: quotconsts) =
wenzelm@45280
   215
      let val (name', qty') = dest_Const (#qconst x);
wenzelm@45280
   216
      in name = name' andalso Sign.typ_instance thy (qty, qty') end
kaliszyk@35222
   217
  in
wenzelm@45340
   218
    (case Symtab.lookup (Quotconsts.get (Context.Theory thy)) name of
bulwahn@45274
   219
      NONE => NONE
bulwahn@45274
   220
    | SOME l => find_first matches l)
kaliszyk@35222
   221
  end
kaliszyk@35222
   222
wenzelm@45279
   223
fun print_quotconsts ctxt =
wenzelm@41444
   224
  let
wenzelm@41444
   225
    fun prt_qconst {qconst, rconst, def} =
wenzelm@41444
   226
      Pretty.block (separate (Pretty.brk 1)
wenzelm@41444
   227
       [Syntax.pretty_term ctxt qconst,
wenzelm@41444
   228
        Pretty.str ":=",
wenzelm@41444
   229
        Syntax.pretty_term ctxt rconst,
wenzelm@41444
   230
        Pretty.str "as",
wenzelm@41444
   231
        Syntax.pretty_term ctxt (prop_of def)])
wenzelm@41444
   232
  in
wenzelm@45280
   233
    map prt_qconst (maps snd (Symtab.dest (Quotconsts.get (Context.Proof ctxt))))
wenzelm@41444
   234
    |> Pretty.big_list "quotient constants:"
wenzelm@41444
   235
    |> Pretty.writeln
wenzelm@41444
   236
  end
kaliszyk@35222
   237
kaliszyk@35222
   238
(* equivalence relation theorems *)
wenzelm@45279
   239
structure Equiv_Rules = Named_Thms
wenzelm@38764
   240
(
wenzelm@45294
   241
  val name = @{binding quot_equiv}
wenzelm@38764
   242
  val description = "equivalence relation theorems"
wenzelm@38764
   243
)
kaliszyk@35222
   244
wenzelm@45279
   245
val equiv_rules = Equiv_Rules.get
wenzelm@45279
   246
val equiv_rules_add = Equiv_Rules.add
kaliszyk@35222
   247
kaliszyk@35222
   248
(* respectfulness theorems *)
wenzelm@45279
   249
structure Rsp_Rules = Named_Thms
wenzelm@38764
   250
(
wenzelm@45294
   251
  val name = @{binding quot_respect}
wenzelm@38764
   252
  val description = "respectfulness theorems"
wenzelm@38764
   253
)
kaliszyk@35222
   254
wenzelm@45279
   255
val rsp_rules = Rsp_Rules.get
wenzelm@45279
   256
val rsp_rules_add = Rsp_Rules.add
kaliszyk@35222
   257
kaliszyk@35222
   258
(* preservation theorems *)
wenzelm@45279
   259
structure Prs_Rules = Named_Thms
wenzelm@38764
   260
(
wenzelm@45294
   261
  val name = @{binding quot_preserve}
wenzelm@38764
   262
  val description = "preservation theorems"
wenzelm@38764
   263
)
kaliszyk@35222
   264
wenzelm@45279
   265
val prs_rules = Prs_Rules.get
wenzelm@45279
   266
val prs_rules_add = Prs_Rules.add
kaliszyk@35222
   267
kaliszyk@35222
   268
(* id simplification theorems *)
wenzelm@45279
   269
structure Id_Simps = Named_Thms
wenzelm@38764
   270
(
wenzelm@45294
   271
  val name = @{binding id_simps}
wenzelm@38764
   272
  val description = "identity simp rules for maps"
wenzelm@38764
   273
)
kaliszyk@35222
   274
wenzelm@45279
   275
val id_simps = Id_Simps.get
kaliszyk@35222
   276
kaliszyk@35222
   277
(* quotient theorems *)
wenzelm@45279
   278
structure Quotient_Rules = Named_Thms
wenzelm@38764
   279
(
wenzelm@45294
   280
  val name = @{binding quot_thm}
wenzelm@38764
   281
  val description = "quotient theorems"
wenzelm@38764
   282
)
kaliszyk@35222
   283
wenzelm@45279
   284
val quotient_rules = Quotient_Rules.get
wenzelm@45279
   285
val quotient_rules_add = Quotient_Rules.add
kaliszyk@35222
   286
wenzelm@41452
   287
wenzelm@41452
   288
(* theory setup *)
kaliszyk@35222
   289
wenzelm@41452
   290
val setup =
wenzelm@45281
   291
  quotmaps_attribute_setup #>
wenzelm@45279
   292
  Equiv_Rules.setup #>
wenzelm@45279
   293
  Rsp_Rules.setup #>
wenzelm@45279
   294
  Prs_Rules.setup #>
wenzelm@45279
   295
  Id_Simps.setup #>
wenzelm@45279
   296
  Quotient_Rules.setup
wenzelm@41452
   297
kaliszyk@35222
   298
wenzelm@41452
   299
(* outer syntax commands *)
wenzelm@41452
   300
wenzelm@41452
   301
val _ =
kuncar@47308
   302
  Outer_Syntax.improper_command @{command_spec "print_quotmapsQ3"} "print quotient map functions"
wenzelm@45279
   303
    (Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
kaliszyk@35222
   304
wenzelm@41452
   305
val _ =
kuncar@47308
   306
  Outer_Syntax.improper_command @{command_spec "print_quotientsQ3"} "print quotients"
wenzelm@45279
   307
    (Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
kaliszyk@35222
   308
wenzelm@41452
   309
val _ =
wenzelm@46961
   310
  Outer_Syntax.improper_command @{command_spec "print_quotconsts"} "print quotient constants"
wenzelm@45279
   311
    (Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
kaliszyk@35222
   312
wenzelm@45279
   313
end;