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
```     1 (*  Title:    HOL/Library/Conditional_Parametricity.thy
```
```     2     Author:   Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel, ETH Zürich
```
```     3
```
```     4 A conditional parametricity prover
```
```     5 *)
```
```     6
```
```     7 theory Conditional_Parametricity
```
```     8 imports Main
```
```     9 keywords "parametric_constant" :: thy_decl
```
```    10 begin
```
```    11
```
```    12 context includes lifting_syntax begin
```
```    13
```
```    14 qualified definition Rel_match :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
```
```    15   "Rel_match R x y = R x y"
```
```    16
```
```    17 named_theorems parametricity_preprocess
```
```    18
```
```    19 lemma bi_unique_Rel_match [parametricity_preprocess]:
```
```    20   "bi_unique A = Rel_match (A ===> A ===> (=)) (=) (=)"
```
```    21   unfolding bi_unique_alt_def2 Rel_match_def ..
```
```    22
```
```    23 lemma bi_total_Rel_match [parametricity_preprocess]:
```
```    24   "bi_total A = Rel_match ((A ===> (=)) ===> (=)) All All"
```
```    25   unfolding bi_total_alt_def2 Rel_match_def ..
```
```    26
```
```    27 lemma is_equality_Rel: "is_equality A \<Longrightarrow> Transfer.Rel A t t"
```
```    28   by (fact transfer_raw)
```
```    29
```
```    30 lemma Rel_Rel_match: "Transfer.Rel R x y \<Longrightarrow> Rel_match R x y"
```
```    31   unfolding Rel_match_def Rel_def .
```
```    32
```
```    33 lemma Rel_match_Rel: "Rel_match R x y \<Longrightarrow> Transfer.Rel R x y"
```
```    34   unfolding Rel_match_def Rel_def .
```
```    35
```
```    36 lemma Rel_Rel_match_eq: "Transfer.Rel R x y = Rel_match R x y"
```
```    37   using Rel_Rel_match Rel_match_Rel by fast
```
```    38
```
```    39 lemma Rel_match_app:
```
```    40   assumes "Rel_match (A ===> B) f g" and "Transfer.Rel A x y"
```
```    41   shows "Rel_match B (f x) (g y)"
```
```    42   using assms Rel_match_Rel Rel_app Rel_Rel_match by fast
```
```    43
```
```    44 end
```
```    45
```
```    46 ML_file "conditional_parametricity.ML"
```
```    47
```
```    48 end
```