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