src/HOL/Tools/functorial_mappers.ML
author haftmann
Wed, 17 Nov 2010 17:27:25 +0100
changeset 40594 fae1da97bb5e
parent 40587 5206d19038c7
child 40597 19b449037ace
permissions -rw-r--r--
infer variances of user-given mapper operation; proper thm storing
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
40586
fe4f6703c59e fixed typo
haftmann
parents: 40584
diff changeset
     1
(*  Title:      HOL/Tools/functorial_mappers.ML
40582
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
     2
    Author:     Florian Haftmann, TU Muenchen
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
     3
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
     4
Functorial mappers on types.
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
     5
*)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
     6
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
     7
signature FUNCTORIAL_MAPPERS =
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
     8
sig
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
     9
  val find_atomic: theory -> typ -> (typ * (bool * bool)) list
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    10
  val construct_mapper: theory -> (string * bool -> term)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    11
    -> bool -> typ -> typ -> term
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    12
  val register: string -> string -> (sort * (bool * bool)) list -> thm -> thm
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    13
    -> theory -> theory
40584
28cc2acbc58a ML signature interface
haftmann
parents: 40583
diff changeset
    14
  val type_mapper: term -> theory -> Proof.state
40582
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    15
  type entry
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    16
  val entries: theory -> entry Symtab.table
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    17
end;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    18
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    19
structure Functorial_Mappers : FUNCTORIAL_MAPPERS =
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    20
struct
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    21
40594
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
    22
val concatenateN = "concatenate";
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
    23
val identityN = "identity";
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
    24
40582
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    25
(** functorial mappers and their properties **)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    26
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    27
(* bookkeeping *)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    28
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    29
type entry = { mapper: string, variances: (sort * (bool * bool)) list,
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    30
  concatenate: thm, identity: thm };
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    31
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    32
structure Data = Theory_Data(
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    33
  type T = entry Symtab.table
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    34
  val empty = Symtab.empty
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    35
  val merge = Symtab.merge (K true)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    36
  val extend = I
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    37
);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    38
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    39
val entries = Data.get;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    40
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    41
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    42
(* type analysis *)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    43
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    44
fun find_atomic thy T =
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    45
  let
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    46
    val variances_of = Option.map #variances o Symtab.lookup (Data.get thy);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    47
    fun add_variance is_contra T =
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    48
      AList.map_default (op =) (T, (false, false))
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    49
        ((if is_contra then apsnd else apfst) (K true));
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    50
    fun analyze' is_contra (_, (co, contra)) T =
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    51
      (if co then analyze is_contra T else I)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    52
      #> (if contra then analyze (not is_contra) T else I)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    53
    and analyze is_contra (T as Type (tyco, Ts)) = (case variances_of tyco
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    54
          of NONE => add_variance is_contra T
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    55
           | SOME variances => fold2 (analyze' is_contra) variances Ts)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    56
      | analyze is_contra T = add_variance is_contra T;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    57
  in analyze false T [] end;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    58
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    59
fun construct_mapper thy atomic =
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    60
  let
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    61
    val lookup = the o Symtab.lookup (Data.get thy);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    62
    fun constructs is_contra (_, (co, contra)) T T' =
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    63
      (if co then [construct is_contra T T'] else [])
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    64
      @ (if contra then [construct (not is_contra) T T'] else [])
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    65
    and construct is_contra (T as Type (tyco, Ts)) (T' as Type (_, Ts')) =
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    66
          let
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    67
            val { mapper, variances, ... } = lookup tyco;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    68
            val args = maps (fn (arg_pattern, (T, T')) =>
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    69
              constructs is_contra arg_pattern T T')
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    70
                (variances ~~ (Ts ~~ Ts'));
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    71
            val (U, U') = if is_contra then (T', T) else (T, T');
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    72
          in list_comb (Const (mapper, map fastype_of args ---> U --> U'), args) end
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    73
      | construct is_contra (TFree (v, _)) (TFree _) = atomic (v, is_contra);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    74
  in construct end;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    75
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    76
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    77
(* mapper properties *)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    78
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    79
fun make_concatenate_prop variances (tyco, mapper) =
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    80
  let
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    81
    fun invents n k nctxt =
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    82
      let
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    83
        val names = Name.invents nctxt n k;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    84
      in (names, fold Name.declare names nctxt) end;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    85
    val (((vs1, vs2), vs3), _) = Name.context
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    86
      |> invents Name.aT (length variances)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    87
      ||>> invents Name.aT (length variances)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    88
      ||>> invents Name.aT (length variances);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    89
    fun mk_Ts vs = map2 (fn v => fn (sort, _) => TFree (v, sort))
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    90
      vs variances;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    91
    val (Ts1, Ts2, Ts3) = (mk_Ts vs1, mk_Ts vs2, mk_Ts vs3);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    92
    fun mk_argT ((T, T'), (_, (co, contra))) =
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    93
      (if co then [(T --> T')] else [])
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    94
      @ (if contra then [(T' --> T)] else []);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    95
    val contras = maps (fn (_, (co, contra)) =>
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    96
      (if co then [false] else []) @ (if contra then [true] else [])) variances;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    97
    val Ts21 = maps mk_argT ((Ts2 ~~ Ts1) ~~ variances);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    98
    val Ts32 = maps mk_argT ((Ts3 ~~ Ts2) ~~ variances);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
    99
    val ((names21, names32), nctxt) = Name.context
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   100
      |> invents "f" (length Ts21)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   101
      ||>> invents "f" (length Ts32);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   102
    val T1 = Type (tyco, Ts1);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   103
    val T2 = Type (tyco, Ts2);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   104
    val T3 = Type (tyco, Ts3);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   105
    val x = Free (the_single (Name.invents nctxt "a" 1), T3);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   106
    val (args21, args32) = (names21 ~~ Ts21, names32 ~~ Ts32);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   107
    val args31 = map2 (fn is_contra => fn ((f21, T21), (f32, T32)) =>
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   108
      if not is_contra then
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   109
        Abs ("x", domain_type T32, Free (f21, T21) $ (Free (f32, T32) $ Bound 0))
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   110
      else
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   111
        Abs ("x", domain_type T21, Free (f32, T32) $ (Free (f21, T21) $ Bound 0))
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   112
      ) contras (args21 ~~ args32)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   113
    fun mk_mapper T T' args = list_comb (Const (mapper,
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   114
      map fastype_of args ---> T --> T'), args);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   115
    val lhs = mk_mapper T2 T1 (map Free args21) $
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   116
      (mk_mapper T3 T2 (map Free args32) $ x);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   117
    val rhs = mk_mapper T3 T1 args31 $ x;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   118
  in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, rhs)) end;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   119
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   120
fun make_identity_prop variances (tyco, mapper) =
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   121
  let
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   122
    val vs = Name.invents Name.context Name.aT (length variances);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   123
    val Ts = map2 (fn v => fn (sort, _) => TFree (v, sort)) vs variances;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   124
    fun bool_num b = if b then 1 else 0;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   125
    fun mk_argT (T, (_, (co, contra))) =
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   126
      replicate (bool_num co + bool_num contra) (T --> T)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   127
    val Ts' = maps mk_argT (Ts ~~ variances)
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   128
    val T = Type (tyco, Ts);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   129
    val x = Free ("a", T);
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   130
    val lhs = list_comb (Const (mapper, Ts' ---> T --> T),
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   131
      map (fn T => Abs ("x", domain_type T, Bound 0)) Ts') $ x;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   132
  in (x, (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhs, x)) end;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   133
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   134
40587
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   135
(* registering mappers *)
40582
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   136
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   137
fun register tyco mapper variances raw_concatenate raw_identity thy =
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   138
  let
40594
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   139
    val concatenate_prop = uncurry Logic.all
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   140
      (make_concatenate_prop variances (tyco, mapper));
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   141
    val identity_prop = uncurry Logic.all
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   142
      (make_identity_prop variances (tyco, mapper));
40582
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   143
    val concatenate = Goal.prove_global thy
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   144
      (Term.add_free_names concatenate_prop []) [] concatenate_prop
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   145
      (K (ALLGOALS (ProofContext.fact_tac [raw_concatenate])));
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   146
    val identity = Goal.prove_global thy
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   147
      (Term.add_free_names identity_prop []) [] identity_prop
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   148
      (K (ALLGOALS (ProofContext.fact_tac [raw_identity])));
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   149
  in
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   150
    thy
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   151
    |> Data.map (Symtab.update (tyco, { mapper = mapper,
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   152
        variances = variances,
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   153
        concatenate = concatenate, identity = identity }))
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   154
  end;
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   155
40594
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   156
fun consume eq x [] = (false, [])
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   157
  | consume eq x (ys as z :: zs) = if eq (x, z) then (true, zs) else (false, ys);
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   158
40587
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   159
fun split_mapper_typ "fun" T =
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   160
      let
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   161
        val (Ts', T') = strip_type T;
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   162
        val (Ts'', T'') = split_last Ts';
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   163
        val (Ts''', T''') = split_last Ts'';
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   164
      in (Ts''', T''', T'' --> T') end
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   165
  | split_mapper_typ tyco T =
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   166
      let
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   167
        val (Ts', T') = strip_type T;
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   168
        val (Ts'', T'') = split_last Ts';
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   169
      in (Ts'', T'', T') end;
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   170
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   171
fun analyze_variances thy tyco T =
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   172
  let
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   173
    fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ_global thy T);
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   174
    val (Ts, T1, T2) = split_mapper_typ tyco T
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   175
      handle List.Empty => bad_typ ();
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   176
    val _ = pairself
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   177
      ((fn tyco' => if tyco' = tyco then () else bad_typ ()) o fst o dest_Type) (T1, T2)
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   178
    val (vs1, vs2) = pairself (map dest_TFree o snd o dest_Type) (T1, T2)
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   179
      handle TYPE _ => bad_typ ();
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   180
    val _ = if has_duplicates (eq_fst (op =)) (vs1 @ vs2)
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   181
      then bad_typ () else ();
40594
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   182
    fun check_variance_pair (var1 as (v1, sort1), var2 as (v2, sort2)) =
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   183
      let
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   184
        val coT = TFree var1 --> TFree var2;
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   185
        val contraT = TFree var2 --> TFree var1;
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   186
        val sort = Sign.inter_sort thy (sort1, sort2);
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   187
      in
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   188
        consume (op =) coT
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   189
        ##>> consume (op =) contraT
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   190
        #>> pair sort
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   191
      end;
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   192
    val (variances, left_variances) = fold_map check_variance_pair (vs1 ~~ vs2) Ts;
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   193
    val _ = if null left_variances then () else bad_typ ();
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   194
  in variances end;
40587
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   195
40583
6fed6f946471 stub for Isar command interface
haftmann
parents: 40582
diff changeset
   196
fun gen_type_mapper prep_term raw_t thy =
6fed6f946471 stub for Isar command interface
haftmann
parents: 40582
diff changeset
   197
  let
40587
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   198
    val (mapper, T) = case prep_term thy raw_t
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   199
     of Const cT => cT
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   200
      | t => error ("No constant: " ^ Syntax.string_of_term_global thy t);
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   201
    val _ = Type.no_tvars T;
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   202
    fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   203
      | add_tycos _ = I;
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   204
    val tycos = add_tycos T [];
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   205
    val tyco = if tycos = ["fun"] then "fun"
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   206
      else case remove (op =) "fun" tycos
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   207
       of [tyco] => tyco
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   208
        | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ_global thy T);
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   209
    val variances = analyze_variances thy tyco T;
40594
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   210
    val concatenate_prop = uncurry Logic.all
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   211
      (make_concatenate_prop variances (tyco, mapper));
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   212
    val identity_prop = uncurry Logic.all
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   213
      (make_identity_prop variances (tyco, mapper));
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   214
    val qualify = Binding.qualify true (Long_Name.base_name mapper) o Binding.name;
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   215
    fun after_qed [single_concatenate, single_identity] lthy =
40587
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   216
      lthy
40594
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   217
      |> Local_Theory.note ((qualify concatenateN, []), single_concatenate)
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   218
      ||>> Local_Theory.note ((qualify identityN, []), single_identity)
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   219
      |-> (fn ((_, [concatenate]), (_, [identity])) =>
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   220
          (Local_Theory.background_theory o Data.map)
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   221
            (Symtab.update (tyco, { mapper = mapper, variances = variances,
fae1da97bb5e infer variances of user-given mapper operation; proper thm storing
haftmann
parents: 40587
diff changeset
   222
              concatenate = concatenate, identity = identity })));
40583
6fed6f946471 stub for Isar command interface
haftmann
parents: 40582
diff changeset
   223
  in
6fed6f946471 stub for Isar command interface
haftmann
parents: 40582
diff changeset
   224
    thy
6fed6f946471 stub for Isar command interface
haftmann
parents: 40582
diff changeset
   225
    |> Named_Target.theory_init
40587
5206d19038c7 emerging Isar command interface
haftmann
parents: 40586
diff changeset
   226
    |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [concatenate_prop, identity_prop])
40583
6fed6f946471 stub for Isar command interface
haftmann
parents: 40582
diff changeset
   227
  end
6fed6f946471 stub for Isar command interface
haftmann
parents: 40582
diff changeset
   228
6fed6f946471 stub for Isar command interface
haftmann
parents: 40582
diff changeset
   229
val type_mapper = gen_type_mapper Sign.cert_term;
6fed6f946471 stub for Isar command interface
haftmann
parents: 40582
diff changeset
   230
val type_mapper_cmd = gen_type_mapper Syntax.read_term_global;
6fed6f946471 stub for Isar command interface
haftmann
parents: 40582
diff changeset
   231
6fed6f946471 stub for Isar command interface
haftmann
parents: 40582
diff changeset
   232
val _ =
6fed6f946471 stub for Isar command interface
haftmann
parents: 40582
diff changeset
   233
  Outer_Syntax.command "type_mapper" "register functorial mapper for type with its properties" Keyword.thy_goal
6fed6f946471 stub for Isar command interface
haftmann
parents: 40582
diff changeset
   234
    (Parse.term >> (fn t => Toplevel.print o (Toplevel.theory_to_proof (type_mapper_cmd t))));
6fed6f946471 stub for Isar command interface
haftmann
parents: 40582
diff changeset
   235
40582
968c481aa18c module for functorial mappers
haftmann
parents:
diff changeset
   236
end;