memo: star to list

Trans.thy

theory Trans
imports Main
begin
(* "Lectures on the Curry-Howard Isomorphism"  Lemma 1.4.2 *)

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

inductive trans_list :: "( 'a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool" for r where
lift': "r x y ⟹ trans_list r (x#y#[])" |
trans': "trans_list r (xs@[y]) ⟹ trans_list r (y#zs) ⟹ trans_list r (xs@(y#zs))"
  
lemma "star r x z ⟹ ∃xs. trans_list r ((x#xs)@[z])"
proof (induction rule: star.induct)
  case (lift x y)
  then show ?case by (metis Cons_eq_append_conv lift')
next
  case (trans x y z)
  assume A1:"∃xs. trans_list r ((x # xs) @ [y])"
  then obtain xs1 where XS1:"trans_list r ((x # xs1) @ [y])" by blast

  assume A2:"∃xs. trans_list r ((y # xs) @ [z])"
  then obtain xs2 where XS2:"trans_list r ((y # xs2) @ [z])" by blast
      
  {have "trans_list r ((x # (xs1 @ [y] @ xs2)) @ [z])"
  proof -
    have "trans_list r (y # (xs2 @ [z]))" using XS2 List.append.append_Cons by auto
    then have "trans_list r ((x # xs1)  @ (y # (xs2 @ [z])))" using XS1 trans_list.trans'  by fastforce
    then show ?thesis by simp 
  qed
  }
  then obtain xs where "trans_list r ((x # xs) @ [z])" by blast
  then show ?case by auto
qed
  
end