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
```