src/HOL/Transfer.thy
changeset 57599 7ef939f89776
parent 57398 882091eb1e9a
child 58128 43a1ba26a8cb
     1.1 --- a/src/HOL/Transfer.thy	Mon Jul 21 17:51:11 2014 +0200
     1.2 +++ b/src/HOL/Transfer.thy	Mon Jul 21 17:51:29 2014 +0200
     1.3 @@ -536,6 +536,45 @@
     1.4    shows "((A ===> op=) ===> A ===> A ===> op=) eq_onp eq_onp"
     1.5  unfolding eq_onp_def[abs_def] by transfer_prover
     1.6  
     1.7 +lemma rtranclp_parametric [transfer_rule]:
     1.8 +  assumes "bi_unique A" "bi_total A"
     1.9 +  shows "((A ===> A ===> op =) ===> A ===> A ===> op =) rtranclp rtranclp"
    1.10 +proof(rule rel_funI iffI)+
    1.11 +  fix R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" and R' x y x' y'
    1.12 +  assume R: "(A ===> A ===> op =) R R'" and "A x x'"
    1.13 +  {
    1.14 +    assume "R\<^sup>*\<^sup>* x y" "A y y'"
    1.15 +    thus "R'\<^sup>*\<^sup>* x' y'"
    1.16 +    proof(induction arbitrary: y')
    1.17 +      case base
    1.18 +      with `bi_unique A` `A x x'` have "x' = y'" by(rule bi_uniqueDr)
    1.19 +      thus ?case by simp
    1.20 +    next
    1.21 +      case (step y z z')
    1.22 +      from `bi_total A` obtain y' where "A y y'" unfolding bi_total_def by blast
    1.23 +      hence "R'\<^sup>*\<^sup>* x' y'" by(rule step.IH)
    1.24 +      moreover from R `A y y'` `A z z'` `R y z`
    1.25 +      have "R' y' z'" by(auto dest: rel_funD)
    1.26 +      ultimately show ?case ..
    1.27 +    qed
    1.28 +  next
    1.29 +    assume "R'\<^sup>*\<^sup>* x' y'" "A y y'"
    1.30 +    thus "R\<^sup>*\<^sup>* x y"
    1.31 +    proof(induction arbitrary: y)
    1.32 +      case base
    1.33 +      with `bi_unique A` `A x x'` have "x = y" by(rule bi_uniqueDl)
    1.34 +      thus ?case by simp
    1.35 +    next
    1.36 +      case (step y' z' z)
    1.37 +      from `bi_total A` obtain y where "A y y'" unfolding bi_total_def by blast
    1.38 +      hence "R\<^sup>*\<^sup>* x y" by(rule step.IH)
    1.39 +      moreover from R `A y y'` `A z z'` `R' y' z'`
    1.40 +      have "R y z" by(auto dest: rel_funD)
    1.41 +      ultimately show ?case ..
    1.42 +    qed
    1.43 +  }
    1.44 +qed
    1.45 +
    1.46  end
    1.47  
    1.48  end