a conditional paramitrecity prover
authortraytel
Mon Dec 18 16:58:13 2017 +0100 (17 months ago)
changeset 67224341fbce5b26d
parent 67223 711eec20aecd
child 67225 cb34f5f49a08
a conditional paramitrecity prover
CONTRIBUTORS
NEWS
src/HOL/Library/Conditional_Parametricity.thy
src/HOL/Library/Library.thy
src/HOL/Library/conditional_parametricity.ML
src/HOL/ROOT
src/HOL/ex/Conditional_Parametricity_Examples.thy
     1.1 --- a/CONTRIBUTORS	Mon Dec 18 11:56:12 2017 +0100
     1.2 +++ b/CONTRIBUTORS	Mon Dec 18 16:58:13 2017 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4  Contributions to this Isabelle version
     1.5  --------------------------------------
     1.6  
     1.7 +* December 2017: Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel
     1.8 +  A new conditional paramertricity prover.
     1.9 +
    1.10  * October 2017: Alexander Maletzky
    1.11    Derivation of axiom "iff" in HOL.thy from the other axioms.
    1.12  
     2.1 --- a/NEWS	Mon Dec 18 11:56:12 2017 +0100
     2.2 +++ b/NEWS	Mon Dec 18 16:58:13 2017 +0100
     2.3 @@ -99,6 +99,12 @@
     2.4  
     2.5  *** HOL ***
     2.6  
     2.7 +* A new command parametric_constant for proving parametricity of
     2.8 +  non-recursive definitions. For constants that are not fully parametric the
     2.9 +  command will infer conditions on relations (e.g., bi_unique, bi_total, or
    2.10 +  type class conditions such as "respects 0") sufficient for parametricity.
    2.11 +  See ~~/src/HOL/ex/Conditional_Parametricity_Examples for some examples.
    2.12 +
    2.13  * SMT module:
    2.14    - The 'smt_oracle' option is now necessary when using the 'smt' method
    2.15      with a solver other than Z3. INCOMPATIBILITY.
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/Conditional_Parametricity.thy	Mon Dec 18 16:58:13 2017 +0100
     3.3 @@ -0,0 +1,48 @@
     3.4 +(*  Title:    HOL/Library/Conditional_Parametricity.thy
     3.5 +    Author:   Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel, ETH Zürich
     3.6 +
     3.7 +A conditional parametricity prover
     3.8 +*)
     3.9 +
    3.10 +theory Conditional_Parametricity
    3.11 +imports Main
    3.12 +keywords "parametric_constant" :: thy_decl
    3.13 +begin
    3.14 +
    3.15 +context includes lifting_syntax begin
    3.16 +
    3.17 +qualified definition Rel_match :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
    3.18 +  "Rel_match R x y = R x y"
    3.19 +
    3.20 +named_theorems parametricity_preprocess
    3.21 +
    3.22 +lemma bi_unique_Rel_match [parametricity_preprocess]:
    3.23 +  "bi_unique A = Rel_match (A ===> A ===> op =) op = op ="
    3.24 +  unfolding bi_unique_alt_def2 Rel_match_def ..
    3.25 +
    3.26 +lemma bi_total_Rel_match [parametricity_preprocess]:
    3.27 +  "bi_total A = Rel_match ((A ===> op =) ===> op =) All All"
    3.28 +  unfolding bi_total_alt_def2 Rel_match_def ..
    3.29 +
    3.30 +lemma is_equality_Rel: "is_equality A \<Longrightarrow> Transfer.Rel A t t"
    3.31 +  by (fact transfer_raw)
    3.32 +
    3.33 +lemma Rel_Rel_match: "Transfer.Rel R x y \<Longrightarrow> Rel_match R x y"
    3.34 +  unfolding Rel_match_def Rel_def .
    3.35 +
    3.36 +lemma Rel_match_Rel: "Rel_match R x y \<Longrightarrow> Transfer.Rel R x y"
    3.37 +  unfolding Rel_match_def Rel_def .
    3.38 +
    3.39 +lemma Rel_Rel_match_eq: "Transfer.Rel R x y = Rel_match R x y"
    3.40 +  using Rel_Rel_match Rel_match_Rel by fast
    3.41 +
    3.42 +lemma Rel_match_app:
    3.43 +  assumes "Rel_match (A ===> B) f g" and "Transfer.Rel A x y"
    3.44 +  shows "Rel_match B (f x) (g y)"
    3.45 +  using assms Rel_match_Rel Rel_app Rel_Rel_match by fast
    3.46 +
    3.47 +end
    3.48 +
    3.49 +ML_file "conditional_parametricity.ML"
    3.50 +
    3.51 +end
    3.52 \ No newline at end of file
     4.1 --- a/src/HOL/Library/Library.thy	Mon Dec 18 11:56:12 2017 +0100
     4.2 +++ b/src/HOL/Library/Library.thy	Mon Dec 18 16:58:13 2017 +0100
     4.3 @@ -12,6 +12,7 @@
     4.4    Code_Test
     4.5    Combine_PER
     4.6    Complete_Partial_Order2
     4.7 +  Conditional_Parametricity
     4.8    Countable
     4.9    Countable_Complete_Lattices
    4.10    Countable_Set_Type
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/conditional_parametricity.ML	Mon Dec 18 16:58:13 2017 +0100
     5.3 @@ -0,0 +1,519 @@
     5.4 +(*  Title:    HOL/Library/conditional_parametricity.ML
     5.5 +    Author:   Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel, ETH Zürich
     5.6 +
     5.7 +A conditional parametricity prover
     5.8 +*)
     5.9 +
    5.10 +signature CONDITIONAL_PARAMETRICITY =
    5.11 +sig
    5.12 +  exception WARNING of string
    5.13 +  type settings =
    5.14 +    {suppress_print_theorem: bool,
    5.15 +    suppress_warnings: bool,
    5.16 +    warnings_as_errors: bool,
    5.17 +    use_equality_heuristic: bool}
    5.18 +  val default_settings: settings
    5.19 +  val quiet_settings: settings
    5.20 +
    5.21 +  val parametric_constant: settings -> Attrib.binding * thm -> Proof.context ->
    5.22 +    (thm * Proof.context)
    5.23 +  val get_parametricity_theorems: Proof.context -> thm list
    5.24 +
    5.25 +  val prove_goal: settings -> Proof.context -> thm option -> term -> thm
    5.26 +  val prove_find_goal_cond: settings -> Proof.context -> thm list -> thm option -> term -> thm
    5.27 +
    5.28 +  val mk_goal: Proof.context -> term -> term
    5.29 +  val mk_cond_goal: Proof.context -> thm -> term * thm
    5.30 +  val mk_param_goal_from_eq_def: Proof.context -> thm -> term
    5.31 +  val step_tac: settings -> Proof.context -> thm list -> int -> tactic
    5.32 +end
    5.33 +
    5.34 +structure Conditional_Parametricity: CONDITIONAL_PARAMETRICITY =
    5.35 +struct
    5.36 +
    5.37 +type settings =
    5.38 +  {suppress_print_theorem: bool,
    5.39 +  suppress_warnings: bool,
    5.40 +  warnings_as_errors: bool (* overrides suppress_warnings!  *),
    5.41 +  use_equality_heuristic: bool};
    5.42 +
    5.43 +val quiet_settings =
    5.44 +  {suppress_print_theorem = true,
    5.45 +  suppress_warnings = true,
    5.46 +  warnings_as_errors = false,
    5.47 +  use_equality_heuristic = false};
    5.48 +
    5.49 +val default_settings =
    5.50 +  {suppress_print_theorem = false,
    5.51 +  suppress_warnings = false,
    5.52 +  warnings_as_errors = false,
    5.53 +  use_equality_heuristic = false};
    5.54 +
    5.55 +(* helper functions *)
    5.56 +
    5.57 +fun strip_imp_prems_concl (Const("Pure.imp", _) $ A $ B) = A :: strip_imp_prems_concl B
    5.58 +  | strip_imp_prems_concl C = [C];
    5.59 +
    5.60 +fun strip_prop_safe t = Logic.unprotect t handle TERM _ => t;
    5.61 +
    5.62 +fun get_class_of ctxt t =
    5.63 +  Axclass.class_of_param (Proof_Context.theory_of ctxt) (fst (dest_Const t));
    5.64 +
    5.65 +fun is_class_op ctxt t =
    5.66 +  let
    5.67 +    val t' = t |> Envir.eta_contract;
    5.68 +  in
    5.69 +    Term.is_Const t' andalso is_some (get_class_of ctxt t')
    5.70 +  end;
    5.71 +
    5.72 +fun apply_Var_to_bounds t =
    5.73 +  let
    5.74 +    val (t, ts) = strip_comb t;
    5.75 +  in
    5.76 +    (case t of
    5.77 +      Var (xi, _) =>
    5.78 +        let
    5.79 +          val (bounds, tail) = take_prefix is_Bound ts;
    5.80 +        in
    5.81 +          list_comb (Var (xi, fastype_of (betapplys (t, bounds))), map apply_Var_to_bounds tail)
    5.82 +        end
    5.83 +    | _ => list_comb (t, map apply_Var_to_bounds ts))
    5.84 +  end;
    5.85 +
    5.86 +fun theorem_format_error ctxt thm =
    5.87 +  let
    5.88 +    val msg = Pretty.string_of (Pretty.chunks [(Pretty.para
    5.89 +      "Unexpected format of definition. Must be an unconditional equation."), Thm.pretty_thm ctxt thm]);
    5.90 +  in error msg end;
    5.91 +
    5.92 +(* Tacticals and Tactics *)
    5.93 +
    5.94 +exception FINISH of thm;
    5.95 +
    5.96 +(* Tacticals *)
    5.97 +fun REPEAT_TRY_ELSE_DEFER tac st =
    5.98 +  let
    5.99 +    fun COMB' tac count st = (
   5.100 +      let
   5.101 +        val n = Thm.nprems_of st;
   5.102 +      in
   5.103 +        (if n = 0 then all_tac st else
   5.104 +          (case Seq.pull ((tac THEN COMB' tac 0) st) of
   5.105 +            NONE =>
   5.106 +              if count+1 = n
   5.107 +              then raise FINISH st
   5.108 +              else (defer_tac 1 THEN (COMB' tac (count+1))) st
   5.109 +          | some => Seq.make (fn () => some)))
   5.110 +      end)
   5.111 +  in COMB' tac 0 st end;
   5.112 +
   5.113 +(* Tactics  *)
   5.114 +(* helper tactics for printing *)
   5.115 +fun error_tac ctxt msg st =
   5.116 +  (error(msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st)));
   5.117 +  Seq.single st);
   5.118 +
   5.119 +fun error_tac' ctxt msg = SELECT_GOAL (error_tac ctxt msg);
   5.120 +
   5.121 +(*  finds assumption of the form "Rel ?B Bound x Bound y", rotates it in front,
   5.122 +    applies rel_app arity times and uses ams_rl *)
   5.123 +fun rel_app_tac ctxt t x y arity =
   5.124 +  let
   5.125 +    val rel_app = [@{thm Rel_app}];
   5.126 +    val assume = [asm_rl];
   5.127 +    fun find_and_rotate_tac t i =
   5.128 +      let
   5.129 +        fun is_correct_rule t =
   5.130 +          (case t of
   5.131 +            Const (@{const_name "HOL.Trueprop"}, _) $ (Const (@{const_name "Transfer.Rel"}, _) $
   5.132 +              _ $ Bound x' $ Bound y') => x = x' andalso y = y'
   5.133 +          | _ => false);
   5.134 +        val idx = find_index is_correct_rule (t |> Logic.strip_assums_hyp);
   5.135 +      in
   5.136 +        if idx < 0 then no_tac else rotate_tac idx i
   5.137 +      end;
   5.138 +    fun rotate_and_dresolve_tac ctxt arity i = REPEAT_DETERM_N (arity - 1)
   5.139 +      (EVERY' [rotate_tac ~1, dresolve_tac ctxt rel_app, defer_tac] i);
   5.140 +  in
   5.141 +    SELECT_GOAL (EVERY' [find_and_rotate_tac t, forward_tac ctxt rel_app, defer_tac,
   5.142 +      rotate_and_dresolve_tac ctxt arity, rotate_tac ~1, eresolve_tac ctxt assume] 1)
   5.143 +  end;
   5.144 +
   5.145 +exception WARNING of string;
   5.146 +
   5.147 +fun transform_rules 0 thms = thms
   5.148 +  | transform_rules n thms = transform_rules (n - 1) (curry (Drule.RL o swap)
   5.149 +      @{thms Rel_app Rel_match_app} thms);
   5.150 +
   5.151 +fun assume_equality_tac settings ctxt t arity i st =
   5.152 +  let
   5.153 +    val quiet = #suppress_warnings settings;
   5.154 +    val errors = #warnings_as_errors settings;
   5.155 +    val T = fastype_of t;
   5.156 +    val is_eq_lemma = @{thm is_equality_Rel} |> Thm.incr_indexes ((Term.maxidx_of_term t) + 1) |>
   5.157 +      Drule.infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt t)];
   5.158 +    val msg = Pretty.string_of (Pretty.chunks [Pretty.paragraph ((Pretty.text
   5.159 +      "No rule found for constant \"") @ [Syntax.pretty_term ctxt t, Pretty.str " :: " ,
   5.160 +      Syntax.pretty_typ ctxt T] @ (Pretty.text "\". Using is_eq_lemma:")), Pretty.quote
   5.161 +      (Thm.pretty_thm ctxt is_eq_lemma)]);
   5.162 +    fun msg_tac st = (if errors then raise WARNING msg else if quiet then () else warning msg;
   5.163 +      Seq.single st)
   5.164 +    val tac = resolve_tac ctxt (transform_rules arity [is_eq_lemma]) i;
   5.165 +  in
   5.166 +    (if fold_atyps (K (K true)) T false then msg_tac THEN tac else tac) st
   5.167 +  end;
   5.168 +
   5.169 +fun mark_class_as_match_tac ctxt const const' arity =
   5.170 +  let
   5.171 +    val rules = transform_rules arity [@{thm Rel_match_Rel} |> Thm.incr_indexes ((Int.max o
   5.172 +      apply2 Term.maxidx_of_term) (const, const') + 1) |> Drule.infer_instantiate' ctxt [NONE,
   5.173 +      SOME (Thm.cterm_of ctxt const), SOME (Thm.cterm_of ctxt const')]];
   5.174 +  in resolve_tac ctxt rules end;
   5.175 +
   5.176 +(* transforms the parametricity theorems to fit a given arity and uses them for resolution *)
   5.177 +fun parametricity_thm_tac settings ctxt parametricity_thms const arity =
   5.178 +  let
   5.179 +    val rules = transform_rules arity parametricity_thms;
   5.180 +  in resolve_tac ctxt rules ORELSE' assume_equality_tac settings ctxt const arity end;
   5.181 +
   5.182 +(* variant of parametricity_thm_tac to use matching *)
   5.183 +fun parametricity_thm_match_tac ctxt parametricity_thms arity =
   5.184 +   let
   5.185 +    val rules = transform_rules arity parametricity_thms;
   5.186 +  in match_tac ctxt rules end;
   5.187 +
   5.188 +fun rel_abs_tac ctxt = resolve_tac ctxt [@{thm Rel_abs}];
   5.189 +
   5.190 +fun step_tac' settings ctxt parametricity_thms (tm, i) =
   5.191 +  (case tm |> Logic.strip_assums_concl of
   5.192 +    Const (@{const_name "HOL.Trueprop"}, _) $ (Const (rel, _) $ _ $ t $ u) =>
   5.193 +    let
   5.194 +      val (arity_of_t, arity_of_u) = apply2 (strip_comb #> snd #> length) (t, u);
   5.195 +    in
   5.196 +      (case rel of
   5.197 +        @{const_name "Transfer.Rel"} =>
   5.198 +          (case (head_of t, head_of u) of
   5.199 +            (Abs _, _) => rel_abs_tac ctxt
   5.200 +          | (_, Abs _) => rel_abs_tac ctxt
   5.201 +          | (const as (Const _), const' as (Const _)) =>
   5.202 +            if #use_equality_heuristic settings andalso t aconv u
   5.203 +              then
   5.204 +                assume_equality_tac quiet_settings ctxt t 0
   5.205 +              else if arity_of_t = arity_of_u
   5.206 +                then if is_class_op ctxt const orelse is_class_op ctxt const'
   5.207 +                  then mark_class_as_match_tac ctxt const const' arity_of_t
   5.208 +                  else parametricity_thm_tac settings ctxt parametricity_thms const arity_of_t
   5.209 +                else error_tac' ctxt "Malformed term. Arities of t and u don't match."
   5.210 +          | (Bound x, Bound y) =>
   5.211 +            if arity_of_t = arity_of_u then if arity_of_t > 0 then rel_app_tac ctxt tm x y arity_of_t
   5.212 +               else assume_tac ctxt
   5.213 +            else  error_tac' ctxt "Malformed term. Arities of t and u don't match."
   5.214 +          | _ => error_tac' ctxt
   5.215 +            "Unexpected format. Expected  (Abs _, _), (_, Abs _), (Const _, Const _) or (Bound _, Bound _).")
   5.216 +         | @{const_name "Conditional_Parametricity.Rel_match"} =>
   5.217 +             parametricity_thm_match_tac ctxt parametricity_thms arity_of_t
   5.218 +      | _ => error_tac' ctxt "Unexpected format. Expected Transfer.Rel or Rel_match marker." ) i
   5.219 +    end
   5.220 +    | Const (@{const_name "HOL.Trueprop"}, _) $ (Const (@{const_name "Transfer.is_equality"}, _) $ _) =>
   5.221 +        Transfer.eq_tac ctxt i
   5.222 +    | _ => error_tac' ctxt "Unexpected format. Not of form Const (HOL.Trueprop, _) $ _" i);
   5.223 +
   5.224 +fun step_tac settings = SUBGOAL oo step_tac' settings;
   5.225 +
   5.226 +fun apply_theorem_tac ctxt thm =
   5.227 +  HEADGOAL (resolve_tac ctxt [Local_Defs.unfold ctxt @{thms Pure.prop_def} thm] THEN_ALL_NEW
   5.228 +    assume_tac ctxt);
   5.229 +
   5.230 +(* Goal Generation  *)
   5.231 +fun strip_boundvars_from_rel_match t =
   5.232 +  (case t of
   5.233 +    (Tp as Const (@{const_name "HOL.Trueprop"}, _)) $
   5.234 +      ((Rm as Const (@{const_name "Conditional_Parametricity.Rel_match"}, _)) $ R $ t $ t') =>
   5.235 +        Tp $ (Rm $ apply_Var_to_bounds R $ t $ t')
   5.236 +  | _ => t);
   5.237 +
   5.238 +val extract_conditions =
   5.239 +  let
   5.240 +    val filter_bounds = filter_out Term.is_open;
   5.241 +    val prem_to_conditions =
   5.242 +      map (map strip_boundvars_from_rel_match o strip_imp_prems_concl o strip_all_body);
   5.243 +    val remove_duplicates = distinct Term.aconv;
   5.244 +  in remove_duplicates o filter_bounds o flat o prem_to_conditions end;
   5.245 +
   5.246 +fun mk_goal ctxt t =
   5.247 +  let
   5.248 +    val ctxt = fold (Variable.declare_typ o snd) (Term.add_frees t []) ctxt;
   5.249 +    val t = singleton (Variable.polymorphic ctxt) t;
   5.250 +    val i = maxidx_of_term t + 1;
   5.251 +    fun tvar_to_tfree ((name, _), sort) = (name, sort);
   5.252 +    val tvars = Term.add_tvars t [];
   5.253 +    val new_frees = map TFree (Term.variant_frees t (map tvar_to_tfree tvars));
   5.254 +    val u = subst_atomic_types ((map TVar tvars) ~~ new_frees) t;
   5.255 +    val T = fastype_of t;
   5.256 +    val U = fastype_of u;
   5.257 +    val R = [T,U] ---> @{typ bool}
   5.258 +    val r = Var (("R", 2 * i), R);
   5.259 +    val transfer_rel = Const (@{const_name "Transfer.Rel"}, [R,T,U] ---> @{typ bool});
   5.260 +  in HOLogic.mk_Trueprop (transfer_rel $ r $ t $ u) end;
   5.261 +
   5.262 +fun mk_abs_helper T t =
   5.263 +  let
   5.264 +    val U = fastype_of t;
   5.265 +    fun mk_abs_helper' T U =
   5.266 +      if T = U then t else
   5.267 +        let
   5.268 +          val (T2, T1) = Term.dest_funT T;
   5.269 +        in
   5.270 +          Term.absdummy T2 (mk_abs_helper' T1 U)
   5.271 +        end;
   5.272 +  in mk_abs_helper' T U end;
   5.273 +
   5.274 +fun compare_ixs ((name, i):indexname, (name', i'):indexname) = if name < name' then LESS
   5.275 +  else if name > name' then GREATER
   5.276 +  else if i < i' then LESS
   5.277 +  else if i > i' then GREATER
   5.278 +  else EQUAL;
   5.279 +
   5.280 +fun mk_cond_goal ctxt thm =
   5.281 +  let
   5.282 +    val conclusion = (hd o strip_imp_prems_concl o strip_prop_safe o Thm.concl_of) thm;
   5.283 +    val conditions = (extract_conditions o Thm.prems_of) thm;
   5.284 +    val goal = Logic.list_implies (conditions, conclusion);
   5.285 +    fun compare ((ix, _), (ix', _)) = compare_ixs (ix, ix');
   5.286 +    val goal_vars = Term.add_vars goal [] |> Ord_List.make compare;
   5.287 +    val (ixs, Ts) = split_list goal_vars;
   5.288 +    val (_, Ts') = Term.add_vars (Thm.prop_of thm) [] |> Ord_List.make compare
   5.289 +      |> Ord_List.inter compare goal_vars |> split_list;
   5.290 +    val (As, _) = Ctr_Sugar_Util.mk_Frees "A" Ts ctxt;
   5.291 +    val goal_subst = ixs ~~ As;
   5.292 +    val thm_subst = ixs ~~ (map2 mk_abs_helper Ts' As);
   5.293 +    val thm' = thm |> Drule.infer_instantiate ctxt (map (apsnd (Thm.cterm_of ctxt)) thm_subst);
   5.294 +  in (goal |> Term.subst_Vars goal_subst, thm') end;
   5.295 +
   5.296 +fun mk_param_goal_from_eq_def ctxt thm =
   5.297 +  let
   5.298 +    val t =
   5.299 +      (case Thm.full_prop_of thm of
   5.300 +        (Const (@{const_name "Pure.eq"}, _) $ t' $ _) => t'
   5.301 +      | _ => theorem_format_error ctxt thm);
   5.302 +  in mk_goal ctxt t end;
   5.303 +
   5.304 +(* Transformations and parametricity theorems *)
   5.305 +fun transform_class_rule ctxt thm =
   5.306 +  (case Thm.concl_of thm of
   5.307 +    Const (@{const_name "HOL.Trueprop"}, _) $ (Const (@{const_name "Transfer.Rel"}, _) $ _ $ t $ u ) =>
   5.308 +      (if curry Term.aconv_untyped t u andalso is_class_op ctxt t then
   5.309 +        thm RS @{thm Rel_Rel_match}
   5.310 +      else thm)
   5.311 +  | _ => thm);
   5.312 +
   5.313 +fun is_parametricity_theorem thm =
   5.314 +  (case Thm.concl_of thm of
   5.315 +    Const (@{const_name "HOL.Trueprop"}, _) $ (Const (rel, _) $ _ $ t $ u ) =>
   5.316 +      if rel = @{const_name "Transfer.Rel"} orelse
   5.317 +        rel = @{const_name "Conditional_Parametricity.Rel_match"}
   5.318 +      then curry Term.aconv_untyped t u
   5.319 +      else false
   5.320 +  | _ => false);
   5.321 +
   5.322 +(* Pre- and postprocessing of theorems *)
   5.323 +fun mk_Domainp_assm (T, R) =
   5.324 +  HOLogic.mk_eq ((Const (@{const_name Domainp}, Term.fastype_of T --> Term.fastype_of R) $ T), R);
   5.325 +
   5.326 +val Domainp_lemma =
   5.327 +  @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"
   5.328 +    by (rule, drule meta_spec,
   5.329 +      erule meta_mp, rule HOL.refl, simp)};
   5.330 +
   5.331 +fun fold_Domainp f (t as Const (@{const_name Domainp},_) $ (Var (_,_))) = f t
   5.332 +  | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u
   5.333 +  | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t
   5.334 +  | fold_Domainp _ _ = I;
   5.335 +
   5.336 +fun subst_terms tab t =
   5.337 +  let
   5.338 +    val t' = Termtab.lookup tab t
   5.339 +  in
   5.340 +    (case t' of
   5.341 +      SOME t' => t'
   5.342 +    | NONE =>
   5.343 +      (case t of
   5.344 +          u $ v => (subst_terms tab u) $ (subst_terms tab v)
   5.345 +        | Abs (a, T, t) => Abs (a, T, subst_terms tab t)
   5.346 +        | t => t))
   5.347 +  end;
   5.348 +
   5.349 +fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =
   5.350 +  let
   5.351 +    val prop = Thm.prop_of thm
   5.352 +    val (t, mk_prop') = dest prop
   5.353 +    val Domainp_ts = rev (fold_Domainp (fn t => insert op= t) t [])
   5.354 +    val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_ts
   5.355 +    val used = Term.add_free_names t []
   5.356 +    val rels = map (snd o dest_comb) Domainp_ts
   5.357 +    val rel_names = map (fst o fst o dest_Var) rels
   5.358 +    val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used
   5.359 +    val frees = map Free (names ~~ Domainp_Ts)
   5.360 +    val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees);
   5.361 +    val t' = subst_terms (fold Termtab.update (Domainp_ts ~~ frees) Termtab.empty) t
   5.362 +    val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))
   5.363 +    val prop2 = Logic.list_rename_params (rev names) prop1
   5.364 +    val cprop = Thm.cterm_of ctxt prop2
   5.365 +    val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop
   5.366 +    fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;
   5.367 +  in
   5.368 +    forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
   5.369 +  end
   5.370 +    handle TERM _ => thm;
   5.371 +
   5.372 +fun abstract_domains_transfer ctxt thm =
   5.373 +  let
   5.374 +    fun dest prop =
   5.375 +      let
   5.376 +        val prems = Logic.strip_imp_prems prop
   5.377 +        val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
   5.378 +        val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
   5.379 +      in
   5.380 +        (x, fn x' =>
   5.381 +          Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))
   5.382 +      end
   5.383 +  in
   5.384 +    gen_abstract_domains ctxt dest thm
   5.385 +  end;
   5.386 +
   5.387 +fun transfer_rel_conv conv =
   5.388 +  Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv)));
   5.389 +
   5.390 +fun fold_relator_eqs_conv ctxt ct = (Transfer.bottom_rewr_conv (Transfer.get_relator_eq ctxt)) ct;
   5.391 +
   5.392 +fun mk_is_equality t =
   5.393 +  Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t;
   5.394 +
   5.395 +val is_equality_lemma =
   5.396 +  @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))"
   5.397 +    by (unfold is_equality_def, rule, drule meta_spec,
   5.398 +      erule meta_mp, rule HOL.refl, simp)};
   5.399 +
   5.400 +fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =
   5.401 +  let
   5.402 +    val prop = Thm.prop_of thm
   5.403 +    val (t, mk_prop') = dest prop
   5.404 +    (* Only consider "op =" at non-base types *)
   5.405 +    fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) =
   5.406 +        (case T of Type (_, []) => false | _ => true)
   5.407 +      | is_eq _ = false
   5.408 +    val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)
   5.409 +    val eq_consts = rev (add_eqs t [])
   5.410 +    val eqTs = map (snd o dest_Const) eq_consts
   5.411 +    val used = Term.add_free_names prop []
   5.412 +    val names = map (K "") eqTs |> Name.variant_list used
   5.413 +    val frees = map Free (names ~~ eqTs)
   5.414 +    val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees
   5.415 +    val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)
   5.416 +    val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))
   5.417 +    val cprop = Thm.cterm_of ctxt prop2
   5.418 +    val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop
   5.419 +    fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm
   5.420 +  in
   5.421 +    forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))
   5.422 +  end
   5.423 +    handle TERM _ => thm;
   5.424 +
   5.425 +fun abstract_equalities_transfer ctxt thm =
   5.426 +  let
   5.427 +    fun dest prop =
   5.428 +      let
   5.429 +        val prems = Logic.strip_imp_prems prop
   5.430 +        val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)
   5.431 +        val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)
   5.432 +      in
   5.433 +        (rel, fn rel' =>
   5.434 +          Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))
   5.435 +      end
   5.436 +    val contracted_eq_thm =
   5.437 +      Conv.fconv_rule (transfer_rel_conv (fold_relator_eqs_conv ctxt)) thm
   5.438 +      handle CTERM _ => thm
   5.439 +  in
   5.440 +    gen_abstract_equalities ctxt dest contracted_eq_thm
   5.441 +  end;
   5.442 +
   5.443 +fun prep_rule ctxt = abstract_equalities_transfer ctxt #> abstract_domains_transfer ctxt;
   5.444 +
   5.445 +fun get_preprocess_theorems ctxt =
   5.446 +  Named_Theorems.get ctxt @{named_theorems parametricity_preprocess};
   5.447 +
   5.448 +fun preprocess_theorem ctxt =
   5.449 +  Local_Defs.unfold0 ctxt (get_preprocess_theorems ctxt)
   5.450 +  #> transform_class_rule ctxt;
   5.451 +
   5.452 +fun postprocess_theorem ctxt =
   5.453 +  Local_Defs.fold ctxt (@{thm Rel_Rel_match_eq} :: get_preprocess_theorems ctxt)
   5.454 +  #> prep_rule ctxt
   5.455 +  #>  Local_Defs.unfold ctxt @{thms Rel_def};
   5.456 +
   5.457 +fun get_parametricity_theorems ctxt =
   5.458 +  let
   5.459 +    val parametricity_thm_map_filter =
   5.460 +      Option.filter (is_parametricity_theorem andf (not o curry Term.could_unify
   5.461 +        (Thm.full_prop_of @{thm is_equality_Rel})) o Thm.full_prop_of) o preprocess_theorem ctxt;
   5.462 +  in
   5.463 +    map_filter (parametricity_thm_map_filter o Thm.transfer (Proof_Context.theory_of ctxt))
   5.464 +      (Transfer.get_transfer_raw ctxt)
   5.465 +  end;
   5.466 +
   5.467 +(* Provers *)
   5.468 +(* Tries to prove a parametricity theorem without conditions, returns the last goal_state as thm *)
   5.469 +fun prove_find_goal_cond settings ctxt rules def_thm t =
   5.470 +  let
   5.471 +    fun find_conditions_tac {context = ctxt, prems = _} = unfold_tac ctxt (the_list def_thm) THEN
   5.472 +      (REPEAT_TRY_ELSE_DEFER o HEADGOAL) (step_tac settings ctxt rules);
   5.473 +  in
   5.474 +    Goal.prove ctxt [] [] t find_conditions_tac handle FINISH st => st
   5.475 +  end;
   5.476 +
   5.477 +(* Simplifies and proves thm *)
   5.478 +fun prove_cond_goal ctxt thm =
   5.479 +  let
   5.480 +    val (goal, thm') = mk_cond_goal ctxt thm;
   5.481 +    val vars = Variable.add_free_names ctxt goal [];
   5.482 +    fun prove_conditions_tac {context = ctxt, prems = _} = apply_theorem_tac ctxt thm';
   5.483 +    val vars = Variable.add_free_names ctxt (Thm.prop_of thm') vars;
   5.484 +  in
   5.485 +    Goal.prove ctxt vars [] goal prove_conditions_tac
   5.486 +  end;
   5.487 +
   5.488 +(* Finds necessary conditions for t and proofs conditional parametricity of t under those conditions *)
   5.489 +fun prove_goal settings ctxt def_thm t =
   5.490 +  let
   5.491 +    val parametricity_thms = get_parametricity_theorems ctxt;
   5.492 +    val found_thm = prove_find_goal_cond settings ctxt parametricity_thms def_thm t;
   5.493 +    val thm = prove_cond_goal ctxt found_thm;
   5.494 +  in
   5.495 +    postprocess_theorem ctxt thm
   5.496 +  end;
   5.497 +
   5.498 +(* Commands  *)
   5.499 +fun gen_parametric_constant settings prep_att prep_thm (raw_b : Attrib.binding, raw_eq) lthy =
   5.500 +  let
   5.501 +    val b = apsnd (map (prep_att lthy)) raw_b;
   5.502 +    val def_thm = (prep_thm lthy raw_eq);
   5.503 +    val eq = Ctr_Sugar_Util.mk_abs_def def_thm handle TERM _ => theorem_format_error lthy def_thm;
   5.504 +    val goal= mk_param_goal_from_eq_def lthy eq;
   5.505 +    val thm = prove_goal settings lthy (SOME eq) goal;
   5.506 +    val (res, lthy') = Local_Theory.note (b, [thm]) lthy;
   5.507 +    val _ = if #suppress_print_theorem settings then () else
   5.508 +      Proof_Display.print_results true (Position.thread_data ()) lthy' (("theorem",""), [res]);
   5.509 +  in
   5.510 +    (the_single (snd res), lthy')
   5.511 +  end;
   5.512 +
   5.513 +fun parametric_constant settings = gen_parametric_constant settings (K I) (K I);
   5.514 +
   5.515 +val parametric_constant_cmd = snd oo gen_parametric_constant default_settings (Attrib.check_src)
   5.516 +  (singleton o Attrib.eval_thms);
   5.517 +
   5.518 +val _ =
   5.519 +  Outer_Syntax.local_theory @{command_keyword parametric_constant} "proves parametricity"
   5.520 +    ((Parse_Spec.opt_thm_name ":" -- Parse.thm) >> parametric_constant_cmd);
   5.521 +
   5.522 +end;
   5.523 \ No newline at end of file
     6.1 --- a/src/HOL/ROOT	Mon Dec 18 11:56:12 2017 +0100
     6.2 +++ b/src/HOL/ROOT	Mon Dec 18 16:58:13 2017 +0100
     6.3 @@ -537,6 +537,7 @@
     6.4      Coherent
     6.5      Commands
     6.6      Computations
     6.7 +    Conditional_Parametricity_Examples
     6.8      Cubic_Quartic
     6.9      Dedekind_Real
    6.10      Erdoes_Szekeres
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/ex/Conditional_Parametricity_Examples.thy	Mon Dec 18 16:58:13 2017 +0100
     7.3 @@ -0,0 +1,64 @@
     7.4 +(*  Title:    HOL/ex/Conditional_Parametricity_Examples.thy
     7.5 +    Author:   Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel, ETH Zürich
     7.6 +
     7.7 +Examples for the parametric_constant command
     7.8 +*)
     7.9 +
    7.10 +theory Conditional_Parametricity_Examples
    7.11 +  imports "HOL-Library.Conditional_Parametricity"
    7.12 +begin
    7.13 +
    7.14 +definition "bar x xs = rev (x # xs)"
    7.15 +parametric_constant bar_def
    7.16 +
    7.17 +definition bar2 where "bar2 = bar"
    7.18 +parametric_constant bar2_def
    7.19 +
    7.20 +parametric_constant bar_thm[transfer_rule]: bar_def
    7.21 +parametric_constant bar2_thm1: bar2_def
    7.22 +
    7.23 +definition "t1 y x = zip x y"
    7.24 +parametric_constant t1_thm: t1_def
    7.25 +
    7.26 +definition "t2 f x = f (rev x)"
    7.27 +parametric_constant t2_thm: t2_def
    7.28 +
    7.29 +definition "t3 xs = rev (rev (xs :: 'b list))"
    7.30 +parametric_constant t3_thm: t3_def
    7.31 +
    7.32 +definition "t4 f x = rev (f x (f x (rev x)))"
    7.33 +parametric_constant t4_thm: t4_def
    7.34 +
    7.35 +definition "t5 x y = zip x (rev y)"
    7.36 +parametric_constant t5_thm: t5_def
    7.37 +
    7.38 +(* Conditional Parametricity*)
    7.39 +
    7.40 +definition "t6_1 x y = inf y x"
    7.41 +parametric_constant t6_1_thm: t6_1_def
    7.42 +
    7.43 +definition "t6_2 x y = sup y x"
    7.44 +parametric_constant t6_2_thm: t6_2_def
    7.45 +
    7.46 +definition "t6_3 x z y = sup (inf x y) z"
    7.47 +parametric_constant t6_3_thm: t6_3_def
    7.48 +
    7.49 +definition "t6_4 x xs y = map (sup (inf y x)) xs"
    7.50 +parametric_constant t6_4_thm: t6_4_def
    7.51 +
    7.52 +definition "t7 x y = (y = x)"
    7.53 +parametric_constant t7_thm: t7_def
    7.54 +
    7.55 +definition "t8 x y = ((x=y) \<and> (y=x))"
    7.56 +parametric_constant t8_thm: t8_def
    7.57 +
    7.58 +(* Definition via primrec*)
    7.59 +primrec delete where
    7.60 +  "delete _ [] = []"
    7.61 +| "delete x (y # ys) = (if x = y then ys else y # (delete x ys))"
    7.62 +parametric_constant delete_thm: delete_def
    7.63 +
    7.64 +definition "foo f x y = (if f x = f y then x else sup y x)"
    7.65 +parametric_constant foo_parametricity: foo_def
    7.66 +
    7.67 +end
    7.68 \ No newline at end of file