|
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 ===> op =) op = op =" |
|
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 ===> op =) ===> op =) 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 |