parametricity transfer rule for INFIMUM, SUPREMUM
authorhaftmann
Wed Apr 09 10:04:31 2014 +0200 (2014-04-09)
changeset 5648239ac12b655ab
parent 56481 47500d0881f9
child 56483 5b82c58b665c
parametricity transfer rule for INFIMUM, SUPREMUM
src/HOL/Lifting_Set.thy
     1.1 --- a/src/HOL/Lifting_Set.thy	Wed Apr 09 09:37:49 2014 +0200
     1.2 +++ b/src/HOL/Lifting_Set.thy	Wed Apr 09 10:04:31 2014 +0200
     1.3 @@ -145,23 +145,21 @@
     1.4    done
     1.5  
     1.6  lemma rel_set_transfer [transfer_rule]:
     1.7 -  "((A ===> B ===> op =) ===> rel_set A ===> rel_set B ===> op =)
     1.8 -    rel_set rel_set"
     1.9 +  "((A ===> B ===> op =) ===> rel_set A ===> rel_set B ===> op =) rel_set rel_set"
    1.10    unfolding rel_fun_def rel_set_def by fast
    1.11  
    1.12 -lemma SUP_parametric [transfer_rule]:
    1.13 -  "(rel_set R ===> (R ===> op =) ===> op =) SUPREMUM (SUPREMUM :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
    1.14 -proof(rule rel_funI)+
    1.15 -  fix A B f and g :: "'b \<Rightarrow> 'c"
    1.16 -  assume AB: "rel_set R A B"
    1.17 -    and fg: "(R ===> op =) f g"
    1.18 -  show "SUPREMUM A f = SUPREMUM B g"
    1.19 -    by (rule SUP_eq) (auto 4 4 dest: rel_setD1 [OF AB] rel_setD2 [OF AB] rel_funD [OF fg] intro: rev_bexI)
    1.20 -qed
    1.21 -
    1.22  lemma bind_transfer [transfer_rule]:
    1.23    "(rel_set A ===> (A ===> rel_set B) ===> rel_set B) Set.bind Set.bind"
    1.24 -unfolding bind_UNION[abs_def] by transfer_prover
    1.25 +  unfolding bind_UNION [abs_def] by transfer_prover
    1.26 +
    1.27 +lemma INF_parametric [transfer_rule]:
    1.28 +  "(rel_set A ===> (A ===> HOL.eq) ===> HOL.eq) INFIMUM INFIMUM"
    1.29 +  unfolding INF_def [abs_def] by transfer_prover
    1.30 +
    1.31 +lemma SUP_parametric [transfer_rule]:
    1.32 +  "(rel_set R ===> (R ===> HOL.eq) ===> HOL.eq) SUPREMUM SUPREMUM"
    1.33 +  unfolding SUP_def [abs_def] by transfer_prover
    1.34 +
    1.35  
    1.36  subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *}
    1.37