theory Retype_C

lemma replicate_append_list [rule_format]:
  "\<forall>n. set L \<subseteq> {0::word8} \<longrightarrow> (replicate n 0 @ L = replicate (n + length L) 0)" apply (rule rev_induct) apply clarsimp apply (rule allI) apply (erule_tac x="n+1" in allE) apply clarsimp apply (subst append_assoc[symmetric]) apply clarsimp apply (subgoal_tac "\<And>n. (replicate n 0 @ [0]) = (0 # replicate n (0 :: word8))") apply clarsimp apply (induct_tac na) apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>n. set L \<subseteq> {0} \<longrightarrow> replicate n 0 @ L = replicate (n + length L) 0 proof (prove)
goal (2 subgoals):
 1. \<forall>n. set [] \<subseteq> {0} \<longrightarrow> replicate n 0 @ [] = replicate (n + length []) 0
 2. \<And>x xs. \<forall>n. set xs \<subseteq> {0} \<longrightarrow> replicate n 0 @ xs = replicate (n + length xs) 0 \<Longrightarrow> \<forall>n. set (xs @ [x]) \<subseteq> {0} \<longrightarrow> replicate n 0 @ xs @ [x] = replicate (n + length (xs @ [x])) 0 proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<forall>n. set xs \<subseteq> {0} \<longrightarrow> replicate n 0 @ xs = replicate (n + length xs) 0 \<Longrightarrow> \<forall>n. set (xs @ [x]) \<subseteq> {0} \<longrightarrow> replicate n 0 @ xs @ [x] = replicate (n + length (xs @ [x])) 0 proof (prove)
goal (1 subgoal):
 1. \<And>x xs n. \<forall>n. set xs \<subseteq> {0} \<longrightarrow> replicate n 0 @ xs = replicate (n + length xs) 0 \<Longrightarrow> set (xs @ [x]) \<subseteq> {0} \<longrightarrow> replicate n 0 @ xs @ [x] = replicate (n + length (xs @ [x])) 0 proof (prove)
goal (1 subgoal):
 1. \<And>x xs n. set xs \<subseteq> {0} \<longrightarrow> replicate (n + 1) 0 @ xs = replicate (n + 1 + length xs) 0 \<Longrightarrow> set (xs @ [x]) \<subseteq> {0} \<longrightarrow> replicate n 0 @ xs @ [x] = replicate (n + length (xs @ [x])) 0 proof (prove)
goal (1 subgoal):
 1. \<And>xs n. \<lbrakk>set xs \<subseteq> {0}; replicate n 0 @ xs = replicate (n + length xs) 0\<rbrakk> \<Longrightarrow> replicate n 0 @ xs @ [0] = 0 # replicate (n + length xs) 0 proof (prove)
goal (1 subgoal):
 1. \<And>xs n. \<lbrakk>set xs \<subseteq> {0}; replicate n 0 @ xs = replicate (n + length xs) 0\<rbrakk> \<Longrightarrow> (replicate n 0 @ xs) @ [0] = 0 # replicate (n + length xs) 0 proof (prove)
goal (1 subgoal):
 1. \<And>xs n. \<lbrakk>set xs \<subseteq> {0}; replicate n 0 @ xs = replicate (n + length xs) 0\<rbrakk> \<Longrightarrow> replicate (n + length xs) 0 @ [0] = 0 # replicate (n + length xs) 0 proof (prove)
goal (2 subgoals):
 1. \<And>xs n. \<lbrakk>set xs \<subseteq> {0}; replicate n 0 @ xs = replicate (n + length xs) 0; \<And>n. replicate n 0 @ [0] = 0 # replicate n 0\<rbrakk> \<Longrightarrow> replicate (n + length xs) 0 @ [0] = 0 # replicate (n + length xs) 0
 2. \<And>xs n na. \<lbrakk>set xs \<subseteq> {0}; replicate n 0 @ xs = replicate (n + length xs) 0\<rbrakk> \<Longrightarrow> replicate na 0 @ [0] = 0 # replicate na 0 proof (prove)
goal (1 subgoal):
 1. \<And>xs n na. \<lbrakk>set xs \<subseteq> {0}; replicate n 0 @ xs = replicate (n + length xs) 0\<rbrakk> \<Longrightarrow> replicate na 0 @ [0] = 0 # replicate na 0 proof (prove)
goal (2 subgoals):
 1. \<And>xs n na. \<lbrakk>set xs \<subseteq> {0}; replicate n 0 @ xs = replicate (n + length xs) 0\<rbrakk> \<Longrightarrow> replicate 0 0 @ [0] = 0 # replicate 0 0
 2. \<And>xs n na nb. \<lbrakk>set xs \<subseteq> {0}; replicate n 0 @ xs = replicate (n + length xs) 0; replicate nb 0 @ [0] = 0 # replicate nb 0\<rbrakk> \<Longrightarrow> replicate (Suc nb) 0 @ [0] = 0 # replicate (Suc nb) 0 proof (prove)
goal (1 subgoal):
 1. \<And>xs n na nb. \<lbrakk>set xs \<subseteq> {0}; replicate n 0 @ xs = replicate (n + length xs) 0; replicate nb 0 @ [0] = 0 # replicate nb 0\<rbrakk> \<Longrightarrow> replicate (Suc nb) 0 @ [0] = 0 # replicate (Suc nb) 0 proof (prove)
goal:
No subgoals!