[STATEMENT]
lemma weighted_RP_imp_RP: "St \<leadsto>\<^sub>w St' \<Longrightarrow> state_of_wstate St \<leadsto> state_of_wstate St'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. St \<leadsto>\<^sub>w St' \<Longrightarrow> state_of_wstate St \<leadsto> state_of_wstate St'
[PROOF STEP]
proof (induction rule: weighted_RP.induct)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<And>A C N i P Q n. \<lbrakk>Neg A \<in># C; Pos A \<in># C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P, Q, n)
 2. \<And>D P Q C N i n. \<lbrakk>D \<in># image_mset fst (P + Q); subsumes D C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P, Q, n)
 3. \<And>D N C P Q n. \<lbrakk>D \<in># image_mset fst N; C \<in># image_mset fst P; strictly_subsumes D C\<rbrakk> \<Longrightarrow> state_of_wstate (N, P, Q, n) \<leadsto> state_of_wstate (N, {#(E, k) \<in># P. E \<noteq> C#}, Q, n)
 4. \<And>D N C P Q i n. \<lbrakk>D \<in># image_mset fst N; strictly_subsumes D C\<rbrakk> \<Longrightarrow> state_of_wstate (N, P, Q + {#(C, i)#}, n) \<leadsto> state_of_wstate (N, P, Q, n)
 5. \<And>D L' P Q L \<sigma> C N i n. \<lbrakk>D + {#L'#} \<in># image_mset fst (P + Q); - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C + {#L#}, i)#}, P, Q, n) \<leadsto> state_of_wstate (N + {#(C, i)#}, P, Q, n)
 6. \<And>D L' N L \<sigma> C P i Q n. \<lbrakk>D + {#L'#} \<in># image_mset fst N; - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C; \<forall>j. (C + {#L#}, j) \<in># P \<longrightarrow> j \<le> i\<rbrakk> \<Longrightarrow> state_of_wstate (N, P + {#(C + {#L#}, i)#}, Q, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 7. \<And>D L' N L \<sigma> C P Q i n. \<lbrakk>D + {#L'#} \<in># image_mset fst N; - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C\<rbrakk> \<Longrightarrow> state_of_wstate (N, P, Q + {#(C + {#L#}, i)#}, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 8. \<And>N C i P Q n. state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 9. \<And>P C i N n Q. \<lbrakk>\<forall>(D, j)\<in>#P. weight (C, i) \<le> weight (D, j); N = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst Q)) C))\<rbrakk> \<Longrightarrow> state_of_wstate ({#}, P + {#(C, i)#}, Q, n) \<leadsto> state_of_wstate (N, {#(D, j) \<in># P. D \<noteq> C#}, Q + {#(C, i)#}, Suc n)
[PROOF STEP]
case (backward_subsumption_P D N C P Q n)
[PROOF STATE]
proof (state)
this:
D \<in># image_mset fst N
C \<in># image_mset fst P
strictly_subsumes D C

goal (9 subgoals):
 1. \<And>A C N i P Q n. \<lbrakk>Neg A \<in># C; Pos A \<in># C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P, Q, n)
 2. \<And>D P Q C N i n. \<lbrakk>D \<in># image_mset fst (P + Q); subsumes D C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P, Q, n)
 3. \<And>D N C P Q n. \<lbrakk>D \<in># image_mset fst N; C \<in># image_mset fst P; strictly_subsumes D C\<rbrakk> \<Longrightarrow> state_of_wstate (N, P, Q, n) \<leadsto> state_of_wstate (N, {#(E, k) \<in># P. E \<noteq> C#}, Q, n)
 4. \<And>D N C P Q i n. \<lbrakk>D \<in># image_mset fst N; strictly_subsumes D C\<rbrakk> \<Longrightarrow> state_of_wstate (N, P, Q + {#(C, i)#}, n) \<leadsto> state_of_wstate (N, P, Q, n)
 5. \<And>D L' P Q L \<sigma> C N i n. \<lbrakk>D + {#L'#} \<in># image_mset fst (P + Q); - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C + {#L#}, i)#}, P, Q, n) \<leadsto> state_of_wstate (N + {#(C, i)#}, P, Q, n)
 6. \<And>D L' N L \<sigma> C P i Q n. \<lbrakk>D + {#L'#} \<in># image_mset fst N; - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C; \<forall>j. (C + {#L#}, j) \<in># P \<longrightarrow> j \<le> i\<rbrakk> \<Longrightarrow> state_of_wstate (N, P + {#(C + {#L#}, i)#}, Q, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 7. \<And>D L' N L \<sigma> C P Q i n. \<lbrakk>D + {#L'#} \<in># image_mset fst N; - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C\<rbrakk> \<Longrightarrow> state_of_wstate (N, P, Q + {#(C + {#L#}, i)#}, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 8. \<And>N C i P Q n. state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 9. \<And>P C i N n Q. \<lbrakk>\<forall>(D, j)\<in>#P. weight (C, i) \<le> weight (D, j); N = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst Q)) C))\<rbrakk> \<Longrightarrow> state_of_wstate ({#}, P + {#(C, i)#}, Q, n) \<leadsto> state_of_wstate (N, {#(D, j) \<in># P. D \<noteq> C#}, Q + {#(C, i)#}, Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_of_wstate (N, P, Q, n) \<leadsto> state_of_wstate (N, {#(E, k) \<in># P. E \<noteq> C#}, Q, n)
[PROOF STEP]
by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>)", OF _ _
          RP.backward_subsumption_P[of D "fst ` set_mset N" C "fst ` set_mset P - {C}"
            "fst ` set_mset Q"]])
      (use backward_subsumption_P in auto)
[PROOF STATE]
proof (state)
this:
state_of_wstate (N, P, Q, n) \<leadsto> state_of_wstate (N, {#(E, k) \<in># P. E \<noteq> C#}, Q, n)

goal (8 subgoals):
 1. \<And>A C N i P Q n. \<lbrakk>Neg A \<in># C; Pos A \<in># C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P, Q, n)
 2. \<And>D P Q C N i n. \<lbrakk>D \<in># image_mset fst (P + Q); subsumes D C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P, Q, n)
 3. \<And>D N C P Q i n. \<lbrakk>D \<in># image_mset fst N; strictly_subsumes D C\<rbrakk> \<Longrightarrow> state_of_wstate (N, P, Q + {#(C, i)#}, n) \<leadsto> state_of_wstate (N, P, Q, n)
 4. \<And>D L' P Q L \<sigma> C N i n. \<lbrakk>D + {#L'#} \<in># image_mset fst (P + Q); - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C + {#L#}, i)#}, P, Q, n) \<leadsto> state_of_wstate (N + {#(C, i)#}, P, Q, n)
 5. \<And>D L' N L \<sigma> C P i Q n. \<lbrakk>D + {#L'#} \<in># image_mset fst N; - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C; \<forall>j. (C + {#L#}, j) \<in># P \<longrightarrow> j \<le> i\<rbrakk> \<Longrightarrow> state_of_wstate (N, P + {#(C + {#L#}, i)#}, Q, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 6. \<And>D L' N L \<sigma> C P Q i n. \<lbrakk>D + {#L'#} \<in># image_mset fst N; - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C\<rbrakk> \<Longrightarrow> state_of_wstate (N, P, Q + {#(C + {#L#}, i)#}, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 7. \<And>N C i P Q n. state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 8. \<And>P C i N n Q. \<lbrakk>\<forall>(D, j)\<in>#P. weight (C, i) \<le> weight (D, j); N = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst Q)) C))\<rbrakk> \<Longrightarrow> state_of_wstate ({#}, P + {#(C, i)#}, Q, n) \<leadsto> state_of_wstate (N, {#(D, j) \<in># P. D \<noteq> C#}, Q + {#(C, i)#}, Suc n)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. \<And>A C N i P Q n. \<lbrakk>Neg A \<in># C; Pos A \<in># C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P, Q, n)
 2. \<And>D P Q C N i n. \<lbrakk>D \<in># image_mset fst (P + Q); subsumes D C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P, Q, n)
 3. \<And>D N C P Q i n. \<lbrakk>D \<in># image_mset fst N; strictly_subsumes D C\<rbrakk> \<Longrightarrow> state_of_wstate (N, P, Q + {#(C, i)#}, n) \<leadsto> state_of_wstate (N, P, Q, n)
 4. \<And>D L' P Q L \<sigma> C N i n. \<lbrakk>D + {#L'#} \<in># image_mset fst (P + Q); - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C + {#L#}, i)#}, P, Q, n) \<leadsto> state_of_wstate (N + {#(C, i)#}, P, Q, n)
 5. \<And>D L' N L \<sigma> C P i Q n. \<lbrakk>D + {#L'#} \<in># image_mset fst N; - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C; \<forall>j. (C + {#L#}, j) \<in># P \<longrightarrow> j \<le> i\<rbrakk> \<Longrightarrow> state_of_wstate (N, P + {#(C + {#L#}, i)#}, Q, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 6. \<And>D L' N L \<sigma> C P Q i n. \<lbrakk>D + {#L'#} \<in># image_mset fst N; - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C\<rbrakk> \<Longrightarrow> state_of_wstate (N, P, Q + {#(C + {#L#}, i)#}, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 7. \<And>N C i P Q n. state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 8. \<And>P C i N n Q. \<lbrakk>\<forall>(D, j)\<in>#P. weight (C, i) \<le> weight (D, j); N = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst Q)) C))\<rbrakk> \<Longrightarrow> state_of_wstate ({#}, P + {#(C, i)#}, Q, n) \<leadsto> state_of_wstate (N, {#(D, j) \<in># P. D \<noteq> C#}, Q + {#(C, i)#}, Suc n)
[PROOF STEP]
case (inference_computation P C i N n Q)
[PROOF STATE]
proof (state)
this:
\<forall>(D, j)\<in>#P. weight (C, i) \<le> weight (D, j)
N = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst Q)) C))

goal (8 subgoals):
 1. \<And>A C N i P Q n. \<lbrakk>Neg A \<in># C; Pos A \<in># C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P, Q, n)
 2. \<And>D P Q C N i n. \<lbrakk>D \<in># image_mset fst (P + Q); subsumes D C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P, Q, n)
 3. \<And>D N C P Q i n. \<lbrakk>D \<in># image_mset fst N; strictly_subsumes D C\<rbrakk> \<Longrightarrow> state_of_wstate (N, P, Q + {#(C, i)#}, n) \<leadsto> state_of_wstate (N, P, Q, n)
 4. \<And>D L' P Q L \<sigma> C N i n. \<lbrakk>D + {#L'#} \<in># image_mset fst (P + Q); - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C + {#L#}, i)#}, P, Q, n) \<leadsto> state_of_wstate (N + {#(C, i)#}, P, Q, n)
 5. \<And>D L' N L \<sigma> C P i Q n. \<lbrakk>D + {#L'#} \<in># image_mset fst N; - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C; \<forall>j. (C + {#L#}, j) \<in># P \<longrightarrow> j \<le> i\<rbrakk> \<Longrightarrow> state_of_wstate (N, P + {#(C + {#L#}, i)#}, Q, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 6. \<And>D L' N L \<sigma> C P Q i n. \<lbrakk>D + {#L'#} \<in># image_mset fst N; - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C\<rbrakk> \<Longrightarrow> state_of_wstate (N, P, Q + {#(C + {#L#}, i)#}, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 7. \<And>N C i P Q n. state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 8. \<And>P C i N n Q. \<lbrakk>\<forall>(D, j)\<in>#P. weight (C, i) \<le> weight (D, j); N = mset_set ((\<lambda>D. (D, n)) ` concls_of (inference_system.inferences_between (ord_FO_\<Gamma> S) (set_mset (image_mset fst Q)) C))\<rbrakk> \<Longrightarrow> state_of_wstate ({#}, P + {#(C, i)#}, Q, n) \<leadsto> state_of_wstate (N, {#(D, j) \<in># P. D \<noteq> C#}, Q + {#(C, i)#}, Suc n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. state_of_wstate ({#}, P + {#(C, i)#}, Q, n) \<leadsto> state_of_wstate (N, {#(D, j) \<in># P. D \<noteq> C#}, Q + {#(C, i)#}, Suc n)
[PROOF STEP]
by (rule arg_cong2[THEN iffD1, of _ _ _ _ "(\<leadsto>)", OF _ _
           RP.inference_computation[of "fst ` set_mset N" "fst ` set_mset Q" C
             "fst ` set_mset P - {C}"]],
         use inference_computation(2) finite_ord_FO_resolution_inferences_between in
           \<open>auto simp: comp_def image_comp inference_system.inferences_between_def\<close>)
[PROOF STATE]
proof (state)
this:
state_of_wstate ({#}, P + {#(C, i)#}, Q, n) \<leadsto> state_of_wstate (N, {#(D, j) \<in># P. D \<noteq> C#}, Q + {#(C, i)#}, Suc n)

goal (7 subgoals):
 1. \<And>A C N i P Q n. \<lbrakk>Neg A \<in># C; Pos A \<in># C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P, Q, n)
 2. \<And>D P Q C N i n. \<lbrakk>D \<in># image_mset fst (P + Q); subsumes D C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P, Q, n)
 3. \<And>D N C P Q i n. \<lbrakk>D \<in># image_mset fst N; strictly_subsumes D C\<rbrakk> \<Longrightarrow> state_of_wstate (N, P, Q + {#(C, i)#}, n) \<leadsto> state_of_wstate (N, P, Q, n)
 4. \<And>D L' P Q L \<sigma> C N i n. \<lbrakk>D + {#L'#} \<in># image_mset fst (P + Q); - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C\<rbrakk> \<Longrightarrow> state_of_wstate (N + {#(C + {#L#}, i)#}, P, Q, n) \<leadsto> state_of_wstate (N + {#(C, i)#}, P, Q, n)
 5. \<And>D L' N L \<sigma> C P i Q n. \<lbrakk>D + {#L'#} \<in># image_mset fst N; - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C; \<forall>j. (C + {#L#}, j) \<in># P \<longrightarrow> j \<le> i\<rbrakk> \<Longrightarrow> state_of_wstate (N, P + {#(C + {#L#}, i)#}, Q, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 6. \<And>D L' N L \<sigma> C P Q i n. \<lbrakk>D + {#L'#} \<in># image_mset fst N; - L = L' \<cdot>l \<sigma>; D \<cdot> \<sigma> \<subseteq># C\<rbrakk> \<Longrightarrow> state_of_wstate (N, P, Q + {#(C + {#L#}, i)#}, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
 7. \<And>N C i P Q n. state_of_wstate (N + {#(C, i)#}, P, Q, n) \<leadsto> state_of_wstate (N, P + {#(C, i)#}, Q, n)
[PROOF STEP]
qed (use RP.intros in simp_all)


[STATEMENT]
lemma set_diff_list: "set (xs -- ys) = set xs - set ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (xs -- ys) = set xs - set ys
[PROOF STEP]
by (simp only: diff_list_def, induct ys arbitrary: xs, auto)


[STATEMENT]
lemma subset_append_diff_cancel:
  assumes "set ys \<subseteq> set xs"
  shows "set (ys @ (xs -- ys)) = set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (ys @ xs -- ys) = set xs
[PROOF STEP]
by (simp only: set_append set_diff_list Un_Diff_cancel, rule Un_absorb1, fact)


[STATEMENT]
lemma regular_closed_inf:
  "regular x \<Longrightarrow> regular y \<Longrightarrow> regular (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>regular x; regular y\<rbrakk> \<Longrightarrow> regular (x \<sqinter> y)
[PROOF STEP]
by (metis p_dist_sup ppp)


[STATEMENT]
lemma red_indI1:
  assumes "f \<in> F" and "f \<noteq> 0" and "p \<noteq> 0" and adds: "lt f adds\<^sub>t lt p"
  shows "red F p (p - monom_mult (lc p / lc f) (lp p - lp f) f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. red F p (p - monom_mult (lc p / lc f) (lp p - lp f) f)
[PROOF STEP]
proof (intro red_setI[OF \<open>f \<in> F\<close>])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. red_single p (p - monom_mult (lc p / lc f) (lp p - lp f) f) f ?t
[PROOF STEP]
let ?s = "lp p - lp f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. red_single p (p - monom_mult (lc p / lc f) (lp p - lp f) f) f ?t
[PROOF STEP]
have c: "lookup p (?s \<oplus> lt f) = lc p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup p ((lp p - lp f) \<oplus> lt f) = lc p
[PROOF STEP]
unfolding lc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup p ((lp p - lp f) \<oplus> lt f) = lookup p (lt p)
[PROOF STEP]
by (metis add_diff_cancel_right' adds adds_termE pp_of_term_splus)
[PROOF STATE]
proof (state)
this:
lookup p ((lp p - lp f) \<oplus> lt f) = lc p

goal (1 subgoal):
 1. red_single p (p - monom_mult (lc p / lc f) (lp p - lp f) f) f ?t
[PROOF STEP]
show "red_single p (p - monom_mult (lc p / lc f) ?s f) f ?s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. red_single p (p - monom_mult (lc p / lc f) (lp p - lp f) f) f (lp p - lp f)
[PROOF STEP]
unfolding red_single_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<noteq> 0 \<and> lookup p ((lp p - lp f) \<oplus> lt f) \<noteq> (0::'b) \<and> p - monom_mult (lc p / lc f) (lp p - lp f) f = p - monom_mult (lookup p ((lp p - lp f) \<oplus> lt f) / lc f) (lp p - lp f) f
[PROOF STEP]
proof (intro conjI, fact)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. lookup p ((lp p - lp f) \<oplus> lt f) \<noteq> (0::'b)
 2. p - monom_mult (lc p / lc f) (lp p - lp f) f = p - monom_mult (lookup p ((lp p - lp f) \<oplus> lt f) / lc f) (lp p - lp f) f
[PROOF STEP]
from c lc_not_0[OF \<open>p \<noteq> 0\<close>]
[PROOF STATE]
proof (chain)
picking this:
lookup p ((lp p - lp f) \<oplus> lt f) = lc p
lc p \<noteq> (0::'b)
[PROOF STEP]
show "lookup p (?s \<oplus> lt f) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
lookup p ((lp p - lp f) \<oplus> lt f) = lc p
lc p \<noteq> (0::'b)

goal (1 subgoal):
 1. lookup p ((lp p - lp f) \<oplus> lt f) \<noteq> (0::'b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
lookup p ((lp p - lp f) \<oplus> lt f) \<noteq> (0::'b)

goal (1 subgoal):
 1. p - monom_mult (lc p / lc f) (lp p - lp f) f = p - monom_mult (lookup p ((lp p - lp f) \<oplus> lt f) / lc f) (lp p - lp f) f
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p - monom_mult (lc p / lc f) (lp p - lp f) f = p - monom_mult (lookup p ((lp p - lp f) \<oplus> lt f) / lc f) (lp p - lp f) f
[PROOF STEP]
from c
[PROOF STATE]
proof (chain)
picking this:
lookup p ((lp p - lp f) \<oplus> lt f) = lc p
[PROOF STEP]
show "p - monom_mult (lc p / lc f) ?s f = p - monom_mult (lookup p (?s \<oplus> lt f) / lc f) ?s f"
[PROOF STATE]
proof (prove)
using this:
lookup p ((lp p - lp f) \<oplus> lt f) = lc p

goal (1 subgoal):
 1. p - monom_mult (lc p / lc f) (lp p - lp f) f = p - monom_mult (lookup p ((lp p - lp f) \<oplus> lt f) / lc f) (lp p - lp f) f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p - monom_mult (lc p / lc f) (lp p - lp f) f = p - monom_mult (lookup p ((lp p - lp f) \<oplus> lt f) / lc f) (lp p - lp f) f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
red_single p (p - monom_mult (lc p / lc f) (lp p - lp f) f) f (lp p - lp f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in encoding_wrt_barbs) enc_respects_barbs_and_barb_set:
  shows "enc_respects_barbs = (\<forall>Barbs. enc_respects_barb_set Barbs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<forall>S x. (\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x) \<longrightarrow> (\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<and> (\<forall>S x. (\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x) \<longrightarrow> (\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x))) = (\<forall>Barbs. (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x))) \<and> (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ((\<forall>S x. (\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x) \<longrightarrow> (\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<and> (\<forall>S x. (\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x) \<longrightarrow> (\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x))) = (\<forall>Barbs. (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x))) \<and> (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x))))
[PROOF STEP]
have "(\<forall>Barbs. enc_respects_barb_set Barbs)
        = ((\<forall>Barbs. enc_preserves_barb_set Barbs)
            \<and> (\<forall>Barbs. enc_reflects_barb_set Barbs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>Barbs. (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x))) \<and> (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x)))) = ((\<forall>Barbs S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x))) \<and> (\<forall>Barbs S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>Barbs. (\<forall>S x. x \<in> Barbs \<and> S\<down><SWB>x \<longrightarrow> \<lbrakk>S\<rbrakk>\<down><TWB>x) \<and> (\<forall>S x. x \<in> Barbs \<and> \<lbrakk>S\<rbrakk>\<down><TWB>x \<longrightarrow> S\<down><SWB>x)) = ((\<forall>Barbs S x. x \<in> Barbs \<and> S\<down><SWB>x \<longrightarrow> \<lbrakk>S\<rbrakk>\<down><TWB>x) \<and> (\<forall>Barbs S x. x \<in> Barbs \<and> \<lbrakk>S\<rbrakk>\<down><TWB>x \<longrightarrow> S\<down><SWB>x))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
(\<forall>Barbs. (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x))) \<and> (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x)))) = ((\<forall>Barbs S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x))) \<and> (\<forall>Barbs S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x))))

goal (1 subgoal):
 1. ((\<forall>S x. (\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x) \<longrightarrow> (\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<and> (\<forall>S x. (\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x) \<longrightarrow> (\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x))) = (\<forall>Barbs. (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x))) \<and> (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<forall>Barbs. (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x))) \<and> (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x)))) = ((\<forall>Barbs S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x))) \<and> (\<forall>Barbs S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x))))

goal (1 subgoal):
 1. ((\<forall>S x. (\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x) \<longrightarrow> (\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<and> (\<forall>S x. (\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x) \<longrightarrow> (\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x))) = (\<forall>Barbs. (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x))) \<and> (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x))))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>Barbs. (\<forall>S x. x \<in> Barbs \<and> S\<down><SWB>x \<longrightarrow> \<lbrakk>S\<rbrakk>\<down><TWB>x) \<and> (\<forall>S x. x \<in> Barbs \<and> \<lbrakk>S\<rbrakk>\<down><TWB>x \<longrightarrow> S\<down><SWB>x)) = ((\<forall>Barbs S x. x \<in> Barbs \<and> S\<down><SWB>x \<longrightarrow> \<lbrakk>S\<rbrakk>\<down><TWB>x) \<and> (\<forall>Barbs S x. x \<in> Barbs \<and> \<lbrakk>S\<rbrakk>\<down><TWB>x \<longrightarrow> S\<down><SWB>x)) \<Longrightarrow> ((\<forall>S x. S\<down><SWB>x \<longrightarrow> \<lbrakk>S\<rbrakk>\<down><TWB>x) \<and> (\<forall>S x. \<lbrakk>S\<rbrakk>\<down><TWB>x \<longrightarrow> S\<down><SWB>x)) = ((\<forall>Barbs S x. x \<in> Barbs \<and> S\<down><SWB>x \<longrightarrow> \<lbrakk>S\<rbrakk>\<down><TWB>x) \<and> (\<forall>Barbs S x. x \<in> Barbs \<and> \<lbrakk>S\<rbrakk>\<down><TWB>x \<longrightarrow> S\<down><SWB>x))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
((\<forall>S x. (\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x) \<longrightarrow> (\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<and> (\<forall>S x. (\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x) \<longrightarrow> (\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x))) = (\<forall>Barbs. (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x))) \<and> (\<forall>S x. x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S TargetTerm (\<lbrakk>S\<rbrakk>) \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T TargetTerm (\<lbrakk>S\<rbrakk>) \<and> T\<down><TWB>x)) \<longrightarrow> x \<in> Barbs \<and> ((\<exists>Sa. Sa \<in>S SourceTerm S \<and> Sa\<down><SWB>x) \<or> (\<exists>T. T \<in>T SourceTerm S \<and> T\<down><TWB>x))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma node_ptr_casts_commute [simp]:
  "cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r ptr = Some node_ptr \<longleftrightarrow> cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r node_ptr = ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cast ptr = Some node_ptr) = (cast node_ptr = ptr)
[PROOF STEP]
unfolding cast\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def cast\<^sub>n\<^sub>o\<^sub>d\<^sub>e\<^sub>_\<^sub>p\<^sub>t\<^sub>r\<^sub>2\<^sub>o\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>_\<^sub>p\<^sub>t\<^sub>r_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((case ptr of object_ptr.Ext (Inl xa) \<Rightarrow> Some xa | object_ptr.Ext (Inr xa) \<Rightarrow> Map.empty xa) = Some node_ptr) = (object_ptr.Ext (Inl node_ptr) = ptr)
[PROOF STEP]
by(auto split: object_ptr.splits sum.splits)


[STATEMENT]
lemma Rf_mono_iia:
  shows "mono (Rf f) \<longleftrightarrow> iia f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (Rf f) = iia f
[PROOF STEP]
using %invisible Rf_mono_on_iia_on[of UNIV f] mono_on_mono
[PROOF STATE]
proof (prove)
using this:
Basis.mono_on (Pow UNIV) (Rf f) = iia f
Basis.mono_on UNIV = mono

goal (1 subgoal):
 1. mono (Rf f) = iia f
[PROOF STEP]
by (simp add: fun_eq_iff) blast


[STATEMENT]
lemma mono:
  assumes "x \<in> linear_cf X"
  shows "\<exists>y \<in> linear_cf (X \<union> Y). (x, y) \<in> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>y\<in>linear_cf (X \<union> Y). (x, y) \<in> r
[PROOF STEP]
using %invisible MaxR.mono assms
[PROOF STATE]
proof (prove)
using this:
local.MaxR.MaxR_opt ?A = Some ?x \<Longrightarrow> \<exists>y. local.MaxR.MaxR_opt (?A \<union> ?B) = Some y \<and> (?x, y) \<in> r
x \<in> linear_cf X

goal (1 subgoal):
 1. \<exists>y\<in>linear_cf (X \<union> Y). (x, y) \<in> r
[PROOF STEP]
unfolding linear_cf_def
[PROOF STATE]
proof (prove)
using this:
local.MaxR.MaxR_opt ?A = Some ?x \<Longrightarrow> \<exists>y. local.MaxR.MaxR_opt (?A \<union> ?B) = Some y \<and> (?x, y) \<in> r
x \<in> set_option (local.MaxR.MaxR_opt X)

goal (1 subgoal):
 1. \<exists>y\<in>set_option (local.MaxR.MaxR_opt (X \<union> Y)). (x, y) \<in> r
[PROOF STEP]
by (metis elem_set)


[STATEMENT]
lemma start_SuboSet:
"\<lbrakk>start_heap P a = Some(C, S); Subobjs P C Cs\<rbrakk> \<Longrightarrow> \<exists>fs. (Cs,fs) \<in> S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>start_heap P a = \<lfloor>(C, S)\<rfloor>; Subobjs P C Cs\<rbrakk> \<Longrightarrow> \<exists>fs. (Cs, fs) \<in> S
[PROOF STEP]
by (fastforce intro:init_obj.intros simp:start_heap_def blank_def
                split:if_split_asm)


[STATEMENT]
lemma D_diag_nonnegI:
  assumes "cycle_free M n" "i \<le> n"
  shows "D M i i n \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> D M i i n
[PROOF STEP]
using assms D_dest''[OF refl, of M i i n]
[PROOF STATE]
proof (prove)
using this:
cycle_free M n
i \<le> n
D M i i n \<in> {len M i i xs |xs. set xs \<subseteq> {0..n}}

goal (1 subgoal):
 1. (0::'a) \<le> D M i i n
[PROOF STEP]
unfolding cycle_free_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i xs. i \<le> n \<and> set xs \<subseteq> {0..n} \<longrightarrow> (\<forall>j\<le>n. len M i j (rem_cycles i j xs) \<le> len M i j xs) \<and> (0::'a) \<le> len M i i xs
i \<le> n
D M i i n \<in> {len M i i xs |xs. set xs \<subseteq> {0..n}}

goal (1 subgoal):
 1. (0::'a) \<le> D M i i n
[PROOF STEP]
by auto


[STATEMENT]
lemma post_dual_post_one:
  "q \<in> assumption \<Longrightarrow> post 1 * q \<le> post (q ^ o)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> assumption \<Longrightarrow> post (1::'a) * q \<le> post (q ^ o)
[PROOF STEP]
by (metis assumption_neg_assume post_sub_fusion)


[STATEMENT]
lemma sdp_Abort:
  "sub_distrib_pconj Abort"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_distrib_pconj Abort
[PROOF STEP]
by(rule sub_distrib_pconjI, unfold wp_eval, auto intro:exp_conj_rzero)


[STATEMENT]
lemma col_line_eq_1:
  assumes "A \<noteq> B" and "B \<noteq> C"and "col A B C"
  shows "line A B = line B C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. line A B = line B C
[PROOF STEP]
by (metis assms ax_uniqueness col_def incidA_lAB incidB_lAB)


[STATEMENT]
lemma conductor_principal [simp]: "\<chi> = principal_dchar n \<Longrightarrow> conductor = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<chi> = principal_dchar n \<Longrightarrow> conductor = 1
[PROOF STEP]
by (subst conductor_eq_1_iff_principal)


[STATEMENT]
lemma "eval 1000
            stmt
            (ASSIGN (Id (STR ''v1'')) (ECALL (ADDRESS (STR ''extaddr'')) (STR ''m1'') [E.INT 8 3, E.INT 8 4] (E.UINT 8 0)))
            (STR ''myaddr'')
            (STR '''')
            (STR ''0'')
            [(STR ''myaddr'', STR ''100'')]
            [
              (STR ''extaddr'',
                ([(STR ''m1'', Method ([(STR ''v2'', Value (TSInt 8)), (STR ''v3'', Value (TSInt 8))], SKIP, Some (PLUS (LVAL (Id (STR ''v2''))) (LVAL (Id (STR ''v3''))))))],
                SKIP))
            ]
            [(STR ''v1'', (Value (TSInt 8), Stackint 0))]
       = STR ''v1==7\<newline>myaddr.balance==100\<newline>''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eval 1000 stmt (ASSIGN (L.Id STR ''v1'') (ECALL (ADDRESS STR ''extaddr'') STR ''m1'' [INT 8 3, INT 8 4] (UINT 8 0))) STR ''myaddr'' STR '''' STR ''0'' [(STR ''myaddr'', STR ''100'')] [(STR ''extaddr'', [(STR ''m1'', Method ([(STR ''v2'', Value (TSInt 8)), (STR ''v3'', Value (TSInt 8))], SKIP, Some (PLUS (LVAL (L.Id STR ''v2'')) (LVAL (L.Id STR ''v3'')))))], SKIP)] [(STR ''v1'', Value (TSInt 8), Stackint 0)] = STR ''v1==7\<newline>myaddr.balance==100\<newline>''
[PROOF STEP]
by (eval)


[STATEMENT]
lemma resolution_class_size1:
  assumes "S \<in># \
"
  shows "\<v> = \<k> * size S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<v> = \<k> * size S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<v> = \<k> * size S
[PROOF STEP]
have "(\<Sum>bl \<in># S . card bl) = (\<Sum>bl \<in> (set_mset S) . card bl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum>\<^sub># (image_mset card S) = sum card (set_mset S)
[PROOF STEP]
using resolutionD2 assms
[PROOF STATE]
proof (prove)
using this:
?S \<in># \
 \<Longrightarrow> distinct_mset ?S
S \<in># \

goal (1 subgoal):
 1. \<Sum>\<^sub># (image_mset card S) = sum card (set_mset S)
[PROOF STEP]
by (simp add:  sum_unfold_sum_mset)
[PROOF STATE]
proof (state)
this:
\<Sum>\<^sub># (image_mset card S) = sum card (set_mset S)

goal (1 subgoal):
 1. \<v> = \<k> * size S
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Sum>\<^sub># (image_mset card S) = sum card (set_mset S)
[PROOF STEP]
have eqv: "(\<Sum>bl \<in># S . card bl) = \<v>"
[PROOF STATE]
proof (prove)
using this:
\<Sum>\<^sub># (image_mset card S) = sum card (set_mset S)

goal (1 subgoal):
 1. \<Sum>\<^sub># (image_mset card S) = \<v>
[PROOF STEP]
using resolutionD3 assms resolution_class_sum_card
[PROOF STATE]
proof (prove)
using this:
\<Sum>\<^sub># (image_mset card S) = sum card (set_mset S)
?S \<in># \
 \<Longrightarrow> resolution_class (set_mset ?S)
S \<in># \

resolution_class ?S \<Longrightarrow> sum card ?S = \<v>

goal (1 subgoal):
 1. \<Sum>\<^sub># (image_mset card S) = \<v>
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
\<Sum>\<^sub># (image_mset card S) = \<v>

goal (1 subgoal):
 1. \<v> = \<k> * size S
[PROOF STEP]
have "(\<Sum>bl \<in># S . card bl) = (\<Sum>bl \<in># S . \<k>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum>\<^sub># (image_mset card S) = (\<Sum>bl\<in>#S. \<k>)
[PROOF STEP]
using resolution_class_blocks_constant_size assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?S \<in># \
; ?bl \<in># ?S\<rbrakk> \<Longrightarrow> card ?bl = \<k>
S \<in># \

goal (1 subgoal):
 1. \<Sum>\<^sub># (image_mset card S) = (\<Sum>bl\<in>#S. \<k>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Sum>\<^sub># (image_mset card S) = (\<Sum>bl\<in>#S. \<k>)

goal (1 subgoal):
 1. \<v> = \<k> * size S
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Sum>\<^sub># (image_mset card S) = (\<Sum>bl\<in>#S. \<k>)

goal (1 subgoal):
 1. \<v> = \<k> * size S
[PROOF STEP]
using eqv
[PROOF STATE]
proof (prove)
using this:
\<Sum>\<^sub># (image_mset card S) = (\<Sum>bl\<in>#S. \<k>)
\<Sum>\<^sub># (image_mset card S) = \<v>

goal (1 subgoal):
 1. \<v> = \<k> * size S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<v> = \<k> * size S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma invalidate_kD_inv [simp]:
  "\<And>rt dests. kD (invalidate rt dests) = kD rt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt dests. kD (invalidate rt dests) = kD rt
[PROOF STEP]
unfolding invalidate_def kD_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>rt dests. {dip. (case (rt dip, dests dip) of (None, x) \<Rightarrow> None | (Some (a, ab, ad, af, ah, ba), None) \<Rightarrow> Some (a, ab, ad, af, ah, ba) | (Some (a, ab, ad, af, ah, ba), Some rsn) \<Rightarrow> Some (rsn, ab, Aodv_Basic.inv, af, ah, ba)) \<noteq> None} = {dip. rt dip \<noteq> None}
[PROOF STEP]
by (simp split: option.split)


[STATEMENT]
lemma is_class_Throwable:
  "wf_prog wf_md P \<Longrightarrow> is_class P Throwable"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_prog wf_md P \<Longrightarrow> is_class P Throwable
[PROOF STEP]
by(rule wf_prog_wf_syscls wf_syscls_is_class_Throwable)+


[STATEMENT]
lemma (in Semilat) le_iff_plus_unchanged2:
  assumes "x \<in> A" and "y \<in> A"
  shows "x \<sqsubseteq>\<^sub>r y \<longleftrightarrow> y \<squnion>\<^sub>f x = y" (is "?P \<longleftrightarrow> ?Q")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqsubseteq>\<^bsub>r\<^esub> y) = (y \<squnion>\<^bsub>f\<^esub> x = y)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqsubseteq>\<^bsub>r\<^esub> y) = (y \<squnion>\<^bsub>f\<^esub> x = y)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x \<sqsubseteq>\<^bsub>r\<^esub> y \<Longrightarrow> y \<squnion>\<^bsub>f\<^esub> x = y
 2. y \<squnion>\<^bsub>f\<^esub> x = y \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
assume ?P
[PROOF STATE]
proof (state)
this:
x \<sqsubseteq>\<^bsub>r\<^esub> y

goal (2 subgoals):
 1. x \<sqsubseteq>\<^bsub>r\<^esub> y \<Longrightarrow> y \<squnion>\<^bsub>f\<^esub> x = y
 2. y \<squnion>\<^bsub>f\<^esub> x = y \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
y \<in> A
x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
show ?Q
[PROOF STATE]
proof (prove)
using this:
x \<in> A
y \<in> A
x \<sqsubseteq>\<^bsub>r\<^esub> y

goal (1 subgoal):
 1. y \<squnion>\<^bsub>f\<^esub> x = y
[PROOF STEP]
by (blast intro: antisym_r lub ub1)
[PROOF STATE]
proof (state)
this:
y \<squnion>\<^bsub>f\<^esub> x = y

goal (1 subgoal):
 1. y \<squnion>\<^bsub>f\<^esub> x = y \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<squnion>\<^bsub>f\<^esub> x = y \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
assume ?Q
[PROOF STATE]
proof (state)
this:
y \<squnion>\<^bsub>f\<^esub> x = y

goal (1 subgoal):
 1. y \<squnion>\<^bsub>f\<^esub> x = y \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<squnion>\<^bsub>f\<^esub> x = y
[PROOF STEP]
have "y = y \<squnion>\<^bsub>f\<^esub> x"
[PROOF STATE]
proof (prove)
using this:
y \<squnion>\<^bsub>f\<^esub> x = y

goal (1 subgoal):
 1. y = y \<squnion>\<^bsub>f\<^esub> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y = y \<squnion>\<^bsub>f\<^esub> x

goal (1 subgoal):
 1. y \<squnion>\<^bsub>f\<^esub> x = y \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y = y \<squnion>\<^bsub>f\<^esub> x

goal (1 subgoal):
 1. y \<squnion>\<^bsub>f\<^esub> x = y \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<in> A
y \<in> A
[PROOF STEP]
have "x \<sqsubseteq>\<^bsub>r\<^esub> y \<squnion>\<^bsub>f\<^esub> x"
[PROOF STATE]
proof (prove)
using this:
x \<in> A
y \<in> A

goal (1 subgoal):
 1. x \<sqsubseteq>\<^bsub>r\<^esub> y \<squnion>\<^bsub>f\<^esub> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<sqsubseteq>\<^bsub>r\<^esub> y \<squnion>\<^bsub>f\<^esub> x

goal (1 subgoal):
 1. y \<squnion>\<^bsub>f\<^esub> x = y \<Longrightarrow> x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y = y \<squnion>\<^bsub>f\<^esub> x
x \<sqsubseteq>\<^bsub>r\<^esub> y \<squnion>\<^bsub>f\<^esub> x
[PROOF STEP]
show ?P
[PROOF STATE]
proof (prove)
using this:
y = y \<squnion>\<^bsub>f\<^esub> x
x \<sqsubseteq>\<^bsub>r\<^esub> y \<squnion>\<^bsub>f\<^esub> x

goal (1 subgoal):
 1. x \<sqsubseteq>\<^bsub>r\<^esub> y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<sqsubseteq>\<^bsub>r\<^esub> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma L_eqvt_aux [simp]: "p \<bullet> L = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> L = L
[PROOF STEP]
by (metis L_eqvt eqvt_def)


[STATEMENT]
lemma FL_bisimilar_simulation_step:
    assumes "P \<sim>\<cdot>[F] Q" and "f \<in>\<^sub>f\<^sub>s F" and "bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f)" and "\<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>"
    obtains Q' where "\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>" and "P' \<sim>\<cdot>[L (\<alpha>,F,f)] Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>; P' \<sim>\<cdot>[L (\<alpha>, F, f)] Q'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<sim>\<cdot>[F] Q
f \<in>\<^sub>f\<^sub>s F
bn \<alpha> \<sharp>* (\<langle>f\<rangle>Q, F, f)
\<langle>f\<rangle>P \<rightarrow> \<langle>\<alpha>,P'\<rangle>

goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>\<langle>f\<rangle>Q \<rightarrow> \<langle>\<alpha>,Q'\<rangle>; P' \<sim>\<cdot>[L (\<alpha>, F, f)] Q'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis (poly_guards_query) FL_bisimilar_is_L_bisimulation is_L_bisimulation_def)


[STATEMENT]
lemma abs_update_length: "length (abs_update k v l) = length l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (abs_update k v l) = length l
[PROOF STEP]
by (simp add: abs_update_def)


[STATEMENT]
lemma abs_update_rehash_map_of:
  assumes "ht_hash l"
  assumes "ht_distinct l"
  assumes "1 < length l"
  shows "map_of (concat (abs_update k v (ls_rehash l)))
  = map_of (concat l)(k \<mapsto> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_of (concat (abs_update k v (ls_rehash l))) = map_of (concat l)(k \<mapsto> v)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map_of (concat (abs_update k v (ls_rehash l))) = map_of (concat l)(k \<mapsto> v)
[PROOF STEP]
note a = ht_hash_ls_rehash[of l]
[PROOF STATE]
proof (state)
this:
ht_hash (ls_rehash l)

goal (1 subgoal):
 1. map_of (concat (abs_update k v (ls_rehash l))) = map_of (concat l)(k \<mapsto> v)
[PROOF STEP]
note b = ht_distinct_ls_rehash[of l]
[PROOF STATE]
proof (state)
this:
ht_distinct (ls_rehash l)

goal (1 subgoal):
 1. map_of (concat (abs_update k v (ls_rehash l))) = map_of (concat l)(k \<mapsto> v)
[PROOF STEP]
note c = length_ls_rehash[OF assms(3)]
[PROOF STATE]
proof (state)
this:
1 < length (ls_rehash l)

goal (1 subgoal):
 1. map_of (concat (abs_update k v (ls_rehash l))) = map_of (concat l)(k \<mapsto> v)
[PROOF STEP]
from abs_update_map_of[OF a b c] ls_rehash_map_of[OF assms]
[PROOF STATE]
proof (chain)
picking this:
map_of (concat (abs_update ?k ?v (ls_rehash l))) = map_of (concat (ls_rehash l))(?k \<mapsto> ?v)
map_of (concat (ls_rehash l)) = map_of (concat l)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
map_of (concat (abs_update ?k ?v (ls_rehash l))) = map_of (concat (ls_rehash l))(?k \<mapsto> ?v)
map_of (concat (ls_rehash l)) = map_of (concat l)

goal (1 subgoal):
 1. map_of (concat (abs_update k v (ls_rehash l))) = map_of (concat l)(k \<mapsto> v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map_of (concat (abs_update k v (ls_rehash l))) = map_of (concat l)(k \<mapsto> v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma concat_take_Suc_empty: "\<lbrakk> n < length l; l!n=[] \<rbrakk>
  \<Longrightarrow> concat (take (Suc n) l) = concat (take n l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length l; l ! n = []\<rbrakk> \<Longrightarrow> concat (take (Suc n) l) = concat (take n l)
[PROOF STEP]
apply (induct n arbitrary: l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>l. \<lbrakk>0 < length l; l ! 0 = []\<rbrakk> \<Longrightarrow> concat (take (Suc 0) l) = concat (take 0 l)
 2. \<And>n l. \<lbrakk>\<And>l. \<lbrakk>n < length l; l ! n = []\<rbrakk> \<Longrightarrow> concat (take (Suc n) l) = concat (take n l); Suc n < length l; l ! Suc n = []\<rbrakk> \<Longrightarrow> concat (take (Suc (Suc n)) l) = concat (take (Suc n) l)
[PROOF STEP]
apply (case_tac l)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>l. \<lbrakk>0 < length l; l ! 0 = []; l = []\<rbrakk> \<Longrightarrow> concat (take (Suc 0) l) = concat (take 0 l)
 2. \<And>l a list. \<lbrakk>0 < length l; l ! 0 = []; l = a # list\<rbrakk> \<Longrightarrow> concat (take (Suc 0) l) = concat (take 0 l)
 3. \<And>n l. \<lbrakk>\<And>l. \<lbrakk>n < length l; l ! n = []\<rbrakk> \<Longrightarrow> concat (take (Suc n) l) = concat (take n l); Suc n < length l; l ! Suc n = []\<rbrakk> \<Longrightarrow> concat (take (Suc (Suc n)) l) = concat (take (Suc n) l)
[PROOF STEP]
apply auto [2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n l. \<lbrakk>\<And>l. \<lbrakk>n < length l; l ! n = []\<rbrakk> \<Longrightarrow> concat (take (Suc n) l) = concat (take n l); Suc n < length l; l ! Suc n = []\<rbrakk> \<Longrightarrow> concat (take (Suc (Suc n)) l) = concat (take (Suc n) l)
[PROOF STEP]
apply (case_tac l)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n l. \<lbrakk>\<And>l. \<lbrakk>n < length l; l ! n = []\<rbrakk> \<Longrightarrow> concat (take (Suc n) l) = concat (take n l); Suc n < length l; l ! Suc n = []; l = []\<rbrakk> \<Longrightarrow> concat (take (Suc (Suc n)) l) = concat (take (Suc n) l)
 2. \<And>n l a list. \<lbrakk>\<And>l. \<lbrakk>n < length l; l ! n = []\<rbrakk> \<Longrightarrow> concat (take (Suc n) l) = concat (take n l); Suc n < length l; l ! Suc n = []; l = a # list\<rbrakk> \<Longrightarrow> concat (take (Suc (Suc n)) l) = concat (take (Suc n) l)
[PROOF STEP]
apply auto [2]
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma to_nat_from_nat:
  assumes t:"to_nat j = k"
  shows "from_nat k = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat k = j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mod_type_class.from_nat k = j
[PROOF STEP]
have "from_nat k = from_nat (to_nat j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat k = mod_type_class.from_nat (mod_type_class.to_nat j)
[PROOF STEP]
unfolding t
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat k = mod_type_class.from_nat k
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat k = mod_type_class.from_nat (mod_type_class.to_nat j)

goal (1 subgoal):
 1. mod_type_class.from_nat k = j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat k = mod_type_class.from_nat (mod_type_class.to_nat j)

goal (1 subgoal):
 1. mod_type_class.from_nat k = j
[PROOF STEP]
have "... = from_nat (the_inv_into {0..<CARD('a)} (from_nat) j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat (mod_type_class.to_nat j) = mod_type_class.from_nat (the_inv_into {0..<CARD('a)} mod_type_class.from_nat j)
[PROOF STEP]
unfolding to_nat_is_inv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat (mod_type_class.to_nat j) = mod_type_class.from_nat (mod_type_class.to_nat j)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat (mod_type_class.to_nat j) = mod_type_class.from_nat (the_inv_into {0..<CARD('a)} mod_type_class.from_nat j)

goal (1 subgoal):
 1. mod_type_class.from_nat k = j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat (mod_type_class.to_nat j) = mod_type_class.from_nat (the_inv_into {0..<CARD('a)} mod_type_class.from_nat j)

goal (1 subgoal):
 1. mod_type_class.from_nat k = j
[PROOF STEP]
have "... = j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat (the_inv_into {0..<CARD('a)} mod_type_class.from_nat j) = j
[PROOF STEP]
proof (rule f_the_inv_into_f)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on mod_type_class.from_nat {0..<CARD('a)}
 2. j \<in> mod_type_class.from_nat ` {0..<CARD('a)}
[PROOF STEP]
show "inj_on from_nat {0..<CARD('a)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on mod_type_class.from_nat {0..<CARD('a)}
[PROOF STEP]
by (metis bij_betw_imp_inj_on bij_from_nat)
[PROOF STATE]
proof (state)
this:
inj_on mod_type_class.from_nat {0..<CARD('a)}

goal (1 subgoal):
 1. j \<in> mod_type_class.from_nat ` {0..<CARD('a)}
[PROOF STEP]
show "j \<in> from_nat ` {0..<CARD('a)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<in> mod_type_class.from_nat ` {0..<CARD('a)}
[PROOF STEP]
by (metis UNIV_I bij_betw_def bij_from_nat)
[PROOF STATE]
proof (state)
this:
j \<in> mod_type_class.from_nat ` {0..<CARD('a)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat (the_inv_into {0..<CARD('a)} mod_type_class.from_nat j) = j

goal (1 subgoal):
 1. mod_type_class.from_nat k = j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
mod_type_class.from_nat k = j
[PROOF STEP]
show "from_nat k = j"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.from_nat k = j

goal (1 subgoal):
 1. mod_type_class.from_nat k = j
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat k = j

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma op_lso_bex_monadify[sepref_monadify_comb]:
    "EVAL$(op_lso_bex$(\<lambda>\<^sub>2x. P x)$s) \<equiv> (\<bind>) $(EVAL$s)$(\<lambda>\<^sub>2s. mop_lso_bex$(\<lambda>\<^sub>2x. EVAL $ P x)$s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. EVAL $ (op_lso_bex $ (\<lambda>x. (#P x#)) $ s) \<equiv> (\<bind>) $ (EVAL $ s) $ (\<lambda>x. (#mop_lso_bex $ (\<lambda>x. (#EVAL $ P x#)) $ x#))
[PROOF STEP]
by simp


[STATEMENT]
lemma vifintersection_vrange_VLambda: "(\<Inter>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. f i) = \<Inter>\<^sub>\<circ> (\<R>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>I. f a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Inter>\<^sub>\<circ> (VLambda I f `\<^sub>\<circ> I) = \<Inter>\<^sub>\<circ> (\<R>\<^sub>\<circ> (VLambda I f))
[PROOF STEP]
by (simp add: vimage_VLambda_vrange_rep)


[STATEMENT]
lemma offset_not_none_1 [rule_format]:
 "offset k x xs \<noteq> None \<longrightarrow> (\<exists>ys zs. xs = ys @ x # zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offset k x xs \<noteq> None \<longrightarrow> (\<exists>ys zs. xs = ys @ x # zs)
[PROOF STEP]
proof (induction xs arbitrary: k, simp, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs k. \<lbrakk>\<And>k. offset k x xs \<noteq> None \<longrightarrow> (\<exists>ys zs. xs = ys @ x # zs); offset k x (a # xs) \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>ys zs. a # xs = ys @ x # zs
[PROOF STEP]
fix w xs k
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs k. \<lbrakk>\<And>k. offset k x xs \<noteq> None \<longrightarrow> (\<exists>ys zs. xs = ys @ x # zs); offset k x (a # xs) \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>ys zs. a # xs = ys @ x # zs
[PROOF STEP]
assume
    A: "\<And>k. offset k x xs \<noteq> None \<longrightarrow> (\<exists>ys zs. xs = ys @ x # zs)" and
    B: "offset k x (w # xs) \<noteq> None"
[PROOF STATE]
proof (state)
this:
offset ?k x xs \<noteq> None \<longrightarrow> (\<exists>ys zs. xs = ys @ x # zs)
offset k x (w # xs) \<noteq> None

goal (1 subgoal):
 1. \<And>a xs k. \<lbrakk>\<And>k. offset k x xs \<noteq> None \<longrightarrow> (\<exists>ys zs. xs = ys @ x # zs); offset k x (a # xs) \<noteq> None\<rbrakk> \<Longrightarrow> \<exists>ys zs. a # xs = ys @ x # zs
[PROOF STEP]
show "\<exists>ys zs. w # xs = ys @ x # zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
proof (cases "w = x", simp)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. w = x \<Longrightarrow> \<exists>ys zs. x # xs = ys @ x # zs
 2. w \<noteq> x \<Longrightarrow> \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
w = x

goal (2 subgoals):
 1. w = x \<Longrightarrow> \<exists>ys zs. x # xs = ys @ x # zs
 2. w \<noteq> x \<Longrightarrow> \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
hence "x # xs = [] @ x # xs"
[PROOF STATE]
proof (prove)
using this:
w = x

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

goal (2 subgoals):
 1. w = x \<Longrightarrow> \<exists>ys zs. x # xs = ys @ x # zs
 2. w \<noteq> x \<Longrightarrow> \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
thus "\<exists>ys zs. x # xs = ys @ x # zs"
[PROOF STATE]
proof (prove)
using this:
x # xs = [] @ x # xs

goal (1 subgoal):
 1. \<exists>ys zs. x # xs = ys @ x # zs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>ys zs. x # xs = ys @ x # zs

goal (1 subgoal):
 1. w \<noteq> x \<Longrightarrow> \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. w \<noteq> x \<Longrightarrow> \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
w \<noteq> x

goal (1 subgoal):
 1. w \<noteq> x \<Longrightarrow> \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
hence "offset k x (w # xs) = offset (Suc k) x xs"
[PROOF STATE]
proof (prove)
using this:
w \<noteq> x

goal (1 subgoal):
 1. offset k x (w # xs) = offset (Suc k) x xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
offset k x (w # xs) = offset (Suc k) x xs

goal (1 subgoal):
 1. w \<noteq> x \<Longrightarrow> \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
hence "offset (Suc k) x xs \<noteq> None"
[PROOF STATE]
proof (prove)
using this:
offset k x (w # xs) = offset (Suc k) x xs

goal (1 subgoal):
 1. offset (Suc k) x xs \<noteq> None
[PROOF STEP]
using B
[PROOF STATE]
proof (prove)
using this:
offset k x (w # xs) = offset (Suc k) x xs
offset k x (w # xs) \<noteq> None

goal (1 subgoal):
 1. offset (Suc k) x xs \<noteq> None
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
offset (Suc k) x xs \<noteq> None

goal (1 subgoal):
 1. w \<noteq> x \<Longrightarrow> \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
offset (Suc k) x xs \<noteq> None

goal (1 subgoal):
 1. w \<noteq> x \<Longrightarrow> \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
have "offset (Suc k) x xs \<noteq> None \<longrightarrow> (\<exists>ys zs. xs = ys @ x # zs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. offset (Suc k) x xs \<noteq> None \<longrightarrow> (\<exists>ys zs. xs = ys @ x # zs)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
offset ?k x xs \<noteq> None \<longrightarrow> (\<exists>ys zs. xs = ys @ x # zs)

goal (1 subgoal):
 1. offset (Suc k) x xs \<noteq> None \<longrightarrow> (\<exists>ys zs. xs = ys @ x # zs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
offset (Suc k) x xs \<noteq> None \<longrightarrow> (\<exists>ys zs. xs = ys @ x # zs)

goal (1 subgoal):
 1. w \<noteq> x \<Longrightarrow> \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
offset (Suc k) x xs \<noteq> None
offset (Suc k) x xs \<noteq> None \<longrightarrow> (\<exists>ys zs. xs = ys @ x # zs)
[PROOF STEP]
have "\<exists>ys zs. xs = ys @ x # zs"
[PROOF STATE]
proof (prove)
using this:
offset (Suc k) x xs \<noteq> None
offset (Suc k) x xs \<noteq> None \<longrightarrow> (\<exists>ys zs. xs = ys @ x # zs)

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

goal (1 subgoal):
 1. w \<noteq> x \<Longrightarrow> \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>ys zs. xs = ys @ x # zs
[PROOF STEP]
obtain ys and zs where "xs = ys @ x # zs"
[PROOF STATE]
proof (prove)
using this:
\<exists>ys zs. xs = ys @ x # zs

goal (1 subgoal):
 1. (\<And>ys zs. xs = ys @ x # zs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
xs = ys @ x # zs

goal (1 subgoal):
 1. w \<noteq> x \<Longrightarrow> \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
hence "w # xs = (w # ys) @ x # zs"
[PROOF STATE]
proof (prove)
using this:
xs = ys @ x # zs

goal (1 subgoal):
 1. w # xs = (w # ys) @ x # zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w # xs = (w # ys) @ x # zs

goal (1 subgoal):
 1. w \<noteq> x \<Longrightarrow> \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
thus "\<exists>ys zs. w # xs = ys @ x # zs"
[PROOF STATE]
proof (prove)
using this:
w # xs = (w # ys) @ x # zs

goal (1 subgoal):
 1. \<exists>ys zs. w # xs = ys @ x # zs
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>ys zs. w # xs = ys @ x # zs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>ys zs. w # xs = ys @ x # zs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma oalist_inv_raw_filter:
  assumes "oalist_inv_raw xs"
  shows "oalist_inv_raw (filter P xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oalist_inv_raw (filter P xs)
[PROOF STEP]
proof (rule oalist_inv_rawI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (0::'b) \<notin> snd ` set (filter P xs)
 2. sorted_wrt lt (map fst (filter P xs))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
oalist_inv_raw xs
[PROOF STEP]
have "0 \<notin> snd ` set xs"
[PROOF STATE]
proof (prove)
using this:
oalist_inv_raw xs

goal (1 subgoal):
 1. (0::'b) \<notin> snd ` set xs
[PROOF STEP]
by (rule oalist_inv_rawD1)
[PROOF STATE]
proof (state)
this:
(0::'b) \<notin> snd ` set xs

goal (2 subgoals):
 1. (0::'b) \<notin> snd ` set (filter P xs)
 2. sorted_wrt lt (map fst (filter P xs))
[PROOF STEP]
thus "0 \<notin> snd ` set (filter P xs)"
[PROOF STATE]
proof (prove)
using this:
(0::'b) \<notin> snd ` set xs

goal (1 subgoal):
 1. (0::'b) \<notin> snd ` set (filter P xs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'b) \<notin> snd ` set (filter P xs)

goal (1 subgoal):
 1. sorted_wrt lt (map fst (filter P xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sorted_wrt lt (map fst (filter P xs))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
oalist_inv_raw xs
[PROOF STEP]
have "sorted_wrt lt (map fst xs)"
[PROOF STATE]
proof (prove)
using this:
oalist_inv_raw xs

goal (1 subgoal):
 1. sorted_wrt lt (map fst xs)
[PROOF STEP]
by (rule oalist_inv_rawD2)
[PROOF STATE]
proof (state)
this:
sorted_wrt lt (map fst xs)

goal (1 subgoal):
 1. sorted_wrt lt (map fst (filter P xs))
[PROOF STEP]
thus "sorted_wrt lt (map fst (filter P xs))"
[PROOF STATE]
proof (prove)
using this:
sorted_wrt lt (map fst xs)

goal (1 subgoal):
 1. sorted_wrt lt (map fst (filter P xs))
[PROOF STEP]
by (induct xs, simp, simp)
[PROOF STATE]
proof (state)
this:
sorted_wrt lt (map fst (filter P xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma oalist_inv_sort_oalist_raw: "oalist_inv (sort_oalist_raw xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oalist_inv (sort_oalist_raw xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. oalist_inv (sort_oalist_raw xs)
[PROOF STEP]
obtain xs' ko where xs: "xs = (xs', ko)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs' ko. xs = (xs', ko) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
xs = (xs', ko)

goal (1 subgoal):
 1. oalist_inv (sort_oalist_raw xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oalist_inv (sort_oalist_raw xs)
[PROOF STEP]
by (simp add: xs oalist_inv_raw_sort_oalist oalist_inv_alt)
[PROOF STATE]
proof (state)
this:
oalist_inv (sort_oalist_raw xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lookup_update_by_fun:
  "lookup (update_by_fun k f xs) k' = (if k = k' then f else id) (lookup xs k')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (update_by_fun k f xs) k' = (if k = k' then f else id) (lookup xs k')
[PROOF STEP]
by (simp add: lookup_def lookup_raw_update_by_fun_raw oalist_inv_list_of_oalist split del: if_split cong: if_cong)


[STATEMENT]
lemma PreFunctorFunctor[simp]: "Functor F \<Longrightarrow> PreFunctor F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Functor F \<Longrightarrow> PreFunctor F
[PROOF STEP]
by (simp add: Functor_def FunctorM_def)


[STATEMENT]
lemma monad_lift_set [simp]: "monad_base.lift return_set bind_set  = image"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monad_base.lift (\<lambda>x. {x}) (\<lambda>A f. \<Union> (f ` A)) = (`)
[PROOF STEP]
by(auto simp add: monad_base.lift_def o_def fun_eq_iff)


[STATEMENT]
lemma cr_envT_stateTD: "cr_envT_stateT s M m1 m2 \<Longrightarrow> M (run_env m1 s) (run_state m2 s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cr_envT_stateT s M m1 m2 \<Longrightarrow> M (run_env m1 s) (run_state m2 s)
[PROOF STEP]
by(auto elim!: cr_envT_stateTE dest: rel_funD simp add: eq_onp_def)


[STATEMENT]
lemma spmf_of_prob_optionT_transfer: "(cr_spmf_prob_optionT A ===> rel_spmf A) spmf_of_prob_optionT (\<lambda>x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cr_spmf_prob_optionT A ===> rel_spmf A) run_option (\<lambda>x. x)
[PROOF STEP]
by(auto simp add: rel_fun_def dest: cr_spmf_prob_optionTD)


[STATEMENT]
lemma finite_fvi[simp]: "finite (fvi b \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (fvi b \<phi>)
[PROOF STEP]
by (induction \<phi> arbitrary: b) simp_all


[STATEMENT]
lemma converse_pair_at_lang:
  "(pair_at_lang \<G> Q)\<inverse> = pair_at_lang (prod.swap \<G>) (Q|\<inverse>|)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pair_at_lang \<G> Q)\<inverse> = pair_at_lang (prod.swap \<G>) (Q|\<inverse>|)
[PROOF STEP]
by (auto simp: pair_at_lang_def)


[STATEMENT]
lemma first_time_image:
  assumes \<open>dilating f sub r\<close>
    shows \<open>first_time sub c n t = first_time r c (f n) t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. first_time sub c n t = first_time r c (f n) t
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. first_time sub c n t \<Longrightarrow> first_time r c (f n) t
 2. first_time r c (f n) t \<Longrightarrow> first_time sub c n t
[PROOF STEP]
assume \<open>first_time sub c n t\<close>
[PROOF STATE]
proof (state)
this:
first_time sub c n t

goal (2 subgoals):
 1. first_time sub c n t \<Longrightarrow> first_time r c (f n) t
 2. first_time r c (f n) t \<Longrightarrow> first_time sub c n t
[PROOF STEP]
with before_first_time[OF this]
[PROOF STATE]
proof (chain)
picking this:
?m < n \<Longrightarrow> time (Rep_run sub ?m c) < t
first_time sub c n t
[PROOF STEP]
have *:\<open>time ((Rep_run sub) n c) = t \<and> (\<forall>m < n. time((Rep_run sub) m c) < t)\<close>
[PROOF STATE]
proof (prove)
using this:
?m < n \<Longrightarrow> time (Rep_run sub ?m c) < t
first_time sub c n t

goal (1 subgoal):
 1. time (Rep_run sub n c) = t \<and> (\<forall>m<n. time (Rep_run sub m c) < t)
[PROOF STEP]
by (simp add: first_time_def)
[PROOF STATE]
proof (state)
this:
time (Rep_run sub n c) = t \<and> (\<forall>m<n. time (Rep_run sub m c) < t)

goal (2 subgoals):
 1. first_time sub c n t \<Longrightarrow> first_time r c (f n) t
 2. first_time r c (f n) t \<Longrightarrow> first_time sub c n t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
time (Rep_run sub n c) = t \<and> (\<forall>m<n. time (Rep_run sub m c) < t)

goal (2 subgoals):
 1. first_time sub c n t \<Longrightarrow> first_time r c (f n) t
 2. first_time r c (f n) t \<Longrightarrow> first_time sub c n t
[PROOF STEP]
have \<open>\<forall>n c. time (Rep_run sub n c) = time (Rep_run r (f n) c)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n c. time (Rep_run sub n c) = time (Rep_run r (f n) c)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
dilating f sub r

goal (1 subgoal):
 1. \<forall>n c. time (Rep_run sub n c) = time (Rep_run r (f n) c)
[PROOF STEP]
by (simp add: dilating_def)
[PROOF STATE]
proof (state)
this:
\<forall>n c. time (Rep_run sub n c) = time (Rep_run r (f n) c)

goal (2 subgoals):
 1. first_time sub c n t \<Longrightarrow> first_time r c (f n) t
 2. first_time r c (f n) t \<Longrightarrow> first_time sub c n t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
time (Rep_run sub n c) = t \<and> (\<forall>m<n. time (Rep_run sub m c) < t)
\<forall>n c. time (Rep_run sub n c) = time (Rep_run r (f n) c)
[PROOF STEP]
have **:
    \<open>time ((Rep_run r) (f n) c) = t \<and> (\<forall>m < n. time((Rep_run r) (f m) c) < t)\<close>
[PROOF STATE]
proof (prove)
using this:
time (Rep_run sub n c) = t \<and> (\<forall>m<n. time (Rep_run sub m c) < t)
\<forall>n c. time (Rep_run sub n c) = time (Rep_run r (f n) c)

goal (1 subgoal):
 1. time (Rep_run r (f n) c) = t \<and> (\<forall>m<n. time (Rep_run r (f m) c) < t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
time (Rep_run r (f n) c) = t \<and> (\<forall>m<n. time (Rep_run r (f m) c) < t)

goal (2 subgoals):
 1. first_time sub c n t \<Longrightarrow> first_time r c (f n) t
 2. first_time r c (f n) t \<Longrightarrow> first_time sub c n t
[PROOF STEP]
have \<open>\<forall>m < f n. time ((Rep_run r) m c) < t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>m<f n. time (Rep_run r m c) < t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>m<f n. time (Rep_run r m c) < t
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>m<f n. time (Rep_run r m c) < t
[PROOF STEP]
fix m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>m<f n. time (Rep_run r m c) < t
[PROOF STEP]
assume hyp:\<open>m < f n\<close>
[PROOF STATE]
proof (state)
this:
m < f n

goal (1 subgoal):
 1. \<forall>m<f n. time (Rep_run r m c) < t
[PROOF STEP]
have \<open>time ((Rep_run r) m c) < t\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. time (Rep_run r m c) < t
[PROOF STEP]
proof (cases \<open>\<exists>m\<^sub>0. f m\<^sub>0 = m\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
 2. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<exists>m\<^sub>0. f m\<^sub>0 = m

goal (2 subgoals):
 1. \<exists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
 2. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>m\<^sub>0. f m\<^sub>0 = m
[PROOF STEP]
obtain m\<^sub>0 where mm0:\<open>m = f m\<^sub>0\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>m\<^sub>0. f m\<^sub>0 = m

goal (1 subgoal):
 1. (\<And>m\<^sub>0. m = f m\<^sub>0 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m = f m\<^sub>0

goal (2 subgoals):
 1. \<exists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
 2. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
with hyp
[PROOF STATE]
proof (chain)
picking this:
m < f n
m = f m\<^sub>0
[PROOF STEP]
have m0n:\<open>m\<^sub>0 < n\<close>
[PROOF STATE]
proof (prove)
using this:
m < f n
m = f m\<^sub>0

goal (1 subgoal):
 1. m\<^sub>0 < n
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
m < f n
m = f m\<^sub>0
dilating f sub r

goal (1 subgoal):
 1. m\<^sub>0 < n
[PROOF STEP]
by (simp add: dilating_def dilating_fun_def strict_mono_less)
[PROOF STATE]
proof (state)
this:
m\<^sub>0 < n

goal (2 subgoals):
 1. \<exists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
 2. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
hence \<open>time ((Rep_run sub) m\<^sub>0 c) < t\<close>
[PROOF STATE]
proof (prove)
using this:
m\<^sub>0 < n

goal (1 subgoal):
 1. time (Rep_run sub m\<^sub>0 c) < t
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
m\<^sub>0 < n
time (Rep_run sub n c) = t \<and> (\<forall>m<n. time (Rep_run sub m c) < t)

goal (1 subgoal):
 1. time (Rep_run sub m\<^sub>0 c) < t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
time (Rep_run sub m\<^sub>0 c) < t

goal (2 subgoals):
 1. \<exists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
 2. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
time (Rep_run sub m\<^sub>0 c) < t

goal (1 subgoal):
 1. time (Rep_run r m c) < t
[PROOF STEP]
by (simp add: mm0 m0n **)
[PROOF STATE]
proof (state)
this:
time (Rep_run r m c) < t

goal (1 subgoal):
 1. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<nexists>m\<^sub>0. f m\<^sub>0 = m

goal (1 subgoal):
 1. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
hence \<open>\<exists>m\<^sub>p. f m\<^sub>p < m \<and> (\<forall>k. f m\<^sub>p < k \<and> k \<le> m \<longrightarrow> (\<nexists>k\<^sub>0. f k\<^sub>0 = k))\<close>
[PROOF STATE]
proof (prove)
using this:
\<nexists>m\<^sub>0. f m\<^sub>0 = m

goal (1 subgoal):
 1. \<exists>m\<^sub>p. f m\<^sub>p < m \<and> (\<forall>k. f m\<^sub>p < k \<and> k \<le> m \<longrightarrow> (\<nexists>k\<^sub>0. f k\<^sub>0 = k))
[PROOF STEP]
using greatest_prev_image[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<nexists>m\<^sub>0. f m\<^sub>0 = m
\<nexists>n\<^sub>0. f n\<^sub>0 = ?n \<Longrightarrow> \<exists>n\<^sub>p. f n\<^sub>p < ?n \<and> (\<forall>k. f n\<^sub>p < k \<and> k \<le> ?n \<longrightarrow> (\<nexists>k\<^sub>0. f k\<^sub>0 = k))

goal (1 subgoal):
 1. \<exists>m\<^sub>p. f m\<^sub>p < m \<and> (\<forall>k. f m\<^sub>p < k \<and> k \<le> m \<longrightarrow> (\<nexists>k\<^sub>0. f k\<^sub>0 = k))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>m\<^sub>p. f m\<^sub>p < m \<and> (\<forall>k. f m\<^sub>p < k \<and> k \<le> m \<longrightarrow> (\<nexists>k\<^sub>0. f k\<^sub>0 = k))

goal (1 subgoal):
 1. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
\<exists>m\<^sub>p. f m\<^sub>p < m \<and> (\<forall>k. f m\<^sub>p < k \<and> k \<le> m \<longrightarrow> (\<nexists>k\<^sub>0. f k\<^sub>0 = k))
[PROOF STEP]
obtain m\<^sub>p where
          mp:\<open>f m\<^sub>p < m \<and> (\<forall>k. f m\<^sub>p < k \<and> k \<le> m \<longrightarrow> (\<nexists>k\<^sub>0. f k\<^sub>0 = k))\<close>
[PROOF STATE]
proof (prove)
using this:
\<exists>m\<^sub>p. f m\<^sub>p < m \<and> (\<forall>k. f m\<^sub>p < k \<and> k \<le> m \<longrightarrow> (\<nexists>k\<^sub>0. f k\<^sub>0 = k))

goal (1 subgoal):
 1. (\<And>m\<^sub>p. f m\<^sub>p < m \<and> (\<forall>k. f m\<^sub>p < k \<and> k \<le> m \<longrightarrow> (\<nexists>k\<^sub>0. f k\<^sub>0 = k)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f m\<^sub>p < m \<and> (\<forall>k. f m\<^sub>p < k \<and> k \<le> m \<longrightarrow> (\<nexists>k\<^sub>0. f k\<^sub>0 = k))

goal (1 subgoal):
 1. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
hence \<open>time ((Rep_run r) m c) = time ((Rep_run sub) m\<^sub>p c)\<close>
[PROOF STATE]
proof (prove)
using this:
f m\<^sub>p < m \<and> (\<forall>k. f m\<^sub>p < k \<and> k \<le> m \<longrightarrow> (\<nexists>k\<^sub>0. f k\<^sub>0 = k))

goal (1 subgoal):
 1. time (Rep_run r m c) = time (Rep_run sub m\<^sub>p c)
[PROOF STEP]
using time_stuttering[OF assms]
[PROOF STATE]
proof (prove)
using this:
f m\<^sub>p < m \<and> (\<forall>k. f m\<^sub>p < k \<and> k \<le> m \<longrightarrow> (\<nexists>k\<^sub>0. f k\<^sub>0 = k))
\<lbrakk>time (Rep_run sub ?n ?c) = ?\<tau>; \<And>k. f ?n < k \<and> k \<le> ?m \<Longrightarrow> \<nexists>k\<^sub>0. f k\<^sub>0 = k; f ?n < ?m\<rbrakk> \<Longrightarrow> time (Rep_run r ?m ?c) = ?\<tau>

goal (1 subgoal):
 1. time (Rep_run r m c) = time (Rep_run sub m\<^sub>p c)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
time (Rep_run r m c) = time (Rep_run sub m\<^sub>p c)

goal (1 subgoal):
 1. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
time (Rep_run r m c) = time (Rep_run sub m\<^sub>p c)

goal (1 subgoal):
 1. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
from hyp mp
[PROOF STATE]
proof (chain)
picking this:
m < f n
f m\<^sub>p < m \<and> (\<forall>k. f m\<^sub>p < k \<and> k \<le> m \<longrightarrow> (\<nexists>k\<^sub>0. f k\<^sub>0 = k))
[PROOF STEP]
have \<open>f m\<^sub>p < f n\<close>
[PROOF STATE]
proof (prove)
using this:
m < f n
f m\<^sub>p < m \<and> (\<forall>k. f m\<^sub>p < k \<and> k \<le> m \<longrightarrow> (\<nexists>k\<^sub>0. f k\<^sub>0 = k))

goal (1 subgoal):
 1. f m\<^sub>p < f n
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
f m\<^sub>p < f n

goal (1 subgoal):
 1. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
hence \<open>m\<^sub>p < n\<close>
[PROOF STATE]
proof (prove)
using this:
f m\<^sub>p < f n

goal (1 subgoal):
 1. m\<^sub>p < n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f m\<^sub>p < f n
dilating f sub r

goal (1 subgoal):
 1. m\<^sub>p < n
[PROOF STEP]
by (simp add:dilating_def dilating_fun_def strict_mono_less)
[PROOF STATE]
proof (state)
this:
m\<^sub>p < n

goal (1 subgoal):
 1. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
hence \<open>time ((Rep_run sub) m\<^sub>p c) < t\<close>
[PROOF STATE]
proof (prove)
using this:
m\<^sub>p < n

goal (1 subgoal):
 1. time (Rep_run sub m\<^sub>p c) < t
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
m\<^sub>p < n
time (Rep_run sub n c) = t \<and> (\<forall>m<n. time (Rep_run sub m c) < t)

goal (1 subgoal):
 1. time (Rep_run sub m\<^sub>p c) < t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
time (Rep_run sub m\<^sub>p c) < t

goal (1 subgoal):
 1. \<nexists>m\<^sub>0. f m\<^sub>0 = m \<Longrightarrow> time (Rep_run r m c) < t
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
time (Rep_run r m c) < t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
time (Rep_run r m c) < t

goal (1 subgoal):
 1. time (Rep_run r m c) < t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
time (Rep_run r m c) < t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
time (Rep_run r m c) < t

goal (1 subgoal):
 1. \<forall>m<f n. time (Rep_run r m c) < t
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?m2 < f n \<Longrightarrow> time (Rep_run r ?m2 c) < t

goal (1 subgoal):
 1. \<forall>m<f n. time (Rep_run r m c) < t
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?m2 < f n \<Longrightarrow> time (Rep_run r ?m2 c) < t

goal (1 subgoal):
 1. \<forall>m<f n. time (Rep_run r m c) < t
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>m<f n. time (Rep_run r m c) < t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>m<f n. time (Rep_run r m c) < t

goal (2 subgoals):
 1. first_time sub c n t \<Longrightarrow> first_time r c (f n) t
 2. first_time r c (f n) t \<Longrightarrow> first_time sub c n t
[PROOF STEP]
with **
[PROOF STATE]
proof (chain)
picking this:
time (Rep_run r (f n) c) = t \<and> (\<forall>m<n. time (Rep_run r (f m) c) < t)
\<forall>m<f n. time (Rep_run r m c) < t
[PROOF STEP]
show \<open>first_time r c (f n) t\<close>
[PROOF STATE]
proof (prove)
using this:
time (Rep_run r (f n) c) = t \<and> (\<forall>m<n. time (Rep_run r (f m) c) < t)
\<forall>m<f n. time (Rep_run r m c) < t

goal (1 subgoal):
 1. first_time r c (f n) t
[PROOF STEP]
by (simp add: alt_first_time_def)
[PROOF STATE]
proof (state)
this:
first_time r c (f n) t

goal (1 subgoal):
 1. first_time r c (f n) t \<Longrightarrow> first_time sub c n t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. first_time r c (f n) t \<Longrightarrow> first_time sub c n t
[PROOF STEP]
assume \<open>first_time r c (f n) t\<close>
[PROOF STATE]
proof (state)
this:
first_time r c (f n) t

goal (1 subgoal):
 1. first_time r c (f n) t \<Longrightarrow> first_time sub c n t
[PROOF STEP]
hence *:\<open>time ((Rep_run r) (f n) c) = t \<and> (\<forall>k < f n. time ((Rep_run r) k c) < t)\<close>
[PROOF STATE]
proof (prove)
using this:
first_time r c (f n) t

goal (1 subgoal):
 1. time (Rep_run r (f n) c) = t \<and> (\<forall>k<f n. time (Rep_run r k c) < t)
[PROOF STEP]
by (simp add: first_time_def before_first_time)
[PROOF STATE]
proof (state)
this:
time (Rep_run r (f n) c) = t \<and> (\<forall>k<f n. time (Rep_run r k c) < t)

goal (1 subgoal):
 1. first_time r c (f n) t \<Longrightarrow> first_time sub c n t
[PROOF STEP]
hence \<open>time ((Rep_run sub) n c) = t\<close>
[PROOF STATE]
proof (prove)
using this:
time (Rep_run r (f n) c) = t \<and> (\<forall>k<f n. time (Rep_run r k c) < t)

goal (1 subgoal):
 1. time (Rep_run sub n c) = t
[PROOF STEP]
using assms dilating_def
[PROOF STATE]
proof (prove)
using this:
time (Rep_run r (f n) c) = t \<and> (\<forall>k<f n. time (Rep_run r k c) < t)
dilating f sub r
dilating ?f ?sub ?r \<equiv> dilating_fun ?f ?r \<and> (\<forall>n c. time (Rep_run ?sub n c) = time (Rep_run ?r (?f n) c)) \<and> (\<forall>n c. hamlet (Rep_run ?sub n c) = hamlet (Rep_run ?r (?f n) c))

goal (1 subgoal):
 1. time (Rep_run sub n c) = t
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
time (Rep_run sub n c) = t

goal (1 subgoal):
 1. first_time r c (f n) t \<Longrightarrow> first_time sub c n t
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
time (Rep_run sub n c) = t

goal (1 subgoal):
 1. first_time r c (f n) t \<Longrightarrow> first_time sub c n t
[PROOF STEP]
from *
[PROOF STATE]
proof (chain)
picking this:
time (Rep_run r (f n) c) = t \<and> (\<forall>k<f n. time (Rep_run r k c) < t)
[PROOF STEP]
have \<open>(\<forall>k < n. time ((Rep_run sub) k c) < t)\<close>
[PROOF STATE]
proof (prove)
using this:
time (Rep_run r (f n) c) = t \<and> (\<forall>k<f n. time (Rep_run r k c) < t)

goal (1 subgoal):
 1. \<forall>k<n. time (Rep_run sub k c) < t
[PROOF STEP]
using assms dilating_def dilating_fun_def strict_monoD
[PROOF STATE]
proof (prove)
using this:
time (Rep_run r (f n) c) = t \<and> (\<forall>k<f n. time (Rep_run r k c) < t)
dilating f sub r
dilating ?f ?sub ?r \<equiv> dilating_fun ?f ?r \<and> (\<forall>n c. time (Rep_run ?sub n c) = time (Rep_run ?r (?f n) c)) \<and> (\<forall>n c. hamlet (Rep_run ?sub n c) = hamlet (Rep_run ?r (?f n) c))
dilating_fun ?f ?r \<equiv> strict_mono ?f \<and> ?f 0 = 0 \<and> (\<forall>n. n \<le> ?f n \<and> ((\<nexists>n\<^sub>0. ?f n\<^sub>0 = n) \<longrightarrow> (\<forall>c. \<not> hamlet (Rep_run ?r n c))) \<and> ((\<nexists>n\<^sub>0. ?f n\<^sub>0 = Suc n) \<longrightarrow> (\<forall>c. time (Rep_run ?r (Suc n) c) = time (Rep_run ?r n c))))
\<lbrakk>strict_mono ?f; ?x < ?y\<rbrakk> \<Longrightarrow> ?f ?x < ?f ?y

goal (1 subgoal):
 1. \<forall>k<n. time (Rep_run sub k c) < t
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<forall>k<n. time (Rep_run sub k c) < t

goal (1 subgoal):
 1. first_time r c (f n) t \<Longrightarrow> first_time sub c n t
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
time (Rep_run sub n c) = t
\<forall>k<n. time (Rep_run sub k c) < t
[PROOF STEP]
show \<open>first_time sub c n t\<close>
[PROOF STATE]
proof (prove)
using this:
time (Rep_run sub n c) = t
\<forall>k<n. time (Rep_run sub k c) < t

goal (1 subgoal):
 1. first_time sub c n t
[PROOF STEP]
by (simp add: alt_first_time_def)
[PROOF STATE]
proof (state)
this:
first_time sub c n t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fix_add: "fetch ap ((x::nat) + 2*n) b = fetch ap (2*n + x) b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fetch ap (x + 2 * n) b = fetch ap (2 * n + x) b
[PROOF STEP]
using Suc_1 add.commute
[PROOF STATE]
proof (prove)
using this:
Suc 1 = 2
?a + ?b = ?b + ?a

goal (1 subgoal):
 1. fetch ap (x + 2 * n) b = fetch ap (2 * n + x) b
[PROOF STEP]
by metis


[STATEMENT]
theorem gt_compat_fun:
  assumes
    wary_t: "wary t" and
    t'_gt_t: "t' >\<^sub>t t"
  shows "App s t' >\<^sub>t App s t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. App s t' >\<^sub>t App s t
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. App s t' >\<^sub>t App s t
[PROOF STEP]
have vars_st': "vars_mset (App s t') \<supseteq># vars_mset (App s t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_mset (App s t) \<subseteq># vars_mset (App s t')
[PROOF STEP]
by (simp add: t'_gt_t gt_imp_vars_mset)
[PROOF STATE]
proof (state)
this:
vars_mset (App s t) \<subseteq># vars_mset (App s t')

goal (1 subgoal):
 1. App s t' >\<^sub>t App s t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. App s t' >\<^sub>t App s t
[PROOF STEP]
proof (cases "wt t' > wt t")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. wt t < wt t' \<Longrightarrow> App s t' >\<^sub>t App s t
 2. \<not> wt t < wt t' \<Longrightarrow> App s t' >\<^sub>t App s t
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
wt t < wt t'

goal (2 subgoals):
 1. wt t < wt t' \<Longrightarrow> App s t' >\<^sub>t App s t
 2. \<not> wt t < wt t' \<Longrightarrow> App s t' >\<^sub>t App s t
[PROOF STEP]
hence wt_st': "wt (App s t') > wt (App s t)"
[PROOF STATE]
proof (prove)
using this:
wt t < wt t'

goal (1 subgoal):
 1. wt (App s t) < wt (App s t')
[PROOF STEP]
by (simp only: wt.simps)
[PROOF STATE]
proof (state)
this:
wt (App s t) < wt (App s t')

goal (2 subgoals):
 1. wt t < wt t' \<Longrightarrow> App s t' >\<^sub>t App s t
 2. \<not> wt t < wt t' \<Longrightarrow> App s t' >\<^sub>t App s t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. App s t' >\<^sub>t App s t
[PROOF STEP]
by (rule gt_wt[OF vars_st' wt_st'])
[PROOF STATE]
proof (state)
this:
App s t' >\<^sub>t App s t

goal (1 subgoal):
 1. \<not> wt t < wt t' \<Longrightarrow> App s t' >\<^sub>t App s t
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> wt t < wt t' \<Longrightarrow> App s t' >\<^sub>t App s t
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> wt t < wt t'

goal (1 subgoal):
 1. \<not> wt t < wt t' \<Longrightarrow> App s t' >\<^sub>t App s t
[PROOF STEP]
hence "wt t' = wt t"
[PROOF STATE]
proof (prove)
using this:
\<not> wt t < wt t'

goal (1 subgoal):
 1. wt t' = wt t
[PROOF STEP]
using t'_gt_t gt_imp_wt_ge order.not_eq_order_implies_strict
[PROOF STATE]
proof (prove)
using this:
\<not> wt t < wt t'
t' >\<^sub>t t
?t >\<^sub>t ?s \<Longrightarrow> wt ?s \<le> wt ?t
\<lbrakk>?a \<noteq> ?b; ?a \<le> ?b\<rbrakk> \<Longrightarrow> ?a < ?b

goal (1 subgoal):
 1. wt t' = wt t
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
wt t' = wt t

goal (1 subgoal):
 1. \<not> wt t < wt t' \<Longrightarrow> App s t' >\<^sub>t App s t
[PROOF STEP]
hence wt_st': "wt (App s t') = wt (App s t)"
[PROOF STATE]
proof (prove)
using this:
wt t' = wt t

goal (1 subgoal):
 1. wt (App s t') = wt (App s t)
[PROOF STEP]
by (simp only: wt.simps)
[PROOF STATE]
proof (state)
this:
wt (App s t') = wt (App s t)

goal (1 subgoal):
 1. \<not> wt t < wt t' \<Longrightarrow> App s t' >\<^sub>t App s t
[PROOF STEP]
have head_st': "head (App s t') = head (App s t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. head (App s t') = head (App s t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
head (App s t') = head (App s t)

goal (1 subgoal):
 1. \<not> wt t < wt t' \<Longrightarrow> App s t' >\<^sub>t App s t
[PROOF STEP]
have extf: "\<And>f. extf f (>\<^sub>t) (args s @ [t']) (args s @ [t])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. extf f (>\<^sub>t) (args s @ [t']) (args s @ [t])
[PROOF STEP]
using t'_gt_t
[PROOF STATE]
proof (prove)
using this:
t' >\<^sub>t t

goal (1 subgoal):
 1. \<And>f. extf f (>\<^sub>t) (args s @ [t']) (args s @ [t])
[PROOF STEP]
by (metis extf_compat_list gt_irrefl[OF wary_t])
[PROOF STATE]
proof (state)
this:
extf ?f (>\<^sub>t) (args s @ [t']) (args s @ [t])

goal (1 subgoal):
 1. \<not> wt t < wt t' \<Longrightarrow> App s t' >\<^sub>t App s t
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. App s t' >\<^sub>t App s t
[PROOF STEP]
by (rule gt_same[OF vars_st' wt_st' head_st']) (simp add: extf)
[PROOF STATE]
proof (state)
this:
App s t' >\<^sub>t App s t

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
App s t' >\<^sub>t App s t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "\<FF> \<F> \<Longrightarrow> MT2(\<^bold>\<not>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> MT2 \<^bold>\<not>
[PROOF STEP]
nitpick
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<F> \<Longrightarrow> MT2 \<^bold>\<not>
[PROOF STEP]
oops