Quot/quotient_def.ML
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 08 Jan 2010 15:02:12 +0100
changeset 829 42b90994ac77
parent 804 ba7e81531c6d
child 830 89d772dae4d4
permissions -rw-r--r--
map and rel simps for all quotients; needed when changing the relations to aggregate ones.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
277
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     2
signature QUOTIENT_DEF =
774
b4ffb8826105 moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
parents: 768
diff changeset
     3
sig 
709
596467882518 Updated comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 705
diff changeset
     4
  val quotient_def: mixfix -> Attrib.binding -> term -> term ->
775
Christian Urban <urbanc@in.tum.de>
parents: 774
diff changeset
     5
    local_theory -> (term * thm) * local_theory
789
Christian Urban <urbanc@in.tum.de>
parents: 776
diff changeset
     6
705
f51c6069cd17 New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 670
diff changeset
     7
  val quotdef_cmd: (Attrib.binding * string) * (mixfix * string) ->
277
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
    local_theory -> local_theory
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
end;
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    11
structure Quotient_Def: QUOTIENT_DEF =
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    12
struct
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    13
762
baac4639ecef avoided global "open"s - replaced by local "open"s
Christian Urban <urbanc@in.tum.de>
parents: 760
diff changeset
    14
open Quotient_Info;
774
b4ffb8826105 moved get_fun into quotient_term; this simplifies the overall including structure of the package
Christian Urban <urbanc@in.tum.de>
parents: 768
diff changeset
    15
open Quotient_Term;
762
baac4639ecef avoided global "open"s - replaced by local "open"s
Christian Urban <urbanc@in.tum.de>
parents: 760
diff changeset
    16
279
b2fd070c8833 slightly tuned
Christian Urban <urbanc@in.tum.de>
parents: 277
diff changeset
    17
(* wrapper for define *)
277
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    18
fun define name mx attr rhs lthy =
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    19
let
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    20
  val ((rhs, (_ , thm)), lthy') =
331
345c422b1cb5 updated to Isabelle 22nd November
Christian Urban <urbanc@in.tum.de>
parents: 329
diff changeset
    21
     Local_Theory.define ((name, mx), (attr, rhs)) lthy
277
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    22
in
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    23
  ((rhs, thm), lthy')
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    24
end
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    25
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    26
709
596467882518 Updated comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 705
diff changeset
    27
(* interface and syntax setup *)
596467882518 Updated comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 705
diff changeset
    28
804
Christian Urban <urbanc@in.tum.de>
parents: 801
diff changeset
    29
(* the ML-interface takes a 4-tuple consisting of     *)
Christian Urban <urbanc@in.tum.de>
parents: 801
diff changeset
    30
(*                                                    *)
Christian Urban <urbanc@in.tum.de>
parents: 801
diff changeset
    31
(* - the mixfix annotation                            *)
Christian Urban <urbanc@in.tum.de>
parents: 801
diff changeset
    32
(* - name and attributes                              *)
Christian Urban <urbanc@in.tum.de>
parents: 801
diff changeset
    33
(* - the new constant as term                         *)
Christian Urban <urbanc@in.tum.de>
parents: 801
diff changeset
    34
(* - the rhs of the definition as term                *)
Christian Urban <urbanc@in.tum.de>
parents: 801
diff changeset
    35
(*                                                    *)
Christian Urban <urbanc@in.tum.de>
parents: 801
diff changeset
    36
(* it returns the defined constant and its definition *)
Christian Urban <urbanc@in.tum.de>
parents: 801
diff changeset
    37
(* theorem; stores the data in the qconsts slot       *)
760
c1989de100b4 various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents: 719
diff changeset
    38
709
596467882518 Updated comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 705
diff changeset
    39
fun quotient_def mx attr lhs rhs lthy =
293
653460d3e849 tuned the code in quotient and quotient_def
Christian Urban <urbanc@in.tum.de>
parents: 290
diff changeset
    40
let
801
282fe9cc278e fixed comment errors
Christian Urban <urbanc@in.tum.de>
parents: 800
diff changeset
    41
  val Free (lhs_str, lhs_ty) = lhs; (* FIXME/TODO: this throws an excpt., if the const is already def.*)
705
f51c6069cd17 New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 670
diff changeset
    42
  val qconst_bname = Binding.name lhs_str;
776
d1064fa29424 renamed get_fun to absrep_fun; introduced explicit checked versions of the term functions
Christian Urban <urbanc@in.tum.de>
parents: 775
diff changeset
    43
  val absrep_trm = absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty) $ rhs
663
0dd10a900cae Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 598
diff changeset
    44
  val prop = Logic.mk_equals (lhs, absrep_trm)
0dd10a900cae Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 598
diff changeset
    45
  val (_, prop') = LocalDefs.cert_def lthy prop
0dd10a900cae Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 598
diff changeset
    46
  val (_, newrhs) = Primitive_Defs.abs_def prop'
310
fec6301a1989 added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
    47
663
0dd10a900cae Different syntax for definitions that allows overloading and retrieving of definitions by matching whole constants.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 598
diff changeset
    48
  val ((trm, thm), lthy') = define qconst_bname mx attr newrhs lthy
310
fec6301a1989 added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
    49
800
71225f4a4635 some slight tuning
Christian Urban <urbanc@in.tum.de>
parents: 799
diff changeset
    50
  (* data storage *)
799
0755f8fd56b3 renamed transfer to transform (Markus)
Christian Urban <urbanc@in.tum.de>
parents: 789
diff changeset
    51
  fun qcinfo phi = transform_qconsts phi {qconst = trm, rconst = rhs, def = thm}
319
0ae9d9e66cb7 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 318
diff changeset
    52
  val lthy'' = Local_Theory.declaration true
705
f51c6069cd17 New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 670
diff changeset
    53
                 (fn phi => qconsts_update_gen lhs_str (qcinfo phi)) lthy'
293
653460d3e849 tuned the code in quotient and quotient_def
Christian Urban <urbanc@in.tum.de>
parents: 290
diff changeset
    54
in
310
fec6301a1989 added a container for quotient constants (does not work yet though)
Christian Urban <urbanc@in.tum.de>
parents: 307
diff changeset
    55
  ((trm, thm), lthy'')
293
653460d3e849 tuned the code in quotient and quotient_def
Christian Urban <urbanc@in.tum.de>
parents: 290
diff changeset
    56
end
653460d3e849 tuned the code in quotient and quotient_def
Christian Urban <urbanc@in.tum.de>
parents: 290
diff changeset
    57
804
Christian Urban <urbanc@in.tum.de>
parents: 801
diff changeset
    58
fun quotdef_cmd ((attr, lhs_str), (mx, rhs_str)) lthy =
277
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    59
let
804
Christian Urban <urbanc@in.tum.de>
parents: 801
diff changeset
    60
  val lhs = Syntax.read_term lthy lhs_str
Christian Urban <urbanc@in.tum.de>
parents: 801
diff changeset
    61
  val rhs = Syntax.read_term lthy rhs_str
277
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    62
in
709
596467882518 Updated comments.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 705
diff changeset
    63
  quotient_def mx attr lhs rhs lthy |> snd
277
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    64
end
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    65
705
f51c6069cd17 New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 670
diff changeset
    66
val _ = OuterKeyword.keyword "as";
f51c6069cd17 New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 670
diff changeset
    67
279
b2fd070c8833 slightly tuned
Christian Urban <urbanc@in.tum.de>
parents: 277
diff changeset
    68
val quotdef_parser =
705
f51c6069cd17 New syntax for definitions.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 670
diff changeset
    69
  (SpecParse.opt_thm_name ":" --
760
c1989de100b4 various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents: 719
diff changeset
    70
     OuterParse.term) --
c1989de100b4 various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents: 719
diff changeset
    71
      (OuterParse.opt_mixfix' --| OuterParse.$$$ "as" --
c1989de100b4 various tunings; map_lookup now raises an exception; addition to FIXME-TODO
Christian Urban <urbanc@in.tum.de>
parents: 719
diff changeset
    72
         OuterParse.term)
279
b2fd070c8833 slightly tuned
Christian Urban <urbanc@in.tum.de>
parents: 277
diff changeset
    73
767
37285ec4387d on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
parents: 762
diff changeset
    74
val _ = OuterSyntax.local_theory "quotient_definition" 
37285ec4387d on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
parents: 762
diff changeset
    75
	  "definition for constants over the quotient type"
37285ec4387d on suggestion of Tobias renamed "quotient_def" to "quotient_definition"; needs new keyword file
Christian Urban <urbanc@in.tum.de>
parents: 762
diff changeset
    76
             OuterKeyword.thy_decl (quotdef_parser >> quotdef_cmd)
277
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    77
37636f2b1c19 separated the quotient_def into a separate file
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    78
end; (* structure *)