[STATEMENT]
lemma Q_inf_exec_impl_Q_inf:
  assumes "gta_lang Q \ \<subseteq> {gpair s t| s t. funas_gterm s \<subseteq> fset \<F> \<and> funas_gterm t \<subseteq> fset \<F>}"
   and "\<Q> \ |\<subseteq>| ta_reachable \" and "\<Q> \ |\<subseteq>| ta_productive Q \"
   and "q \<in> Q_inf_e \"
  shows "q |\<in>| Q_infty \ \<F>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q |\<in>| Q_infty \ \<F>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q |\<in>| Q_infty \ \<F>
[PROOF STEP]
let ?S = "{t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q |\<in>| Q_infty \ \<F>
[PROOF STEP]
let ?P = "\<lambda> t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q |\<in>| Q_infty \ \<F>
[PROOF STEP]
let ?F = "(\<lambda>(f, n). ((None, Some f), n)) |`| \<F>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q |\<in>| Q_infty \ \<F>
[PROOF STEP]
from Q_inf_e_infinite_terms_res[OF assms(4, 2)]
[PROOF STATE]
proof (chain)
picking this:
infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
have inf: "infinite ?S"
[PROOF STATE]
proof (prove)
using this:
infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}

goal (1 subgoal):
 1. infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}

goal (1 subgoal):
 1. q |\<in>| Q_infty \ \<F>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
infinite {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}

goal (1 subgoal):
 1. q |\<in>| Q_infty \ \<F>
[PROOF STEP]
fix t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q |\<in>| Q_infty \ \<F>
[PROOF STEP]
assume "t \<in> ?S"
[PROOF STATE]
proof (state)
this:
t \<in> {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}

goal (1 subgoal):
 1. q |\<in>| Q_infty \ \<F>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
t \<in> {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
[PROOF STEP]
have "\<exists> u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> fset \<F>"
[PROOF STATE]
proof (prove)
using this:
t \<in> {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}

goal (1 subgoal):
 1. \<exists>u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> fset \<F>
[PROOF STEP]
using prod_automata_from_none_root_dec[OF assms(1)] assms(2, 3)
[PROOF STATE]
proof (prove)
using this:
t \<in> {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
\<lbrakk>?q |\<in>| ta_der \ (term_of_gterm ?t); fst (groot_sym ?t) = None; \<Q> \ |\<subseteq>| ta_reachable \; ?q |\<in>| ta_productive Q \\<rbrakk> \<Longrightarrow> \<exists>u. ?t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> fset \<F>
\<Q> \ |\<subseteq>| ta_reachable \
\<Q> \ |\<subseteq>| ta_productive Q \

goal (1 subgoal):
 1. \<exists>u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> fset \<F>
[PROOF STEP]
using fin_mono
[PROOF STATE]
proof (prove)
using this:
t \<in> {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None}
\<lbrakk>?q |\<in>| ta_der \ (term_of_gterm ?t); fst (groot_sym ?t) = None; \<Q> \ |\<subseteq>| ta_reachable \; ?q |\<in>| ta_productive Q \\<rbrakk> \<Longrightarrow> \<exists>u. ?t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> fset \<F>
\<Q> \ |\<subseteq>| ta_reachable \
\<Q> \ |\<subseteq>| ta_productive Q \
?A |\<subseteq>| ?B \<Longrightarrow> ?x |\<in>| ?A \<longrightarrow> ?x |\<in>| ?B

goal (1 subgoal):
 1. \<exists>u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> fset \<F>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>u. t = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> fset \<F>

goal (1 subgoal):
 1. q |\<in>| Q_infty \ \<F>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?t3 \<in> {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None} \<Longrightarrow> \<exists>u. ?t3 = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> fset \<F>

goal (1 subgoal):
 1. q |\<in>| Q_infty \ \<F>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?t3 \<in> {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None} \<Longrightarrow> \<exists>u. ?t3 = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> fset \<F>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?t3 \<in> {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None} \<Longrightarrow> \<exists>u. ?t3 = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> fset \<F>

goal (1 subgoal):
 1. q |\<in>| Q_infty \ \<F>
[PROOF STEP]
using infinite_set_dec_infinite[OF inf, of gterm_to_None_Some ?P]
[PROOF STATE]
proof (prove)
using this:
?t3 \<in> {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None} \<Longrightarrow> \<exists>u. ?t3 = gterm_to_None_Some u \<and> funas_gterm u \<subseteq> fset \<F>
(\<And>s. s \<in> {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None} \<Longrightarrow> \<exists>t. gterm_to_None_Some t = s \<and> funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))) \<Longrightarrow> infinite {uu_. \<exists>t s. uu_ = t \<and> s \<in> {t. q |\<in>| ta_der \ (term_of_gterm t) \<and> fst (groot_sym t) = None} \<and> gterm_to_None_Some t = s \<and> funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))}

goal (1 subgoal):
 1. q |\<in>| Q_infty \ \<F>
[PROOF STEP]
by (auto simp: Q_infty_fmember) blast
[PROOF STATE]
proof (state)
this:
q |\<in>| Q_infty \ \<F>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Q_inf_impl_Q_inf_exec:
  assumes "q |\<in>| Q_infty \ \<F>"
    shows "q \<in> Q_inf_e \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
let ?t_of_g = "\<lambda> t. term_of_gterm t :: ('b option \<times> 'b option, 'a) term"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
let ?t_og_g2 = "\<lambda> t. term_of_gterm t :: ('b, 'a) term"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
let ?inf = "(?t_og_g2 :: 'b gterm \<Rightarrow> ('b, 'a) term) ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (?t_of_g (gterm_to_None_Some t))}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
obtain n where card_st: "fcard (\<Q> \) < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. fcard (\<Q> \) < n \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
fcard (\<Q> \) < n

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
q |\<in>| Q_infty \ \<F>
[PROOF STEP]
have "infinite {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (?t_of_g (gterm_to_None_Some t))}"
[PROOF STATE]
proof (prove)
using this:
q |\<in>| Q_infty \ \<F>

goal (1 subgoal):
 1. infinite {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))}
[PROOF STEP]
unfolding Q_infty_def
[PROOF STATE]
proof (prove)
using this:
q |\<in>| {|q |q. infinite {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))}|}

goal (1 subgoal):
 1. infinite {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infinite {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))}

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
from infinite_inj_image_infinite[OF this, of "?t_og_g2"]
[PROOF STATE]
proof (chain)
picking this:
inj_on term_of_gterm {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))} \<Longrightarrow> infinite (term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))})
[PROOF STEP]
have inf: "infinite ?inf"
[PROOF STATE]
proof (prove)
using this:
inj_on term_of_gterm {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))} \<Longrightarrow> infinite (term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))})

goal (1 subgoal):
 1. infinite (term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))})
[PROOF STEP]
using inj_term_of_gterm
[PROOF STATE]
proof (prove)
using this:
inj_on term_of_gterm {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))} \<Longrightarrow> infinite (term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))})
inj_on term_of_gterm ?X

goal (1 subgoal):
 1. infinite (term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))})
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
infinite (term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))})

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
infinite (term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))})

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
fix s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
assume "s \<in> ?inf"
[PROOF STATE]
proof (state)
this:
s \<in> term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))}

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
s \<in> term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))}
[PROOF STEP]
have "ground s" "funas_term s \<subseteq> fset \<F>"
[PROOF STATE]
proof (prove)
using this:
s \<in> term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))}

goal (1 subgoal):
 1. ground s &&& funas_term s \<subseteq> fset \<F>
[PROOF STEP]
by (auto simp: funas_term_of_gterm_conv subsetD)
[PROOF STATE]
proof (state)
this:
ground s
funas_term s \<subseteq> fset \<F>

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?s2 \<in> term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))} \<Longrightarrow> ground ?s2
?s2 \<in> term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))} \<Longrightarrow> funas_term ?s2 \<subseteq> fset \<F>

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
from infinte_no_depth_limit[OF inf, of "fset \<F>"] this
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>finite (fset \<F>); \<forall>t\<in>term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \<A> (term_of_gterm (gterm_to_None_Some t))}. funas_term t \<subseteq> fset \<F>; \<forall>t\<in>term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))}. ground t\<rbrakk> \<Longrightarrow> \<forall>n. \<exists>t\<in>term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))}. n < depth t
?s2 \<in> term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))} \<Longrightarrow> ground ?s2
?s2 \<in> term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))} \<Longrightarrow> funas_term ?s2 \<subseteq> fset \<F>
[PROOF STEP]
obtain u where
    funas: "funas_gterm u \<subseteq> fset \<F>" and card_d: "n < depth (?t_og_g2 u)" and reach: "q |\<in>| ta_der \ (?t_of_g (gterm_to_None_Some u))"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite (fset \<F>); \<forall>t\<in>term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \<A> (term_of_gterm (gterm_to_None_Some t))}. funas_term t \<subseteq> fset \<F>; \<forall>t\<in>term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))}. ground t\<rbrakk> \<Longrightarrow> \<forall>n. \<exists>t\<in>term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))}. n < depth t
?s2 \<in> term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))} \<Longrightarrow> ground ?s2
?s2 \<in> term_of_gterm ` {t |t. funas_gterm t \<subseteq> fset \<F> \<and> q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some t))} \<Longrightarrow> funas_term ?s2 \<subseteq> fset \<F>

goal (1 subgoal):
 1. (\<And>u. \<lbrakk>funas_gterm u \<subseteq> fset \<F>; n < depth (term_of_gterm u); q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some u))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto blast
[PROOF STATE]
proof (state)
this:
funas_gterm u \<subseteq> fset \<F>
n < depth (term_of_gterm u)
q |\<in>| ta_der \ (term_of_gterm (gterm_to_None_Some u))

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
have "depth (?t_og_g2 u) = depth (?t_of_g (gterm_to_None_Some u))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. depth (term_of_gterm u) = depth (term_of_gterm (gterm_to_None_Some u))
[PROOF STEP]
proof (induct u)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2a. (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> depth (term_of_gterm x2aa) = depth (term_of_gterm (gterm_to_None_Some x2aa))) \<Longrightarrow> depth (term_of_gterm (GFun x1a x2a)) = depth (term_of_gterm (gterm_to_None_Some (GFun x1a x2a)))
[PROOF STEP]
case (GFun f ts)
[PROOF STATE]
proof (state)
this:
?x2aa \<in> set ts \<Longrightarrow> depth (term_of_gterm ?x2aa) = depth (term_of_gterm (gterm_to_None_Some ?x2aa))

goal (1 subgoal):
 1. \<And>x1a x2a. (\<And>x2aa. x2aa \<in> set x2a \<Longrightarrow> depth (term_of_gterm x2aa) = depth (term_of_gterm (gterm_to_None_Some x2aa))) \<Longrightarrow> depth (term_of_gterm (GFun x1a x2a)) = depth (term_of_gterm (gterm_to_None_Some (GFun x1a x2a)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x2aa \<in> set ts \<Longrightarrow> depth (term_of_gterm ?x2aa) = depth (term_of_gterm (gterm_to_None_Some ?x2aa))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?x2aa \<in> set ts \<Longrightarrow> depth (term_of_gterm ?x2aa) = depth (term_of_gterm (gterm_to_None_Some ?x2aa))

goal (1 subgoal):
 1. depth (term_of_gterm (GFun f ts)) = depth (term_of_gterm (gterm_to_None_Some (GFun f ts)))
[PROOF STEP]
by (auto simp: comp_def intro: nth_args_depth_eqI)
[PROOF STATE]
proof (state)
this:
depth (term_of_gterm (GFun f ts)) = depth (term_of_gterm (gterm_to_None_Some (GFun f ts)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
depth (term_of_gterm u) = depth (term_of_gterm (gterm_to_None_Some u))

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
from this pigeonhole_tree_automata[OF _ reach] card_st card_d
[PROOF STATE]
proof (chain)
picking this:
depth (term_of_gterm u) = depth (term_of_gterm (gterm_to_None_Some u))
\<lbrakk>fcard (\<Q> \) < depth (term_of_gterm (gterm_to_None_Some u)); ground (term_of_gterm (gterm_to_None_Some u))\<rbrakk> \<Longrightarrow> \<exists>C C2 v p. C2 \<noteq> \<box> \<and> C\<langle>C2\<langle>v\<rangle>\<rangle> = term_of_gterm (gterm_to_None_Some u) \<and> p |\<in>| ta_der \ v \<and> p |\<in>| ta_der \ C2\<langle>Var p\<rangle> \<and> q |\<in>| ta_der \ C\<langle>Var p\<rangle>
fcard (\<Q> \) < n
n < depth (term_of_gterm u)
[PROOF STEP]
obtain C2 C s v p where
    ctxt: "C2 \<noteq> \<box>" "C\<langle>s\<rangle> = term_of_gterm (gterm_to_None_Some u)" "C2\<langle>v\<rangle> = s" and
    loop: "p |\<in>| ta_der \ v \<and> p |\<in>| ta_der \ C2\<langle>Var p\<rangle> \<and> q |\<in>| ta_der \ C\<langle>Var p\<rangle>"
[PROOF STATE]
proof (prove)
using this:
depth (term_of_gterm u) = depth (term_of_gterm (gterm_to_None_Some u))
\<lbrakk>fcard (\<Q> \) < depth (term_of_gterm (gterm_to_None_Some u)); ground (term_of_gterm (gterm_to_None_Some u))\<rbrakk> \<Longrightarrow> \<exists>C C2 v p. C2 \<noteq> \<box> \<and> C\<langle>C2\<langle>v\<rangle>\<rangle> = term_of_gterm (gterm_to_None_Some u) \<and> p |\<in>| ta_der \ v \<and> p |\<in>| ta_der \ C2\<langle>Var p\<rangle> \<and> q |\<in>| ta_der \ C\<langle>Var p\<rangle>
fcard (\<Q> \) < n
n < depth (term_of_gterm u)

goal (1 subgoal):
 1. (\<And>C2 C s v p. \<lbrakk>C2 \<noteq> \<box>; C\<langle>s\<rangle> = term_of_gterm (gterm_to_None_Some u); C2\<langle>v\<rangle> = s; p |\<in>| ta_der \ v \<and> p |\<in>| ta_der \ C2\<langle>Var p\<rangle> \<and> q |\<in>| ta_der \ C\<langle>Var p\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
C2 \<noteq> \<box>
C\<langle>s\<rangle> = term_of_gterm (gterm_to_None_Some u)
C2\<langle>v\<rangle> = s
p |\<in>| ta_der \ v \<and> p |\<in>| ta_der \ C2\<langle>Var p\<rangle> \<and> q |\<in>| ta_der \ C\<langle>Var p\<rangle>

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
from ctxt
[PROOF STATE]
proof (chain)
picking this:
C2 \<noteq> \<box>
C\<langle>s\<rangle> = term_of_gterm (gterm_to_None_Some u)
C2\<langle>v\<rangle> = s
[PROOF STEP]
have gr: "ground_ctxt C2" "ground_ctxt C"
[PROOF STATE]
proof (prove)
using this:
C2 \<noteq> \<box>
C\<langle>s\<rangle> = term_of_gterm (gterm_to_None_Some u)
C2\<langle>v\<rangle> = s

goal (1 subgoal):
 1. ground_ctxt C2 &&& ground_ctxt C
[PROOF STEP]
by auto (metis ground_ctxt_apply ground_term_of_gterm)+
[PROOF STATE]
proof (state)
this:
ground_ctxt C2
ground_ctxt C

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
from ta_der_to_ta_strict[OF _ gr(1)] loop
[PROOF STATE]
proof (chain)
picking this:
?q |\<in>| ta_der ?A C2\<langle>Var ?p\<rangle> \<Longrightarrow> \<exists>q'. (?p = q' \<or> (?p, q') |\<in>| (eps ?A)|\<^sup>+|) \<and> ?q |\<in>| ta_der_strict ?A C2\<langle>Var q'\<rangle>
p |\<in>| ta_der \ v \<and> p |\<in>| ta_der \ C2\<langle>Var p\<rangle> \<and> q |\<in>| ta_der \ C\<langle>Var p\<rangle>
[PROOF STEP]
obtain q' where
    to_strict: "(p = q' \<or> (p, q') |\<in>| (eps \)|\<^sup>+|) \<and> p |\<in>| ta_der_strict \ C2\<langle>Var q'\<rangle>"
[PROOF STATE]
proof (prove)
using this:
?q |\<in>| ta_der ?A C2\<langle>Var ?p\<rangle> \<Longrightarrow> \<exists>q'. (?p = q' \<or> (?p, q') |\<in>| (eps ?A)|\<^sup>+|) \<and> ?q |\<in>| ta_der_strict ?A C2\<langle>Var q'\<rangle>
p |\<in>| ta_der \ v \<and> p |\<in>| ta_der \ C2\<langle>Var p\<rangle> \<and> q |\<in>| ta_der \ C\<langle>Var p\<rangle>

goal (1 subgoal):
 1. (\<And>q'. (p = q' \<or> (p, q') |\<in>| (eps \)|\<^sup>+|) \<and> p |\<in>| ta_der_strict \ C2\<langle>Var q'\<rangle> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(p = q' \<or> (p, q') |\<in>| (eps \)|\<^sup>+|) \<and> p |\<in>| ta_der_strict \ C2\<langle>Var q'\<rangle>

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
have *: "\<exists> C. C2 = map_funs_ctxt lift_None_Some C \<and> C \<noteq> \<box>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>C. C2 = map_funs_ctxt lift_None_Some C \<and> C \<noteq> \<box>
[PROOF STEP]
using ctxt(1, 2)
[PROOF STATE]
proof (prove)
using this:
C2 \<noteq> \<box>
C\<langle>s\<rangle> = term_of_gterm (gterm_to_None_Some u)

goal (1 subgoal):
 1. \<exists>C. C2 = map_funs_ctxt lift_None_Some C \<and> C \<noteq> \<box>
[PROOF STEP]
by (auto simp flip: ctxt(3)) (smt ctxt.simps(8) map_funs_term_ctxt_decomp map_term_of_gterm)
[PROOF STATE]
proof (state)
this:
\<exists>C. C2 = map_funs_ctxt lift_None_Some C \<and> C \<noteq> \<box>

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>C. C2 = map_funs_ctxt lift_None_Some C \<and> C \<noteq> \<box>
[PROOF STEP]
have q_p: "(q', p) \<in> Q_inf \"
[PROOF STATE]
proof (prove)
using this:
\<exists>C. C2 = map_funs_ctxt lift_None_Some C \<and> C \<noteq> \<box>

goal (1 subgoal):
 1. (q', p) \<in> Q_inf \
[PROOF STEP]
using to_strict ta_der_Q_inf[of p \ _  q'] ctxt
[PROOF STATE]
proof (prove)
using this:
\<exists>C. C2 = map_funs_ctxt lift_None_Some C \<and> C \<noteq> \<box>
(p = q' \<or> (p, q') |\<in>| (eps \)|\<^sup>+|) \<and> p |\<in>| ta_der_strict \ C2\<langle>Var q'\<rangle>
\<lbrakk>p |\<in>| ta_der_strict \ (map_funs_term lift_None_Some ?C\<langle>Var q'\<rangle>); ?C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (q', p) \<in> Q_inf \
C2 \<noteq> \<box>
C\<langle>s\<rangle> = term_of_gterm (gterm_to_None_Some u)
C2\<langle>v\<rangle> = s

goal (1 subgoal):
 1. (q', p) \<in> Q_inf \
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(q', p) \<in> Q_inf \

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q', p) \<in> Q_inf \
[PROOF STEP]
have cycle: "(q', q') \<in> Q_inf \"
[PROOF STATE]
proof (prove)
using this:
(q', p) \<in> Q_inf \

goal (1 subgoal):
 1. (q', q') \<in> Q_inf \
[PROOF STEP]
using to_strict
[PROOF STATE]
proof (prove)
using this:
(q', p) \<in> Q_inf \
(p = q' \<or> (p, q') |\<in>| (eps \)|\<^sup>+|) \<and> p |\<in>| ta_der_strict \ C2\<langle>Var q'\<rangle>

goal (1 subgoal):
 1. (q', q') \<in> Q_inf \
[PROOF STEP]
by (auto intro: Q_inf_ta_eps_Q_inf)
[PROOF STATE]
proof (state)
this:
(q', q') \<in> Q_inf \

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
proof (cases "C = \<box>")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. C = \<box> \<Longrightarrow> q \<in> Q_inf_e \
 2. C \<noteq> \<box> \<Longrightarrow> q \<in> Q_inf_e \
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
C = \<box>

goal (2 subgoals):
 1. C = \<box> \<Longrightarrow> q \<in> Q_inf_e \
 2. C \<noteq> \<box> \<Longrightarrow> q \<in> Q_inf_e \
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C = \<box>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C = \<box>

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
using cycle q_p loop
[PROOF STATE]
proof (prove)
using this:
C = \<box>
(q', q') \<in> Q_inf \
(q', p) \<in> Q_inf \
p |\<in>| ta_der \ v \<and> p |\<in>| ta_der \ C2\<langle>Var p\<rangle> \<and> q |\<in>| ta_der \ C\<langle>Var p\<rangle>

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
by (auto intro: Q_inf_ta_eps_Q_inf)
[PROOF STATE]
proof (state)
this:
q \<in> Q_inf_e \

goal (1 subgoal):
 1. C \<noteq> \<box> \<Longrightarrow> q \<in> Q_inf_e \
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C \<noteq> \<box> \<Longrightarrow> q \<in> Q_inf_e \
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
C \<noteq> \<box>

goal (1 subgoal):
 1. C \<noteq> \<box> \<Longrightarrow> q \<in> Q_inf_e \
[PROOF STEP]
obtain q'' where r: "p = q'' \<or> (p, q'') |\<in>| (eps \)|\<^sup>+|" "q |\<in>| ta_der_strict \ C\<langle>Var q''\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q''. \<lbrakk>p = q'' \<or> (p, q'') |\<in>| (eps \)|\<^sup>+|; q |\<in>| ta_der_strict \ C\<langle>Var q''\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using ta_der_to_ta_strict[OF conjunct2[OF conjunct2[OF loop]] gr(2)]
[PROOF STATE]
proof (prove)
using this:
\<exists>q'. (p = q' \<or> (p, q') |\<in>| (eps \)|\<^sup>+|) \<and> q |\<in>| ta_der_strict \ C\<langle>Var q'\<rangle>

goal (1 subgoal):
 1. (\<And>q''. \<lbrakk>p = q'' \<or> (p, q'') |\<in>| (eps \)|\<^sup>+|; q |\<in>| ta_der_strict \ C\<langle>Var q''\<rangle>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = q'' \<or> (p, q'') |\<in>| (eps \)|\<^sup>+|
q |\<in>| ta_der_strict \ C\<langle>Var q''\<rangle>

goal (1 subgoal):
 1. C \<noteq> \<box> \<Longrightarrow> q \<in> Q_inf_e \
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = q'' \<or> (p, q'') |\<in>| (eps \)|\<^sup>+|
q |\<in>| ta_der_strict \ C\<langle>Var q''\<rangle>
[PROOF STEP]
have "(q'', q) \<in>  Q_inf \"
[PROOF STATE]
proof (prove)
using this:
p = q'' \<or> (p, q'') |\<in>| (eps \)|\<^sup>+|
q |\<in>| ta_der_strict \ C\<langle>Var q''\<rangle>

goal (1 subgoal):
 1. (q'', q) \<in> Q_inf \
[PROOF STEP]
using ta_der_Q_inf[of q \ _  q''] ctxt False
[PROOF STATE]
proof (prove)
using this:
p = q'' \<or> (p, q'') |\<in>| (eps \)|\<^sup>+|
q |\<in>| ta_der_strict \ C\<langle>Var q''\<rangle>
\<lbrakk>q |\<in>| ta_der_strict \ (map_funs_term lift_None_Some ?C\<langle>Var q''\<rangle>); ?C \<noteq> \<box>\<rbrakk> \<Longrightarrow> (q'', q) \<in> Q_inf \
C2 \<noteq> \<box>
C\<langle>s\<rangle> = term_of_gterm (gterm_to_None_Some u)
C2\<langle>v\<rangle> = s
C \<noteq> \<box>

goal (1 subgoal):
 1. (q'', q) \<in> Q_inf \
[PROOF STEP]
by auto (smt (z3) ctxt.simps(8) map_funs_term_ctxt_decomp map_term_of_gterm)+
[PROOF STATE]
proof (state)
this:
(q'', q) \<in> Q_inf \

goal (1 subgoal):
 1. C \<noteq> \<box> \<Longrightarrow> q \<in> Q_inf_e \
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(q'', q) \<in> Q_inf \
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(q'', q) \<in> Q_inf \

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
using r(1) cycle q_p
[PROOF STATE]
proof (prove)
using this:
(q'', q) \<in> Q_inf \
p = q'' \<or> (p, q'') |\<in>| (eps \)|\<^sup>+|
(q', q') \<in> Q_inf \
(q', p) \<in> Q_inf \

goal (1 subgoal):
 1. q \<in> Q_inf_e \
[PROOF STEP]
by (auto simp: Q_inf_ta_eps_Q_inf intro!: exI[of _ q'])
         (meson Q_inf.trans Q_inf_ta_eps_Q_inf)+
[PROOF STATE]
proof (state)
this:
q \<in> Q_inf_e \

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Q_infty_fQ_inf_e_conv:
  assumes "gta_lang Q \ \<subseteq> {gpair s t| s t. funas_gterm s \<subseteq> fset \<F> \<and> funas_gterm t \<subseteq> fset \<F>}"
   and "\<Q> \ |\<subseteq>| ta_reachable \" and "\<Q> \ |\<subseteq>| ta_productive Q \"
  shows "Q_infty \ \<F> = fQ_inf_e \"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q_infty \ \<F> = fQ_inf_e \
[PROOF STEP]
using Q_inf_impl_Q_inf_exec Q_inf_exec_impl_Q_inf[OF assms]
[PROOF STATE]
proof (prove)
using this:
?q |\<in>| Q_infty ?\ ?\<F> \<Longrightarrow> ?q \<in> Q_inf_e ?\
?q \<in> Q_inf_e \ \<Longrightarrow> ?q |\<in>| Q_infty \ \<F>

goal (1 subgoal):
 1. Q_infty \ \<F> = fQ_inf_e \
[PROOF STEP]
by (auto simp: fQ_inf_e.rep_eq fmember.rep_eq) fastforce


[STATEMENT]
lemma Inf_reg_impl_sound:
  assumes "\<L> \<A> \<subseteq> {gpair s t| s t. funas_gterm s \<subseteq> fset \<F> \<and> funas_gterm t \<subseteq> fset \<F>}"
   and "\<Q>\<^sub>r \<A> |\<subseteq>| ta_reachable (ta \<A>)" and "\<Q>\<^sub>r \<A> |\<subseteq>| ta_productive (fin \<A>) (ta \<A>)"
  shows "\<L> (Inf_reg_impl \<A>) = \<L> (Inf_reg \<A> (Q_infty (ta \<A>) \<F>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<L> (Inf_reg_impl \<A>) = \<L> (Inf_reg \<A> (Q_infty (ta \<A>) \<F>))
[PROOF STEP]
using Q_infty_fQ_inf_e_conv[of "fin \<A>" "ta \<A>" \<F>] assms[unfolded \<L>_def]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>gta_lang (fin \<A>) (ta \<A>) \<subseteq> {gpair s t |s t. funas_gterm s \<subseteq> fset \<F> \<and> funas_gterm t \<subseteq> fset \<F>}; \<Q>\<^sub>r \<A> |\<subseteq>| ta_reachable (ta \<A>); \<Q>\<^sub>r \<A> |\<subseteq>| ta_productive (fin \<A>) (ta \<A>)\<rbrakk> \<Longrightarrow> Q_infty (ta \<A>) \<F> = fQ_inf_e (ta \<A>)
gta_lang (fin \<A>) (ta \<A>) \<subseteq> {gpair s t |s t. funas_gterm s \<subseteq> fset \<F> \<and> funas_gterm t \<subseteq> fset \<F>}
\<Q>\<^sub>r \<A> |\<subseteq>| ta_reachable (ta \<A>)
\<Q>\<^sub>r \<A> |\<subseteq>| ta_productive (fin \<A>) (ta \<A>)

goal (1 subgoal):
 1. \<L> (Inf_reg_impl \<A>) = \<L> (Inf_reg \<A> (Q_infty (ta \<A>) \<F>))
[PROOF STEP]
by (simp add: Inf_reg_impl_def)


[STATEMENT]
lemma (in state_space)"\<Gamma>\<turnstile> \<lbrace>\<acute>N = n\<rbrace> LOC \<acute>N :== 10;; \<acute>N :== \<acute>N + 2 COL \<lbrace>\<acute>N = n\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>N = n\<rbrace>  LOC \<acute>N :== 10;; \<acute>N :== \<acute>N + 2 COL \<lbrace>\<acute>N = n\<rbrace>
[PROOF STEP]
by vcg


[STATEMENT]
lemma (in state_space) "\<Gamma>\<turnstile> {|\<acute>N = 5|} \<acute>N :== 2 * \<acute>N {|\<acute>N = 10|}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> \<acute>N :== 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>
[PROOF STEP]
apply (rule HoarePartial.Basic)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<acute>N = 5\<rbrace> \<subseteq> {s. s\<lparr>locals := update project_Nat_nat inject_Nat_nat N_' (K_statefun (2 * lookup project_Nat_nat N_' (locals s))) (locals s)\<rparr> \<in> \<lbrace>\<acute>N = 10\<rbrace>}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space) "\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>N :== 10 \<lbrace>\<acute>N = 10\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>N :== 10 \<lbrace>\<acute>N = 10\<rbrace>
[PROOF STEP]
by vcg


[STATEMENT]
lemma (in state_space) "\<Gamma>\<turnstile> \<lbrace>2 * \<acute>N = 10\<rbrace> \<acute>N :== 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>2 * \<acute>N = 10\<rbrace> \<acute>N :== 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>
[PROOF STEP]
by vcg


[STATEMENT]
lemma (in state_space) "\<Gamma>\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> \<acute>N :== 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> \<acute>N :== 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N. N = 5 \<Longrightarrow> 2 * N = 10
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space) "\<Gamma>\<turnstile> \<lbrace>\<acute>N + 1 = a + 1\<rbrace> \<acute>N :== \<acute>N + 1 \<lbrace>\<acute>N = a + 1\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>N + 1 = a + 1\<rbrace> \<acute>N :== \<acute>N + 1 \<lbrace>\<acute>N = a + 1\<rbrace>
[PROOF STEP]
by vcg


[STATEMENT]
lemma (in state_space) "\<Gamma>\<turnstile> \<lbrace>\<acute>N = a\<rbrace> \<acute>N :== \<acute>N + 1 \<lbrace>\<acute>N = a + 1\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>N = a\<rbrace> \<acute>N :== \<acute>N + 1 \<lbrace>\<acute>N = a + 1\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N. N + 1 = N + 1
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>a = a \<and> b = b\<rbrace> \<acute>M :== a;; \<acute>N :== b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>a = a \<and> b = b\<rbrace> \<acute>M :== a;; \<acute>N :== b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
[PROOF STEP]
by vcg


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>M :== a;; \<acute>N :== b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>M :== a;; \<acute>N :== b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
[PROOF STEP]
by vcg


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
                \<acute>I :== \<acute>M;; \<acute>M :== \<acute>N;; \<acute>N :== \<acute>I
              \<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace> \<acute>I :== \<acute>M;; \<acute>M :== \<acute>N;; \<acute>N :== \<acute>I \<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M N. N = N \<and> M = M
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>
               \<acute>I :== \<acute>M;; \<acute>M :== \<acute>N;; \<acute>N :== \<acute>I
              \<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace> \<acute>I :== \<acute>M;; \<acute>M :== \<acute>N;; \<acute>N :== \<acute>I \<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>
[PROOF STEP]
apply vcg_step
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace> \<acute>I :== \<acute>M;; \<acute>M :== \<acute>N \<lbrace>\<acute>M = b \<and> \<acute>I = a\<rbrace>
[PROOF STEP]
apply vcg_step
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace> \<acute>I :== \<acute>M \<lbrace>\<acute>N = b \<and> \<acute>I = a\<rbrace>
[PROOF STEP]
apply vcg_step
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace> \<subseteq> \<lbrace>\<acute>N = b \<and> \<acute>M = a\<rbrace>
[PROOF STEP]
apply vcg_step
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M N. N = N \<and> M = M
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
have "\<lbrace>\<acute>M = \<acute>N\<rbrace> \<subseteq> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<acute>M = \<acute>N\<rbrace> \<subseteq> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrace>\<acute>M = \<acute>N\<rbrace> \<subseteq> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrace>\<acute>M = \<acute>N\<rbrace> \<subseteq> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
have "\<Gamma>\<turnstile> \<dots> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
by vcg
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
have "\<And>m n::nat. m = n \<longrightarrow> m + 1 \<noteq> n"
      \<comment> \<open>inclusion of assertions expressed in ``pure'' logic,\<close>
      \<comment> \<open>without mentioning the state space\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m n. m = n \<longrightarrow> m + 1 \<noteq> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?m = ?n \<longrightarrow> ?m + 1 \<noteq> ?n

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
?m = ?n \<longrightarrow> ?m + 1 \<noteq> ?n

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
have "\<Gamma>\<turnstile> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
by vcg
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M N. M = N \<Longrightarrow> M + 1 \<noteq> N
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
      WHILE \<acute>M \<noteq> a
      DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD
      \<lbrace>\<acute>S = a * b\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
let "\<Gamma>\<turnstile> _ ?while _" = ?thesis
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
let "\<lbrace>\<acute>?inv\<rbrace>" = "\<lbrace>\<acute>S = \<acute>M * b\<rbrace>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
have "\<lbrace>\<acute>M = 0 & \<acute>S = 0\<rbrace> \<subseteq> \<lbrace>\<acute>?inv\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> \<subseteq> \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> \<subseteq> \<lbrace>\<acute>S = \<acute>M * b\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> \<subseteq> \<lbrace>\<acute>S = \<acute>M * b\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
have "\<Gamma>\<turnstile> \<dots> ?while \<lbrace>\<acute>?inv \<and> \<not> (\<acute>M \<noteq> a)\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S = \<acute>M * b\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = \<acute>M * b \<and> \<not> \<acute>M \<noteq> a\<rbrace>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S = \<acute>M * b \<and> \<acute>M \<noteq> a\<rbrace> \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
[PROOF STEP]
let ?c = "\<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S = \<acute>M * b \<and> \<acute>M \<noteq> a\<rbrace> \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
[PROOF STEP]
have "\<lbrace>\<acute>?inv \<and> \<acute>M \<noteq> a\<rbrace> \<subseteq> \<lbrace>\<acute>S + b = (\<acute>M + 1) * b\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<acute>S = \<acute>M * b \<and> \<acute>M \<noteq> a\<rbrace> \<subseteq> \<lbrace>\<acute>S + b = (\<acute>M + 1) * b\<rbrace>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrace>\<acute>S = \<acute>M * b \<and> \<acute>M \<noteq> a\<rbrace> \<subseteq> \<lbrace>\<acute>S + b = (\<acute>M + 1) * b\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S = \<acute>M * b \<and> \<acute>M \<noteq> a\<rbrace> \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lbrace>\<acute>S = \<acute>M * b \<and> \<acute>M \<noteq> a\<rbrace> \<subseteq> \<lbrace>\<acute>S + b = (\<acute>M + 1) * b\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S = \<acute>M * b \<and> \<acute>M \<noteq> a\<rbrace> \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
[PROOF STEP]
have "\<Gamma>\<turnstile> \<dots> ?c \<lbrace>\<acute>?inv\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S + b = (\<acute>M + 1) * b\<rbrace> \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
[PROOF STEP]
by vcg
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>\<acute>S + b = (\<acute>M + 1) * b\<rbrace> \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>S = \<acute>M * b\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S = \<acute>M * b \<and> \<acute>M \<noteq> a\<rbrace> \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<lbrace>\<acute>S = \<acute>M * b \<and> \<acute>M \<noteq> a\<rbrace> \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
[PROOF STEP]
show "\<Gamma>\<turnstile> \<lbrace>\<acute>?inv \<and> \<acute>M \<noteq> a\<rbrace> ?c \<lbrace>\<acute>?inv\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<lbrace>\<acute>S = \<acute>M * b \<and> \<acute>M \<noteq> a\<rbrace> \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>S = \<acute>M * b\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S = \<acute>M * b \<and> \<acute>M \<noteq> a\<rbrace> \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>\<acute>S = \<acute>M * b \<and> \<acute>M \<noteq> a\<rbrace> \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>S = \<acute>M * b\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>\<acute>S = \<acute>M * b\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = \<acute>M * b \<and> \<not> \<acute>M \<noteq> a\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>\<acute>S = \<acute>M * b\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = \<acute>M * b \<and> \<not> \<acute>M \<noteq> a\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
have "\<lbrace>\<acute>?inv \<and> \<not> (\<acute>M \<noteq> a)\<rbrace> \<subseteq> \<lbrace>\<acute>S = a * b\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<acute>S = \<acute>M * b \<and> \<not> \<acute>M \<noteq> a\<rbrace> \<subseteq> \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrace>\<acute>S = \<acute>M * b \<and> \<not> \<acute>M \<noteq> a\<rbrace> \<subseteq> \<lbrace>\<acute>S = a * b\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
{} \<subseteq> ?A \<Longrightarrow> \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = a * b\<rbrace>,?A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{} \<subseteq> ?A \<Longrightarrow> \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = a * b\<rbrace>,?A

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> WHILE \<acute>M \<noteq> a DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = a * b\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
          WHILE \<acute>M \<noteq> a
          INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
          DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD
          \<lbrace>\<acute>S = a * b\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> WHILE \<acute>M \<noteq> a INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace> DO \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>M S. \<lbrakk>M = 0; S = 0\<rbrakk> \<Longrightarrow> S = M * b
 2. \<And>M S. \<lbrakk>S = M * b; M \<noteq> a\<rbrakk> \<Longrightarrow> S + b = (M + 1) * b
 3. \<And>M S. \<lbrakk>S = M * b; \<not> M \<noteq> a\<rbrakk> \<Longrightarrow> S = a * b
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
          TRY
            WHILE True
            INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
            DO IF \<acute>M = a THEN THROW ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 FI OD
          CATCH
            SKIP
          END
          \<lbrace>\<acute>S = a * b\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> TRY WHILE True INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace> DO IF \<acute>M = a THEN THROW ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 FI OD CATCH SKIP END \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>M S. \<lbrakk>M = 0; S = 0\<rbrakk> \<Longrightarrow> S = M * b
 2. \<And>M S. \<lbrakk>S = M * b; True\<rbrakk> \<Longrightarrow> (M = a \<longrightarrow> S = a * b) \<and> (M \<noteq> a \<longrightarrow> S + b = (M + 1) * b)
 3. \<And>M S. \<lbrakk>S = M * b; \<not> True\<rbrakk> \<Longrightarrow> S = a * b
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
          TRY
            WHILE True
            INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
            DO IF \<acute>M = a THEN \<acute>Abr :== ''Break'';;THROW
               ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1
               FI
            OD
          CATCH
            IF \<acute>Abr = ''Break'' THEN SKIP ELSE Throw FI
          END
          \<lbrace>\<acute>S = a * b\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> TRY WHILE True INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace> DO IF \<acute>M = a THEN \<acute>Abr :== ''Break'';; THROW ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 FI OD CATCH IF \<acute>Abr = ''Break'' THEN SKIP ELSE THROW FI END \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>M S. \<lbrakk>M = 0; S = 0\<rbrakk> \<Longrightarrow> S = M * b
 2. \<And>M S. \<lbrakk>S = M * b; True\<rbrakk> \<Longrightarrow> (M = a \<longrightarrow> (''Break'' = ''Break'' \<longrightarrow> S = a * b) \<and> (''Break'' \<noteq> ''Break'' \<longrightarrow> False)) \<and> (M \<noteq> a \<longrightarrow> S + b = (M + 1) * b)
 3. \<And>M S. \<lbrakk>S = M * b; \<not> True\<rbrakk> \<Longrightarrow> S = a * b
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
          \<lbrace>\<acute>Abr = ''Break''\<rbrace>\<bullet> WHILE True INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
           DO IF \<acute>M = a THEN RAISE \<acute>Abr :== ''Break''
              ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1
              FI
           OD
          \<lbrace>\<acute>S = a * b\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> \<lbrace>\<acute>Abr = ''Break''\<rbrace>\<bullet>WHILE True INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace> DO IF \<acute>M = a THEN RAISE \<acute>Abr :== ''Break'' ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 FI OD \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>M S. \<lbrakk>M = 0; S = 0\<rbrakk> \<Longrightarrow> S = M * b
 2. \<And>M S. \<lbrakk>S = M * b; True\<rbrakk> \<Longrightarrow> (M = a \<longrightarrow> S = a * b) \<and> (M \<noteq> a \<longrightarrow> S + b = (M + 1) * b)
 3. \<And>M S. \<lbrakk>S = M * b; \<not> True\<rbrakk> \<Longrightarrow> S = a * b
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
          TRY
            WHILE True
            INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
            DO IF \<acute>M = a THEN RAISE \<acute>Abr :== ''Break''
               ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1
               FI
            OD
          CATCH
            IF \<acute>Abr = ''Break'' THEN SKIP ELSE Throw FI
          END
          \<lbrace>\<acute>S = a * b\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> TRY WHILE True INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace> DO IF \<acute>M = a THEN RAISE \<acute>Abr :== ''Break'' ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 FI OD CATCH IF \<acute>Abr = ''Break'' THEN SKIP ELSE THROW FI END \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>M S. \<lbrakk>M = 0; S = 0\<rbrakk> \<Longrightarrow> S = M * b
 2. \<And>M S. \<lbrakk>S = M * b; True\<rbrakk> \<Longrightarrow> (M = a \<longrightarrow> S = a * b) \<and> (M \<noteq> a \<longrightarrow> S + b = (M + 1) * b)
 3. \<And>M S. \<lbrakk>S = M * b; \<not> True\<rbrakk> \<Longrightarrow> S = a * b
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>
          \<lbrace>\<acute>Abr = ''Break''\<rbrace> \<bullet> WHILE True
          INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace>
          DO IF \<acute>M = a THEN RAISE \<acute>Abr :== ''Break''
               ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1
               FI
          OD
          \<lbrace>\<acute>S = a * b\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> \<lbrace>\<acute>Abr = ''Break''\<rbrace>\<bullet>WHILE True INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace> DO IF \<acute>M = a THEN RAISE \<acute>Abr :== ''Break'' ELSE \<acute>S :== \<acute>S + b;; \<acute>M :== \<acute>M + 1 FI OD \<lbrace>\<acute>S = a * b\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>M S. \<lbrakk>M = 0; S = 0\<rbrakk> \<Longrightarrow> S = M * b
 2. \<And>M S. \<lbrakk>S = M * b; True\<rbrakk> \<Longrightarrow> (M = a \<longrightarrow> S = a * b) \<and> (M \<noteq> a \<longrightarrow> S + b = (M + 1) * b)
 3. \<And>M S. \<lbrakk>S = M * b; \<not> True\<rbrakk> \<Longrightarrow> S = a * b
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma  (in state_space)
  shows "\<Gamma>\<turnstile>\<lbrace>\<acute>I = i\<rbrace> LOC \<acute>I;; \<acute>I :== 2  COL \<lbrace>\<acute>I \<le> i\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>I = i\<rbrace>  LOC \<acute>I;; \<acute>I :== 2 COL \<lbrace>\<acute>I \<le> i\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I. I \<le> I
[PROOF STEP]
by simp


[STATEMENT]
theorem (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
           \<acute>S :== 0;; \<acute>I :== 1;;
           WHILE \<acute>I \<noteq> n
           DO
             \<acute>S :== \<acute>S + \<acute>I;;
             \<acute>I :== \<acute>I + 1
           OD
           \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>"
  (is "\<Gamma>\<turnstile> _ (_;; ?while) _")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
let ?sum = "\<lambda>k. SUMM j<k. j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
let ?inv = "\<lambda>s i. s = ?sum i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
have "\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
have "True \<longrightarrow> 0 = ?sum 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. True \<longrightarrow> 0 = (SUMM j<1. j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
True \<longrightarrow> 0 = (SUMM j<1. j)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
True \<longrightarrow> 0 = (SUMM j<1. j)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
have "\<Gamma>\<turnstile> \<lbrace>\<dots>\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>0 = (SUMM j<1. j)\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
by vcg
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>0 = (SUMM j<1. j)\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
have "\<Gamma>\<turnstile> \<lbrace>?inv \<acute>S \<acute>I\<rbrace> ?while \<lbrace>?inv \<acute>S \<acute>I \<and> \<not> \<acute>I \<noteq> n\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace> WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<\<acute>I. j) \<and> \<not> \<acute>I \<noteq> n\<rbrace>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S = (SUMM j<\<acute>I. j) \<and> \<acute>I \<noteq> n\<rbrace> \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
let ?body = "\<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S = (SUMM j<\<acute>I. j) \<and> \<acute>I \<noteq> n\<rbrace> \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
have "\<And>s i. ?inv s i \<and> i \<noteq> n \<longrightarrow>  ?inv (s + i) (i + 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s i. s = (SUMM j<i. j) \<and> i \<noteq> n \<longrightarrow> s + i = (SUMM j<i + 1. j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?s1 = (SUMM j<?i1. j) \<and> ?i1 \<noteq> n \<longrightarrow> ?s1 + ?i1 = (SUMM j<?i1 + 1. j)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S = (SUMM j<\<acute>I. j) \<and> \<acute>I \<noteq> n\<rbrace> \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
?s1 = (SUMM j<?i1. j) \<and> ?i1 \<noteq> n \<longrightarrow> ?s1 + ?i1 = (SUMM j<?i1 + 1. j)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S = (SUMM j<\<acute>I. j) \<and> \<acute>I \<noteq> n\<rbrace> \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
have "\<Gamma>\<turnstile> \<lbrace>\<acute>S + \<acute>I = ?sum (\<acute>I + 1)\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S + \<acute>I = (SUMM j<\<acute>I + 1. j)\<rbrace> \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
by vcg
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>\<acute>S + \<acute>I = (SUMM j<\<acute>I + 1. j)\<rbrace> \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S = (SUMM j<\<acute>I. j) \<and> \<acute>I \<noteq> n\<rbrace> \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<lbrace>\<acute>S = (SUMM j<\<acute>I. j) \<and> \<acute>I \<noteq> n\<rbrace> \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
show "\<Gamma>\<turnstile> \<lbrace>?inv \<acute>S \<acute>I \<and> \<acute>I \<noteq> n\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>"
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<lbrace>\<acute>S = (SUMM j<\<acute>I. j) \<and> \<acute>I \<noteq> n\<rbrace> \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>S = (SUMM j<\<acute>I. j) \<and> \<acute>I \<noteq> n\<rbrace> \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>\<acute>S = (SUMM j<\<acute>I. j) \<and> \<acute>I \<noteq> n\<rbrace> \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace> WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<\<acute>I. j) \<and> \<not> \<acute>I \<noteq> n\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace> WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<\<acute>I. j) \<and> \<not> \<acute>I \<noteq> n\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
have "\<And>s i. s = ?sum i \<and> \<not> i \<noteq> n \<longrightarrow> s = ?sum n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s i. s = (SUMM j<i. j) \<and> \<not> i \<noteq> n \<longrightarrow> s = (SUMM j<n. j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?s = (SUMM j<?i. j) \<and> \<not> ?i \<noteq> n \<longrightarrow> ?s = (SUMM j<n. j)

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
           \<acute>S :== 0;; \<acute>I :== 1;;
           WHILE \<acute>I \<noteq> n
           INV \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
           DO
             \<acute>S :== \<acute>S + \<acute>I;;
             \<acute>I :== \<acute>I + 1
           OD
          \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n INV \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace> DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n INV \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace> DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
let ?sum = "\<lambda>k. SUMM j<k. j"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n INV \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace> DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
let ?inv = "\<lambda>s i. s = ?sum i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n INV \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace> DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n INV \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace> DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
proof vcg
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. True \<Longrightarrow> 0 = (SUMM j<1. j)
 2. \<And>I S. \<lbrakk>S = (SUMM j<I. j); I \<noteq> n\<rbrakk> \<Longrightarrow> S + I = (SUMM j<I + 1. j)
 3. \<And>I S. \<lbrakk>S = (SUMM j<I. j); \<not> I \<noteq> n\<rbrakk> \<Longrightarrow> S = (SUMM j<n. j)
[PROOF STEP]
show "?inv 0 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 = (SUMM j<1. j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 = (SUMM j<1. j)

goal (2 subgoals):
 1. \<And>I S. \<lbrakk>S = (SUMM j<I. j); I \<noteq> n\<rbrakk> \<Longrightarrow> S + I = (SUMM j<I + 1. j)
 2. \<And>I S. \<lbrakk>S = (SUMM j<I. j); \<not> I \<noteq> n\<rbrakk> \<Longrightarrow> S = (SUMM j<n. j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>I S. \<lbrakk>S = (SUMM j<I. j); I \<noteq> n\<rbrakk> \<Longrightarrow> S + I = (SUMM j<I + 1. j)
 2. \<And>I S. \<lbrakk>S = (SUMM j<I. j); \<not> I \<noteq> n\<rbrakk> \<Longrightarrow> S = (SUMM j<n. j)
[PROOF STEP]
fix i s
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>I S. \<lbrakk>S = (SUMM j<I. j); I \<noteq> n\<rbrakk> \<Longrightarrow> S + I = (SUMM j<I + 1. j)
 2. \<And>I S. \<lbrakk>S = (SUMM j<I. j); \<not> I \<noteq> n\<rbrakk> \<Longrightarrow> S = (SUMM j<n. j)
[PROOF STEP]
assume "?inv s i" "i \<noteq> n"
[PROOF STATE]
proof (state)
this:
s = (SUMM j<i. j)
i \<noteq> n

goal (2 subgoals):
 1. \<And>I S. \<lbrakk>S = (SUMM j<I. j); I \<noteq> n\<rbrakk> \<Longrightarrow> S + I = (SUMM j<I + 1. j)
 2. \<And>I S. \<lbrakk>S = (SUMM j<I. j); \<not> I \<noteq> n\<rbrakk> \<Longrightarrow> S = (SUMM j<n. j)
[PROOF STEP]
thus "?inv (s + i) (i + 1)"
[PROOF STATE]
proof (prove)
using this:
s = (SUMM j<i. j)
i \<noteq> n

goal (1 subgoal):
 1. s + i = (SUMM j<i + 1. j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s + i = (SUMM j<i + 1. j)

goal (1 subgoal):
 1. \<And>I S. \<lbrakk>S = (SUMM j<I. j); \<not> I \<noteq> n\<rbrakk> \<Longrightarrow> S = (SUMM j<n. j)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I S. \<lbrakk>S = (SUMM j<I. j); \<not> I \<noteq> n\<rbrakk> \<Longrightarrow> S = (SUMM j<n. j)
[PROOF STEP]
fix i s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>I S. \<lbrakk>S = (SUMM j<I. j); \<not> I \<noteq> n\<rbrakk> \<Longrightarrow> S = (SUMM j<n. j)
[PROOF STEP]
assume x: "?inv s i" "\<not> i \<noteq> n"
[PROOF STATE]
proof (state)
this:
s = (SUMM j<i. j)
\<not> i \<noteq> n

goal (1 subgoal):
 1. \<And>I S. \<lbrakk>S = (SUMM j<I. j); \<not> I \<noteq> n\<rbrakk> \<Longrightarrow> S = (SUMM j<n. j)
[PROOF STEP]
thus "s = ?sum n"
[PROOF STATE]
proof (prove)
using this:
s = (SUMM j<i. j)
\<not> i \<noteq> n

goal (1 subgoal):
 1. s = (SUMM j<n. j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
s = (SUMM j<n. j)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n INV \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace> DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>True\<rbrace>
           \<acute>S :== 0;; \<acute>I :== 1;;
           WHILE \<acute>I \<noteq> n
           INV \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace>
           DO
             \<acute>S :== \<acute>S + \<acute>I;;
             \<acute>I :== \<acute>I + 1
           OD
           \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> \<acute>S :== 0;; \<acute>I :== 1;; WHILE \<acute>I \<noteq> n INV \<lbrace>\<acute>S = (SUMM j<\<acute>I. j)\<rbrace> DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>I :== \<acute>I + 1 OD \<lbrace>\<acute>S = (SUMM j<n. j)\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. True \<Longrightarrow> 0 = (SUMM j<1. j)
 2. \<And>I S. \<lbrakk>S = (SUMM j<I. j); I \<noteq> n\<rbrakk> \<Longrightarrow> S + I = (SUMM j<I + 1. j)
 3. \<And>I S. \<lbrakk>S = (SUMM j<I. j); \<not> I \<noteq> n\<rbrakk> \<Longrightarrow> S = (SUMM j<n. j)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> SWITCH \<acute>B
                        {True} \<Rightarrow> \<acute>N :== 6
                      | {False} \<Rightarrow> \<acute>N :== 7
                     END
          \<lbrace>\<acute>N > 5\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>N = 5\<rbrace>  SWITCH \<acute>B {True}\<Rightarrow> \<acute>N :== 6 | {False}\<Rightarrow> \<acute>N :== 7 END \<lbrace>5 < \<acute>N\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>B N. N = 5 \<Longrightarrow> (True = B \<longrightarrow> 5 < 6) \<and> (True \<noteq> B \<longrightarrow> (False = B \<longrightarrow> 5 < 7) \<and> (False \<noteq> B \<longrightarrow> 5 < N))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space)
  shows "\<Gamma>\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> SWITCH \<acute>N
                        {v. v < 5} \<Rightarrow> \<acute>N :== 6
                      | {v. v \<ge> 5} \<Rightarrow> \<acute>N :== 7
                     END
          \<lbrace>\<acute>N > 5\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>\<acute>N = 5\<rbrace>  SWITCH \<acute>N {v. v < 5}\<Rightarrow> \<acute>N :== 6 | {v. 5 \<le> v}\<Rightarrow> \<acute>N :== 7 END \<lbrace>5 < \<acute>N\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N. N = 5 \<Longrightarrow> (N < 5 \<longrightarrow> 5 < 6) \<and> (\<not> N < 5 \<longrightarrow> (5 \<le> N \<longrightarrow> 5 < 7) \<and> (\<not> 5 \<le> N \<longrightarrow> 5 < N))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fac_simp [simp]: "0 < i \<Longrightarrow>  fac i = i * fac (i - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < i \<Longrightarrow> fac i = i * fac (i - 1)
[PROOF STEP]
by (cases i) simp_all


[STATEMENT]
lemma (in Fac_impl) Fac_spec':
  shows "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>{\<sigma>} PROC Fac(\<acute>N,\<acute>R) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
apply (hoare_rule HoarePartial.ProcRec1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N. (N = 0 \<longrightarrow> 1 = fac N) \<and> (N \<noteq> 0 \<longrightarrow> (\<forall>R. R = fac (N - 1) \<longrightarrow> N * fac (N - 1) = fac N))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Fac_impl) Fac_spec1:
  shows "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>{\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
apply (hoare_rule HoarePartial.ProcRec1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
apply vcg_step
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> (?P1.4 \<sigma>) \<acute>R :== 1 \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
 2. \<And>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> (?P2.4 \<sigma>) \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
 3. \<And>\<sigma>. {\<sigma>} \<subseteq> {s. (s \<in> \<lbrace>\<acute>N = 0\<rbrace> \<longrightarrow> s \<in> ?P1.4 \<sigma>) \<and> (s \<notin> \<lbrace>\<acute>N = 0\<rbrace> \<longrightarrow> s \<in> ?P2.4 \<sigma>)}
[PROOF STEP]
apply   vcg_step
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> (?P2.4 \<sigma>) \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
 2. \<And>\<sigma>. {\<sigma>} \<subseteq> {s. (s \<in> \<lbrace>\<acute>N = 0\<rbrace> \<longrightarrow> s \<in> \<lbrace>1 = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>) \<and> (s \<notin> \<lbrace>\<acute>N = 0\<rbrace> \<longrightarrow> s \<in> ?P2.4 \<sigma>)}
[PROOF STEP]
apply  vcg_step
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> (?P2.4 \<sigma>) \<acute>R :== CALL Fac(\<acute>N - 1) \<lbrace>\<acute>N * \<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
 2. \<And>\<sigma>. {\<sigma>} \<subseteq> {s. (s \<in> \<lbrace>\<acute>N = 0\<rbrace> \<longrightarrow> s \<in> \<lbrace>1 = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>) \<and> (s \<notin> \<lbrace>\<acute>N = 0\<rbrace> \<longrightarrow> s \<in> ?P2.4 \<sigma>)}
[PROOF STEP]
apply vcg_step
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {\<sigma>} \<subseteq> {s. (s \<in> \<lbrace>\<acute>N = 0\<rbrace> \<longrightarrow> s \<in> \<lbrace>1 = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>) \<and> (s \<notin> \<lbrace>\<acute>N = 0\<rbrace> \<longrightarrow> s \<in> \<lbrace>\<forall>t. \<^bsup>t\<^esup>R = fac (\<acute>N - 1) \<longrightarrow> \<acute>N * fac (\<acute>N - 1) = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>)}
[PROOF STEP]
apply vcg_step
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N. (N = 0 \<longrightarrow> 1 = fac N) \<and> (N \<noteq> 0 \<longrightarrow> (\<forall>R. R = fac (N - 1) \<longrightarrow> N * fac (N - 1) = fac N))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in Fac_impl) Fac_spec2:

  shows "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>{\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
proof (hoare_rule HoarePartial.ProcRec1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
have Fac_spec: "\<forall>\<sigma>. \<Gamma>,(\<Theta>\<union>(\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>,{})}))
                       \<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
apply (rule hoarep.Asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. ({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {}) \<in> \<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>

goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
show "\<forall>\<sigma>. \<Gamma>,(\<Theta>\<union>(\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>,{})}))
            \<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1
            ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N. (N = 0 \<longrightarrow> 1 = fac N) \<and> (N \<noteq> 0 \<longrightarrow> (\<forall>R. R = fac (N - 1) \<longrightarrow> N * fac (N - 1) = fac N))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Fac_impl) Fac_spec3:
  shows "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>{\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>"
  (is "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>(?Pre \<sigma>) ?Fac (?Post \<sigma>)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
proof (hoare_rule HoarePartial.ProcRec1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
have Fac_spec: "\<forall>\<sigma>. \<Gamma>,(\<Theta>\<union>(\<Union>\<sigma>. {(?Pre \<sigma>, Fac_'proc, ?Post \<sigma>,{})}))
                       \<turnstile>(?Pre \<sigma>) ?Fac (?Post \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
apply (rule allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
apply (rule hoarep.Asm)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. ({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {}) \<in> \<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>

goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
show "\<forall>\<sigma>. \<Gamma>,(\<Theta>\<union>(\<Union>\<sigma>. {(?Pre \<sigma>, Fac_'proc, ?Post \<sigma>,{})}))
            \<turnstile> (?Pre \<sigma>) IF \<acute>N = 0 THEN \<acute>R :== 1
            ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI (?Post \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N. (N = 0 \<longrightarrow> 1 = fac N) \<and> (N \<noteq> 0 \<longrightarrow> (\<forall>R. R = fac (N - 1) \<longrightarrow> N * fac (N - 1) = fac N))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in Fac_impl) Fac_spec4:
  shows "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>{\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>"
  (is "\<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile>(?Pre \<sigma>) ?Fac (?Post \<sigma>)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta>\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
proof (hoare_rule HoarePartial.ProcRec1)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
define \<Theta>' where "\<Theta>' = \<Theta> \<union> (\<Union>\<sigma>. {(?Pre \<sigma>, Fac_'proc, ?Post \<sigma>,{})})"
[PROOF STATE]
proof (state)
this:
\<Theta>' = \<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})

goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
have Fac_spec: "\<forall>\<sigma>. \<Gamma>,\<Theta>'\<turnstile>(?Pre \<sigma>) ?Fac (?Post \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta>'\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
by (unfold \<Theta>'_def, rule allI, rule hoarep.Asm) simp
[PROOF STATE]
proof (state)
this:
\<forall>\<sigma>. \<Gamma>,\<Theta>'\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>

goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
txt \<open>We have to name the fact \<open>Fac_spec\<close>, so that the vcg can
   use the specification for the recursive call, since it cannot infer it
   from the opaque @{term "\<Theta>'"}.\<close>
[PROOF STATE]
proof (state)
this:
\<forall>\<sigma>. \<Gamma>,\<Theta>'\<turnstile> {\<sigma>} \<acute>R :== PROC Fac(\<acute>N) \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>

goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta> \<union> (\<Union>\<sigma>. {({\<sigma>}, Fac_'proc, \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>, {})})\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
show "\<forall>\<sigma>. \<Gamma>,\<Theta>'\<turnstile> (?Pre \<sigma>) IF \<acute>N = 0 THEN \<acute>R :== 1
            ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI (?Post \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>,\<Theta>'\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>N. (N = 0 \<longrightarrow> 1 = fac N) \<and> (N \<noteq> 0 \<longrightarrow> (\<forall>R. R = fac (N - 1) \<longrightarrow> N * fac (N - 1) = fac N))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>\<sigma>. \<Gamma>,\<Theta>'\<turnstile> {\<sigma>} IF \<acute>N = 0 THEN \<acute>R :== 1 ELSE \<acute>R :== CALL Fac(\<acute>N - 1);; \<acute>R :== \<acute>N * \<acute>R FI \<lbrace>\<acute>R = fac \<^bsup>\<sigma>\<^esup>N\<rbrace>

goal:
No subgoals!
[PROOF STEP]
qed