[STATEMENT]
lemma hn_monadic_nfoldli_rl'[sepref_comb_rules]:
  assumes "INDEP Rk" "INDEP R\<sigma>"
  assumes FR: "P \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rk) s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>"
  assumes c_ref: "\<And>\<sigma> \<sigma>'. hn_refine
    (\<Gamma> * hn_ctxt R\<sigma> \<sigma>' \<sigma>)
    (c \<sigma>)
    (\<Gamma>c \<sigma>' \<sigma>)
    bool_assn
    (c' \<sigma>')"
  assumes C_FR:
    "\<And>\<sigma>' \<sigma>. TERM monadic_nfoldli \<Longrightarrow>
      \<Gamma>c \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt R\<sigma> \<sigma>' \<sigma>"

  assumes f_ref: "\<And>x' x \<sigma>' \<sigma>. \<lbrakk>x'\<in>set s'\<rbrakk> \<Longrightarrow> hn_refine
    (\<Gamma> * hn_ctxt Rk x' x * hn_ctxt R\<sigma> \<sigma>' \<sigma>)
    (f x \<sigma>)
    (\<Gamma>f x' x \<sigma>' \<sigma>) R\<sigma>
    (f' x' \<sigma>')"
  assumes F_FR: "\<And>x' x \<sigma>' \<sigma>. TERM monadic_nfoldli \<Longrightarrow> \<Gamma>f x' x \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t
    \<Gamma> * hn_ctxt Rk' x' x * hn_ctxt Pf\<sigma> \<sigma>' \<sigma>"

  assumes MERGE: "\<And>x x'. hn_ctxt Rk' x' x \<or>\<^sub>A hn_ctxt Rk x' x \<Longrightarrow>\<^sub>t hn_ctxt Rk'' x' x"

  shows "hn_refine
    P
    (imp_nfoldli s c f \<sigma>)
    (\<Gamma> * hn_ctxt (list_assn Rk'') s' s * hn_invalid R\<sigma> \<sigma>' \<sigma>)
    R\<sigma>
    ((monadic_nfoldli)
      $s'$(\<lambda>\<^sub>2\<sigma>'. c' \<sigma>')$(\<lambda>\<^sub>2x' \<sigma>'. f' x' \<sigma>')$\<sigma>'
    )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine P (imp_nfoldli s c f \<sigma>) (\<Gamma> * hn_ctxt (list_assn Rk'') s' s * hn_invalid R\<sigma> \<sigma>' \<sigma>) R\<sigma> (monadic_nfoldli $ s' $ (\<lambda>x. (#c' x#)) $ (\<lambda>x. (#\<lambda>xa. (#f' x xa#)#)) $ \<sigma>')
[PROOF STEP]
unfolding APP_def PROTECT2_def PR_CONST_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine P (imp_nfoldli s c f \<sigma>) (\<Gamma> * hn_ctxt (list_assn Rk'') s' s * hn_invalid R\<sigma> \<sigma>' \<sigma>) R\<sigma> (monadic_nfoldli s' c' f' \<sigma>')
[PROOF STEP]
apply1 (rule hn_refine_cons_pre[OF FR])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (\<Gamma> * hn_ctxt (list_assn Rk) s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>) (imp_nfoldli s c f \<sigma>) (\<Gamma> * hn_ctxt (list_assn Rk'') s' s * hn_invalid R\<sigma> \<sigma>' \<sigma>) R\<sigma> (monadic_nfoldli s' c' f' \<sigma>')
[PROOF STEP]
apply1 weaken_hnr_post
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (\<Gamma> * hn_ctxt (list_assn Rk) s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>) (imp_nfoldli s c f \<sigma>) (\<Gamma> * hn_ctxt (list_assn Rk'') s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma>) R\<sigma> (monadic_nfoldli s' c' f' \<sigma>')
[PROOF STEP]
applyF (rule hn_refine_cons[rotated])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. hn_refine ?P'13 (imp_nfoldli s c f \<sigma>) ?Q13 ?R13 (monadic_nfoldli s' c' f' \<sigma>')
 2. ?Q13 \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rk'') s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma>
 3. \<And>x y. ?R13 x y \<Longrightarrow>\<^sub>t R\<sigma> x y
 4. \<Gamma> * hn_ctxt (list_assn Rk) s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t ?P'13
[PROOF STEP]
applyF (rule monadic_nfoldli_refine_aux'[OF order_refl])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>s s'. hn_refine (?\<Gamma>19 * hn_ctxt ?R13 s' s) (c s) (?\<Gamma>19 * hn_ctxt ?R13 s' s) bool_assn (c' s')
 2. \<And>x x' s s'a. x' \<in> set s' \<Longrightarrow> hn_refine (?\<Gamma>19 * hn_ctxt ?Rl19 x' x * hn_ctxt ?R13 s'a s) (f x s) (?\<Gamma>19 * hn_ctxt ?Rl'19 x' x * hn_invalid ?R13 s'a s) ?R13 (f' x' s'a)
 3. \<And>x x'. hn_ctxt ?Rl'19 x' x \<or>\<^sub>A hn_ctxt ?Rl19 x' x \<Longrightarrow>\<^sub>t hn_ctxt ?Rl''19 x' x
[PROOF STEP]
focus
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. hn_refine (?\<Gamma>19 * hn_ctxt ?R13 s' s) (c s) (?\<Gamma>19 * hn_ctxt ?R13 s' s) bool_assn (c' s')
[PROOF STEP]
apply (rule hn_refine_cons_post)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. hn_refine (?\<Gamma>19 * hn_ctxt ?R13 s' s) (c s) (?Q25 s s') bool_assn (c' s')
 2. \<And>s s'. ?Q25 s s' \<Longrightarrow>\<^sub>t ?\<Gamma>19 * hn_ctxt ?R13 s' s
[PROOF STEP]
applyS (rule c_ref)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<Gamma>c s' s \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt R\<sigma> s' s
[PROOF STEP]
apply1 (rule entt_trans[OF C_FR[OF TERMI]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<Gamma> * hn_ctxt R\<sigma> s' s \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt R\<sigma> s' s
[PROOF STEP]
applyS (rule entt_refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x x' s s'a. x' \<in> set s' \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt ?Rl19 x' x * hn_ctxt R\<sigma> s'a s) (f x s) (\<Gamma> * hn_ctxt ?Rl'19 x' x * hn_invalid R\<sigma> s'a s) R\<sigma> (f' x' s'a)
 2. \<And>x x'. hn_ctxt ?Rl'19 x' x \<or>\<^sub>A hn_ctxt ?Rl19 x' x \<Longrightarrow>\<^sub>t hn_ctxt ?Rl''19 x' x
[PROOF STEP]
apply1 weaken_hnr_post
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x x' s s'a. x' \<in> set s' \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt ?Rl8 x' x * hn_ctxt R\<sigma> s'a s) (f x s) (\<Gamma> * hn_ctxt ?Rl'8 x' x * hn_ctxt (\<lambda>_ _. true) s'a s) R\<sigma> (f' x' s'a)
 2. \<And>x x'. hn_ctxt ?Rl'8 x' x \<or>\<^sub>A hn_ctxt ?Rl8 x' x \<Longrightarrow>\<^sub>t hn_ctxt ?Rl''8 x' x
[PROOF STEP]
applyF (rule hn_refine_cons_post)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x x' s s'a. x' \<in> set s' \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt ?Rl8 x' x * hn_ctxt R\<sigma> s'a s) (f x s) (?Q11 x x' s s'a) R\<sigma> (f' x' s'a)
 2. \<And>x x' s s'a. x' \<in> set s' \<Longrightarrow> ?Q11 x x' s s'a \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt ?Rl'8 x' x * hn_ctxt (\<lambda>_ _. true) s'a s
[PROOF STEP]
applyS (rule f_ref; simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x x' s s'a. x' \<in> set s' \<Longrightarrow> \<Gamma>f x' x s'a s \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt ?Rl'8 x' x * hn_ctxt (\<lambda>_ _. true) s'a s
[PROOF STEP]
apply1 (rule entt_trans[OF F_FR[OF TERMI]])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x x' s s'a. x' \<in> set s' \<Longrightarrow> \<Gamma> * hn_ctxt Rk' x' x * hn_ctxt Pf\<sigma> s'a s \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt ?Rl'8 x' x * hn_ctxt (\<lambda>_ _. true) s'a s
[PROOF STEP]
applyS (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x x'. hn_ctxt Rk' x' x \<or>\<^sub>A hn_ctxt Rk x' x \<Longrightarrow>\<^sub>t hn_ctxt ?Rl''8 x' x
[PROOF STEP]
apply (rule MERGE)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<Gamma> * hn_ctxt (list_assn Rk'') s' s * hn_invalid R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rk'') s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma>
 2. \<And>x y. R\<sigma> x y \<Longrightarrow>\<^sub>t R\<sigma> x y
 3. \<Gamma> * hn_ctxt (list_assn Rk) s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rk) s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>
[PROOF STEP]
applyS (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y. R\<sigma> x y \<Longrightarrow>\<^sub>t R\<sigma> x y
 2. \<Gamma> * hn_ctxt (list_assn Rk) s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rk) s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>
[PROOF STEP]
applyS (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma> * hn_ctxt (list_assn Rk) s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rk) s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>
[PROOF STEP]
applyS (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nfoldli_assert:
  assumes "set l \<subseteq> S"
  shows "nfoldli l c (\<lambda> x s. ASSERT (x \<in> S) \<then> f x s) s = nfoldli l c f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfoldli l c (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f x s)) s = nfoldli l c f s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set l \<subseteq> S

goal (1 subgoal):
 1. nfoldli l c (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f x s)) s = nfoldli l c f s
[PROOF STEP]
by (induction l arbitrary: s) (auto simp: pw_eq_iff refine_pw_simps)


[STATEMENT]
lemma fold_eq_nfoldli:
  "RETURN (fold f l s) = nfoldli l (\<lambda>_. True) (\<lambda>x s. RETURN (f x s)) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RETURN (fold f l s) = nfoldli l (\<lambda>_. True) (\<lambda>x s. RETURN (f x s)) s
[PROOF STEP]
apply (induction l arbitrary: s)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. RETURN (fold f [] s) = nfoldli [] (\<lambda>_. True) (\<lambda>x s. RETURN (f x s)) s
 2. \<And>a l s. (\<And>s. RETURN (fold f l s) = nfoldli l (\<lambda>_. True) (\<lambda>x s. RETURN (f x s)) s) \<Longrightarrow> RETURN (fold f (a # l) s) = nfoldli (a # l) (\<lambda>_. True) (\<lambda>x s. RETURN (f x s)) s
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma fold_eq_nfoldli_assert:
  "RETURN (fold f l s) = nfoldli l (\<lambda>_. True) (\<lambda>x s. ASSERT (x\<in>set l) \<then> RETURN (f x s)) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RETURN (fold f l s) = nfoldli l (\<lambda>_. True) (\<lambda>x s. ASSERT (x \<in> set l) \<bind> (\<lambda>_. RETURN (f x s))) s
[PROOF STEP]
by (simp add: nfoldli_assert' fold_eq_nfoldli)


[STATEMENT]
lemma fold_arity[sepref_monadify_arity]: "fold \<equiv> \<lambda>\<^sub>2f l s. SP fold$(\<lambda>\<^sub>2x s. f$x$s)$l$s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold \<equiv> \<lambda>x. (#\<lambda>xa. (#\<lambda>xb. (#SP fold $ (\<lambda>xa. (#\<lambda>xb. (#x $ xa $ xb#)#)) $ xa $ xb#)#)#)
[PROOF STEP]
by auto


[STATEMENT]
lemma monadify_plain_fold[sepref_monadify_comb]:
  "EVAL$(fold$(\<lambda>\<^sub>2x s. f x s)$l$s) \<equiv> (\<bind>)$(EVAL$l)$(\<lambda>\<^sub>2l. (\<bind>)$(EVAL$s)$(\<lambda>\<^sub>2s. nfoldli$l$(\<lambda>\<^sub>2_. True)$(\<lambda>\<^sub>2x s. EVAL$(f x s))$s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EVAL $ (fold $ (\<lambda>x. (#\<lambda>xa. (#f x xa#)#)) $ l $ s) \<equiv> (\<bind>) $ (EVAL $ l) $ (\<lambda>x. (#(\<bind>) $ (EVAL $ s) $ (\<lambda>xa. (#nfoldli $ x $ (\<lambda>x. (#True#)) $ (\<lambda>x. (#\<lambda>xa. (#EVAL $ f x xa#)#)) $ xa#))#))
[PROOF STEP]
by (simp add: fold_eq_nfoldli)


[STATEMENT]
lemma monadify_plain_fold_old_rl:
  "EVAL$(fold$(\<lambda>\<^sub>2x s. f x s)$l$s) \<equiv> (\<bind>)$(EVAL$l)$(\<lambda>\<^sub>2l. (\<bind>)$(EVAL$s)$(\<lambda>\<^sub>2s. nfoldli$l$(\<lambda>\<^sub>2_. True)$(\<lambda>\<^sub>2x s. PR_CONST (op_ASSERT_bind (x\<in>set l))$(EVAL$(f x s)))$s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EVAL $ (fold $ (\<lambda>x. (#\<lambda>xa. (#f x xa#)#)) $ l $ s) \<equiv> (\<bind>) $ (EVAL $ l) $ (\<lambda>x. (#(\<bind>) $ (EVAL $ s) $ (\<lambda>xa. (#nfoldli $ x $ (\<lambda>x. (#True#)) $ (\<lambda>xa. (#\<lambda>xb. (#PR_CONST (op_ASSERT_bind (xa \<in> set x)) $ (EVAL $ f xa xb)#)#)) $ xa#))#))
[PROOF STEP]
by (simp add: fold_eq_nfoldli_assert)


[STATEMENT]
lemma foldli_eq_nfoldli:
  "RETURN (foldli l c f s) = nfoldli l c (\<lambda>x s. RETURN (f x s)) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. RETURN (foldli l c f s) = nfoldli l c (\<lambda>x s. RETURN (f x s)) s
[PROOF STEP]
by (induction l arbitrary: s) auto


[STATEMENT]
lemma foldli_arities[sepref_monadify_arity]:
  "foldli \<equiv> \<lambda>\<^sub>2s c f \<sigma>. SP (foldli)$s$(\<lambda>\<^sub>2x. c$x)$(\<lambda>\<^sub>2x \<sigma>. f$x$\<sigma>)$\<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. foldli \<equiv> \<lambda>x. (#\<lambda>xa. (#\<lambda>xb. (#\<lambda>xc. (#SP foldli $ x $ (\<lambda>x. (#xa $ x#)) $ (\<lambda>x. (#\<lambda>xa. (#xb $ x $ xa#)#)) $ xc#)#)#)#)
[PROOF STEP]
by (simp_all)


[STATEMENT]
lemma monadify_plain_foldli[sepref_monadify_comb]:
  "EVAL$(foldli$l$c$(\<lambda>\<^sub>2x s. f x s)$s) \<equiv>
    (\<bind>)$(EVAL$l)$
     (\<lambda>\<^sub>2l. (\<bind>)$(EVAL$s)$
      (\<lambda>\<^sub>2s. nfoldli$l$c$(\<lambda>\<^sub>2x s. (EVAL$(f x s)))$s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EVAL $ (foldli $ l $ c $ (\<lambda>x. (#\<lambda>xa. (#f x xa#)#)) $ s) \<equiv> (\<bind>) $ (EVAL $ l) $ (\<lambda>x. (#(\<bind>) $ (EVAL $ s) $ (\<lambda>xa. (#nfoldli $ x $ c $ (\<lambda>x. (#\<lambda>xa. (#EVAL $ f x xa#)#)) $ xa#))#))
[PROOF STEP]
by (simp add: foldli_eq_nfoldli)


[STATEMENT]
lemma nfoldli_filter_deforestation:
  "nfoldli (filter P xs) c f s = nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfoldli (filter P xs) c f s = nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s
[PROOF STEP]
apply (induction xs arbitrary: s)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. nfoldli (filter P []) c f s = nfoldli [] c (\<lambda>x s. if P x then f x s else RETURN s) s
 2. \<And>a xs s. (\<And>s. nfoldli (filter P xs) c f s = nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s) \<Longrightarrow> nfoldli (filter P (a # xs)) c f s = nfoldli (a # xs) c (\<lambda>x s. if P x then f x s else RETURN s) s
[PROOF STEP]
by (auto simp: pw_eq_iff refine_pw_simps)


[STATEMENT]
lemma extend_list_of_filtered_set:
  assumes [simp, intro!]: "finite S"
    and A: "distinct xs'" "set xs' = {x \<in> S. P x}"
  obtains xs where "xs' = filter P xs" "distinct xs" "set xs = S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>xs' = filter P xs; distinct xs; set xs = S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>xs' = filter P xs; distinct xs; set xs = S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain xs2 where "{x\<in>S. \<not>P x} = set xs2" "distinct xs2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs2. \<lbrakk>{x \<in> S. \<not> P x} = set xs2; distinct xs2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using finite_distinct_list[where A="{x\<in>S. \<not>P x}"]
[PROOF STATE]
proof (prove)
using this:
finite {x \<in> S. \<not> P x} \<Longrightarrow> \<exists>xs. set xs = {x \<in> S. \<not> P x} \<and> distinct xs

goal (1 subgoal):
 1. (\<And>xs2. \<lbrakk>{x \<in> S. \<not> P x} = set xs2; distinct xs2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x \<in> S. \<not> P x} = set xs2
distinct xs2

goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>xs' = filter P xs; distinct xs; set xs = S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
distinct xs'
set xs' = {x \<in> S. P x}
{x \<in> S. \<not> P x} = set xs2
distinct xs2
[PROOF STEP]
have "xs' = filter P (xs'@xs2)" "distinct (xs'@xs2)" "set (xs'@xs2) = S"
[PROOF STATE]
proof (prove)
using this:
distinct xs'
set xs' = {x \<in> S. P x}
{x \<in> S. \<not> P x} = set xs2
distinct xs2

goal (1 subgoal):
 1. xs' = filter P (xs' @ xs2) &&& distinct (xs' @ xs2) &&& set (xs' @ xs2) = S
[PROOF STEP]
by (auto simp: filter_empty_conv)
[PROOF STATE]
proof (state)
this:
xs' = filter P (xs' @ xs2)
distinct (xs' @ xs2)
set (xs' @ xs2) = S

goal (1 subgoal):
 1. (\<And>xs. \<lbrakk>xs' = filter P xs; distinct xs; set xs = S\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from that[OF this]
[PROOF STATE]
proof (chain)
picking this:
thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma FOREACHc_filter_deforestation:
  assumes FIN[simp, intro!]: "finite S"
  shows "(FOREACHc {x\<in>S. P x} c f s)
    = FOREACHc S c (\<lambda>x s. if P x then f x s else RETURN s) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FOREACH\<^sub>C {x \<in> S. P x} c f s = FOREACH\<^sub>C S c (\<lambda>x s. if P x then f x s else RETURN s) s
[PROOF STEP]
unfolding FOREACHc_def FOREACHci_def FOREACHoci_by_LIST_FOREACH LIST_FOREACH'_eq
      LIST_FOREACH'_def it_to_sorted_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (finite {x \<in> S. P x}) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s)) = ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s))
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (finite {x \<in> S. P x}) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s)) = ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s))
[PROOF STEP]
proof (induction rule: antisym[consumes 0, case_names 1 2])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ASSERT (finite {x \<in> S. P x}) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s)) \<le> ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s))
 2. ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s)) \<le> ASSERT (finite {x \<in> S. P x}) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. ASSERT (finite {x \<in> S. P x}) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s)) \<le> ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s))
 2. ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s)) \<le> ASSERT (finite {x \<in> S. P x}) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (finite {x \<in> S. P x}) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s)) \<le> ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s))
[PROOF STEP]
apply (rule le_ASSERTI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite S \<Longrightarrow> ASSERT (finite {x \<in> S. P x}) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s)) \<le> SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s)
[PROOF STEP]
apply (rule ASSERT_leI, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite S; finite {x \<in> S. P x}\<rbrakk> \<Longrightarrow> SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s) \<le> SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s)
[PROOF STEP]
apply (rule intro_spec_refine[where R=Id, simplified]; clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>distinct xs; {x \<in> S. P x} = set xs\<rbrakk> \<Longrightarrow> nfoldli xs c f s \<le> SPEC (\<lambda>l. distinct l \<and> S = set l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s)
[PROOF STEP]
apply (rule extend_list_of_filtered_set[OF FIN _ sym], assumption, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs xsa. \<lbrakk>distinct xs; {x \<in> S. P x} = set xs; xs = filter P xsa; distinct xsa; set xsa = S\<rbrakk> \<Longrightarrow> nfoldli xs c f s \<le> SPEC (\<lambda>l. distinct l \<and> S = set l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s)
[PROOF STEP]
subgoal for xs' xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs'; {x \<in> S. P x} = set xs'; xs' = filter P xs; distinct xs; set xs = S\<rbrakk> \<Longrightarrow> nfoldli xs' c f s \<le> SPEC (\<lambda>l. distinct l \<and> S = set l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s)
[PROOF STEP]
apply (rule rhs_step_bind_SPEC[where R=Id and x'="xs", simplified])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct xs'; {x \<in> S. P x} = set xs'; xs' = filter P xs; distinct xs; set xs = S\<rbrakk> \<Longrightarrow> distinct xs \<and> S = set xs
 2. \<lbrakk>distinct xs'; {x \<in> S. P x} = set xs'; xs' = filter P xs; distinct xs; set xs = S\<rbrakk> \<Longrightarrow> nfoldli xs' c f s \<le> nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s
[PROOF STEP]
applyS simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs'; {x \<in> S. P x} = set xs'; xs' = filter P xs; distinct xs; set xs = S\<rbrakk> \<Longrightarrow> nfoldli xs' c f s \<le> nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s
[PROOF STEP]
applyS (simp add: nfoldli_filter_deforestation)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ASSERT (finite {x \<in> S. P x}) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s)) \<le> ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s))

goal (1 subgoal):
 1. ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s)) \<le> ASSERT (finite {x \<in> S. P x}) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s)) \<le> ASSERT (finite {x \<in> S. P x}) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s))
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s)) \<le> ASSERT (finite {x \<in> S. P x}) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s)) \<le> ASSERT (finite {x \<in> S. P x}) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s))
[PROOF STEP]
apply (rule le_ASSERTI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x \<in> S. P x} \<Longrightarrow> ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s)) \<le> SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s)
[PROOF STEP]
apply (rule ASSERT_leI, (simp; fail))
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite {x \<in> S. P x}; finite S\<rbrakk> \<Longrightarrow> SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s) \<le> SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s)
[PROOF STEP]
apply (rule intro_spec_refine[where R=Id, simplified]; clarsimp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>distinct xs; S = set xs\<rbrakk> \<Longrightarrow> nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s \<le> SPEC (\<lambda>l. distinct l \<and> {x \<in> set xs. P x} = set l) \<bind> (\<lambda>xs. nfoldli xs c f s)
[PROOF STEP]
subgoal for xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; S = set xs\<rbrakk> \<Longrightarrow> nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s \<le> SPEC (\<lambda>l. distinct l \<and> {x \<in> set xs. P x} = set l) \<bind> (\<lambda>xs. nfoldli xs c f s)
[PROOF STEP]
apply (rule rhs_step_bind_SPEC[where R=Id and x'="filter P xs", simplified])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>distinct xs; S = set xs\<rbrakk> \<Longrightarrow> distinct (filter P xs) \<and> {x \<in> set xs. P x} = set (filter P xs)
 2. \<lbrakk>distinct xs; S = set xs\<rbrakk> \<Longrightarrow> nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s \<le> nfoldli (filter P xs) c f s
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; S = set xs\<rbrakk> \<Longrightarrow> nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s \<le> nfoldli (filter P xs) c f s
[PROOF STEP]
apply (simp add: nfoldli_filter_deforestation)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
ASSERT (finite S) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> S = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c (\<lambda>x s. if P x then f x s else RETURN s) s)) \<le> ASSERT (finite {x \<in> S. P x}) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> {x \<in> S. P x} = set l \<and> sorted_wrt (\<lambda>_ _. True) l) \<bind> (\<lambda>xs. nfoldli xs c f s))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma FOREACHc_filter_deforestation2:
  assumes [simp]: "distinct xs"
  shows "(FOREACHc (set (filter P xs)) c f s)
    = FOREACHc (set xs) c (\<lambda>x s. if P x then f x s else RETURN s) s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FOREACH\<^sub>C (set (filter P xs)) c f s = FOREACH\<^sub>C (set xs) c (\<lambda>x s. if P x then f x s else RETURN s) s
[PROOF STEP]
using FOREACHc_filter_deforestation[of "set xs", simplified, folded set_filter]
[PROOF STATE]
proof (prove)
using this:
FOREACH\<^sub>C (set (filter ?P xs)) ?c ?f ?s = FOREACH\<^sub>C (set xs) ?c (\<lambda>x s. if ?P x then ?f x s else RETURN s) ?s

goal (1 subgoal):
 1. FOREACH\<^sub>C (set (filter P xs)) c f s = FOREACH\<^sub>C (set xs) c (\<lambda>x s. if P x then f x s else RETURN s) s
[PROOF STEP]
.


[STATEMENT]
lemma [simp]:
  "i \<ge> u \<Longrightarrow> imp_for i u c f s = return s"
  "i < u \<Longrightarrow> imp_for i u c f s = do {ctn <- c s; if ctn then f i s \<bind> imp_for (i + 1) u c f else return s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u \<le> i \<Longrightarrow> imp_for i u c f s = return s) &&& (i < u \<Longrightarrow> imp_for i u c f s = c s \<bind> (\<lambda>ctn. if ctn then f i s \<bind> imp_for (i + 1) u c f else return s))
[PROOF STEP]
by (auto simp: imp_for.simps)


[STATEMENT]
lemma imp_nfoldli_deforest[sepref_opt_simps]:
  "imp_nfoldli [l..<u] c = imp_for l u c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_nfoldli [l..<u] c = imp_for l u c
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. imp_nfoldli [l..<u] c x xa = imp_for l u c x xa
[PROOF STEP]
subgoal for f s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_nfoldli [l..<u] c f s = imp_for l u c f s
[PROOF STEP]
apply (induction "u - l" arbitrary: l u s)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l u s. 0 = u - l \<Longrightarrow> imp_nfoldli [l..<u] c f s = imp_for l u c f s
 2. \<And>x l u s. \<lbrakk>\<And>l u s. x = u - l \<Longrightarrow> imp_nfoldli [l..<u] c f s = imp_for l u c f s; Suc x = u - l\<rbrakk> \<Longrightarrow> imp_nfoldli [l..<u] c f s = imp_for l u c f s
[PROOF STEP]
apply (simp add: upt_conv_Cons; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x l u s. \<lbrakk>\<And>l u s. x = u - l \<Longrightarrow> imp_nfoldli [l..<u] c f s = imp_for l u c f s; Suc x = u - l\<rbrakk> \<Longrightarrow> imp_nfoldli [l..<u] c f s = imp_for l u c f s
[PROOF STEP]
apply (simp add: upt_conv_Cons)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x l u s. \<lbrakk>\<And>l u s. x = u - l \<Longrightarrow> imp_nfoldli [l..<u] c f s = imp_for l u c f s; Suc x = u - l\<rbrakk> \<Longrightarrow> c s \<bind> (\<lambda>b. if b then f l s \<bind> imp_nfoldli [Suc l..<u] c f else return s) = c s \<bind> (\<lambda>ctn. if ctn then f l s \<bind> imp_for (l + 1) u c f else return s)
[PROOF STEP]
apply (fo_rule arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x l u s. \<lbrakk>\<And>l u s. x = u - l \<Longrightarrow> imp_nfoldli [l..<u] c f s = imp_for l u c f s; Suc x = u - l\<rbrakk> \<Longrightarrow> (\<lambda>b. if b then f l s \<bind> imp_nfoldli [Suc l..<u] c f else return s) = (\<lambda>ctn. if ctn then f l s \<bind> imp_for (l + 1) u c f else return s)
[PROOF STEP]
by (auto cong: if_cong)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]:
  "i \<ge> u \<Longrightarrow> imp_for' i u f s = return s"
  "i < u \<Longrightarrow> imp_for' i u f s = f i s \<bind> imp_for' (i + 1) u f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u \<le> i \<Longrightarrow> imp_for' i u f s = return s) &&& (i < u \<Longrightarrow> imp_for' i u f s = f i s \<bind> imp_for' (i + 1) u f)
[PROOF STEP]
by (auto simp: imp_for'.simps)


[STATEMENT]
lemma imp_for_imp_for'[sepref_opt_simps]:
  "imp_for i u (\<lambda> _. return True) = imp_for' i u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_for i u (\<lambda>_. return True) = imp_for' i u
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x xa. imp_for i u (\<lambda>_. return True) x xa = imp_for' i u x xa
[PROOF STEP]
subgoal for f s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_for i u (\<lambda>_. return True) f s = imp_for' i u f s
[PROOF STEP]
apply (induction "u - i" arbitrary: i u s)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i u s. 0 = u - i \<Longrightarrow> imp_for i u (\<lambda>_. return True) f s = imp_for' i u f s
 2. \<And>x i u s. \<lbrakk>\<And>i u s. x = u - i \<Longrightarrow> imp_for i u (\<lambda>_. return True) f s = imp_for' i u f s; Suc x = u - i\<rbrakk> \<Longrightarrow> imp_for i u (\<lambda>_. return True) f s = imp_for' i u f s
[PROOF STEP]
apply (simp; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i u s. \<lbrakk>\<And>i u s. x = u - i \<Longrightarrow> imp_for i u (\<lambda>_. return True) f s = imp_for' i u f s; Suc x = u - i\<rbrakk> \<Longrightarrow> imp_for i u (\<lambda>_. return True) f s = imp_for' i u f s
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i u s. \<lbrakk>\<And>i u s. x = u - i \<Longrightarrow> imp_for i u (\<lambda>_. return True) f s = imp_for' i u f s; Suc x = u - i\<rbrakk> \<Longrightarrow> f i s \<bind> imp_for (Suc i) u (\<lambda>_. return True) f = f i s \<bind> imp_for' (Suc i) u f
[PROOF STEP]
apply (fo_rule arg_cong)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x i u s. \<lbrakk>\<And>i u s. x = u - i \<Longrightarrow> imp_for i u (\<lambda>_. return True) f s = imp_for' i u f s; Suc x = u - i\<rbrakk> \<Longrightarrow> imp_for (Suc i) u (\<lambda>_. return True) f = imp_for' (Suc i) u f
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma imp_nfoldli_deforest_down[sepref_opt_simps]:
  "imp_nfoldli (rev [l..<u]) c =
    (\<lambda>f s. if u\<le>l then return s else imp_for_down l u c f s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_nfoldli (rev [l..<u]) c = (\<lambda>f s. if u \<le> l then return s else imp_for_down l u c f s)
[PROOF STEP]
proof (intro ext)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f s. imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)
[PROOF STEP]
fix f s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f s. imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)
[PROOF STEP]
show "imp_nfoldli (rev [l..<u]) c f s =
          (if l \<ge> u then return s else imp_for_down l u c f s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)
[PROOF STEP]
proof cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)
 2. \<not> ?P \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)
[PROOF STEP]
assume "l\<ge>u"
[PROOF STATE]
proof (state)
this:
u \<le> l

goal (2 subgoals):
 1. ?P \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)
 2. \<not> ?P \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
u \<le> l

goal (1 subgoal):
 1. imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)

goal (1 subgoal):
 1. \<not> u \<le> l \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> u \<le> l \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)
[PROOF STEP]
assume "\<not>(l\<ge>u)"
[PROOF STATE]
proof (state)
this:
\<not> u \<le> l

goal (1 subgoal):
 1. \<not> u \<le> l \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)
[PROOF STEP]
hence "l<u"
[PROOF STATE]
proof (prove)
using this:
\<not> u \<le> l

goal (1 subgoal):
 1. l < u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l < u

goal (1 subgoal):
 1. \<not> u \<le> l \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l < u

goal (1 subgoal):
 1. imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l < u \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s
[PROOF STEP]
proof (induction "u - l" arbitrary: u s)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u s. \<lbrakk>0 = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s
 2. \<And>x u s. \<lbrakk>\<And>u s. \<lbrakk>x = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s; Suc x = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = u - l
l < u

goal (2 subgoals):
 1. \<And>u s. \<lbrakk>0 = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s
 2. \<And>x u s. \<lbrakk>\<And>u s. \<lbrakk>x = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s; Suc x = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
0 = u - l
l < u

goal (1 subgoal):
 1. imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s

goal (1 subgoal):
 1. \<And>x u s. \<lbrakk>\<And>u s. \<lbrakk>x = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s; Suc x = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x u s. \<lbrakk>\<And>u s. \<lbrakk>x = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s; Suc x = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s
[PROOF STEP]
case (Suc u')
[PROOF STATE]
proof (state)
this:
\<lbrakk>u' = ?u - l; l < ?u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<?u]) c f ?s = imp_for_down l ?u c f ?s
Suc u' = u - l
l < u

goal (1 subgoal):
 1. \<And>x u s. \<lbrakk>\<And>u s. \<lbrakk>x = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s; Suc x = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s
[PROOF STEP]
from Suc.prems Suc.hyps(2)
[PROOF STATE]
proof (chain)
picking this:
l < u
Suc u' = u - l
[PROOF STEP]
have [simp]: "rev [l..<u] = (u-1)#rev [l..<u-1]"
[PROOF STATE]
proof (prove)
using this:
l < u
Suc u' = u - l

goal (1 subgoal):
 1. rev [l..<u] = (u - 1) # rev [l..<u - 1]
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>l < u; Suc u' = u - l\<rbrakk> \<Longrightarrow> [l..<u] = [l..<u - Suc 0] @ [u - Suc 0]
[PROOF STEP]
apply (subst upt_Suc_append[symmetric])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>l < u; Suc u' = u - l\<rbrakk> \<Longrightarrow> l \<le> u - Suc 0
 2. \<lbrakk>l < u; Suc u' = u - l\<rbrakk> \<Longrightarrow> [l..<u] = [l..<Suc (u - Suc 0)]
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
rev [l..<u] = (u - 1) # rev [l..<u - 1]

goal (1 subgoal):
 1. \<And>x u s. \<lbrakk>\<And>u s. \<lbrakk>x = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s; Suc x = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s
[PROOF STEP]
using Suc.hyps(1)[of "u-1"] Suc.hyps(2) Suc.prems
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>u' = u - 1 - l; l < u - 1\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u - 1]) c f ?s = imp_for_down l (u - 1) c f ?s
Suc u' = u - l
l < u

goal (1 subgoal):
 1. imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s
[PROOF STEP]
apply (subst imp_for_down.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<lbrakk>u' = u - 1 - l; l < u - 1\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u - 1]) c f s = imp_for_down l (u - 1) c f s; Suc u' = u - l; l < u\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = (let i = u - 1 in c s \<bind> (\<lambda>ctn. if ctn then f i s \<bind> (\<lambda>s. if l < i then imp_for_down l i c f s else return s) else return s))
[PROOF STEP]
apply (cases "l < u - Suc 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>s. \<lbrakk>u' = u - 1 - l; l < u - 1\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u - 1]) c f s = imp_for_down l (u - 1) c f s; Suc u' = u - l; l < u; l < u - Suc 0\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = (let i = u - 1 in c s \<bind> (\<lambda>ctn. if ctn then f i s \<bind> (\<lambda>s. if l < i then imp_for_down l i c f s else return s) else return s))
 2. \<lbrakk>\<And>s. \<lbrakk>u' = u - 1 - l; l < u - 1\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u - 1]) c f s = imp_for_down l (u - 1) c f s; Suc u' = u - l; l < u; \<not> l < u - Suc 0\<rbrakk> \<Longrightarrow> imp_nfoldli (rev [l..<u]) c f s = (let i = u - 1 in c s \<bind> (\<lambda>ctn. if ctn then f i s \<bind> (\<lambda>s. if l < i then imp_for_down l i c f s else return s) else return s))
[PROOF STEP]
apply (auto simp: Let_def cong: if_cong)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
imp_nfoldli (rev [l..<u]) c f s = imp_for_down l u c f s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
imp_nfoldli (rev [l..<u]) c f s = (if u \<le> l then return s else imp_for_down l u c f s)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma imp_for_down_no_cond[sepref_opt_simps]:
  "imp_for_down l u (\<lambda>_. return True) = imp_for_down' l u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_for_down l u (\<lambda>_. return True) = imp_for_down' l u
[PROOF STEP]
apply (induction l u rule: imp_for_down_induction_scheme.induct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l i. (\<And>x. \<lbrakk>x = i - 1; l < x\<rbrakk> \<Longrightarrow> imp_for_down l x (\<lambda>_. return True) = imp_for_down' l x) \<Longrightarrow> imp_for_down l i (\<lambda>_. return True) = imp_for_down' l i
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l i x xa. (\<And>x. \<lbrakk>x = i - 1; l < x\<rbrakk> \<Longrightarrow> imp_for_down l x (\<lambda>_. return True) = imp_for_down' l x) \<Longrightarrow> imp_for_down l i (\<lambda>_. return True) x xa = imp_for_down' l i x xa
[PROOF STEP]
apply (subst imp_for_down.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l i x xa. (\<And>x. \<lbrakk>x = i - 1; l < x\<rbrakk> \<Longrightarrow> imp_for_down l x (\<lambda>_. return True) = imp_for_down' l x) \<Longrightarrow> (let i = i - 1 in return True \<bind> (\<lambda>ctn. if ctn then x i xa \<bind> (\<lambda>s. if l < i then imp_for_down l i (\<lambda>_. return True) x s else return s) else return xa)) = imp_for_down' l i x xa
[PROOF STEP]
apply (subst imp_for_down'.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l i x xa. (\<And>x. \<lbrakk>x = i - 1; l < x\<rbrakk> \<Longrightarrow> imp_for_down l x (\<lambda>_. return True) = imp_for_down' l x) \<Longrightarrow> (let i = i - 1 in return True \<bind> (\<lambda>ctn. if ctn then x i xa \<bind> (\<lambda>s. if l < i then imp_for_down l i (\<lambda>_. return True) x s else return s) else return xa)) = (let i = i - 1 in x i xa \<bind> (\<lambda>s. if l < i then imp_for_down' l i x s else return s))
[PROOF STEP]
apply (simp cong: if_cong)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma imp_for'_rule:
  assumes LESS: "l\<le>u"
  assumes PRE: "P \<Longrightarrow>\<^sub>A I l s"
  assumes STEP: "\<And>i s. \<lbrakk> l\<le>i; i<u \<rbrakk> \<Longrightarrow> <I i s> f i s <I (i+1)>"
  shows "<P> imp_for' l u f s <I u>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <P> imp_for' l u f s <I u>
[PROOF STEP]
apply (rule Hoare_Triple.cons_pre_rule[OF PRE])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <I l s> imp_for' l u f s <I u>
[PROOF STEP]
using LESS
[PROOF STATE]
proof (prove)
using this:
l \<le> u

goal (1 subgoal):
 1. <I l s> imp_for' l u f s <I u>
[PROOF STEP]
proof (induction arbitrary: s rule: inc_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. <I u s> imp_for' u u f s <I u>
 2. \<And>n s. \<lbrakk>l \<le> n; n < u; \<And>s. <I (Suc n) s> imp_for' (Suc n) u f s <I u>\<rbrakk> \<Longrightarrow> <I n s> imp_for' n u f s <I u>
[PROOF STEP]
case base
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>s. <I u s> imp_for' u u f s <I u>
 2. \<And>n s. \<lbrakk>l \<le> n; n < u; \<And>s. <I (Suc n) s> imp_for' (Suc n) u f s <I u>\<rbrakk> \<Longrightarrow> <I n s> imp_for' n u f s <I u>
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <I u s> imp_for' u u f s <I u>
[PROOF STEP]
by sep_auto
[PROOF STATE]
proof (state)
this:
<I u s> imp_for' u u f s <I u>

goal (1 subgoal):
 1. \<And>n s. \<lbrakk>l \<le> n; n < u; \<And>s. <I (Suc n) s> imp_for' (Suc n) u f s <I u>\<rbrakk> \<Longrightarrow> <I n s> imp_for' n u f s <I u>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n s. \<lbrakk>l \<le> n; n < u; \<And>s. <I (Suc n) s> imp_for' (Suc n) u f s <I u>\<rbrakk> \<Longrightarrow> <I n s> imp_for' n u f s <I u>
[PROOF STEP]
case (step k)
[PROOF STATE]
proof (state)
this:
l \<le> k
k < u
<I (Suc k) ?s> imp_for' (Suc k) u f ?s <I u>

goal (1 subgoal):
 1. \<And>n s. \<lbrakk>l \<le> n; n < u; \<And>s. <I (Suc n) s> imp_for' (Suc n) u f s <I u>\<rbrakk> \<Longrightarrow> <I n s> imp_for' n u f s <I u>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <I k s> imp_for' k u f s <I u>
[PROOF STEP]
using step.hyps
[PROOF STATE]
proof (prove)
using this:
l \<le> k
k < u

goal (1 subgoal):
 1. <I k s> imp_for' k u f s <I u>
[PROOF STEP]
by (sep_auto heap: STEP step.IH)
[PROOF STATE]
proof (state)
this:
<I k s> imp_for' k u f s <I u>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fold_idx_conv: "fold f l s = fold (\<lambda>i. f (l!i)) [0..<length l] s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold f l s = fold (\<lambda>i. f (l ! i)) [0..<length l] s
[PROOF STEP]
proof (induction l arbitrary: s rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>s. fold f [] s = fold (\<lambda>i. f ([] ! i)) [0..<length []] s
 2. \<And>x xs s. (\<And>s. fold f xs s = fold (\<lambda>i. f (xs ! i)) [0..<length xs] s) \<Longrightarrow> fold f (xs @ [x]) s = fold (\<lambda>i. f ((xs @ [x]) ! i)) [0..<length (xs @ [x])] s
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>s. fold f [] s = fold (\<lambda>i. f ([] ! i)) [0..<length []] s
 2. \<And>x xs s. (\<And>s. fold f xs s = fold (\<lambda>i. f (xs ! i)) [0..<length xs] s) \<Longrightarrow> fold f (xs @ [x]) s = fold (\<lambda>i. f ((xs @ [x]) ! i)) [0..<length (xs @ [x])] s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold f [] s = fold (\<lambda>i. f ([] ! i)) [0..<length []] s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fold f [] s = fold (\<lambda>i. f ([] ! i)) [0..<length []] s

goal (1 subgoal):
 1. \<And>x xs s. (\<And>s. fold f xs s = fold (\<lambda>i. f (xs ! i)) [0..<length xs] s) \<Longrightarrow> fold f (xs @ [x]) s = fold (\<lambda>i. f ((xs @ [x]) ! i)) [0..<length (xs @ [x])] s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs s. (\<And>s. fold f xs s = fold (\<lambda>i. f (xs ! i)) [0..<length xs] s) \<Longrightarrow> fold f (xs @ [x]) s = fold (\<lambda>i. f ((xs @ [x]) ! i)) [0..<length (xs @ [x])] s
[PROOF STEP]
case (snoc x l)
[PROOF STATE]
proof (state)
this:
fold f l ?s = fold (\<lambda>i. f (l ! i)) [0..<length l] ?s

goal (1 subgoal):
 1. \<And>x xs s. (\<And>s. fold f xs s = fold (\<lambda>i. f (xs ! i)) [0..<length xs] s) \<Longrightarrow> fold f (xs @ [x]) s = fold (\<lambda>i. f ((xs @ [x]) ! i)) [0..<length (xs @ [x])] s
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
fold f l ?s = fold (\<lambda>i. f (l ! i)) [0..<length l] ?s

goal (1 subgoal):
 1. \<And>x xs s. (\<And>s. fold f xs s = fold (\<lambda>i. f (xs ! i)) [0..<length xs] s) \<Longrightarrow> fold f (xs @ [x]) s = fold (\<lambda>i. f ((xs @ [x]) ! i)) [0..<length (xs @ [x])] s
[PROOF STEP]
fix x s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs s. (\<And>s. fold f xs s = fold (\<lambda>i. f (xs ! i)) [0..<length xs] s) \<Longrightarrow> fold f (xs @ [x]) s = fold (\<lambda>i. f ((xs @ [x]) ! i)) [0..<length (xs @ [x])] s
[PROOF STEP]
have "fold (\<lambda>a. f ((l @ [x]) ! a)) [0..<length l] s = fold (\<lambda>a. f (l ! a)) [0..<length l] s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold (\<lambda>a. f ((l @ [x]) ! a)) [0..<length l] s = fold (\<lambda>a. f (l ! a)) [0..<length l] s
[PROOF STEP]
by (rule fold_cong) (simp_all add: nth_append)
[PROOF STATE]
proof (state)
this:
fold (\<lambda>a. f ((l @ [x]) ! a)) [0..<length l] s = fold (\<lambda>a. f (l ! a)) [0..<length l] s

goal (1 subgoal):
 1. \<And>x xs s. (\<And>s. fold f xs s = fold (\<lambda>i. f (xs ! i)) [0..<length xs] s) \<Longrightarrow> fold f (xs @ [x]) s = fold (\<lambda>i. f ((xs @ [x]) ! i)) [0..<length (xs @ [x])] s
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
fold (\<lambda>a. f ((l @ [?xa2]) ! a)) [0..<length l] ?sb2 = fold (\<lambda>a. f (l ! a)) [0..<length l] ?sb2

goal (1 subgoal):
 1. \<And>x xs s. (\<And>s. fold f xs s = fold (\<lambda>i. f (xs ! i)) [0..<length xs] s) \<Longrightarrow> fold f (xs @ [x]) s = fold (\<lambda>i. f ((xs @ [x]) ! i)) [0..<length (xs @ [x])] s
[PROOF STEP]
with snoc
[PROOF STATE]
proof (chain)
picking this:
fold f l ?s = fold (\<lambda>i. f (l ! i)) [0..<length l] ?s
fold (\<lambda>a. f ((l @ [?xa2]) ! a)) [0..<length l] ?sb2 = fold (\<lambda>a. f (l ! a)) [0..<length l] ?sb2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
fold f l ?s = fold (\<lambda>i. f (l ! i)) [0..<length l] ?s
fold (\<lambda>a. f ((l @ [?xa2]) ! a)) [0..<length l] ?sb2 = fold (\<lambda>a. f (l ! a)) [0..<length l] ?sb2

goal (1 subgoal):
 1. fold f (l @ [x]) s = fold (\<lambda>i. f ((l @ [x]) ! i)) [0..<length (l @ [x])] s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fold f (l @ [x]) s = fold (\<lambda>i. f ((l @ [x]) ! i)) [0..<length (l @ [x])] s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma two_sqrt_irrat[simp]: "2 \<in> sqrt_irrat"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 \<in> sqrt_irrat
[PROOF STEP]
using sqrt_prime_irrational[OF two_is_prime_nat]
[PROOF STATE]
proof (prove)
using this:
sqrt (real 2) \<notin> \<rat>

goal (1 subgoal):
 1. 2 \<in> sqrt_irrat
[PROOF STEP]
unfolding Rats_def sqrt_irrat_def image_def
[PROOF STATE]
proof (prove)
using this:
sqrt (real 2) \<notin> {y. \<exists>x\<in>UNIV. y = real_of_rat x}

goal (1 subgoal):
 1. 2 \<in> {q. \<nexists>p. p * p = rat_of_nat q}
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. sqrt 2 \<noteq> real_of_rat x; p * p = 2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. sqrt 2 \<noteq> real_of_rat x; p * p = 2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
(* Sledgehammer proof *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. sqrt 2 \<noteq> real_of_rat x; p * p = 2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix p :: rat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. sqrt 2 \<noteq> real_of_rat x; p * p = 2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "p * p = 2"
[PROOF STATE]
proof (state)
this:
p * p = 2

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. sqrt 2 \<noteq> real_of_rat x; p * p = 2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence f1: "(Ratreal p)\<^sup>2 = real 2"
[PROOF STATE]
proof (prove)
using this:
p * p = 2

goal (1 subgoal):
 1. (Ratreal p)\<^sup>2 = real 2
[PROOF STEP]
by (metis Ratreal_def of_nat_numeral of_rat_numeral_eq power2_eq_square real_times_code)
[PROOF STATE]
proof (state)
this:
(Ratreal p)\<^sup>2 = real 2

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. sqrt 2 \<noteq> real_of_rat x; p * p = 2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<forall>r. if 0 \<le> r then sqrt (r\<^sup>2) = r else r + sqrt (r\<^sup>2) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>r. if 0 \<le> r then sqrt (r\<^sup>2) = r else r + sqrt (r\<^sup>2) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>r. if 0 \<le> r then sqrt (r\<^sup>2) = r else r + sqrt (r\<^sup>2) = 0

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. sqrt 2 \<noteq> real_of_rat x; p * p = 2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence f2: "Ratreal p + sqrt ((Ratreal p)\<^sup>2) = 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>r. if 0 \<le> r then sqrt (r\<^sup>2) = r else r + sqrt (r\<^sup>2) = 0

goal (1 subgoal):
 1. Ratreal p + sqrt ((Ratreal p)\<^sup>2) = 0
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
\<forall>r. if 0 \<le> r then sqrt (r\<^sup>2) = r else r + sqrt (r\<^sup>2) = 0
(Ratreal p)\<^sup>2 = real 2

goal (1 subgoal):
 1. Ratreal p + sqrt ((Ratreal p)\<^sup>2) = 0
[PROOF STEP]
by (metis Ratreal_def Rats_def \<open>sqrt (real 2) \<notin> \<rat>\<close> range_eqI)
[PROOF STATE]
proof (state)
this:
Ratreal p + sqrt ((Ratreal p)\<^sup>2) = 0

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. sqrt 2 \<noteq> real_of_rat x; p * p = 2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have f3: "sqrt (real 2) + - 1 * sqrt ((Ratreal p)\<^sup>2) \<le> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (real 2) + - 1 * sqrt ((Ratreal p)\<^sup>2) \<le> 0
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
(Ratreal p)\<^sup>2 = real 2

goal (1 subgoal):
 1. sqrt (real 2) + - 1 * sqrt ((Ratreal p)\<^sup>2) \<le> 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
sqrt (real 2) + - 1 * sqrt ((Ratreal p)\<^sup>2) \<le> 0

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. sqrt 2 \<noteq> real_of_rat x; p * p = 2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have f4: "0 \<le> sqrt (real 2) + - 1 * sqrt ((Ratreal p)\<^sup>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> sqrt (real 2) + - 1 * sqrt ((Ratreal p)\<^sup>2)
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
(Ratreal p)\<^sup>2 = real 2

goal (1 subgoal):
 1. 0 \<le> sqrt (real 2) + - 1 * sqrt ((Ratreal p)\<^sup>2)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
0 \<le> sqrt (real 2) + - 1 * sqrt ((Ratreal p)\<^sup>2)

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. sqrt 2 \<noteq> real_of_rat x; p * p = 2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have f5: "(- 1 * sqrt (real 2) = real_of_rat p) = (sqrt (real 2) + real_of_rat p = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- 1 * sqrt (real 2) = real_of_rat p) = (sqrt (real 2) + real_of_rat p = 0)
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
(- 1 * sqrt (real 2) = real_of_rat p) = (sqrt (real 2) + real_of_rat p = 0)

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. sqrt 2 \<noteq> real_of_rat x; p * p = 2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "\<forall>x0. - (x0::real) = - 1 * x0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x0. - x0 = - 1 * x0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x0. - x0 = - 1 * x0

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. sqrt 2 \<noteq> real_of_rat x; p * p = 2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence "sqrt (real 2) + real_of_rat p \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
\<forall>x0. - x0 = - 1 * x0

goal (1 subgoal):
 1. sqrt (real 2) + real_of_rat p \<noteq> 0
[PROOF STEP]
using f5
[PROOF STATE]
proof (prove)
using this:
\<forall>x0. - x0 = - 1 * x0
(- 1 * sqrt (real 2) = real_of_rat p) = (sqrt (real 2) + real_of_rat p = 0)

goal (1 subgoal):
 1. sqrt (real 2) + real_of_rat p \<noteq> 0
[PROOF STEP]
by (metis (no_types) Rats_def Rats_minus_iff \<open>sqrt (real 2) \<notin> \<rat>\<close> range_eqI)
[PROOF STATE]
proof (state)
this:
sqrt (real 2) + real_of_rat p \<noteq> 0

goal (1 subgoal):
 1. \<And>p. \<lbrakk>\<forall>x. sqrt 2 \<noteq> real_of_rat x; p * p = 2\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
sqrt (real 2) + real_of_rat p \<noteq> 0

goal (1 subgoal):
 1. False
[PROOF STEP]
using f4 f3 f2
[PROOF STATE]
proof (prove)
using this:
sqrt (real 2) + real_of_rat p \<noteq> 0
0 \<le> sqrt (real 2) + - 1 * sqrt ((Ratreal p)\<^sup>2)
sqrt (real 2) + - 1 * sqrt ((Ratreal p)\<^sup>2) \<le> 0
Ratreal p + sqrt ((Ratreal p)\<^sup>2) = 0

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complex_number_code_post[code_post]:
  shows "Complex a 0 = complex_of_real a"
    and "complex_of_real 0 = 0"
    and "complex_of_real 1 = 1"
    and "complex_of_real (a/b) = complex_of_real a / complex_of_real b"
    and "complex_of_real (numeral n) = numeral n"
    and "complex_of_real (-r) = - complex_of_real r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Complex a 0 = complex_of_real a &&& complex_of_real 0 = 0 &&& complex_of_real 1 = 1) &&& complex_of_real (a / b) = complex_of_real a / complex_of_real b &&& complex_of_real (numeral n) = numeral n &&& complex_of_real (- r) = - complex_of_real r
[PROOF STEP]
using complex_eq_cancel_iff2
[PROOF STATE]
proof (prove)
using this:
(Complex ?x ?y = complex_of_real ?xa) = (?x = ?xa \<and> ?y = 0)

goal (1 subgoal):
 1. (Complex a 0 = complex_of_real a &&& complex_of_real 0 = 0 &&& complex_of_real 1 = 1) &&& complex_of_real (a / b) = complex_of_real a / complex_of_real b &&& complex_of_real (numeral n) = numeral n &&& complex_of_real (- r) = - complex_of_real r
[PROOF STEP]
by auto


[STATEMENT]
lemma real_number_code_post[code_post]:
  shows "real_of (Abs_mini_alg (p, 0, b)) = real_of_rat p"
    and "real_of (Abs_mini_alg (p, q, 2)) = real_of_rat p + real_of_rat q * sqrt 2"
    and "sqrt 0 = 0"
    and "sqrt (real 0) = 0"
    and "x * (0::real) = 0"
    and "(0::real) * x = 0"
    and "(0::real) + x = x"
    and "x + (0::real) = x"
    and "(1::real) * x = x"
    and "x * (1::real) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((real_of (Abs_mini_alg (p, 0, b)) = real_of_rat p &&& real_of (Abs_mini_alg (p, q, 2)) = real_of_rat p + real_of_rat q * sqrt 2) &&& sqrt 0 = 0 &&& sqrt (real 0) = 0 &&& x * 0 = 0) &&& (0 * x = 0 &&& 0 + x = x) &&& x + 0 = x &&& 1 * x = x &&& x * 1 = x
[PROOF STEP]
by (auto simp add: eq_onp_same_args real_of.abs_eq)


[STATEMENT]
lemma array_sum_aux: "l\<^sub>0\<le>l \<Longrightarrow> {l\<^sub>0..<l + 1} = insert l {l\<^sub>0..<l}" for l\<^sub>0 l :: int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l\<^sub>0 \<le> l \<Longrightarrow> {l\<^sub>0..<l + 1} = insert l {l\<^sub>0..<l}
[PROOF STEP]
by auto


[STATEMENT]
lemma fun_rel_def[refine_rel_defs]:
  "A\<rightarrow>B \<equiv> { (f,f'). \<forall>(a,a')\<in>A. (f a, f' a')\<in>B }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<rightarrow> B \<equiv> {(f, f'). \<forall>(a, a')\<in>A. (f a, f' a') \<in> B}
[PROOF STEP]
by (simp add: relAPP_def fun_rel_def_internal)


[STATEMENT]
lemma fun_relI[intro!]: "\<lbrakk>\<And>a a'. (a,a')\<in>A \<Longrightarrow> (f a,f' a')\<in>B\<rbrakk> \<Longrightarrow> (f,f')\<in>A\<rightarrow>B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a a'. (a, a') \<in> A \<Longrightarrow> (f a, f' a') \<in> B) \<Longrightarrow> (f, f') \<in> A \<rightarrow> B
[PROOF STEP]
by (auto simp: fun_rel_def)


[STATEMENT]
lemma fun_relD:
  shows " ((f,f')\<in>(A\<rightarrow>B)) \<Longrightarrow>
  (\<And>x x'. \<lbrakk> (x,x')\<in>A \<rbrakk> \<Longrightarrow> (f x, f' x')\<in>B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f, f') \<in> A \<rightarrow> B \<Longrightarrow> (\<And>x x'. (x, x') \<in> A \<Longrightarrow> (f x, f' x') \<in> B)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x x'. \<lbrakk>(f, f') \<in> A \<rightarrow> B; (x, x') \<in> A\<rbrakk> \<Longrightarrow> (f x, f' x') \<in> ?A x x'
 2. \<And>x x'. \<lbrakk>(f, f') \<in> A \<rightarrow> B; (x, x') \<in> A\<rbrakk> \<Longrightarrow> ?A x x' \<subseteq> B
[PROOF STEP]
by (auto simp: fun_rel_def)


[STATEMENT]
lemma fun_relD1:
  assumes "(f,f')\<in>Ra\<rightarrow>Rr"
  assumes "f x = r"
  shows "\<forall>x'. (x,x')\<in>Ra \<longrightarrow> (r,f' x')\<in>Rr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x'. (x, x') \<in> Ra \<longrightarrow> (r, f' x') \<in> Rr
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> Ra \<rightarrow> Rr
f x = r

goal (1 subgoal):
 1. \<forall>x'. (x, x') \<in> Ra \<longrightarrow> (r, f' x') \<in> Rr
[PROOF STEP]
by (auto simp: fun_rel_def)


[STATEMENT]
lemma fun_relD2:
  assumes "(f,f')\<in>Ra\<rightarrow>Rr"
  assumes "f' x' = r'"
  shows "\<forall>x. (x,x')\<in>Ra \<longrightarrow> (f x,r')\<in>Rr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. (x, x') \<in> Ra \<longrightarrow> (f x, r') \<in> Rr
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> Ra \<rightarrow> Rr
f' x' = r'

goal (1 subgoal):
 1. \<forall>x. (x, x') \<in> Ra \<longrightarrow> (f x, r') \<in> Rr
[PROOF STEP]
by (auto simp: fun_rel_def)


[STATEMENT]
lemma fun_relE1:
  assumes "(f,f')\<in>Id \<rightarrow> Rv"
  assumes "t' = f' x"
  shows "(f x,t')\<in>Rv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (f x, t') \<in> Rv
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> Id \<rightarrow> Rv
t' = f' x

goal (1 subgoal):
 1. (f x, t') \<in> Rv
[PROOF STEP]
by (auto elim: fun_relD)


[STATEMENT]
lemma fun_relE2:
  assumes "(f,f')\<in>Id \<rightarrow> Rv"
  assumes "t = f x"
  shows "(t,f' x)\<in>Rv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t, f' x) \<in> Rv
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(f, f') \<in> Id \<rightarrow> Rv
t = f x

goal (1 subgoal):
 1. (t, f' x) \<in> Rv
[PROOF STEP]
by (auto elim: fun_relD)


[STATEMENT]
lemma prod_rel_def[refine_rel_defs]:
  "(\<langle>R1,R2\<rangle>prod_rel) \<equiv> { ((a,b),(a',b')) . (a,a')\<in>R1 \<and> (b,b')\<in>R2 }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R1 \<times>\<^sub>r R2 \<equiv> {((a, b), a', b'). (a, a') \<in> R1 \<and> (b, b') \<in> R2}
[PROOF STEP]
by (simp add: prod_rel_def_internal relAPP_def)


[STATEMENT]
lemma prod_relI: "\<lbrakk>(a,a')\<in>R1; (b,b')\<in>R2\<rbrakk> \<Longrightarrow> ((a,b),(a',b'))\<in>\<langle>R1,R2\<rangle>prod_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, a') \<in> R1; (b, b') \<in> R2\<rbrakk> \<Longrightarrow> ((a, b), a', b') \<in> R1 \<times>\<^sub>r R2
[PROOF STEP]
by (auto simp: prod_rel_def)


[STATEMENT]
lemma prod_relE:
  assumes "(p,p')\<in>\<langle>R1,R2\<rangle>prod_rel"
  obtains a b a' b' where "p=(a,b)" and "p'=(a',b')"
  and "(a,a')\<in>R1" and "(b,b')\<in>R2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>a b a' b'. \<lbrakk>p = (a, b); p' = (a', b'); (a, a') \<in> R1; (b, b') \<in> R2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(p, p') \<in> R1 \<times>\<^sub>r R2

goal (1 subgoal):
 1. (\<And>a b a' b'. \<lbrakk>p = (a, b); p' = (a', b'); (a, a') \<in> R1; (b, b') \<in> R2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: prod_rel_def)


[STATEMENT]
lemma prod_rel_simp[simp]:
  "((a,b),(a',b'))\<in>\<langle>R1,R2\<rangle>prod_rel \<longleftrightarrow> (a,a')\<in>R1 \<and> (b,b')\<in>R2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((a, b), a', b') \<in> R1 \<times>\<^sub>r R2) = ((a, a') \<in> R1 \<and> (b, b') \<in> R2)
[PROOF STEP]
by (auto intro: prod_relI elim: prod_relE)


[STATEMENT]
lemma in_Domain_prod_rel_iff[iff]: "(a,b)\<in>Domain (A\<times>\<^sub>rB) \<longleftrightarrow> a\<in>Domain A \<and> b\<in>Domain B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((a, b) \<in> Domain (A \<times>\<^sub>r B)) = (a \<in> Domain A \<and> b \<in> Domain B)
[PROOF STEP]
by (auto simp: prod_rel_def)


[STATEMENT]
lemma prod_rel_comp: "(A \<times>\<^sub>r B) O (C \<times>\<^sub>r D) = (A O C) \<times>\<^sub>r (B O D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A \<times>\<^sub>r B) O (C \<times>\<^sub>r D) = A O C \<times>\<^sub>r B O D
[PROOF STEP]
unfolding prod_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {((a, b), a', b'). (a, a') \<in> A \<and> (b, b') \<in> B} O {((a, b), a', b'). (a, a') \<in> C \<and> (b, b') \<in> D} = {((a, b), a', b'). (a, a') \<in> A O C \<and> (b, b') \<in> B O D}
[PROOF STEP]
by auto


[STATEMENT]
lemma option_rel_def[refine_rel_defs]:
  "\<langle>R\<rangle>option_rel \<equiv> { (Some a,Some a') | a a'. (a,a')\<in>R } \<union> {(None,None)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>R\<rangle>option_rel \<equiv> {(Some a, Some a') |a a'. (a, a') \<in> R} \<union> {(None, None)}
[PROOF STEP]
by (simp add: option_rel_def_internal relAPP_def)


[STATEMENT]
lemma option_relI:
  "(None,None)\<in>\<langle>R\<rangle> option_rel"
  "\<lbrakk> (a,a')\<in>R \<rbrakk> \<Longrightarrow> (Some a, Some a')\<in>\<langle>R\<rangle>option_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (None, None) \<in> \<langle>R\<rangle>option_rel &&& ((a, a') \<in> R \<Longrightarrow> (Some a, Some a') \<in> \<langle>R\<rangle>option_rel)
[PROOF STEP]
by (auto simp: option_rel_def)


[STATEMENT]
lemma option_relE:
  assumes "(x,x')\<in>\<langle>R\<rangle>option_rel"
  obtains "x=None" and "x'=None"
  | a a' where "x=Some a" and "x'=Some a'" and "(a,a')\<in>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>x = None; x' = None\<rbrakk> \<Longrightarrow> thesis; \<And>a a'. \<lbrakk>x = Some a; x' = Some a'; (a, a') \<in> R\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(x, x') \<in> \<langle>R\<rangle>option_rel

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>x = None; x' = None\<rbrakk> \<Longrightarrow> thesis; \<And>a a'. \<lbrakk>x = Some a; x' = Some a'; (a, a') \<in> R\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: option_rel_def)


[STATEMENT]
lemma option_rel_simp[simp]:
  "(None,a)\<in>\<langle>R\<rangle>option_rel \<longleftrightarrow> a=None"
  "(c,None)\<in>\<langle>R\<rangle>option_rel \<longleftrightarrow> c=None"
  "(Some x,Some y)\<in>\<langle>R\<rangle>option_rel \<longleftrightarrow> (x,y)\<in>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((None, a) \<in> \<langle>R\<rangle>option_rel) = (a = None) &&& ((c, None) \<in> \<langle>R\<rangle>option_rel) = (c = None) &&& ((Some x, Some y) \<in> \<langle>R\<rangle>option_rel) = ((x, y) \<in> R)
[PROOF STEP]
by (auto intro: option_relI elim: option_relE)


[STATEMENT]
lemma sum_rel_def[refine_rel_defs]:
  "\<langle>Rl,Rr\<rangle>sum_rel \<equiv>
     { (Inl a, Inl a') | a a'. (a,a')\<in>Rl } \<union>
     { (Inr a, Inr a') | a a'. (a,a')\<in>Rr }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Rl, Rr\<rangle>sum_rel \<equiv> {(Inl a, Inl a') |a a'. (a, a') \<in> Rl} \<union> {(Inr a, Inr a') |a a'. (a, a') \<in> Rr}
[PROOF STEP]
by (simp add: sum_rel_def_internal relAPP_def)


[STATEMENT]
lemma sum_rel_simp[simp]:
  "\<And>a a'. (Inl a, Inl a') \<in> \<langle>Rl,Rr\<rangle>sum_rel \<longleftrightarrow> (a,a')\<in>Rl"
  "\<And>a a'. (Inr a, Inr a') \<in> \<langle>Rl,Rr\<rangle>sum_rel \<longleftrightarrow> (a,a')\<in>Rr"
  "\<And>a a'. (Inl a, Inr a') \<notin> \<langle>Rl,Rr\<rangle>sum_rel"
  "\<And>a a'. (Inr a, Inl a') \<notin> \<langle>Rl,Rr\<rangle>sum_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>a a'. ((Inl a, Inl a') \<in> \<langle>Rl, Rr\<rangle>sum_rel) = ((a, a') \<in> Rl)) &&& (\<And>a a'. ((Inr a, Inr a') \<in> \<langle>Rl, Rr\<rangle>sum_rel) = ((a, a') \<in> Rr))) &&& (\<And>a a'. (Inl a, Inr a') \<notin> \<langle>Rl, Rr\<rangle>sum_rel) &&& (\<And>a a'. (Inr a, Inl a') \<notin> \<langle>Rl, Rr\<rangle>sum_rel)
[PROOF STEP]
unfolding sum_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>a a'. ((Inl a, Inl a') \<in> {(Inl a, Inl a') |a a'. (a, a') \<in> Rl} \<union> {(Inr a, Inr a') |a a'. (a, a') \<in> Rr}) = ((a, a') \<in> Rl)) &&& (\<And>a a'. ((Inr a, Inr a') \<in> {(Inl a, Inl a') |a a'. (a, a') \<in> Rl} \<union> {(Inr a, Inr a') |a a'. (a, a') \<in> Rr}) = ((a, a') \<in> Rr))) &&& (\<And>a a'. (Inl a, Inr a') \<notin> {(Inl a, Inl a') |a a'. (a, a') \<in> Rl} \<union> {(Inr a, Inr a') |a a'. (a, a') \<in> Rr}) &&& (\<And>a a'. (Inr a, Inl a') \<notin> {(Inl a, Inl a') |a a'. (a, a') \<in> Rl} \<union> {(Inr a, Inr a') |a a'. (a, a') \<in> Rr})
[PROOF STEP]
by auto


[STATEMENT]
lemma sum_relI:
  "(l,l')\<in>Rl \<Longrightarrow> (Inl l, Inl l') \<in> \<langle>Rl,Rr\<rangle>sum_rel"
  "(r,r')\<in>Rr \<Longrightarrow> (Inr r, Inr r') \<in> \<langle>Rl,Rr\<rangle>sum_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((l, l') \<in> Rl \<Longrightarrow> (Inl l, Inl l') \<in> \<langle>Rl, Rr\<rangle>sum_rel) &&& ((r, r') \<in> Rr \<Longrightarrow> (Inr r, Inr r') \<in> \<langle>Rl, Rr\<rangle>sum_rel)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma sum_relE:
  assumes "(x,x')\<in>\<langle>Rl,Rr\<rangle>sum_rel"
  obtains
    l l' where "x=Inl l" and "x'=Inl l'" and "(l,l')\<in>Rl"
  | r r' where "x=Inr r" and "x'=Inr r'" and "(r,r')\<in>Rr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>l l'. \<lbrakk>x = Inl l; x' = Inl l'; (l, l') \<in> Rl\<rbrakk> \<Longrightarrow> thesis; \<And>r r'. \<lbrakk>x = Inr r; x' = Inr r'; (r, r') \<in> Rr\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(x, x') \<in> \<langle>Rl, Rr\<rangle>sum_rel

goal (1 subgoal):
 1. \<lbrakk>\<And>l l'. \<lbrakk>x = Inl l; x' = Inl l'; (l, l') \<in> Rl\<rbrakk> \<Longrightarrow> thesis; \<And>r r'. \<lbrakk>x = Inr r; x' = Inr r'; (r, r') \<in> Rr\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: sum_rel_def)


[STATEMENT]
lemma list_rel_def[refine_rel_defs]:
  "\<langle>R\<rangle>list_rel \<equiv> {(l,l'). list_all2 (\<lambda>x x'. (x,x')\<in>R) l l'}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>R\<rangle>list_rel \<equiv> {(l, l'). list_all2 (\<lambda>x x'. (x, x') \<in> R) l l'}
[PROOF STEP]
by (simp add: list_rel_def_internal relAPP_def)


[STATEMENT]
lemma list_rel_induct[induct set,consumes 1, case_names Nil Cons]:
  assumes "(l,l')\<in>\<langle>R\<rangle> list_rel"
  assumes "P [] []"
  assumes "\<And>x x' l l'. \<lbrakk> (x,x')\<in>R; (l,l')\<in>\<langle>R\<rangle>list_rel; P l l' \<rbrakk>
    \<Longrightarrow> P (x#l) (x'#l')"
  shows "P l l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P l l'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(l, l') \<in> \<langle>R\<rangle>list_rel
P [] []
\<lbrakk>(?x, ?x') \<in> R; (?l, ?l') \<in> \<langle>R\<rangle>list_rel; P ?l ?l'\<rbrakk> \<Longrightarrow> P (?x # ?l) (?x' # ?l')

goal (1 subgoal):
 1. P l l'
[PROOF STEP]
unfolding list_rel_def
[PROOF STATE]
proof (prove)
using this:
(l, l') \<in> {(l, l'). list_all2 (\<lambda>x x'. (x, x') \<in> R) l l'}
P [] []
\<lbrakk>(?x, ?x') \<in> R; (?l, ?l') \<in> {(l, l'). list_all2 (\<lambda>x x'. (x, x') \<in> R) l l'}; P ?l ?l'\<rbrakk> \<Longrightarrow> P (?x # ?l) (?x' # ?l')

goal (1 subgoal):
 1. P l l'
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all2 (\<lambda>x x'. (x, x') \<in> R) l l'; P [] []; \<And>x x' l l'. \<lbrakk>(x, x') \<in> R; list_all2 (\<lambda>x x'. (x, x') \<in> R) l l'; P l l'\<rbrakk> \<Longrightarrow> P (x # l) (x' # l')\<rbrakk> \<Longrightarrow> P l l'
[PROOF STEP]
by (rule list_all2_induct)


[STATEMENT]
lemma list_rel_eq_listrel: "list_rel = listrel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_rel = listrel
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. list_rel x = listrel x
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x a b. (a, b) \<in> list_rel x \<Longrightarrow> (a, b) \<in> listrel x
 2. \<And>x a b. (a, b) \<in> listrel x \<Longrightarrow> (a, b) \<in> list_rel x
[PROOF STEP]
proof goal_cases
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x a b. (a, b) \<in> list_rel x \<Longrightarrow> (a, b) \<in> listrel x
 2. \<And>x a b. (a, b) \<in> listrel x \<Longrightarrow> (a, b) \<in> list_rel x
[PROOF STEP]
case (1 x a b)
[PROOF STATE]
proof (state)
this:
(a, b) \<in> list_rel x

goal (2 subgoals):
 1. \<And>x a b. (a, b) \<in> list_rel x \<Longrightarrow> (a, b) \<in> listrel x
 2. \<And>x a b. (a, b) \<in> listrel x \<Longrightarrow> (a, b) \<in> list_rel x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> list_rel x

goal (1 subgoal):
 1. (a, b) \<in> listrel x
[PROOF STEP]
unfolding list_rel_def_internal
[PROOF STATE]
proof (prove)
using this:
(a, b) \<in> {(l, l'). list_all2 (\<lambda>xa x'. (xa, x') \<in> x) l l'}

goal (1 subgoal):
 1. (a, b) \<in> listrel x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all2 (\<lambda>xa x'. (xa, x') \<in> x) a b \<Longrightarrow> (a, b) \<in> listrel x
[PROOF STEP]
apply (induct a b rule: list_all2_induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ([], []) \<in> listrel x
 2. \<And>xa x' ls ls'. \<lbrakk>(xa, x') \<in> x; list_all2 (\<lambda>xa x'. (xa, x') \<in> x) ls ls'; (ls, ls') \<in> listrel x\<rbrakk> \<Longrightarrow> (xa # ls, x' # ls') \<in> listrel x
[PROOF STEP]
apply (auto intro: listrel.intros)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(a, b) \<in> listrel x

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> listrel x \<Longrightarrow> (a, b) \<in> list_rel x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> listrel x \<Longrightarrow> (a, b) \<in> list_rel x
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
(a_, b_) \<in> listrel x_

goal (1 subgoal):
 1. \<And>x a b. (a, b) \<in> listrel x \<Longrightarrow> (a, b) \<in> list_rel x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(a_, b_) \<in> listrel x_

goal (1 subgoal):
 1. (a_, b_) \<in> list_rel x_
[PROOF STEP]
apply (induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. ([], []) \<in> list_rel x_
 2. \<And>xa y xs ys. \<lbrakk>(xa, y) \<in> x_; (xs, ys) \<in> listrel x_; (xs, ys) \<in> list_rel x_\<rbrakk> \<Longrightarrow> (xa # xs, y # ys) \<in> list_rel x_
[PROOF STEP]
apply (auto simp: list_rel_def_internal)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(a_, b_) \<in> list_rel x_

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_relI:
  "([],[])\<in>\<langle>R\<rangle>list_rel"
  "\<lbrakk> (x,x')\<in>R; (l,l')\<in>\<langle>R\<rangle>list_rel \<rbrakk> \<Longrightarrow> (x#l,x'#l')\<in>\<langle>R\<rangle>list_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([], []) \<in> \<langle>R\<rangle>list_rel &&& (\<lbrakk>(x, x') \<in> R; (l, l') \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> (x # l, x' # l') \<in> \<langle>R\<rangle>list_rel)
[PROOF STEP]
by (auto simp: list_rel_def)


[STATEMENT]
lemma list_rel_simp[simp]:
  "([],l')\<in>\<langle>R\<rangle>list_rel \<longleftrightarrow> l'=[]"
  "(l,[])\<in>\<langle>R\<rangle>list_rel \<longleftrightarrow> l=[]"
  "([],[])\<in>\<langle>R\<rangle>list_rel"
  "(x#l,x'#l')\<in>\<langle>R\<rangle>list_rel \<longleftrightarrow> (x,x')\<in>R \<and> (l,l')\<in>\<langle>R\<rangle>list_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((([], l') \<in> \<langle>R\<rangle>list_rel) = (l' = []) &&& ((l, []) \<in> \<langle>R\<rangle>list_rel) = (l = [])) &&& ([], []) \<in> \<langle>R\<rangle>list_rel &&& ((x # l, x' # l') \<in> \<langle>R\<rangle>list_rel) = ((x, x') \<in> R \<and> (l, l') \<in> \<langle>R\<rangle>list_rel)
[PROOF STEP]
by (auto simp: list_rel_def)


[STATEMENT]
lemma list_relE1:
  assumes "(l,[])\<in>\<langle>R\<rangle>list_rel" obtains "l=[]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l = [] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(l, []) \<in> \<langle>R\<rangle>list_rel

goal (1 subgoal):
 1. (l = [] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma list_relE2:
  assumes "([],l)\<in>\<langle>R\<rangle>list_rel" obtains "l=[]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l = [] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
([], l) \<in> \<langle>R\<rangle>list_rel

goal (1 subgoal):
 1. (l = [] \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma list_relE3:
  assumes "(x#xs,l')\<in>\<langle>R\<rangle>list_rel" obtains x' xs' where
  "l'=x'#xs'" and "(x,x')\<in>R" and "(xs,xs')\<in>\<langle>R\<rangle>list_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x' xs'. \<lbrakk>l' = x' # xs'; (x, x') \<in> R; (xs, xs') \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(x # xs, l') \<in> \<langle>R\<rangle>list_rel

goal (1 subgoal):
 1. (\<And>x' xs'. \<lbrakk>l' = x' # xs'; (x, x') \<in> R; (xs, xs') \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases l')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x' xs'. \<lbrakk>l' = x' # xs'; (x, x') \<in> R; (xs, xs') \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> thesis; (x # xs, l') \<in> \<langle>R\<rangle>list_rel; l' = []\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a list. \<lbrakk>\<And>x' xs'. \<lbrakk>l' = x' # xs'; (x, x') \<in> R; (xs, xs') \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> thesis; (x # xs, l') \<in> \<langle>R\<rangle>list_rel; l' = a # list\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_relE4:
  assumes "(l,x'#xs')\<in>\<langle>R\<rangle>list_rel" obtains x xs where
  "l=x#xs" and "(x,x')\<in>R" and "(xs,xs')\<in>\<langle>R\<rangle>list_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x xs. \<lbrakk>l = x # xs; (x, x') \<in> R; (xs, xs') \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(l, x' # xs') \<in> \<langle>R\<rangle>list_rel

goal (1 subgoal):
 1. (\<And>x xs. \<lbrakk>l = x # xs; (x, x') \<in> R; (xs, xs') \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (cases l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>x xs. \<lbrakk>l = x # xs; (x, x') \<in> R; (xs, xs') \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> thesis; (l, x' # xs') \<in> \<langle>R\<rangle>list_rel; l = []\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a list. \<lbrakk>\<And>x xs. \<lbrakk>l = x # xs; (x, x') \<in> R; (xs, xs') \<in> \<langle>R\<rangle>list_rel\<rbrakk> \<Longrightarrow> thesis; (l, x' # xs') \<in> \<langle>R\<rangle>list_rel; l = a # list\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma list_rel_imp_same_length:
    "(l, l') \<in> \<langle>R\<rangle>list_rel \<Longrightarrow> length l = length l'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, l') \<in> \<langle>R\<rangle>list_rel \<Longrightarrow> length l = length l'
[PROOF STEP]
unfolding list_rel_eq_listrel relAPP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (l, l') \<in> listrel R \<Longrightarrow> length l = length l'
[PROOF STEP]
by (rule listrel_eq_len)


[STATEMENT]
lemma list_rel_split_right_iff:
  "(x#xs,l)\<in>\<langle>R\<rangle>list_rel \<longleftrightarrow> (\<exists>y ys. l=y#ys \<and> (x,y)\<in>R \<and> (xs,ys)\<in>\<langle>R\<rangle>list_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((x # xs, l) \<in> \<langle>R\<rangle>list_rel) = (\<exists>y ys. l = y # ys \<and> (x, y) \<in> R \<and> (xs, ys) \<in> \<langle>R\<rangle>list_rel)
[PROOF STEP]
by (cases l) auto


[STATEMENT]
lemma list_rel_split_left_iff:
  "(l,y#ys)\<in>\<langle>R\<rangle>list_rel \<longleftrightarrow> (\<exists>x xs. l=x#xs \<and> (x,y)\<in>R \<and> (xs,ys)\<in>\<langle>R\<rangle>list_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((l, y # ys) \<in> \<langle>R\<rangle>list_rel) = (\<exists>x xs. l = x # xs \<and> (x, y) \<in> R \<and> (xs, ys) \<in> \<langle>R\<rangle>list_rel)
[PROOF STEP]
by (cases l) auto


[STATEMENT]
lemma set_rel_def[refine_rel_defs]:
  "\<langle>R\<rangle>set_rel \<equiv> {(A,B). (\<forall>x\<in>A. \<exists>y\<in>B. (x,y)\<in>R) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. (x,y)\<in>R)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>R\<rangle>set_rel \<equiv> {(A, B). (\<forall>x\<in>A. \<exists>y\<in>B. (x, y) \<in> R) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. (x, y) \<in> R)}
[PROOF STEP]
by (simp add: set_rel_def_internal relAPP_def)


[STATEMENT]
lemma set_rel_alt: "\<langle>R\<rangle>set_rel = {(A,B). A \<subseteq> R\<inverse>``B \<and> B \<subseteq> R``A}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>R\<rangle>set_rel = {(A, B). A \<subseteq> R\<inverse> `` B \<and> B \<subseteq> R `` A}
[PROOF STEP]
unfolding set_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(A, B). (\<forall>x\<in>A. \<exists>y\<in>B. (x, y) \<in> R) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. (x, y) \<in> R)} = {(A, B). A \<subseteq> R\<inverse> `` B \<and> B \<subseteq> R `` A}
[PROOF STEP]
by auto


[STATEMENT]
lemma set_relI[intro?]:
  assumes "\<And>x. x\<in>A \<Longrightarrow> \<exists>y\<in>B. (x,y)\<in>R"
  assumes "\<And>y. y\<in>B \<Longrightarrow> \<exists>x\<in>A. (x,y)\<in>R"
  shows "(A,B)\<in>\<langle>R\<rangle>set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A, B) \<in> \<langle>R\<rangle>set_rel
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> \<exists>y\<in>B. (?x, y) \<in> R
?y \<in> B \<Longrightarrow> \<exists>x\<in>A. (x, ?y) \<in> R

goal (1 subgoal):
 1. (A, B) \<in> \<langle>R\<rangle>set_rel
[PROOF STEP]
unfolding set_rel_def
[PROOF STATE]
proof (prove)
using this:
?x \<in> A \<Longrightarrow> \<exists>y\<in>B. (?x, y) \<in> R
?y \<in> B \<Longrightarrow> \<exists>x\<in>A. (x, ?y) \<in> R

goal (1 subgoal):
 1. (A, B) \<in> {(A, B). (\<forall>x\<in>A. \<exists>y\<in>B. (x, y) \<in> R) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. (x, y) \<in> R)}
[PROOF STEP]
by blast


[STATEMENT]
lemma old_set_rel_def[refine_rel_defs]:
  "\<langle>R\<rangle>old_set_rel \<equiv> {(S,S'). S'=R``S \<and> S\<subseteq>Domain R}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>R\<rangle>old_set_rel \<equiv> {(S, S'). S' = R `` S \<and> S \<subseteq> Domain R}
[PROOF STEP]
by (simp add: old_set_rel_def_internal relAPP_def)


[STATEMENT]
lemma old_set_rel_sv_eq: "single_valued R \<Longrightarrow> \<langle>R\<rangle>old_set_rel = \<langle>R\<rangle>set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued R \<Longrightarrow> \<langle>R\<rangle>old_set_rel = \<langle>R\<rangle>set_rel
[PROOF STEP]
unfolding set_rel_def old_set_rel_def single_valued_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. (x, y) \<in> R \<longrightarrow> (\<forall>z. (x, z) \<in> R \<longrightarrow> y = z) \<Longrightarrow> {(S, S'). S' = R `` S \<and> S \<subseteq> Domain R} = {(A, B). (\<forall>x\<in>A. \<exists>y\<in>B. (x, y) \<in> R) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. (x, y) \<in> R)}
[PROOF STEP]
by blast


[STATEMENT]
lemma set_rel_simp[simp]:
  "({},{})\<in>\<langle>R\<rangle>set_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ({}, {}) \<in> \<langle>R\<rangle>set_rel
[PROOF STEP]
by (auto simp: set_rel_def)


[STATEMENT]
lemma set_rel_empty_iff[simp]:
  "({},y)\<in>\<langle>A\<rangle>set_rel \<longleftrightarrow> y={}"
  "(x,{})\<in>\<langle>A\<rangle>set_rel \<longleftrightarrow> x={}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (({}, y) \<in> \<langle>A\<rangle>set_rel) = (y = {}) &&& ((x, {}) \<in> \<langle>A\<rangle>set_rel) = (x = {})
[PROOF STEP]
by (auto simp: set_rel_def; fastforce)+


[STATEMENT]
lemma set_relD1: "(s,s')\<in>\<langle>R\<rangle>set_rel \<Longrightarrow> x\<in>s \<Longrightarrow> \<exists>x'\<in>s'. (x,x')\<in>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> \<langle>R\<rangle>set_rel; x \<in> s\<rbrakk> \<Longrightarrow> \<exists>x'\<in>s'. (x, x') \<in> R
[PROOF STEP]
unfolding set_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> {(A, B). (\<forall>x\<in>A. \<exists>y\<in>B. (x, y) \<in> R) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. (x, y) \<in> R)}; x \<in> s\<rbrakk> \<Longrightarrow> \<exists>x'\<in>s'. (x, x') \<in> R
[PROOF STEP]
by blast


[STATEMENT]
lemma set_relD2: "(s,s')\<in>\<langle>R\<rangle>set_rel \<Longrightarrow> x'\<in>s' \<Longrightarrow> \<exists>x\<in>s. (x,x')\<in>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> \<langle>R\<rangle>set_rel; x' \<in> s'\<rbrakk> \<Longrightarrow> \<exists>x\<in>s. (x, x') \<in> R
[PROOF STEP]
unfolding set_rel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> {(A, B). (\<forall>x\<in>A. \<exists>y\<in>B. (x, y) \<in> R) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. (x, y) \<in> R)}; x' \<in> s'\<rbrakk> \<Longrightarrow> \<exists>x\<in>s. (x, x') \<in> R
[PROOF STEP]
by blast


[STATEMENT]
lemma set_relE1[consumes 2]:
  assumes "(s,s')\<in>\<langle>R\<rangle>set_rel" "x\<in>s"
  obtains x' where "x'\<in>s'" "(x,x')\<in>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x' \<in> s'; (x, x') \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using set_relD1[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<exists>x'\<in>s'. (x, x') \<in> R

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>x' \<in> s'; (x, x') \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..


[STATEMENT]
lemma set_relE2[consumes 2]:
  assumes "(s,s')\<in>\<langle>R\<rangle>set_rel" "x'\<in>s'"
  obtains x where "x\<in>s" "(x,x')\<in>R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> s; (x, x') \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using set_relD2[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<in>s. (x, x') \<in> R

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> s; (x, x') \<in> R\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..


[STATEMENT]
lemma relprop_triggers:
  "\<And>R. single_valued R \<Longrightarrow> single_valued R"
  "\<And>R. R=Id \<Longrightarrow> R=Id"
  "\<And>R. R=Id \<Longrightarrow> Id=R"
  "\<And>R. Range R = UNIV \<Longrightarrow> Range R = UNIV"
  "\<And>R. Range R = UNIV \<Longrightarrow> UNIV = Range R"
  "\<And>R R'. R\<subseteq>R' \<Longrightarrow> R\<subseteq>R'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<And>R. single_valued R \<Longrightarrow> single_valued R) &&& (\<And>R. R = Id \<Longrightarrow> R = Id) &&& (\<And>R. R = Id \<Longrightarrow> Id = R)) &&& (\<And>R. Range R = UNIV \<Longrightarrow> Range R = UNIV) &&& (\<And>R. Range R = UNIV \<Longrightarrow> UNIV = Range R) &&& (\<And>R R'. R \<subseteq> R' \<Longrightarrow> R \<subseteq> R')
[PROOF STEP]
by auto


[STATEMENT]
lemma
  relprop_id_orient[relator_props]: "R=Id \<Longrightarrow> Id=R" and
  relprop_eq_refl[solve_relator_props]: "t = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (R = Id \<Longrightarrow> Id = R) &&& t = t
[PROOF STEP]
by auto


[STATEMENT]
lemma
  relprop_UNIV_orient[relator_props]: "R=UNIV \<Longrightarrow> UNIV=R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R = UNIV \<Longrightarrow> UNIV = R
[PROOF STEP]
by auto


[STATEMENT]
lemma eq_UNIV_iff: "S=UNIV \<longleftrightarrow> (\<forall>x. x\<in>S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (S = UNIV) = (\<forall>x. x \<in> S)
[PROOF STEP]
by auto


[STATEMENT]
lemma fun_rel_sv[relator_props]:
  assumes RAN: "Range Ra = UNIV"
  assumes SV: "single_valued Rv"
  shows "single_valued (Ra \<rightarrow> Rv)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued (Ra \<rightarrow> Rv)
[PROOF STEP]
proof (intro single_valuedI ext impI allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z xa. \<lbrakk>(x, y) \<in> Ra \<rightarrow> Rv; (x, z) \<in> Ra \<rightarrow> Rv\<rbrakk> \<Longrightarrow> y xa = z xa
[PROOF STEP]
fix f g h x'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z xa. \<lbrakk>(x, y) \<in> Ra \<rightarrow> Rv; (x, z) \<in> Ra \<rightarrow> Rv\<rbrakk> \<Longrightarrow> y xa = z xa
[PROOF STEP]
assume R1: "(f,g)\<in>Ra\<rightarrow>Rv"
  and R2: "(f,h)\<in>Ra\<rightarrow>Rv"
[PROOF STATE]
proof (state)
this:
(f, g) \<in> Ra \<rightarrow> Rv
(f, h) \<in> Ra \<rightarrow> Rv

goal (1 subgoal):
 1. \<And>x y z xa. \<lbrakk>(x, y) \<in> Ra \<rightarrow> Rv; (x, z) \<in> Ra \<rightarrow> Rv\<rbrakk> \<Longrightarrow> y xa = z xa
[PROOF STEP]
from RAN
[PROOF STATE]
proof (chain)
picking this:
Range Ra = UNIV
[PROOF STEP]
obtain x where AR: "(x,x')\<in>Ra"
[PROOF STATE]
proof (prove)
using this:
Range Ra = UNIV

goal (1 subgoal):
 1. (\<And>x. (x, x') \<in> Ra \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, x') \<in> Ra

goal (1 subgoal):
 1. \<And>x y z xa. \<lbrakk>(x, y) \<in> Ra \<rightarrow> Rv; (x, z) \<in> Ra \<rightarrow> Rv\<rbrakk> \<Longrightarrow> y xa = z xa
[PROOF STEP]
from fun_relD[OF R1 AR]
[PROOF STATE]
proof (chain)
picking this:
(f x, g x') \<in> Rv
[PROOF STEP]
have "(f x,g x') \<in> Rv"
[PROOF STATE]
proof (prove)
using this:
(f x, g x') \<in> Rv

goal (1 subgoal):
 1. (f x, g x') \<in> Rv
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(f x, g x') \<in> Rv

goal (1 subgoal):
 1. \<And>x y z xa. \<lbrakk>(x, y) \<in> Ra \<rightarrow> Rv; (x, z) \<in> Ra \<rightarrow> Rv\<rbrakk> \<Longrightarrow> y xa = z xa
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(f x, g x') \<in> Rv

goal (1 subgoal):
 1. \<And>x y z xa. \<lbrakk>(x, y) \<in> Ra \<rightarrow> Rv; (x, z) \<in> Ra \<rightarrow> Rv\<rbrakk> \<Longrightarrow> y xa = z xa
[PROOF STEP]
from fun_relD[OF R2 AR]
[PROOF STATE]
proof (chain)
picking this:
(f x, h x') \<in> Rv
[PROOF STEP]
have "(f x,h x') \<in> Rv"
[PROOF STATE]
proof (prove)
using this:
(f x, h x') \<in> Rv

goal (1 subgoal):
 1. (f x, h x') \<in> Rv
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(f x, h x') \<in> Rv

goal (1 subgoal):
 1. \<And>x y z xa. \<lbrakk>(x, y) \<in> Ra \<rightarrow> Rv; (x, z) \<in> Ra \<rightarrow> Rv\<rbrakk> \<Longrightarrow> y xa = z xa
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(f x, g x') \<in> Rv
(f x, h x') \<in> Rv
[PROOF STEP]
show "g x' = h x'"
[PROOF STATE]
proof (prove)
using this:
(f x, g x') \<in> Rv
(f x, h x') \<in> Rv

goal (1 subgoal):
 1. g x' = h x'
[PROOF STEP]
using SV
[PROOF STATE]
proof (prove)
using this:
(f x, g x') \<in> Rv
(f x, h x') \<in> Rv
single_valued Rv

goal (1 subgoal):
 1. g x' = h x'
[PROOF STEP]
by (auto dest: single_valuedD)
[PROOF STATE]
proof (state)
this:
g x' = h x'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fun_rel_id[relator_props]: "\<lbrakk>R1=Id; R2=Id\<rbrakk> \<Longrightarrow> R1 \<rightarrow> R2 = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R1 = Id; R2 = Id\<rbrakk> \<Longrightarrow> R1 \<rightarrow> R2 = Id
[PROOF STEP]
by (auto simp: fun_rel_def)


[STATEMENT]
lemma fun_rel_id_simp[simp]: "Id\<rightarrow>Id = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Id \<rightarrow> Id = Id
[PROOF STEP]
by tagged_solver


[STATEMENT]
lemma fun_rel_comp_dist[relator_props]:
  "(R1\<rightarrow>R2) O (R3\<rightarrow>R4) \<subseteq> ((R1 O R3) \<rightarrow> (R2 O R4))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (R1 \<rightarrow> R2) O (R3 \<rightarrow> R4) \<subseteq> R1 O R3 \<rightarrow> R2 O R4
[PROOF STEP]
by (auto simp: fun_rel_def)


[STATEMENT]
lemma fun_rel_mono[relator_props]: "\<lbrakk> R1\<subseteq>R2; R3\<subseteq>R4 \<rbrakk> \<Longrightarrow> R2\<rightarrow>R3 \<subseteq> R1\<rightarrow>R4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R1 \<subseteq> R2; R3 \<subseteq> R4\<rbrakk> \<Longrightarrow> R2 \<rightarrow> R3 \<subseteq> R1 \<rightarrow> R4
[PROOF STEP]
by (force simp: fun_rel_def)


[STATEMENT]
lemma prod_rel_sv[relator_props]:
  "\<lbrakk>single_valued R1; single_valued R2\<rbrakk> \<Longrightarrow> single_valued (\<langle>R1,R2\<rangle>prod_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>single_valued R1; single_valued R2\<rbrakk> \<Longrightarrow> single_valued (R1 \<times>\<^sub>r R2)
[PROOF STEP]
by (auto intro: single_valuedI dest: single_valuedD simp: prod_rel_def)


[STATEMENT]
lemma prod_rel_id[relator_props]: "\<lbrakk>R1=Id; R2=Id\<rbrakk> \<Longrightarrow> \<langle>R1,R2\<rangle>prod_rel = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R1 = Id; R2 = Id\<rbrakk> \<Longrightarrow> R1 \<times>\<^sub>r R2 = Id
[PROOF STEP]
by (auto simp: prod_rel_def)


[STATEMENT]
lemma prod_rel_id_simp[simp]: "\<langle>Id,Id\<rangle>prod_rel = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Id \<times>\<^sub>r Id = Id
[PROOF STEP]
by tagged_solver


[STATEMENT]
lemma prod_rel_mono[relator_props]:
"\<lbrakk> R2\<subseteq>R1; R3\<subseteq>R4 \<rbrakk> \<Longrightarrow> \<langle>R2,R3\<rangle>prod_rel \<subseteq> \<langle>R1,R4\<rangle>prod_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R2 \<subseteq> R1; R3 \<subseteq> R4\<rbrakk> \<Longrightarrow> R2 \<times>\<^sub>r R3 \<subseteq> R1 \<times>\<^sub>r R4
[PROOF STEP]
by (auto simp: prod_rel_def)


[STATEMENT]
lemma prod_rel_range[relator_props]: "\<lbrakk>Range Ra=UNIV; Range Rb=UNIV\<rbrakk>
  \<Longrightarrow> Range (\<langle>Ra,Rb\<rangle>prod_rel) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Range Ra = UNIV; Range Rb = UNIV\<rbrakk> \<Longrightarrow> Range (Ra \<times>\<^sub>r Rb) = UNIV
[PROOF STEP]
apply (auto simp: prod_rel_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>Range Ra = UNIV; Range Rb = UNIV\<rbrakk> \<Longrightarrow> \<exists>aa. (aa, a) \<in> Ra
 2. \<And>b. \<lbrakk>Range Ra = UNIV; Range Rb = UNIV\<rbrakk> \<Longrightarrow> \<exists>ba. (ba, b) \<in> Rb
[PROOF STEP]
by (metis Range_iff UNIV_I)+


[STATEMENT]
lemma option_rel_sv[relator_props]:
  "\<lbrakk>single_valued R\<rbrakk> \<Longrightarrow> single_valued (\<langle>R\<rangle>option_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued R \<Longrightarrow> single_valued (\<langle>R\<rangle>option_rel)
[PROOF STEP]
by (auto intro: single_valuedI dest: single_valuedD simp: option_rel_def)


[STATEMENT]
lemma option_rel_id[relator_props]:
  "R=Id \<Longrightarrow> \<langle>R\<rangle>option_rel = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R = Id \<Longrightarrow> \<langle>R\<rangle>option_rel = Id
[PROOF STEP]
by (auto simp: option_rel_def)


[STATEMENT]
lemma option_rel_id_simp[simp]: "\<langle>Id\<rangle>option_rel = Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>Id\<rangle>option_rel = Id
[PROOF STEP]
by tagged_solver


[STATEMENT]
lemma option_rel_mono[relator_props]: "R\<subseteq>R' \<Longrightarrow> \<langle>R\<rangle>option_rel \<subseteq> \<langle>R'\<rangle>option_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<subseteq> R' \<Longrightarrow> \<langle>R\<rangle>option_rel \<subseteq> \<langle>R'\<rangle>option_rel
[PROOF STEP]
by (auto simp: option_rel_def)


[STATEMENT]
lemma option_rel_range: "Range R = UNIV \<Longrightarrow> Range (\<langle>R\<rangle>option_rel) = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Range R = UNIV \<Longrightarrow> Range (\<langle>R\<rangle>option_rel) = UNIV
[PROOF STEP]
apply (auto simp: option_rel_def Range_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>Range R = UNIV; \<forall>a a'. x = Some a' \<longrightarrow> (a, a') \<notin> R\<rbrakk> \<Longrightarrow> x = None
[PROOF STEP]
by (metis Range_iff UNIV_I option.exhaust)


[STATEMENT]
lemma option_rel_inter[simp]: "\<langle>R1 \<inter> R2\<rangle>option_rel = \<langle>R1\<rangle>option_rel \<inter> \<langle>R2\<rangle>option_rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<langle>R1 \<inter> R2\<rangle>option_rel = \<langle>R1\<rangle>option_rel \<inter> \<langle>R2\<rangle>option_rel
[PROOF STEP]
by (auto simp: option_rel_def)