src/HOL/Tools/Quotient/quotient_term.ML
author Cezary Kaliszyk <kaliszyk@in.tum.de>
Fri, 19 Feb 2010 13:54:19 +0100
changeset 35222 4f1fba00f66d
child 35402 115a5a95710a
permissions -rw-r--r--
Initial version of HOL quotient package.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     1
(*  Title:      quotient_term.thy
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
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     4
    Constructs terms corresponding to goals from
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     5
    lifting theorems to quotient types.
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
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     8
signature QUOTIENT_TERM =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     9
sig
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    10
  exception LIFT_MATCH of string
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    11
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    12
  datatype flag = AbsF | RepF
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    13
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    14
  val absrep_fun: flag -> Proof.context -> typ * typ -> term
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    15
  val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    16
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    17
  (* Allows Nitpick to represent quotient types as single elements from raw type *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    18
  val absrep_const_chk: flag -> Proof.context -> string -> term
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    19
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    20
  val equiv_relation: Proof.context -> typ * typ -> term
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    21
  val equiv_relation_chk: Proof.context -> typ * typ -> term
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    22
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    23
  val regularize_trm: Proof.context -> term * term -> term
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    24
  val regularize_trm_chk: Proof.context -> term * term -> term
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    25
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    26
  val inj_repabs_trm: Proof.context -> term * term -> term
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    27
  val inj_repabs_trm_chk: Proof.context -> term * term -> term
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    28
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    29
  val quotient_lift_const: string * term -> local_theory -> term
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    30
  val quotient_lift_all: Proof.context -> term -> term
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    31
end;
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    32
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    33
structure Quotient_Term: QUOTIENT_TERM =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    34
struct
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    35
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    36
open Quotient_Info;
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    37
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    38
exception LIFT_MATCH of string
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    39
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    40
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    41
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    42
(*** Aggregate Rep/Abs Function ***)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    43
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    44
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    45
(* The flag RepF is for types in negative position; AbsF is for types
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    46
   in positive position. Because of this, function types need to be
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    47
   treated specially, since there the polarity changes.
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    48
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    49
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    50
datatype flag = AbsF | RepF
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    51
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    52
fun negF AbsF = RepF
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    53
  | negF RepF = AbsF
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    54
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    55
fun is_identity (Const (@{const_name "id"}, _)) = true
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    56
  | is_identity _ = false
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    57
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    58
fun mk_identity ty = Const (@{const_name "id"}, ty --> ty)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    59
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    60
fun mk_fun_compose flag (trm1, trm2) =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    61
  case flag of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    62
    AbsF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    63
  | RepF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    64
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    65
fun get_mapfun ctxt s =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    66
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    67
  val thy = ProofContext.theory_of ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    68
  val exn = LIFT_MATCH ("No map function for type " ^ quote s ^ " found.")
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    69
  val mapfun = #mapfun (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    70
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    71
  Const (mapfun, dummyT)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    72
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    73
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    74
(* makes a Free out of a TVar *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    75
fun mk_Free (TVar ((x, i), _)) = Free (unprefix "'" x ^ string_of_int i, dummyT)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    76
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    77
(* produces an aggregate map function for the
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    78
   rty-part of a quotient definition; abstracts
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    79
   over all variables listed in vs (these variables
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    80
   correspond to the type variables in rty)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    81
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    82
   for example for: (?'a list * ?'b)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    83
   it produces:     %a b. prod_map (map a) b
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    84
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    85
fun mk_mapfun ctxt vs rty =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    86
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    87
  val vs' = map (mk_Free) vs
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    88
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    89
  fun mk_mapfun_aux rty =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    90
    case rty of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    91
      TVar _ => mk_Free rty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    92
    | Type (_, []) => mk_identity rty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    93
    | Type (s, tys) => list_comb (get_mapfun ctxt s, map mk_mapfun_aux tys)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    94
    | _ => raise LIFT_MATCH "mk_mapfun (default)"
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    95
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    96
  fold_rev Term.lambda vs' (mk_mapfun_aux rty)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    97
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    98
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    99
(* looks up the (varified) rty and qty for
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   100
   a quotient definition
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   101
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   102
fun get_rty_qty ctxt s =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   103
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   104
  val thy = ProofContext.theory_of ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   105
  val exn = LIFT_MATCH ("No quotient type " ^ quote s ^ " found.")
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   106
  val qdata = (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   107
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   108
  (#rtyp qdata, #qtyp qdata)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   109
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   110
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   111
(* takes two type-environments and looks
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   112
   up in both of them the variable v, which
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   113
   must be listed in the environment
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   114
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   115
fun double_lookup rtyenv qtyenv v =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   116
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   117
  val v' = fst (dest_TVar v)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   118
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   119
  (snd (the (Vartab.lookup rtyenv v')), snd (the (Vartab.lookup qtyenv v')))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   120
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   121
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   122
(* matches a type pattern with a type *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   123
fun match ctxt err ty_pat ty =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   124
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   125
  val thy = ProofContext.theory_of ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   126
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   127
  Sign.typ_match thy (ty_pat, ty) Vartab.empty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   128
  handle MATCH_TYPE => err ctxt ty_pat ty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   129
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   130
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   131
(* produces the rep or abs constant for a qty *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   132
fun absrep_const flag ctxt qty_str =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   133
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   134
  val thy = ProofContext.theory_of ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   135
  val qty_name = Long_Name.base_name qty_str
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   136
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   137
  case flag of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   138
    AbsF => Const (Sign.full_bname thy ("abs_" ^ qty_name), dummyT)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   139
  | RepF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   140
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   141
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   142
(* Lets Nitpick represent elements of quotient types as elements of the raw type *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   143
fun absrep_const_chk flag ctxt qty_str =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   144
  Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   145
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   146
fun absrep_match_err ctxt ty_pat ty =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   147
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   148
  val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   149
  val ty_str = Syntax.string_of_typ ctxt ty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   150
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   151
  raise LIFT_MATCH (space_implode " "
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   152
    ["absrep_fun (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   153
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   154
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   155
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   156
(** generation of an aggregate absrep function **)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   157
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   158
(* - In case of equal types we just return the identity.
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   159
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   160
   - In case of TFrees we also return the identity.
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   161
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   162
   - In case of function types we recurse taking
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   163
     the polarity change into account.
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   164
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   165
   - If the type constructors are equal, we recurse for the
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   166
     arguments and build the appropriate map function.
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   167
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   168
   - If the type constructors are unequal, there must be an
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   169
     instance of quotient types:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   170
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   171
       - we first look up the corresponding rty_pat and qty_pat
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   172
         from the quotient definition; the arguments of qty_pat
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   173
         must be some distinct TVars
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   174
       - we then match the rty_pat with rty and qty_pat with qty;
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   175
         if matching fails the types do not correspond -> error
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   176
       - the matching produces two environments; we look up the
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   177
         assignments for the qty_pat variables and recurse on the
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   178
         assignments
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   179
       - we prefix the aggregate map function for the rty_pat,
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   180
         which is an abstraction over all type variables
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   181
       - finally we compose the result with the appropriate
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   182
         absrep function in case at least one argument produced
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   183
         a non-identity function /
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   184
         otherwise we just return the appropriate absrep
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   185
         function
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   186
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   187
     The composition is necessary for types like
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   188
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   189
        ('a list) list / ('a foo) foo
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   190
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   191
     The matching is necessary for types like
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   192
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   193
        ('a * 'a) list / 'a bar
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   194
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   195
     The test is necessary in order to eliminate superfluous
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   196
     identity maps.
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   197
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   198
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   199
fun absrep_fun flag ctxt (rty, qty) =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   200
  if rty = qty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   201
  then mk_identity rty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   202
  else
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   203
    case (rty, qty) of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   204
      (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   205
        let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   206
          val arg1 = absrep_fun (negF flag) ctxt (ty1, ty1')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   207
          val arg2 = absrep_fun flag ctxt (ty2, ty2')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   208
        in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   209
          list_comb (get_mapfun ctxt "fun", [arg1, arg2])
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   210
        end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   211
    | (Type (s, tys), Type (s', tys')) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   212
        if s = s'
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   213
        then
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   214
           let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   215
             val args = map (absrep_fun flag ctxt) (tys ~~ tys')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   216
           in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   217
             list_comb (get_mapfun ctxt s, args)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   218
           end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   219
        else
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   220
           let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   221
             val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   222
             val rtyenv = match ctxt absrep_match_err rty_pat rty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   223
             val qtyenv = match ctxt absrep_match_err qty_pat qty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   224
             val args_aux = map (double_lookup rtyenv qtyenv) vs
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   225
             val args = map (absrep_fun flag ctxt) args_aux
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   226
             val map_fun = mk_mapfun ctxt vs rty_pat
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   227
             val result = list_comb (map_fun, args)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   228
           in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   229
             if forall is_identity args
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   230
             then absrep_const flag ctxt s'
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   231
             else mk_fun_compose flag (absrep_const flag ctxt s', result)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   232
           end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   233
    | (TFree x, TFree x') =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   234
        if x = x'
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   235
        then mk_identity rty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   236
        else raise (LIFT_MATCH "absrep_fun (frees)")
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   237
    | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   238
    | _ => raise (LIFT_MATCH "absrep_fun (default)")
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   239
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   240
fun absrep_fun_chk flag ctxt (rty, qty) =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   241
  absrep_fun flag ctxt (rty, qty)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   242
  |> Syntax.check_term ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   243
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   244
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   245
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   246
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   247
(*** Aggregate Equivalence Relation ***)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   248
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   249
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   250
(* works very similar to the absrep generation,
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   251
   except there is no need for polarities
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   252
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   253
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   254
(* instantiates TVars so that the term is of type ty *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   255
fun force_typ ctxt trm ty =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   256
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   257
  val thy = ProofContext.theory_of ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   258
  val trm_ty = fastype_of trm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   259
  val ty_inst = Sign.typ_match thy (trm_ty, ty) Vartab.empty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   260
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   261
  map_types (Envir.subst_type ty_inst) trm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   262
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   263
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   264
fun is_eq (Const (@{const_name "op ="}, _)) = true
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   265
  | is_eq _ = false
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   266
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   267
fun mk_rel_compose (trm1, trm2) =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   268
  Const (@{const_name "rel_conj"}, dummyT) $ trm1 $ trm2
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   269
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   270
fun get_relmap ctxt s =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   271
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   272
  val thy = ProofContext.theory_of ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   273
  val exn = LIFT_MATCH ("get_relmap (no relation map function found for type " ^ s ^ ")")
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   274
  val relmap = #relmap (maps_lookup thy s) handle Quotient_Info.NotFound => raise exn
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   275
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   276
  Const (relmap, dummyT)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   277
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   278
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   279
fun mk_relmap ctxt vs rty =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   280
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   281
  val vs' = map (mk_Free) vs
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   282
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   283
  fun mk_relmap_aux rty =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   284
    case rty of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   285
      TVar _ => mk_Free rty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   286
    | Type (_, []) => HOLogic.eq_const rty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   287
    | Type (s, tys) => list_comb (get_relmap ctxt s, map mk_relmap_aux tys)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   288
    | _ => raise LIFT_MATCH ("mk_relmap (default)")
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   289
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   290
  fold_rev Term.lambda vs' (mk_relmap_aux rty)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   291
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   292
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   293
fun get_equiv_rel ctxt s =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   294
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   295
  val thy = ProofContext.theory_of ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   296
  val exn = LIFT_MATCH ("get_quotdata (no quotient found for type " ^ s ^ ")")
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   297
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   298
  #equiv_rel (quotdata_lookup thy s) handle Quotient_Info.NotFound => raise exn
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   299
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   300
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   301
fun equiv_match_err ctxt ty_pat ty =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   302
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   303
  val ty_pat_str = Syntax.string_of_typ ctxt ty_pat
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   304
  val ty_str = Syntax.string_of_typ ctxt ty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   305
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   306
  raise LIFT_MATCH (space_implode " "
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   307
    ["equiv_relation (Types ", quote ty_pat_str, "and", quote ty_str, " do not match.)"])
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   308
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   309
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   310
(* builds the aggregate equivalence relation
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   311
   that will be the argument of Respects
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   312
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   313
fun equiv_relation ctxt (rty, qty) =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   314
  if rty = qty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   315
  then HOLogic.eq_const rty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   316
  else
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   317
    case (rty, qty) of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   318
      (Type (s, tys), Type (s', tys')) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   319
       if s = s'
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   320
       then
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   321
         let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   322
           val args = map (equiv_relation ctxt) (tys ~~ tys')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   323
         in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   324
           list_comb (get_relmap ctxt s, args)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   325
         end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   326
       else
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   327
         let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   328
           val (rty_pat, qty_pat as Type (_, vs)) = get_rty_qty ctxt s'
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   329
           val rtyenv = match ctxt equiv_match_err rty_pat rty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   330
           val qtyenv = match ctxt equiv_match_err qty_pat qty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   331
           val args_aux = map (double_lookup rtyenv qtyenv) vs
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   332
           val args = map (equiv_relation ctxt) args_aux
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   333
           val rel_map = mk_relmap ctxt vs rty_pat
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   334
           val result = list_comb (rel_map, args)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   335
           val eqv_rel = get_equiv_rel ctxt s'
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   336
           val eqv_rel' = force_typ ctxt eqv_rel ([rty, rty] ---> @{typ bool})
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   337
         in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   338
           if forall is_eq args
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   339
           then eqv_rel'
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   340
           else mk_rel_compose (result, eqv_rel')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   341
         end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   342
      | _ => HOLogic.eq_const rty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   343
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   344
fun equiv_relation_chk ctxt (rty, qty) =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   345
  equiv_relation ctxt (rty, qty)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   346
  |> Syntax.check_term ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   347
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   348
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   349
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   350
(*** Regularization ***)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   351
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   352
(* Regularizing an rtrm means:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   353
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   354
 - Quantifiers over types that need lifting are replaced
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   355
   by bounded quantifiers, for example:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   356
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   357
      All P  ----> All (Respects R) P
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   358
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   359
   where the aggregate relation R is given by the rty and qty;
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   360
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   361
 - Abstractions over types that need lifting are replaced
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   362
   by bounded abstractions, for example:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   363
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   364
      %x. P  ----> Ball (Respects R) %x. P
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   365
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   366
 - Equalities over types that need lifting are replaced by
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   367
   corresponding equivalence relations, for example:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   368
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   369
      A = B  ----> R A B
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   370
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   371
   or
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   372
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   373
      A = B  ----> (R ===> R) A B
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   374
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   375
   for more complicated types of A and B
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   376
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   377
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   378
 The regularize_trm accepts raw theorems in which equalities
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   379
 and quantifiers match exactly the ones in the lifted theorem
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   380
 but also accepts partially regularized terms.
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   381
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   382
 This means that the raw theorems can have:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   383
   Ball (Respects R),  Bex (Respects R), Bex1_rel (Respects R), Babs, R
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   384
 in the places where:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   385
   All, Ex, Ex1, %, (op =)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   386
 is required the lifted theorem.
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   387
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   388
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   389
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   390
val mk_babs = Const (@{const_name Babs}, dummyT)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   391
val mk_ball = Const (@{const_name Ball}, dummyT)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   392
val mk_bex  = Const (@{const_name Bex}, dummyT)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   393
val mk_bex1_rel = Const (@{const_name Bex1_rel}, dummyT)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   394
val mk_resp = Const (@{const_name Respects}, dummyT)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   395
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   396
(* - applies f to the subterm of an abstraction,
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   397
     otherwise to the given term,
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   398
   - used by regularize, therefore abstracted
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   399
     variables do not have to be treated specially
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   400
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   401
fun apply_subt f (trm1, trm2) =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   402
  case (trm1, trm2) of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   403
    (Abs (x, T, t), Abs (_ , _, t')) => Abs (x, T, f (t, t'))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   404
  | _ => f (trm1, trm2)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   405
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   406
fun term_mismatch str ctxt t1 t2 =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   407
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   408
  val t1_str = Syntax.string_of_term ctxt t1
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   409
  val t2_str = Syntax.string_of_term ctxt t2
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   410
  val t1_ty_str = Syntax.string_of_typ ctxt (fastype_of t1)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   411
  val t2_ty_str = Syntax.string_of_typ ctxt (fastype_of t2)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   412
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   413
  raise LIFT_MATCH (cat_lines [str, t1_str ^ "::" ^ t1_ty_str, t2_str ^ "::" ^ t2_ty_str])
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   414
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   415
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   416
(* the major type of All and Ex quantifiers *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   417
fun qnt_typ ty = domain_type (domain_type ty)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   418
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   419
(* Checks that two types match, for example:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   420
     rty -> rty   matches   qty -> qty *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   421
fun matches_typ thy rT qT =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   422
  if rT = qT then true else
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   423
  case (rT, qT) of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   424
    (Type (rs, rtys), Type (qs, qtys)) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   425
      if rs = qs then
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   426
        if length rtys <> length qtys then false else
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   427
        forall (fn x => x = true) (map2 (matches_typ thy) rtys qtys)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   428
      else
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   429
        (case Quotient_Info.quotdata_lookup_raw thy qs of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   430
          SOME quotinfo => Sign.typ_instance thy (rT, #rtyp quotinfo)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   431
        | NONE => false)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   432
  | _ => false
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   433
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   434
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   435
(* produces a regularized version of rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   436
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   437
   - the result might contain dummyTs
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   438
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   439
   - for regularisation we do not need any
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   440
     special treatment of bound variables
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   441
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   442
fun regularize_trm ctxt (rtrm, qtrm) =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   443
  case (rtrm, qtrm) of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   444
    (Abs (x, ty, t), Abs (_, ty', t')) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   445
       let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   446
         val subtrm = Abs(x, ty, regularize_trm ctxt (t, t'))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   447
       in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   448
         if ty = ty' then subtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   449
         else mk_babs $ (mk_resp $ equiv_relation ctxt (ty, ty')) $ subtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   450
       end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   451
  | (Const (@{const_name "Babs"}, T) $ resrel $ (t as (Abs (_, ty, _))), t' as (Abs (_, ty', _))) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   452
       let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   453
         val subtrm = regularize_trm ctxt (t, t')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   454
         val needres = mk_resp $ equiv_relation_chk ctxt (ty, ty')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   455
       in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   456
         if resrel <> needres
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   457
         then term_mismatch "regularize (Babs)" ctxt resrel needres
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   458
         else mk_babs $ resrel $ subtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   459
       end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   460
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   461
  | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   462
       let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   463
         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   464
       in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   465
         if ty = ty' then Const (@{const_name "All"}, ty) $ subtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   466
         else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   467
       end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   468
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   469
  | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   470
       let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   471
         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   472
       in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   473
         if ty = ty' then Const (@{const_name "Ex"}, ty) $ subtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   474
         else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   475
       end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   476
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   477
  | (Const (@{const_name "Ex1"}, ty) $ (Abs (_, _,
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   478
      (Const (@{const_name "op &"}, _) $ (Const (@{const_name "op :"}, _) $ _ $
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   479
        (Const (@{const_name "Respects"}, _) $ resrel)) $ (t $ _)))),
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   480
     Const (@{const_name "Ex1"}, ty') $ t') =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   481
       let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   482
         val t_ = incr_boundvars (~1) t
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   483
         val subtrm = apply_subt (regularize_trm ctxt) (t_, t')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   484
         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   485
       in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   486
         if resrel <> needrel
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   487
         then term_mismatch "regularize (Bex1)" ctxt resrel needrel
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   488
         else mk_bex1_rel $ resrel $ subtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   489
       end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   490
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   491
  | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   492
       let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   493
         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   494
       in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   495
         if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   496
         else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   497
       end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   498
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   499
  | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   500
     Const (@{const_name "All"}, ty') $ t') =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   501
       let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   502
         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   503
         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   504
       in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   505
         if resrel <> needrel
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   506
         then term_mismatch "regularize (Ball)" ctxt resrel needrel
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   507
         else mk_ball $ (mk_resp $ resrel) $ subtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   508
       end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   509
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   510
  | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   511
     Const (@{const_name "Ex"}, ty') $ t') =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   512
       let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   513
         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   514
         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   515
       in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   516
         if resrel <> needrel
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   517
         then term_mismatch "regularize (Bex)" ctxt resrel needrel
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   518
         else mk_bex $ (mk_resp $ resrel) $ subtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   519
       end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   520
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   521
  | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   522
       let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   523
         val subtrm = apply_subt (regularize_trm ctxt) (t, t')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   524
         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   525
       in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   526
         if resrel <> needrel
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   527
         then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   528
         else mk_bex1_rel $ resrel $ subtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   529
       end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   530
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   531
  | (* equalities need to be replaced by appropriate equivalence relations *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   532
    (Const (@{const_name "op ="}, ty), Const (@{const_name "op ="}, ty')) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   533
         if ty = ty' then rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   534
         else equiv_relation ctxt (domain_type ty, domain_type ty')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   535
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   536
  | (* in this case we just check whether the given equivalence relation is correct *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   537
    (rel, Const (@{const_name "op ="}, ty')) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   538
       let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   539
         val rel_ty = fastype_of rel
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   540
         val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   541
       in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   542
         if rel' aconv rel then rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   543
         else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   544
       end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   545
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   546
  | (_, Const _) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   547
       let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   548
         val thy = ProofContext.theory_of ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   549
         fun same_const (Const (s, T)) (Const (s', T')) = (s = s') andalso matches_typ thy T T'
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   550
           | same_const _ _ = false
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   551
       in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   552
         if same_const rtrm qtrm then rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   553
         else
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   554
           let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   555
             val rtrm' = #rconst (qconsts_lookup thy qtrm)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   556
               handle Quotient_Info.NotFound => term_mismatch "regularize(constant notfound)" ctxt rtrm qtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   557
           in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   558
             if Pattern.matches thy (rtrm', rtrm)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   559
             then rtrm else term_mismatch "regularize(constant mismatch)" ctxt rtrm qtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   560
           end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   561
       end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   562
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   563
  | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   564
     ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   565
       regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   566
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   567
  | (((t1 as Const (@{const_name "split"}, _)) $ Abs (v1, ty, s1)),
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   568
     ((t2 as Const (@{const_name "split"}, _)) $ Abs (v2, _ , s2))) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   569
       regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   570
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   571
  | (t1 $ t2, t1' $ t2') =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   572
       regularize_trm ctxt (t1, t1') $ regularize_trm ctxt (t2, t2')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   573
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   574
  | (Bound i, Bound i') =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   575
       if i = i' then rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   576
       else raise (LIFT_MATCH "regularize (bounds mismatch)")
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   577
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   578
  | _ =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   579
       let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   580
         val rtrm_str = Syntax.string_of_term ctxt rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   581
         val qtrm_str = Syntax.string_of_term ctxt qtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   582
       in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   583
         raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   584
       end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   585
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   586
fun regularize_trm_chk ctxt (rtrm, qtrm) =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   587
  regularize_trm ctxt (rtrm, qtrm)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   588
  |> Syntax.check_term ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   589
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   590
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   591
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   592
(*** Rep/Abs Injection ***)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   593
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   594
(*
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   595
Injection of Rep/Abs means:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   596
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   597
  For abstractions:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   598
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   599
  * If the type of the abstraction needs lifting, then we add Rep/Abs
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   600
    around the abstraction; otherwise we leave it unchanged.
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   601
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   602
  For applications:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   603
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   604
  * If the application involves a bounded quantifier, we recurse on
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   605
    the second argument. If the application is a bounded abstraction,
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   606
    we always put an Rep/Abs around it (since bounded abstractions
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   607
    are assumed to always need lifting). Otherwise we recurse on both
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   608
    arguments.
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   609
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   610
  For constants:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   611
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   612
  * If the constant is (op =), we leave it always unchanged.
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   613
    Otherwise the type of the constant needs lifting, we put
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   614
    and Rep/Abs around it.
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   615
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   616
  For free variables:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   617
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   618
  * We put a Rep/Abs around it if the type needs lifting.
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   619
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   620
  Vars case cannot occur.
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   621
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   622
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   623
fun mk_repabs ctxt (T, T') trm =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   624
  absrep_fun RepF ctxt (T, T') $ (absrep_fun AbsF ctxt (T, T') $ trm)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   625
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   626
fun inj_repabs_err ctxt msg rtrm qtrm =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   627
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   628
  val rtrm_str = Syntax.string_of_term ctxt rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   629
  val qtrm_str = Syntax.string_of_term ctxt qtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   630
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   631
  raise LIFT_MATCH (space_implode " " [msg, quote rtrm_str, "and", quote qtrm_str])
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   632
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   633
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   634
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   635
(* bound variables need to be treated properly,
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   636
   as the type of subterms needs to be calculated   *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   637
fun inj_repabs_trm ctxt (rtrm, qtrm) =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   638
 case (rtrm, qtrm) of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   639
    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   640
       Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   641
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   642
  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   643
       Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   644
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   645
  | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   646
      let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   647
        val rty = fastype_of rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   648
        val qty = fastype_of qtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   649
      in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   650
        mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   651
      end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   652
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   653
  | (Abs (x, T, t), Abs (x', T', t')) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   654
      let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   655
        val rty = fastype_of rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   656
        val qty = fastype_of qtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   657
        val (y, s) = Term.dest_abs (x, T, t)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   658
        val (_, s') = Term.dest_abs (x', T', t')
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   659
        val yvar = Free (y, T)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   660
        val result = Term.lambda_name (y, yvar) (inj_repabs_trm ctxt (s, s'))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   661
      in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   662
        if rty = qty then result
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   663
        else mk_repabs ctxt (rty, qty) result
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   664
      end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   665
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   666
  | (t $ s, t' $ s') =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   667
       (inj_repabs_trm ctxt (t, t')) $ (inj_repabs_trm ctxt (s, s'))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   668
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   669
  | (Free (_, T), Free (_, T')) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   670
        if T = T' then rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   671
        else mk_repabs ctxt (T, T') rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   672
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   673
  | (_, Const (@{const_name "op ="}, _)) => rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   674
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   675
  | (_, Const (_, T')) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   676
      let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   677
        val rty = fastype_of rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   678
      in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   679
        if rty = T' then rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   680
        else mk_repabs ctxt (rty, T') rtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   681
      end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   682
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   683
  | _ => inj_repabs_err ctxt "injection (default):" rtrm qtrm
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   684
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   685
fun inj_repabs_trm_chk ctxt (rtrm, qtrm) =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   686
  inj_repabs_trm ctxt (rtrm, qtrm)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   687
  |> Syntax.check_term ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   688
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   689
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   690
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   691
(*** Wrapper for automatically transforming an rthm into a qthm ***)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   692
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   693
(* subst_tys takes a list of (rty, qty) substitution pairs
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   694
   and replaces all occurences of rty in the given type
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   695
   by appropriate qty, with substitution *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   696
fun subst_ty thy ty (rty, qty) r =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   697
  if r <> NONE then r else
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   698
  case try (Sign.typ_match thy (rty, ty)) Vartab.empty of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   699
    SOME inst => SOME (Envir.subst_type inst qty)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   700
  | NONE => NONE
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   701
fun subst_tys thy substs ty =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   702
  case fold (subst_ty thy ty) substs NONE of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   703
    SOME ty => ty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   704
  | NONE =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   705
      (case ty of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   706
        Type (s, tys) => Type (s, map (subst_tys thy substs) tys)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   707
      | x => x)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   708
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   709
(* subst_trms takes a list of (rtrm, qtrm) substitution pairs
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   710
   and if the given term matches any of the raw terms it
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   711
   returns the appropriate qtrm instantiated. If none of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   712
   them matched it returns NONE. *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   713
fun subst_trm thy t (rtrm, qtrm) s =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   714
  if s <> NONE then s else
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   715
    case try (Pattern.match thy (rtrm, t)) (Vartab.empty, Vartab.empty) of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   716
      SOME inst => SOME (Envir.subst_term inst qtrm)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   717
    | NONE => NONE;
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   718
fun subst_trms thy substs t = fold (subst_trm thy t) substs NONE
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   719
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   720
(* prepares type and term substitution pairs to be used by above
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   721
   functions that let replace all raw constructs by appropriate
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   722
   lifted counterparts. *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   723
fun get_ty_trm_substs ctxt =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   724
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   725
  val thy = ProofContext.theory_of ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   726
  val quot_infos  = Quotient_Info.quotdata_dest ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   727
  val const_infos = Quotient_Info.qconsts_dest ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   728
  val ty_substs = map (fn ri => (#rtyp ri, #qtyp ri)) quot_infos
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   729
  val const_substs = map (fn ci => (#rconst ci, #qconst ci)) const_infos
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   730
  fun rel_eq rel = HOLogic.eq_const (subst_tys thy ty_substs (domain_type (fastype_of rel)))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   731
  val rel_substs = map (fn ri => (#equiv_rel ri, rel_eq (#equiv_rel ri))) quot_infos
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   732
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   733
  (ty_substs, const_substs @ rel_substs)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   734
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   735
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   736
fun quotient_lift_const (b, t) ctxt =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   737
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   738
  val thy = ProofContext.theory_of ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   739
  val (ty_substs, _) = get_ty_trm_substs ctxt;
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   740
  val (_, ty) = dest_Const t;
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   741
  val nty = subst_tys thy ty_substs ty;
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   742
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   743
  Free(b, nty)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   744
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   745
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   746
(*
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   747
Takes a term and
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   748
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   749
* replaces raw constants by the quotient constants
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   750
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   751
* replaces equivalence relations by equalities
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   752
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   753
* replaces raw types by the quotient types
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   754
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   755
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   756
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   757
fun quotient_lift_all ctxt t =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   758
let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   759
  val thy = ProofContext.theory_of ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   760
  val (ty_substs, substs) = get_ty_trm_substs ctxt
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   761
  fun lift_aux t =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   762
    case subst_trms thy substs t of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   763
      SOME x => x
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   764
    | NONE =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   765
      (case t of
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   766
        a $ b => lift_aux a $ lift_aux b
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   767
      | Abs(a, ty, s) =>
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   768
          let
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   769
            val (y, s') = Term.dest_abs (a, ty, s)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   770
            val nty = subst_tys thy ty_substs ty
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   771
          in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   772
            Abs(y, nty, abstract_over (Free (y, nty), lift_aux s'))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   773
          end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   774
      | Free(n, ty) => Free(n, subst_tys thy ty_substs ty)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   775
      | Var(n, ty) => Var(n, subst_tys thy ty_substs ty)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   776
      | Bound i => Bound i
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   777
      | Const(s, ty) => Const(s, subst_tys thy ty_substs ty))
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   778
in
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   779
  lift_aux t
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   780
end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   781
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   782
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   783
end; (* structure *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   784
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   785
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   786