[STATEMENT]
lemma postfix_conv_eq_length_drop:
  "ST' \<bind> ST \<longleftrightarrow> length ST \<le> length ST' \<and> drop (length ST' - length ST) ST' = ST"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ST' \<bind> ST) = (length ST \<le> length ST' \<and> drop (length ST' - length ST) ST' = ST)
[PROOF STEP]
apply(auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. ST' \<bind> ST \<Longrightarrow> length ST \<le> length ST'
 2. ST' \<bind> ST \<Longrightarrow> drop (length ST' - length ST) ST' = ST
 3. \<lbrakk>length ST \<le> length ST'; drop (length ST' - length ST) ST' = ST\<rbrakk> \<Longrightarrow> ST' \<bind> ST
[PROOF STEP]
apply (metis append_eq_conv_conj append_take_drop_id diff_is_0_eq drop_0 linorder_not_less nat_le_linear suffix_take)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ST' \<bind> ST \<Longrightarrow> drop (length ST' - length ST) ST' = ST
 2. \<lbrakk>length ST \<le> length ST'; drop (length ST' - length ST) ST' = ST\<rbrakk> \<Longrightarrow> ST' \<bind> ST
[PROOF STEP]
apply (metis append_take_drop_id length_drop suffix_take same_append_eq size_list_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ST \<le> length ST'; drop (length ST' - length ST) ST' = ST\<rbrakk> \<Longrightarrow> ST' \<bind> ST
[PROOF STEP]
by (metis suffix_drop)


[STATEMENT]
lemma fun_of_simp [simp]: "fun_of S x y = ((x,y) \<in> S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fun_of S x y = ((x, y) \<in> S)
[PROOF STEP]
by (simp add: fun_of_def)