kings-crown/FVELER_Isabelle huggingface dataset:
theory Distinct_Prop

lemma distinct_prop_nth:
  "\<lbrakk> distinct_prop P ls; n < n'; n' < length ls \<rbrakk> \<Longrightarrow> P (ls ! n) (ls ! n')" apply (induct ls arbitrary: n n'; simp) apply (case_tac n'; simp) apply (case_tac n; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_prop P ls; n < n'; n' < length ls\<rbrakk> \<Longrightarrow> P (ls ! n) (ls ! n') proof (prove)
goal (1 subgoal):
 1. \<And>a ls n n'. \<lbrakk>\<And>n n'. \<lbrakk>n < n'; n' < length ls\<rbrakk> \<Longrightarrow> P (ls ! n) (ls ! n'); (\<forall>y\<in>set ls. P a y) \<and> distinct_prop P ls; n < n'; n' < Suc (length ls)\<rbrakk> \<Longrightarrow> P ((a # ls) ! n) (ls ! (n' - Suc 0)) proof (prove)
goal (1 subgoal):
 1. \<And>a ls n n' nat. \<lbrakk>\<And>n n'. \<lbrakk>n < n'; n' < length ls\<rbrakk> \<Longrightarrow> P (ls ! n) (ls ! n'); (\<forall>y\<in>set ls. P a y) \<and> distinct_prop P ls; n < Suc nat; nat < length ls; n' = Suc nat\<rbrakk> \<Longrightarrow> P ((a # ls) ! n) (ls ! nat) proof (prove)
goal:
No subgoals!
theory WordSetup

lemma distinct_prop_enum_step:
  "\<lbrakk> \<And>x y. \<lbrakk> x \<le> stop div step; y \<le> stop div step; x \<noteq> y \<rbrakk> \<Longrightarrow> P (x * step) (y * step) \<rbrakk>
     \<Longrightarrow> distinct_prop P [0, step .e. stop]" apply (simp add: upto_enum_step_def distinct_prop_map) apply (rule distinct_prop_enum) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<le> stop div step; y \<le> stop div step; x \<noteq> y\<rbrakk> \<Longrightarrow> P (x * step) (y * step)) \<Longrightarrow> distinct_prop P [0 , step .e. stop] proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<le> stop div step; y \<le> stop div step; x \<noteq> y\<rbrakk> \<Longrightarrow> P (x * step) (y * step)) \<Longrightarrow> distinct_prop (\<lambda>x y. P (x * step) (y * step)) [0 .e. stop div step] proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>\<And>x y. \<lbrakk>x \<le> stop div step; y \<le> stop div step; x \<noteq> y\<rbrakk> \<Longrightarrow> P (x * step) (y * step); x \<le> stop div step; y \<le> stop div step; x \<noteq> y\<rbrakk> \<Longrightarrow> P (x * step) (y * step) proof (prove)
goal:
No subgoals!
theory Fun_Pred_Syntax

lemma pred_top_comp[simp]:
  "\<top> \<circ> f = \<top>" by (simp add: comp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>_. True) \<circ> f = (\<lambda>_. True)
theory Fun_Pred_Syntax

lemma pred_bot_comp[simp]:
  "\<bottom> \<circ> f = \<bottom>" by (simp add: comp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>_. False) \<circ> f = (\<lambda>_. False)
theory Fun_Pred_Syntax

lemma bipred_disj_op_eq[simp]:
  "reflp R \<Longrightarrow> ((=) or R) = R"
  "reflp R \<Longrightarrow> (R or (=)) = R" by (auto simp: reflp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (reflp R \<Longrightarrow> ((=) or R) = R) &&& (reflp R \<Longrightarrow> R\<^sup>=\<^sup>= = R)
theory Fun_Pred_Syntax

lemma bipred_le_true[simp]: "R \<le> \<top>\<top>" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R \<le> (\<lambda>_ _. True)
theory Fun_Pred_Syntax

lemma bipred_and_or_True[simp]:
  "(P or \<top>\<top>) = \<top>\<top>"
  "(\<top>\<top> or P) = \<top>\<top>"
  "(P and \<top>\<top>) = P"
  "(\<top>\<top> and P) = P" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((P or (\<lambda>_ _. True)) = (\<lambda>_ _. True) &&& ((\<lambda>_ _. True) or P) = (\<lambda>_ _. True)) &&& (P and (\<lambda>_ _. True)) = P &&& ((\<lambda>_ _. True) and P) = P
theory Fun_Pred_Syntax

lemma "(P and P) = P" for P :: "'a \<Rightarrow> bool" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P and P) = P
theory Fun_Pred_Syntax

lemma "(P and Q) = (Q and P)" for P :: "'a \<Rightarrow> 'b \<Rightarrow> bool" by (simp add: pred_conj_aci)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P and Q) = (Q and P)
theory Fun_Pred_Syntax

lemma "(P and Q) s t = (P s t \<and> Q s t)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P and Q) s t = (P s t \<and> Q s t)
theory Fun_Pred_Syntax

lemma "(P and not P) = \<bottom>" for P :: "'a \<Rightarrow> bool" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P and not P) = (\<lambda>_. False)
theory Fun_Pred_Syntax

lemma "(P and not P) = (\<lambda>_ _. \<bottom>)" for P :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> bool" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P and not P) = (\<lambda>_ _ _. False)
theory Fun_Pred_Syntax

lemma "(P and (\<lambda>_ _. \<bottom>)) = (\<lambda>_ _. \<bottom>)" by (simp flip: pred_bot_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P and (\<lambda>_ _ _. False)) = (\<lambda>_ _ _. False)
theory Monad_Lib

lemma fun_app_cong[fundef_cong]:
  "\<lbrakk> f x = f' x' \<rbrakk> \<Longrightarrow> (f $ x) = (f' $ x')" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f x = f' x' \<Longrightarrow> (f $ x) = (f' $ x')
theory Monad_Lib

lemma fun_app_apply_cong[fundef_cong]:
  "f x y = f' x' y' \<Longrightarrow> (f $ x) y = (f' $ x') y'" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f x y = f' x' y' \<Longrightarrow> (f $ x) y = (f' $ x') y'
theory Monad_Lib

lemma swp_apply[simp]: "swp f y x = f x y" by (simp add: swp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. swp f y x = f x y
theory Monad_Lib

lemma K_apply[simp]:
  "K x y = x" by (simp add: K_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. K x y = x
theory Monad_Lib

lemma o_const_simp[simp]:
  "(\<lambda>x. C) \<circ> f = (\<lambda>x. C)" by (simp add: o_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. C) \<circ> f = (\<lambda>x. C)
theory Monad_Lib

lemma zipWith_Nil[simp]:
  "zipWith f xs [] = []" unfolding zipWith_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zipWith f xs [] = [] proof (prove)
goal (1 subgoal):
 1. map2 f xs [] = []
theory Monad_Lib

lemma zipWith_nth:
  "\<lbrakk> n < min (length xs) (length ys) \<rbrakk> \<Longrightarrow> zipWith f xs ys ! n = f (xs ! n) (ys ! n)" unfolding zipWith_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < min (length xs) (length ys) \<Longrightarrow> zipWith f xs ys ! n = f (xs ! n) (ys ! n) proof (prove)
goal (1 subgoal):
 1. n < min (length xs) (length ys) \<Longrightarrow> map2 f xs ys ! n = f (xs ! n) (ys ! n)
theory Monad_Lib

lemma length_zipWith [simp]:
  "length (zipWith f xs ys) = min (length xs) (length ys)" unfolding zipWith_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (zipWith f xs ys) = min (length xs) (length ys) proof (prove)
goal (1 subgoal):
 1. length (map2 f xs ys) = min (length xs) (length ys)
theory Monad_Lib

lemma sum_all_ex[simp]:
  "(\<forall>a. x \<noteq> Inl a) = (\<exists>a. x = Inr a)"
  "(\<forall>a. x \<noteq> Inr a) = (\<exists>a. x = Inl a)" by (metis Inr_not_Inl sum.exhaust)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>a. x \<noteq> Inl a) = (\<exists>a. x = Inr a) &&& (\<forall>a. x \<noteq> Inr a) = (\<exists>a. x = Inl a)
theory Monad_Lib

lemma context_disjE:
  "\<lbrakk>P \<or> Q; P \<Longrightarrow> R; \<lbrakk>\<not>P; Q\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<or> Q; P \<Longrightarrow> R; \<lbrakk>\<not> P; Q\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Monad_Lib

lemma subst2:
  "\<lbrakk>s = t; u = v; P s u\<rbrakk> \<Longrightarrow> P t v" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s = t; u = v; P s u\<rbrakk> \<Longrightarrow> P t v
theory Nondet_Monad

lemma simpler_gets_def:
  "gets f = (\<lambda>s. ({(f s, s)}, False))" by (simp add: gets_def return_def bind_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets f = (\<lambda>s. ({(f s, s)}, False))
theory Nondet_Monad

lemma simpler_modify_def:
  "modify f = (\<lambda>s. ({((), f s)}, False))" by (simp add: modify_def bind_def get_def put_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify f = (\<lambda>s. ({((), f s)}, False))
theory Nondet_Monad

lemma bind_def':
  "(f >>= g) \<equiv>
       \<lambda>s. ({(r'', s''). \<exists>(r', s') \<in> fst (f s). (r'', s'') \<in> fst (g r' s') },
                     snd (f s) \<or> (\<exists>(r', s') \<in> fst (f s). snd (g r' s')))" by (rule eq_reflection)
     (auto simp add: bind_def split_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f >>= g \<equiv> \<lambda>s. ({(r'', s''). \<exists>(r', s')\<in>fst (f s). (r'', s'') \<in> fst (g r' s')}, snd (f s) \<or> (\<exists>(r', s')\<in>fst (f s). snd (g r' s')))
theory Nondet_Monad

lemma return_bind[simp]:
  "(return x >>= f) = f x" by (simp add: return_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. return x >>= f = f x
theory Nondet_Monad

lemma bind_return[simp]:
  "(m >>= return) = m" by (simp add: bind_def return_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m >>= return = m
theory Nondet_Monad

lemma bind_assoc:
  fixes m :: "('a,'b) nondet_monad"
  fixes f :: "'b \<Rightarrow> ('a,'c) nondet_monad"
  fixes g :: "'c \<Rightarrow> ('a,'d) nondet_monad"
  shows "(m >>= f) >>= g  =  m >>= (\<lambda>x. f x >>= g)" unfolding bind_def Let_def split_def by (auto intro: rev_image_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m >>= f >>= g = m >>= (\<lambda>x. f x >>= g) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. (\<Union> (fst ` (\<lambda>p. g (fst p) (snd p)) ` fst (\<Union> (fst ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s)), True \<in> snd ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s) \<or> snd (m s))), True \<in> snd ` (\<lambda>p. g (fst p) (snd p)) ` fst (\<Union> (fst ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s)), True \<in> snd ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s) \<or> snd (m s)) \<or> snd (\<Union> (fst ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s)), True \<in> snd ` (\<lambda>p. f (fst p) (snd p)) ` fst (m s) \<or> snd (m s)))) = (\<lambda>s. (\<Union> (fst ` (\<lambda>p. (\<Union> (fst ` (\<lambda>p. g (fst p) (snd p)) ` fst (f (fst p) (snd p))), True \<in> snd ` (\<lambda>p. g (fst p) (snd p)) ` fst (f (fst p) (snd p)) \<or> snd (f (fst p) (snd p)))) ` fst (m s)), True \<in> snd ` (\<lambda>p. (\<Union> (fst ` (\<lambda>p. g (fst p) (snd p)) ` fst (f (fst p) (snd p))), True \<in> snd ` (\<lambda>p. g (fst p) (snd p)) ` fst (f (fst p) (snd p)) \<or> snd (f (fst p) (snd p)))) ` fst (m s) \<or> snd (m s)))
theory Nondet_Monad

lemma liftE_def2:
  "liftE f = (\<lambda>s. ((\<lambda>(v,s'). (Inr v, s')) ` fst (f s), snd (f s)))" by (auto simp: liftE_def return_def split_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE f = (\<lambda>s. ((\<lambda>(v, s'). (Inr v, s')) ` fst (f s), snd (f s)))
theory Nondet_Monad

lemma returnOk_bindE[simp]: "(returnOk x >>=E f) = f x" unfolding bindE_def returnOk_def by (clarsimp simp: lift_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. returnOk x >>=E f = f x proof (prove)
goal (1 subgoal):
 1. (return \<circ> Inr) x >>= lift f = f x
theory Nondet_Monad

lemma lift_return[simp]:
  "lift (return \<circ> Inr) = return" by (auto simp: lift_def throwError_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lift (return \<circ> Inr) = return
theory Nondet_Monad

lemma bindE_returnOk[simp]:
  "(m >>=E returnOk) = m" by (simp add: bindE_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m >>=E returnOk = m
theory Nondet_Monad

lemma bindE_assoc:
  "(m >>=E f) >>=E g = m >>=E (\<lambda>x. f x >>=E g)" unfolding bindE_def by (fastforce simp: bind_assoc lift_def throwError_def
                split: sum.splits
                intro: arg_cong[where f="\<lambda>x. m >>= x"])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m >>=E f >>=E g = m >>=E (\<lambda>x. f x >>=E g) proof (prove)
goal (1 subgoal):
 1. m >>= lift f >>= lift g = m >>= lift (\<lambda>x. f x >>= lift g)
theory Nondet_Monad

lemma returnOk_liftE:
  "returnOk x = liftE (return x)" by (simp add: liftE_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. returnOk x = liftE (return x)
theory Nondet_Monad

lemma throwError_bindE[simp]:
  "(throwError E >>=E f) = throwError E" by (simp add: bindE_def bind_def throwError_def lift_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. throwError E >>=E f = throwError E
theory Nondet_Monad

lemma "do x \<leftarrow> return 1;
          return (2::nat);
          return x
       od =
       return 1 >>=
       (\<lambda>x. return (2::nat) >>=
            K_bind (return x))" by (rule refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- return (1::'b);
return 2;
return x
od = do x <- return (1::'b);
return 2;
return x
od
theory Nondet_Monad

lemma "do x \<leftarrow> return 1;
          return 2;
          return x
       od = return 1" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- return (1::'b);
return (2::'c);
return x
od = return (1::'b)
theory Nondet_Monad

lemma "doE x \<leftarrow> returnOk 1;
           returnOk (2::nat);
           returnOk x
       odE =
       returnOk 1 >>=E
       (\<lambda>x. returnOk (2::nat) >>=E
            K_bind (returnOk x))" by (rule refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doE x <- returnOk (1::'c);
returnOk 2;
returnOk x
odE = doE x <- returnOk (1::'c);
returnOk 2;
returnOk x
odE
theory Nondet_Monad

lemma state_select_def2:
  "state_select r \<equiv> (do
    s \<leftarrow> get;
    S \<leftarrow> return {s'. (s, s') \<in> r};
    assert (S \<noteq> {});
    s' \<leftarrow> select S;
    put s'
  od)" apply (clarsimp simp add: state_select_def get_def return_def assert_def fail_def select_def
                            put_def bind_def fun_eq_iff
                    intro!: eq_reflection) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_select r \<equiv> do s <- get;
S <- return {s'. (s, s') \<in> r};
assert (S \<noteq> {});
select S >>= put
od proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (x, xa) \<in> r \<Longrightarrow> Pair () ` {s'. (x, s') \<in> r} = (\<Union>a\<in>{s'. (x, s') \<in> r} \<times> {x}. fst (case a of (s', uu_) \<Rightarrow> ({((), s')}, False))) proof (prove)
goal:
No subgoals!
theory Trace_Schematic_Insts

lemma rule_add:
  "PROP P \<equiv> (container True xs \<Longrightarrow> PROP P)" by (simp add: container_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. PROP P \<equiv> (container True xs \<Longrightarrow> PROP P)
theory Trace_Schematic_Insts

lemma rule_remove:
  "(container True xs \<Longrightarrow> PROP P) \<equiv> PROP P" by (simp add: container_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (container True xs \<Longrightarrow> PROP P) \<equiv> PROP P
theory Trace_Schematic_Insts

lemma elim:
  "container a b" by (simp add: container_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. container a b
theory WP_Pre

lemma test_wp_pre_pre[wp_pre]:
  "test_wp_pre P' Q \<Longrightarrow> (P \<Longrightarrow> P')
    \<Longrightarrow> test_wp_pre P Q" by (simp add: test_wp_pre_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>test_wp_pre P' Q; P \<Longrightarrow> P'\<rbrakk> \<Longrightarrow> test_wp_pre P Q
theory Datatype_Schematic

lemma wrap_ds_id:
  "x = ds_id x" by (simp add: ds_id_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x = ds_id x
theory Datatype_Schematic

lemma handles_nested_constructors:
  "\<exists>f. \<forall>y. f True (Some [x, (y, z)]) = y" apply (rule exI, rule allI) apply datatype_schem apply (rule refl) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>f. \<forall>y. f True (Some [x, (y, z)]) = y proof (prove)
goal (1 subgoal):
 1. \<And>y. ?f True (Some [x, (y, z)]) = y proof (prove)
goal (1 subgoal):
 1. \<And>y. ?f7 y (y, z) [(y, z)] [x, (y, z)] (ds_id True) (Some [x, (y, z)]) = y proof (prove)
goal:
No subgoals!
theory Datatype_Schematic

lemma selectively_exposing_datatype_arugments:
  notes get_basic_0.simps[datatype_schematic]
  shows "\<exists>x. \<forall>a b. x (basic a b) = a" apply (rule exI, (rule allI)+) apply datatype_schem \<comment> \<open>Only exposes @{text a} to the schematic.\<close> by (rule refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x. \<forall>a b. x (basic a b) = a proof (prove)
goal (1 subgoal):
 1. \<And>a b. ?x (basic a b) = a proof (prove)
goal (1 subgoal):
 1. \<And>a b. ?x6 a (basic a b) = a
theory Datatype_Schematic

lemma method_handles_primrecs_with_two_constructors:
  shows "\<exists>x. \<forall>a b. x (basic a b) = a" apply (rule exI, (rule allI)+) apply (datatype_schem add: get_nat.simps) by (rule refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x. \<forall>a b. x (basic a b) = a proof (prove)
goal (1 subgoal):
 1. \<And>a b. ?x (basic a b) = a proof (prove)
goal (1 subgoal):
 1. \<And>a b. ?x6 a (basic a b) = a
theory Strengthen

lemma failedI:
  "<strg-failed>" by (simp add: failed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. <strg-failed>
theory Strengthen

lemma strengthen_refl:
  "st P rel x x" by (simp add: st_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st P rel x x
theory Strengthen

lemma st_prop_refl:
  "PROP (st_prop1 (PROP P) (PROP P))"
  "PROP (st_prop2 (PROP P) (PROP P))" unfolding st_prop1_def st_prop2_def by safe

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_prop1 PROP P PROP P &&& st_prop2 PROP P PROP P proof (prove)
goal (1 subgoal):
 1. (PROP P \<Longrightarrow> PROP P) &&& (PROP P \<Longrightarrow> PROP P)
theory Strengthen

lemma strengthenI:
  "rel x y \<Longrightarrow> st True rel x y"
  "rel y x \<Longrightarrow> st False rel x y" by (simp_all add: st_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rel x y \<Longrightarrow> st True rel x y) &&& (rel y x \<Longrightarrow> st False rel x y)
theory Strengthen

lemma use_strengthen_imp:
  "st False (\<longrightarrow>) Q P \<Longrightarrow> P \<Longrightarrow> Q" by (simp add: st_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Q =strg<--|=> P; P\<rbrakk> \<Longrightarrow> Q
theory Strengthen

lemma use_strengthen_prop_elim:
  "PROP P \<Longrightarrow> PROP (st_prop2 (PROP P) (PROP Q))
    \<Longrightarrow> (PROP Q \<Longrightarrow> PROP R) \<Longrightarrow> PROP R" unfolding st_prop2_def apply (drule(1) meta_mp)+ apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PROP P; st_prop2 PROP P PROP Q; PROP Q \<Longrightarrow> PROP R\<rbrakk> \<Longrightarrow> PROP R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PROP P; PROP P \<Longrightarrow> PROP Q; PROP Q \<Longrightarrow> PROP R\<rbrakk> \<Longrightarrow> PROP R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PROP P; PROP Q; PROP R\<rbrakk> \<Longrightarrow> PROP R proof (prove)
goal:
No subgoals!
theory Strengthen

lemma strengthen_Not:
  "st False rel x y \<Longrightarrow> st (\<not> True) rel x y"
  "st True rel x y \<Longrightarrow> st (\<not> False) rel x y" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (st False rel x y \<Longrightarrow> st (\<not> True) rel x y) &&& (st True rel x y \<Longrightarrow> st (\<not> False) rel x y)
theory Strengthen

lemma mk_True_imp:
  "P \<equiv> True \<longrightarrow> P" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P \<equiv> True \<longrightarrow> P
theory Strengthen

lemma narrow_quant:
  "(\<And>x. PROP P \<Longrightarrow> PROP (Q x)) \<equiv> (PROP P \<Longrightarrow> (\<And>x. PROP (Q x)))"
  "(\<And>x. (R \<longrightarrow> S x)) \<equiv> PROP (Trueprop (R \<longrightarrow> (\<forall>x. S x)))"
  "(\<And>x. (S x \<longrightarrow> R)) \<equiv> PROP (Trueprop ((\<exists>x. S x) \<longrightarrow> R))" apply (simp_all add: atomize_all) apply rule apply assumption apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<And>x. PROP P \<Longrightarrow> PROP Q x) \<equiv> (PROP P \<Longrightarrow> (\<And>x. PROP Q x))) &&& ((\<And>x. R \<longrightarrow> S x) \<equiv> R \<longrightarrow> (\<forall>x. S x)) &&& (\<And>x. S x \<longrightarrow> R) \<equiv> (\<exists>x. S x) \<longrightarrow> R proof (prove)
goal (1 subgoal):
 1. (\<And>x. PROP P \<Longrightarrow> PROP Q x) \<equiv> (PROP P \<Longrightarrow> (\<And>x. PROP Q x)) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>\<And>x. PROP P \<Longrightarrow> PROP Q x; PROP P\<rbrakk> \<Longrightarrow> PROP Q x
 2. \<And>x. \<lbrakk>\<And>x. PROP P \<Longrightarrow> PROP Q x; PROP P\<rbrakk> \<Longrightarrow> PROP Q x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>x. PROP P \<Longrightarrow> PROP Q x; PROP P\<rbrakk> \<Longrightarrow> PROP Q x proof (prove)
goal:
No subgoals!
theory Strengthen

lemma do_elim:
  "PROP P \<Longrightarrow> PROP elim (PROP P)" by (simp add: elim_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. PROP P \<Longrightarrow> {elim| PROP P |}
theory Strengthen

lemma intro_oblig:
  "PROP P \<Longrightarrow> PROP oblig (PROP P)" by (simp add: oblig_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. PROP P \<Longrightarrow> {oblig| PROP P |}
theory Strengthen

lemma strengthen_imp_imp[simp]:
  "st True (\<longrightarrow>) A B = (A \<longrightarrow> B)"
  "st False (\<longrightarrow>) A B = (B \<longrightarrow> A)" by (simp_all add: st_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A =strg-->|=> B = (A \<longrightarrow> B) &&& A =strg<--|=> B = (B \<longrightarrow> A)
theory Strengthen

lemma strengthen_imp_ord[simp]:
  "st_ord True A B = (A \<le> B)"
  "st_ord False A B = (B \<le> A)" by (auto simp add: st_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A =strg>=|=> B = (A \<le> B) &&& A =strg<=|=> B = (B \<le> A)
theory Strengthen

lemma strengthen_imp_conj [strg]:
  "\<lbrakk> A' \<Longrightarrow> st F (\<longrightarrow>) B B'; B \<Longrightarrow> st F (\<longrightarrow>) A A' \<rbrakk>
    \<Longrightarrow> st F (\<longrightarrow>) (A \<and> B) (A' \<and> B')" by (cases F, auto)

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

lemma strengthen_imp_disj [strg]:
  "\<lbrakk> \<not> A' \<Longrightarrow> st F (\<longrightarrow>) B B'; \<not> B \<Longrightarrow> st F (\<longrightarrow>) A A' \<rbrakk>
    \<Longrightarrow> st F (\<longrightarrow>) (A \<or> B) (A' \<or> B')" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> A' \<Longrightarrow> st F (\<longrightarrow>) B B'; \<not> B \<Longrightarrow> st F (\<longrightarrow>) A A'\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) (A \<or> B) (A' \<or> B')
theory Strengthen

lemma strengthen_imp_implies [strg]:
  "\<lbrakk> st (\<not> F) (\<longrightarrow>) X X'; X \<Longrightarrow> st F (\<longrightarrow>) Y Y' \<rbrakk>
    \<Longrightarrow> st F (\<longrightarrow>) (X \<longrightarrow> Y) (X' \<longrightarrow> Y')" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st (\<not> F) (\<longrightarrow>) X X'; X \<Longrightarrow> st F (\<longrightarrow>) Y Y'\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) (X \<longrightarrow> Y) (X' \<longrightarrow> Y')
theory Strengthen

lemma strengthen_all[strg]:
  "\<lbrakk> \<And>x. st F (\<longrightarrow>) (P x) (Q x) \<rbrakk>
    \<Longrightarrow> st F (\<longrightarrow>) (\<forall>x. P x) (\<forall>x. Q x)" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. st F (\<longrightarrow>) (P x) (Q x)) \<Longrightarrow> st F (\<longrightarrow>) (\<forall>x. P x) (\<forall>x. Q x)