more transfer rules
authorAndreas Lochbihler
Wed Feb 11 15:03:21 2015 +0100 (2015-02-11)
changeset 59523860fb1c65553
parent 59522 0c5c5ad5d2e0
child 59524 67deb7bed6d3
more transfer rules
src/HOL/Option.thy
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Option.thy	Wed Feb 11 14:45:10 2015 +0100
     1.2 +++ b/src/HOL/Option.thy	Wed Feb 11 15:03:21 2015 +0100
     1.3 @@ -77,6 +77,7 @@
     1.4    "(\<And>x. x \<in> set_option y \<Longrightarrow> P x x) \<Longrightarrow> rel_option P y y"
     1.5  by(cases y) auto
     1.6  
     1.7 +
     1.8  subsubsection {* Operations *}
     1.9  
    1.10  lemma ospec [dest]: "(ALL x:set_option A. P x) ==> A = Some x ==> P x"
    1.11 @@ -261,6 +262,10 @@
    1.12      Option.bind Option.bind"
    1.13    unfolding rel_fun_def split_option_all by simp
    1.14  
    1.15 +lemma pred_option_parametric [transfer_rule]:
    1.16 +  "((A ===> op =) ===> rel_option A ===> op =) pred_option pred_option"
    1.17 +by(rule rel_funI)+(auto simp add: rel_option_unfold is_none_def dest: rel_funD)
    1.18 +
    1.19  end
    1.20  
    1.21  
     2.1 --- a/src/HOL/Transfer.thy	Wed Feb 11 14:45:10 2015 +0100
     2.2 +++ b/src/HOL/Transfer.thy	Wed Feb 11 15:03:21 2015 +0100
     2.3 @@ -533,13 +533,35 @@
     2.4  by fast+
     2.5  
     2.6  lemma right_unique_transfer [transfer_rule]:
     2.7 -  assumes [transfer_rule]: "right_total A"
     2.8 -  assumes [transfer_rule]: "right_total B"
     2.9 -  assumes [transfer_rule]: "bi_unique B"
    2.10 -  shows "((A ===> B ===> op=) ===> implies) right_unique right_unique"
    2.11 -using assms unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
    2.12 +  "\<lbrakk> right_total A; right_total B; bi_unique B \<rbrakk>
    2.13 +  \<Longrightarrow> ((A ===> B ===> op=) ===> implies) right_unique right_unique"
    2.14 +unfolding right_unique_def[abs_def] right_total_def bi_unique_def rel_fun_def
    2.15  by metis
    2.16  
    2.17 +lemma left_total_parametric [transfer_rule]:
    2.18 +  assumes [transfer_rule]: "bi_total A" "bi_total B"
    2.19 +  shows "((A ===> B ===> op =) ===> op =) left_total left_total"
    2.20 +unfolding left_total_def[abs_def] by transfer_prover
    2.21 +
    2.22 +lemma right_total_parametric [transfer_rule]:
    2.23 +  assumes [transfer_rule]: "bi_total A" "bi_total B"
    2.24 +  shows "((A ===> B ===> op =) ===> op =) right_total right_total"
    2.25 +unfolding right_total_def[abs_def] by transfer_prover
    2.26 +
    2.27 +lemma left_unique_parametric [transfer_rule]:
    2.28 +  assumes [transfer_rule]: "bi_unique A" "bi_total A" "bi_total B"
    2.29 +  shows "((A ===> B ===> op =) ===> op =) left_unique left_unique"
    2.30 +unfolding left_unique_def[abs_def] by transfer_prover
    2.31 +
    2.32 +lemma prod_pred_parametric [transfer_rule]:
    2.33 +  "((A ===> op =) ===> (B ===> op =) ===> rel_prod A B ===> op =) pred_prod pred_prod"
    2.34 +unfolding pred_prod_def[abs_def] Basic_BNFs.fsts_def Basic_BNFs.snds_def fstsp.simps sndsp.simps 
    2.35 +by simp transfer_prover
    2.36 +
    2.37 +lemma apfst_parametric [transfer_rule]:
    2.38 +  "((A ===> B) ===> rel_prod A C ===> rel_prod B C) apfst apfst"
    2.39 +unfolding apfst_def[abs_def] by transfer_prover
    2.40 +
    2.41  lemma rel_fun_eq_eq_onp: "(op= ===> eq_onp P) = eq_onp (\<lambda>f. \<forall>x. P(f x))"
    2.42  unfolding eq_onp_def rel_fun_def by auto
    2.43  
    2.44 @@ -591,6 +613,11 @@
    2.45    }
    2.46  qed
    2.47  
    2.48 +lemma right_unique_parametric [transfer_rule]:
    2.49 +  assumes [transfer_rule]: "bi_total A" "bi_unique B" "bi_total B"
    2.50 +  shows "((A ===> B ===> op =) ===> op =) right_unique right_unique"
    2.51 +unfolding right_unique_def[abs_def] by transfer_prover
    2.52 +
    2.53  end
    2.54  
    2.55  end