theory Bit_Comprehension_Int

lemma wf_set_bits_int_fun_upd [simp]:
  "wf_set_bits_int (f(n := b)) \<longleftrightarrow> wf_set_bits_int f" (is "?lhs \<longleftrightarrow> ?rhs") proof assume ?lhs then obtain n'
    where "(\<forall>n''\<ge>n'. \<not> (f(n := b)) n'') \<or> (\<forall>n''\<ge>n'. (f(n := b)) n'')" by(auto simp add: wf_set_bits_int_simps) hence "(\<forall>n''\<ge>max (Suc n) n'. \<not> f n'') \<or> (\<forall>n''\<ge>max (Suc n) n'. f n'')" by auto thus ?rhs by(auto simp only: wf_set_bits_int_simps) next assume ?rhs then obtain n' where "(\<forall>n''\<ge>n'. \<not> f n'') \<or> (\<forall>n''\<ge>n'. f n'')" (is "?wf f n'") by(auto simp add: wf_set_bits_int_simps) hence "?wf (f(n := b)) (max (Suc n) n')" by auto thus ?lhs by(auto simp only: wf_set_bits_int_simps) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wf_set_bits_int (f(n := b)) = wf_set_bits_int f proof (state)
goal (2 subgoals):
 1. wf_set_bits_int (f(n := b)) \<Longrightarrow> wf_set_bits_int f
 2. wf_set_bits_int f \<Longrightarrow> wf_set_bits_int (f(n := b)) proof (state)
this:
wf_set_bits_int (f(n := b))

goal (2 subgoals):
 1. wf_set_bits_int (f(n := b)) \<Longrightarrow> wf_set_bits_int f
 2. wf_set_bits_int f \<Longrightarrow> wf_set_bits_int (f(n := b)) proof (chain)
picking this:
wf_set_bits_int (f(n := b)) proof (prove)
using this:
wf_set_bits_int (f(n := b))

goal (1 subgoal):
 1. (\<And>n'. (\<forall>n''\<ge>n'. \<not> (f(n := b)) n'') \<or> (\<forall>n''\<ge>n'. (f(n := b)) n'') \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
(\<forall>n''\<ge>n'. \<not> (f(n := b)) n'') \<or> (\<forall>n''\<ge>n'. (f(n := b)) n'')

goal (2 subgoals):
 1. wf_set_bits_int (f(n := b)) \<Longrightarrow> wf_set_bits_int f
 2. wf_set_bits_int f \<Longrightarrow> wf_set_bits_int (f(n := b)) proof (prove)
using this:
(\<forall>n''\<ge>n'. \<not> (f(n := b)) n'') \<or> (\<forall>n''\<ge>n'. (f(n := b)) n'')

goal (1 subgoal):
 1. (\<forall>n''\<ge>max (Suc n) n'. \<not> f n'') \<or> (\<forall>n''\<ge>max (Suc n) n'. f n'') proof (state)
this:
(\<forall>n''\<ge>max (Suc n) n'. \<not> f n'') \<or> (\<forall>n''\<ge>max (Suc n) n'. f n'')

goal (2 subgoals):
 1. wf_set_bits_int (f(n := b)) \<Longrightarrow> wf_set_bits_int f
 2. wf_set_bits_int f \<Longrightarrow> wf_set_bits_int (f(n := b)) proof (prove)
using this:
(\<forall>n''\<ge>max (Suc n) n'. \<not> f n'') \<or> (\<forall>n''\<ge>max (Suc n) n'. f n'')

goal (1 subgoal):
 1. wf_set_bits_int f proof (state)
this:
wf_set_bits_int f

goal (1 subgoal):
 1. wf_set_bits_int f \<Longrightarrow> wf_set_bits_int (f(n := b)) proof (state)
goal (1 subgoal):
 1. wf_set_bits_int f \<Longrightarrow> wf_set_bits_int (f(n := b)) proof (state)
this:
wf_set_bits_int f

goal (1 subgoal):
 1. wf_set_bits_int f \<Longrightarrow> wf_set_bits_int (f(n := b)) proof (chain)
picking this:
wf_set_bits_int f proof (prove)
using this:
wf_set_bits_int f

goal (1 subgoal):
 1. (\<And>n'. (\<forall>n''\<ge>n'. \<not> f n'') \<or> (\<forall>n''\<ge>n'. f n'') \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
(\<forall>n''\<ge>n'. \<not> f n'') \<or> (\<forall>n''\<ge>n'. f n'')

goal (1 subgoal):
 1. wf_set_bits_int f \<Longrightarrow> wf_set_bits_int (f(n := b)) proof (prove)
using this:
(\<forall>n''\<ge>n'. \<not> f n'') \<or> (\<forall>n''\<ge>n'. f n'')

goal (1 subgoal):
 1. (\<forall>n''\<ge>max (Suc n) n'. \<not> (f(n := b)) n'') \<or> (\<forall>n''\<ge>max (Suc n) n'. (f(n := b)) n'') proof (state)
this:
(\<forall>n''\<ge>max (Suc n) n'. \<not> (f(n := b)) n'') \<or> (\<forall>n''\<ge>max (Suc n) n'. (f(n := b)) n'')

goal (1 subgoal):
 1. wf_set_bits_int f \<Longrightarrow> wf_set_bits_int (f(n := b)) proof (prove)
using this:
(\<forall>n''\<ge>max (Suc n) n'. \<not> (f(n := b)) n'') \<or> (\<forall>n''\<ge>max (Suc n) n'. (f(n := b)) n'')

goal (1 subgoal):
 1. wf_set_bits_int (f(n := b)) proof (state)
this:
wf_set_bits_int (f(n := b))

goal:
No subgoals!