src/HOL/Tools/Quotient/quotient_def.ML
author wenzelm
Fri, 28 Oct 2011 23:10:44 +0200
changeset 45292 90106a351a11
parent 45291 57cd50f98fdc
child 45598 87a2624f57e4
permissions -rw-r--r--
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37744
3daaf23b9ab4 tuned titles
haftmann
parents: 37592
diff changeset
     1
(*  Title:      HOL/Tools/Quotient/quotient_def.ML
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     2
    Author:     Cezary Kaliszyk and Christian Urban
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
35788
f1deaca15ca3 observe standard header format;
wenzelm
parents: 35624
diff changeset
     4
Definitions for constants on quotient types.
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     5
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     6
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     7
signature QUOTIENT_DEF =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     8
sig
43608
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
     9
  val quotient_def: (binding * typ option * mixfix) option * (Attrib.binding * (term * term)) ->
45279
89a17197cb98 simplified/standardized signatures;
wenzelm
parents: 43663
diff changeset
    10
    local_theory -> Quotient_Info.quotconsts * local_theory
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    11
43608
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
    12
  val quotdef_cmd: (binding * string option * mixfix) option * (Attrib.binding * (string * string)) ->
45279
89a17197cb98 simplified/standardized signatures;
wenzelm
parents: 43663
diff changeset
    13
    local_theory -> Quotient_Info.quotconsts * local_theory
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    14
37561
19fca77829ea mixfix can be given for automatically lifted constants
Christian Urban <urbanc@in.tum.de>
parents: 37532
diff changeset
    15
  val lift_raw_const: typ list -> (string * term * mixfix) -> local_theory ->
45279
89a17197cb98 simplified/standardized signatures;
wenzelm
parents: 43663
diff changeset
    16
    Quotient_Info.quotconsts * local_theory
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    17
end;
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    18
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    19
structure Quotient_Def: QUOTIENT_DEF =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    20
struct
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    21
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    22
(** Interface and Syntax Setup **)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    23
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    24
(* The ML-interface for a quotient definition takes
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    25
   as argument:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    26
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    27
    - an optional binding and mixfix annotation
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    28
    - attributes
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    29
    - the new constant as term
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    30
    - the rhs of the definition as term
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    31
45279
89a17197cb98 simplified/standardized signatures;
wenzelm
parents: 43663
diff changeset
    32
   It stores the qconst_info in the quotconsts data slot.
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    33
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    34
   Restriction: At the moment the left- and right-hand
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    35
   side of the definition must be a constant.
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    36
*)
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    37
fun error_msg bind str =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    38
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    39
    val name = Binding.name_of bind
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    40
    val pos = Position.str_of (Binding.pos_of bind)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    41
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    42
    error ("Head of quotient_definition " ^
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    43
      quote str ^ " differs from declaration " ^ name ^ pos)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    44
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    45
43608
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
    46
fun gen_quotient_def prep_vars prep_term (raw_var, (attr, (lhs_raw, rhs_raw))) lthy =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    47
  let
43608
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
    48
    val (vars, ctxt) = prep_vars (the_list raw_var) lthy
43663
e8c80bbc0c5d re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents: 43608
diff changeset
    49
    val T_opt = (case vars of [(_, SOME T, _)] => SOME T | _ => NONE)
e8c80bbc0c5d re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents: 43608
diff changeset
    50
    val lhs = prep_term T_opt ctxt lhs_raw
e8c80bbc0c5d re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents: 43608
diff changeset
    51
    val rhs = prep_term NONE ctxt rhs_raw
43608
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
    52
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    53
    val (lhs_str, lhs_ty) = dest_Free lhs handle TERM _ => error "Constant already defined."
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    54
    val _ = if null (strip_abs_vars rhs) then () else error "The definiens cannot be an abstraction"
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    55
    val _ = if is_Const rhs then () else warning "The definiens is not a constant"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    56
43608
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
    57
    val var =
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
    58
      (case vars of 
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
    59
        [] => (Binding.name lhs_str, NoSyn)
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
    60
      | [(binding, _, mx)] =>
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
    61
          if Variable.check_name binding = lhs_str then (binding, mx)
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
    62
          else error_msg binding lhs_str
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
    63
      | _ => raise Match)
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    64
41451
892e67be8304 do not open ML structures;
wenzelm
parents: 41444
diff changeset
    65
    val absrep_trm = Quotient_Term.absrep_fun Quotient_Term.AbsF lthy (fastype_of rhs, lhs_ty) $ rhs
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    66
    val prop = Logic.mk_equals (lhs, Syntax.check_term lthy absrep_trm)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    67
    val (_, prop') = Local_Defs.cert_def lthy prop
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    68
    val (_, newrhs) = Local_Defs.abs_def prop'
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    69
43608
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
    70
    val ((trm, (_ , thm)), lthy') = Local_Theory.define (var, (attr, newrhs)) lthy
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    71
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    72
    (* data storage *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    73
    val qconst_data = {qconst = trm, rconst = rhs, def = thm}
37530
70d03844b2f9 export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 36960
diff changeset
    74
45292
90106a351a11 more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents: 45291
diff changeset
    75
    val lthy'' = lthy'
90106a351a11 more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents: 45291
diff changeset
    76
      |> Local_Theory.declaration {syntax = false, pervasive = true}
90106a351a11 more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents: 45291
diff changeset
    77
        (fn phi =>
90106a351a11 more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents: 45291
diff changeset
    78
          (case Quotient_Info.transform_quotconsts phi qconst_data of
90106a351a11 more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents: 45291
diff changeset
    79
            qcinfo as {qconst = Const (c, _), ...} =>
90106a351a11 more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents: 45291
diff changeset
    80
              Quotient_Info.update_quotconsts c qcinfo
90106a351a11 more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
wenzelm
parents: 45291
diff changeset
    81
          | _ => I));
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    82
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    83
    (qconst_data, lthy'')
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    84
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    85
43663
e8c80bbc0c5d re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents: 43608
diff changeset
    86
fun check_term' cnstr ctxt =
e8c80bbc0c5d re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents: 43608
diff changeset
    87
  Syntax.check_term ctxt o (case cnstr of SOME T => Type.constraint T | _ => I)
e8c80bbc0c5d re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents: 43608
diff changeset
    88
fun read_term' cnstr ctxt = check_term' cnstr ctxt o tap (writeln o @{make_string}) o Syntax.parse_term ctxt
e8c80bbc0c5d re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents: 43608
diff changeset
    89
e8c80bbc0c5d re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents: 43608
diff changeset
    90
val quotient_def = gen_quotient_def Proof_Context.cert_vars check_term'
e8c80bbc0c5d re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
krauss
parents: 43608
diff changeset
    91
val quotdef_cmd = gen_quotient_def Proof_Context.read_vars read_term'
43608
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
    92
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    93
37532
8a9a34be09e0 slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents: 37530
diff changeset
    94
(* a wrapper for automatically lifting a raw constant *)
37561
19fca77829ea mixfix can be given for automatically lifted constants
Christian Urban <urbanc@in.tum.de>
parents: 37532
diff changeset
    95
fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    96
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    97
    val rty = fastype_of rconst
41451
892e67be8304 do not open ML structures;
wenzelm
parents: 41444
diff changeset
    98
    val qty = Quotient_Term.derive_qtyp ctxt qtys rty
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
    99
    val lhs = Free (qconst_name, qty)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
   100
  in
43608
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
   101
    quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 38624
diff changeset
   102
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   103
37532
8a9a34be09e0 slight cleaning and simplification of the automatic wrapper for quotient definitions
Christian Urban <urbanc@in.tum.de>
parents: 37530
diff changeset
   104
(* parser and command *)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   105
val quotdef_parser =
43608
294570668f25 parse term in auxiliary context augmented with variable;
krauss
parents: 42494
diff changeset
   106
  Scan.option Parse_Spec.constdecl --
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36954
diff changeset
   107
    Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| Parse.$$$ "is" -- Parse.term))
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   108
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   109
val _ =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36954
diff changeset
   110
  Outer_Syntax.local_theory "quotient_definition"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   111
    "definition for constants over the quotient type"
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36954
diff changeset
   112
      Keyword.thy_decl (quotdef_parser >> (snd oo quotdef_cmd))
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   113
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   114
end; (* structure *)