[STATEMENT]
lemma fold_const_fa_Mult_eq_NumE:
  assumes "fold_const_fa (Mult a b) = Num x"
  obtains y z where "fold_const_fa a = Num y" "fold_const_fa b = Num z" "x = y * z"
  | y where "fold_const_fa a = Num 0" "x = 0"
  | y where "fold_const_fa b = Num 0" "x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>y z. \<lbrakk>fold_const_fa a = Num y; fold_const_fa b = Num z; x = y * z\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>fold_const_fa a = Num 0; x = 0\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>fold_const_fa b = Num 0; x = 0\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
fold_const_fa (Mult a b) = Num x

goal (1 subgoal):
 1. \<lbrakk>\<And>y z. \<lbrakk>fold_const_fa a = Num y; fold_const_fa b = Num z; x = y * z\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>fold_const_fa a = Num 0; x = 0\<rbrakk> \<Longrightarrow> thesis; \<lbrakk>fold_const_fa b = Num 0; x = 0\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim (auto simp: fold_const_fa.simps split!: option.splits if_splits
      elim!: dest_Num_fa_Some dest_Num_fa_None)


[STATEMENT]
lemma fold_const_fa_Add_eq_NumE:
  assumes "fold_const_fa (Add a b) = Num x"
  obtains y z where "fold_const_fa a = Num y" "fold_const_fa b = Num z" "x = y + z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y z. \<lbrakk>fold_const_fa a = Num y; fold_const_fa b = Num z; x = y + z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
fold_const_fa (Add a b) = Num x

goal (1 subgoal):
 1. (\<And>y z. \<lbrakk>fold_const_fa a = Num y; fold_const_fa b = Num z; x = y + z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by atomize_elim (auto simp: fold_const_fa.simps split!: option.splits if_splits
      elim!: dest_Num_fa_Some dest_Num_fa_None)