[STATEMENT]
lemma (in igb_fr_graph) find_lasso_correct: "find_lasso \<le> find_lasso_spec"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_lasso \<le> find_lasso_spec
[PROOF STEP]
unfolding find_lasso_spec_def find_lasso_def find_ce_spec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> is_lasso_prpl prpl | Some (x, xa) \<Rightarrow> ce_correct x xa) \<bind> (\<lambda>ce. case ce of None \<Rightarrow> RETURN None | Some (Vr, Vl) \<Rightarrow> reconstruct_lasso Vr Vl \<bind> (\<lambda>l. RETURN (Some l))) \<le> SPEC (\<lambda>r. case r of None \<Rightarrow> \<forall>prpl. \<not> is_lasso_prpl prpl | Some x \<Rightarrow> is_lasso_prpl x)
[PROOF STEP]
apply (refine_rcg refine_vcg order_trans[OF reconstruct_lasso_correct])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>case x of None \<Rightarrow> \<forall>prpl. \<not> is_lasso_prpl prpl | Some (x, xa) \<Rightarrow> ce_correct x xa; x = None\<rbrakk> \<Longrightarrow> case None of None \<Rightarrow> \<forall>prpl. \<not> is_lasso_prpl prpl | Some x \<Rightarrow> is_lasso_prpl x
 2. \<And>x xa a b. \<lbrakk>case x of None \<Rightarrow> \<forall>prpl. \<not> is_lasso_prpl prpl | Some (x, xa) \<Rightarrow> ce_correct x xa; x = Some xa; xa = (a, b)\<rbrakk> \<Longrightarrow> ce_correct a b
 3. \<And>x xa a b xb. \<lbrakk>case x of None \<Rightarrow> \<forall>prpl. \<not> is_lasso_prpl prpl | Some (x, xa) \<Rightarrow> ce_correct x xa; x = Some xa; xa = (a, b); is_lasso_prpl xb\<rbrakk> \<Longrightarrow> case Some xb of None \<Rightarrow> \<forall>prpl. \<not> is_lasso_prpl prpl | Some x \<Rightarrow> is_lasso_prpl x
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done