[STATEMENT]
lemma length_compTpExpr_Exprs [rule_format]: "
  (\<forall>sttp. (length (mt_of (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex)))
  \<and> (\<forall>sttp. (length (mt_of (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>sttp. length (fst (compTpExpr jmb G ex sttp)) = length (compExpr jmb ex)) \<and> (\<forall>sttp. length (fst (compTpExprs jmb G exs sttp)) = length (compExprs jmb exs))
[PROOF STEP]
apply (rule compat_expr_expr_list.induct)
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. \<And>x. \<forall>sttp. length (fst (compTpExpr jmb G (NewC x) sttp)) = length (compExpr jmb (NewC x))
 2. \<And>x1 x2. \<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2) \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (Cast x1 x2) sttp)) = length (compExpr jmb (Cast x1 x2))
 3. \<And>x. \<forall>sttp. length (fst (compTpExpr jmb G (Lit x) sttp)) = length (compExpr jmb (Lit x))
 4. \<And>x1 x2 x3. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExpr jmb G x3 sttp)) = length (compExpr jmb x3)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (BinOp x1 x2 x3) sttp)) = length (compExpr jmb (BinOp x1 x2 x3))
 5. \<And>x. \<forall>sttp. length (fst (compTpExpr jmb G (LAcc x) sttp)) = length (compExpr jmb (LAcc x))
 6. \<And>x1 x2. \<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2) \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (x1::=x2) sttp)) = length (compExpr jmb (x1::=x2))
 7. \<And>x1 x2 x3. \<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2) \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3) sttp)) = length (compExpr jmb ({x1}x2..x3))
 8. \<And>x1 x2 x3 x4. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExpr jmb G x4 sttp)) = length (compExpr jmb x4)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3:=x4) sttp)) = length (compExpr jmb ({x1}x2..x3:=x4))
 9. \<And>x1 x2 x3 x4 x5. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExprs jmb G x5 sttp)) = length (compExprs jmb x5)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3( {x4}x5)) sttp)) = length (compExpr jmb ({x1}x2..x3( {x4}x5)))
 10. \<forall>sttp. length (fst (compTpExprs jmb G [] sttp)) = length (compExprs jmb [])
A total of 11 subgoals...
[PROOF STEP]
apply (simp_all)[3]
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<And>x1 x2 x3. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExpr jmb G x3 sttp)) = length (compExpr jmb x3)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (BinOp x1 x2 x3) sttp)) = length (compExpr jmb (BinOp x1 x2 x3))
 2. \<And>x. \<forall>sttp. length (fst (compTpExpr jmb G (LAcc x) sttp)) = length (compExpr jmb (LAcc x))
 3. \<And>x1 x2. \<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2) \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (x1::=x2) sttp)) = length (compExpr jmb (x1::=x2))
 4. \<And>x1 x2 x3. \<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2) \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3) sttp)) = length (compExpr jmb ({x1}x2..x3))
 5. \<And>x1 x2 x3 x4. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExpr jmb G x4 sttp)) = length (compExpr jmb x4)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3:=x4) sttp)) = length (compExpr jmb ({x1}x2..x3:=x4))
 6. \<And>x1 x2 x3 x4 x5. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExprs jmb G x5 sttp)) = length (compExprs jmb x5)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3( {x4}x5)) sttp)) = length (compExpr jmb ({x1}x2..x3( {x4}x5)))
 7. \<forall>sttp. length (fst (compTpExprs jmb G [] sttp)) = length (compExprs jmb [])
 8. \<And>x1 x2. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x1 sttp)) = length (compExpr jmb x1); \<forall>sttp. length (fst (compTpExprs jmb G x2 sttp)) = length (compExprs jmb x2)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExprs jmb G (x1 # x2) sttp)) = length (compExprs jmb (x1 # x2))
[PROOF STEP]
apply (rename_tac binop a b, case_tac binop)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>binop a b. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G a sttp)) = length (compExpr jmb a); \<forall>sttp. length (fst (compTpExpr jmb G b sttp)) = length (compExpr jmb b); binop = Eq\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (BinOp binop a b) sttp)) = length (compExpr jmb (BinOp binop a b))
 2. \<And>binop a b. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G a sttp)) = length (compExpr jmb a); \<forall>sttp. length (fst (compTpExpr jmb G b sttp)) = length (compExpr jmb b); binop = Add\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (BinOp binop a b) sttp)) = length (compExpr jmb (BinOp binop a b))
 3. \<And>x. \<forall>sttp. length (fst (compTpExpr jmb G (LAcc x) sttp)) = length (compExpr jmb (LAcc x))
 4. \<And>x1 x2. \<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2) \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G (x1::=x2) sttp)) = length (compExpr jmb (x1::=x2))
 5. \<And>x1 x2 x3. \<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2) \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3) sttp)) = length (compExpr jmb ({x1}x2..x3))
 6. \<And>x1 x2 x3 x4. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExpr jmb G x4 sttp)) = length (compExpr jmb x4)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3:=x4) sttp)) = length (compExpr jmb ({x1}x2..x3:=x4))
 7. \<And>x1 x2 x3 x4 x5. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x2 sttp)) = length (compExpr jmb x2); \<forall>sttp. length (fst (compTpExprs jmb G x5 sttp)) = length (compExprs jmb x5)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExpr jmb G ({x1}x2..x3( {x4}x5)) sttp)) = length (compExpr jmb ({x1}x2..x3( {x4}x5)))
 8. \<forall>sttp. length (fst (compTpExprs jmb G [] sttp)) = length (compExprs jmb [])
 9. \<And>x1 x2. \<lbrakk>\<forall>sttp. length (fst (compTpExpr jmb G x1 sttp)) = length (compExpr jmb x1); \<forall>sttp. length (fst (compTpExprs jmb G x2 sttp)) = length (compExprs jmb x2)\<rbrakk> \<Longrightarrow> \<forall>sttp. length (fst (compTpExprs jmb G (x1 # x2) sttp)) = length (compExprs jmb (x1 # x2))
[PROOF STEP]
apply (auto simp add: pushST_def split_beta)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done