[STATEMENT]
lemma mult_aform'E:
  fixes X Y::"aform_err"
  assumes e: "e \<in> UNIV \<rightarrow> {- 1..1}"
  assumes x: "x \<in> aform_err e X"
  assumes y: "y \<in> aform_err e Y"
  shows "x * y \<in> aform_err e (mult_aform' p X Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
let ?z0 = "trunc_bound_eucl p (fst (fst X) * fst (fst Y))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
from trunc_bound_euclE
[PROOF STATE]
proof (chain)
picking this:
(\<And>err. \<lbrakk>\<bar>err\<bar> \<le> snd (trunc_bound_eucl ?p ?x); fst (trunc_bound_eucl ?p ?x) = ?x + err\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain e1 where abs_e1: "\<bar>e1\<bar> \<le> snd ?z0" and e1: "fst ?z0 = fst (fst X) * fst (fst Y) + e1"
[PROOF STATE]
proof (prove)
using this:
(\<And>err. \<lbrakk>\<bar>err\<bar> \<le> snd (trunc_bound_eucl ?p ?x); fst (trunc_bound_eucl ?p ?x) = ?x + err\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>e1. \<lbrakk>\<bar>e1\<bar> \<le> snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))); fst (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) = fst (fst X) * fst (fst Y) + e1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<bar>e1\<bar> \<le> snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y)))
fst (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) = fst (fst X) * fst (fst Y) + e1

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
let ?u = "trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
from trunc_bound_pdevsE[OF e]
[PROOF STATE]
proof (chain)
picking this:
(\<And>err. \<lbrakk>\<bar>err\<bar> \<le> snd (trunc_bound_pdevs ?p ?x); pdevs_val e (fst (trunc_bound_pdevs ?p ?x)) = pdevs_val e ?x + err\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain e2 where abs_e2: "\<bar>e2\<bar> \<le> snd (?u)"
    and e2: "pdevs_val e (fst ?u) = pdevs_val e (scaleR_pdevs (fst (fst Y)) (snd (fst X))) + e2"
[PROOF STATE]
proof (prove)
using this:
(\<And>err. \<lbrakk>\<bar>err\<bar> \<le> snd (trunc_bound_pdevs ?p ?x); pdevs_val e (fst (trunc_bound_pdevs ?p ?x)) = pdevs_val e ?x + err\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>e2. \<lbrakk>\<bar>e2\<bar> \<le> snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))); pdevs_val e (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) = pdevs_val e (scaleR_pdevs (fst (fst Y)) (snd (fst X))) + e2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<bar>e2\<bar> \<le> snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))
pdevs_val e (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) = pdevs_val e (scaleR_pdevs (fst (fst Y)) (snd (fst X))) + e2

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
let ?v = "trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
from trunc_bound_pdevsE[OF e]
[PROOF STATE]
proof (chain)
picking this:
(\<And>err. \<lbrakk>\<bar>err\<bar> \<le> snd (trunc_bound_pdevs ?p ?x); pdevs_val e (fst (trunc_bound_pdevs ?p ?x)) = pdevs_val e ?x + err\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain e3 where abs_e3: "\<bar>e3\<bar> \<le> snd (?v)"
    and e3: "pdevs_val e (fst ?v) = pdevs_val e (scaleR_pdevs (fst (fst X)) (snd (fst Y))) + e3"
[PROOF STATE]
proof (prove)
using this:
(\<And>err. \<lbrakk>\<bar>err\<bar> \<le> snd (trunc_bound_pdevs ?p ?x); pdevs_val e (fst (trunc_bound_pdevs ?p ?x)) = pdevs_val e ?x + err\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>e3. \<lbrakk>\<bar>e3\<bar> \<le> snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))); pdevs_val e (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y))))) = pdevs_val e (scaleR_pdevs (fst (fst X)) (snd (fst Y))) + e3\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<bar>e3\<bar> \<le> snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y))))
pdevs_val e (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y))))) = pdevs_val e (scaleR_pdevs (fst (fst X)) (snd (fst Y))) + e3

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
let ?w = "trunc_bound_pdevs p (add_pdevs (fst ?u) (fst ?v))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
from trunc_bound_pdevsE[OF e]
[PROOF STATE]
proof (chain)
picking this:
(\<And>err. \<lbrakk>\<bar>err\<bar> \<le> snd (trunc_bound_pdevs ?p ?x); pdevs_val e (fst (trunc_bound_pdevs ?p ?x)) = pdevs_val e ?x + err\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain e4 where abs_e4: "\<bar>e4\<bar> \<le> snd (?w)"
    and e4: "pdevs_val e (fst ?w) = pdevs_val e (add_pdevs (fst ?u) (fst ?v)) + e4"
[PROOF STATE]
proof (prove)
using this:
(\<And>err. \<lbrakk>\<bar>err\<bar> \<le> snd (trunc_bound_pdevs ?p ?x); pdevs_val e (fst (trunc_bound_pdevs ?p ?x)) = pdevs_val e ?x + err\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>e4. \<lbrakk>\<bar>e4\<bar> \<le> snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y))))))); pdevs_val e (fst (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))) = pdevs_val e (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))) + e4\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<bar>e4\<bar> \<le> snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))
pdevs_val e (fst (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))) = pdevs_val e (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))) + e4

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
let ?tx = "tdev' p (snd (fst X))" and ?ty = "tdev' p (snd (fst Y))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
let ?l = "truncate_up p (?tx * ?ty)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
let ?ee = "truncate_up p (abs (snd X) * abs (snd Y))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
let ?e1 = "truncate_up p (abs (snd X) * truncate_up p (\<bar>fst (fst Y)\<bar> + ?ty))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
let ?e2 = "truncate_up p (abs (snd Y) * truncate_up p (\<bar>fst (fst X)\<bar> + ?tx))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
let ?e0 = "x * y - fst (fst X) * fst (fst Y) -
      fst (fst X) * pdevs_val e (snd (fst Y)) -
      fst (fst Y) * pdevs_val e (snd (fst X))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
let ?err = "?e0 - (e1 + e2  + e3 + e4)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
have "abs ?err \<le> abs ?e0 + abs e1 + abs e2 + abs e3 + abs e4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X)) - (e1 + e2 + e3 + e4)\<bar> \<le> \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> + \<bar>e1\<bar> + \<bar>e2\<bar> + \<bar>e3\<bar> + \<bar>e4\<bar>
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X)) - (e1 + e2 + e3 + e4)\<bar> \<le> \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> + \<bar>e1\<bar> + \<bar>e2\<bar> + \<bar>e3\<bar> + \<bar>e4\<bar>

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X)) - (e1 + e2 + e3 + e4)\<bar> \<le> \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> + \<bar>e1\<bar> + \<bar>e2\<bar> + \<bar>e3\<bar> + \<bar>e4\<bar>

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
have "\<dots> \<le> abs ?e0 + snd ?z0 + snd ?u + snd ?v + snd ?w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> + \<bar>e1\<bar> + \<bar>e2\<bar> + \<bar>e3\<bar> + \<bar>e4\<bar> \<le> \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))
[PROOF STEP]
unfolding abs_mult
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> + \<bar>e1\<bar> + \<bar>e2\<bar> + \<bar>e3\<bar> + \<bar>e4\<bar> \<le> \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))
[PROOF STEP]
by (auto intro!: add_mono mult_mono e abs_pdevs_val_le_tdev' abs_ge_zero abs_e1 abs_e2 abs_e3
      abs_e4 intro: tdev'_le)
[PROOF STATE]
proof (state)
this:
\<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> + \<bar>e1\<bar> + \<bar>e2\<bar> + \<bar>e3\<bar> + \<bar>e4\<bar> \<le> \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> + \<bar>e1\<bar> + \<bar>e2\<bar> + \<bar>e3\<bar> + \<bar>e4\<bar> \<le> \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
have asdf: "snd (mult_aform X Y) \<le> tdev' p (snd (fst X)) * tdev' p (snd (fst Y)) + ?e1 + ?e2 + ?ee"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (mult_aform X Y) \<le> Radius' p (fst X) * Radius' p (fst Y) + truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))) + truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))) + truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>)
[PROOF STEP]
by (auto simp: mult_aform_def intro!: add_mono mult_mono order_trans[OF _ tdev'] truncate_up_le)
[PROOF STATE]
proof (state)
this:
snd (mult_aform X Y) \<le> Radius' p (fst X) * Radius' p (fst Y) + truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))) + truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))) + truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>)

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
have "abs ?e0 \<le> ?ee + ?e1 + ?e2 + tdev' p (snd (fst X)) * tdev' p (snd (fst Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> \<le> truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>) + truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))) + truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))) + Radius' p (fst X) * Radius' p (fst Y)
[PROOF STEP]
using mult_aformE[OF e x y, THEN aform_errE, THEN order_trans, OF asdf]
[PROOF STATE]
proof (prove)
using this:
\<bar>x * y - aform_val e (fst (mult_aform X Y))\<bar> \<le> Radius' p (fst X) * Radius' p (fst Y) + truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))) + truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))) + truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>)

goal (1 subgoal):
 1. \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> \<le> truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>) + truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))) + truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))) + Radius' p (fst X) * Radius' p (fst Y)
[PROOF STEP]
by (simp add: aform_val_def mult_aform_def) arith
[PROOF STATE]
proof (state)
this:
\<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> \<le> truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>) + truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))) + truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))) + Radius' p (fst X) * Radius' p (fst Y)

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X))\<bar> \<le> truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>) + truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))) + truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))) + Radius' p (fst X) * Radius' p (fst Y)

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
have "tdev' p (snd (fst X)) * tdev' p (snd (fst Y)) \<le> ?l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Radius' p (fst X) * Radius' p (fst Y) \<le> truncate_up p (Radius' p (fst X) * Radius' p (fst Y))
[PROOF STEP]
by (auto intro!: truncate_up_le)
[PROOF STATE]
proof (state)
this:
Radius' p (fst X) * Radius' p (fst Y) \<le> truncate_up p (Radius' p (fst X) * Radius' p (fst Y))

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Radius' p (fst X) * Radius' p (fst Y) \<le> truncate_up p (Radius' p (fst X) * Radius' p (fst Y))

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
have "?ee + ?e1 + ?e2 + ?l + snd ?z0 + snd ?u + snd ?v + snd ?w \<le>
      sum_list' p [?ee, ?e1, ?e2, ?l, snd ?z0, snd ?u, snd ?v, snd ?w]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>) + truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))) + truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))) + truncate_up p (Radius' p (fst X) * Radius' p (fst Y)) + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y))))))) \<le> sum_list' p [truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>), truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))), truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))), truncate_up p (Radius' p (fst X) * Radius' p (fst Y)), snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))), snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))), snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))), snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))]
[PROOF STEP]
by (rule order_trans[OF _ sum_list_le_sum_list']) simp
[PROOF STATE]
proof (state)
this:
truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>) + truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))) + truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))) + truncate_up p (Radius' p (fst X) * Radius' p (fst Y)) + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y))))))) \<le> sum_list' p [truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>), truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))), truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))), truncate_up p (Radius' p (fst X) * Radius' p (fst Y)), snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))), snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))), snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))), snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))]

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>) + truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))) + truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))) + truncate_up p (Radius' p (fst X) * Radius' p (fst Y)) + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y))))))) \<le> sum_list' p [truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>), truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))), truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))), truncate_up p (Radius' p (fst X) * Radius' p (fst Y)), snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))), snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))), snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))), snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))]

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
have "\<dots> \<le> (snd (mult_aform' p X Y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list' p [truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>), truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))), truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))), truncate_up p (Radius' p (fst X) * Radius' p (fst Y)), snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))), snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))), snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))), snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))] \<le> snd (mult_aform' p X Y)
[PROOF STEP]
by (auto simp: mult_aform'_def Let_def assms split: prod.splits)
[PROOF STATE]
proof (state)
this:
sum_list' p [truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>), truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))), truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))), truncate_up p (Radius' p (fst X) * Radius' p (fst Y)), snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))), snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))), snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))), snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))] \<le> snd (mult_aform' p X Y)

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> x + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y))))))) \<le> y + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y))))))); \<And>x y. x \<le> y \<Longrightarrow> truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>) + truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))) + truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))) + x + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y))))))) \<le> truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>) + truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))) + truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))) + y + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))\<rbrakk> \<Longrightarrow> \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X)) - (e1 + e2 + e3 + e4)\<bar> \<le> snd (mult_aform' p X Y)
[PROOF STEP]
have err_le: "abs ?err \<le> (snd (mult_aform' p X Y))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> x + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y))))))) \<le> y + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y))))))); \<And>x y. x \<le> y \<Longrightarrow> truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>) + truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))) + truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))) + x + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y))))))) \<le> truncate_up p (\<bar>snd X\<bar> * \<bar>snd Y\<bar>) + truncate_up p (\<bar>snd X\<bar> * truncate_up p (\<bar>fst (fst Y)\<bar> + Radius' p (fst Y))) + truncate_up p (\<bar>snd Y\<bar> * truncate_up p (\<bar>fst (fst X)\<bar> + Radius' p (fst X))) + y + snd (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X)))) + snd (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))) + snd (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))\<rbrakk> \<Longrightarrow> \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X)) - (e1 + e2 + e3 + e4)\<bar> \<le> snd (mult_aform' p X Y)

goal (1 subgoal):
 1. \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X)) - (e1 + e2 + e3 + e4)\<bar> \<le> snd (mult_aform' p X Y)
[PROOF STEP]
by arith
[PROOF STATE]
proof (state)
this:
\<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X)) - (e1 + e2 + e3 + e4)\<bar> \<le> snd (mult_aform' p X Y)

goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * y \<in> aform_err e (mult_aform' p X Y)
[PROOF STEP]
apply (rule aform_errI[OF order_trans[OF _ err_le]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x * y - aform_val e (fst (mult_aform' p X Y))\<bar> \<le> \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X)) - (e1 + e2 + e3 + e4)\<bar>
[PROOF STEP]
apply (subst mult_aform'_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<bar>x * y - aform_val e (fst (let (fx, sx) = X; (fy, sy) = Y; ex = \<bar>sx\<bar>; ey = \<bar>sy\<bar>; z0 = trunc_bound_eucl p (fst fx * fst fy); u = trunc_bound_pdevs p (scaleR_pdevs (fst fy) (snd fx)); v = trunc_bound_pdevs p (scaleR_pdevs (fst fx) (snd fy)); w = trunc_bound_pdevs p (add_pdevs (fst u) (fst v)); tx = Radius' p fx; ty = Radius' p fy; l = truncate_up p (tx * ty); ee = truncate_up p (ex * ey); e1 = truncate_up p (ex * truncate_up p (\<bar>fst fy\<bar> + ty)); e2 = truncate_up p (ey * truncate_up p (\<bar>fst fx\<bar> + tx)) in ((fst z0, fst w), sum_list' p [ee, e1, e2, l, snd z0, snd u, snd v, snd w])))\<bar> \<le> \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X)) - (e1 + e2 + e3 + e4)\<bar>
[PROOF STEP]
using e1 e2 e3 e4
[PROOF STATE]
proof (prove)
using this:
fst (trunc_bound_eucl p (fst (fst X) * fst (fst Y))) = fst (fst X) * fst (fst Y) + e1
pdevs_val e (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) = pdevs_val e (scaleR_pdevs (fst (fst Y)) (snd (fst X))) + e2
pdevs_val e (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y))))) = pdevs_val e (scaleR_pdevs (fst (fst X)) (snd (fst Y))) + e3
pdevs_val e (fst (trunc_bound_pdevs p (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))))) = pdevs_val e (add_pdevs (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst Y)) (snd (fst X))))) (fst (trunc_bound_pdevs p (scaleR_pdevs (fst (fst X)) (snd (fst Y)))))) + e4

goal (1 subgoal):
 1. \<bar>x * y - aform_val e (fst (let (fx, sx) = X; (fy, sy) = Y; ex = \<bar>sx\<bar>; ey = \<bar>sy\<bar>; z0 = trunc_bound_eucl p (fst fx * fst fy); u = trunc_bound_pdevs p (scaleR_pdevs (fst fy) (snd fx)); v = trunc_bound_pdevs p (scaleR_pdevs (fst fx) (snd fy)); w = trunc_bound_pdevs p (add_pdevs (fst u) (fst v)); tx = Radius' p fx; ty = Radius' p fy; l = truncate_up p (tx * ty); ee = truncate_up p (ex * ey); e1 = truncate_up p (ex * truncate_up p (\<bar>fst fy\<bar> + ty)); e2 = truncate_up p (ey * truncate_up p (\<bar>fst fx\<bar> + tx)) in ((fst z0, fst w), sum_list' p [ee, e1, e2, l, snd z0, snd u, snd v, snd w])))\<bar> \<le> \<bar>x * y - fst (fst X) * fst (fst Y) - fst (fst X) * pdevs_val e (snd (fst Y)) - fst (fst Y) * pdevs_val e (snd (fst X)) - (e1 + e2 + e3 + e4)\<bar>
[PROOF STEP]
apply (auto simp: aform_val_def Let_def assms split: prod.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
x * y \<in> aform_err e (mult_aform' p X Y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ordinal_mod_self [simp]: "x mod x = (0::ordinal)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x mod x = 0
[PROOF STEP]
apply (case_tac "x=0", simp add: ordinal_mod_0, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x \<Longrightarrow> x mod x = 0
[PROOF STEP]
apply (rule_tac q=1 in ordinal_modI, simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma cindex_combine:
  assumes finite:"finite {x. jump f x\<noteq>0 \<and> a<x \<and> x<c}" and "a<b" "b<c"
  shows "cindex a c f = cindex a b f  + jump f b + cindex b c f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindex a c f = cindex a b f + jump f b + cindex b c f
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cindex a c f = cindex a b f + jump f b + cindex b c f
[PROOF STEP]
define ssum where "ssum = (\<lambda>s. sum (jump f) ({x. jump f x\<noteq>0 \<and> a<x \<and> x<c} \<inter> s))"
[PROOF STATE]
proof (state)
this:
ssum = (\<lambda>s. sum (jump f) ({x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} \<inter> s))

goal (1 subgoal):
 1. cindex a c f = cindex a b f + jump f b + cindex b c f
[PROOF STEP]
have ssum_union:"ssum (A \<union> B) = ssum A + ssum B" when "A \<inter> B ={}" for A B
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ssum (A \<union> B) = ssum A + ssum B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ssum (A \<union> B) = ssum A + ssum B
[PROOF STEP]
define C where "C={x. jump f x \<noteq> 0 \<and> a<x \<and> x<c}"
[PROOF STATE]
proof (state)
this:
C = {x. jump f x \<noteq> 0 \<and> a < x \<and> x < c}

goal (1 subgoal):
 1. ssum (A \<union> B) = ssum A + ssum B
[PROOF STEP]
have "finite C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite C
[PROOF STEP]
using finite
[PROOF STATE]
proof (prove)
using this:
finite {x. jump f x \<noteq> 0 \<and> a < x \<and> x < c}

goal (1 subgoal):
 1. finite C
[PROOF STEP]
unfolding C_def
[PROOF STATE]
proof (prove)
using this:
finite {x. jump f x \<noteq> 0 \<and> a < x \<and> x < c}

goal (1 subgoal):
 1. finite {x. jump f x \<noteq> 0 \<and> a < x \<and> x < c}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
finite C

goal (1 subgoal):
 1. ssum (A \<union> B) = ssum A + ssum B
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite C

goal (1 subgoal):
 1. ssum (A \<union> B) = ssum A + ssum B
[PROOF STEP]
unfolding ssum_def
[PROOF STATE]
proof (prove)
using this:
finite C

goal (1 subgoal):
 1. sum (jump f) ({x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} \<inter> (A \<union> B)) = sum (jump f) ({x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} \<inter> A) + sum (jump f) ({x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} \<inter> B)
[PROOF STEP]
apply (fold C_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite C \<Longrightarrow> sum (jump f) (C \<inter> (A \<union> B)) = sum (jump f) (C \<inter> A) + sum (jump f) (C \<inter> B)
[PROOF STEP]
using sum_Un[of "C \<inter> A" "C \<inter> B"] that
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite (C \<inter> A); finite (C \<inter> B)\<rbrakk> \<Longrightarrow> sum ?f (C \<inter> A \<union> C \<inter> B) = sum ?f (C \<inter> A) + sum ?f (C \<inter> B) - sum ?f (C \<inter> A \<inter> (C \<inter> B))
A \<inter> B = {}

goal (1 subgoal):
 1. finite C \<Longrightarrow> sum (jump f) (C \<inter> (A \<union> B)) = sum (jump f) (C \<inter> A) + sum (jump f) (C \<inter> B)
[PROOF STEP]
by (simp add: inf_assoc inf_sup_aci(3) inf_sup_distrib1 sum.union_disjoint)
[PROOF STATE]
proof (state)
this:
ssum (A \<union> B) = ssum A + ssum B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?A \<inter> ?B = {} \<Longrightarrow> ssum (?A \<union> ?B) = ssum ?A + ssum ?B

goal (1 subgoal):
 1. cindex a c f = cindex a b f + jump f b + cindex b c f
[PROOF STEP]
have "cindex a c f = ssum ({a<..<b} \<union> {b} \<union> {b<..<c})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindex a c f = ssum ({a<..<b} \<union> {b} \<union> {b<..<c})
[PROOF STEP]
unfolding ssum_def cindex_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (jump f) {x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} = sum (jump f) ({x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} \<inter> ({a<..<b} \<union> {b} \<union> {b<..<c}))
[PROOF STEP]
apply (rule sum.cong[of _ _ "jump f" "jump f",simplified])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} = {x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} \<inter> ({a<..<b} \<union> {b} \<union> {b<..<c})
[PROOF STEP]
using \<open>a<b\<close> \<open>b<c\<close>
[PROOF STATE]
proof (prove)
using this:
a < b
b < c

goal (1 subgoal):
 1. {x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} = {x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} \<inter> ({a<..<b} \<union> {b} \<union> {b<..<c})
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
cindex a c f = ssum ({a<..<b} \<union> {b} \<union> {b<..<c})

goal (1 subgoal):
 1. cindex a c f = cindex a b f + jump f b + cindex b c f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cindex a c f = ssum ({a<..<b} \<union> {b} \<union> {b<..<c})

goal (1 subgoal):
 1. cindex a c f = cindex a b f + jump f b + cindex b c f
[PROOF STEP]
have "cindex a b f = ssum {a<..<b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindex a b f = ssum {a<..<b}
[PROOF STEP]
unfolding cindex_def ssum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (jump f) {x. jump f x \<noteq> 0 \<and> a < x \<and> x < b} = sum (jump f) ({x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} \<inter> {a<..<b})
[PROOF STEP]
using \<open>a<b\<close> \<open>b<c\<close>
[PROOF STATE]
proof (prove)
using this:
a < b
b < c

goal (1 subgoal):
 1. sum (jump f) {x. jump f x \<noteq> 0 \<and> a < x \<and> x < b} = sum (jump f) ({x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} \<inter> {a<..<b})
[PROOF STEP]
by (intro sum.cong,auto)
[PROOF STATE]
proof (state)
this:
cindex a b f = ssum {a<..<b}

goal (1 subgoal):
 1. cindex a c f = cindex a b f + jump f b + cindex b c f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
cindex a b f = ssum {a<..<b}

goal (1 subgoal):
 1. cindex a c f = cindex a b f + jump f b + cindex b c f
[PROOF STEP]
have "jump f b = ssum {b}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. jump f b = ssum {b}
[PROOF STEP]
unfolding ssum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. jump f b = sum (jump f) ({x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} \<inter> {b})
[PROOF STEP]
using \<open>a<b\<close> \<open>b<c\<close>
[PROOF STATE]
proof (prove)
using this:
a < b
b < c

goal (1 subgoal):
 1. jump f b = sum (jump f) ({x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} \<inter> {b})
[PROOF STEP]
by (cases "jump f b=0",auto)
[PROOF STATE]
proof (state)
this:
jump f b = ssum {b}

goal (1 subgoal):
 1. cindex a c f = cindex a b f + jump f b + cindex b c f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
jump f b = ssum {b}

goal (1 subgoal):
 1. cindex a c f = cindex a b f + jump f b + cindex b c f
[PROOF STEP]
have "cindex b c f = ssum {b<..<c}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cindex b c f = ssum {b<..<c}
[PROOF STEP]
unfolding cindex_def ssum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (jump f) {x. jump f x \<noteq> 0 \<and> b < x \<and> x < c} = sum (jump f) ({x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} \<inter> {b<..<c})
[PROOF STEP]
using \<open>a<b\<close> \<open>b<c\<close>
[PROOF STATE]
proof (prove)
using this:
a < b
b < c

goal (1 subgoal):
 1. sum (jump f) {x. jump f x \<noteq> 0 \<and> b < x \<and> x < c} = sum (jump f) ({x. jump f x \<noteq> 0 \<and> a < x \<and> x < c} \<inter> {b<..<c})
[PROOF STEP]
by (intro sum.cong,auto)
[PROOF STATE]
proof (state)
this:
cindex b c f = ssum {b<..<c}

goal (1 subgoal):
 1. cindex a c f = cindex a b f + jump f b + cindex b c f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
cindex a c f = ssum ({a<..<b} \<union> {b} \<union> {b<..<c})
cindex a b f = ssum {a<..<b}
jump f b = ssum {b}
cindex b c f = ssum {b<..<c}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cindex a c f = ssum ({a<..<b} \<union> {b} \<union> {b<..<c})
cindex a b f = ssum {a<..<b}
jump f b = ssum {b}
cindex b c f = ssum {b<..<c}

goal (1 subgoal):
 1. cindex a c f = cindex a b f + jump f b + cindex b c f
[PROOF STEP]
apply (subst (asm) ssum_union,simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cindex a c f = ssum ({a<..<b} \<union> {b}) + ssum {b<..<c}; cindex a b f = ssum {a<..<b}; jump f b = ssum {b}; cindex b c f = ssum {b<..<c}\<rbrakk> \<Longrightarrow> cindex a c f = cindex a b f + jump f b + cindex b c f
[PROOF STEP]
by (subst (asm) ssum_union,auto)
[PROOF STATE]
proof (state)
this:
cindex a c f = cindex a b f + jump f b + cindex b c f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma chosen_adjoint_equivalence:
    assumes "C.obj a"
    shows "adjoint_equivalence_in_bicategory V\<^sub>D H\<^sub>D \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) (\<tau>\<^sub>0' a) (\<eta> a) (\<epsilon> a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) (map\<^sub>0 a) (unit a) (counit a)
[PROOF STEP]
using assms \<tau>.components_are_equivalences map\<^sub>0_def unit_def counit_def
            D.obj_is_equivalence_map D.equivalence_map_extends_to_adjoint_equivalence
            someI_ex [of "\<lambda>g. \<exists>\<eta> \<epsilon>. adjoint_equivalence_in_bicategory
                                      V\<^sub>D H\<^sub>D \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) g \<eta> \<epsilon>"]
            someI_ex [of "\<lambda>\<eta>. \<exists>\<epsilon>. adjoint_equivalence_in_bicategory
                                    V\<^sub>D H\<^sub>D \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) (\<tau>\<^sub>0' a) \<eta> \<epsilon>"]
            someI_ex [of "\<lambda>\<epsilon>. adjoint_equivalence_in_bicategory
                                    V\<^sub>D H\<^sub>D \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) (\<tau>\<^sub>0' a) (\<eta> a) \<epsilon>"]
[PROOF STATE]
proof (prove)
using this:
C.obj a
C.obj ?a \<Longrightarrow> D.equivalence_map (\<tau>\<^sub>0 ?a)
map\<^sub>0 ?a = (SOME g. \<exists>\<eta> \<epsilon>. adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 ?a) g \<eta> \<epsilon>)
unit ?a = (SOME \<eta>. \<exists>\<epsilon>. adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 ?a) (map\<^sub>0 ?a) \<eta> \<epsilon>)
counit ?a = (SOME \<epsilon>. adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 ?a) (map\<^sub>0 ?a) (unit ?a) \<epsilon>)
D.obj ?a \<Longrightarrow> D.equivalence_map ?a
D.equivalence_map ?f \<Longrightarrow> \<exists>g \<eta> \<epsilon>. adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D ?f g \<eta> \<epsilon>
\<exists>x \<eta> \<epsilon>. adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) x \<eta> \<epsilon> \<Longrightarrow> \<exists>\<eta> \<epsilon>. adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) (SOME x. \<exists>\<eta> \<epsilon>. adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) x \<eta> \<epsilon>) \<eta> \<epsilon>
\<exists>x \<epsilon>. adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) (map\<^sub>0 a) x \<epsilon> \<Longrightarrow> \<exists>\<epsilon>. adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) (map\<^sub>0 a) (SOME x. \<exists>\<epsilon>. adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) (map\<^sub>0 a) x \<epsilon>) \<epsilon>
\<exists>x. adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) (map\<^sub>0 a) (unit a) x \<Longrightarrow> adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) (map\<^sub>0 a) (unit a) (SOME x. adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) (map\<^sub>0 a) (unit a) x)

goal (1 subgoal):
 1. adjoint_equivalence_in_bicategory (\<cdot>\<^sub>D) (\<star>\<^sub>D) \<a>\<^sub>D \<i>\<^sub>D src\<^sub>D trg\<^sub>D (\<tau>\<^sub>0 a) (map\<^sub>0 a) (unit a) (counit a)
[PROOF STEP]
by simp


[STATEMENT]
lemma learn_fin_wrt_goedel:
  assumes "goedel_numbering \<chi>" and "learn_fin \<psi> U s"
  shows "\<exists>t. learn_fin \<chi> U t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>t. learn_fin \<chi> U t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>t. learn_fin \<chi> U t
[PROOF STEP]
have env: "environment \<psi> U s"
    and fin: "\<And>f. f \<in> U \<Longrightarrow>
      \<exists>i n\<^sub>0. \<psi> i = f \<and> (\<forall>n<n\<^sub>0. s (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. s (f \<triangleright> n) \<down>= Suc i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. environment \<psi> U s &&& (\<And>f. f \<in> U \<Longrightarrow> \<exists>i n\<^sub>0. \<psi> i = f \<and> (\<forall>n<n\<^sub>0. s (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. s (f \<triangleright> n) \<down>= Suc i))
[PROOF STEP]
using assms(2) learn_finE
[PROOF STATE]
proof (prove)
using this:
learn_fin \<psi> U s
learn_fin ?\<psi> ?U ?s \<Longrightarrow> environment ?\<psi> ?U ?s
\<lbrakk>learn_fin ?\<psi> ?U ?s; ?f \<in> ?U\<rbrakk> \<Longrightarrow> \<exists>i n\<^sub>0. ?\<psi> i = ?f \<and> (\<forall>n<n\<^sub>0. ?s (?f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. ?s (?f \<triangleright> n) \<down>= Suc i)

goal (1 subgoal):
 1. environment \<psi> U s &&& (\<And>f. f \<in> U \<Longrightarrow> \<exists>i n\<^sub>0. \<psi> i = f \<and> (\<forall>n<n\<^sub>0. s (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. s (f \<triangleright> n) \<down>= Suc i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
environment \<psi> U s
?f \<in> U \<Longrightarrow> \<exists>i n\<^sub>0. \<psi> i = ?f \<and> (\<forall>n<n\<^sub>0. s (?f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. s (?f \<triangleright> n) \<down>= Suc i)

goal (1 subgoal):
 1. \<exists>t. learn_fin \<chi> U t
[PROOF STEP]
obtain c where c: "c \<in> \<R>" "\<forall>i. \<psi> i = \<chi> (the (c i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in> \<R>; \<forall>i. \<psi> i = \<chi> (the (c i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using env goedel_numberingE[OF assms(1), of \<psi>]
[PROOF STATE]
proof (prove)
using this:
environment \<psi> U s
\<lbrakk>\<psi> \<in> \
\<^sup>2; \<And>c. \<lbrakk>c \<in> \<R>; \<forall>i. \<psi> i = \<chi> (the (c i))\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<in> \<R>; \<forall>i. \<psi> i = \<chi> (the (c i))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
c \<in> \<R>
\<forall>i. \<psi> i = \<chi> (the (c i))

goal (1 subgoal):
 1. \<exists>t. learn_fin \<chi> U t
[PROOF STEP]
define t where "t \<equiv>
    \<lambda>x. if s x \<up> then None
         else if s x = Some 0 then Some 0
              else Some (Suc (the (c (the (s x) - 1))))"
[PROOF STATE]
proof (state)
this:
t \<equiv> \<lambda>x. if s x \<up> then None else if s x \<down>= 0 then Some 0 else Some (Suc (the (c (the (s x) - 1))))

goal (1 subgoal):
 1. \<exists>t. learn_fin \<chi> U t
[PROOF STEP]
have "t \<in> \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
from c
[PROOF STATE]
proof (chain)
picking this:
c \<in> \<R>
\<forall>i. \<psi> i = \<chi> (the (c i))
[PROOF STEP]
obtain rc where rc:
      "recfn 1 rc"
      "total rc"
      "\<forall>x. c x = eval rc [x]"
[PROOF STATE]
proof (prove)
using this:
c \<in> \<R>
\<forall>i. \<psi> i = \<chi> (the (c i))

goal (1 subgoal):
 1. (\<And>rc. \<lbrakk>recfn 1 rc; Partial_Recursive.total rc; \<forall>x. c x = eval rc [x]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
recfn 1 rc
Partial_Recursive.total rc
\<forall>x. c x = eval rc [x]

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
from env
[PROOF STATE]
proof (chain)
picking this:
environment \<psi> U s
[PROOF STEP]
obtain rs where rs: "recfn 1 rs" "\<forall>x. s x = eval rs [x]"
[PROOF STATE]
proof (prove)
using this:
environment \<psi> U s

goal (1 subgoal):
 1. (\<And>rs. \<lbrakk>recfn 1 rs; \<forall>x. s x = eval rs [x]\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
recfn 1 rs
\<forall>x. s x = eval rs [x]

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
recfn 1 rs
\<forall>x. s x = eval rs [x]
[PROOF STEP]
have "eval rs [f \<triangleright> n] \<down>" if "f \<in> U" for f n
[PROOF STATE]
proof (prove)
using this:
recfn 1 rs
\<forall>x. s x = eval rs [x]

goal (1 subgoal):
 1. eval rs [f \<triangleright> n] \<down>
[PROOF STEP]
using env that
[PROOF STATE]
proof (prove)
using this:
recfn 1 rs
\<forall>x. s x = eval rs [x]
environment \<psi> U s
f \<in> U

goal (1 subgoal):
 1. eval rs [f \<triangleright> n] \<down>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?f \<in> U \<Longrightarrow> eval rs [?f \<triangleright> ?n] \<down>

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
define rt where "rt = Cn 1 r_ifz [rs, Z, Cn 1 S [Cn 1 rc [Cn 1 r_dec [rs]]]]"
[PROOF STATE]
proof (state)
this:
rt = Cn 1 r_ifz [rs, Z, Cn 1 S [Cn 1 rc [Cn 1 r_dec [rs]]]]

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
rt = Cn 1 r_ifz [rs, Z, Cn 1 S [Cn 1 rc [Cn 1 r_dec [rs]]]]
[PROOF STEP]
have "recfn 1 rt"
[PROOF STATE]
proof (prove)
using this:
rt = Cn 1 r_ifz [rs, Z, Cn 1 S [Cn 1 rc [Cn 1 r_dec [rs]]]]

goal (1 subgoal):
 1. recfn 1 rt
[PROOF STEP]
using rc(1) rs(1)
[PROOF STATE]
proof (prove)
using this:
rt = Cn 1 r_ifz [rs, Z, Cn 1 S [Cn 1 rc [Cn 1 r_dec [rs]]]]
recfn 1 rc
recfn 1 rs

goal (1 subgoal):
 1. recfn 1 rt
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
recfn 1 rt

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
have "eval rt [x] \<up>" if "eval rs [x] \<up>" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval rt [x] \<up>
[PROOF STEP]
using rc(1) rs(1) rt_def that
[PROOF STATE]
proof (prove)
using this:
recfn 1 rc
recfn 1 rs
rt = Cn 1 r_ifz [rs, Z, Cn 1 S [Cn 1 rc [Cn 1 r_dec [rs]]]]
eval rs [x] \<up>

goal (1 subgoal):
 1. eval rt [x] \<up>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval rs [?x] \<up> \<Longrightarrow> eval rt [?x] \<up>

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval rs [?x] \<up> \<Longrightarrow> eval rt [?x] \<up>

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
have "eval rt [x] \<down>= 0" if "eval rs [x] \<down>= 0" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval rt [x] \<down>= 0
[PROOF STEP]
using rt_def that rc(1,2) rs(1)
[PROOF STATE]
proof (prove)
using this:
rt = Cn 1 r_ifz [rs, Z, Cn 1 S [Cn 1 rc [Cn 1 r_dec [rs]]]]
eval rs [x] \<down>= 0
recfn 1 rc
Partial_Recursive.total rc
recfn 1 rs

goal (1 subgoal):
 1. eval rt [x] \<down>= 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
eval rs [?x] \<down>= 0 \<Longrightarrow> eval rt [?x] \<down>= 0

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eval rs [?x] \<down>= 0 \<Longrightarrow> eval rt [?x] \<down>= 0

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
have "eval rt [x] \<down>= Suc (the (c (the (s x) - 1)))" if "eval rs [x] \<down>\<noteq> 0" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval rt [x] \<down>= Suc (the (c (the (s x) - 1)))
[PROOF STEP]
using rt_def that rc rs
[PROOF STATE]
proof (prove)
using this:
rt = Cn 1 r_ifz [rs, Z, Cn 1 S [Cn 1 rc [Cn 1 r_dec [rs]]]]
eval rs [x] \<down>\<noteq> 0
recfn 1 rc
Partial_Recursive.total rc
\<forall>x. c x = eval rc [x]
recfn 1 rs
\<forall>x. s x = eval rs [x]

goal (1 subgoal):
 1. eval rt [x] \<down>= Suc (the (c (the (s x) - 1)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
eval rs [?x] \<down>\<noteq> 0 \<Longrightarrow> eval rt [?x] \<down>= Suc (the (c (the (s ?x) - 1)))

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eval rs [?x] \<up> \<Longrightarrow> eval rt [?x] \<up>
eval rs [?x] \<down>= 0 \<Longrightarrow> eval rt [?x] \<down>= 0
eval rs [?x] \<down>\<noteq> 0 \<Longrightarrow> eval rt [?x] \<down>= Suc (the (c (the (s ?x) - 1)))
[PROOF STEP]
have "eval rt [x] = t x" for x
[PROOF STATE]
proof (prove)
using this:
eval rs [?x] \<up> \<Longrightarrow> eval rt [?x] \<up>
eval rs [?x] \<down>= 0 \<Longrightarrow> eval rt [?x] \<down>= 0
eval rs [?x] \<down>\<noteq> 0 \<Longrightarrow> eval rt [?x] \<down>= Suc (the (c (the (s ?x) - 1)))

goal (1 subgoal):
 1. eval rt [x] = t x
[PROOF STEP]
by (simp add: rs(2) t_def)
[PROOF STATE]
proof (state)
this:
eval rt [?x] = t ?x

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
with \<open>recfn 1 rt\<close>
[PROOF STATE]
proof (chain)
picking this:
recfn 1 rt
eval rt [?x] = t ?x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
recfn 1 rt
eval rt [?x] = t ?x

goal (1 subgoal):
 1. t \<in> \

[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t \<in> \

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
t \<in> \

goal (1 subgoal):
 1. \<exists>t. learn_fin \<chi> U t
[PROOF STEP]
have t: "t (f \<triangleright> n) \<down>=
      (if s (f \<triangleright> n) = Some 0 then 0 else Suc (the (c (the (s (f \<triangleright> n)) - 1))))"
    if "f \<in> U" for f n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t (f \<triangleright> n) \<down>= (if s (f \<triangleright> n) \<down>= 0 then 0 else Suc (the (c (the (s (f \<triangleright> n)) - 1))))
[PROOF STEP]
using that env
[PROOF STATE]
proof (prove)
using this:
f \<in> U
environment \<psi> U s

goal (1 subgoal):
 1. t (f \<triangleright> n) \<down>= (if s (f \<triangleright> n) \<down>= 0 then 0 else Suc (the (c (the (s (f \<triangleright> n)) - 1))))
[PROOF STEP]
by (simp add: t_def)
[PROOF STATE]
proof (state)
this:
?f \<in> U \<Longrightarrow> t (?f \<triangleright> ?n) \<down>= (if s (?f \<triangleright> ?n) \<down>= 0 then 0 else Suc (the (c (the (s (?f \<triangleright> ?n)) - 1))))

goal (1 subgoal):
 1. \<exists>t. learn_fin \<chi> U t
[PROOF STEP]
have "learn_fin \<chi> U t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. learn_fin \<chi> U t
[PROOF STEP]
proof (rule learn_finI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. environment \<chi> U t
 2. \<And>f. f \<in> U \<Longrightarrow> \<exists>i n\<^sub>0. \<chi> i = f \<and> (\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= Suc i)
[PROOF STEP]
show "environment \<chi> U t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. environment \<chi> U t
[PROOF STEP]
using t
[PROOF STATE]
proof (prove)
using this:
?f \<in> U \<Longrightarrow> t (?f \<triangleright> ?n) \<down>= (if s (?f \<triangleright> ?n) \<down>= 0 then 0 else Suc (the (c (the (s (?f \<triangleright> ?n)) - 1))))

goal (1 subgoal):
 1. environment \<chi> U t
[PROOF STEP]
by (simp add: \<open>t \<in> \
\<close> env goedel_numbering_P2[OF assms(1)])
[PROOF STATE]
proof (state)
this:
environment \<chi> U t

goal (1 subgoal):
 1. \<And>f. f \<in> U \<Longrightarrow> \<exists>i n\<^sub>0. \<chi> i = f \<and> (\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= Suc i)
[PROOF STEP]
show "\<exists>i n\<^sub>0. \<chi> i = f \<and> (\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= Suc i)"
      if "f \<in> U" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<chi> i = f \<and> (\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= Suc i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<chi> i = f \<and> (\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= Suc i)
[PROOF STEP]
from fin
[PROOF STATE]
proof (chain)
picking this:
?f \<in> U \<Longrightarrow> \<exists>i n\<^sub>0. \<psi> i = ?f \<and> (\<forall>n<n\<^sub>0. s (?f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. s (?f \<triangleright> n) \<down>= Suc i)
[PROOF STEP]
obtain i n\<^sub>0 where
        i: "\<psi> i = f \<and> (\<forall>n<n\<^sub>0. s (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. s (f \<triangleright> n) \<down>= Suc i)"
[PROOF STATE]
proof (prove)
using this:
?f \<in> U \<Longrightarrow> \<exists>i n\<^sub>0. \<psi> i = ?f \<and> (\<forall>n<n\<^sub>0. s (?f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. s (?f \<triangleright> n) \<down>= Suc i)

goal (1 subgoal):
 1. (\<And>i n\<^sub>0. \<psi> i = f \<and> (\<forall>n<n\<^sub>0. s (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. s (f \<triangleright> n) \<down>= Suc i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>f \<in> U\<close>
[PROOF STATE]
proof (prove)
using this:
?f \<in> U \<Longrightarrow> \<exists>i n\<^sub>0. \<psi> i = ?f \<and> (\<forall>n<n\<^sub>0. s (?f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. s (?f \<triangleright> n) \<down>= Suc i)
f \<in> U

goal (1 subgoal):
 1. (\<And>i n\<^sub>0. \<psi> i = f \<and> (\<forall>n<n\<^sub>0. s (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. s (f \<triangleright> n) \<down>= Suc i) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<psi> i = f \<and> (\<forall>n<n\<^sub>0. s (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. s (f \<triangleright> n) \<down>= Suc i)

goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<chi> i = f \<and> (\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= Suc i)
[PROOF STEP]
let ?j = "the (c i)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<chi> i = f \<and> (\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= Suc i)
[PROOF STEP]
have "\<chi> ?j = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<chi> (the (c i)) = f
[PROOF STEP]
using c(2) i
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<psi> i = \<chi> (the (c i))
\<psi> i = f \<and> (\<forall>n<n\<^sub>0. s (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. s (f \<triangleright> n) \<down>= Suc i)

goal (1 subgoal):
 1. \<chi> (the (c i)) = f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<chi> (the (c i)) = f

goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<chi> i = f \<and> (\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= Suc i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<chi> (the (c i)) = f

goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<chi> i = f \<and> (\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= Suc i)
[PROOF STEP]
have "\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0
[PROOF STEP]
using t[OF that] i
[PROOF STATE]
proof (prove)
using this:
t (f \<triangleright> ?n) \<down>= (if s (f \<triangleright> ?n) \<down>= 0 then 0 else Suc (the (c (the (s (f \<triangleright> ?n)) - 1))))
\<psi> i = f \<and> (\<forall>n<n\<^sub>0. s (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. s (f \<triangleright> n) \<down>= Suc i)

goal (1 subgoal):
 1. \<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0

goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<chi> i = f \<and> (\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= Suc i)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0

goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<chi> i = f \<and> (\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= Suc i)
[PROOF STEP]
have "t (f \<triangleright> n) \<down>= Suc ?j" if "n \<ge> n\<^sub>0" for n
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t (f \<triangleright> n) \<down>= Suc (the (c i))
[PROOF STEP]
using that i t[OF \<open>f \<in> U\<close>]
[PROOF STATE]
proof (prove)
using this:
n\<^sub>0 \<le> n
\<psi> i = f \<and> (\<forall>n<n\<^sub>0. s (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. s (f \<triangleright> n) \<down>= Suc i)
t (f \<triangleright> ?n) \<down>= (if s (f \<triangleright> ?n) \<down>= 0 then 0 else Suc (the (c (the (s (f \<triangleright> ?n)) - 1))))

goal (1 subgoal):
 1. t (f \<triangleright> n) \<down>= Suc (the (c i))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n\<^sub>0 \<le> ?n \<Longrightarrow> t (f \<triangleright> ?n) \<down>= Suc (the (c i))

goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<chi> i = f \<and> (\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= Suc i)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<chi> (the (c i)) = f
\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0
n\<^sub>0 \<le> ?n \<Longrightarrow> t (f \<triangleright> ?n) \<down>= Suc (the (c i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<chi> (the (c i)) = f
\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0
n\<^sub>0 \<le> ?n \<Longrightarrow> t (f \<triangleright> ?n) \<down>= Suc (the (c i))

goal (1 subgoal):
 1. \<exists>i n\<^sub>0. \<chi> i = f \<and> (\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= Suc i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>i n\<^sub>0. \<chi> i = f \<and> (\<forall>n<n\<^sub>0. t (f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (f \<triangleright> n) \<down>= Suc i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?f \<in> U \<Longrightarrow> \<exists>i n\<^sub>0. \<chi> i = ?f \<and> (\<forall>n<n\<^sub>0. t (?f \<triangleright> n) \<down>= 0) \<and> (\<forall>n\<ge>n\<^sub>0. t (?f \<triangleright> n) \<down>= Suc i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
learn_fin \<chi> U t

goal (1 subgoal):
 1. \<exists>t. learn_fin \<chi> U t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
learn_fin \<chi> U t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
learn_fin \<chi> U t

goal (1 subgoal):
 1. \<exists>t. learn_fin \<chi> U t
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>t. learn_fin \<chi> U t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma omega_sum_0_iff [simp]: "normal ns \<Longrightarrow> omega_sum ns = 0 \<longleftrightarrow> ns = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normal ns \<Longrightarrow> (omega_sum ns = 0) = (ns = [])
[PROOF STEP]
by (induction ns rule: normal.induct) auto


[STATEMENT]
lemma eval_akra_bazzi_sum':
  "(\<Sum>i<0. as!i * f ((ts!i) x)) = 0"
  "(\<Sum>i<Suc 0. (a#as)!i * f (((t#ts)!i) x)) = a * f (t x)"
  "(\<Sum>i<Suc k. (a#as)!i * f (((t#ts)!i) x)) = a * f (t x) + (\<Sum>i<k. as!i * f ((ts!i) x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<0. as ! i * f ((ts ! i) x)) = (0::'a) &&& (\<Sum>i<Suc 0. (a # as) ! i * f (((t # ts) ! i) x)) = a * f (t x) &&& (\<Sum>i<Suc k. (a # as) ! i * f (((t # ts) ! i) x)) = a * f (t x) + (\<Sum>i<k. as ! i * f ((ts ! i) x))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (\<Sum>i<Suc 0. (a # as) ! i * f (((t # ts) ! i) x)) = a * f (t x)
 2. (\<Sum>i<Suc k. (a # as) ! i * f (((t # ts) ! i) x)) = a * f (t x) + (\<Sum>i<k. as ! i * f ((ts ! i) x))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<Suc k. (a # as) ! i * f (((t # ts) ! i) x)) = a * f (t x) + (\<Sum>i<k. as ! i * f ((ts ! i) x))
[PROOF STEP]
apply (induction k arbitrary: a as t ts)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as t ts. (\<Sum>i<Suc 0. (a # as) ! i * f (((t # ts) ! i) x)) = a * f (t x) + (\<Sum>i<0. as ! i * f ((ts ! i) x))
 2. \<And>k a as t ts. (\<And>a as t ts. (\<Sum>i<Suc k. (a # as) ! i * f (((t # ts) ! i) x)) = a * f (t x) + (\<Sum>i<k. as ! i * f ((ts ! i) x))) \<Longrightarrow> (\<Sum>i<Suc (Suc k). (a # as) ! i * f (((t # ts) ! i) x)) = a * f (t x) + (\<Sum>i<Suc k. as ! i * f ((ts ! i) x))
[PROOF STEP]
apply (simp_all add: algebra_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sin_periodic_pi_diff: "sin (x - pi) = - sin x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sin (x - pi) = - sin x
[PROOF STEP]
by (fact sin_minus_pi)


[STATEMENT]
lemma square_lesseq_square: "\<And> x y. 0 \<le> (x :: 'a :: linordered_field) \<Longrightarrow> 0 \<le> y \<Longrightarrow> (x * x \<le> y * y) = (x \<le> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>(0::'a) \<le> x; (0::'a) \<le> y\<rbrakk> \<Longrightarrow> (x * x \<le> y * y) = (x \<le> y)
[PROOF STEP]
by (metis mult_mono mult_strict_mono' not_less)


[STATEMENT]
lemma map_of_mpoly_to_mpoly_poly_impl_aux1:
  "map_of (mpoly_to_mpoly_poly_impl_aux1 i xs j) = (\<lambda>mon.
     (if lookup mon i > 0 then None
      else map_of xs (mon + Poly_Mapping.single i j)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (mpoly_to_mpoly_poly_impl_aux1 i xs j) = (\<lambda>mon. if 0 < lookup mon i then None else map_of xs (mon + monomial j i))
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>mon. map_of (mpoly_to_mpoly_poly_impl_aux1 i xs j) mon = (if 0 < lookup mon i then None else map_of xs (mon + monomial j i))
[PROOF STEP]
apply (induction i xs j rule: mpoly_to_mpoly_poly_impl_aux1.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i j mon. map_of (mpoly_to_mpoly_poly_impl_aux1 i [] j) mon = (if 0 < lookup mon i then None else map_of [] (mon + monomial j i))
 2. \<And>i mon' c xs j mon. (\<And>mon. map_of (mpoly_to_mpoly_poly_impl_aux1 i xs j) mon = (if 0 < lookup mon i then None else map_of xs (mon + monomial j i))) \<Longrightarrow> map_of (mpoly_to_mpoly_poly_impl_aux1 i ((mon', c) # xs) j) mon = (if 0 < lookup mon i then None else map_of ((mon', c) # xs) (mon + monomial j i))
[PROOF STEP]
apply (auto simp: remove_key_lookup)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>i mon' c xs. \<lbrakk>\<And>mon. map_of (mpoly_to_mpoly_poly_impl_aux1 i xs (lookup mon' i)) mon = (if 0 < lookup mon i then None else map_of xs (mon + monomial (lookup mon' i) i)); remove_key i mon' + monomial (lookup mon' i) i \<noteq> mon'\<rbrakk> \<Longrightarrow> Some c = map_of xs (remove_key i mon' + monomial (lookup mon' i) i)
 2. \<And>i mon' c xs j. \<lbrakk>\<And>mon. map_of (mpoly_to_mpoly_poly_impl_aux1 i xs j) mon = (if 0 < lookup mon i then None else map_of xs (mon + monomial j i)); lookup mon' i \<noteq> j; remove_key i mon' + monomial j i = mon'\<rbrakk> \<Longrightarrow> map_of xs mon' = Some c
 3. \<And>i c xs j mon. \<lbrakk>\<And>mon. map_of (mpoly_to_mpoly_poly_impl_aux1 i xs j) mon = (if 0 < lookup mon i then None else map_of xs (mon + monomial j i)); mon \<noteq> remove_key i (mon + monomial j i); lookup mon i = 0\<rbrakk> \<Longrightarrow> map_of xs (mon + monomial j i) = Some c
[PROOF STEP]
apply (meson remove_key_sum)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i mon' c xs j. \<lbrakk>\<And>mon. map_of (mpoly_to_mpoly_poly_impl_aux1 i xs j) mon = (if 0 < lookup mon i then None else map_of xs (mon + monomial j i)); lookup mon' i \<noteq> j; remove_key i mon' + monomial j i = mon'\<rbrakk> \<Longrightarrow> map_of xs mon' = Some c
 2. \<And>i c xs j mon. \<lbrakk>\<And>mon. map_of (mpoly_to_mpoly_poly_impl_aux1 i xs j) mon = (if 0 < lookup mon i then None else map_of xs (mon + monomial j i)); mon \<noteq> remove_key i (mon + monomial j i); lookup mon i = 0\<rbrakk> \<Longrightarrow> map_of xs (mon + monomial j i) = Some c
[PROOF STEP]
apply (metis add_left_cancel lookup_single_eq remove_key_sum)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i c xs j mon. \<lbrakk>\<And>mon. map_of (mpoly_to_mpoly_poly_impl_aux1 i xs j) mon = (if 0 < lookup mon i then None else map_of xs (mon + monomial j i)); mon \<noteq> remove_key i (mon + monomial j i); lookup mon i = 0\<rbrakk> \<Longrightarrow> map_of xs (mon + monomial j i) = Some c
[PROOF STEP]
apply (metis remove_key_add remove_key_single remove_key_sum single_zero)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma merge_Suc_aux':
  "\<rho> \<in> space (state_measure (Suc ` V') (case_nat t \<Gamma>)) \<Longrightarrow>
    (\<lambda>\<sigma>. merge V V' (\<sigma>, \<rho> \<circ> Suc)) \<in> measurable (state_measure V \<Gamma>) (state_measure (V \<union> V') \<Gamma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> \<in> space (state_measure (Suc ` V') (case_nat t \<Gamma>)) \<Longrightarrow> (\<lambda>\<sigma>. merge V V' (\<sigma>, \<rho> \<circ> Suc)) \<in> state_measure V \<Gamma> \<rightarrow>\<^sub>M state_measure (V \<union> V') \<Gamma>
[PROOF STEP]
by (unfold state_measure_def,
    rule measurable_compose[OF measurable_Pair measurable_merge], simp,
    rule measurable_const, auto simp: space_PiM dest: PiE_mem)


[STATEMENT]
lemma weak_invariant_simplex:
  "invariant_simplex cs J s \<Longrightarrow> weak_invariant_simplex cs J s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invariant_simplex cs J s \<Longrightarrow> weak_invariant_simplex cs J s
[PROOF STEP]
using Incremental_Simplex.weak_invariant_cs[of cs J]
[PROOF STATE]
proof (prove)
using this:
invariant_simplex' cs J ?s \<Longrightarrow> weak_invariant_simplex' cs J ?s

goal (1 subgoal):
 1. invariant_simplex cs J s \<Longrightarrow> weak_invariant_simplex cs J s
[PROOF STEP]
by (cases s, auto)


[STATEMENT]
lemma \<mu>_stable_subfrmlsn:
  "\<mu>_stable \<phi> w \<Longrightarrow> \<psi> \<in> subfrmlsn \<phi> \<Longrightarrow> \<mu>_stable \<psi> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<mu>_stable \<phi> w; \<psi> \<in> subfrmlsn \<phi>\<rbrakk> \<Longrightarrow> \<mu>_stable \<psi> w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<mu>_stable \<phi> w; \<psi> \<in> subfrmlsn \<phi>\<rbrakk> \<Longrightarrow> \<mu>_stable \<psi> w
[PROOF STEP]
assume a1: "\<psi> \<in> subfrmlsn \<phi>" and a2: "\<mu>_stable \<phi> w"
[PROOF STATE]
proof (state)
this:
\<psi> \<in> subfrmlsn \<phi>
\<mu>_stable \<phi> w

goal (1 subgoal):
 1. \<lbrakk>\<mu>_stable \<phi> w; \<psi> \<in> subfrmlsn \<phi>\<rbrakk> \<Longrightarrow> \<mu>_stable \<psi> w
[PROOF STEP]
have "subformulas\<^sub>\<mu> \<psi> \<subseteq> subformulas\<^sub>\<mu> \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subformulas\<^sub>\<mu> \<psi> \<subseteq> subformulas\<^sub>\<mu> \<phi>
[PROOF STEP]
using a1
[PROOF STATE]
proof (prove)
using this:
\<psi> \<in> subfrmlsn \<phi>

goal (1 subgoal):
 1. subformulas\<^sub>\<mu> \<psi> \<subseteq> subformulas\<^sub>\<mu> \<phi>
[PROOF STEP]
by (simp add: subformulas\<^sub>\<mu>_subset)
[PROOF STATE]
proof (state)
this:
subformulas\<^sub>\<mu> \<psi> \<subseteq> subformulas\<^sub>\<mu> \<phi>

goal (1 subgoal):
 1. \<lbrakk>\<mu>_stable \<phi> w; \<psi> \<in> subfrmlsn \<phi>\<rbrakk> \<Longrightarrow> \<mu>_stable \<psi> w
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
subformulas\<^sub>\<mu> \<psi> \<subseteq> subformulas\<^sub>\<mu> \<phi>

goal (1 subgoal):
 1. \<lbrakk>\<mu>_stable \<phi> w; \<psi> \<in> subfrmlsn \<phi>\<rbrakk> \<Longrightarrow> \<mu>_stable \<psi> w
[PROOF STEP]
have "\<G>\<F> \<phi> w = \<F> \<phi> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<G>\<F> \<phi> w = \<F> \<phi> w
[PROOF STEP]
using a2
[PROOF STATE]
proof (prove)
using this:
\<mu>_stable \<phi> w

goal (1 subgoal):
 1. \<G>\<F> \<phi> w = \<F> \<phi> w
[PROOF STEP]
by (meson \<mu>_stable_def)
[PROOF STATE]
proof (state)
this:
\<G>\<F> \<phi> w = \<F> \<phi> w

goal (1 subgoal):
 1. \<lbrakk>\<mu>_stable \<phi> w; \<psi> \<in> subfrmlsn \<phi>\<rbrakk> \<Longrightarrow> \<mu>_stable \<psi> w
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
subformulas\<^sub>\<mu> \<psi> \<subseteq> subformulas\<^sub>\<mu> \<phi>
\<G>\<F> \<phi> w = \<F> \<phi> w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
subformulas\<^sub>\<mu> \<psi> \<subseteq> subformulas\<^sub>\<mu> \<phi>
\<G>\<F> \<phi> w = \<F> \<phi> w

goal (1 subgoal):
 1. \<mu>_stable \<psi> w
[PROOF STEP]
by (metis (no_types) Un_commute \<F>_semantics' \<G>\<F>_semantics' \<mu>_stable_def inf_left_commute inf_sup_absorb sup.orderE)
[PROOF STATE]
proof (state)
this:
\<mu>_stable \<psi> w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eq_or_mem_image_simp[simp]: "{f l |l. l = a \<or> l\<in>B} = insert (f a) {f l|l. l\<in>B}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f l |l. l = a \<or> l \<in> B} = insert (f a) {f l |l. l \<in> B}
[PROOF STEP]
by blast


[STATEMENT]
lemma set_union_code [code_unfold]:
    "set xs \<union> set ys = set (xs @ ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set xs \<union> set ys = set (xs @ ys)
[PROOF STEP]
by auto


[STATEMENT]
lemma take_update_last: "length list>n \<Longrightarrow> (take (Suc n) list) [n:=x] = take n list @ [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n < length list \<Longrightarrow> (take (Suc n) list)[n := x] = take n list @ [x]
[PROOF STEP]
by (induct list arbitrary: n)
       (auto split: nat.split)


[STATEMENT]
lemma r_le_rtrancl[simp]: "S\<subseteq>S\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S \<subseteq> S\<^sup>*
[PROOF STEP]
by auto


[STATEMENT]
lemma rel_restrict_Int_empty:
  "A \<inter> Field R = {} \<Longrightarrow> rel_restrict R A = R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> Field R = {} \<Longrightarrow> rel_restrict R A = R
[PROOF STEP]
unfolding rel_restrict_def Field_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<inter> (Domain R \<union> Range R) = {} \<Longrightarrow> {(v, w). (v, w) \<in> R \<and> v \<notin> A \<and> w \<notin> A} = R
[PROOF STEP]
by auto


[STATEMENT]
lemma map_of_distinct_lookup:
  assumes "x \<notin> set(map fst xs)"
  "x \<notin> set (map fst ys)"
  shows "map_of (xs @ (x,y) # ys) x = Some y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (xs @ (x, y) # ys) x = Some y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_of (xs @ (x, y) # ys) x = Some y
[PROOF STEP]
have "map_of (xs @ (x,y) # ys) = (map_of (xs @ ys)) (x \<mapsto> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (xs @ (x, y) # ys) = map_of (xs @ ys)(x \<mapsto> y)
[PROOF STEP]
using assms map_of_distinct_upd2
[PROOF STATE]
proof (prove)
using this:
x \<notin> set (map fst xs)
x \<notin> set (map fst ys)
\<lbrakk>?x \<notin> set (map fst ?xs); ?x \<notin> set (map fst ?ys)\<rbrakk> \<Longrightarrow> map_of (?xs @ (?x, ?y) # ?ys) = map_of (?xs @ ?ys)(?x \<mapsto> ?y)

goal (1 subgoal):
 1. map_of (xs @ (x, y) # ys) = map_of (xs @ ys)(x \<mapsto> y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_of (xs @ (x, y) # ys) = map_of (xs @ ys)(x \<mapsto> y)

goal (1 subgoal):
 1. map_of (xs @ (x, y) # ys) x = Some y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
map_of (xs @ (x, y) # ys) = map_of (xs @ ys)(x \<mapsto> y)

goal (1 subgoal):
 1. map_of (xs @ (x, y) # ys) x = Some y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_of (xs @ (x, y) # ys) x = Some y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tm_simp1 : "tm (\<sigma>\<lparr>sqsum := s\<rparr>) = tm \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tm (\<sigma>\<lparr>sqsum := s\<rparr>) = tm \<sigma>
[PROOF STEP]
by simp


[STATEMENT]
lemma closure_idem [simp]:
  "closure (closure S) = closure S" (is "?LS = ?RS")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. closure (closure S) = closure S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closure (closure S) = closure S
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closure (closure S) = closure S
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closure (closure S) = closure S
[PROOF STEP]
assume "s \<in> ?LS"
[PROOF STATE]
proof (state)
this:
s \<in> closure (closure S)

goal (1 subgoal):
 1. closure (closure S) = closure S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> closure (closure S)
[PROOF STEP]
have "s \<in> ?RS"
[PROOF STATE]
proof (prove)
using this:
s \<in> closure (closure S)

goal (1 subgoal):
 1. s \<in> closure S
[PROOF STEP]
by induct auto
[PROOF STATE]
proof (state)
this:
s \<in> closure S

goal (1 subgoal):
 1. closure (closure S) = closure S
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?s2 \<in> closure (closure S) \<Longrightarrow> ?s2 \<in> closure S

goal (1 subgoal):
 1. closure (closure S) = closure S
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?s2 \<in> closure (closure S) \<Longrightarrow> ?s2 \<in> closure S

goal (1 subgoal):
 1. closure (closure S) = closure S
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?s2 \<in> closure (closure S) \<Longrightarrow> ?s2 \<in> closure S

goal (1 subgoal):
 1. closure (closure S) = closure S
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. closure (closure S) = closure S
[PROOF STEP]
assume "s \<in> ?RS"
[PROOF STATE]
proof (state)
this:
s \<in> closure S

goal (1 subgoal):
 1. closure (closure S) = closure S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> closure S
[PROOF STEP]
have "s \<in> ?LS"
[PROOF STATE]
proof (prove)
using this:
s \<in> closure S

goal (1 subgoal):
 1. s \<in> closure (closure S)
[PROOF STEP]
by induct auto
[PROOF STATE]
proof (state)
this:
s \<in> closure (closure S)

goal (1 subgoal):
 1. closure (closure S) = closure S
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?s2 \<in> closure S \<Longrightarrow> ?s2 \<in> closure (closure S)

goal (1 subgoal):
 1. closure (closure S) = closure S
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
?s2 \<in> closure (closure S) \<Longrightarrow> ?s2 \<in> closure S
?s2 \<in> closure S \<Longrightarrow> ?s2 \<in> closure (closure S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?s2 \<in> closure (closure S) \<Longrightarrow> ?s2 \<in> closure S
?s2 \<in> closure S \<Longrightarrow> ?s2 \<in> closure (closure S)

goal (1 subgoal):
 1. closure (closure S) = closure S
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
closure (closure S) = closure S

goal:
No subgoals!
[PROOF STEP]
qed