kings-crown/FVELER_Isabelle huggingface dataset:
theory Peterson_Atomicity

lemma peterson_sr_peterson_rel3:
  "peterson_sr as0 cs0 \<Longrightarrow> peterson_sr as cs
   \<Longrightarrow> peterson_rel ident as0 as \<Longrightarrow> peterson_rel3 ident cs0 cs" apply (clarsimp simp: peterson_rel_def peterson_rel3_def invs_def
                        invs_defs peterson_sr_ab_label) apply (clarsimp simp: peterson_sr_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>peterson_sr as0 cs0; peterson_sr as cs; peterson_rel ident as0 as\<rbrakk> \<Longrightarrow> peterson_rel3 ident cs0 cs proof (prove)
goal (1 subgoal):
 1. \<lbrakk>peterson_sr as0 cs0; peterson_sr as cs; (ab_label cs0 A = Critical \<or> ab_label cs0 B = Critical \<or> csI (cs2_v as0)) \<and> (ab_label cs0 A \<noteq> Critical \<and> (ab_label cs0 A = Awaiting \<longrightarrow> t_v as0 = B) \<or> ab_label cs0 B \<noteq> Critical \<and> (ab_label cs0 B = Awaiting \<longrightarrow> t_v as0 = A)) \<and> (\<forall>ident. ab_label cs0 ident \<noteq> Exited \<longrightarrow> ab_v as0 ident) \<longrightarrow> (ab_label cs A = Critical \<longrightarrow> ab_label cs B \<noteq> Critical) \<and> (ab_label cs A = Critical \<or> ab_label cs B = Critical \<or> csI (cs2_v as)) \<and> (ab_label cs A \<noteq> Critical \<and> (ab_label cs A = Awaiting \<longrightarrow> t_v as = B) \<or> ab_label cs B \<noteq> Critical \<and> (ab_label cs B = Awaiting \<longrightarrow> t_v as = A)) \<and> (\<forall>ident. ab_label cs ident \<noteq> Exited \<longrightarrow> ab_v as ident) \<and> ab_v as (other_ident ident) = ab_v as0 (other_ident ident) \<and> ab_label cs (other_ident ident) = ab_label cs0 (other_ident ident) \<and> (t_v as0 \<noteq> ident \<longrightarrow> t_v as \<noteq> ident) \<and> (ab_label cs0 (other_ident ident) = Critical \<longrightarrow> cs2_v as = cs2_v as0 \<and> cs1_v as = cs1_v as0); ab_label cs0 A = Critical \<longrightarrow> ab_label cs0 B \<noteq> Critical; ab_label cs0 A = Critical \<or> ab_label cs0 B = Critical \<or> csI (cs2_v cs0); ab_label cs0 A \<noteq> Critical \<and> (ab_label cs0 A = Awaiting \<longrightarrow> t_v cs0 = B) \<or> ab_label cs0 B \<noteq> Critical \<and> (ab_label cs0 B = Awaiting \<longrightarrow> t_v cs0 = A); \<forall>ident. ab_label cs0 ident \<noteq> Exited \<longrightarrow> ab_v cs0 ident\<rbrakk> \<Longrightarrow> (ab_label cs A = Critical \<longrightarrow> ab_label cs B \<noteq> Critical) \<and> (ab_label cs A = Critical \<or> ab_label cs B = Critical \<or> csI (cs2_v cs)) \<and> (ab_label cs A \<noteq> Critical \<and> (ab_label cs A = Awaiting \<longrightarrow> t_v cs = B) \<or> ab_label cs B \<noteq> Critical \<and> (ab_label cs B = Awaiting \<longrightarrow> t_v cs = A)) \<and> (\<forall>ident. ab_label cs ident \<noteq> Exited \<longrightarrow> ab_v cs ident) \<and> ab_v cs (other_ident ident) = ab_v cs0 (other_ident ident) \<and> ab_label cs (other_ident ident) = ab_label cs0 (other_ident ident) \<and> (t_v cs0 \<noteq> ident \<longrightarrow> t_v cs \<noteq> ident) \<and> (ab_label cs0 (other_ident ident) = Critical \<longrightarrow> cs2_v cs = cs2_v cs0) proof (prove)
goal:
No subgoals!
theory Peterson_Atomicity

lemma peterson_proc_prefix_closed[simp]:
  "prefix_closed (peterson_proc ident)" by (auto intro!: prefix_closed_bind
           simp: cs_closed peterson_proc_def acquire_lock_def release_lock_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed (peterson_proc ident)
theory Peterson_Atomicity

lemma peterson_proc_mutual_excl:
  "\<lbrace> \<lambda>s0 s. peterson_rel ident s0 s \<and> invs s
            \<and> ab_label s ident = Exited \<rbrace>,
   \<lbrace> peterson_rel (other_ident ident) \<rbrace>
     peterson_proc ident
   \<lbrace> peterson_rel ident \<rbrace>,
   \<lbrace> \<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s
               \<and> ab_label s ident = Exited \<rbrace>" apply (rule rg_strengthen_guar, rule rg_strengthen_post, rule validI_guar_post_conj_lift) apply (rule peterson_proc_mutual_excl_helper) apply (rule peterson_proc_mutual_excl_helper') apply (clarsimp simp: peterson_rel_helpers)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> peterson_proc ident \<lbrace>peterson_rel ident\<rbrace>, \<lbrace>\<lambda>rv s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrace>\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> peterson_proc ident \<lbrace>?G1.6\<rbrace>, \<lbrace>?Q1.6\<rbrace>
 2. \<lbrace>\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> peterson_proc ident \<lbrace>?G2.6\<rbrace>, \<lbrace>?Q2.6\<rbrace>
 3. \<And>v s0 s. ?Q1.6 v s0 s \<and> ?Q2.6 v s0 s \<Longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited
 4. \<And>s0 s. ?G1.6 s0 s \<and> ?G2.6 s0 s \<Longrightarrow> peterson_rel ident s0 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s0 s. peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited\<rbrace>, \<lbrace>peterson_rel (other_ident ident)\<rbrace> peterson_proc ident \<lbrace>?G2.6\<rbrace>, \<lbrace>?Q2.6\<rbrace>
 2. \<And>v s0 s. (peterson_rel3 ident s0 s \<and> invs s \<and> ab_label s ident = Exited) \<and> ?Q2.6 v s0 s \<Longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited
 3. \<And>s0 s. peterson_rel3 ident s0 s \<and> ?G2.6 s0 s \<Longrightarrow> peterson_rel ident s0 s proof (prove)
goal (2 subgoals):
 1. \<And>v s0 s. (peterson_rel3 ident s0 s \<and> invs s \<and> ab_label s ident = Exited) \<and> peterson_rel2 ident s0 s \<and> invs s \<and> ab_label s ident = Exited \<Longrightarrow> peterson_rel ident s0 s \<and> invs s \<and> ab_label s ident = Exited
 2. \<And>s0 s. peterson_rel3 ident s0 s \<and> peterson_rel2 ident s0 s \<Longrightarrow> peterson_rel ident s0 s proof (prove)
goal:
No subgoals!
theory Peterson_Atomicity

lemma abs_peterson_proc_prefix_closed[simp]:
  "prefix_closed (abs_peterson_proc ident)" by (auto intro!: prefix_closed_bind
           simp: cs_closed abs_peterson_proc_def acquire_lock_def release_lock_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed (abs_peterson_proc ident)
theory Peterson_Atomicity

lemma peterson_proc_system_prefix_closed[simp]:
  "prefix_closed (peterson_proc_system)" by (auto intro!: prefix_closed_bind prefix_closed_parallel
             simp: cs_closed peterson_proc_system_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed peterson_proc_system
theory Plus2_Prefix

lemma plus2_rel_trans[simp]:
  "rtranclp (plus2_rel tids ftids) = plus2_rel tids ftids" apply (rule rtranclp_id2) apply (simp add: plus2_rel_def) apply (clarsimp simp: plus2_rel_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (plus2_rel tids ftids)\<^sup>*\<^sup>* = plus2_rel tids ftids proof (prove)
goal (2 subgoals):
 1. \<forall>x. plus2_rel tids ftids x x
 2. \<forall>x xa. (plus2_rel tids ftids OO plus2_rel tids ftids) x xa \<le> plus2_rel tids ftids x xa proof (prove)
goal (1 subgoal):
 1. \<forall>x xa. (plus2_rel tids ftids OO plus2_rel tids ftids) x xa \<le> plus2_rel tids ftids x xa proof (prove)
goal:
No subgoals!
theory Plus2_Prefix

lemma plus2_inv_Suc[simp]:
  "tid \<in> tids \<Longrightarrow> finite tids
    \<Longrightarrow> plus2_inv tids (mainv_update Suc (threadv_update (point_update tid Suc) s))
        = plus2_inv tids s" apply (simp add: plus2_inv_def point_update_def) apply (simp add: sum.If_cases[where h=f and g=f and P="(=) tid" and A="tids" for f x, simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tid \<in> tids; finite tids\<rbrakk> \<Longrightarrow> plus2_inv tids (mainv_update Suc (threadv_update (point_update tid Suc) s)) = plus2_inv tids s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tid \<in> tids; finite tids\<rbrakk> \<Longrightarrow> (Suc (mainv s) = (\<Sum>x\<in>tids. if x = tid then Suc (threadv s tid) else threadv s x)) = (mainv s = sum (threadv s) tids) proof (prove)
goal:
No subgoals!
theory Plus2_Prefix

theorem plus2_x_property:
  "\<lbrace>\<lambda>s0 s. plus2_inv tids s \<and> threadv s tid = 0 \<and> s = s0 \<and> tid \<in> tids \<and> finite tids\<rbrace>,\<lbrace>plus2_rel tids {tid}\<rbrace>
    plus2_x tid \<lbrace>plus2_rel tids (- {tid})\<rbrace>,\<lbrace>\<lambda>_ _ s. plus2_inv tids s \<and> threadv s tid = 2\<rbrace>" apply (simp add: plus2_x_def) apply wpsimp apply (clarsimp simp: plus2_rel_def point_update_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. plus2_inv tids s \<and> threadv s tid = 0 \<and> s = s0 \<and> tid \<in> tids \<and> finite tids\<rbrace>, \<lbrace>plus2_rel tids {tid}\<rbrace> plus2_x tid \<lbrace>plus2_rel tids (- {tid})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv tids s \<and> threadv s tid = 2\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s0 s. plus2_inv tids s \<and> threadv s tid = 0 \<and> s = s0 \<and> tid \<in> tids \<and> finite tids\<rbrace>, \<lbrace>plus2_rel tids {tid}\<rbrace> do y <- env_steps;
y <- modify (mainv_update ((+) (Suc 0)) \<circ> threadv_update (point_update tid ((+) (Suc 0))));
y <- interference;
y <- modify (mainv_update ((+) (Suc 0)) \<circ> threadv_update (point_update tid ((+) (Suc 0))));
interference
od \<lbrace>plus2_rel tids (- {tid})\<rbrace>, \<lbrace>\<lambda>_ _ s. plus2_inv tids s \<and> threadv s tid = 2\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s0. \<lbrakk>plus2_inv tids s0; threadv s0 tid = 0; tid \<in> tids; finite tids\<rbrakk> \<Longrightarrow> (\<forall>s'. plus2_rel tids {tid} s0 s' \<longrightarrow> (\<forall>s'a. plus2_rel tids {tid} (mainv_update Suc (threadv_update (point_update tid Suc) s')) s'a \<longrightarrow> (\<forall>s'. plus2_rel tids {tid} (mainv_update Suc (threadv_update (point_update tid Suc) s'a)) s' \<longrightarrow> plus2_inv tids s' \<and> threadv s' tid = 2) \<and> plus2_rel tids (- {tid}) s'a (mainv_update Suc (threadv_update (point_update tid Suc) s'a))) \<and> plus2_rel tids (- {tid}) s' (mainv_update Suc (threadv_update (point_update tid Suc) s'))) \<and> (\<forall>s'. plus2_rel tids {tid} (mainv_update Suc (threadv_update (point_update tid Suc) s0)) s' \<longrightarrow> (\<forall>s'a. plus2_rel tids {tid} (mainv_update Suc (threadv_update (point_update tid Suc) s')) s'a \<longrightarrow> plus2_inv tids s'a \<and> threadv s'a tid = 2) \<and> plus2_rel tids (- {tid}) s' (mainv_update Suc (threadv_update (point_update tid Suc) s'))) \<and> plus2_rel tids (- {tid}) s0 (mainv_update Suc (threadv_update (point_update tid Suc) s0)) proof (prove)
goal:
No subgoals!
theory Plus2_Prefix

lemma env_stable:
  "env_stable AR R (\<lambda>s t. t = mainv s) (\<lambda>s t. t = mainv s) \<top>" apply (simp add: env_stable_def rely_stable_def env_rely_stable_iosr_def) apply (simp add: plus2_xstate.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. env_stable AR R (\<lambda>s t. t = mainv s) (\<lambda>s t. t = mainv s) (\<lambda>_. True) proof (prove)
goal (1 subgoal):
 1. \<forall>s t'. R (mainv s) t' \<longrightarrow> (\<exists>s'. t' = mainv s') proof (prove)
goal:
No subgoals!
theory Plus2_Prefix

theorem pfx_refn_plus2_x:
  "p_refn (\<top>\<top>) (=) (\<top>\<top>) AR R (plus2_x tid) plus2" apply (simp add: plus2_x_def plus2_def) apply (rule prefix_refinement_weaken_pre) apply (rule pfx_refn_bind prefix_refinement_interference
                prefix_refinement_env_steps pfx_refn_modifyT env_stable
           | wpsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pfx_refn (\<lambda>s t. t = mainv s) (\<lambda>_ _. True) (=) (\<lambda>_ _. True) AR R (plus2_x tid) plus2 proof (prove)
goal (1 subgoal):
 1. pfx_refn (\<lambda>s t. t = mainv s) (\<lambda>_ _. True) (=) (\<lambda>_ _. True) AR R (do y <- env_steps;
y <- modify (mainv_update ((+) (Suc 0)) \<circ> threadv_update (point_update tid ((+) (Suc 0))));
y <- interference;
y <- modify (mainv_update ((+) (Suc 0)) \<circ> threadv_update (point_update tid ((+) (Suc 0))));
interference
od) (do y <- env_steps;
y <- modify ((+) (Suc 0));
y <- interference;
y <- modify ((+) (Suc 0));
interference
od) proof (prove)
goal (3 subgoals):
 1. pfx_refn (\<lambda>s t. t = mainv s) (\<lambda>_ _. True) ?P'1 ?Q'1 AR R (do y <- env_steps;
y <- modify (mainv_update ((+) (Suc 0)) \<circ> threadv_update (point_update tid ((+) (Suc 0))));
y <- interference;
y <- modify (mainv_update ((+) (Suc 0)) \<circ> threadv_update (point_update tid ((+) (Suc 0))));
interference
od) (do y <- env_steps;
y <- modify ((+) (Suc 0));
y <- interference;
y <- modify ((+) (Suc 0));
interference
od)
 2. \<forall>s s0. s0 = s \<longrightarrow> ?P'1 s0 s
 3. \<forall>s t s0 t0. t = mainv s \<longrightarrow> t0 = mainv s0 \<longrightarrow> s0 = s \<longrightarrow> True \<longrightarrow> ?Q'1 t0 t proof (prove)
goal:
No subgoals!
theory Plus2_Prefix

lemma par_tr_fin_plus2_x:
  "par_tr_fin_principle (plus2_x tid)" by (simp add: plus2_x_def par_tr_fin_interference par_tr_fin_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. par_tr_fin_principle (plus2_x tid)
theory Plus2_Prefix

lemma prefix_closed_plus2:
  "prefix_closed plus2" apply (simp add: plus2_def) apply (rule validI_prefix_closed_T, wpsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix_closed plus2 proof (prove)
goal (1 subgoal):
 1. prefix_closed (do y <- env_steps;
y <- modify ((+) (Suc 0));
y <- interference;
y <- modify ((+) (Suc 0));
interference
od) proof (prove)
goal:
No subgoals!
theory Plus2_Prefix

theorem plus2_x_n_parallel:
  "n > 0 \<Longrightarrow>
  \<lbrace>\<lambda>s0 s. mainv s = 0 \<and> (\<forall>i < n. threadv s i = 0) \<and> s = s0\<rbrace>,\<lbrace>plus2_rel {..< n} {..< n}\<rbrace>
    fold parallel (map plus2_x [1 ..< n]) (plus2_x 0) \<lbrace>\<lambda>s0 s. True\<rbrace>,\<lbrace>\<lambda>_ _ s. mainv s = (n * 2)\<rbrace>" apply (rule rg_weaken_pre, rule rg_strengthen_post,
      rule rg_strengthen_guar, erule plus2_x_n_parallel_induct) apply simp apply simp apply (clarsimp simp: plus2_inv_def) apply (clarsimp simp: plus2_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> \<lbrace>\<lambda>s0 s. mainv s = 0 \<and> (\<forall>i<n. threadv s i = 0) \<and> s = s0\<rbrace>, \<lbrace>plus2_rel {..<n} {..<n}\<rbrace> fold Trace_Monad.parallel (map plus2_x [1..<n]) (plus2_x 0) -, \<lbrace>\<lambda>_ _ s. mainv s = n * 2\<rbrace> proof (prove)
goal (4 subgoals):
 1. n \<le> n
 2. \<And>s0 s. \<lbrakk>0 < n; plus2_rel {..<n} (- {..<n}) s0 s\<rbrakk> \<Longrightarrow> True
 3. \<And>v s0 s. \<lbrakk>0 < n; plus2_inv {..<n} s \<and> (\<forall>i<n. threadv s i = 2)\<rbrakk> \<Longrightarrow> mainv s = n * 2
 4. \<And>s0 s. \<lbrakk>0 < n; mainv s = 0 \<and> (\<forall>i<n. threadv s i = 0) \<and> s = s0\<rbrakk> \<Longrightarrow> plus2_inv {..<n} s \<and> (\<forall>i<n. threadv s i = 0) \<and> s = s0 proof (prove)
goal (3 subgoals):
 1. \<And>s0 s. \<lbrakk>0 < n; plus2_rel {..<n} (- {..<n}) s0 s\<rbrakk> \<Longrightarrow> True
 2. \<And>v s0 s. \<lbrakk>0 < n; plus2_inv {..<n} s \<and> (\<forall>i<n. threadv s i = 2)\<rbrakk> \<Longrightarrow> mainv s = n * 2
 3. \<And>s0 s. \<lbrakk>0 < n; mainv s = 0 \<and> (\<forall>i<n. threadv s i = 0) \<and> s = s0\<rbrakk> \<Longrightarrow> plus2_inv {..<n} s \<and> (\<forall>i<n. threadv s i = 0) \<and> s = s0 proof (prove)
goal (2 subgoals):
 1. \<And>v s0 s. \<lbrakk>0 < n; plus2_inv {..<n} s \<and> (\<forall>i<n. threadv s i = 2)\<rbrakk> \<Longrightarrow> mainv s = n * 2
 2. \<And>s0 s. \<lbrakk>0 < n; mainv s = 0 \<and> (\<forall>i<n. threadv s i = 0) \<and> s = s0\<rbrakk> \<Longrightarrow> plus2_inv {..<n} s \<and> (\<forall>i<n. threadv s i = 0) \<and> s = s0 proof (prove)
goal (1 subgoal):
 1. \<And>s0 s. \<lbrakk>0 < n; mainv s = 0 \<and> (\<forall>i<n. threadv s i = 0) \<and> s = s0\<rbrakk> \<Longrightarrow> plus2_inv {..<n} s \<and> (\<forall>i<n. threadv s i = 0) \<and> s = s0 proof (prove)
goal:
No subgoals!
theory Plus2_Prefix

lemma par_tr_fin_principle_parallel:
  "par_tr_fin_principle f \<Longrightarrow> par_tr_fin_principle g
    \<Longrightarrow> par_tr_fin_principle (parallel f g)" apply (subst par_tr_fin_principle_def, clarsimp simp: parallel_def3) apply (drule(1) par_tr_fin_principleD)+ apply (clarsimp simp: neq_Nil_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>par_tr_fin_principle f; par_tr_fin_principle g\<rbrakk> \<Longrightarrow> par_tr_fin_principle (Trace_Monad.parallel f g) proof (prove)
goal (1 subgoal):
 1. \<And>s s' a aa. \<lbrakk>par_tr_fin_principle f; par_tr_fin_principle g; (a, Result ((), s')) \<in> f s; (aa, Result ((), s')) \<in> g s; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) a aa\<rbrakk> \<Longrightarrow> s' = last_st_tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) a aa) s \<and> a \<noteq> [] \<and> aa \<noteq> [] proof (prove)
goal (1 subgoal):
 1. \<And>s s' a aa. \<lbrakk>(a, Result ((), s')) \<in> f s; (aa, Result ((), s')) \<in> g s; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) a aa; s' = last_st_tr a s \<and> a \<noteq> []; s' = last_st_tr aa s \<and> aa \<noteq> []\<rbrakk> \<Longrightarrow> s' = last_st_tr (map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) a aa) s \<and> a \<noteq> [] \<and> aa \<noteq> [] proof (prove)
goal:
No subgoals!
theory Plus2_Prefix

lemma fold_parallel_par_tr_fin_principle[where xs="rev xs" for xs, simplified]:
  "\<forall>x \<in> insert x (set xs). par_tr_fin_principle x
    \<Longrightarrow> par_tr_fin_principle (fold parallel (rev xs) x)" by (induct xs, simp_all add: par_tr_fin_principle_parallel)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>insert x (set xs). par_tr_fin_principle x \<Longrightarrow> par_tr_fin_principle (fold Trace_Monad.parallel (rev xs) x)
theory Plus2_Prefix

lemma fold_parallel_prefix_closed[where xs="rev xs" for xs, simplified]:
  "\<forall>x \<in> insert x (set xs). prefix_closed x
    \<Longrightarrow> prefix_closed (fold parallel (rev xs) x)" by (induct xs, simp_all add: prefix_closed_parallel)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>insert x (set xs). prefix_closed x \<Longrightarrow> prefix_closed (fold Trace_Monad.parallel (rev xs) x)
theory Local_Method_Tests

lemma "A \<Longrightarrow> B \<Longrightarrow> A \<or> B" supply_local_method my_simp = simp apply (local_method my_simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<or> B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<or> B proof (prove)
goal:
No subgoals!
theory Local_Method_Tests

lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" supply_local_method my_slightly_complicated_method = (rule conjI, assumption+) apply (local_method my_slightly_complicated_method) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B proof (prove)
goal:
No subgoals!
theory Local_Method_Tests

lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" supply_local_method my_rule = (rule conjI)
                        my_asm = assumption+ apply (local_method my_rule) apply (local_method my_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A
 2. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> B proof (prove)
goal:
No subgoals!
theory Local_Method_Tests

lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" supply_local_method foo = simp apply (fails \<open>local_method bar\<close>) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B
theory Local_Method_Tests

lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" apply (rule conjI) subgoal supply_local_method my_simp = simp apply (local_method my_simp) done apply (fails \<open>local_method my_simp\<close>) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A
 2. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A proof (prove)
goal:
No subgoals! proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> B
theory Local_Method_Tests

lemma "A \<Longrightarrow> B \<Longrightarrow> A \<and> B" supply_local_method magic = foo apply (local_method magic) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B\<rbrakk> \<Longrightarrow> A \<and> B proof (prove)
goal:
No subgoals!
theory TacticTutorial

lemma my_conj_commute: "(A \<and> B) = (B \<and> A)" apply (rule iffI) apply (rule conjI) apply (erule conjunct2) apply (erule conjunct1) apply (erule conjE) apply (rule conjI) apply assumption apply assumption done

\<comment> \<open>
  The goal of this exercise is *not* for you to have a deep and comprehensive
  understanding of every utility available to you that concerns ML tactic
  internals. The goal is for you to know the basics needed to understand the
  (somewhat sparse) documentation on tactics and how they work, and to not get
  too confused when you see them in the wild.

  However, if you *do* come up with an interesting example that demonstrates a
  principle really well, or you discover a cool and useful trick, feel free to
  add it here!
\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (A \<and> B) = (B \<and> A) proof (prove)
goal (2 subgoals):
 1. A \<and> B \<Longrightarrow> B \<and> A
 2. B \<and> A \<Longrightarrow> A \<and> B proof (prove)
goal (3 subgoals):
 1. A \<and> B \<Longrightarrow> B
 2. A \<and> B \<Longrightarrow> A
 3. B \<and> A \<Longrightarrow> A \<and> B proof (prove)
goal (2 subgoals):
 1. A \<and> B \<Longrightarrow> A
 2. B \<and> A \<Longrightarrow> A \<and> B proof (prove)
goal (1 subgoal):
 1. B \<and> A \<Longrightarrow> A \<and> B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B; A\<rbrakk> \<Longrightarrow> A \<and> B proof (prove)
goal (2 subgoals):
 1. \<lbrakk>B; A\<rbrakk> \<Longrightarrow> A
 2. \<lbrakk>B; A\<rbrakk> \<Longrightarrow> B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B; A\<rbrakk> \<Longrightarrow> B proof (prove)
goal:
No subgoals!
theory TacticTutorial

lemma "X \<or> Y \<Longrightarrow> A \<and> B" apply (erule disjE) apply (tactic \<open>resolve_tac @{context} @{thms conjI} 2\<close>) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. X \<or> Y \<Longrightarrow> A \<and> B proof (prove)
goal (2 subgoals):
 1. X \<Longrightarrow> A \<and> B
 2. Y \<Longrightarrow> A \<and> B proof (prove)
goal (3 subgoals):
 1. X \<Longrightarrow> A \<and> B
 2. Y \<Longrightarrow> A
 3. Y \<Longrightarrow> B