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 \ 'b \ bool) \ 'a \ 'b \ 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 \ 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 \ 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 \ 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 ```