[STATEMENT]
lemma i_Exec_Stream_Acc_LocalState__State_Idle_all[rule_format]: "
  \<lbrakk> 0 < l; l \<le> k;
    State_Idle localState output_fun trans_fun (localState c);
    \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow>
      State_Idle localState output_fun trans_fun (
        localState (f_Exec_Comp trans_fun (m # \<NoMsg>\<^bsup>l - Suc 0\<^esup>) c)) \<rbrakk> \<Longrightarrow>
  State_Idle localState output_fun trans_fun (
    i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c i)
[PROOF STEP]
apply (simp only: i_Exec_Stream_Acc_LocalState_nth_f_nth)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun (xs \<Down> Suc i) c ! i)
[PROOF STEP]
apply (rule f_Exec_Stream_Acc_LocalState__State_Idle_all)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> 0 < ?l8
 2. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> ?l8 \<le> k
 3. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState c)
 4. \<And>ca m. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); State_Idle localState output_fun trans_fun (localState ca)\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>?l8 - Suc 0\<^esup>) ca))
 5. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> i < length (xs \<Down> Suc i)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ca m. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); \<forall>c. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> (\<forall>m. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m c)))); State_Idle localState output_fun trans_fun (localState ca)\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m ca)))
[PROOF STEP]
apply (rename_tac c' m, drule_tac x=c' in spec)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c' m. \<lbrakk>0 < l; l \<le> k; State_Idle localState output_fun trans_fun (localState c); State_Idle localState output_fun trans_fun (localState c'); State_Idle localState output_fun trans_fun (localState c') \<longrightarrow> (\<forall>m. State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m c'))))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun NoMsg\<^bsup>l - Suc 0\<^esup> (trans_fun m c')))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_Acc_Output__State_Idle_all_imp_eq[rule_format]: "
  \<lbrakk> 0 < l; l \<le> k; Exec_Equal_State localState trans_fun;
    State_Idle localState output_fun trans_fun (localState c);
    \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow>
      State_Idle localState output_fun trans_fun (
        localState (f_Exec_Comp trans_fun (m # \<NoMsg>\<^bsup>l - Suc 0\<^esup>) c)) \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c =
  f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun xs c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_Output k output_fun trans_fun xs c = f_Exec_Comp_Stream_Acc_Output l output_fun trans_fun xs c
[PROOF STEP]
apply (rule f_Exec_Stream_Acc_Output__State_Idle_eq, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); n < length xs\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n)
[PROOF STEP]
apply (simp add: f_Exec_Stream_Acc_LocalState__State_Idle_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Exec_Stream_Acc_Output__State_Idle_all_imp_eq[rule_format]: "
  \<lbrakk> 0 < l; l \<le> k; Exec_Equal_State localState trans_fun;
    State_Idle localState output_fun trans_fun (localState c);
    \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow>
      State_Idle localState output_fun trans_fun (
        localState (f_Exec_Comp trans_fun (m # \<NoMsg>\<^bsup>l - Suc 0\<^esup>) c)) \<rbrakk> \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c =
  i_Exec_Comp_Stream_Acc_Output l output_fun trans_fun input c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream_Acc_Output k output_fun trans_fun input c = i_Exec_Comp_Stream_Acc_Output l output_fun trans_fun input c
[PROOF STEP]
apply (rule i_Exec_Stream_Acc_Output__State_Idle_eq, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun input c n)
[PROOF STEP]
apply (simp add: i_Exec_Stream_Acc_LocalState__State_Idle_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_Stream_Acc_LocalState__State_Idle_all_imp_eq[rule_format]: "
  \<lbrakk> 0 < l; l \<le> k; Exec_Equal_State localState trans_fun;
    State_Idle localState output_fun trans_fun (localState c);
    \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow>
      State_Idle localState output_fun trans_fun (
        localState (f_Exec_Comp trans_fun (m # \<NoMsg>\<^bsup>l - Suc 0\<^esup>) c)) \<rbrakk> \<Longrightarrow>
  f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c =
  f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> f_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c = f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c
[PROOF STEP]
apply (rule f_Exec_Stream_Acc_LocalState__State_Idle_eq, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); n < length xs\<rbrakk> \<Longrightarrow> State_Idle localState ?output_fun trans_fun (f_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c ! n)
[PROOF STEP]
apply (rule f_Exec_Stream_Acc_LocalState__State_Idle_all)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); n < length xs\<rbrakk> \<Longrightarrow> 0 < ?l5 n
 2. \<And>n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); n < length xs\<rbrakk> \<Longrightarrow> ?l5 n \<le> l
 3. \<And>n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); n < length xs\<rbrakk> \<Longrightarrow> State_Idle localState ?output_fun trans_fun (localState c)
 4. \<And>n ca m. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); n < length xs; State_Idle localState ?output_fun trans_fun (localState ca)\<rbrakk> \<Longrightarrow> State_Idle localState ?output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>?l5 n - Suc 0\<^esup>) ca))
 5. \<And>n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); n < length xs\<rbrakk> \<Longrightarrow> n < length xs
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma i_Exec_Stream_Acc_LocalState__State_Idle_all_imp_eq[rule_format]: "
  \<lbrakk> 0 < l; l \<le> k; Exec_Equal_State localState trans_fun;
    State_Idle localState output_fun trans_fun (localState c);
    \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow>
      State_Idle localState output_fun trans_fun (
        localState (f_Exec_Comp trans_fun (m # \<NoMsg>\<^bsup>l - Suc 0\<^esup>) c)) \<rbrakk> \<Longrightarrow>
  i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c =
  i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> i_Exec_Comp_Stream_Acc_LocalState k localState trans_fun xs c = i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c
[PROOF STEP]
apply (rule i_Exec_Stream_Acc_LocalState__State_Idle_eq, assumption+)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState ?output_fun trans_fun (i_Exec_Comp_Stream_Acc_LocalState l localState trans_fun xs c n)
[PROOF STEP]
apply (rule i_Exec_Stream_Acc_LocalState__State_Idle_all)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> 0 < ?l5 n
 2. \<And>n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> ?l5 n \<le> l
 3. \<And>n. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c))\<rbrakk> \<Longrightarrow> State_Idle localState ?output_fun trans_fun (localState c)
 4. \<And>n ca m. \<lbrakk>0 < l; l \<le> k; Exec_Equal_State localState trans_fun; State_Idle localState output_fun trans_fun (localState c); \<forall>c m. State_Idle localState output_fun trans_fun (localState c) \<longrightarrow> State_Idle localState output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>l - Suc 0\<^esup>) c)); State_Idle localState ?output_fun trans_fun (localState ca)\<rbrakk> \<Longrightarrow> State_Idle localState ?output_fun trans_fun (localState (f_Exec_Comp trans_fun (m # NoMsg\<^bsup>?l5 n - Suc 0\<^esup>) ca))
[PROOF STEP]
apply simp+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma f_Exec_input_map: "\<And>c.
  f_Exec_Comp trans_fun (map f xs) c = f_Exec_Comp (trans_fun \<circ> f) xs c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>c. f_Exec_Comp trans_fun (map f xs) c = f_Exec_Comp (trans_fun \<circ> f) xs c
[PROOF STEP]
by (induct xs, simp+)


[STATEMENT]
lemma f_Exec_Stream_input_map: "
  f_Exec_Comp_Stream trans_fun (map f xs) c =
  f_Exec_Comp_Stream (trans_fun \<circ> f) xs c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f_Exec_Comp_Stream trans_fun (map f xs) c = f_Exec_Comp_Stream (trans_fun \<circ> f) xs c
[PROOF STEP]
by (simp add: list_eq_iff f_Exec_Stream_nth take_map f_Exec_input_map)


[STATEMENT]
lemma i_Exec_Stream_input_map: "
  i_Exec_Comp_Stream trans_fun (f \<circ> input) c =
  i_Exec_Comp_Stream (trans_fun \<circ> f) input c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i_Exec_Comp_Stream trans_fun (f \<circ> input) c = i_Exec_Comp_Stream (trans_fun \<circ> f) input c
[PROOF STEP]
by (simp add: ilist_eq_iff i_Exec_Stream_nth f_Exec_input_map)


[STATEMENT]
lemma make_map_transfer[transfer_rule]: "(rel_fset (=) ===> A ===> rel_map A) make_map make_map"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_fset (=) ===> A ===> rel_map A) make_map make_map
[PROOF STEP]
unfolding make_map_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_fset (=) ===> A ===> rel_map A) (\<lambda>ks v k. if k \<in> fset ks then Some v else None) (\<lambda>ks v k. if k \<in> fset ks then Some v else None)
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma dom_make_map:
  "dom (make_map ks v) = fset ks"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (make_map ks v) = fset ks
[PROOF STEP]
by (metis domIff make_map_def not_Some_eq set_eqI)


[STATEMENT]
lemma make_fmap_empty[simp]: "[ {||} |=> f ] = fmempty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [ {||} |=> f ] = fmempty
[PROOF STEP]
by transfer (simp add: make_map_def)


[STATEMENT]
lemma fmap_add_commute:
  assumes "fmdom A |\<inter>| fmdom B = {||}"
  shows "A ++\<^sub>f B = B ++\<^sub>f A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A ++\<^sub>f B = B ++\<^sub>f A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
fmdom A |\<inter>| fmdom B = {||}

goal (1 subgoal):
 1. A ++\<^sub>f B = B ++\<^sub>f A
[PROOF STEP]
including fset.lifting
[PROOF STATE]
proof (prove)
using this:
fmdom A |\<inter>| fmdom B = {||}

goal (1 subgoal):
 1. A ++\<^sub>f B = B ++\<^sub>f A
[PROOF STEP]
apply (transfer)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A B. \<lbrakk>finite (dom A); finite (dom B); dom A \<inter> dom B = {}\<rbrakk> \<Longrightarrow> A ++ B = B ++ A
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A B x. \<lbrakk>finite (dom A); finite (dom B); dom A \<inter> dom B = {}\<rbrakk> \<Longrightarrow> (A ++ B) x = (B ++ A) x
[PROOF STEP]
apply (auto simp: dom_def map_add_def split: option.splits)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma make_fmap_union:
  "[ xs |=> v ] ++\<^sub>f [ ys |=> v] = [ xs |\<union>| ys |=> v ]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [ xs |=> v ] ++\<^sub>f [ ys |=> v ] = [ xs |\<union>| ys |=> v ]
[PROOF STEP]
by (transfer, auto simp add: make_map_def map_add_def)


[STATEMENT]
lemma fdom_make_fmap: "fmdom [ ks |=> v ] = ks"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmdom [ ks |=> v ] = ks
[PROOF STEP]
(* FIXME proper transfer proof *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fmdom [ ks |=> v ] = ks
[PROOF STEP]
apply (subst fmdom_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fmlookup ---> Abs_fset) dom [ ks |=> v ] = ks
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ks v. ((\<lambda>x. x) ---> Abs_fset) dom (make_map ks v) = ks
[PROOF STEP]
apply (auto simp: dom_def make_map_def fset_inverse)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lookup_make_fmap:
  assumes "k \<in> fset ks"
  shows "lookup [ ks |=> v ] k = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup [ ks |=> v ] k = v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k \<in> fset ks

goal (1 subgoal):
 1. lookup [ ks |=> v ] k = v
[PROOF STEP]
by (transfer, simp add: make_map_def)


[STATEMENT]
lemma lookup_make_fmap1:
  "lookup [ {|k|} |=> v ] k = v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup [ {|k|} |=> v ] k = v
[PROOF STEP]
by (metis finsert.rep_eq insert_iff lookup_make_fmap)


[STATEMENT]
lemma lookup_union1:
  assumes "k |\<in>| fmdom ys"
  shows "lookup (xs ++\<^sub>f ys) k = lookup ys k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (xs ++\<^sub>f ys) k = lookup ys k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k |\<in>| fmdom ys

goal (1 subgoal):
 1. lookup (xs ++\<^sub>f ys) k = lookup ys k
[PROOF STEP]
including fset.lifting
[PROOF STATE]
proof (prove)
using this:
k |\<in>| fmdom ys

goal (1 subgoal):
 1. lookup (xs ++\<^sub>f ys) k = lookup ys k
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma lookup_union2:
  assumes "k |\<notin>| fmdom ys"
  shows "lookup (xs ++\<^sub>f ys) k = lookup xs k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (xs ++\<^sub>f ys) k = lookup xs k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k |\<notin>| fmdom ys

goal (1 subgoal):
 1. lookup (xs ++\<^sub>f ys) k = lookup xs k
[PROOF STEP]
including fset.lifting
[PROOF STATE]
proof (prove)
using this:
k |\<notin>| fmdom ys

goal (1 subgoal):
 1. lookup (xs ++\<^sub>f ys) k = lookup xs k
[PROOF STEP]
by transfer (auto simp: map_add_def split: option.splits)


[STATEMENT]
lemma lookup_union3:
  assumes "k |\<notin>| fmdom xs"
  shows "lookup (xs ++\<^sub>f ys) k = lookup ys k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (xs ++\<^sub>f ys) k = lookup ys k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k |\<notin>| fmdom xs

goal (1 subgoal):
 1. lookup (xs ++\<^sub>f ys) k = lookup ys k
[PROOF STEP]
including fset.lifting
[PROOF STATE]
proof (prove)
using this:
k |\<notin>| fmdom xs

goal (1 subgoal):
 1. lookup (xs ++\<^sub>f ys) k = lookup ys k
[PROOF STEP]
by transfer (auto simp: map_add_def split: option.splits)


[STATEMENT]
lemma int_times_rat_code[code abstract]: "quotient_of (int_times_rat i x) =
  (case quotient_of x of (n,d) \<Rightarrow> Rat.normalize (i * n, d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quotient_of (int_times_rat i x) = (case quotient_of x of (n, d) \<Rightarrow> Rat.normalize (i * n, d))
[PROOF STEP]
unfolding int_times_rat_def rat_times_code
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (let (a, c) = quotient_of (rat_of_int i); (b, d) = quotient_of x in Rat.normalize (a * b, c * d)) = (case quotient_of x of (n, d) \<Rightarrow> Rat.normalize (i * n, d))
[PROOF STEP]
by auto


[STATEMENT]
lemma quotient_of_square: assumes "quotient_of x = (a,b)"
  shows "quotient_of (x * x) = (a * a, b * b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quotient_of (x * x) = (a * a, b * b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. quotient_of (x * x) = (a * a, b * b)
[PROOF STEP]
have b0: "b > 0" "b \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < b &&& b \<noteq> 0
[PROOF STEP]
using quotient_of_denom_pos[OF assms]
[PROOF STATE]
proof (prove)
using this:
0 < b

goal (1 subgoal):
 1. 0 < b &&& b \<noteq> 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < b
b \<noteq> 0

goal (1 subgoal):
 1. quotient_of (x * x) = (a * a, b * b)
[PROOF STEP]
hence b: "(b * b > 0) = True"
[PROOF STATE]
proof (prove)
using this:
0 < b
b \<noteq> 0

goal (1 subgoal):
 1. (0 < b * b) = True
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0 < b * b) = True

goal (1 subgoal):
 1. quotient_of (x * x) = (a * a, b * b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quotient_of (x * x) = (a * a, b * b)
[PROOF STEP]
unfolding rat_times_code assms Let_def split Rat.normalize_def fst_conv snd_conv b if_True
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a * a div gcd (a * a) (b * b), b * b div gcd (a * a) (b * b)) = (a * a, b * b)
[PROOF STEP]
using quotient_of_coprime[OF assms] b0
[PROOF STATE]
proof (prove)
using this:
algebraic_semidom_class.coprime a b
0 < b
b \<noteq> 0

goal (1 subgoal):
 1. (a * a div gcd (a * a) (b * b), b * b div gcd (a * a) (b * b)) = (a * a, b * b)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
quotient_of (x * x) = (a * a, b * b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma square_rat_code[code abstract]: "quotient_of (square_rat x) = (case quotient_of x of (n,d)
  \<Rightarrow> (n * n, d * d))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. quotient_of (square_rat x) = (case quotient_of x of (n, d) \<Rightarrow> (n * n, d * d))
[PROOF STEP]
using quotient_of_square[of x]
[PROOF STATE]
proof (prove)
using this:
quotient_of x = (?a, ?b) \<Longrightarrow> quotient_of (x * x) = (?a * ?a, ?b * ?b)

goal (1 subgoal):
 1. quotient_of (square_rat x) = (case quotient_of x of (n, d) \<Rightarrow> (n * n, d * d))
[PROOF STEP]
unfolding square_rat_def
[PROOF STATE]
proof (prove)
using this:
quotient_of x = (?a, ?b) \<Longrightarrow> quotient_of (x * x) = (?a * ?a, ?b * ?b)

goal (1 subgoal):
 1. quotient_of (x * x) = (case quotient_of x of (n, d) \<Rightarrow> (n * n, d * d))
[PROOF STEP]
by (cases "quotient_of x", auto)


[STATEMENT]
lemma scalar_prod_int_rat_code[code]: "v \<bullet>i w = (\<Sum>i = 0..<dim_vec v. int_times_rat (v $ i) (w $ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<bullet>i w = (\<Sum>i = 0..<dim_vec v. int_times_rat (v $ i) (w $ i))
[PROOF STEP]
unfolding scalar_prod_int_rat_def Let_def scalar_prod_def int_times_rat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<dim_vec (of_int_hom.vec_hom v). w $ i * of_int_hom.vec_hom v $ i) = (\<Sum>i = 0..<dim_vec v. rat_of_int (v $ i) * w $ i)
[PROOF STEP]
by (rule sum.cong, auto)


[STATEMENT]
lemma scalar_prod_int_rat[simp]: "dim_vec x = dim_vec y \<Longrightarrow> x \<bullet>i y = map_vec of_int x \<bullet> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec x = dim_vec y \<Longrightarrow> x \<bullet>i y = of_int_hom.vec_hom x \<bullet> y
[PROOF STEP]
unfolding scalar_prod_int_rat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec x = dim_vec y \<Longrightarrow> y \<bullet> of_int_hom.vec_hom x = of_int_hom.vec_hom x \<bullet> y
[PROOF STEP]
by (intro comm_scalar_prod[of _ "dim_vec x"], auto intro: carrier_vecI)


[STATEMENT]
lemma sq_norm_vec_rat_code[code]: "sq_norm_vec_rat x = (\<Sum>x\<leftarrow>list_of_vec x. square_rat x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sq_norm_vec_rat x = sum_list (map square_rat (list_of_vec x))
[PROOF STEP]
unfolding sq_norm_vec_rat_def sq_norm_vec_def square_rat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map sq_norm (list_of_vec x)) = (\<Sum>x\<leftarrow>list_of_vec x. x * x)
[PROOF STEP]
by auto


[STATEMENT]
lemma denot_implies_rel: "(v \<in> E e \<rho>) \<Longrightarrow> (\<rho> \<turnstile> e \<Rightarrow> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> E e \<rho> \<Longrightarrow> \<rho> \<turnstile> e \<Rightarrow> v
[PROOF STEP]
proof (induction e arbitrary: v \<rho>)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x v \<rho>. v \<in> E (EVar x) \<rho> \<Longrightarrow> \<rho> \<turnstile> EVar x \<Rightarrow> v
 2. \<And>x v \<rho>. v \<in> E (ENat x) \<rho> \<Longrightarrow> \<rho> \<turnstile> ENat x \<Rightarrow> v
 3. \<And>x1a e v \<rho>. \<lbrakk>\<And>v \<rho>. v \<in> E e \<rho> \<Longrightarrow> \<rho> \<turnstile> e \<Rightarrow> v; v \<in> E (ELam x1a e) \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> ELam x1a e \<Rightarrow> v
 4. \<And>e1 e2 v \<rho>. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; v \<in> E (EApp e1 e2) \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EApp e1 e2 \<Rightarrow> v
 5. \<And>x1a e1 e2 v \<rho>. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; v \<in> E (EPrim x1a e1 e2) \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EPrim x1a e1 e2 \<Rightarrow> v
 6. \<And>e1 e2 e3 v \<rho>. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e3 \<rho> \<Longrightarrow> \<rho> \<turnstile> e3 \<Rightarrow> v; v \<in> E (EIf e1 e2 e3) \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EIf e1 e2 e3 \<Rightarrow> v
[PROOF STEP]
case (EIf e1 e2 e3)
[PROOF STATE]
proof (state)
this:
?v \<in> E e1 ?\<rho> \<Longrightarrow> ?\<rho> \<turnstile> e1 \<Rightarrow> ?v
?v \<in> E e2 ?\<rho> \<Longrightarrow> ?\<rho> \<turnstile> e2 \<Rightarrow> ?v
?v \<in> E e3 ?\<rho> \<Longrightarrow> ?\<rho> \<turnstile> e3 \<Rightarrow> ?v
v \<in> E (EIf e1 e2 e3) \<rho>

goal (6 subgoals):
 1. \<And>x v \<rho>. v \<in> E (EVar x) \<rho> \<Longrightarrow> \<rho> \<turnstile> EVar x \<Rightarrow> v
 2. \<And>x v \<rho>. v \<in> E (ENat x) \<rho> \<Longrightarrow> \<rho> \<turnstile> ENat x \<Rightarrow> v
 3. \<And>x1a e v \<rho>. \<lbrakk>\<And>v \<rho>. v \<in> E e \<rho> \<Longrightarrow> \<rho> \<turnstile> e \<Rightarrow> v; v \<in> E (ELam x1a e) \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> ELam x1a e \<Rightarrow> v
 4. \<And>e1 e2 v \<rho>. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; v \<in> E (EApp e1 e2) \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EApp e1 e2 \<Rightarrow> v
 5. \<And>x1a e1 e2 v \<rho>. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; v \<in> E (EPrim x1a e1 e2) \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EPrim x1a e1 e2 \<Rightarrow> v
 6. \<And>e1 e2 e3 v \<rho>. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e3 \<rho> \<Longrightarrow> \<rho> \<turnstile> e3 \<Rightarrow> v; v \<in> E (EIf e1 e2 e3) \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EIf e1 e2 e3 \<Rightarrow> v
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?v \<in> E e1 ?\<rho> \<Longrightarrow> ?\<rho> \<turnstile> e1 \<Rightarrow> ?v
?v \<in> E e2 ?\<rho> \<Longrightarrow> ?\<rho> \<turnstile> e2 \<Rightarrow> ?v
?v \<in> E e3 ?\<rho> \<Longrightarrow> ?\<rho> \<turnstile> e3 \<Rightarrow> ?v
v \<in> E (EIf e1 e2 e3) \<rho>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?v \<in> E e1 ?\<rho> \<Longrightarrow> ?\<rho> \<turnstile> e1 \<Rightarrow> ?v
?v \<in> E e2 ?\<rho> \<Longrightarrow> ?\<rho> \<turnstile> e2 \<Rightarrow> ?v
?v \<in> E e3 ?\<rho> \<Longrightarrow> ?\<rho> \<turnstile> e3 \<Rightarrow> ?v
v \<in> E (EIf e1 e2 e3) \<rho>

goal (1 subgoal):
 1. \<rho> \<turnstile> EIf e1 e2 e3 \<Rightarrow> v
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e3 \<rho> \<Longrightarrow> \<rho> \<turnstile> e3 \<Rightarrow> v; \<exists>n. VNat n \<in> E e1 \<rho> \<and> (n = 0 \<longrightarrow> v \<in> E e3 \<rho>) \<and> (0 < n \<longrightarrow> v \<in> E e2 \<rho>)\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EIf e1 e2 e3 \<Rightarrow> v
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e3 \<rho> \<Longrightarrow> \<rho> \<turnstile> e3 \<Rightarrow> v; VNat n \<in> E e1 \<rho>; n = 0 \<longrightarrow> v \<in> E e3 \<rho>; 0 < n \<longrightarrow> v \<in> E e2 \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EIf e1 e2 e3 \<Rightarrow> v
[PROOF STEP]
apply (rename_tac n)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e3 \<rho> \<Longrightarrow> \<rho> \<turnstile> e3 \<Rightarrow> v; VNat n \<in> E e1 \<rho>; n = 0 \<longrightarrow> v \<in> E e3 \<rho>; 0 < n \<longrightarrow> v \<in> E e2 \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EIf e1 e2 e3 \<Rightarrow> v
[PROOF STEP]
apply (case_tac n)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e3 \<rho> \<Longrightarrow> \<rho> \<turnstile> e3 \<Rightarrow> v; VNat n \<in> E e1 \<rho>; n = 0 \<longrightarrow> v \<in> E e3 \<rho>; 0 < n \<longrightarrow> v \<in> E e2 \<rho>; n = 0\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EIf e1 e2 e3 \<Rightarrow> v
 2. \<And>n nat. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e3 \<rho> \<Longrightarrow> \<rho> \<turnstile> e3 \<Rightarrow> v; VNat n \<in> E e1 \<rho>; n = 0 \<longrightarrow> v \<in> E e3 \<rho>; 0 < n \<longrightarrow> v \<in> E e2 \<rho>; n = Suc nat\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EIf e1 e2 e3 \<Rightarrow> v
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n nat. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e3 \<rho> \<Longrightarrow> \<rho> \<turnstile> e3 \<Rightarrow> v; VNat n \<in> E e1 \<rho>; n = 0 \<longrightarrow> v \<in> E e3 \<rho>; 0 < n \<longrightarrow> v \<in> E e2 \<rho>; n = Suc nat\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EIf e1 e2 e3 \<Rightarrow> v
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n nat. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e3 \<rho> \<Longrightarrow> \<rho> \<turnstile> e3 \<Rightarrow> v; VNat (Suc nat) \<in> E e1 \<rho>; v \<in> E e2 \<rho>; n = Suc nat\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EIf e1 e2 e3 \<Rightarrow> v
[PROOF STEP]
apply (rule rifnz)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>n nat. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e3 \<rho> \<Longrightarrow> \<rho> \<turnstile> e3 \<Rightarrow> v; VNat (Suc nat) \<in> E e1 \<rho>; v \<in> E e2 \<rho>; n = Suc nat\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> VNat (?n25 n nat)
 2. \<And>n nat. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e3 \<rho> \<Longrightarrow> \<rho> \<turnstile> e3 \<Rightarrow> v; VNat (Suc nat) \<in> E e1 \<rho>; v \<in> E e2 \<rho>; n = Suc nat\<rbrakk> \<Longrightarrow> ?n25 n nat \<noteq> 0
 3. \<And>n nat. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e3 \<rho> \<Longrightarrow> \<rho> \<turnstile> e3 \<Rightarrow> v; VNat (Suc nat) \<in> E e1 \<rho>; v \<in> E e2 \<rho>; n = Suc nat\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v
[PROOF STEP]
apply force+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<rho> \<turnstile> EIf e1 e2 e3 \<Rightarrow> v

goal (5 subgoals):
 1. \<And>x v \<rho>. v \<in> E (EVar x) \<rho> \<Longrightarrow> \<rho> \<turnstile> EVar x \<Rightarrow> v
 2. \<And>x v \<rho>. v \<in> E (ENat x) \<rho> \<Longrightarrow> \<rho> \<turnstile> ENat x \<Rightarrow> v
 3. \<And>x1a e v \<rho>. \<lbrakk>\<And>v \<rho>. v \<in> E e \<rho> \<Longrightarrow> \<rho> \<turnstile> e \<Rightarrow> v; v \<in> E (ELam x1a e) \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> ELam x1a e \<Rightarrow> v
 4. \<And>e1 e2 v \<rho>. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; v \<in> E (EApp e1 e2) \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EApp e1 e2 \<Rightarrow> v
 5. \<And>x1a e1 e2 v \<rho>. \<lbrakk>\<And>v \<rho>. v \<in> E e1 \<rho> \<Longrightarrow> \<rho> \<turnstile> e1 \<Rightarrow> v; \<And>v \<rho>. v \<in> E e2 \<rho> \<Longrightarrow> \<rho> \<turnstile> e2 \<Rightarrow> v; v \<in> E (EPrim x1a e1 e2) \<rho>\<rbrakk> \<Longrightarrow> \<rho> \<turnstile> EPrim x1a e1 e2 \<Rightarrow> v
[PROOF STEP]
qed auto


[STATEMENT]
lemma rel_implies_denot: "\<rho> \<turnstile> e \<Rightarrow> v \<Longrightarrow> v \<in> E e \<rho>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> \<turnstile> e \<Rightarrow> v \<Longrightarrow> v \<in> E e \<rho>
[PROOF STEP]
by (induction \<rho> e v rule: rel_sem.induct) auto


[STATEMENT]
theorem equivalence_relational_denotational: "(v \<in> E e \<rho>) = (\<rho> \<turnstile> e \<Rightarrow> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (v \<in> E e \<rho>) = \<rho> \<turnstile> e \<Rightarrow> v
[PROOF STEP]
using denot_implies_rel rel_implies_denot
[PROOF STATE]
proof (prove)
using this:
?v \<in> E ?e ?\<rho> \<Longrightarrow> ?\<rho> \<turnstile> ?e \<Rightarrow> ?v
?\<rho> \<turnstile> ?e \<Rightarrow> ?v \<Longrightarrow> ?v \<in> E ?e ?\<rho>

goal (1 subgoal):
 1. (v \<in> E e \<rho>) = \<rho> \<turnstile> e \<Rightarrow> v
[PROOF STEP]
by blast


[STATEMENT]
lemma primorial_mono: "x \<le> y \<Longrightarrow> primorial x \<le> primorial y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> primorial x \<le> primorial y
[PROOF STEP]
unfolding primorial_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> \<Prod>{p. prime p \<and> real p \<le> x} \<le> \<Prod>{p. prime p \<and> real p \<le> y}
[PROOF STEP]
by (intro dvd_imp_le prod_dvd_prod_subset)
     (auto intro!: prod_pos finite_primes_le dest: prime_gt_0_nat)


[STATEMENT]
lemma prime_factorization_primorial:
  "prime_factorization (primorial x) = mset_set {p. prime p \<and> real p \<le> x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factorization (primorial x) = mset_set {p. prime p \<and> real p \<le> x}
[PROOF STEP]
proof (intro multiset_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. count (prime_factorization (primorial x)) xa = count (mset_set {p. prime p \<and> real p \<le> x}) xa
[PROOF STEP]
fix p :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. count (prime_factorization (primorial x)) xa = count (mset_set {p. prime p \<and> real p \<le> x}) xa
[PROOF STEP]
note fin = finite_primes_le[of x]
[PROOF STATE]
proof (state)
this:
finite {p. prime p \<and> real p \<le> x}

goal (1 subgoal):
 1. \<And>xa. count (prime_factorization (primorial x)) xa = count (mset_set {p. prime p \<and> real p \<le> x}) xa
[PROOF STEP]
show "count (prime_factorization (primorial x)) p =
          count (mset_set {p. prime p \<and> real p \<le> x}) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
[PROOF STEP]
proof (cases "prime p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
 2. \<not> prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
prime p

goal (2 subgoals):
 1. prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
 2. \<not> prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
[PROOF STEP]
hence "count (prime_factorization (primorial x)) p =
             sum (multiplicity p) {p. prime p \<and> real p \<le> x}"
[PROOF STATE]
proof (prove)
using this:
prime p

goal (1 subgoal):
 1. count (prime_factorization (primorial x)) p = sum (multiplicity p) {p. prime p \<and> real p \<le> x}
[PROOF STEP]
unfolding primorial_def count_prime_factorization
[PROOF STATE]
proof (prove)
using this:
prime p

goal (1 subgoal):
 1. (if prime p then multiplicity p (\<Prod>{p. prime p \<and> real p \<le> x}) else 0) = sum (multiplicity p) {p. prime p \<and> real p \<le> x}
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
prime p
finite {p. prime p \<and> real p \<le> x}

goal (1 subgoal):
 1. (if prime p then multiplicity p (\<Prod>{p. prime p \<and> real p \<le> x}) else 0) = sum (multiplicity p) {p. prime p \<and> real p \<le> x}
[PROOF STEP]
by (subst prime_elem_multiplicity_prod_distrib) auto
[PROOF STATE]
proof (state)
this:
count (prime_factorization (primorial x)) p = sum (multiplicity p) {p. prime p \<and> real p \<le> x}

goal (2 subgoals):
 1. prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
 2. \<not> prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
count (prime_factorization (primorial x)) p = sum (multiplicity p) {p. prime p \<and> real p \<le> x}

goal (2 subgoals):
 1. prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
 2. \<not> prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
[PROOF STEP]
from True
[PROOF STATE]
proof (chain)
picking this:
prime p
[PROOF STEP]
have "\<dots> = sum (\<lambda>_. 1) (if p \<le> x then {p} else {})"
[PROOF STATE]
proof (prove)
using this:
prime p

goal (1 subgoal):
 1. sum (multiplicity p) {p. prime p \<and> real p \<le> x} = (\<Sum>_\<in>(if real p \<le> x then {p} else {}). 1)
[PROOF STEP]
using fin
[PROOF STATE]
proof (prove)
using this:
prime p
finite {p. prime p \<and> real p \<le> x}

goal (1 subgoal):
 1. sum (multiplicity p) {p. prime p \<and> real p \<le> x} = (\<Sum>_\<in>(if real p \<le> x then {p} else {}). 1)
[PROOF STEP]
by (intro sum.mono_neutral_cong_right) (auto simp: prime_multiplicity_other split: if_splits)
[PROOF STATE]
proof (state)
this:
sum (multiplicity p) {p. prime p \<and> real p \<le> x} = (\<Sum>_\<in>(if real p \<le> x then {p} else {}). 1)

goal (2 subgoals):
 1. prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
 2. \<not> prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum (multiplicity p) {p. prime p \<and> real p \<le> x} = (\<Sum>_\<in>(if real p \<le> x then {p} else {}). 1)

goal (2 subgoals):
 1. prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
 2. \<not> prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
[PROOF STEP]
have "\<dots> = count (mset_set {p. prime p \<and> real p \<le> x}) p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>_\<in>(if real p \<le> x then {p} else {}). 1) = count (mset_set {p. prime p \<and> real p \<le> x}) p
[PROOF STEP]
using True fin
[PROOF STATE]
proof (prove)
using this:
prime p
finite {p. prime p \<and> real p \<le> x}

goal (1 subgoal):
 1. (\<Sum>_\<in>(if real p \<le> x then {p} else {}). 1) = count (mset_set {p. prime p \<and> real p \<le> x}) p
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<Sum>_\<in>(if real p \<le> x then {p} else {}). 1) = count (mset_set {p. prime p \<and> real p \<le> x}) p

goal (2 subgoals):
 1. prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
 2. \<not> prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p

goal (1 subgoal):
 1. count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p

goal (1 subgoal):
 1. \<not> prime p \<Longrightarrow> count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
count (prime_factorization (primorial x)) p = count (mset_set {p. prime p \<and> real p \<le> x}) p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_factors_primorial [simp]:
  "prime_factors (primorial x) = {p. prime p \<and> real p \<le> x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factors (primorial x) = {p. prime p \<and> real p \<le> x}
[PROOF STEP]
unfolding prime_factorization_primorial
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_mset (mset_set {p. prime p \<and> real p \<le> x}) = {p. prime p \<and> real p \<le> x}
[PROOF STEP]
using finite_primes_le[of x]
[PROOF STATE]
proof (prove)
using this:
finite {p. prime p \<and> real p \<le> x}

goal (1 subgoal):
 1. set_mset (mset_set {p. prime p \<and> real p \<le> x}) = {p. prime p \<and> real p \<le> x}
[PROOF STEP]
by simp


[STATEMENT]
lemma primorial_pos [simp, intro]: "primorial x > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < primorial x
[PROOF STEP]
unfolding primorial_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < \<Prod>{p. prime p \<and> real p \<le> x}
[PROOF STEP]
by (intro prod_pos) (auto dest: prime_gt_0_nat)


[STATEMENT]
lemma primorial_neq_zero [simp]: "primorial x \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primorial x \<noteq> 0
[PROOF STEP]
by auto


[STATEMENT]
lemma of_nat_primes_omega_primorial [simp]: "real (primes_omega (primorial x)) = primes_pi x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (primes_omega (primorial x)) = primes_pi x
[PROOF STEP]
by (simp add: primes_omega_def primes_pi_def prime_sum_upto_def)


[STATEMENT]
lemma primes_omega_primorial: "primes_omega (primorial x) = nat \<lfloor>primes_pi x\<rfloor>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primes_omega (primorial x) = nat \<lfloor>primes_pi x\<rfloor>
[PROOF STEP]
by (simp add: primes_omega_def primes_pi_def prime_sum_upto_def)


[STATEMENT]
lemma prime_dvd_primorial_iff: "prime p \<Longrightarrow> p dvd primorial x \<longleftrightarrow> p \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime p \<Longrightarrow> (p dvd primorial x) = (real p \<le> x)
[PROOF STEP]
using finite_primes_le[of x]
[PROOF STATE]
proof (prove)
using this:
finite {p. prime p \<and> real p \<le> x}

goal (1 subgoal):
 1. prime p \<Longrightarrow> (p dvd primorial x) = (real p \<le> x)
[PROOF STEP]
by (auto simp: primorial_def prime_dvd_prod_iff dest: primes_dvd_imp_eq)


[STATEMENT]
lemma squarefree_primorial [intro]: "squarefree (primorial x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. squarefree (primorial x)
[PROOF STEP]
unfolding primorial_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. squarefree (\<Prod>{p. prime p \<and> real p \<le> x})
[PROOF STEP]
by (intro squarefree_prod_coprime) (auto simp: squarefree_prime intro: primes_coprime)


[STATEMENT]
lemma primorial_ge: "primorial x \<ge> 2 powr primes_pi x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 powr primes_pi x \<le> real (primorial x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 powr primes_pi x \<le> real (primorial x)
[PROOF STEP]
have "2 powr primes_pi x = real (\<Prod>p | prime p \<and> real p \<le> x. 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 powr primes_pi x = real (\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 2)
[PROOF STEP]
by (simp add: primes_pi_def prime_sum_upto_def powr_realpow)
[PROOF STATE]
proof (state)
this:
2 powr primes_pi x = real (\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 2)

goal (1 subgoal):
 1. 2 powr primes_pi x \<le> real (primorial x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 powr primes_pi x = real (\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 2)

goal (1 subgoal):
 1. 2 powr primes_pi x \<le> real (primorial x)
[PROOF STEP]
have "(\<Prod>p | prime p \<and> real p \<le> x. 2) \<le> (\<Prod>p | prime p \<and> real p \<le> x. p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 2) \<le> \<Prod>{p. prime p \<and> real p \<le> x}
[PROOF STEP]
by (intro prod_mono) (auto dest: prime_gt_1_nat)
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 2) \<le> \<Prod>{p. prime p \<and> real p \<le> x}

goal (1 subgoal):
 1. 2 powr primes_pi x \<le> real (primorial x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 2) \<le> \<Prod>{p. prime p \<and> real p \<le> x}

goal (1 subgoal):
 1. 2 powr primes_pi x \<le> real (primorial x)
[PROOF STEP]
have "\<dots> = primorial x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Prod>{p. prime p \<and> real p \<le> x} = primorial x
[PROOF STEP]
by (simp add: primorial_def)
[PROOF STATE]
proof (state)
this:
\<Prod>{p. prime p \<and> real p \<le> x} = primorial x

goal (1 subgoal):
 1. 2 powr primes_pi x \<le> real (primorial x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> real x \<le> real y) \<Longrightarrow> 2 powr primes_pi x \<le> real (primorial x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> real x \<le> real y) \<Longrightarrow> 2 powr primes_pi x \<le> real (primorial x)

goal (1 subgoal):
 1. 2 powr primes_pi x \<le> real (primorial x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 powr primes_pi x \<le> real (primorial x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma primorial_at_top: "filterlim primorial at_top at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. filterlim primorial sequentially at_top
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. filterlim primorial sequentially at_top
[PROOF STEP]
have "filterlim (\<lambda>x. real (primorial x)) at_top at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LIM x at_top. real (primorial x) :> at_top
[PROOF STEP]
proof (rule filterlim_at_top_mono)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. filterlim ?f at_top at_top
 2. \<forall>\<^sub>F x in at_top. ?f x \<le> real (primorial x)
[PROOF STEP]
show "eventually (\<lambda>x. primorial x \<ge> 2 powr primes_pi x) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_top. 2 powr primes_pi x \<le> real (primorial x)
[PROOF STEP]
by (intro always_eventually primorial_ge allI)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at_top. 2 powr primes_pi x \<le> real (primorial x)

goal (1 subgoal):
 1. LIM x at_top. 2 powr primes_pi x :> at_top
[PROOF STEP]
have "filterlim (\<lambda>x. exp (ln 2 * primes_pi x)) at_top at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LIM x at_top. exp (ln 2 * primes_pi x) :> at_top
[PROOF STEP]
by (intro filterlim_compose[OF exp_at_top]
                filterlim_tendsto_pos_mult_at_top[OF tendsto_const] \<pi>_at_top) auto
[PROOF STATE]
proof (state)
this:
LIM x at_top. exp (ln 2 * primes_pi x) :> at_top

goal (1 subgoal):
 1. LIM x at_top. 2 powr primes_pi x :> at_top
[PROOF STEP]
thus "filterlim (\<lambda>x. 2 powr primes_pi x) at_top at_top"
[PROOF STATE]
proof (prove)
using this:
LIM x at_top. exp (ln 2 * primes_pi x) :> at_top

goal (1 subgoal):
 1. LIM x at_top. 2 powr primes_pi x :> at_top
[PROOF STEP]
by (simp add: powr_def mult_ac)
[PROOF STATE]
proof (state)
this:
LIM x at_top. 2 powr primes_pi x :> at_top

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
LIM x at_top. real (primorial x) :> at_top

goal (1 subgoal):
 1. filterlim primorial sequentially at_top
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
LIM x at_top. real (primorial x) :> at_top

goal (1 subgoal):
 1. filterlim primorial sequentially at_top
[PROOF STEP]
unfolding filterlim_sequentially_iff_filterlim_real [symmetric]
[PROOF STATE]
proof (prove)
using this:
filterlim primorial sequentially at_top

goal (1 subgoal):
 1. filterlim primorial sequentially at_top
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
filterlim primorial sequentially at_top

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma totient_primorial:
  "real (totient (primorial x)) =
     real (primorial x) * (\<Prod>p | prime p \<and> real p \<le> x. 1 - 1 / real p)" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (totient (primorial x)) = real (primorial x) * (\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 1 - 1 / real p)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real (totient (primorial x)) = real (primorial x) * (\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 1 - 1 / real p)
[PROOF STEP]
have "real (totient (primorial x)) =
          primorial x * (\<Prod>p\<in>prime_factors (primorial x). 1 - 1 / p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (totient (primorial x)) = real (primorial x) * (\<Prod>p\<in>prime_factors (primorial x). 1 - 1 / real p)
[PROOF STEP]
by (rule totient_formula2)
[PROOF STATE]
proof (state)
this:
real (totient (primorial x)) = real (primorial x) * (\<Prod>p\<in>prime_factors (primorial x). 1 - 1 / real p)

goal (1 subgoal):
 1. real (totient (primorial x)) = real (primorial x) * (\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 1 - 1 / real p)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
real (totient (primorial x)) = real (primorial x) * (\<Prod>p\<in>prime_factors (primorial x). 1 - 1 / real p)

goal (1 subgoal):
 1. real (totient (primorial x)) = real (primorial x) * (\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 1 - 1 / real p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (totient (primorial x)) = real (primorial x) * (\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 1 - 1 / real p)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ln_primorial: "ln (primorial x) = primes_theta x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ln (real (primorial x)) = primes_theta x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ln (real (primorial x)) = primes_theta x
[PROOF STEP]
have "finite {p. prime p \<and> real p \<le> x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {p. prime p \<and> real p \<le> x}
[PROOF STEP]
by (rule finite_subset[of _ "{..nat \<lfloor>x\<rfloor>}"]) (auto simp: le_nat_iff le_floor_iff)
[PROOF STATE]
proof (state)
this:
finite {p. prime p \<and> real p \<le> x}

goal (1 subgoal):
 1. ln (real (primorial x)) = primes_theta x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {p. prime p \<and> real p \<le> x}

goal (1 subgoal):
 1. ln (real (primorial x)) = primes_theta x
[PROOF STEP]
unfolding of_nat_prod primorial_def
[PROOF STATE]
proof (prove)
using this:
finite {p. prime p \<and> real p \<le> x}

goal (1 subgoal):
 1. ln (prod real {p. prime p \<and> real p \<le> x}) = primes_theta x
[PROOF STEP]
by (subst ln_prod) (auto dest: prime_gt_0_nat simp: \<theta>_def prime_sum_upto_def)
[PROOF STATE]
proof (state)
this:
ln (real (primorial x)) = primes_theta x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma divisor_count_primorial: "divisor_count (primorial x) = 2 powr primes_pi x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (divisor_count (primorial x)) = 2 powr primes_pi x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real (divisor_count (primorial x)) = 2 powr primes_pi x
[PROOF STEP]
have "divisor_count (primorial x) = (\<Prod>p | prime p \<and> real p \<le> x. divisor_count p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_count (primorial x) = prod divisor_count {p. prime p \<and> real p \<le> x}
[PROOF STEP]
unfolding primorial_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_count (\<Prod>{p. prime p \<and> real p \<le> x}) = prod divisor_count {p. prime p \<and> real p \<le> x}
[PROOF STEP]
by (subst divisor_count.prod_coprime) (auto simp: primes_coprime)
[PROOF STATE]
proof (state)
this:
divisor_count (primorial x) = prod divisor_count {p. prime p \<and> real p \<le> x}

goal (1 subgoal):
 1. real (divisor_count (primorial x)) = 2 powr primes_pi x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
divisor_count (primorial x) = prod divisor_count {p. prime p \<and> real p \<le> x}

goal (1 subgoal):
 1. real (divisor_count (primorial x)) = 2 powr primes_pi x
[PROOF STEP]
have "\<dots> = (\<Prod>p | prime p \<and> real p \<le> x. 2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prod divisor_count {p. prime p \<and> real p \<le> x} = (\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 2)
[PROOF STEP]
by (intro prod.cong divisor_count.prime) auto
[PROOF STATE]
proof (state)
this:
prod divisor_count {p. prime p \<and> real p \<le> x} = (\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 2)

goal (1 subgoal):
 1. real (divisor_count (primorial x)) = 2 powr primes_pi x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prod divisor_count {p. prime p \<and> real p \<le> x} = (\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 2)

goal (1 subgoal):
 1. real (divisor_count (primorial x)) = 2 powr primes_pi x
[PROOF STEP]
have "\<dots> = 2 powr primes_pi x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 2) = 2 powr primes_pi x
[PROOF STEP]
by (simp add: primes_pi_def prime_sum_upto_def powr_realpow)
[PROOF STATE]
proof (state)
this:
real (\<Prod>p\<in>{p. prime p \<and> real p \<le> x}. 2) = 2 powr primes_pi x

goal (1 subgoal):
 1. real (divisor_count (primorial x)) = 2 powr primes_pi x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real (divisor_count (primorial x)) = 2 powr primes_pi x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
real (divisor_count (primorial x)) = 2 powr primes_pi x

goal (1 subgoal):
 1. real (divisor_count (primorial x)) = 2 powr primes_pi x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
real (divisor_count (primorial x)) = 2 powr primes_pi x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma primorial'_0 [simp]: "primorial' 0 = 1"
  and primorial'_1 [simp]: "primorial' 1 = 2"
  and primorial'_2 [simp]: "primorial' 2 = 6"
  and primorial'_3 [simp]: "primorial' 3 = 30"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (primorial' 0 = 1 &&& primorial' 1 = 2) &&& primorial' 2 = 6 &&& primorial' 3 = 30
[PROOF STEP]
by (simp_all add: primorial'_def lessThan_nat_numeral)


[STATEMENT]
lemma primorial'_Suc: "primorial' (Suc n) = nth_prime n * primorial' n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primorial' (Suc n) = nth_prime n * primorial' n
[PROOF STEP]
by (simp add: primorial'_def)


[STATEMENT]
lemma primorial'_pos [intro]: "primorial' n > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < primorial' n
[PROOF STEP]
unfolding primorial'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < prod nth_prime {..<n}
[PROOF STEP]
by (auto intro: prime_gt_0_nat)


[STATEMENT]
lemma primorial'_neq_0 [simp]: "primorial' n \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primorial' n \<noteq> 0
[PROOF STEP]
by auto


[STATEMENT]
lemma strict_mono_primorial': "strict_mono primorial'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strict_mono primorial'
[PROOF STEP]
unfolding strict_mono_Suc_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. primorial' n < primorial' (Suc n)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. primorial' n < primorial' (Suc n)
[PROOF STEP]
fix n :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. primorial' n < primorial' (Suc n)
[PROOF STEP]
have "primorial' n * 1 < primorial' n * nth_prime n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primorial' n * 1 < primorial' n * nth_prime n
[PROOF STEP]
using prime_gt_1_nat[OF prime_nth_prime[of n]]
[PROOF STATE]
proof (prove)
using this:
1 < nth_prime n

goal (1 subgoal):
 1. primorial' n * 1 < primorial' n * nth_prime n
[PROOF STEP]
by (intro mult_strict_left_mono) auto
[PROOF STATE]
proof (state)
this:
primorial' n * 1 < primorial' n * nth_prime n

goal (1 subgoal):
 1. \<And>n. primorial' n < primorial' (Suc n)
[PROOF STEP]
thus "primorial' n < primorial' (Suc n)"
[PROOF STATE]
proof (prove)
using this:
primorial' n * 1 < primorial' n * nth_prime n

goal (1 subgoal):
 1. primorial' n < primorial' (Suc n)
[PROOF STEP]
by (simp add: primorial'_Suc)
[PROOF STATE]
proof (state)
this:
primorial' n < primorial' (Suc n)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_factorization_primorial':
  "prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})
[PROOF STEP]
have "prime_factorization (primorial' k) = (\<Sum>i<k. prime_factorization (nth_prime i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factorization (primorial' k) = (\<Sum>i<k. prime_factorization (nth_prime i))
[PROOF STEP]
unfolding primorial'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factorization (prod nth_prime {..<k}) = (\<Sum>i<k. prime_factorization (nth_prime i))
[PROOF STEP]
by (subst prime_factorization_prod) (auto intro: prime_gt_0_nat)
[PROOF STATE]
proof (state)
this:
prime_factorization (primorial' k) = (\<Sum>i<k. prime_factorization (nth_prime i))

goal (1 subgoal):
 1. prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
prime_factorization (primorial' k) = (\<Sum>i<k. prime_factorization (nth_prime i))

goal (1 subgoal):
 1. prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})
[PROOF STEP]
have "\<dots> = (\<Sum>i<k. {#nth_prime i#})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<k. prime_factorization (nth_prime i)) = (\<Sum>i<k. {#nth_prime i#})
[PROOF STEP]
by (intro sum.cong prime_factorization_prime) auto
[PROOF STATE]
proof (state)
this:
(\<Sum>i<k. prime_factorization (nth_prime i)) = (\<Sum>i<k. {#nth_prime i#})

goal (1 subgoal):
 1. prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<k. prime_factorization (nth_prime i)) = (\<Sum>i<k. {#nth_prime i#})

goal (1 subgoal):
 1. prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})
[PROOF STEP]
have "\<dots> = (\<Sum>p\<in>nth_prime ` {..<k}. {#p#})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<k. {#nth_prime i#}) = (\<Sum>p\<in>nth_prime ` {..<k}. {#p#})
[PROOF STEP]
by (subst sum.reindex) (auto intro: inj_onI)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<k. {#nth_prime i#}) = (\<Sum>p\<in>nth_prime ` {..<k}. {#p#})

goal (1 subgoal):
 1. prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<k. {#nth_prime i#}) = (\<Sum>p\<in>nth_prime ` {..<k}. {#p#})

goal (1 subgoal):
 1. prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})
[PROOF STEP]
have "\<dots> = mset_set (nth_prime ` {..<k})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>p\<in>nth_prime ` {..<k}. {#p#}) = mset_set (nth_prime ` {..<k})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>p\<in>nth_prime ` {..<k}. {#p#}) = mset_set (nth_prime ` {..<k})

goal (1 subgoal):
 1. prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})

goal (1 subgoal):
 1. prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
prime_factorization (primorial' k) = mset_set (nth_prime ` {..<k})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_factors_primorial': "prime_factors (primorial' k) = nth_prime ` {..<k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime_factors (primorial' k) = nth_prime ` {..<k}
[PROOF STEP]
by (simp add: prime_factorization_primorial')


[STATEMENT]
lemma primes_omega_primorial' [simp]: "primes_omega (primorial' k) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primes_omega (primorial' k) = k
[PROOF STEP]
unfolding primes_omega_def prime_factors_primorial'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (nth_prime ` {..<k}) = k
[PROOF STEP]
by (subst card_image) (auto intro: inj_onI)


[STATEMENT]
lemma squarefree_primorial' [intro]: "squarefree (primorial' x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. squarefree (primorial' x)
[PROOF STEP]
unfolding primorial'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. squarefree (prod nth_prime {..<x})
[PROOF STEP]
by (intro squarefree_prod_coprime) (auto intro: squarefree_prime intro: primes_coprime)


[STATEMENT]
lemma divisor_count_primorial' [simp]: "divisor_count (primorial' k) = 2 ^ k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_count (primorial' k) = 2 ^ k
[PROOF STEP]
by (subst divisor_count_squarefree) auto


[STATEMENT]
lemma totient_primorial':
  "totient (primorial' k) = primorial' k * (\<Prod>i<k. 1 - 1 / nth_prime i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (totient (primorial' k)) = real (primorial' k) * (\<Prod>i<k. 1 - 1 / real (nth_prime i))
[PROOF STEP]
unfolding totient_formula2 prime_factors_primorial'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (primorial' k) * (\<Prod>p\<in>nth_prime ` {..<k}. 1 - 1 / real p) = real (primorial' k) * (\<Prod>i<k. 1 - 1 / real (nth_prime i))
[PROOF STEP]
by (subst prod.reindex) (auto intro: inj_onI)


[STATEMENT]
lemma primorial_conv_primorial': "primorial x = primorial' (nat \<lfloor>primes_pi x\<rfloor>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primorial x = primorial' (nat \<lfloor>primes_pi x\<rfloor>)
[PROOF STEP]
unfolding primorial_def primorial'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Prod>{p. prime p \<and> real p \<le> x} = prod nth_prime {..<nat \<lfloor>primes_pi x\<rfloor>}
[PROOF STEP]
proof (rule prod.reindex_bij_witness[of _ nth_prime "\<lambda>p. nat \<lfloor>primes_pi (real p)\<rfloor> - 1"])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nth_prime (nat \<lfloor>primes_pi (real a)\<rfloor> - 1) = a
 2. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nat \<lfloor>primes_pi (real a)\<rfloor> - 1 \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}
 3. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nat \<lfloor>primes_pi (real (nth_prime b))\<rfloor> - 1 = b
 4. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
 5. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nth_prime (nat \<lfloor>primes_pi (real a)\<rfloor> - 1) = a
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nth_prime (nat \<lfloor>primes_pi (real a)\<rfloor> - 1) = a
 2. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nat \<lfloor>primes_pi (real a)\<rfloor> - 1 \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}
 3. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nat \<lfloor>primes_pi (real (nth_prime b))\<rfloor> - 1 = b
 4. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
 5. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nth_prime (nat \<lfloor>primes_pi (real a)\<rfloor> - 1) = a
[PROOF STEP]
assume p: "p \<in> {p. prime p \<and> real p \<le> x}"
[PROOF STATE]
proof (state)
this:
p \<in> {p. prime p \<and> real p \<le> x}

goal (5 subgoals):
 1. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nth_prime (nat \<lfloor>primes_pi (real a)\<rfloor> - 1) = a
 2. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nat \<lfloor>primes_pi (real a)\<rfloor> - 1 \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}
 3. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nat \<lfloor>primes_pi (real (nth_prime b))\<rfloor> - 1 = b
 4. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
 5. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nth_prime (nat \<lfloor>primes_pi (real a)\<rfloor> - 1) = a
[PROOF STEP]
have [simp]: "primes_pi 2 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primes_pi 2 = 1
[PROOF STEP]
by (auto simp: eval_\<pi>)
[PROOF STATE]
proof (state)
this:
primes_pi 2 = 1

goal (5 subgoals):
 1. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nth_prime (nat \<lfloor>primes_pi (real a)\<rfloor> - 1) = a
 2. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nat \<lfloor>primes_pi (real a)\<rfloor> - 1 \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}
 3. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nat \<lfloor>primes_pi (real (nth_prime b))\<rfloor> - 1 = b
 4. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
 5. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nth_prime (nat \<lfloor>primes_pi (real a)\<rfloor> - 1) = a
[PROOF STEP]
have "primes_pi p \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> primes_pi (real p)
[PROOF STEP]
using p \<pi>_mono[of 2 "real p"]
[PROOF STATE]
proof (prove)
using this:
p \<in> {p. prime p \<and> real p \<le> x}
2 \<le> real p \<Longrightarrow> primes_pi 2 \<le> primes_pi (real p)

goal (1 subgoal):
 1. 1 \<le> primes_pi (real p)
[PROOF STEP]
by (auto dest!: prime_gt_1_nat)
[PROOF STATE]
proof (state)
this:
1 \<le> primes_pi (real p)

goal (5 subgoals):
 1. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nth_prime (nat \<lfloor>primes_pi (real a)\<rfloor> - 1) = a
 2. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nat \<lfloor>primes_pi (real a)\<rfloor> - 1 \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}
 3. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nat \<lfloor>primes_pi (real (nth_prime b))\<rfloor> - 1 = b
 4. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
 5. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nth_prime (nat \<lfloor>primes_pi (real a)\<rfloor> - 1) = a
[PROOF STEP]
with p
[PROOF STATE]
proof (chain)
picking this:
p \<in> {p. prime p \<and> real p \<le> x}
1 \<le> primes_pi (real p)
[PROOF STEP]
show "nth_prime (nat \<lfloor>primes_pi p\<rfloor> - 1) = p"
[PROOF STATE]
proof (prove)
using this:
p \<in> {p. prime p \<and> real p \<le> x}
1 \<le> primes_pi (real p)

goal (1 subgoal):
 1. nth_prime (nat \<lfloor>primes_pi (real p)\<rfloor> - 1) = p
[PROOF STEP]
using \<pi>_pos[of "real p"]
[PROOF STATE]
proof (prove)
using this:
p \<in> {p. prime p \<and> real p \<le> x}
1 \<le> primes_pi (real p)
2 \<le> real p \<Longrightarrow> 0 < primes_pi (real p)

goal (1 subgoal):
 1. nth_prime (nat \<lfloor>primes_pi (real p)\<rfloor> - 1) = p
[PROOF STEP]
by (intro nth_prime_eqI'')
       (auto simp: le_nat_iff le_floor_iff primes_pi_def prime_sum_upto_def of_nat_diff)
[PROOF STATE]
proof (state)
this:
nth_prime (nat \<lfloor>primes_pi (real p)\<rfloor> - 1) = p

goal (4 subgoals):
 1. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nat \<lfloor>primes_pi (real a)\<rfloor> - 1 \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}
 2. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nat \<lfloor>primes_pi (real (nth_prime b))\<rfloor> - 1 = b
 3. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
 4. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nth_prime (nat \<lfloor>primes_pi (real a)\<rfloor> - 1) = a
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
p \<in> {p. prime p \<and> real p \<le> x}
[PROOF STEP]
have "nat \<lfloor>primes_pi (real p)\<rfloor> \<le> nat \<lfloor>primes_pi x\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
p \<in> {p. prime p \<and> real p \<le> x}

goal (1 subgoal):
 1. nat \<lfloor>primes_pi (real p)\<rfloor> \<le> nat \<lfloor>primes_pi x\<rfloor>
[PROOF STEP]
by (intro nat_mono floor_mono \<pi>_mono) auto
[PROOF STATE]
proof (state)
this:
nat \<lfloor>primes_pi (real p)\<rfloor> \<le> nat \<lfloor>primes_pi x\<rfloor>

goal (4 subgoals):
 1. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nat \<lfloor>primes_pi (real a)\<rfloor> - 1 \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}
 2. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nat \<lfloor>primes_pi (real (nth_prime b))\<rfloor> - 1 = b
 3. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
 4. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nth_prime (nat \<lfloor>primes_pi (real a)\<rfloor> - 1) = a
[PROOF STEP]
hence "nat \<lfloor>primes_pi (real p)\<rfloor> - 1 < nat \<lfloor>primes_pi x\<rfloor>"
[PROOF STATE]
proof (prove)
using this:
nat \<lfloor>primes_pi (real p)\<rfloor> \<le> nat \<lfloor>primes_pi x\<rfloor>

goal (1 subgoal):
 1. nat \<lfloor>primes_pi (real p)\<rfloor> - 1 < nat \<lfloor>primes_pi x\<rfloor>
[PROOF STEP]
using \<open>primes_pi p \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
nat \<lfloor>primes_pi (real p)\<rfloor> \<le> nat \<lfloor>primes_pi x\<rfloor>
1 \<le> primes_pi (real p)

goal (1 subgoal):
 1. nat \<lfloor>primes_pi (real p)\<rfloor> - 1 < nat \<lfloor>primes_pi x\<rfloor>
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
nat \<lfloor>primes_pi (real p)\<rfloor> - 1 < nat \<lfloor>primes_pi x\<rfloor>

goal (4 subgoals):
 1. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nat \<lfloor>primes_pi (real a)\<rfloor> - 1 \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}
 2. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nat \<lfloor>primes_pi (real (nth_prime b))\<rfloor> - 1 = b
 3. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
 4. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nth_prime (nat \<lfloor>primes_pi (real a)\<rfloor> - 1) = a
[PROOF STEP]
thus  "nat \<lfloor>primes_pi (real p)\<rfloor> - 1 \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}"
[PROOF STATE]
proof (prove)
using this:
nat \<lfloor>primes_pi (real p)\<rfloor> - 1 < nat \<lfloor>primes_pi x\<rfloor>

goal (1 subgoal):
 1. nat \<lfloor>primes_pi (real p)\<rfloor> - 1 \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nat \<lfloor>primes_pi (real p)\<rfloor> - 1 \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}

goal (3 subgoals):
 1. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nat \<lfloor>primes_pi (real (nth_prime b))\<rfloor> - 1 = b
 2. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
 3. \<And>a. a \<in> {p. prime p \<and> real p \<le> x} \<Longrightarrow> nth_prime (nat \<lfloor>primes_pi (real a)\<rfloor> - 1) = a
[PROOF STEP]
show "nth_prime (nat \<lfloor>primes_pi (real p)\<rfloor> - 1) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_prime (nat \<lfloor>primes_pi (real p)\<rfloor> - 1) = p
[PROOF STEP]
using p \<open>primes_pi p \<ge> 1\<close>
[PROOF STATE]
proof (prove)
using this:
p \<in> {p. prime p \<and> real p \<le> x}
1 \<le> primes_pi (real p)

goal (1 subgoal):
 1. nth_prime (nat \<lfloor>primes_pi (real p)\<rfloor> - 1) = p
[PROOF STEP]
by (intro nth_prime_eqI'') (auto simp: le_nat_iff primes_pi_def prime_sum_upto_def)
[PROOF STATE]
proof (state)
this:
nth_prime (nat \<lfloor>primes_pi (real p)\<rfloor> - 1) = p

goal (2 subgoals):
 1. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nat \<lfloor>primes_pi (real (nth_prime b))\<rfloor> - 1 = b
 2. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nat \<lfloor>primes_pi (real (nth_prime b))\<rfloor> - 1 = b
 2. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nat \<lfloor>primes_pi (real (nth_prime b))\<rfloor> - 1 = b
 2. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
[PROOF STEP]
assume k: "k \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}"
[PROOF STATE]
proof (state)
this:
k \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}

goal (2 subgoals):
 1. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nat \<lfloor>primes_pi (real (nth_prime b))\<rfloor> - 1 = b
 2. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
[PROOF STEP]
thus *: "nat \<lfloor>primes_pi (real (nth_prime k))\<rfloor> - 1 = k"
[PROOF STATE]
proof (prove)
using this:
k \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}

goal (1 subgoal):
 1. nat \<lfloor>primes_pi (real (nth_prime k))\<rfloor> - 1 = k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat \<lfloor>primes_pi (real (nth_prime k))\<rfloor> - 1 = k

goal (1 subgoal):
 1. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
[PROOF STEP]
from k
[PROOF STATE]
proof (chain)
picking this:
k \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}
[PROOF STEP]
have "\<not>(x < 2)"
[PROOF STATE]
proof (prove)
using this:
k \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}

goal (1 subgoal):
 1. \<not> x < 2
[PROOF STEP]
by (intro notI) auto
[PROOF STATE]
proof (state)
this:
\<not> x < 2

goal (1 subgoal):
 1. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
[PROOF STEP]
hence "x \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
\<not> x < 2

goal (1 subgoal):
 1. 2 \<le> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 \<le> x

goal (1 subgoal):
 1. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
[PROOF STEP]
have "real (nth_prime k) \<le> real (nth_prime (nat \<lfloor>primes_pi x\<rfloor> - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (nth_prime k) \<le> real (nth_prime (nat \<lfloor>primes_pi x\<rfloor> - 1))
[PROOF STEP]
using k
[PROOF STATE]
proof (prove)
using this:
k \<in> {..<nat \<lfloor>primes_pi x\<rfloor>}

goal (1 subgoal):
 1. real (nth_prime k) \<le> real (nth_prime (nat \<lfloor>primes_pi x\<rfloor> - 1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (nth_prime k) \<le> real (nth_prime (nat \<lfloor>primes_pi x\<rfloor> - 1))

goal (1 subgoal):
 1. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
real (nth_prime k) \<le> real (nth_prime (nat \<lfloor>primes_pi x\<rfloor> - 1))

goal (1 subgoal):
 1. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
[PROOF STEP]
have "\<dots> \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (nth_prime (nat \<lfloor>primes_pi x\<rfloor> - 1)) \<le> x
[PROOF STEP]
using nth_prime_partition''[of x] \<open>x \<ge> 2\<close>
[PROOF STATE]
proof (prove)
using this:
2 \<le> x \<Longrightarrow> x \<in> {real (nth_prime (nat \<lfloor>primes_pi x\<rfloor> - 1))..<real (nth_prime (nat \<lfloor>primes_pi x\<rfloor>))}
2 \<le> x

goal (1 subgoal):
 1. real (nth_prime (nat \<lfloor>primes_pi x\<rfloor> - 1)) \<le> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (nth_prime (nat \<lfloor>primes_pi x\<rfloor> - 1)) \<le> x

goal (1 subgoal):
 1. \<And>b. b \<in> {..<nat \<lfloor>primes_pi x\<rfloor>} \<Longrightarrow> nth_prime b \<in> {p. prime p \<and> real p \<le> x}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
real (nth_prime k) \<le> x
[PROOF STEP]
show "nth_prime k \<in> {p. prime p \<and> real p \<le> x}"
[PROOF STATE]
proof (prove)
using this:
real (nth_prime k) \<le> x

goal (1 subgoal):
 1. nth_prime k \<in> {p. prime p \<and> real p \<le> x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nth_prime k \<in> {p. prime p \<and> real p \<le> x}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma primorial'_conv_primorial:
  assumes "n > 0"
  shows   "primorial' n = primorial (nth_prime (n - 1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primorial' n = primorial (real (nth_prime (n - 1)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. primorial' n = primorial (real (nth_prime (n - 1)))
[PROOF STEP]
have "primorial (nth_prime (n - 1)) = (\<Prod>k<nat (int (n - 1) + 1). nth_prime k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primorial (real (nth_prime (n - 1))) = prod nth_prime {..<nat (int (n - 1) + 1)}
[PROOF STEP]
by (simp add: primorial_conv_primorial' primorial'_def)
[PROOF STATE]
proof (state)
this:
primorial (real (nth_prime (n - 1))) = prod nth_prime {..<nat (int (n - 1) + 1)}

goal (1 subgoal):
 1. primorial' n = primorial (real (nth_prime (n - 1)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
primorial (real (nth_prime (n - 1))) = prod nth_prime {..<nat (int (n - 1) + 1)}

goal (1 subgoal):
 1. primorial' n = primorial (real (nth_prime (n - 1)))
[PROOF STEP]
have "nat (int (n - 1) + 1) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat (int (n - 1) + 1) = n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. nat (int (n - 1) + 1) = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat (int (n - 1) + 1) = n

goal (1 subgoal):
 1. primorial' n = primorial (real (nth_prime (n - 1)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
primorial (real (nth_prime (n - 1))) = prod nth_prime {..<n}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
primorial (real (nth_prime (n - 1))) = prod nth_prime {..<n}

goal (1 subgoal):
 1. primorial' n = primorial (real (nth_prime (n - 1)))
[PROOF STEP]
by (simp add: primorial'_def)
[PROOF STATE]
proof (state)
this:
primorial' n = primorial (real (nth_prime (n - 1)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nth_prime_le_prime_sequence:
  fixes p :: "nat \<Rightarrow> nat"
  assumes "strict_mono_on {..<n} p" and "\<And>k. k < n \<Longrightarrow> prime (p k)" and "k < n"
  shows   "nth_prime k \<le> p k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_prime k \<le> p k
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
k < n

goal (1 subgoal):
 1. nth_prime k \<le> p k
[PROOF STEP]
proof (induction k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. 0 < n \<Longrightarrow> nth_prime 0 \<le> p 0
 2. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 < n

goal (2 subgoals):
 1. 0 < n \<Longrightarrow> nth_prime 0 \<le> p 0
 2. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
hence "prime (p 0)"
[PROOF STATE]
proof (prove)
using this:
0 < n

goal (1 subgoal):
 1. prime (p 0)
[PROOF STEP]
by (intro assms)
[PROOF STATE]
proof (state)
this:
prime (p 0)

goal (2 subgoals):
 1. 0 < n \<Longrightarrow> nth_prime 0 \<le> p 0
 2. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
hence "p 0 \<ge> 2"
[PROOF STATE]
proof (prove)
using this:
prime (p 0)

goal (1 subgoal):
 1. 2 \<le> p 0
[PROOF STEP]
by (auto dest: prime_gt_1_nat)
[PROOF STATE]
proof (state)
this:
2 \<le> p 0

goal (2 subgoals):
 1. 0 < n \<Longrightarrow> nth_prime 0 \<le> p 0
 2. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
2 \<le> p 0

goal (1 subgoal):
 1. nth_prime 0 \<le> p 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nth_prime 0 \<le> p 0

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
k < n \<Longrightarrow> nth_prime k \<le> p k
Suc k < n

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
have IH: "Suc (nth_prime k) \<le> Suc (p k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (nth_prime k) \<le> Suc (p k)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
k < n \<Longrightarrow> nth_prime k \<le> p k
Suc k < n

goal (1 subgoal):
 1. Suc (nth_prime k) \<le> Suc (p k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (nth_prime k) \<le> Suc (p k)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
have "nth_prime (Suc k) = smallest_prime_beyond (Suc (nth_prime k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nth_prime (Suc k) = smallest_prime_beyond (Suc (nth_prime k))
[PROOF STEP]
by (simp add: nth_prime_Suc)
[PROOF STATE]
proof (state)
this:
nth_prime (Suc k) = smallest_prime_beyond (Suc (nth_prime k))

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nth_prime (Suc k) = smallest_prime_beyond (Suc (nth_prime k))

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
nth_prime (Suc k) = smallest_prime_beyond (Suc (nth_prime k))

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
have "Suc (nth_prime k) \<le> Suc (p k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (nth_prime k) \<le> Suc (p k)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
k < n \<Longrightarrow> nth_prime k \<le> p k
Suc k < n

goal (1 subgoal):
 1. Suc (nth_prime k) \<le> Suc (p k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Suc (nth_prime k) \<le> Suc (p k)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc (nth_prime k) \<le> Suc (p k)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
have "\<dots> \<le> smallest_prime_beyond (Suc (p k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (p k) \<le> smallest_prime_beyond (Suc (p k))
[PROOF STEP]
by (rule smallest_prime_beyond_le)
[PROOF STATE]
proof (state)
this:
Suc (p k) \<le> smallest_prime_beyond (Suc (p k))

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Suc (nth_prime k) \<le> smallest_prime_beyond (Suc (p k))
[PROOF STEP]
have "smallest_prime_beyond (Suc (nth_prime k)) \<le> smallest_prime_beyond (Suc (p k))"
[PROOF STATE]
proof (prove)
using this:
Suc (nth_prime k) \<le> smallest_prime_beyond (Suc (p k))

goal (1 subgoal):
 1. smallest_prime_beyond (Suc (nth_prime k)) \<le> smallest_prime_beyond (Suc (p k))
[PROOF STEP]
by (rule smallest_prime_beyond_smallest[OF prime_smallest_prime_beyond])
[PROOF STATE]
proof (state)
this:
smallest_prime_beyond (Suc (nth_prime k)) \<le> smallest_prime_beyond (Suc (p k))

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
smallest_prime_beyond (Suc (nth_prime k)) \<le> smallest_prime_beyond (Suc (p k))

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
smallest_prime_beyond (Suc (nth_prime k)) \<le> smallest_prime_beyond (Suc (p k))

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
have "p k < p (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p k < p (Suc k)
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
k < n \<Longrightarrow> nth_prime k \<le> p k
Suc k < n

goal (1 subgoal):
 1. p k < p (Suc k)
[PROOF STEP]
by (intro strict_mono_onD[OF assms(1)]) auto
[PROOF STATE]
proof (state)
this:
p k < p (Suc k)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
hence "smallest_prime_beyond (Suc (p k)) \<le> p (Suc k)"
[PROOF STATE]
proof (prove)
using this:
p k < p (Suc k)

goal (1 subgoal):
 1. smallest_prime_beyond (Suc (p k)) \<le> p (Suc k)
[PROOF STEP]
using Suc.prems
[PROOF STATE]
proof (prove)
using this:
p k < p (Suc k)
Suc k < n

goal (1 subgoal):
 1. smallest_prime_beyond (Suc (p k)) \<le> p (Suc k)
[PROOF STEP]
by (intro smallest_prime_beyond_smallest assms) auto
[PROOF STATE]
proof (state)
this:
smallest_prime_beyond (Suc (p k)) \<le> p (Suc k)

goal (1 subgoal):
 1. \<And>k. \<lbrakk>k < n \<Longrightarrow> nth_prime k \<le> p k; Suc k < n\<rbrakk> \<Longrightarrow> nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
nth_prime (Suc k) \<le> p (Suc k)

goal (1 subgoal):
 1. nth_prime (Suc k) \<le> p (Suc k)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
nth_prime (Suc k) \<le> p (Suc k)

goal:
No subgoals!
[PROOF STEP]
qed