src/HOL/Library/conditional_parametricity.ML
author wenzelm
Tue May 15 13:57:39 2018 +0200 (16 months ago)
changeset 68189 6163c90694ef
parent 67649 1e1782c1aedf
child 69593 3dda49e08b9d
permissions -rw-r--r--
tuned headers;
traytel@67224
     1
(*  Title:    HOL/Library/conditional_parametricity.ML
traytel@67224
     2
    Author:   Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel, ETH Z├╝rich
traytel@67224
     3
traytel@67224
     4
A conditional parametricity prover
traytel@67224
     5
*)
traytel@67224
     6
traytel@67224
     7
signature CONDITIONAL_PARAMETRICITY =
traytel@67224
     8
sig
traytel@67224
     9
  exception WARNING of string
traytel@67224
    10
  type settings =
traytel@67224
    11
    {suppress_print_theorem: bool,
traytel@67224
    12
    suppress_warnings: bool,
traytel@67224
    13
    warnings_as_errors: bool,
traytel@67224
    14
    use_equality_heuristic: bool}
traytel@67224
    15
  val default_settings: settings
traytel@67224
    16
  val quiet_settings: settings
traytel@67224
    17
traytel@67224
    18
  val parametric_constant: settings -> Attrib.binding * thm -> Proof.context ->
traytel@67224
    19
    (thm * Proof.context)
traytel@67224
    20
  val get_parametricity_theorems: Proof.context -> thm list
traytel@67224
    21
traytel@67224
    22
  val prove_goal: settings -> Proof.context -> thm option -> term -> thm
traytel@67224
    23
  val prove_find_goal_cond: settings -> Proof.context -> thm list -> thm option -> term -> thm
traytel@67224
    24
traytel@67224
    25
  val mk_goal: Proof.context -> term -> term
traytel@67224
    26
  val mk_cond_goal: Proof.context -> thm -> term * thm
traytel@67224
    27
  val mk_param_goal_from_eq_def: Proof.context -> thm -> term
traytel@67224
    28
  val step_tac: settings -> Proof.context -> thm list -> int -> tactic
traytel@67224
    29
end
traytel@67224
    30
traytel@67224
    31
structure Conditional_Parametricity: CONDITIONAL_PARAMETRICITY =
traytel@67224
    32
struct
traytel@67224
    33
traytel@67224
    34
type settings =
traytel@67224
    35
  {suppress_print_theorem: bool,
traytel@67224
    36
  suppress_warnings: bool,
traytel@67224
    37
  warnings_as_errors: bool (* overrides suppress_warnings!  *),
traytel@67224
    38
  use_equality_heuristic: bool};
traytel@67224
    39
traytel@67224
    40
val quiet_settings =
traytel@67224
    41
  {suppress_print_theorem = true,
traytel@67224
    42
  suppress_warnings = true,
traytel@67224
    43
  warnings_as_errors = false,
traytel@67224
    44
  use_equality_heuristic = false};
traytel@67224
    45
traytel@67224
    46
val default_settings =
traytel@67224
    47
  {suppress_print_theorem = false,
traytel@67224
    48
  suppress_warnings = false,
traytel@67224
    49
  warnings_as_errors = false,
traytel@67224
    50
  use_equality_heuristic = false};
traytel@67224
    51
traytel@67224
    52
(* helper functions *)
traytel@67224
    53
traytel@67224
    54
fun strip_imp_prems_concl (Const("Pure.imp", _) $ A $ B) = A :: strip_imp_prems_concl B
traytel@67224
    55
  | strip_imp_prems_concl C = [C];
traytel@67224
    56
traytel@67224
    57
fun strip_prop_safe t = Logic.unprotect t handle TERM _ => t;
traytel@67224
    58
traytel@67224
    59
fun get_class_of ctxt t =
traytel@67224
    60
  Axclass.class_of_param (Proof_Context.theory_of ctxt) (fst (dest_Const t));
traytel@67224
    61
traytel@67224
    62
fun is_class_op ctxt t =
traytel@67224
    63
  let
traytel@67224
    64
    val t' = t |> Envir.eta_contract;
traytel@67224
    65
  in
traytel@67224
    66
    Term.is_Const t' andalso is_some (get_class_of ctxt t')
traytel@67224
    67
  end;
traytel@67224
    68
traytel@67224
    69
fun apply_Var_to_bounds t =
traytel@67224
    70
  let
traytel@67224
    71
    val (t, ts) = strip_comb t;
traytel@67224
    72
  in
traytel@67224
    73
    (case t of
traytel@67224
    74
      Var (xi, _) =>
traytel@67224
    75
        let
wenzelm@67522
    76
          val (bounds, tail) = chop_prefix is_Bound ts;
traytel@67224
    77
        in
traytel@67224
    78
          list_comb (Var (xi, fastype_of (betapplys (t, bounds))), map apply_Var_to_bounds tail)
traytel@67224
    79
        end
traytel@67224
    80
    | _ => list_comb (t, map apply_Var_to_bounds ts))
traytel@67224
    81
  end;
traytel@67224
    82
traytel@67224
    83
fun theorem_format_error ctxt thm =
traytel@67224
    84
  let
traytel@67224
    85
    val msg = Pretty.string_of (Pretty.chunks [(Pretty.para
traytel@67224
    86
      "Unexpected format of definition. Must be an unconditional equation."), Thm.pretty_thm ctxt thm]);
traytel@67224
    87
  in error msg end;
traytel@67224
    88
traytel@67224
    89
(* Tacticals and Tactics *)
traytel@67224
    90
traytel@67224
    91
exception FINISH of thm;
traytel@67224
    92
traytel@67224
    93
(* Tacticals *)
traytel@67224
    94
fun REPEAT_TRY_ELSE_DEFER tac st =
traytel@67224
    95
  let
traytel@67224
    96
    fun COMB' tac count st = (
traytel@67224
    97
      let
traytel@67224
    98
        val n = Thm.nprems_of st;
traytel@67224
    99
      in
traytel@67224
   100
        (if n = 0 then all_tac st else
traytel@67224
   101
          (case Seq.pull ((tac THEN COMB' tac 0) st) of
traytel@67224
   102
            NONE =>
traytel@67224
   103
              if count+1 = n
traytel@67224
   104
              then raise FINISH st
traytel@67224
   105
              else (defer_tac 1 THEN (COMB' tac (count+1))) st
traytel@67224
   106
          | some => Seq.make (fn () => some)))
traytel@67224
   107
      end)
traytel@67224
   108
  in COMB' tac 0 st end;
traytel@67224
   109
traytel@67224
   110
(* Tactics  *)
traytel@67224
   111
(* helper tactics for printing *)
traytel@67224
   112
fun error_tac ctxt msg st =
traytel@67224
   113
  (error(msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st)));
traytel@67224
   114
  Seq.single st);
traytel@67224
   115
traytel@67224
   116
fun error_tac' ctxt msg = SELECT_GOAL (error_tac ctxt msg);
traytel@67224
   117
traytel@67224
   118
(*  finds assumption of the form "Rel ?B Bound x Bound y", rotates it in front,
traytel@67224
   119
    applies rel_app arity times and uses ams_rl *)
traytel@67224
   120
fun rel_app_tac ctxt t x y arity =
traytel@67224
   121
  let
traytel@67224
   122
    val rel_app = [@{thm Rel_app}];
traytel@67224
   123
    val assume = [asm_rl];
traytel@67224
   124
    fun find_and_rotate_tac t i =
traytel@67224
   125
      let
traytel@67224
   126
        fun is_correct_rule t =
traytel@67224
   127
          (case t of
traytel@67224
   128
            Const (@{const_name "HOL.Trueprop"}, _) $ (Const (@{const_name "Transfer.Rel"}, _) $
traytel@67224
   129
              _ $ Bound x' $ Bound y') => x = x' andalso y = y'
traytel@67224
   130
          | _ => false);
traytel@67224
   131
        val idx = find_index is_correct_rule (t |> Logic.strip_assums_hyp);
traytel@67224
   132
      in
traytel@67224
   133
        if idx < 0 then no_tac else rotate_tac idx i
traytel@67224
   134
      end;
traytel@67224
   135
    fun rotate_and_dresolve_tac ctxt arity i = REPEAT_DETERM_N (arity - 1)
traytel@67224
   136
      (EVERY' [rotate_tac ~1, dresolve_tac ctxt rel_app, defer_tac] i);
traytel@67224
   137
  in
traytel@67224
   138
    SELECT_GOAL (EVERY' [find_and_rotate_tac t, forward_tac ctxt rel_app, defer_tac,
traytel@67224
   139
      rotate_and_dresolve_tac ctxt arity, rotate_tac ~1, eresolve_tac ctxt assume] 1)
traytel@67224
   140
  end;
traytel@67224
   141
traytel@67224
   142
exception WARNING of string;
traytel@67224
   143
traytel@67224
   144
fun transform_rules 0 thms = thms
traytel@67224
   145
  | transform_rules n thms = transform_rules (n - 1) (curry (Drule.RL o swap)
traytel@67224
   146
      @{thms Rel_app Rel_match_app} thms);
traytel@67224
   147
traytel@67224
   148
fun assume_equality_tac settings ctxt t arity i st =
traytel@67224
   149
  let
traytel@67224
   150
    val quiet = #suppress_warnings settings;
traytel@67224
   151
    val errors = #warnings_as_errors settings;
traytel@67224
   152
    val T = fastype_of t;
traytel@67224
   153
    val is_eq_lemma = @{thm is_equality_Rel} |> Thm.incr_indexes ((Term.maxidx_of_term t) + 1) |>
traytel@67224
   154
      Drule.infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt t)];
traytel@67224
   155
    val msg = Pretty.string_of (Pretty.chunks [Pretty.paragraph ((Pretty.text
traytel@67224
   156
      "No rule found for constant \"") @ [Syntax.pretty_term ctxt t, Pretty.str " :: " ,
traytel@67224
   157
      Syntax.pretty_typ ctxt T] @ (Pretty.text "\". Using is_eq_lemma:")), Pretty.quote
traytel@67224
   158
      (Thm.pretty_thm ctxt is_eq_lemma)]);
traytel@67224
   159
    fun msg_tac st = (if errors then raise WARNING msg else if quiet then () else warning msg;
traytel@67224
   160
      Seq.single st)
traytel@67224
   161
    val tac = resolve_tac ctxt (transform_rules arity [is_eq_lemma]) i;
traytel@67224
   162
  in
traytel@67224
   163
    (if fold_atyps (K (K true)) T false then msg_tac THEN tac else tac) st
traytel@67224
   164
  end;
traytel@67224
   165
traytel@67224
   166
fun mark_class_as_match_tac ctxt const const' arity =
traytel@67224
   167
  let
traytel@67224
   168
    val rules = transform_rules arity [@{thm Rel_match_Rel} |> Thm.incr_indexes ((Int.max o
traytel@67224
   169
      apply2 Term.maxidx_of_term) (const, const') + 1) |> Drule.infer_instantiate' ctxt [NONE,
traytel@67224
   170
      SOME (Thm.cterm_of ctxt const), SOME (Thm.cterm_of ctxt const')]];
traytel@67224
   171
  in resolve_tac ctxt rules end;
traytel@67224
   172
traytel@67224
   173
(* transforms the parametricity theorems to fit a given arity and uses them for resolution *)
traytel@67224
   174
fun parametricity_thm_tac settings ctxt parametricity_thms const arity =
traytel@67224
   175
  let
traytel@67224
   176
    val rules = transform_rules arity parametricity_thms;
traytel@67224
   177
  in resolve_tac ctxt rules ORELSE' assume_equality_tac settings ctxt const arity end;
traytel@67224
   178
traytel@67224
   179
(* variant of parametricity_thm_tac to use matching *)
traytel@67224
   180
fun parametricity_thm_match_tac ctxt parametricity_thms arity =
traytel@67224
   181
   let
traytel@67224
   182
    val rules = transform_rules arity parametricity_thms;
traytel@67224
   183
  in match_tac ctxt rules end;
traytel@67224
   184
traytel@67224
   185
fun rel_abs_tac ctxt = resolve_tac ctxt [@{thm Rel_abs}];
traytel@67224
   186
traytel@67224
   187
fun step_tac' settings ctxt parametricity_thms (tm, i) =
traytel@67224
   188
  (case tm |> Logic.strip_assums_concl of
traytel@67224
   189
    Const (@{const_name "HOL.Trueprop"}, _) $ (Const (rel, _) $ _ $ t $ u) =>
traytel@67224
   190
    let
traytel@67224
   191
      val (arity_of_t, arity_of_u) = apply2 (strip_comb #> snd #> length) (t, u);
traytel@67224
   192
    in
traytel@67224
   193
      (case rel of
traytel@67224
   194
        @{const_name "Transfer.Rel"} =>
traytel@67224
   195
          (case (head_of t, head_of u) of
traytel@67224
   196
            (Abs _, _) => rel_abs_tac ctxt
traytel@67224
   197
          | (_, Abs _) => rel_abs_tac ctxt
traytel@67224
   198
          | (const as (Const _), const' as (Const _)) =>
traytel@67224
   199
            if #use_equality_heuristic settings andalso t aconv u
traytel@67224
   200
              then
traytel@67224
   201
                assume_equality_tac quiet_settings ctxt t 0
traytel@67224
   202
              else if arity_of_t = arity_of_u
traytel@67224
   203
                then if is_class_op ctxt const orelse is_class_op ctxt const'
traytel@67224
   204
                  then mark_class_as_match_tac ctxt const const' arity_of_t
traytel@67224
   205
                  else parametricity_thm_tac settings ctxt parametricity_thms const arity_of_t
traytel@67224
   206
                else error_tac' ctxt "Malformed term. Arities of t and u don't match."
traytel@67224
   207
          | (Bound x, Bound y) =>
traytel@67224
   208
            if arity_of_t = arity_of_u then if arity_of_t > 0 then rel_app_tac ctxt tm x y arity_of_t
traytel@67224
   209
               else assume_tac ctxt
traytel@67224
   210
            else  error_tac' ctxt "Malformed term. Arities of t and u don't match."
traytel@67224
   211
          | _ => error_tac' ctxt
traytel@67224
   212
            "Unexpected format. Expected  (Abs _, _), (_, Abs _), (Const _, Const _) or (Bound _, Bound _).")
traytel@67224
   213
         | @{const_name "Conditional_Parametricity.Rel_match"} =>
traytel@67224
   214
             parametricity_thm_match_tac ctxt parametricity_thms arity_of_t
traytel@67224
   215
      | _ => error_tac' ctxt "Unexpected format. Expected Transfer.Rel or Rel_match marker." ) i
traytel@67224
   216
    end
traytel@67224
   217
    | Const (@{const_name "HOL.Trueprop"}, _) $ (Const (@{const_name "Transfer.is_equality"}, _) $ _) =>
traytel@67224
   218
        Transfer.eq_tac ctxt i
traytel@67224
   219
    | _ => error_tac' ctxt "Unexpected format. Not of form Const (HOL.Trueprop, _) $ _" i);
traytel@67224
   220
traytel@67224
   221
fun step_tac settings = SUBGOAL oo step_tac' settings;
traytel@67224
   222
traytel@67224
   223
fun apply_theorem_tac ctxt thm =
traytel@67224
   224
  HEADGOAL (resolve_tac ctxt [Local_Defs.unfold ctxt @{thms Pure.prop_def} thm] THEN_ALL_NEW
traytel@67224
   225
    assume_tac ctxt);
traytel@67224
   226
traytel@67224
   227
(* Goal Generation  *)
traytel@67224
   228
fun strip_boundvars_from_rel_match t =
traytel@67224
   229
  (case t of
traytel@67224
   230
    (Tp as Const (@{const_name "HOL.Trueprop"}, _)) $
traytel@67224
   231
      ((Rm as Const (@{const_name "Conditional_Parametricity.Rel_match"}, _)) $ R $ t $ t') =>
traytel@67224
   232
        Tp $ (Rm $ apply_Var_to_bounds R $ t $ t')
traytel@67224
   233
  | _ => t);
traytel@67224
   234
traytel@67224
   235
val extract_conditions =
traytel@67224
   236
  let
traytel@67224
   237
    val filter_bounds = filter_out Term.is_open;
traytel@67224
   238
    val prem_to_conditions =
traytel@67224
   239
      map (map strip_boundvars_from_rel_match o strip_imp_prems_concl o strip_all_body);
traytel@67224
   240
    val remove_duplicates = distinct Term.aconv;
traytel@67224
   241
  in remove_duplicates o filter_bounds o flat o prem_to_conditions end;
traytel@67224
   242
traytel@67224
   243
fun mk_goal ctxt t =
traytel@67224
   244
  let
traytel@67224
   245
    val ctxt = fold (Variable.declare_typ o snd) (Term.add_frees t []) ctxt;
traytel@67224
   246
    val t = singleton (Variable.polymorphic ctxt) t;
traytel@67224
   247
    val i = maxidx_of_term t + 1;
traytel@67224
   248
    fun tvar_to_tfree ((name, _), sort) = (name, sort);
traytel@67224
   249
    val tvars = Term.add_tvars t [];
traytel@67224
   250
    val new_frees = map TFree (Term.variant_frees t (map tvar_to_tfree tvars));
traytel@67224
   251
    val u = subst_atomic_types ((map TVar tvars) ~~ new_frees) t;
traytel@67224
   252
    val T = fastype_of t;
traytel@67224
   253
    val U = fastype_of u;
traytel@67224
   254
    val R = [T,U] ---> @{typ bool}
traytel@67224
   255
    val r = Var (("R", 2 * i), R);
traytel@67224
   256
    val transfer_rel = Const (@{const_name "Transfer.Rel"}, [R,T,U] ---> @{typ bool});
traytel@67224
   257
  in HOLogic.mk_Trueprop (transfer_rel $ r $ t $ u) end;
traytel@67224
   258
traytel@67224
   259
fun mk_abs_helper T t =
traytel@67224
   260
  let
traytel@67224
   261
    val U = fastype_of t;
traytel@67224
   262
    fun mk_abs_helper' T U =
traytel@67224
   263
      if T = U then t else
traytel@67224
   264
        let
traytel@67224
   265
          val (T2, T1) = Term.dest_funT T;
traytel@67224
   266
        in
traytel@67224
   267
          Term.absdummy T2 (mk_abs_helper' T1 U)
traytel@67224
   268
        end;
traytel@67224
   269
  in mk_abs_helper' T U end;
traytel@67224
   270
traytel@67224
   271
fun compare_ixs ((name, i):indexname, (name', i'):indexname) = if name < name' then LESS
traytel@67224
   272
  else if name > name' then GREATER
traytel@67224
   273
  else if i < i' then LESS
traytel@67224
   274
  else if i > i' then GREATER
traytel@67224
   275
  else EQUAL;
traytel@67224
   276
traytel@67224
   277
fun mk_cond_goal ctxt thm =
traytel@67224
   278
  let
traytel@67224
   279
    val conclusion = (hd o strip_imp_prems_concl o strip_prop_safe o Thm.concl_of) thm;
traytel@67224
   280
    val conditions = (extract_conditions o Thm.prems_of) thm;
traytel@67224
   281
    val goal = Logic.list_implies (conditions, conclusion);
traytel@67224
   282
    fun compare ((ix, _), (ix', _)) = compare_ixs (ix, ix');
traytel@67224
   283
    val goal_vars = Term.add_vars goal [] |> Ord_List.make compare;
traytel@67224
   284
    val (ixs, Ts) = split_list goal_vars;
traytel@67224
   285
    val (_, Ts') = Term.add_vars (Thm.prop_of thm) [] |> Ord_List.make compare
traytel@67224
   286
      |> Ord_List.inter compare goal_vars |> split_list;
traytel@67224
   287
    val (As, _) = Ctr_Sugar_Util.mk_Frees "A" Ts ctxt;
traytel@67224
   288
    val goal_subst = ixs ~~ As;
traytel@67224
   289
    val thm_subst = ixs ~~ (map2 mk_abs_helper Ts' As);
traytel@67224
   290
    val thm' = thm |> Drule.infer_instantiate ctxt (map (apsnd (Thm.cterm_of ctxt)) thm_subst);
traytel@67224
   291
  in (goal |> Term.subst_Vars goal_subst, thm') end;
traytel@67224
   292
traytel@67224
   293
fun mk_param_goal_from_eq_def ctxt thm =
traytel@67224
   294
  let
traytel@67224
   295
    val t =
traytel@67224
   296
      (case Thm.full_prop_of thm of
traytel@67224
   297
        (Const (@{const_name "Pure.eq"}, _) $ t' $ _) => t'
traytel@67224
   298
      | _ => theorem_format_error ctxt thm);
traytel@67224
   299
  in mk_goal ctxt t end;
traytel@67224
   300
traytel@67224
   301
(* Transformations and parametricity theorems *)
traytel@67224
   302
fun transform_class_rule ctxt thm =
traytel@67224
   303
  (case Thm.concl_of thm of
traytel@67224
   304
    Const (@{const_name "HOL.Trueprop"}, _) $ (Const (@{const_name "Transfer.Rel"}, _) $ _ $ t $ u ) =>
traytel@67224
   305
      (if curry Term.aconv_untyped t u andalso is_class_op ctxt t then
traytel@67224
   306
        thm RS @{thm Rel_Rel_match}
traytel@67224
   307
      else thm)
traytel@67224
   308
  | _ => thm);
traytel@67224
   309
traytel@67224
   310
fun is_parametricity_theorem thm =
traytel@67224
   311
  (case Thm.concl_of thm of
traytel@67224
   312
    Const (@{const_name "HOL.Trueprop"}, _) $ (Const (rel, _) $ _ $ t $ u ) =>
traytel@67224
   313
      if rel = @{const_name "Transfer.Rel"} orelse
traytel@67224
   314
        rel = @{const_name "Conditional_Parametricity.Rel_match"}
traytel@67224
   315
      then curry Term.aconv_untyped t u
traytel@67224
   316
      else false
traytel@67224
   317
  | _ => false);
traytel@67224
   318
traytel@67224
   319
(* Pre- and postprocessing of theorems *)
traytel@67224
   320
fun mk_Domainp_assm (T, R) =
traytel@67224
   321
  HOLogic.mk_eq ((Const (@{const_name Domainp}, Term.fastype_of T --> Term.fastype_of R) $ T), R);
traytel@67224
   322
traytel@67224
   323
val Domainp_lemma =
traytel@67224
   324
  @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"
traytel@67224
   325
    by (rule, drule meta_spec,
traytel@67224
   326
      erule meta_mp, rule HOL.refl, simp)};
traytel@67224
   327
traytel@67224
   328
fun fold_Domainp f (t as Const (@{const_name Domainp},_) $ (Var (_,_))) = f t
traytel@67224
   329
  | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u
traytel@67224
   330
  | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t
traytel@67224
   331
  | fold_Domainp _ _ = I;
traytel@67224
   332
traytel@67224
   333
fun subst_terms tab t =
traytel@67224
   334
  let
traytel@67224
   335
    val t' = Termtab.lookup tab t
traytel@67224
   336
  in
traytel@67224
   337
    (case t' of
traytel@67224
   338
      SOME t' => t'
traytel@67224
   339
    | NONE =>
traytel@67224
   340
      (case t of
traytel@67224
   341
          u $ v => (subst_terms tab u) $ (subst_terms tab v)
traytel@67224
   342
        | Abs (a, T, t) => Abs (a, T, subst_terms tab t)
traytel@67224
   343
        | t => t))
traytel@67224
   344
  end;
traytel@67224
   345
traytel@67224
   346
fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
traytel@67224
   347
  let
traytel@67224
   348
    val prop = Thm.prop_of thm
traytel@67224
   349
    val (t, mk_prop') = dest prop
traytel@67224
   350
    val Domainp_ts = rev (fold_Domainp (fn t => insert op= t) t [])
traytel@67224
   351
    val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_ts
traytel@67224
   352
    val used = Term.add_free_names t []
traytel@67224
   353
    val rels = map (snd o dest_comb) Domainp_ts
traytel@67224
   354
    val rel_names = map (fst o fst o dest_Var) rels
traytel@67224
   355
    val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used
traytel@67224
   356
    val frees = map Free (names ~~ Domainp_Ts)
traytel@67224
   357
    val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees);
traytel@67224
   358
    val t' = subst_terms (fold Termtab.update (Domainp_ts ~~ frees) Termtab.empty) t
traytel@67224
   359
    val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
traytel@67224
   360
    val prop2 = Logic.list_rename_params (rev names) prop1
traytel@67224
   361
    val cprop = Thm.cterm_of ctxt prop2
traytel@67224
   362
    val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
traytel@67224
   363
    fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
traytel@67224
   364
  in
traytel@67224
   365
    forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
traytel@67224
   366
  end
traytel@67224
   367
    handle TERM _ => thm;
traytel@67224
   368
traytel@67224
   369
fun abstract_domains_transfer ctxt thm =
traytel@67224
   370
  let
traytel@67224
   371
    fun dest prop =
traytel@67224
   372
      let
traytel@67224
   373
        val prems = Logic.strip_imp_prems prop
traytel@67224
   374
        val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
traytel@67224
   375
        val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
traytel@67224
   376
      in
traytel@67224
   377
        (x, fn x' =>
traytel@67224
   378
          Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
traytel@67224
   379
      end
traytel@67224
   380
  in
traytel@67224
   381
    gen_abstract_domains ctxt dest thm
traytel@67224
   382
  end;
traytel@67224
   383
traytel@67224
   384
fun transfer_rel_conv conv =
traytel@67224
   385
  Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv)));
traytel@67224
   386
traytel@67224
   387
fun fold_relator_eqs_conv ctxt ct = (Transfer.bottom_rewr_conv (Transfer.get_relator_eq ctxt)) ct;
traytel@67224
   388
traytel@67224
   389
fun mk_is_equality t =
traytel@67224
   390
  Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t;
traytel@67224
   391
traytel@67224
   392
val is_equality_lemma =
nipkow@67399
   393
  @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (=))"
traytel@67224
   394
    by (unfold is_equality_def, rule, drule meta_spec,
traytel@67224
   395
      erule meta_mp, rule HOL.refl, simp)};
traytel@67224
   396
traytel@67224
   397
fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
traytel@67224
   398
  let
traytel@67224
   399
    val prop = Thm.prop_of thm
traytel@67224
   400
    val (t, mk_prop') = dest prop
nipkow@67399
   401
    (* Only consider "(=)" at non-base types *)
traytel@67224
   402
    fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) =
traytel@67224
   403
        (case T of Type (_, []) => false | _ => true)
traytel@67224
   404
      | is_eq _ = false
traytel@67224
   405
    val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
traytel@67224
   406
    val eq_consts = rev (add_eqs t [])
traytel@67224
   407
    val eqTs = map (snd o dest_Const) eq_consts
traytel@67224
   408
    val used = Term.add_free_names prop []
traytel@67224
   409
    val names = map (K "") eqTs |> Name.variant_list used
traytel@67224
   410
    val frees = map Free (names ~~ eqTs)
traytel@67224
   411
    val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
traytel@67224
   412
    val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
traytel@67224
   413
    val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
traytel@67224
   414
    val cprop = Thm.cterm_of ctxt prop2
traytel@67224
   415
    val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
traytel@67224
   416
    fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
traytel@67224
   417
  in
traytel@67224
   418
    forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
traytel@67224
   419
  end
traytel@67224
   420
    handle TERM _ => thm;
traytel@67224
   421
traytel@67224
   422
fun abstract_equalities_transfer ctxt thm =
traytel@67224
   423
  let
traytel@67224
   424
    fun dest prop =
traytel@67224
   425
      let
traytel@67224
   426
        val prems = Logic.strip_imp_prems prop
traytel@67224
   427
        val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
traytel@67224
   428
        val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
traytel@67224
   429
      in
traytel@67224
   430
        (rel, fn rel' =>
traytel@67224
   431
          Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
traytel@67224
   432
      end
traytel@67224
   433
    val contracted_eq_thm =
traytel@67224
   434
      Conv.fconv_rule (transfer_rel_conv (fold_relator_eqs_conv ctxt)) thm
traytel@67224
   435
      handle CTERM _ => thm
traytel@67224
   436
  in
traytel@67224
   437
    gen_abstract_equalities ctxt dest contracted_eq_thm
traytel@67224
   438
  end;
traytel@67224
   439
traytel@67224
   440
fun prep_rule ctxt = abstract_equalities_transfer ctxt #> abstract_domains_transfer ctxt;
traytel@67224
   441
traytel@67224
   442
fun get_preprocess_theorems ctxt =
traytel@67224
   443
  Named_Theorems.get ctxt @{named_theorems parametricity_preprocess};
traytel@67224
   444
traytel@67224
   445
fun preprocess_theorem ctxt =
traytel@67224
   446
  Local_Defs.unfold0 ctxt (get_preprocess_theorems ctxt)
traytel@67224
   447
  #> transform_class_rule ctxt;
traytel@67224
   448
traytel@67224
   449
fun postprocess_theorem ctxt =
traytel@67224
   450
  Local_Defs.fold ctxt (@{thm Rel_Rel_match_eq} :: get_preprocess_theorems ctxt)
traytel@67224
   451
  #> prep_rule ctxt
traytel@67224
   452
  #>  Local_Defs.unfold ctxt @{thms Rel_def};
traytel@67224
   453
traytel@67224
   454
fun get_parametricity_theorems ctxt =
traytel@67224
   455
  let
traytel@67224
   456
    val parametricity_thm_map_filter =
traytel@67224
   457
      Option.filter (is_parametricity_theorem andf (not o curry Term.could_unify
traytel@67224
   458
        (Thm.full_prop_of @{thm is_equality_Rel})) o Thm.full_prop_of) o preprocess_theorem ctxt;
traytel@67224
   459
  in
wenzelm@67649
   460
    map_filter (parametricity_thm_map_filter o Thm.transfer' ctxt)
traytel@67224
   461
      (Transfer.get_transfer_raw ctxt)
traytel@67224
   462
  end;
traytel@67224
   463
traytel@67224
   464
(* Provers *)
traytel@67224
   465
(* Tries to prove a parametricity theorem without conditions, returns the last goal_state as thm *)
traytel@67224
   466
fun prove_find_goal_cond settings ctxt rules def_thm t =
traytel@67224
   467
  let
traytel@67224
   468
    fun find_conditions_tac {context = ctxt, prems = _} = unfold_tac ctxt (the_list def_thm) THEN
traytel@67224
   469
      (REPEAT_TRY_ELSE_DEFER o HEADGOAL) (step_tac settings ctxt rules);
traytel@67224
   470
  in
traytel@67224
   471
    Goal.prove ctxt [] [] t find_conditions_tac handle FINISH st => st
traytel@67224
   472
  end;
traytel@67224
   473
traytel@67224
   474
(* Simplifies and proves thm *)
traytel@67224
   475
fun prove_cond_goal ctxt thm =
traytel@67224
   476
  let
traytel@67224
   477
    val (goal, thm') = mk_cond_goal ctxt thm;
traytel@67224
   478
    val vars = Variable.add_free_names ctxt goal [];
traytel@67224
   479
    fun prove_conditions_tac {context = ctxt, prems = _} = apply_theorem_tac ctxt thm';
traytel@67224
   480
    val vars = Variable.add_free_names ctxt (Thm.prop_of thm') vars;
traytel@67224
   481
  in
traytel@67224
   482
    Goal.prove ctxt vars [] goal prove_conditions_tac
traytel@67224
   483
  end;
traytel@67224
   484
traytel@67224
   485
(* Finds necessary conditions for t and proofs conditional parametricity of t under those conditions *)
traytel@67224
   486
fun prove_goal settings ctxt def_thm t =
traytel@67224
   487
  let
traytel@67224
   488
    val parametricity_thms = get_parametricity_theorems ctxt;
traytel@67224
   489
    val found_thm = prove_find_goal_cond settings ctxt parametricity_thms def_thm t;
traytel@67224
   490
    val thm = prove_cond_goal ctxt found_thm;
traytel@67224
   491
  in
traytel@67224
   492
    postprocess_theorem ctxt thm
traytel@67224
   493
  end;
traytel@67224
   494
traytel@67224
   495
(* Commands  *)
traytel@67224
   496
fun gen_parametric_constant settings prep_att prep_thm (raw_b : Attrib.binding, raw_eq) lthy =
traytel@67224
   497
  let
traytel@67224
   498
    val b = apsnd (map (prep_att lthy)) raw_b;
traytel@67224
   499
    val def_thm = (prep_thm lthy raw_eq);
traytel@67224
   500
    val eq = Ctr_Sugar_Util.mk_abs_def def_thm handle TERM _ => theorem_format_error lthy def_thm;
traytel@67224
   501
    val goal= mk_param_goal_from_eq_def lthy eq;
traytel@67224
   502
    val thm = prove_goal settings lthy (SOME eq) goal;
traytel@67224
   503
    val (res, lthy') = Local_Theory.note (b, [thm]) lthy;
traytel@67224
   504
    val _ = if #suppress_print_theorem settings then () else
traytel@67224
   505
      Proof_Display.print_results true (Position.thread_data ()) lthy' (("theorem",""), [res]);
traytel@67224
   506
  in
traytel@67224
   507
    (the_single (snd res), lthy')
traytel@67224
   508
  end;
traytel@67224
   509
traytel@67224
   510
fun parametric_constant settings = gen_parametric_constant settings (K I) (K I);
traytel@67224
   511
traytel@67224
   512
val parametric_constant_cmd = snd oo gen_parametric_constant default_settings (Attrib.check_src)
traytel@67224
   513
  (singleton o Attrib.eval_thms);
traytel@67224
   514
traytel@67224
   515
val _ =
traytel@67224
   516
  Outer_Syntax.local_theory @{command_keyword parametric_constant} "proves parametricity"
traytel@67224
   517
    ((Parse_Spec.opt_thm_name ":" -- Parse.thm) >> parametric_constant_cmd);
traytel@67224
   518
nipkow@67399
   519
end;