concrete semantics Ex43

Ex43.thy

theory Ex43 imports Main begin

inductive star :: "( 'a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where
refl: "star r x x" |
step: "r x y ⟹ star r y z ⟹ star r x z"

thm star.step [where ?z = "y"]


lemma r2star: "r x y ⟹ star r x y"
apply (rule  star.step [where ?z = "y"])
apply(auto)
apply(rule star.refl [where ?x=y])
done

thm r2star[where ?x=y and ?y=z]
thm r2star[where ?r=r and ?x=y and ?y=z]

lemma star_trans: "star r x y ⟹ star r y z ⟹ star r x z"
apply(induction rule: star.induct)
apply(auto)
apply(metis step)
done

inductive star' :: "( 'a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where
refl' : "star' r x x" |
step' : "star' r x y ⟹ r y z ⟹ star' r x z"

lemma r2star': "r x y ⟹ star' r x y"
apply (rule  star'.step' [where ?z = "y"])
apply(auto)
apply(rule star'.refl' [where ?x=x])
done

 
lemma star_trans': "star' r x y ⟹ star' r y z ⟹ star' r x z"
proof (induction x y arbitrary:z rule: star'.induct)
  case (refl' x)
  then show ?case by blast
next
  case (step' x y w)
  then have A:"star' r y w" by (simp add: r2star')
  then have A:"star' r x w" by (simp add: step'.IH)
  then have A:"star' r w z" using step'.prems by blast
  then have A:"star' r x z" using step'.prems r2star' by blast
  then show ?case by blast
qed

lemma star'2star:"(star' r x y) ⟹ star r x y"
proof (induction rule: star'.induct)
  case (refl' x)
  then show ?case by (simp add:refl)
next
  case (step' x y z)
  then show ?case by (meson r2star star_trans)
qed
  
  
lemma star2star':"(star r x y) ⟹ star' r x y"
proof (induction rule: star.induct)
  case (refl x)
  then show ?case by (simp add:refl')
next
  case (step x y z)
  then have "star' r x y" using  r2star' by blast
  then show ?case using star_trans' by auto
qed

end