[STATEMENT]
lemma M_fin\<^sub>C_af_correct:
  assumes "t \<in> reach\<^sub>t \<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af \<up>af\<^sub>G Abs \<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C Abs Abs \<phi>)"
  assumes "dom \<pi> \<subseteq> \<^bold>G \<phi>"
  shows "abstract_transition t \<in> M_fin \<pi> = M_fin\<^sub>C_af \<phi> (Mapping.Mapping \<pi>) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
let ?delta = "ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af \<up>af\<^sub>G Abs \<Sigma>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
let ?initial = "ltl_to_rabin_base_code_def.initial\<^sub>C Abs Abs \<phi>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
obtain x y \<nu> z z' where t_def [simp]: "t = ((x, y), \<nu>, (z, z'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y \<nu> z z'. t = ((x, y), \<nu>, z, z') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
t = ((x, y), \<nu>, z, z')

goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
have "(x, y) \<in> reach \<Sigma> ?delta ?initial"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> reach \<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af \<up>af\<^sub>G Abs \<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C Abs Abs \<phi>)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
t \<in> reach\<^sub>t \<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af \<up>af\<^sub>G Abs \<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C Abs Abs \<phi>)

goal (1 subgoal):
 1. (x, y) \<in> reach \<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af \<up>af\<^sub>G Abs \<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C Abs Abs \<phi>)
[PROOF STEP]
by (simp add: reach\<^sub>t_def reach_def; blast)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> reach \<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af \<up>af\<^sub>G Abs \<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C Abs Abs \<phi>)

goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
hence N1: "\<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> Mapping.lookup y \<chi> \<noteq> None"
    and D1: "\<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> distinct (the (Mapping.lookup y \<chi>))"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> reach \<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af \<up>af\<^sub>G Abs \<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C Abs Abs \<phi>)

goal (1 subgoal):
 1. (\<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> Mapping.lookup y \<chi> \<noteq> None) &&& (\<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> distinct (the (Mapping.lookup y \<chi>)))
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> reach \<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af \<up>af\<^sub>G Abs \<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C Abs Abs \<phi>)
dom \<pi> \<subseteq> \<^bold>G \<phi>

goal (1 subgoal):
 1. (\<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> Mapping.lookup y \<chi> \<noteq> None) &&& (\<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> distinct (the (Mapping.lookup y \<chi>)))
[PROOF STEP]
by (blast dest: ltl_to_rabin_base_code_def.reach_delta_initial)+
[PROOF STATE]
proof (state)
this:
?\<chi> \<in> dom \<pi> \<Longrightarrow> Mapping.lookup y ?\<chi> \<noteq> None
?\<chi> \<in> dom \<pi> \<Longrightarrow> distinct (the (Mapping.lookup y ?\<chi>))

goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?\<chi> \<in> dom \<pi> \<Longrightarrow> Mapping.lookup y ?\<chi> \<noteq> None
?\<chi> \<in> dom \<pi> \<Longrightarrow> distinct (the (Mapping.lookup y ?\<chi>))

goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
let ?m' = "\<lambda>\<chi>. map_option rk (Mapping.lookup y \<chi>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
fix \<chi>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
assume "\<chi> \<in> dom \<pi>"
[PROOF STATE]
proof (state)
this:
\<chi> \<in> dom \<pi>

goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
hence "S \<up>\<Turnstile>\<^sub>P (foldl and_abs (Abs \<chi>) (map (\<up>eval\<^sub>G (dom \<pi>)) (drop (the (\<pi> \<chi>)) (the (Mapping.lookup y \<chi>)))))
         \<longleftrightarrow> S \<up>\<Turnstile>\<^sub>P (Abs \<chi>) \<and> (\<forall>q. (\<exists>j \<ge> the (\<pi> \<chi>). the (?m' \<chi>) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q)"
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> dom \<pi>

goal (1 subgoal):
 1. S \<up>\<Turnstile>\<^sub>P foldl and_abs (Abs \<chi>) (map (\<up>eval\<^sub>G (dom \<pi>)) (drop (the (\<pi> \<chi>)) (the (Mapping.lookup y \<chi>)))) = (S \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (map_option rk (Mapping.lookup y \<chi>)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q))
[PROOF STEP]
using D1[THEN drop_rk, of _ "the (\<pi> \<chi>)"] N1[THEN option.map_sel, of _ rk]
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> dom \<pi>
?\<chi>1 \<in> dom \<pi> \<Longrightarrow> set (drop (the (\<pi> \<chi>)) (the (Mapping.lookup y ?\<chi>1))) = {q. \<exists>j\<ge>the (\<pi> \<chi>). rk (the (Mapping.lookup y ?\<chi>1)) q = Some j}
?\<chi>1 \<in> dom \<pi> \<Longrightarrow> the (map_option rk (Mapping.lookup y ?\<chi>1)) = rk (the (Mapping.lookup y ?\<chi>1))

goal (1 subgoal):
 1. S \<up>\<Turnstile>\<^sub>P foldl and_abs (Abs \<chi>) (map (\<up>eval\<^sub>G (dom \<pi>)) (drop (the (\<pi> \<chi>)) (the (Mapping.lookup y \<chi>)))) = (S \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (map_option rk (Mapping.lookup y \<chi>)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q))
[PROOF STEP]
by (auto simp add: foldl_LTLAnd_prop_entailment_abs)
[PROOF STATE]
proof (state)
this:
S \<up>\<Turnstile>\<^sub>P foldl and_abs (Abs \<chi>) (map (\<up>eval\<^sub>G (dom \<pi>)) (drop (the (\<pi> \<chi>)) (the (Mapping.lookup y \<chi>)))) = (S \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (map_option rk (Mapping.lookup y \<chi>)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q))

goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?\<chi>2 \<in> dom \<pi> \<Longrightarrow> S \<up>\<Turnstile>\<^sub>P foldl and_abs (Abs ?\<chi>2) (map (\<up>eval\<^sub>G (dom \<pi>)) (drop (the (\<pi> ?\<chi>2)) (the (Mapping.lookup y ?\<chi>2)))) = (S \<up>\<Turnstile>\<^sub>P Abs ?\<chi>2 \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> ?\<chi>2). the (map_option rk (Mapping.lookup y ?\<chi>2)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q))

goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
hence "S \<up>\<Turnstile>\<^sub>P (M_fin\<^sub>C_af_lhs \<phi> (Mapping.Mapping \<pi>) y)
      \<longleftrightarrow> (\<forall>\<chi> \<in> dom \<pi>. S \<up>\<Turnstile>\<^sub>P (Abs \<chi>) \<and> (\<forall>q. (\<exists>j \<ge> the (\<pi> \<chi>). the (?m' \<chi>) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q))"
[PROOF STATE]
proof (prove)
using this:
?\<chi>2 \<in> dom \<pi> \<Longrightarrow> S \<up>\<Turnstile>\<^sub>P foldl and_abs (Abs ?\<chi>2) (map (\<up>eval\<^sub>G (dom \<pi>)) (drop (the (\<pi> ?\<chi>2)) (the (Mapping.lookup y ?\<chi>2)))) = (S \<up>\<Turnstile>\<^sub>P Abs ?\<chi>2 \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> ?\<chi>2). the (map_option rk (Mapping.lookup y ?\<chi>2)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q))

goal (1 subgoal):
 1. S \<up>\<Turnstile>\<^sub>P M_fin\<^sub>C_af_lhs \<phi> (mapping.Mapping \<pi>) y = (\<forall>\<chi>\<in>dom \<pi>. S \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (map_option rk (Mapping.lookup y \<chi>)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q))
[PROOF STEP]
unfolding M_fin\<^sub>C_af_lhs_def Let_def And_prop_entailment_abs set_map Ball_def keys.abs_eq lookup.abs_eq
[PROOF STATE]
proof (prove)
using this:
?\<chi>2 \<in> dom \<pi> \<Longrightarrow> S \<up>\<Turnstile>\<^sub>P foldl and_abs (Abs ?\<chi>2) (map (\<up>eval\<^sub>G (dom \<pi>)) (drop (the (\<pi> ?\<chi>2)) (the (Mapping.lookup y ?\<chi>2)))) = (S \<up>\<Turnstile>\<^sub>P Abs ?\<chi>2 \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> ?\<chi>2). the (map_option rk (Mapping.lookup y ?\<chi>2)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q))

goal (1 subgoal):
 1. (\<forall>x. x \<in> (\<lambda>\<chi>. foldl and_abs (Abs \<chi>) (map (\<up>eval\<^sub>G (dom \<pi>)) (drop (the (\<pi> \<chi>)) (the (Mapping.lookup y \<chi>))))) ` set (filter (\<lambda>x. x \<in> dom \<pi>) (G_list \<phi>)) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P x) = (\<forall>x. x \<in> dom \<pi> \<longrightarrow> S \<up>\<Turnstile>\<^sub>P Abs x \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> x). the (map_option rk (Mapping.lookup y x)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q))
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
?\<chi>2 \<in> dom \<pi> \<Longrightarrow> S \<up>\<Turnstile>\<^sub>P foldl and_abs (Abs ?\<chi>2) (map (\<up>eval\<^sub>G (dom \<pi>)) (drop (the (\<pi> ?\<chi>2)) (the (Mapping.lookup y ?\<chi>2)))) = (S \<up>\<Turnstile>\<^sub>P Abs ?\<chi>2 \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> ?\<chi>2). the (map_option rk (Mapping.lookup y ?\<chi>2)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q))
dom \<pi> \<subseteq> \<^bold>G \<phi>

goal (1 subgoal):
 1. (\<forall>x. x \<in> (\<lambda>\<chi>. foldl and_abs (Abs \<chi>) (map (\<up>eval\<^sub>G (dom \<pi>)) (drop (the (\<pi> \<chi>)) (the (Mapping.lookup y \<chi>))))) ` set (filter (\<lambda>x. x \<in> dom \<pi>) (G_list \<phi>)) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P x) = (\<forall>x. x \<in> dom \<pi> \<longrightarrow> S \<up>\<Turnstile>\<^sub>P Abs x \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> x). the (map_option rk (Mapping.lookup y x)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q))
[PROOF STEP]
by (simp add: image_def inter_set_filter[symmetric] G_eq_G_list[symmetric]; blast)
[PROOF STATE]
proof (state)
this:
S \<up>\<Turnstile>\<^sub>P M_fin\<^sub>C_af_lhs \<phi> (mapping.Mapping \<pi>) y = (\<forall>\<chi>\<in>dom \<pi>. S \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (map_option rk (Mapping.lookup y \<chi>)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q))

goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?S2 \<up>\<Turnstile>\<^sub>P M_fin\<^sub>C_af_lhs \<phi> (mapping.Mapping \<pi>) y = (\<forall>\<chi>\<in>dom \<pi>. ?S2 \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (map_option rk (Mapping.lookup y \<chi>)) q = Some j) \<longrightarrow> ?S2 \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q))

goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?S2 \<up>\<Turnstile>\<^sub>P M_fin\<^sub>C_af_lhs \<phi> (mapping.Mapping \<pi>) y = (\<forall>\<chi>\<in>dom \<pi>. ?S2 \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (map_option rk (Mapping.lookup y \<chi>)) q = Some j) \<longrightarrow> ?S2 \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) q))

goal (1 subgoal):
 1. (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
by (simp add: ltl_prop_implies_def ltl_prop_implies_abs_def ltl_prop_entails_abs_def)
[PROOF STATE]
proof (state)
this:
(abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ltl_to_generalized_rabin\<^sub>C_af_correct:
  assumes "range w \<subseteq> set \<Sigma>"
  shows "w \<Turnstile> \<phi> \<longleftrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af \<Sigma> \<phi>) w"
  (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af \<Sigma> \<phi>) w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af \<Sigma> \<phi>) w
[PROOF STEP]
have X: "ltl_to_rabin_base_code \<up>af \<up>af\<^sub>G Abs Abs M_fin (set \<Sigma>) w M_fin\<^sub>C_af"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltl_to_rabin_base_code \<up>af \<up>af\<^sub>G Abs Abs M_fin (set \<Sigma>) w M_fin\<^sub>C_af
[PROOF STEP]
using ltl_to_generalized_rabin_af_wellformed[OF finite_set assms] M_fin\<^sub>C_af_correct assms
[PROOF STATE]
proof (prove)
using this:
ltl_to_rabin_af (set \<Sigma>) w
\<lbrakk>?t \<in> reach\<^sub>t ?\<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af \<up>af\<^sub>G Abs ?\<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C Abs Abs ?\<phi>); dom ?\<pi> \<subseteq> \<^bold>G ?\<phi>\<rbrakk> \<Longrightarrow> (abstract_transition ?t \<in> M_fin ?\<pi>) = M_fin\<^sub>C_af ?\<phi> (mapping.Mapping ?\<pi>) ?t
range w \<subseteq> set \<Sigma>

goal (1 subgoal):
 1. ltl_to_rabin_base_code \<up>af \<up>af\<^sub>G Abs Abs M_fin (set \<Sigma>) w M_fin\<^sub>C_af
[PROOF STEP]
unfolding ltl_to_rabin_af_def ltl_to_rabin_base_code_def ltl_to_rabin_base_code_axioms_def
[PROOF STATE]
proof (prove)
using this:
ltl_to_rabin_base \<up>af \<up>af\<^sub>G Abs Abs M_fin (set \<Sigma>) w
\<lbrakk>?t \<in> reach\<^sub>t ?\<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af \<up>af\<^sub>G Abs ?\<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C Abs Abs ?\<phi>); dom ?\<pi> \<subseteq> \<^bold>G ?\<phi>\<rbrakk> \<Longrightarrow> (abstract_transition ?t \<in> M_fin ?\<pi>) = M_fin\<^sub>C_af ?\<phi> (mapping.Mapping ?\<pi>) ?t
range w \<subseteq> set \<Sigma>

goal (1 subgoal):
 1. ltl_to_rabin_base \<up>af \<up>af\<^sub>G Abs Abs M_fin (set \<Sigma>) w \<and> (\<forall>t \<phi> \<pi>. t \<in> reach\<^sub>t (set \<Sigma>) (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af \<up>af\<^sub>G Abs (set \<Sigma>)) (ltl_to_rabin_base_code_def.initial\<^sub>C Abs Abs \<phi>) \<longrightarrow> dom \<pi> \<subseteq> \<^bold>G \<phi> \<longrightarrow> (abstract_transition t \<in> M_fin \<pi>) = M_fin\<^sub>C_af \<phi> (mapping.Mapping \<pi>) t)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ltl_to_rabin_base_code \<up>af \<up>af\<^sub>G Abs Abs M_fin (set \<Sigma>) w M_fin\<^sub>C_af

goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af \<Sigma> \<phi>) w
[PROOF STEP]
have "?lhs \<longleftrightarrow> accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af (set \<Sigma>) \<phi>) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af (set \<Sigma>) \<phi>) w
[PROOF STEP]
using assms ltl_to_generalized_rabin_af_correct
[PROOF STATE]
proof (prove)
using this:
range w \<subseteq> set \<Sigma>
\<lbrakk>finite ?\<Sigma>; range ?w \<subseteq> ?\<Sigma>\<rbrakk> \<Longrightarrow> ?w \<Turnstile> ?\<phi> = accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af ?\<Sigma> ?\<phi>) ?w

goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af (set \<Sigma>) \<phi>) w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af (set \<Sigma>) \<phi>) w

goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af \<Sigma> \<phi>) w
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af (set \<Sigma>) \<phi>) w

goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af \<Sigma> \<phi>) w
[PROOF STEP]
have "\<dots> \<longleftrightarrow> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af (set \<Sigma>) \<phi>) w = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af \<Sigma> \<phi>) w
[PROOF STEP]
using ltl_to_rabin_base_code.ltl_to_generalized_rabin\<^sub>C_correct[OF X]
[PROOF STATE]
proof (prove)
using this:
set \<Sigma> = set ?\<Sigma>' \<Longrightarrow> accept\<^sub>G\<^sub>R (ltl_to_rabin_base_def.ltl_to_generalized_rabin \<up>af \<up>af\<^sub>G Abs Abs M_fin (set \<Sigma>) ?\<phi>) w = accept\<^sub>G\<^sub>R_LTS (ltl_to_rabin_base_code_def.ltl_to_generalized_rabin\<^sub>C \<up>af \<up>af\<^sub>G Abs Abs M_fin\<^sub>C_af ?\<Sigma>' ?\<phi>) w

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af (set \<Sigma>) \<phi>) w = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af \<Sigma> \<phi>) w
[PROOF STEP]
unfolding ltl_to_generalized_rabin\<^sub>C_af_def
[PROOF STATE]
proof (prove)
using this:
set \<Sigma> = set ?\<Sigma>' \<Longrightarrow> accept\<^sub>G\<^sub>R (ltl_to_rabin_base_def.ltl_to_generalized_rabin \<up>af \<up>af\<^sub>G Abs Abs M_fin (set \<Sigma>) ?\<phi>) w = accept\<^sub>G\<^sub>R_LTS (ltl_to_rabin_base_code_def.ltl_to_generalized_rabin\<^sub>C \<up>af \<up>af\<^sub>G Abs Abs M_fin\<^sub>C_af ?\<Sigma>' ?\<phi>) w

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af (set \<Sigma>) \<phi>) w = accept\<^sub>G\<^sub>R_LTS (ltl_to_rabin_base_code_def.ltl_to_generalized_rabin\<^sub>C \<up>af \<up>af\<^sub>G Abs Abs M_fin\<^sub>C_af \<Sigma> \<phi>) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af (set \<Sigma>) \<phi>) w = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af \<Sigma> \<phi>) w

goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af \<Sigma> \<phi>) w
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af \<Sigma> \<phi>) w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af \<Sigma> \<phi>) w

goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af \<Sigma> \<phi>) w
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af \<Sigma> \<phi>) w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma M_fin\<^sub>C_af\<^sub>\<UU>_correct:
  assumes "t \<in> reach\<^sub>t \<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf\<^sub>G) \<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) \<phi>)"
  assumes "dom \<pi> \<subseteq> \<^bold>G \<phi>"
  shows "abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi> = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (Mapping.Mapping \<pi>) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
let ?delta = "ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf\<^sub>G) \<Sigma>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
let ?initial = "ltl_to_rabin_base_code_def.initial\<^sub>C (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) \<phi>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
obtain x y \<nu> z z' where t_def [simp]: "t = ((x, y), \<nu>, (z, z'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y \<nu> z z'. t = ((x, y), \<nu>, z, z') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
t = ((x, y), \<nu>, z, z')

goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
have "(x, y) \<in> reach \<Sigma> ?delta ?initial"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> reach \<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf\<^sub>G) \<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) \<phi>)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
t \<in> reach\<^sub>t \<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf\<^sub>G) \<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) \<phi>)

goal (1 subgoal):
 1. (x, y) \<in> reach \<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf\<^sub>G) \<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) \<phi>)
[PROOF STEP]
by (simp add: reach\<^sub>t_def reach_def; blast)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> reach \<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf\<^sub>G) \<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) \<phi>)

goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
hence N1: "\<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> Mapping.lookup y \<chi> \<noteq> None"
    and D1: "\<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> distinct (the (Mapping.lookup y \<chi>))"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> reach \<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf\<^sub>G) \<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) \<phi>)

goal (1 subgoal):
 1. (\<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> Mapping.lookup y \<chi> \<noteq> None) &&& (\<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> distinct (the (Mapping.lookup y \<chi>)))
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> reach \<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf\<^sub>G) \<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) \<phi>)
dom \<pi> \<subseteq> \<^bold>G \<phi>

goal (1 subgoal):
 1. (\<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> Mapping.lookup y \<chi> \<noteq> None) &&& (\<And>\<chi>. \<chi> \<in> dom \<pi> \<Longrightarrow> distinct (the (Mapping.lookup y \<chi>)))
[PROOF STEP]
by (blast dest: ltl_to_rabin_base_code_def.reach_delta_initial)+
[PROOF STATE]
proof (state)
this:
?\<chi> \<in> dom \<pi> \<Longrightarrow> Mapping.lookup y ?\<chi> \<noteq> None
?\<chi> \<in> dom \<pi> \<Longrightarrow> distinct (the (Mapping.lookup y ?\<chi>))

goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?\<chi> \<in> dom \<pi> \<Longrightarrow> Mapping.lookup y ?\<chi> \<noteq> None
?\<chi> \<in> dom \<pi> \<Longrightarrow> distinct (the (Mapping.lookup y ?\<chi>))

goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
fix S
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
let ?m' = "\<lambda>\<chi>. map_option rk (Mapping.lookup y \<chi>)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
fix \<chi>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
assume "\<chi> \<in> dom \<pi>"
[PROOF STATE]
proof (state)
this:
\<chi> \<in> dom \<pi>

goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
hence "S \<up>\<Turnstile>\<^sub>P (foldl and_abs (and_abs (Abs \<chi>) (\<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)))) (map (\<up>eval\<^sub>G (dom \<pi>) o (\<lambda>q. \<up>step q \<nu>)) (drop (the (\<pi> \<chi>)) (the (Mapping.lookup y \<chi>)))))
         \<longleftrightarrow> S \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)) \<and> (\<forall>q. (\<exists>j \<ge> the (\<pi> \<chi>). the (?m' \<chi>) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>))"
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> dom \<pi>

goal (1 subgoal):
 1. S \<up>\<Turnstile>\<^sub>P foldl and_abs Abs \<chi> \<up>and \<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)) (map (\<up>eval\<^sub>G (dom \<pi>) \<circ> (\<lambda>q. \<up>step q \<nu>)) (drop (the (\<pi> \<chi>)) (the (Mapping.lookup y \<chi>)))) = (S \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)) \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (map_option rk (Mapping.lookup y \<chi>)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>)))
[PROOF STEP]
using D1[THEN drop_rk, of _ "the (\<pi> \<chi>)"] N1[THEN option.map_sel, of _ rk]
[PROOF STATE]
proof (prove)
using this:
\<chi> \<in> dom \<pi>
?\<chi>1 \<in> dom \<pi> \<Longrightarrow> set (drop (the (\<pi> \<chi>)) (the (Mapping.lookup y ?\<chi>1))) = {q. \<exists>j\<ge>the (\<pi> \<chi>). rk (the (Mapping.lookup y ?\<chi>1)) q = Some j}
?\<chi>1 \<in> dom \<pi> \<Longrightarrow> the (map_option rk (Mapping.lookup y ?\<chi>1)) = rk (the (Mapping.lookup y ?\<chi>1))

goal (1 subgoal):
 1. S \<up>\<Turnstile>\<^sub>P foldl and_abs Abs \<chi> \<up>and \<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)) (map (\<up>eval\<^sub>G (dom \<pi>) \<circ> (\<lambda>q. \<up>step q \<nu>)) (drop (the (\<pi> \<chi>)) (the (Mapping.lookup y \<chi>)))) = (S \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)) \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (map_option rk (Mapping.lookup y \<chi>)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>)))
[PROOF STEP]
by (auto simp add: foldl_LTLAnd_prop_entailment_abs and_abs_conjunction simp del: rk.simps)
[PROOF STATE]
proof (state)
this:
S \<up>\<Turnstile>\<^sub>P foldl and_abs Abs \<chi> \<up>and \<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)) (map (\<up>eval\<^sub>G (dom \<pi>) \<circ> (\<lambda>q. \<up>step q \<nu>)) (drop (the (\<pi> \<chi>)) (the (Mapping.lookup y \<chi>)))) = (S \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)) \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (map_option rk (Mapping.lookup y \<chi>)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>)))

goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?\<chi>2 \<in> dom \<pi> \<Longrightarrow> S \<up>\<Turnstile>\<^sub>P foldl and_abs Abs ?\<chi>2 \<up>and \<up>eval\<^sub>G (dom \<pi>) (Abs (theG ?\<chi>2)) (map (\<up>eval\<^sub>G (dom \<pi>) \<circ> (\<lambda>q. \<up>step q \<nu>)) (drop (the (\<pi> ?\<chi>2)) (the (Mapping.lookup y ?\<chi>2)))) = (S \<up>\<Turnstile>\<^sub>P Abs ?\<chi>2 \<and> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG ?\<chi>2)) \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> ?\<chi>2). the (map_option rk (Mapping.lookup y ?\<chi>2)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>)))

goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
hence "S \<up>\<Turnstile>\<^sub>P (M_fin\<^sub>C_af\<^sub>\<UU>_lhs \<phi> (Mapping.Mapping \<pi>) y \<nu>)
      \<longleftrightarrow> ((\<forall>\<chi> \<in> dom \<pi>. (S \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)) \<and> (\<forall>q. (\<exists>j \<ge> the (\<pi> \<chi>). the (?m' \<chi>) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>)))))"
[PROOF STATE]
proof (prove)
using this:
?\<chi>2 \<in> dom \<pi> \<Longrightarrow> S \<up>\<Turnstile>\<^sub>P foldl and_abs Abs ?\<chi>2 \<up>and \<up>eval\<^sub>G (dom \<pi>) (Abs (theG ?\<chi>2)) (map (\<up>eval\<^sub>G (dom \<pi>) \<circ> (\<lambda>q. \<up>step q \<nu>)) (drop (the (\<pi> ?\<chi>2)) (the (Mapping.lookup y ?\<chi>2)))) = (S \<up>\<Turnstile>\<^sub>P Abs ?\<chi>2 \<and> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG ?\<chi>2)) \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> ?\<chi>2). the (map_option rk (Mapping.lookup y ?\<chi>2)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>)))

goal (1 subgoal):
 1. S \<up>\<Turnstile>\<^sub>P M_fin\<^sub>C_af\<^sub>\<UU>_lhs \<phi> (mapping.Mapping \<pi>) y \<nu> = (\<forall>\<chi>\<in>dom \<pi>. S \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)) \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (map_option rk (Mapping.lookup y \<chi>)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>)))
[PROOF STEP]
unfolding M_fin\<^sub>C_af\<^sub>\<UU>_lhs_def Let_def And_prop_entailment_abs set_map Ball_def keys.abs_eq lookup.abs_eq
[PROOF STATE]
proof (prove)
using this:
?\<chi>2 \<in> dom \<pi> \<Longrightarrow> S \<up>\<Turnstile>\<^sub>P foldl and_abs Abs ?\<chi>2 \<up>and \<up>eval\<^sub>G (dom \<pi>) (Abs (theG ?\<chi>2)) (map (\<up>eval\<^sub>G (dom \<pi>) \<circ> (\<lambda>q. \<up>step q \<nu>)) (drop (the (\<pi> ?\<chi>2)) (the (Mapping.lookup y ?\<chi>2)))) = (S \<up>\<Turnstile>\<^sub>P Abs ?\<chi>2 \<and> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG ?\<chi>2)) \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> ?\<chi>2). the (map_option rk (Mapping.lookup y ?\<chi>2)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>)))

goal (1 subgoal):
 1. (\<forall>x. x \<in> (\<lambda>\<chi>. foldl and_abs Abs \<chi> \<up>and \<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)) (map (\<up>eval\<^sub>G (dom \<pi>) \<circ> (\<lambda>q. \<up>step q \<nu>)) (drop (the (\<pi> \<chi>)) (the (Mapping.lookup y \<chi>))))) ` set (filter (\<lambda>x. x \<in> dom \<pi>) (G_list \<phi>)) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P x) = (\<forall>x. x \<in> dom \<pi> \<longrightarrow> S \<up>\<Turnstile>\<^sub>P Abs x \<and> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG x)) \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> x). the (map_option rk (Mapping.lookup y x)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>)))
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
?\<chi>2 \<in> dom \<pi> \<Longrightarrow> S \<up>\<Turnstile>\<^sub>P foldl and_abs Abs ?\<chi>2 \<up>and \<up>eval\<^sub>G (dom \<pi>) (Abs (theG ?\<chi>2)) (map (\<up>eval\<^sub>G (dom \<pi>) \<circ> (\<lambda>q. \<up>step q \<nu>)) (drop (the (\<pi> ?\<chi>2)) (the (Mapping.lookup y ?\<chi>2)))) = (S \<up>\<Turnstile>\<^sub>P Abs ?\<chi>2 \<and> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG ?\<chi>2)) \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> ?\<chi>2). the (map_option rk (Mapping.lookup y ?\<chi>2)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>)))
dom \<pi> \<subseteq> \<^bold>G \<phi>

goal (1 subgoal):
 1. (\<forall>x. x \<in> (\<lambda>\<chi>. foldl and_abs Abs \<chi> \<up>and \<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)) (map (\<up>eval\<^sub>G (dom \<pi>) \<circ> (\<lambda>q. \<up>step q \<nu>)) (drop (the (\<pi> \<chi>)) (the (Mapping.lookup y \<chi>))))) ` set (filter (\<lambda>x. x \<in> dom \<pi>) (G_list \<phi>)) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P x) = (\<forall>x. x \<in> dom \<pi> \<longrightarrow> S \<up>\<Turnstile>\<^sub>P Abs x \<and> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG x)) \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> x). the (map_option rk (Mapping.lookup y x)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>)))
[PROOF STEP]
by (simp add: image_def inter_set_filter[symmetric] G_eq_G_list[symmetric]; blast)
[PROOF STATE]
proof (state)
this:
S \<up>\<Turnstile>\<^sub>P M_fin\<^sub>C_af\<^sub>\<UU>_lhs \<phi> (mapping.Mapping \<pi>) y \<nu> = (\<forall>\<chi>\<in>dom \<pi>. S \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)) \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (map_option rk (Mapping.lookup y \<chi>)) q = Some j) \<longrightarrow> S \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>)))

goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?S2 \<up>\<Turnstile>\<^sub>P M_fin\<^sub>C_af\<^sub>\<UU>_lhs \<phi> (mapping.Mapping \<pi>) y \<nu> = (\<forall>\<chi>\<in>dom \<pi>. ?S2 \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> ?S2 \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)) \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (map_option rk (Mapping.lookup y \<chi>)) q = Some j) \<longrightarrow> ?S2 \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>)))

goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?S2 \<up>\<Turnstile>\<^sub>P M_fin\<^sub>C_af\<^sub>\<UU>_lhs \<phi> (mapping.Mapping \<pi>) y \<nu> = (\<forall>\<chi>\<in>dom \<pi>. ?S2 \<up>\<Turnstile>\<^sub>P Abs \<chi> \<and> ?S2 \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (Abs (theG \<chi>)) \<and> (\<forall>q. (\<exists>j\<ge>the (\<pi> \<chi>). the (map_option rk (Mapping.lookup y \<chi>)) q = Some j) \<longrightarrow> ?S2 \<up>\<Turnstile>\<^sub>P \<up>eval\<^sub>G (dom \<pi>) (\<up>step q \<nu>)))

goal (1 subgoal):
 1. (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t
[PROOF STEP]
by (simp add: ltl_prop_implies_def ltl_prop_implies_abs_def ltl_prop_entails_abs_def)
[PROOF STATE]
proof (state)
this:
(abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU>_correct:
  assumes "range w \<subseteq> set \<Sigma>"
  shows "w \<Turnstile> \<phi> \<longleftrightarrow> accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w"
  (is "?lhs \<longleftrightarrow> ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w
[PROOF STEP]
have X: "ltl_to_rabin_base_code \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) M\<^sub>\<UU>_fin (set \<Sigma>) w M_fin\<^sub>C_af\<^sub>\<UU>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ltl_to_rabin_base_code \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) M\<^sub>\<UU>_fin (set \<Sigma>) w M_fin\<^sub>C_af\<^sub>\<UU>
[PROOF STEP]
using ltl_to_generalized_rabin_af\<^sub>\<UU>_wellformed[OF finite_set assms] M_fin\<^sub>C_af\<^sub>\<UU>_correct assms
[PROOF STATE]
proof (prove)
using this:
ltl_to_rabin_af_unf (set \<Sigma>) w
\<lbrakk>?t \<in> reach\<^sub>t ?\<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf\<^sub>G) ?\<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) ?\<phi>); dom ?\<pi> \<subseteq> \<^bold>G ?\<phi>\<rbrakk> \<Longrightarrow> (abstract_transition ?t \<in> M\<^sub>\<UU>_fin ?\<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> ?\<phi> (mapping.Mapping ?\<pi>) ?t
range w \<subseteq> set \<Sigma>

goal (1 subgoal):
 1. ltl_to_rabin_base_code \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) M\<^sub>\<UU>_fin (set \<Sigma>) w M_fin\<^sub>C_af\<^sub>\<UU>
[PROOF STEP]
unfolding ltl_to_rabin_af_unf_def ltl_to_rabin_base_code_def ltl_to_rabin_base_code_axioms_def
[PROOF STATE]
proof (prove)
using this:
ltl_to_rabin_base \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) M\<^sub>\<UU>_fin (set \<Sigma>) w
\<lbrakk>?t \<in> reach\<^sub>t ?\<Sigma> (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf\<^sub>G) ?\<Sigma>) (ltl_to_rabin_base_code_def.initial\<^sub>C (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) ?\<phi>); dom ?\<pi> \<subseteq> \<^bold>G ?\<phi>\<rbrakk> \<Longrightarrow> (abstract_transition ?t \<in> M\<^sub>\<UU>_fin ?\<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> ?\<phi> (mapping.Mapping ?\<pi>) ?t
range w \<subseteq> set \<Sigma>

goal (1 subgoal):
 1. ltl_to_rabin_base \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) M\<^sub>\<UU>_fin (set \<Sigma>) w \<and> (\<forall>t \<phi> \<pi>. t \<in> reach\<^sub>t (set \<Sigma>) (ltl_to_rabin_base_code_def.delta\<^sub>C \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf\<^sub>G) (set \<Sigma>)) (ltl_to_rabin_base_code_def.initial\<^sub>C (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) \<phi>) \<longrightarrow> dom \<pi> \<subseteq> \<^bold>G \<phi> \<longrightarrow> (abstract_transition t \<in> M\<^sub>\<UU>_fin \<pi>) = M_fin\<^sub>C_af\<^sub>\<UU> \<phi> (mapping.Mapping \<pi>) t)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ltl_to_rabin_base_code \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) M\<^sub>\<UU>_fin (set \<Sigma>) w M_fin\<^sub>C_af\<^sub>\<UU>

goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w
[PROOF STEP]
have "?lhs \<longleftrightarrow> accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af\<^sub>\<UU> (set \<Sigma>) \<phi>) w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af\<^sub>\<UU> (set \<Sigma>) \<phi>) w
[PROOF STEP]
using assms ltl_to_generalized_rabin_af\<^sub>\<UU>_correct
[PROOF STATE]
proof (prove)
using this:
range w \<subseteq> set \<Sigma>
\<lbrakk>finite ?\<Sigma>; range ?w \<subseteq> ?\<Sigma>\<rbrakk> \<Longrightarrow> ?w \<Turnstile> ?\<phi> = accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af\<^sub>\<UU> ?\<Sigma> ?\<phi>) ?w

goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af\<^sub>\<UU> (set \<Sigma>) \<phi>) w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af\<^sub>\<UU> (set \<Sigma>) \<phi>) w

goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af\<^sub>\<UU> (set \<Sigma>) \<phi>) w

goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w
[PROOF STEP]
have "\<dots> \<longleftrightarrow> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af\<^sub>\<UU> (set \<Sigma>) \<phi>) w = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w
[PROOF STEP]
using ltl_to_rabin_base_code.ltl_to_generalized_rabin\<^sub>C_correct[OF X]
[PROOF STATE]
proof (prove)
using this:
set \<Sigma> = set ?\<Sigma>' \<Longrightarrow> accept\<^sub>G\<^sub>R (ltl_to_rabin_base_def.ltl_to_generalized_rabin \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) M\<^sub>\<UU>_fin (set \<Sigma>) ?\<phi>) w = accept\<^sub>G\<^sub>R_LTS (ltl_to_rabin_base_code_def.ltl_to_generalized_rabin\<^sub>C \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) M_fin\<^sub>C_af\<^sub>\<UU> ?\<Sigma>' ?\<phi>) w

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af\<^sub>\<UU> (set \<Sigma>) \<phi>) w = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w
[PROOF STEP]
unfolding ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU>_def
[PROOF STATE]
proof (prove)
using this:
set \<Sigma> = set ?\<Sigma>' \<Longrightarrow> accept\<^sub>G\<^sub>R (ltl_to_rabin_base_def.ltl_to_generalized_rabin \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) M\<^sub>\<UU>_fin (set \<Sigma>) ?\<phi>) w = accept\<^sub>G\<^sub>R_LTS (ltl_to_rabin_base_code_def.ltl_to_generalized_rabin\<^sub>C \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) M_fin\<^sub>C_af\<^sub>\<UU> ?\<Sigma>' ?\<phi>) w

goal (1 subgoal):
 1. accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af\<^sub>\<UU> (set \<Sigma>) \<phi>) w = accept\<^sub>G\<^sub>R_LTS (ltl_to_rabin_base_code_def.ltl_to_generalized_rabin\<^sub>C \<up>af\<^sub>\<UU> \<up>af\<^sub>G\<^sub>\<UU> (Abs \<circ> Unf) (Abs \<circ> Unf\<^sub>G) M_fin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
accept\<^sub>G\<^sub>R (ltl_to_generalized_rabin_af\<^sub>\<UU> (set \<Sigma>) \<phi>) w = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w

goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w

goal (1 subgoal):
 1. w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
w \<Turnstile> \<phi> = accept\<^sub>G\<^sub>R_LTS (ltl_to_generalized_rabin\<^sub>C_af\<^sub>\<UU> \<Sigma> \<phi>) w

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inj_on_finite:
  \<open>finite (f ` A) \<longleftrightarrow> finite A\<close> if \<open>inj_on f A\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (f ` A) = finite A
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
inj_on f A

goal (1 subgoal):
 1. finite (f ` A) = finite A
[PROOF STEP]
by (fact finite_image_iff)


[STATEMENT]
lemma finite_bounded_functions:
  assumes fS: "finite S"
  shows "finite T \<Longrightarrow> finite {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite T \<Longrightarrow> finite {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}
[PROOF STEP]
proof (induct T rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite {f. (\<forall>i\<in>{}. f i \<in> S) \<and> (\<forall>i. i \<notin> {} \<longrightarrow> f i = i)}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = i)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = i)}
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. finite {f. (\<forall>i\<in>{}. f i \<in> S) \<and> (\<forall>i. i \<notin> {} \<longrightarrow> f i = i)}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = i)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = i)}
[PROOF STEP]
have th: "{f. \<forall>i. f i = i} = {id}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f. \<forall>i. f i = i} = {id}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{f. \<forall>i. f i = i} = {id}

goal (2 subgoals):
 1. finite {f. (\<forall>i\<in>{}. f i \<in> S) \<and> (\<forall>i. i \<notin> {} \<longrightarrow> f i = i)}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = i)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = i)}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {f. (\<forall>i\<in>{}. f i \<in> S) \<and> (\<forall>i. i \<notin> {} \<longrightarrow> f i = i)}
[PROOF STEP]
by (auto simp add: th)
[PROOF STATE]
proof (state)
this:
finite {f. (\<forall>i\<in>{}. f i \<in> S) \<and> (\<forall>i. i \<notin> {} \<longrightarrow> f i = i)}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = i)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = i)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = i)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = i)}
[PROOF STEP]
case (insert a T)
[PROOF STATE]
proof (state)
this:
finite T
a \<notin> T
finite {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = i)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = i)}
[PROOF STEP]
let ?f = "\<lambda>(y,g) i. if i = a then y else g i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = i)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = i)}
[PROOF STEP]
let ?S = "?f ` (S \<times> {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)})"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = i)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = i)}
[PROOF STEP]
have "?S = {f. (\<forall>i\<in> insert a T. f i \<in> S) \<and> (\<forall>i. i \<notin> insert a T \<longrightarrow> f i = i)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(y, g) i. if i = a then y else g i) ` (S \<times> {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}) = {f. (\<forall>i\<in>insert a T. f i \<in> S) \<and> (\<forall>i. i \<notin> insert a T \<longrightarrow> f i = i)}
[PROOF STEP]
apply (auto simp add: image_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x a \<in> S; \<forall>i\<in>T. x i \<in> S; \<forall>i. i \<noteq> a \<and> i \<notin> T \<longrightarrow> x i = i\<rbrakk> \<Longrightarrow> \<exists>xa\<in>S. \<exists>y. (\<forall>i\<in>T. y i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> y i = i) \<and> x = (\<lambda>i. if i = a then xa else y i)
[PROOF STEP]
apply (rule_tac x="x a" in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x a \<in> S; \<forall>i\<in>T. x i \<in> S; \<forall>i. i \<noteq> a \<and> i \<notin> T \<longrightarrow> x i = i\<rbrakk> \<Longrightarrow> \<exists>y. (\<forall>i\<in>T. y i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> y i = i) \<and> x = (\<lambda>i. if i = a then x a else y i)
 2. \<And>x. \<lbrakk>x a \<in> S; \<forall>i\<in>T. x i \<in> S; \<forall>i. i \<noteq> a \<and> i \<notin> T \<longrightarrow> x i = i\<rbrakk> \<Longrightarrow> x a \<in> S
[PROOF STEP]
apply (rule_tac x = "\<lambda>i. if i = a then i else x i" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x a \<in> S; \<forall>i\<in>T. x i \<in> S; \<forall>i. i \<noteq> a \<and> i \<notin> T \<longrightarrow> x i = i\<rbrakk> \<Longrightarrow> (\<forall>i\<in>T. (if i = a then i else x i) \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> (if i = a then i else x i) = i) \<and> x = (\<lambda>i. if i = a then x a else if i = a then i else x i)
 2. \<And>x. \<lbrakk>x a \<in> S; \<forall>i\<in>T. x i \<in> S; \<forall>i. i \<noteq> a \<and> i \<notin> T \<longrightarrow> x i = i\<rbrakk> \<Longrightarrow> x a \<in> S
[PROOF STEP]
apply (insert insert, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>(y, g) i. if i = a then y else g i) ` (S \<times> {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}) = {f. (\<forall>i\<in>insert a T. f i \<in> S) \<and> (\<forall>i. i \<notin> insert a T \<longrightarrow> f i = i)}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = i)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = i)}
[PROOF STEP]
with finite_imageI[OF finite_cartesian_product[OF fS insert.hyps(3)], of ?f]
[PROOF STATE]
proof (chain)
picking this:
finite ((\<lambda>(y, g) i. if i = a then y else g i) ` (S \<times> {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}))
(\<lambda>(y, g) i. if i = a then y else g i) ` (S \<times> {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}) = {f. (\<forall>i\<in>insert a T. f i \<in> S) \<and> (\<forall>i. i \<notin> insert a T \<longrightarrow> f i = i)}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite ((\<lambda>(y, g) i. if i = a then y else g i) ` (S \<times> {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}))
(\<lambda>(y, g) i. if i = a then y else g i) ` (S \<times> {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}) = {f. (\<forall>i\<in>insert a T. f i \<in> S) \<and> (\<forall>i. i \<notin> insert a T \<longrightarrow> f i = i)}

goal (1 subgoal):
 1. finite {f. (\<forall>i\<in>insert a T. f i \<in> S) \<and> (\<forall>i. i \<notin> insert a T \<longrightarrow> f i = i)}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
finite {f. (\<forall>i\<in>insert a T. f i \<in> S) \<and> (\<forall>i. i \<notin> insert a T \<longrightarrow> f i = i)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_bounded_functions':
  assumes fS: "finite S"
  shows "finite T \<Longrightarrow> finite {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = j)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite T \<Longrightarrow> finite {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = j)}
[PROOF STEP]
proof (induct T rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite {f. (\<forall>i\<in>{}. f i \<in> S) \<and> (\<forall>i. i \<notin> {} \<longrightarrow> f i = j)}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = j)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = j)}
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. finite {f. (\<forall>i\<in>{}. f i \<in> S) \<and> (\<forall>i. i \<notin> {} \<longrightarrow> f i = j)}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = j)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = j)}
[PROOF STEP]
have th: "{f. \<forall>i. f i = j} = {(\<lambda> x. j)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {f. \<forall>i. f i = j} = {\<lambda>x. j}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{f. \<forall>i. f i = j} = {\<lambda>x. j}

goal (2 subgoals):
 1. finite {f. (\<forall>i\<in>{}. f i \<in> S) \<and> (\<forall>i. i \<notin> {} \<longrightarrow> f i = j)}
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = j)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = j)}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {f. (\<forall>i\<in>{}. f i \<in> S) \<and> (\<forall>i. i \<notin> {} \<longrightarrow> f i = j)}
[PROOF STEP]
by (auto simp add: th)
[PROOF STATE]
proof (state)
this:
finite {f. (\<forall>i\<in>{}. f i \<in> S) \<and> (\<forall>i. i \<notin> {} \<longrightarrow> f i = j)}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = j)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = j)}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = j)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = j)}
[PROOF STEP]
case (insert a T)
[PROOF STATE]
proof (state)
this:
finite T
a \<notin> T
finite {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = j)}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = j)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = j)}
[PROOF STEP]
let ?f = "\<lambda>(y,g) i. if i = a then y else g i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = j)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = j)}
[PROOF STEP]
let ?S = "?f ` (S \<times> {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = j)})"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = j)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = j)}
[PROOF STEP]
have "?S = {f. (\<forall>i\<in> insert a T. f i \<in> S) \<and> (\<forall>i. i \<notin> insert a T \<longrightarrow> f i = j)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(y, g) i. if i = a then y else g i) ` (S \<times> {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = j)}) = {f. (\<forall>i\<in>insert a T. f i \<in> S) \<and> (\<forall>i. i \<notin> insert a T \<longrightarrow> f i = j)}
[PROOF STEP]
apply (auto simp add: image_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>x a \<in> S; \<forall>i\<in>T. x i \<in> S; \<forall>i. i \<noteq> a \<and> i \<notin> T \<longrightarrow> x i = j\<rbrakk> \<Longrightarrow> \<exists>xa\<in>S. \<exists>y. (\<forall>i\<in>T. y i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> y i = j) \<and> x = (\<lambda>i. if i = a then xa else y i)
[PROOF STEP]
apply (rule_tac x="x a" in bexI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x a \<in> S; \<forall>i\<in>T. x i \<in> S; \<forall>i. i \<noteq> a \<and> i \<notin> T \<longrightarrow> x i = j\<rbrakk> \<Longrightarrow> \<exists>y. (\<forall>i\<in>T. y i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> y i = j) \<and> x = (\<lambda>i. if i = a then x a else y i)
 2. \<And>x. \<lbrakk>x a \<in> S; \<forall>i\<in>T. x i \<in> S; \<forall>i. i \<noteq> a \<and> i \<notin> T \<longrightarrow> x i = j\<rbrakk> \<Longrightarrow> x a \<in> S
[PROOF STEP]
apply (rule_tac x = "\<lambda>i. if i = a then j else x i" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>x a \<in> S; \<forall>i\<in>T. x i \<in> S; \<forall>i. i \<noteq> a \<and> i \<notin> T \<longrightarrow> x i = j\<rbrakk> \<Longrightarrow> (\<forall>i\<in>T. (if i = a then j else x i) \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> (if i = a then j else x i) = j) \<and> x = (\<lambda>i. if i = a then x a else if i = a then j else x i)
 2. \<And>x. \<lbrakk>x a \<in> S; \<forall>i\<in>T. x i \<in> S; \<forall>i. i \<noteq> a \<and> i \<notin> T \<longrightarrow> x i = j\<rbrakk> \<Longrightarrow> x a \<in> S
[PROOF STEP]
apply (insert insert, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<lambda>(y, g) i. if i = a then y else g i) ` (S \<times> {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = j)}) = {f. (\<forall>i\<in>insert a T. f i \<in> S) \<and> (\<forall>i. i \<notin> insert a T \<longrightarrow> f i = j)}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; finite {f. (\<forall>i\<in>F. f i \<in> S) \<and> (\<forall>i. i \<notin> F \<longrightarrow> f i = j)}\<rbrakk> \<Longrightarrow> finite {f. (\<forall>i\<in>insert x F. f i \<in> S) \<and> (\<forall>i. i \<notin> insert x F \<longrightarrow> f i = j)}
[PROOF STEP]
with finite_imageI[OF finite_cartesian_product[OF fS insert.hyps(3)], of ?f]
[PROOF STATE]
proof (chain)
picking this:
finite ((\<lambda>(y, g) i. if i = a then y else g i) ` (S \<times> {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = j)}))
(\<lambda>(y, g) i. if i = a then y else g i) ` (S \<times> {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = j)}) = {f. (\<forall>i\<in>insert a T. f i \<in> S) \<and> (\<forall>i. i \<notin> insert a T \<longrightarrow> f i = j)}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite ((\<lambda>(y, g) i. if i = a then y else g i) ` (S \<times> {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = j)}))
(\<lambda>(y, g) i. if i = a then y else g i) ` (S \<times> {f. (\<forall>i\<in>T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = j)}) = {f. (\<forall>i\<in>insert a T. f i \<in> S) \<and> (\<forall>i. i \<notin> insert a T \<longrightarrow> f i = j)}

goal (1 subgoal):
 1. finite {f. (\<forall>i\<in>insert a T. f i \<in> S) \<and> (\<forall>i. i \<notin> insert a T \<longrightarrow> f i = j)}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
finite {f. (\<forall>i\<in>insert a T. f i \<in> S) \<and> (\<forall>i. i \<notin> insert a T \<longrightarrow> f i = j)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma permutes_less [simp]:
  assumes p: "p permutes {0..<(n :: nat)}"
  shows
    "i < n \<Longrightarrow> p i < n"
    "i < n \<Longrightarrow> inv p i < n"
    "p (inv p i) = i"
    "inv p (p i) = i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((i < n \<Longrightarrow> p i < n) &&& (i < n \<Longrightarrow> inv p i < n)) &&& p (inv p i) = i &&& inv p (p i) = i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p permutes {0..<n}

goal (1 subgoal):
 1. ((i < n \<Longrightarrow> p i < n) &&& (i < n \<Longrightarrow> inv p i < n)) &&& p (inv p i) = i &&& inv p (p i) = i
[PROOF STEP]
by (simp_all add: permutes_inverses permutes_nat_less permutes_nat_inv_less)


[STATEMENT]
lemma permutes_prod:
  assumes p: "p permutes S"
  shows "(\<Prod>s\<in>S. f (p s) s) = (\<Prod>s\<in>S. f s (inv p s))"
    (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>s\<in>S. f (p s) s) = (\<Prod>s\<in>S. f s (inv p s))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p permutes S

goal (1 subgoal):
 1. (\<Prod>s\<in>S. f (p s) s) = (\<Prod>s\<in>S. f s (inv p s))
[PROOF STEP]
by (fact prod.permutes_inv)


[STATEMENT]
lemma permutes_sum:
  assumes p: "p permutes S"
  shows "(\<Sum>s\<in>S. f (p s) s) = (\<Sum>s\<in>S. f s (inv p s))"
    (is "?l = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>s\<in>S. f (p s) s) = (\<Sum>s\<in>S. f s (inv p s))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p permutes S

goal (1 subgoal):
 1. (\<Sum>s\<in>S. f (p s) s) = (\<Sum>s\<in>S. f s (inv p s))
[PROOF STEP]
by (fact sum.permutes_inv)


[STATEMENT]
lemma permutes_memb: fixes p :: "'b \<Rightarrow> 'b"
  assumes p: "p permutes B"
  and a: "a \<in> A"
  defines "ip \<equiv> Hilbert_Choice.inv p"
  shows "a \<in> A" "a_to_b a \<in> B" "ip (a_to_b a) \<in> B" "p (a_to_b a) \<in> B"
    "b_to_a (p (a_to_b a)) \<in> A" "b_to_a (ip (a_to_b a)) \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a \<in> A &&& a_to_b a \<in> B &&& ip (a_to_b a) \<in> B) &&& p (a_to_b a) \<in> B &&& b_to_a (p (a_to_b a)) \<in> A &&& b_to_a (ip (a_to_b a)) \<in> A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. a \<in> A
 2. a_to_b a \<in> B
 3. ip (a_to_b a) \<in> B
 4. p (a_to_b a) \<in> B
 5. b_to_a (p (a_to_b a)) \<in> A
 6. b_to_a (ip (a_to_b a)) \<in> A
[PROOF STEP]
let ?b = "a_to_b a"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. a \<in> A
 2. a_to_b a \<in> B
 3. ip (a_to_b a) \<in> B
 4. p (a_to_b a) \<in> B
 5. b_to_a (p (a_to_b a)) \<in> A
 6. b_to_a (ip (a_to_b a)) \<in> A
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
p permutes B
[PROOF STEP]
have ip: "ip permutes B"
[PROOF STATE]
proof (prove)
using this:
p permutes B

goal (1 subgoal):
 1. ip permutes B
[PROOF STEP]
unfolding ip_def
[PROOF STATE]
proof (prove)
using this:
p permutes B

goal (1 subgoal):
 1. inv p permutes B
[PROOF STEP]
by (rule permutes_inv)
[PROOF STATE]
proof (state)
this:
ip permutes B

goal (6 subgoals):
 1. a \<in> A
 2. a_to_b a \<in> B
 3. ip (a_to_b a) \<in> B
 4. p (a_to_b a) \<in> B
 5. b_to_a (p (a_to_b a)) \<in> A
 6. b_to_a (ip (a_to_b a)) \<in> A
[PROOF STEP]
note in_ip = permutes_in_image[OF ip]
[PROOF STATE]
proof (state)
this:
(ip ?x \<in> B) = (?x \<in> B)

goal (6 subgoals):
 1. a \<in> A
 2. a_to_b a \<in> B
 3. ip (a_to_b a) \<in> B
 4. p (a_to_b a) \<in> B
 5. b_to_a (p (a_to_b a)) \<in> A
 6. b_to_a (ip (a_to_b a)) \<in> A
[PROOF STEP]
note in_p = permutes_in_image[OF p]
[PROOF STATE]
proof (state)
this:
(p ?x \<in> B) = (?x \<in> B)

goal (6 subgoals):
 1. a \<in> A
 2. a_to_b a \<in> B
 3. ip (a_to_b a) \<in> B
 4. p (a_to_b a) \<in> B
 5. b_to_a (p (a_to_b a)) \<in> A
 6. b_to_a (ip (a_to_b a)) \<in> A
[PROOF STEP]
show a: "a \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in> A
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
a \<in> A

goal (5 subgoals):
 1. a_to_b a \<in> B
 2. ip (a_to_b a) \<in> B
 3. p (a_to_b a) \<in> B
 4. b_to_a (p (a_to_b a)) \<in> A
 5. b_to_a (ip (a_to_b a)) \<in> A
[PROOF STEP]
show b: "?b \<in> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_to_b a \<in> B
[PROOF STEP]
by (rule ab[OF a])
[PROOF STATE]
proof (state)
this:
a_to_b a \<in> B

goal (4 subgoals):
 1. ip (a_to_b a) \<in> B
 2. p (a_to_b a) \<in> B
 3. b_to_a (p (a_to_b a)) \<in> A
 4. b_to_a (ip (a_to_b a)) \<in> A
[PROOF STEP]
show pb: "p ?b \<in> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p (a_to_b a) \<in> B
[PROOF STEP]
unfolding in_p
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_to_b a \<in> B
[PROOF STEP]
by (rule b)
[PROOF STATE]
proof (state)
this:
p (a_to_b a) \<in> B

goal (3 subgoals):
 1. ip (a_to_b a) \<in> B
 2. b_to_a (p (a_to_b a)) \<in> A
 3. b_to_a (ip (a_to_b a)) \<in> A
[PROOF STEP]
show ipb: "ip ?b \<in> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ip (a_to_b a) \<in> B
[PROOF STEP]
unfolding in_ip
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a_to_b a \<in> B
[PROOF STEP]
by (rule b)
[PROOF STATE]
proof (state)
this:
ip (a_to_b a) \<in> B

goal (2 subgoals):
 1. b_to_a (p (a_to_b a)) \<in> A
 2. b_to_a (ip (a_to_b a)) \<in> A
[PROOF STEP]
show "b_to_a (p ?b) \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_to_a (p (a_to_b a)) \<in> A
[PROOF STEP]
by (rule ba[OF pb])
[PROOF STATE]
proof (state)
this:
b_to_a (p (a_to_b a)) \<in> A

goal (1 subgoal):
 1. b_to_a (ip (a_to_b a)) \<in> A
[PROOF STEP]
show "b_to_a (ip ?b) \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_to_a (ip (a_to_b a)) \<in> A
[PROOF STEP]
by (rule ba[OF ipb])
[PROOF STATE]
proof (state)
this:
b_to_a (ip (a_to_b a)) \<in> A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma permutes_bij_main:
  "{p . p permutes A} \<supseteq> (\<lambda> p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p . p permutes B}"
  (is "?A \<supseteq> ?f ` ?B")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<subseteq> {p. p permutes A}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
note d = permutes_def
[PROOF STATE]
proof (state)
this:
(?p permutes ?S) = ((\<forall>x. x \<notin> ?S \<longrightarrow> ?p x = x) \<and> (\<forall>y. \<exists>!x. ?p x = y))

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
let ?g = "\<lambda> q b. if b \<in> B then a_to_b (q (b_to_a b)) else b"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
let ?inv = "Hilbert_Choice.inv"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
assume p: "p \<in> ?f ` ?B"
[PROOF STATE]
proof (state)
this:
p \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}
[PROOF STEP]
obtain q where q: "q permutes B" and p: "p = ?f q"
[PROOF STATE]
proof (prove)
using this:
p \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B}

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>q permutes B; p = (\<lambda>a. if a \<in> A then b_to_a (q (a_to_b a)) else a)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q permutes B
p = (\<lambda>a. if a \<in> A then b_to_a (q (a_to_b a)) else a)

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
let ?iq = "?inv q"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
from q
[PROOF STATE]
proof (chain)
picking this:
q permutes B
[PROOF STEP]
have iq: "?iq permutes B"
[PROOF STATE]
proof (prove)
using this:
q permutes B

goal (1 subgoal):
 1. inv q permutes B
[PROOF STEP]
by (rule permutes_inv)
[PROOF STATE]
proof (state)
this:
inv q permutes B

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
note in_iq = permutes_in_image[OF iq]
[PROOF STATE]
proof (state)
this:
(inv q ?x \<in> B) = (?x \<in> B)

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
note in_q = permutes_in_image[OF q]
[PROOF STATE]
proof (state)
this:
(q ?x \<in> B) = (?x \<in> B)

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
have qiB: "\<And> b. b \<in> B \<Longrightarrow> q (?iq b) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. b \<in> B \<Longrightarrow> q (inv q b) = b
[PROOF STEP]
using q
[PROOF STATE]
proof (prove)
using this:
q permutes B

goal (1 subgoal):
 1. \<And>b. b \<in> B \<Longrightarrow> q (inv q b) = b
[PROOF STEP]
by (rule permutes_inverses)
[PROOF STATE]
proof (state)
this:
?b1 \<in> B \<Longrightarrow> q (inv q ?b1) = ?b1

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
have iqB: "\<And> b. b \<in> B \<Longrightarrow> ?iq (q b) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b. b \<in> B \<Longrightarrow> inv q (q b) = b
[PROOF STEP]
using q
[PROOF STATE]
proof (prove)
using this:
q permutes B

goal (1 subgoal):
 1. \<And>b. b \<in> B \<Longrightarrow> inv q (q b) = b
[PROOF STEP]
by (rule permutes_inverses)
[PROOF STATE]
proof (state)
this:
?b1 \<in> B \<Longrightarrow> inv q (q ?b1) = ?b1

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
from q[unfolded d]
[PROOF STATE]
proof (chain)
picking this:
(\<forall>x. x \<notin> B \<longrightarrow> q x = x) \<and> (\<forall>y. \<exists>!x. q x = y)
[PROOF STEP]
have q1: "\<And> b. b \<notin> B \<Longrightarrow> q b = b"
   and q2: "\<And> b. \<exists>!b'. q b' = b"
[PROOF STATE]
proof (prove)
using this:
(\<forall>x. x \<notin> B \<longrightarrow> q x = x) \<and> (\<forall>y. \<exists>!x. q x = y)

goal (1 subgoal):
 1. (\<And>b. b \<notin> B \<Longrightarrow> q b = b) &&& (\<And>b. \<exists>!b'. q b' = b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?b1 \<notin> B \<Longrightarrow> q ?b1 = ?b1
\<exists>!b'. q b' = ?b1

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
note memb = permutes_memb[OF q]
[PROOF STATE]
proof (state)
this:
?a \<in> A \<Longrightarrow> ?a \<in> A
?a \<in> A \<Longrightarrow> a_to_b ?a \<in> B
?a \<in> A \<Longrightarrow> inv q (a_to_b ?a) \<in> B
?a \<in> A \<Longrightarrow> q (a_to_b ?a) \<in> B
?a \<in> A \<Longrightarrow> b_to_a (q (a_to_b ?a)) \<in> A
?a \<in> A \<Longrightarrow> b_to_a (inv q (a_to_b ?a)) \<in> A

goal (1 subgoal):
 1. \<And>x. x \<in> (\<lambda>p a. if a \<in> A then b_to_a (p (a_to_b a)) else a) ` {p. p permutes B} \<Longrightarrow> x \<in> {p. p permutes A}
[PROOF STEP]
show "p \<in> ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> {p. p permutes A}
[PROOF STEP]
unfolding p d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a. if a \<in> A then b_to_a (q (a_to_b a)) else a) \<in> {p. (\<forall>x. x \<notin> A \<longrightarrow> p x = x) \<and> (\<forall>y. \<exists>!x. p x = y)}
[PROOF STEP]
proof (rule, intro conjI impI allI, force)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>!x. (if x \<in> A then b_to_a (q (a_to_b x)) else x) = y
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. \<exists>!x. (if x \<in> A then b_to_a (q (a_to_b x)) else x) = y
[PROOF STEP]
show "\<exists>!a'. ?f q a' = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
[PROOF STEP]
proof (cases "a \<in> A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> A \<Longrightarrow> \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
 2. a \<notin> A \<Longrightarrow> \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a \<in> A

goal (2 subgoals):
 1. a \<in> A \<Longrightarrow> \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
 2. a \<notin> A \<Longrightarrow> \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
[PROOF STEP]
note a = memb[OF True]
[PROOF STATE]
proof (state)
this:
a \<in> A
a_to_b a \<in> B
inv q (a_to_b a) \<in> B
q (a_to_b a) \<in> B
b_to_a (q (a_to_b a)) \<in> A
b_to_a (inv q (a_to_b a)) \<in> A

goal (2 subgoals):
 1. a \<in> A \<Longrightarrow> \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
 2. a \<notin> A \<Longrightarrow> \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
[PROOF STEP]
let ?a = "b_to_a (?iq (a_to_b a))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<in> A \<Longrightarrow> \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
 2. a \<notin> A \<Longrightarrow> \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (if ?a \<in> A then b_to_a (q (a_to_b ?a)) else ?a) = a
 2. \<And>a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a \<Longrightarrow> a' = ?a
[PROOF STEP]
show "?f q ?a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if b_to_a (inv q (a_to_b a)) \<in> A then b_to_a (q (a_to_b (b_to_a (inv q (a_to_b a))))) else b_to_a (inv q (a_to_b a))) = a
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
a \<in> A
a_to_b a \<in> B
inv q (a_to_b a) \<in> B
q (a_to_b a) \<in> B
b_to_a (q (a_to_b a)) \<in> A
b_to_a (inv q (a_to_b a)) \<in> A

goal (1 subgoal):
 1. (if b_to_a (inv q (a_to_b a)) \<in> A then b_to_a (q (a_to_b (b_to_a (inv q (a_to_b a))))) else b_to_a (inv q (a_to_b a))) = a
[PROOF STEP]
by (simp add: ba_ab qiB ab_ba)
[PROOF STATE]
proof (state)
this:
(if b_to_a (inv q (a_to_b a)) \<in> A then b_to_a (q (a_to_b (b_to_a (inv q (a_to_b a))))) else b_to_a (inv q (a_to_b a))) = a

goal (1 subgoal):
 1. \<And>a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
fix a'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
assume id: "?f q a' = a"
[PROOF STATE]
proof (state)
this:
(if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a

goal (1 subgoal):
 1. \<And>a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
show "a' = ?a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
proof (cases "a' \<in> A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a' \<in> A \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
 2. a' \<notin> A \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a' \<notin> A

goal (2 subgoals):
 1. a' \<in> A \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
 2. a' \<notin> A \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
a' \<notin> A

goal (1 subgoal):
 1. a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
using id a
[PROOF STATE]
proof (prove)
using this:
a' \<notin> A
(if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
a \<in> A
a_to_b a \<in> B
inv q (a_to_b a) \<in> B
q (a_to_b a) \<in> B
b_to_a (q (a_to_b a)) \<in> A
b_to_a (inv q (a_to_b a)) \<in> A

goal (1 subgoal):
 1. a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a' = b_to_a (inv q (a_to_b a))

goal (1 subgoal):
 1. a' \<in> A \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a' \<in> A \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a' \<in> A

goal (1 subgoal):
 1. a' \<in> A \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
note a' = memb[OF this]
[PROOF STATE]
proof (state)
this:
a' \<in> A
a_to_b a' \<in> B
inv q (a_to_b a') \<in> B
q (a_to_b a') \<in> B
b_to_a (q (a_to_b a')) \<in> A
b_to_a (inv q (a_to_b a')) \<in> A

goal (1 subgoal):
 1. a' \<in> A \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
from id True
[PROOF STATE]
proof (chain)
picking this:
(if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
a' \<in> A
[PROOF STEP]
have "b_to_a (q (a_to_b a')) = a"
[PROOF STATE]
proof (prove)
using this:
(if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
a' \<in> A

goal (1 subgoal):
 1. b_to_a (q (a_to_b a')) = a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b_to_a (q (a_to_b a')) = a

goal (1 subgoal):
 1. a' \<in> A \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
from arg_cong[OF this, of "a_to_b"] a' a
[PROOF STATE]
proof (chain)
picking this:
a_to_b (b_to_a (q (a_to_b a'))) = a_to_b a
a' \<in> A
a_to_b a' \<in> B
inv q (a_to_b a') \<in> B
q (a_to_b a') \<in> B
b_to_a (q (a_to_b a')) \<in> A
b_to_a (inv q (a_to_b a')) \<in> A
a \<in> A
a_to_b a \<in> B
inv q (a_to_b a) \<in> B
q (a_to_b a) \<in> B
b_to_a (q (a_to_b a)) \<in> A
b_to_a (inv q (a_to_b a)) \<in> A
[PROOF STEP]
have "q (a_to_b a') = a_to_b a"
[PROOF STATE]
proof (prove)
using this:
a_to_b (b_to_a (q (a_to_b a'))) = a_to_b a
a' \<in> A
a_to_b a' \<in> B
inv q (a_to_b a') \<in> B
q (a_to_b a') \<in> B
b_to_a (q (a_to_b a')) \<in> A
b_to_a (inv q (a_to_b a')) \<in> A
a \<in> A
a_to_b a \<in> B
inv q (a_to_b a) \<in> B
q (a_to_b a) \<in> B
b_to_a (q (a_to_b a)) \<in> A
b_to_a (inv q (a_to_b a)) \<in> A

goal (1 subgoal):
 1. q (a_to_b a') = a_to_b a
[PROOF STEP]
by (simp add: ba_ab)
[PROOF STATE]
proof (state)
this:
q (a_to_b a') = a_to_b a

goal (1 subgoal):
 1. a' \<in> A \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
from arg_cong[OF this, of ?iq]
[PROOF STATE]
proof (chain)
picking this:
inv q (q (a_to_b a')) = inv q (a_to_b a)
[PROOF STEP]
have "a_to_b a' = ?iq (a_to_b a)"
[PROOF STATE]
proof (prove)
using this:
inv q (q (a_to_b a')) = inv q (a_to_b a)

goal (1 subgoal):
 1. a_to_b a' = inv q (a_to_b a)
[PROOF STEP]
unfolding iqB[OF a'(2)]
[PROOF STATE]
proof (prove)
using this:
a_to_b a' = inv q (a_to_b a)

goal (1 subgoal):
 1. a_to_b a' = inv q (a_to_b a)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a_to_b a' = inv q (a_to_b a)

goal (1 subgoal):
 1. a' \<in> A \<Longrightarrow> a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
from arg_cong[OF this, of b_to_a]
[PROOF STATE]
proof (chain)
picking this:
b_to_a (a_to_b a') = b_to_a (inv q (a_to_b a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b_to_a (a_to_b a') = b_to_a (inv q (a_to_b a))

goal (1 subgoal):
 1. a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
unfolding ab_ba[OF True]
[PROOF STATE]
proof (prove)
using this:
a' = b_to_a (inv q (a_to_b a))

goal (1 subgoal):
 1. a' = b_to_a (inv q (a_to_b a))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
a' = b_to_a (inv q (a_to_b a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a' = b_to_a (inv q (a_to_b a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a

goal (1 subgoal):
 1. a \<notin> A \<Longrightarrow> \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a \<notin> A \<Longrightarrow> \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a \<notin> A

goal (1 subgoal):
 1. a \<notin> A \<Longrightarrow> \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
[PROOF STEP]
note a = this
[PROOF STATE]
proof (state)
this:
a \<notin> A

goal (1 subgoal):
 1. a \<notin> A \<Longrightarrow> \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (if ?a \<in> A then b_to_a (q (a_to_b ?a)) else ?a) = a
 2. \<And>a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a \<Longrightarrow> a' = ?a
[PROOF STEP]
show "?f q a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if a \<in> A then b_to_a (q (a_to_b a)) else a) = a
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
a \<notin> A

goal (1 subgoal):
 1. (if a \<in> A then b_to_a (q (a_to_b a)) else a) = a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(if a \<in> A then b_to_a (q (a_to_b a)) else a) = a

goal (1 subgoal):
 1. \<And>a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a \<Longrightarrow> a' = a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a \<Longrightarrow> a' = a
[PROOF STEP]
fix a'
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a \<Longrightarrow> a' = a
[PROOF STEP]
assume id: "?f q a' = a"
[PROOF STATE]
proof (state)
this:
(if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a

goal (1 subgoal):
 1. \<And>a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a \<Longrightarrow> a' = a
[PROOF STEP]
show "a' = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a' = a
[PROOF STEP]
proof (cases "a' \<in> A")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a' \<in> A \<Longrightarrow> a' = a
 2. a' \<notin> A \<Longrightarrow> a' = a
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
a' \<notin> A

goal (2 subgoals):
 1. a' \<in> A \<Longrightarrow> a' = a
 2. a' \<notin> A \<Longrightarrow> a' = a
[PROOF STEP]
with id
[PROOF STATE]
proof (chain)
picking this:
(if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
a' \<notin> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
a' \<notin> A

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

goal (1 subgoal):
 1. a' \<in> A \<Longrightarrow> a' = a
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a' \<in> A \<Longrightarrow> a' = a
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
a' \<in> A

goal (1 subgoal):
 1. a' \<in> A \<Longrightarrow> a' = a
[PROOF STEP]
note a' = memb[OF True]
[PROOF STATE]
proof (state)
this:
a' \<in> A
a_to_b a' \<in> B
inv q (a_to_b a') \<in> B
q (a_to_b a') \<in> B
b_to_a (q (a_to_b a')) \<in> A
b_to_a (inv q (a_to_b a')) \<in> A

goal (1 subgoal):
 1. a' \<in> A \<Longrightarrow> a' = a
[PROOF STEP]
with id False
[PROOF STATE]
proof (chain)
picking this:
(if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
a \<notin> A
a' \<in> A
a_to_b a' \<in> B
inv q (a_to_b a') \<in> B
q (a_to_b a') \<in> B
b_to_a (q (a_to_b a')) \<in> A
b_to_a (inv q (a_to_b a')) \<in> A
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a
a \<notin> A
a' \<in> A
a_to_b a' \<in> B
inv q (a_to_b a') \<in> B
q (a_to_b a') \<in> B
b_to_a (q (a_to_b a')) \<in> A
b_to_a (inv q (a_to_b a')) \<in> A

goal (1 subgoal):
 1. a' = a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a' = a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a' = a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>!a'. (if a' \<in> A then b_to_a (q (a_to_b a')) else a') = a

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
p \<in> {p. p permutes A}

goal:
No subgoals!
[PROOF STEP]
qed