(* A simple data transmission protocol *)

theory Pro = Main:

(* The state consists of
   - the infinite input queue
   - an index into the input queue of the next element to be sent
   - the channel between input and output
   - the finite output buffer
*)
   
types 'a state =  "(nat \<Rightarrow> 'a) * nat * 'a list * 'a list"

consts Pro :: "'a state set"

inductive Pro
intros
Init:
"(f,0,[],[]) \<in> Pro"
Send_message: (* from input into transmission channel *)
"(f,n,c,xs) \<in> Pro \<Longrightarrow> (f,Suc n,c@[f n],xs) \<in> Pro"
Receive_message: (* from transmission channel into output *)
"(f,n,x#c,xs) \<in> Pro \<Longrightarrow> (f,n,c,xs@[x]) \<in> Pro"

declare nth_append[simp]

theorem "(f,n,c,xs) \<in> Pro
 \<Longrightarrow> n = size c + size xs &
    (\<forall>i < size c. c!i = f(i+size xs)) &
    (\<forall>i < size xs. xs!i = f i)"
apply(erule Pro.induct)
(* Init *)
apply simp
(* Smsg *)
apply clarsimp
apply(subgoal_tac "i = length c")
 prefer 2 apply simp
apply clarify
(* Rmsg *)
apply clarsimp
apply(rule conjI)
 apply clarsimp
 apply(erule_tac x="Suc i" in allE)
 apply simp
apply clarsimp
apply(subgoal_tac "i = length xs")
 prefer 2 apply simp
apply clarify
apply simp
apply(erule_tac x="0" in allE)
apply simp
done

end