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
  assumes "star r x z"
  obtains xs where "trans_list r ((x#xs)@[z])"
apply (induction rule: star.induct [OF assms])
  apply (metis append.left_neutral append_Cons lift')
  apply (metis append.assoc append_Cons trans_list.intros(2))
done
  
end