1(* Title: HOL/ex/Conditional_Parametricity_Examples.thy 2 Author: Jan Gilcher, Andreas Lochbihler, Dmitriy Traytel, ETH Z��rich 3 4Examples for the parametric_constant command 5*) 6 7theory Conditional_Parametricity_Examples 8 imports "HOL-Library.Conditional_Parametricity" 9begin 10 11definition "bar x xs = rev (x # xs)" 12parametric_constant bar_def 13 14definition bar2 where "bar2 = bar" 15parametric_constant bar2_def 16 17parametric_constant bar_thm[transfer_rule]: bar_def 18parametric_constant bar2_thm1: bar2_def 19 20definition "t1 y x = zip x y" 21parametric_constant t1_thm: t1_def 22 23definition "t2 f x = f (rev x)" 24parametric_constant t2_thm: t2_def 25 26definition "t3 xs = rev (rev (xs :: 'b list))" 27parametric_constant t3_thm: t3_def 28 29definition "t4 f x = rev (f x (f x (rev x)))" 30parametric_constant t4_thm: t4_def 31 32definition "t5 x y = zip x (rev y)" 33parametric_constant t5_thm: t5_def 34 35(* Conditional Parametricity*) 36 37definition "t6_1 x y = inf y x" 38parametric_constant t6_1_thm: t6_1_def 39 40definition "t6_2 x y = sup y x" 41parametric_constant t6_2_thm: t6_2_def 42 43definition "t6_3 x z y = sup (inf x y) z" 44parametric_constant t6_3_thm: t6_3_def 45 46definition "t6_4 x xs y = map (sup (inf y x)) xs" 47parametric_constant t6_4_thm: t6_4_def 48 49definition "t7 x y = (y = x)" 50parametric_constant t7_thm: t7_def 51 52definition "t8 x y = ((x=y) \<and> (y=x))" 53parametric_constant t8_thm: t8_def 54 55(* Definition via primrec*) 56primrec delete where 57 "delete _ [] = []" 58| "delete x (y # ys) = (if x = y then ys else y # (delete x ys))" 59parametric_constant delete_thm: delete_def 60 61definition "foo f x y = (if f x = f y then x else sup y x)" 62parametric_constant foo_parametricity: foo_def 63 64end 65