kings-crown/FVELER_Isabelle huggingface dataset:
theory Ctac

lemma ceqv_xpres_lvar_nondet_init:
  "ceqv_xpres_lvar_nondet_init xf v_upd pres \<Longrightarrow>
   ceqv_xpres \<Gamma> xf v True (lvar_nondet_init v_acc v_upd) pres pres_abr False (lvar_nondet_init v_acc v_upd)" apply (clarsimp simp: ceqv_xpres_defs lvar_nondet_init_def ceqv_xpres_lvar_nondet_init_def) apply (intro conjI impI; erule exec.cases; clarsimp) done

\<comment> \<open>
Some ceqv_xpres rules as stated above are too general for the automation, and need to
be instantiated to ensure that output parameters are fully determined by input parameters.
The instantiations we use in `ceqv_xpres_rules` allow us to take advantage of exceptional
control flow.
\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres_lvar_nondet_init xf v_upd pres \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (lvar_nondet_init v_acc v_upd) pres pres_abr False (lvar_nondet_init v_acc v_upd) proof (prove)
goal (1 subgoal):
 1. \<And>s t. pres \<longrightarrow> (\<forall>s v. xf (v_upd (\<lambda>_. v) s) = xf s) \<Longrightarrow> (\<Gamma>\<turnstile> \<langle>Spec {(s, t). \<exists>v. t = v_upd (\<lambda>_. v) s},Normal s\<rangle> \<Rightarrow> Normal t \<longrightarrow> pres \<longrightarrow> xf s = v \<longrightarrow> xf t = v) \<and> (\<Gamma>\<turnstile> \<langle>Spec {(s, t). \<exists>v. t = v_upd (\<lambda>_. v) s},Normal s\<rangle> \<Rightarrow> Abrupt t \<longrightarrow> pres_abr \<longrightarrow> xf s = v \<longrightarrow> xf t = v) proof (prove)
goal:
No subgoals!
theory Ctac

lemma ceqv_xpres_FalseI:
  "ceqv_xpres \<Gamma> xf v pres c False False False c" by (simp add: ceqv_xpres_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v pres c False False False c
theory Ctac

lemma ceqv_xpres_rewrite_basic_left_cong:
  "\<lbrakk> \<And>s. xf s = v \<Longrightarrow> f s = f'' s \<rbrakk>
     \<Longrightarrow> ceqv_xpres_rewrite_basic xf v f f'
           = ceqv_xpres_rewrite_basic xf v f'' f'" by (simp add: ceqv_xpres_rewrite_basic_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. xf s = v \<Longrightarrow> f s = f'' s) \<Longrightarrow> ceqv_xpres_rewrite_basic xf v f f' = ceqv_xpres_rewrite_basic xf v f'' f'
theory Ctac

lemma ceqv_xpres_rewrite_basic_refl:
  "ceqv_xpres_rewrite_basic xf v f f" by (simp add: ceqv_xpres_rewrite_basic_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres_rewrite_basic xf v f f
theory Ctac

lemma ceqv_xpres_basic_preserves_TrueI:
  "\<lbrakk> \<And>s. xf s = v \<longrightarrow> P s \<longrightarrow> xf (f s) = v \<rbrakk> \<Longrightarrow> ceqv_xpres_basic_preserves trace xf v P f True" by (simp add: ceqv_xpres_basic_preserves_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. xf s = v \<longrightarrow> P s \<longrightarrow> xf (f s) = v) \<Longrightarrow> ceqv_xpres_basic_preserves trace xf v P f True
theory Ctac

lemma ceqv_xpres_basic_preserves_FalseI:
  "ceqv_xpres_basic_preserves trace xf v P f False" by (simp add: ceqv_xpres_basic_preserves_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres_basic_preserves trace xf v P f False
theory Ctac

lemma ceqv_xpres_lvar_nondet_init_TrueI:
  "(\<And>s v. xf (v_upd (\<lambda>_. v) s) = xf s) \<Longrightarrow> ceqv_xpres_lvar_nondet_init xf v_upd True" by (simp add: ceqv_xpres_lvar_nondet_init_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s v. xf (v_upd (\<lambda>_. v) s) = xf s) \<Longrightarrow> ceqv_xpres_lvar_nondet_init xf v_upd True
theory Ctac

lemma ceqv_xpres_lvar_nondet_init_FalseI:
  "ceqv_xpres_lvar_nondet_init xf v_upd False" by (simp add: ceqv_xpres_lvar_nondet_init_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres_lvar_nondet_init xf v_upd False
theory Ctac

lemma ceqv_xpres_rewrite_set_rules:
  "ceqv_xpres_rewrite_basic xf v P P'
     \<Longrightarrow> ceqv_xpres_rewrite_set xf v {s. P s} {s. P' s}"
  "ceqv_xpres_rewrite_set xf v UNIV UNIV"
  "ceqv_xpres_rewrite_set xf v {} {}"
  "\<lbrakk> ceqv_xpres_rewrite_set xf v S S''; ceqv_xpres_rewrite_set xf v S' S''' \<rbrakk>
     \<Longrightarrow> ceqv_xpres_rewrite_set xf v (if G then S else S') (if G then S'' else S''')" by (simp_all add: ceqv_xpres_rewrite_set_def ceqv_xpres_rewrite_basic_def
             split: if_split)

\<comment> \<open>\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((ceqv_xpres_rewrite_basic xf v P P' \<Longrightarrow> ceqv_xpres_rewrite_set xf v {s. P s} {s. P' s}) &&& ceqv_xpres_rewrite_set xf v UNIV UNIV) &&& ceqv_xpres_rewrite_set xf v {} {} &&& (\<lbrakk>ceqv_xpres_rewrite_set xf v S S''; ceqv_xpres_rewrite_set xf v S' S'''\<rbrakk> \<Longrightarrow> ceqv_xpres_rewrite_set xf v (if G then S else S') (if G then S'' else S'''))
theory Ctac

lemma ccorres_save_pre_move:
  "ccorres_save_pre srel \<Gamma> rrel xf arrel axf G (S \<inter> E) G' hs a c
   \<longleftrightarrow> ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S (G' \<inter> E) hs a c" by (rule ccorres_save_pre_iff; blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_save_pre srel \<Gamma> rrel xf arrel axf G (S \<inter> E) G' hs a c = ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S (G' \<inter> E) hs a c
theory Ctac

lemma ccorres_save_pre_trivial:
  "ccorres_save_pre srel \<Gamma> rrel xf arrel axf G UNIV G' hs a c
   \<longleftrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs a c" unfolding ccorres_save_pre_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_save_pre srel \<Gamma> rrel xf arrel axf G UNIV G' hs a c = ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs a c proof (prove)
goal (1 subgoal):
 1. ccorres_underlying srel \<Gamma> rrel xf arrel axf G (G' \<inter> UNIV) hs a c = ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs a c
theory Ctac

lemma ccorres_save_pre_dup_iff:
  "ccorres_save_pre srel \<Gamma> rrel xf arrel axf G (S \<inter> E) (G' \<inter> E) hs a c
   \<longleftrightarrow> ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S (G' \<inter> E) hs a c" by (rule ccorres_save_pre_iff; blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_save_pre srel \<Gamma> rrel xf arrel axf G (S \<inter> E) (G' \<inter> E) hs a c = ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S (G' \<inter> E) hs a c
theory Ctac

lemma ccorres_save_pre_Int_def:
  "ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S (G' \<inter> E) hs m c
   \<longleftrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G (G' \<inter> S \<inter> E) hs m c" by (prop_tac "G' \<inter> E \<inter> S = G' \<inter> S \<inter> E", blast, simp add: ccorres_save_pre_def)

\<comment> \<open>If we use this rule for the first lift in `cinit`, then the precondition will be consumed
    in the second lift, by `ccorres_save_pre_init_lift2`. This reflects the older behaviour
    of `cinit`, which always dropped preconditions used for lifting. It is still used for all
    local variable lifting.\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S (G' \<inter> E) hs m c = ccorres_underlying srel \<Gamma> rrel xf arrel axf G (G' \<inter> S \<inter> E) hs m c
theory Ctac

lemma ccorres_save_pre_lift1:
  assumes "\<And>rv'. P rv' \<Longrightarrow> ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S (G' \<inter> {s. xf' s = rv'}) hs m c"
  shows "ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S (G' \<inter> {s. P (xf' s)}) hs m c" using assms by (clarsimp simp: ccorres_save_pre_Int_def ccorres_tmp_lift1)

\<comment> \<open>On the other hand, if we use this rule for the first lift in `cinit`, the precondition is
    copied. One copy will be consumed by `ccorres_save_pre_init_lift2`, but the second copy will be
    used to restore the precondition at the end of `cinit`. The end result is that `cinit` performs
    lifting without dropping the precondition. Ideally, we would use this for all variable lifting,
    but using this for local variables breaks some existing proofs. Currently, we use it for
    lifting global variables only; see `ccorres_save_pre_lift1_save_global` below.\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S (G' \<inter> {s. P (xf' s)}) hs m c proof (prove)
using this:
P ?rv' \<Longrightarrow> ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S (G' \<inter> {s. xf' s = ?rv'}) hs m c

goal (1 subgoal):
 1. ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S (G' \<inter> {s. P (xf' s)}) hs m c
theory Ctac

lemma ccorres_save_pre_init_lift2:
  assumes ceqv: "\<And>t t'. ceqv \<Gamma> xf' rv' t t' c c'"
  assumes ccorres: "ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S G' hs m c'"
  shows "ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S (G' \<inter> {s. xf' s = rv'}) hs m c" using  ccorres_init_tmp_lift2[OF ceqv ccorres[unfolded ccorres_save_pre_def]] by (clarsimp simp: ccorres_save_pre_Int_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S (G' \<inter> {s. xf' s = rv'}) hs m c proof (prove)
using this:
ccorres_underlying srel \<Gamma> rrel xf arrel axf G (G' \<inter> S \<inter> {s. xf' s = rv'}) hs m c

goal (1 subgoal):
 1. ccorres_save_pre srel \<Gamma> rrel xf arrel axf G S (G' \<inter> {s. xf' s = rv'}) hs m c
theory Ctac

lemma ccorres_save_pre_UNIV_Int:
  assumes "ccorres_save_pre rf_sr \<Gamma> r xf arrel axf G S (UNIV \<inter> {x. P x}) hs a c"
  shows "ccorres_save_pre rf_sr \<Gamma> r xf arrel axf G S {x. P x} hs a c" using assms by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_save_pre rf_sr \<Gamma> r xf arrel axf G S {x. P x} hs a c proof (prove)
using this:
ccorres_save_pre rf_sr \<Gamma> r xf arrel axf G S (UNIV \<inter> {x. P x}) hs a c

goal (1 subgoal):
 1. ccorres_save_pre rf_sr \<Gamma> r xf arrel axf G S {x. P x} hs a c
theory Ctac

lemma simpl_sequence_Cons:
  "simpl_sequence f (x # xs) = Seq (f x) (simpl_sequence f xs)" by (simp add: simpl_sequence_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. simpl_sequence f (x # xs) = (f x;;
simpl_sequence f xs)
theory Ctac

lemma xpres_strong_False_trivial:
  "xpres_strong \<Gamma> xf v c False False False" by (simp add: xpres_strong_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v c False False False
theory Ctac

lemma ceqv_xpres_eq_ceqv:
  "ceqv_xpres \<Gamma> xf v True c False False False c' = (\<forall>s t. ceqv \<Gamma> xf v s t c c')" by (simp add: ceqv_xpres_def xpres_strong_False_trivial)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True c False False False c' = (\<forall>s t. ceqv \<Gamma> xf v s t c c')
theory Ctac

lemma ccorres_underlying_name_seq_bound:
  "(\<not> CP n \<and> (\<forall>n' < n. CP n'))
    \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m
        (simpl_sequence c' (map f [0 ..< n]))
    \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf
          G G' hs m (if \<exists>n. \<not> CP n
            then simpl_sequence c' (map f [0 ..< (LEAST n. \<not> CP n)])
            else c)" apply (subst if_P, blast) apply (subst Least_equality[where x=n], simp_all) apply (rule ccontr, simp add: linorder_not_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> CP n \<and> (\<forall>n'<n. CP n'); ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m (simpl_sequence c' (map f [0..<n]))\<rbrakk> \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m (if \<exists>n. \<not> CP n then simpl_sequence c' (map f [0..<LEAST n. \<not> CP n]) else c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> CP n \<and> (\<forall>n'<n. CP n'); ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m (simpl_sequence c' (map f [0..<n]))\<rbrakk> \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m (simpl_sequence c' (map f [0..<LEAST n. \<not> CP n])) proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>\<not> CP n \<and> (\<forall>n'<n. CP n'); ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m (simpl_sequence c' (map f [0..<n])); \<not> CP y\<rbrakk> \<Longrightarrow> n \<le> y proof (prove)
goal:
No subgoals!
theory Ctac

lemma wpc_helper_ccorres_final:
  "ccorres_underlying sr G rv xf arrel axf Q Q'' hs f f'
   \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'')
                  (ccorres_underlying sr G rv xf arrel axf P P'' hs f f')" apply (clarsimp simp: wpc_helper_def) apply (erule ccorres_guard_imp) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr G rv xf arrel axf Q Q'' hs f f' \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (ccorres_underlying sr G rv xf arrel axf P P'' hs f f') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying sr G rv xf arrel axf Q Q'' hs f f'; \<forall>s. P s \<longrightarrow> Q s; \<forall>s. P' s \<longrightarrow> Q' s; P'' \<subseteq> Q''\<rbrakk> \<Longrightarrow> ccorres_underlying sr G rv xf arrel axf P P'' hs f f' proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> Q s; \<forall>s. P' s \<longrightarrow> Q' s; P'' \<subseteq> Q''; P s\<rbrakk> \<Longrightarrow> Q s
 2. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> Q s; \<forall>s. P' s \<longrightarrow> Q' s; P'' \<subseteq> Q''; s \<in> P''\<rbrakk> \<Longrightarrow> s \<in> Q'' proof (prove)
goal:
No subgoals!
theory Ctac

lemma c_guard_field_abs:
  fixes p :: "'a :: mem_type ptr"
  assumes abs: "\<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<longrightarrow> c_guard p"
  shows "\<forall>s s'. (s, s') \<in> rf_sr \<and> P s
  \<and> (P' s' \<and> (\<exists>t. field_ti TYPE('a) f = Some t \<and> export_uinfo t = export_uinfo (typ_info_t TYPE('b :: mem_type))))
  \<longrightarrow> c_guard (Ptr &(p\<rightarrow>f) :: 'b :: mem_type ptr)" using c_guard_field abs by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<and> (\<exists>t. field_ti TYPE('a) f = Some t \<and> export_uinfo t = export_uinfo (typ_info_t TYPE('b))) \<longrightarrow> c_guard (PTR('b) &(p\<rightarrow>f)) proof (prove)
using this:
\<lbrakk>c_guard ?p; field_ti TYPE(?'a) ?f = Some ?t; export_uinfo ?t = export_uinfo (typ_info_t TYPE(?'b))\<rbrakk> \<Longrightarrow> c_guard (PTR(?'b) &(?p\<rightarrow>?f))
\<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<longrightarrow> c_guard p

goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<and> (\<exists>t. field_ti TYPE('a) f = Some t \<and> export_uinfo t = export_uinfo (typ_info_t TYPE('b))) \<longrightarrow> c_guard (PTR('b) &(p\<rightarrow>f))
theory Ctac

lemma h_t_valid_field_abs:
  fixes p :: "'a :: mem_type ptr"
  assumes abs: "\<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<longrightarrow> s' \<Turnstile>\<^sub>c p"
  shows "\<forall>s s'. (s, s') \<in> rf_sr \<and> P s
  \<and> (P' s' \<and> (\<exists>t. field_ti TYPE('a) f = Some t \<and> export_uinfo t = export_uinfo (typ_info_t TYPE('b :: mem_type))))
  \<longrightarrow> s' \<Turnstile>\<^sub>c (Ptr &(p\<rightarrow>f) :: 'b :: mem_type ptr)" using h_t_valid_field abs by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<and> (\<exists>t. field_ti TYPE('a) f = Some t \<and> export_uinfo t = export_uinfo (typ_info_t TYPE('b))) \<longrightarrow> s' \<Turnstile>\<^sub>c PTR('b) &(p\<rightarrow>f) proof (prove)
using this:
\<lbrakk>?d \<Turnstile>\<^sub>t ?p; field_ti TYPE(?'a) ?f = Some ?t; export_uinfo ?t = export_uinfo (typ_info_t TYPE(?'b))\<rbrakk> \<Longrightarrow> ?d \<Turnstile>\<^sub>t PTR(?'b) &(?p\<rightarrow>?f)
\<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<longrightarrow> s' \<Turnstile>\<^sub>c p

goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<and> (\<exists>t. field_ti TYPE('a) f = Some t \<and> export_uinfo t = export_uinfo (typ_info_t TYPE('b))) \<longrightarrow> s' \<Turnstile>\<^sub>c PTR('b) &(p\<rightarrow>f)
theory Ctac

lemma abs_c_guard_from_abs_h_t_valid:
  "(\<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<longrightarrow> s' \<Turnstile>\<^sub>c p)
    \<Longrightarrow> (\<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<longrightarrow> c_guard p)" by (auto intro: h_t_valid_c_guard)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<longrightarrow> s' \<Turnstile>\<^sub>c p \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<longrightarrow> c_guard p
theory Ctac

lemma array_assertion_abs_to_const:
  "\<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s'
    \<longrightarrow> (Suc 0 = 0 \<or> array_assertion (ptr s s') (n s s') (htd s s'))
    \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s'
        \<longrightarrow> array_assertion (ptr s s') (n s s') (htd s s')" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<longrightarrow> Suc 0 = 0 \<or> array_assertion (ptr s s') (n s s') (htd s s') \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> P s \<and> P' s' \<longrightarrow> array_assertion (ptr s s') (n s s') (htd s s')
theory Ctac

lemma ptr_add_assertion_positive_helper:
  "n == m \<Longrightarrow> 0 \<le> sint m \<Longrightarrow> 0 \<le> sint n" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<equiv> m; 0 \<le> sint m\<rbrakk> \<Longrightarrow> 0 \<le> sint n
theory Ctac

lemma cvariable_array_map_const_add_map_option:
  "cvariable_array_map_relation m (\<lambda>_. n)
        = cvariable_array_map_relation (map_option f o m) (\<lambda>_. n)" by (simp add: cvariable_array_map_relation_def fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cvariable_array_map_relation m (\<lambda>_. n) = cvariable_array_map_relation (map_option f \<circ> m) (\<lambda>_. n)
theory Ctac

lemma ccorres_move_const_guard:
  "ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m c
    \<Longrightarrow> ccorres_underlying rf_sr Gamm rrel xf arrel axf
         (P and K G) P' hs m (Guard F {s. G} c)"
  "ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (c ;; d)
    \<Longrightarrow> ccorres_underlying rf_sr Gamm rrel xf arrel axf
         (P and K G) P' hs m (Guard F {s. G} c ;; d)" apply (rule ccorres_guard_imp2, erule ccorres_Guard, simp) apply (rule ccorres_guard_imp2, erule ccorres_Guard_Seq, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m c \<Longrightarrow> ccorres_underlying rf_sr Gamm rrel xf arrel axf (P and K G) P' hs m (Guard F \<lbrace>G\<rbrace> c)) &&& (ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (c;;
d) \<Longrightarrow> ccorres_underlying rf_sr Gamm rrel xf arrel axf (P and K G) P' hs m (Guard F \<lbrace>G\<rbrace> c;;
d)) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr Gamm rrel xf arrel axf P P' hs m (c;;
d) \<Longrightarrow> ccorres_underlying rf_sr Gamm rrel xf arrel axf (P and K G) P' hs m (Guard F \<lbrace>G\<rbrace> c;;
d) proof (prove)
goal:
No subgoals!
theory Ctac

lemma liftM_exs_valid:
  "\<lbrace>P\<rbrace> m \<exists>\<lbrace>\<lambda>rv. Q (f rv)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> liftM f m \<exists>\<lbrace>Q\<rbrace>" unfolding liftM_def exs_valid_def apply (clarsimp) apply (drule spec, drule (1) mp) apply (clarsimp simp: bind_def return_def) apply (erule bexI [rotated]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> m \<exists>\<lbrace>\<lambda>rv. Q (f rv)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> liftM f m \<exists>\<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. P s \<longrightarrow> (\<exists>(rv, s')\<in>fst (m s). Q (f rv) s') \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<exists>(rv, s')\<in>fst ((do x <- m;
return (f x)
od) s). Q rv s') proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<exists>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> Q (f rv) s'); P s\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do x <- m;
return (f x)
od) s). case x of (rv, s') \<Rightarrow> Q rv s' proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P s; \<exists>x\<in>fst (m s). case x of (rv, s') \<Rightarrow> Q (f rv) s'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do x <- m;
return (f x)
od) s). case x of (rv, s') \<Rightarrow> Q rv s' proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (m s); Q (f a) b\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (m s). \<exists>x\<in>fst (case y of (x, s) \<Rightarrow> ({(f x, s)}, False)). case x of (x, xa) \<Rightarrow> Q x xa proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; Q (f a) b\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (case (a, b) of (x, s) \<Rightarrow> ({(f x, s)}, False)). case x of (x, xa) \<Rightarrow> Q x xa proof (prove)
goal:
No subgoals!
theory Ctac

lemma xpres_triv:
  "xpres G xf () c" by (simp add: xpres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres G xf () c
theory Ctac

lemma ceqv_Guard_UNIV:
  "ceqv G xf v s s' (Guard Err UNIV c) c'
       = ceqv G xf v s s' c c'" by (simp add: ceqv_def exec_Guard)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv G xf v s s' (Guard Err UNIV c) c' = ceqv G xf v s s' c c'
theory Ctac

lemma ceqv_guard_into_seq:
  "ceqv \<Gamma> xf v s s' (Guard Err S (a ;; b)) (Guard Err S a ;; b)" by (auto simp: ceqv_def elim!: exec_elim_cases intro: exec.intros)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v s s' (Guard Err S (a;;
b)) (Guard Err S a;;
b)
theory Ctac

lemma ceqv_Seq_Skip_cases:
  "\<lbrakk> \<And>s'. ceqv \<Gamma> xf v s s' a a'; \<And>s. ceqv \<Gamma> xf v s s' b c; xpres \<Gamma> xf v a;
        (c = Skip \<and> c' = a' \<or> c' = (a' ;; c)) \<rbrakk> \<Longrightarrow>
     ceqv \<Gamma> xf v s s' (a ;; b) c'" by (metis Seq_ceqv ceqv_remove_eqv_skip')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s'. ceqv \<Gamma> xf v s s' a a'; \<And>s. ceqv \<Gamma> xf v s s' b c; xpres \<Gamma> xf v a; c = SKIP \<and> c' = a' \<or> c' = (a';;
c)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf v s s' (a;;
b) c'
theory Ctac

lemma finish_ceqv_Seq_Skip_cases:
  "(Skip = Skip \<and> x = x \<or> x = y)"
  "(y = Skip \<and> (x ;; y) = z \<or> (x ;; y) = (x ;; y))" by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. SKIP = SKIP \<and> x = x \<or> x = y &&& y = SKIP \<and> (x;;
y) = z \<or> (x;;
y) = (x;;
y)
theory Ctac

lemma semantic_equiv_IF_True:
  "semantic_equiv G s s'  (IF True THEN c ELSE c' FI) c" apply (simp add: semantic_equiv_seq_assoc_eq[symmetric]) by (auto simp: semantic_equiv_def2 elim!: exec_Normal_elim_cases intro: exec.intros)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv G s s' (IF True THEN
  c
ELSE
  c'
FI) c proof (prove)
goal (1 subgoal):
 1. semantic_equiv G s s' (Cond UNIV c c') c