src/HOL/Library/Conditional_Parametricity.thy
author haftmann
Wed Jul 18 20:51:21 2018 +0200 (11 months ago)
changeset 68658 16cc1161ad7f
parent 67399 eab6ce8368fa
child 69605 a96320074298
permissions -rw-r--r--
tuned equation
traytel@67224
     1
(*  Title:    HOL/Library/Conditional_Parametricity.thy
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
theory Conditional_Parametricity
traytel@67224
     8
imports Main
traytel@67224
     9
keywords "parametric_constant" :: thy_decl
traytel@67224
    10
begin
traytel@67224
    11
traytel@67224
    12
context includes lifting_syntax begin
traytel@67224
    13
traytel@67224
    14
qualified definition Rel_match :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
traytel@67224
    15
  "Rel_match R x y = R x y"
traytel@67224
    16
traytel@67224
    17
named_theorems parametricity_preprocess
traytel@67224
    18
traytel@67224
    19
lemma bi_unique_Rel_match [parametricity_preprocess]:
nipkow@67399
    20
  "bi_unique A = Rel_match (A ===> A ===> (=)) (=) (=)"
traytel@67224
    21
  unfolding bi_unique_alt_def2 Rel_match_def ..
traytel@67224
    22
traytel@67224
    23
lemma bi_total_Rel_match [parametricity_preprocess]:
nipkow@67399
    24
  "bi_total A = Rel_match ((A ===> (=)) ===> (=)) All All"
traytel@67224
    25
  unfolding bi_total_alt_def2 Rel_match_def ..
traytel@67224
    26
traytel@67224
    27
lemma is_equality_Rel: "is_equality A \<Longrightarrow> Transfer.Rel A t t"
traytel@67224
    28
  by (fact transfer_raw)
traytel@67224
    29
traytel@67224
    30
lemma Rel_Rel_match: "Transfer.Rel R x y \<Longrightarrow> Rel_match R x y"
traytel@67224
    31
  unfolding Rel_match_def Rel_def .
traytel@67224
    32
traytel@67224
    33
lemma Rel_match_Rel: "Rel_match R x y \<Longrightarrow> Transfer.Rel R x y"
traytel@67224
    34
  unfolding Rel_match_def Rel_def .
traytel@67224
    35
traytel@67224
    36
lemma Rel_Rel_match_eq: "Transfer.Rel R x y = Rel_match R x y"
traytel@67224
    37
  using Rel_Rel_match Rel_match_Rel by fast
traytel@67224
    38
traytel@67224
    39
lemma Rel_match_app:
traytel@67224
    40
  assumes "Rel_match (A ===> B) f g" and "Transfer.Rel A x y"
traytel@67224
    41
  shows "Rel_match B (f x) (g y)"
traytel@67224
    42
  using assms Rel_match_Rel Rel_app Rel_Rel_match by fast
traytel@67224
    43
traytel@67224
    44
end
traytel@67224
    45
traytel@67224
    46
ML_file "conditional_parametricity.ML"
traytel@67224
    47
nipkow@67399
    48
end