[STATEMENT]
lemma bisim_J1_JVM_start:
  assumes wf: "wf_J1_prog P"
  and wf_start: "wf_start_state P C M vs"
  shows "Red1_execd.mbisim (J1_start_state P C M vs) (JVM_start_state (compP2 P) C M vs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
from wf_start
[PROOF STATE]
proof (chain)
picking this:
wf_start_state P C M vs
[PROOF STEP]
obtain Ts T body D where start: "start_heap_ok"
  and sees: "P \<turnstile> C sees M:Ts\<rightarrow>T=\<lfloor>body\<rfloor> in D" and conf: "P,start_heap \<turnstile> vs [:\<le>] Ts"
[PROOF STATE]
proof (prove)
using this:
wf_start_state P C M vs

goal (1 subgoal):
 1. (\<And>Ts T body D. \<lbrakk>start_heap_ok; P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D; P,start_heap \<turnstile> vs [:\<le>] Ts\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases
[PROOF STATE]
proof (state)
this:
start_heap_ok
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D
P,start_heap \<turnstile> vs [:\<le>] Ts

goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
let ?e = "blocks1 0 (Class D#Ts) body"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
let ?xs = "Null # vs @ replicate (max_vars body) undefined_value"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
from sees_wf_mdecl[OF wf sees]
[PROOF STATE]
proof (chain)
picking this:
wf_mdecl wf_J1_mdecl P D (M, Ts, T, \<lfloor>body\<rfloor>)
[PROOF STEP]
obtain T'
    where B: "\<B> body (Suc (length Ts))"
    and wt: "P,Class D # Ts \<turnstile>1 body :: T'"
    and da: "\<D> body \<lfloor>{..length Ts}\<rfloor>"
    and sv: "syncvars body"
[PROOF STATE]
proof (prove)
using this:
wf_mdecl wf_J1_mdecl P D (M, Ts, T, \<lfloor>body\<rfloor>)

goal (1 subgoal):
 1. (\<And>T'. \<lbrakk>\<B> body (Suc (length Ts)); P,Class D # Ts \<turnstile>1 body :: T'; \<D> body \<lfloor>{..length Ts}\<rfloor>; syncvars body\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: wf_mdecl_def)
[PROOF STATE]
proof (state)
this:
\<B> body (Suc (length Ts))
P,Class D # Ts \<turnstile>1 body :: T'
\<D> body \<lfloor>{..length Ts}\<rfloor>
syncvars body

goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
have "P,?e,start_heap \<turnstile> (?e, ?xs) \<leftrightarrow> ([], ?xs, 0, None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,blocks1 0 (Class D # Ts) body,start_heap \<turnstile> (blocks1 0 (Class D # Ts) body, Null # vs @ replicate (max_vars body) undefined_value) \<leftrightarrow> ([], Null # vs @ replicate (max_vars body) undefined_value, 0, None)
[PROOF STEP]
by(rule bisim1_refl)
[PROOF STATE]
proof (state)
this:
P,blocks1 0 (Class D # Ts) body,start_heap \<turnstile> (blocks1 0 (Class D # Ts) body, Null # vs @ replicate (max_vars body) undefined_value) \<leftrightarrow> ([], Null # vs @ replicate (max_vars body) undefined_value, 0, None)

goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P,blocks1 0 (Class D # Ts) body,start_heap \<turnstile> (blocks1 0 (Class D # Ts) body, Null # vs @ replicate (max_vars body) undefined_value) \<leftrightarrow> ([], Null # vs @ replicate (max_vars body) undefined_value, 0, None)

goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
from wf
[PROOF STATE]
proof (chain)
picking this:
wf_J1_prog P
[PROOF STEP]
have wf': "wf_jvm_prog\<^bsub>compTP P\<^esub> (compP2 P)"
[PROOF STATE]
proof (prove)
using this:
wf_J1_prog P

goal (1 subgoal):
 1. wf_jvm_prog\<^bsub>compTP P\<^esub> (compP2 P)
[PROOF STEP]
by(rule wt_compTP_compP2)
[PROOF STATE]
proof (state)
this:
wf_jvm_prog\<^bsub>compTP P\<^esub> (compP2 P)

goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
from sees_method_compP[OF sees, of "\<lambda>C M Ts T. compMb2"]
[PROOF STATE]
proof (chain)
picking this:
compP (\<lambda>C M Ts T. compMb2) P \<turnstile> C sees M: Ts\<rightarrow>T = map_option compMb2 \<lfloor>body\<rfloor> in D
[PROOF STEP]
have sees': "compP2 P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>compMb2 body\<rfloor> in D"
[PROOF STATE]
proof (prove)
using this:
compP (\<lambda>C M Ts T. compMb2) P \<turnstile> C sees M: Ts\<rightarrow>T = map_option compMb2 \<lfloor>body\<rfloor> in D

goal (1 subgoal):
 1. compP2 P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>compMb2 body\<rfloor> in D
[PROOF STEP]
by(simp add: compP2_def)
[PROOF STATE]
proof (state)
this:
compP2 P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>compMb2 body\<rfloor> in D

goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
from conf
[PROOF STATE]
proof (chain)
picking this:
P,start_heap \<turnstile> vs [:\<le>] Ts
[PROOF STEP]
have "compP2 P,start_heap \<turnstile> vs [:\<le>] Ts"
[PROOF STATE]
proof (prove)
using this:
P,start_heap \<turnstile> vs [:\<le>] Ts

goal (1 subgoal):
 1. compP2 P,start_heap \<turnstile> vs [:\<le>] Ts
[PROOF STEP]
by(simp add: compP2_def heap_base.compP_confs)
[PROOF STATE]
proof (state)
this:
compP2 P,start_heap \<turnstile> vs [:\<le>] Ts

goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
from BV_correct_initial[OF wf' start sees' this] sees'
[PROOF STATE]
proof (chain)
picking this:
compTP P \<turnstile> start_tid:JVM_start_state' (compP2 P) C M vs \<surd>
compP2 P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>compMb2 body\<rfloor> in D
[PROOF STEP]
have "compTP P \<turnstile> start_tid:(None, start_heap, [([], ?xs, D, M, 0)]) \<surd>"
[PROOF STATE]
proof (prove)
using this:
compTP P \<turnstile> start_tid:JVM_start_state' (compP2 P) C M vs \<surd>
compP2 P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>compMb2 body\<rfloor> in D

goal (1 subgoal):
 1. compTP P \<turnstile> start_tid:(None, start_heap, [([], Null # vs @ replicate (max_vars body) undefined_value, D, M, 0)]) \<surd>
[PROOF STEP]
by(simp add: JVM_start_state'_def compP2_def compMb2_def)
[PROOF STATE]
proof (state)
this:
compTP P \<turnstile> start_tid:(None, start_heap, [([], Null # vs @ replicate (max_vars body) undefined_value, D, M, 0)]) \<surd>

goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
hence "bisim1_list1 start_tid start_heap (?e, ?xs) [] None [([], ?xs, D, M, 0)]"
[PROOF STATE]
proof (prove)
using this:
compTP P \<turnstile> start_tid:(None, start_heap, [([], Null # vs @ replicate (max_vars body) undefined_value, D, M, 0)]) \<surd>

goal (1 subgoal):
 1. bisim1_list1 start_tid start_heap (blocks1 0 (Class D # Ts) body, Null # vs @ replicate (max_vars body) undefined_value) [] None [([], Null # vs @ replicate (max_vars body) undefined_value, D, M, 0)]
[PROOF STEP]
using sees_method_idemp[OF sees]
[PROOF STATE]
proof (prove)
using this:
compTP P \<turnstile> start_tid:(None, start_heap, [([], Null # vs @ replicate (max_vars body) undefined_value, D, M, 0)]) \<surd>
P \<turnstile> D sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D

goal (1 subgoal):
 1. bisim1_list1 start_tid start_heap (blocks1 0 (Class D # Ts) body, Null # vs @ replicate (max_vars body) undefined_value) [] None [([], Null # vs @ replicate (max_vars body) undefined_value, D, M, 0)]
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. P,blocks1 0 (Class D # Ts) body,start_heap \<turnstile> (blocks1 0 (Class D # Ts) body, Null # vs @ replicate (max_vars body) undefined_value) \<leftrightarrow> ([], Null # vs @ replicate (max_vars body) undefined_value, 0, None)
 2. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Null # vs @ replicate (max_vars body) undefined_value)
 3. list_all2 (bisim1_fr P start_heap) [] []
[PROOF STEP]
show "P,?e,start_heap \<turnstile> (?e, ?xs) \<leftrightarrow> ([], ?xs, 0, None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P,blocks1 0 (Class D # Ts) body,start_heap \<turnstile> (blocks1 0 (Class D # Ts) body, Null # vs @ replicate (max_vars body) undefined_value) \<leftrightarrow> ([], Null # vs @ replicate (max_vars body) undefined_value, 0, None)
[PROOF STEP]
by(rule bisim1_refl)
[PROOF STATE]
proof (state)
this:
P,blocks1 0 (Class D # Ts) body,start_heap \<turnstile> (blocks1 0 (Class D # Ts) body, Null # vs @ replicate (max_vars body) undefined_value) \<leftrightarrow> ([], Null # vs @ replicate (max_vars body) undefined_value, 0, None)

goal (2 subgoals):
 1. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Null # vs @ replicate (max_vars body) undefined_value)
 2. list_all2 (bisim1_fr P start_heap) [] []
[PROOF STEP]
show "max_vars ?e \<le> length ?xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Null # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
using conf
[PROOF STATE]
proof (prove)
using this:
P,start_heap \<turnstile> vs [:\<le>] Ts

goal (1 subgoal):
 1. max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Null # vs @ replicate (max_vars body) undefined_value)
[PROOF STEP]
by(auto simp add: blocks1_max_vars dest: list_all2_lengthD)
[PROOF STATE]
proof (state)
this:
max_vars (blocks1 0 (Class D # Ts) body) \<le> length (Null # vs @ replicate (max_vars body) undefined_value)

goal (1 subgoal):
 1. list_all2 (bisim1_fr P start_heap) [] []
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
bisim1_list1 start_tid start_heap (blocks1 0 (Class D # Ts) body, Null # vs @ replicate (max_vars body) undefined_value) [] None [([], Null # vs @ replicate (max_vars body) undefined_value, D, M, 0)]

goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
bisim1_list1 start_tid start_heap (blocks1 0 (Class D # Ts) body, Null # vs @ replicate (max_vars body) undefined_value) [] None [([], Null # vs @ replicate (max_vars body) undefined_value, D, M, 0)]

goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
using sees sees'
[PROOF STATE]
proof (prove)
using this:
bisim1_list1 start_tid start_heap (blocks1 0 (Class D # Ts) body, Null # vs @ replicate (max_vars body) undefined_value) [] None [([], Null # vs @ replicate (max_vars body) undefined_value, D, M, 0)]
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D
compP2 P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>compMb2 body\<rfloor> in D

goal (1 subgoal):
 1. Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)
[PROOF STEP]
unfolding start_state_def
[PROOF STATE]
proof (prove)
using this:
bisim1_list1 start_tid start_heap (blocks1 0 (Class D # Ts) body, Null # vs @ replicate (max_vars body) undefined_value) [] None [([], Null # vs @ replicate (max_vars body) undefined_value, D, M, 0)]
P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>body\<rfloor> in D
compP2 P \<turnstile> C sees M: Ts\<rightarrow>T = \<lfloor>compMb2 body\<rfloor> in D

goal (1 subgoal):
 1. Red1_execd.mbisim (let (D, Ts, T, m) = method P C M in (K$ None, ([start_tid \<mapsto> (((blocks1 0 (Class D # Ts) (the m), Null # vs @ replicate (max_vars (the m)) undefined_value), []), no_wait_locks)], start_heap), Map.empty, {})) (let (D, Ts, T, m) = method (compP2 P) C M in (K$ None, ([start_tid \<mapsto> ((case the m of (mxs, mxl0, b) \<Rightarrow> \<lambda>vs. (None, [([], Null # vs @ replicate mxl0 undefined_value, D, M, 0)])) vs, no_wait_locks)], start_heap), Map.empty, {}))
[PROOF STEP]
by -(rule Red1_execd.mbisimI, auto split: if_split_asm intro: wset_thread_okI simp add: compP2_def compMb2_def)
[PROOF STATE]
proof (state)
this:
Red1_execd.mbisim (J1_start_state P C M vs) (start_state JVM_local_start (compP2 P) C M vs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma document_ptr_kinds_simp [simp]:
  "document_ptr_kinds (Heap (fmupd (cast document_ptr) document (the_heap h)))
          = {|document_ptr|} |\<union>| document_ptr_kinds h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. document_ptr_kinds (Heap (fmupd (cast document_ptr) document (the_heap h))) = {|document_ptr|} |\<union>| document_ptr_kinds h
[PROOF STEP]
apply(auto simp add: document_ptr_kinds_def)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. document_ptr |\<in>| (the \<circ> cast) |`| ffilter is_document_ptr_kind (finsert (cast document_ptr) (object_ptr_kinds h))
[PROOF STEP]
by force


[STATEMENT]
lemma document_ptr_kinds_commutes [simp]:
  "cast document_ptr |\<in>| object_ptr_kinds h \<longleftrightarrow> document_ptr |\<in>| document_ptr_kinds h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cast document_ptr |\<in>| object_ptr_kinds h) = (document_ptr |\<in>| document_ptr_kinds h)
[PROOF STEP]
apply(auto simp add: object_ptr_kinds_def document_ptr_kinds_def)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast document_ptr |\<in>| fmdom (the_heap h) \<Longrightarrow> document_ptr |\<in>| (the \<circ> cast) |`| ffilter is_document_ptr_kind (fmdom (the_heap h))
[PROOF STEP]
by (metis (no_types, lifting) document_ptr_casts_commute2 document_ptr_document_ptr_cast
      ffmember_filter fimage_eqI fset.map_comp option.sel)


[STATEMENT]
lemma get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_type_wf:
  assumes "type_wf h"
  shows "document_ptr |\<in>| document_ptr_kinds h \<longleftrightarrow> get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr h \<noteq> None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (document_ptr |\<in>| document_ptr_kinds h) = (get document_ptr h \<noteq> None)
[PROOF STEP]
using l_type_wf\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_axioms assms
[PROOF STATE]
proof (prove)
using this:
l_type_wf\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t type_wf
type_wf h

goal (1 subgoal):
 1. (document_ptr |\<in>| document_ptr_kinds h) = (get document_ptr h \<noteq> None)
[PROOF STEP]
apply(simp add: type_wf_defs get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def l_type_wf\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>h. type_wf h \<longrightarrow> CharacterDataClass.type_wf h \<and> (\<forall>document_ptr\<in>fset (document_ptr_kinds h). \<exists>y. Option.bind (get (cast document_ptr) h) cast = Some y); type_wf h\<rbrakk> \<Longrightarrow> (document_ptr |\<in>| document_ptr_kinds h) = (\<exists>y. Option.bind (get (cast document_ptr) h) cast = Some y)
[PROOF STEP]
by (metis document_ptr_kinds_commutes fmember.rep_eq is_none_bind is_none_simps(1)
      is_none_simps(2) local.get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_type_wf)


[STATEMENT]
lemma put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_in_heap:
  assumes "put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr document h = h'"
  shows "document_ptr |\<in>| document_ptr_kinds h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. document_ptr |\<in>| document_ptr_kinds h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
put document_ptr document h = h'

goal (1 subgoal):
 1. document_ptr |\<in>| document_ptr_kinds h'
[PROOF STEP]
unfolding put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def
[PROOF STATE]
proof (prove)
using this:
put (cast document_ptr) (cast document) h = h'

goal (1 subgoal):
 1. document_ptr |\<in>| document_ptr_kinds h'
[PROOF STEP]
by (metis document_ptr_kinds_commutes put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_ptr_in_heap)


[STATEMENT]
lemma put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_put_ptrs:
  assumes "put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr document h = h'"
  shows "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|cast document_ptr|}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|cast document_ptr|}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
put document_ptr document h = h'

goal (1 subgoal):
 1. object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|cast document_ptr|}
[PROOF STEP]
by (simp add: put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_put_ptrs)


[STATEMENT]
lemma cast\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_inject [simp]: "cast\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t x = cast\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cast x = cast y) = (x = y)
[PROOF STEP]
apply(simp add: cast\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def RObject.extend_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (RObject.more x = RObject.more y) = (x = y)
[PROOF STEP]
by (metis (full_types) RObject.surjective old.unit.exhaust)


[STATEMENT]
lemma cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_none [simp]:
  "cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t obj = None \<longleftrightarrow> \<not> (\<exists>document. cast\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t document = obj)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cast obj = None) = (\<nexists>document. cast document = obj)
[PROOF STEP]
apply(auto simp add: cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def cast\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def RObject.extend_def
      split: sum.splits)[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x1. RObject.more obj = Inr (Inl x1) \<Longrightarrow> \<exists>document. \<lparr>RObject.nothing = (), \<dots> = Inr (Inl (RObject.more document))\<rparr> = obj
[PROOF STEP]
by (metis (full_types) RObject.select_convs(2) RObject.surjective old.unit.exhaust)


[STATEMENT]
lemma cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_some [simp]:
  "cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t obj = Some document \<longleftrightarrow> cast document = obj"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cast obj = Some document) = (cast document = obj)
[PROOF STEP]
by(auto simp add: cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def cast\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def RObject.extend_def
      split: sum.splits)


[STATEMENT]
lemma cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_inv [simp]: "cast\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t\<^sub>2\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t (cast\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t document) = Some document"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast (cast document) = Some document
[PROOF STEP]
by simp


[STATEMENT]
lemma cast_document_not_node [simp]:
  "cast\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t document \<noteq> cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t node"
  "cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t node \<noteq> cast\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t document"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cast document \<noteq> cast node &&& cast node \<noteq> cast document
[PROOF STEP]
by(auto simp add: cast\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def cast\<^sub>N\<^sub>o\<^sub>d\<^sub>e\<^sub>2\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t_def RObject.extend_def)


[STATEMENT]
lemma get_document_ptr_simp1 [simp]:
  "get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr (put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr document h) = Some document"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get document_ptr (put document_ptr document h) = Some document
[PROOF STEP]
by(auto simp add: get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)


[STATEMENT]
lemma get_document_ptr_simp2 [simp]:
  "document_ptr \<noteq> document_ptr'
   \<Longrightarrow> get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr (put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr' document h) = get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. document_ptr \<noteq> document_ptr' \<Longrightarrow> get document_ptr (put document_ptr' document h) = get document_ptr h
[PROOF STEP]
by(auto simp add: get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)


[STATEMENT]
lemma get_document_ptr_simp3 [simp]:
  "get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr (put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr f h) = get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get element_ptr (put document_ptr f h) = get element_ptr h
[PROOF STEP]
by(auto simp add: get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)


[STATEMENT]
lemma get_document_ptr_simp4 [simp]:
  "get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr (put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t element_ptr f h) = get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get document_ptr (put element_ptr f h) = get document_ptr h
[PROOF STEP]
by(auto simp add: get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)


[STATEMENT]
lemma get_document_ptr_simp5 [simp]:
  "get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr (put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr f h) = get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get character_data_ptr (put document_ptr f h) = get character_data_ptr h
[PROOF STEP]
by(auto simp add: get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)


[STATEMENT]
lemma get_document_ptr_simp6 [simp]:
  "get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr (put\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a character_data_ptr f h) = get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t document_ptr h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get document_ptr (put character_data_ptr f h) = get document_ptr h
[PROOF STEP]
by(auto simp add: get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def put\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)


[STATEMENT]
lemma new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t [simp]:
  assumes "new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_element_ptr, h')"
  shows "get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr h = get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get ptr h = get ptr h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_element_ptr, h')

goal (1 subgoal):
 1. get ptr h = get ptr h'
[PROOF STEP]
by(auto simp add: new\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def)


[STATEMENT]
lemma new\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t [simp]:
  assumes "new\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a h = (new_character_data_ptr, h')"
  shows "get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr h = get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get ptr h = get ptr h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
new\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a h = (new_character_data_ptr, h')

goal (1 subgoal):
 1. get ptr h = get ptr h'
[PROOF STEP]
by(auto simp add: new\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a_def Let_def)


[STATEMENT]
lemma new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_in_heap:
  assumes "new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')"
  shows "new_document_ptr |\<in>| document_ptr_kinds h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_document_ptr |\<in>| document_ptr_kinds h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')

goal (1 subgoal):
 1. new_document_ptr |\<in>| document_ptr_kinds h'
[PROOF STEP]
unfolding new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def
[PROOF STATE]
proof (prove)
using this:
(document_ptr.Ref (Suc (fMax (finsert 0 (document_ptr.the_ref |`| document_ptrs h)))), put (document_ptr.Ref (Suc (fMax (finsert 0 (document_ptr.the_ref |`| document_ptrs h))))) (create_document_obj [] None []) h) = (new_document_ptr, h')

goal (1 subgoal):
 1. new_document_ptr |\<in>| document_ptr_kinds h'
[PROOF STEP]
using put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_in_heap
[PROOF STATE]
proof (prove)
using this:
(document_ptr.Ref (Suc (fMax (finsert 0 (document_ptr.the_ref |`| document_ptrs h)))), put (document_ptr.Ref (Suc (fMax (finsert 0 (document_ptr.the_ref |`| document_ptrs h))))) (create_document_obj [] None []) h) = (new_document_ptr, h')
put ?document_ptr ?document ?h = ?h' \<Longrightarrow> ?document_ptr |\<in>| document_ptr_kinds ?h'

goal (1 subgoal):
 1. new_document_ptr |\<in>| document_ptr_kinds h'
[PROOF STEP]
by blast


[STATEMENT]
lemma new_document_ptr_new:
  "document_ptr.Ref (Suc (fMax (finsert 0 (document_ptr.the_ref |`| document_ptrs h))))
      |\<notin>| document_ptrs h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. document_ptr.Ref (Suc (fMax (finsert 0 (document_ptr.the_ref |`| document_ptrs h)))) |\<notin>| document_ptrs h
[PROOF STEP]
by (metis Suc_n_not_le_n document_ptr.sel(1) fMax_ge fimage_finsert finsertI1 finsertI2 set_finsert)


[STATEMENT]
lemma new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_ptr_not_in_heap:
  assumes "new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')"
  shows "new_document_ptr |\<notin>| document_ptr_kinds h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. new_document_ptr |\<notin>| document_ptr_kinds h
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')

goal (1 subgoal):
 1. new_document_ptr |\<notin>| document_ptr_kinds h
[PROOF STEP]
unfolding new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def
[PROOF STATE]
proof (prove)
using this:
(let new_document_ptr = document_ptr.Ref (Suc (fMax (finsert 0 (document_ptr.the_ref |`| document_ptrs h)))) in (new_document_ptr, put new_document_ptr (create_document_obj [] None []) h)) = (new_document_ptr, h')

goal (1 subgoal):
 1. new_document_ptr |\<notin>| document_ptr_kinds h
[PROOF STEP]
by (metis Pair_inject document_ptrs_def fMax_finsert fempty_iff ffmember_filter
      fimage_is_fempty is_document_ptr_ref max_0L new_document_ptr_new)


[STATEMENT]
lemma new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_new_ptr:
  assumes "new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')"
  shows "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|cast new_document_ptr|}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|cast new_document_ptr|}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')

goal (1 subgoal):
 1. object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|cast new_document_ptr|}
[PROOF STEP]
by (metis Pair_inject new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_put_ptrs)


[STATEMENT]
lemma new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_is_document_ptr:
  assumes "new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')"
  shows "is_document_ptr new_document_ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_document_ptr new_document_ptr
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')

goal (1 subgoal):
 1. is_document_ptr new_document_ptr
[PROOF STEP]
by(auto simp add: new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def)


[STATEMENT]
lemma new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t [simp]:
  assumes "new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')"
  assumes "ptr \<noteq> cast new_document_ptr"
  shows "get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr h = get\<^sub>O\<^sub>b\<^sub>j\<^sub>e\<^sub>c\<^sub>t ptr h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get ptr h = get ptr h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')
ptr \<noteq> cast new_document_ptr

goal (1 subgoal):
 1. get ptr h = get ptr h'
[PROOF STEP]
by(auto simp add: new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)


[STATEMENT]
lemma new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_get\<^sub>N\<^sub>o\<^sub>d\<^sub>e [simp]:
  assumes "new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')"
  shows "get\<^sub>N\<^sub>o\<^sub>d\<^sub>e ptr h = get\<^sub>N\<^sub>o\<^sub>d\<^sub>e ptr h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get ptr h = get ptr h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')

goal (1 subgoal):
 1. get ptr h = get ptr h'
[PROOF STEP]
apply(simp add: new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def put\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. document_ptr.Ref (Suc (if document_ptrs h = {||} then 0 else max 0 (fMax (document_ptr.the_ref |`| document_ptrs h)))) = new_document_ptr \<and> put (cast (document_ptr.Ref (Suc (if document_ptrs h = {||} then 0 else max 0 (fMax (document_ptr.the_ref |`| document_ptrs h)))))) (cast (create_document_obj [] None [])) h = h' \<Longrightarrow> get ptr h = get ptr h'
[PROOF STEP]
by(auto simp add: get\<^sub>N\<^sub>o\<^sub>d\<^sub>e_def)


[STATEMENT]
lemma new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t [simp]:
  assumes "new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')"
  shows "get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr h = get\<^sub>E\<^sub>l\<^sub>e\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get ptr h = get ptr h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')

goal (1 subgoal):
 1. get ptr h = get ptr h'
[PROOF STEP]
by(auto simp add: new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def)


[STATEMENT]
lemma new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a [simp]:
  assumes "new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')"
  shows "get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a ptr h = get\<^sub>C\<^sub>h\<^sub>a\<^sub>r\<^sub>a\<^sub>c\<^sub>t\<^sub>e\<^sub>r\<^sub>D\<^sub>a\<^sub>t\<^sub>a ptr h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get ptr h = get ptr h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')

goal (1 subgoal):
 1. get ptr h = get ptr h'
[PROOF STEP]
by(auto simp add: new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def)


[STATEMENT]
lemma new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t [simp]:
  assumes "new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')"
  assumes "ptr \<noteq> new_document_ptr"
  shows "get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr h = get\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t ptr h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get ptr h = get ptr h'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t h = (new_document_ptr, h')
ptr \<noteq> new_document_ptr

goal (1 subgoal):
 1. get ptr h = get ptr h'
[PROOF STEP]
by(auto simp add: new\<^sub>D\<^sub>o\<^sub>c\<^sub>u\<^sub>m\<^sub>e\<^sub>n\<^sub>t_def Let_def)


[STATEMENT]
lemma known_ptr_not_document_ptr: "\<not>is_document_ptr ptr \<Longrightarrow> a_known_ptr ptr \<Longrightarrow> known_ptr ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> (case cast ptr of None \<Rightarrow> False | Some document_ptr \<Rightarrow> is_document_ptr document_ptr); local.a_known_ptr ptr\<rbrakk> \<Longrightarrow> CharacterDataClass.known_ptr ptr
[PROOF STEP]
by(simp add: a_known_ptr_def)


[STATEMENT]
lemma known_ptrs_known_ptr: "a_known_ptrs h \<Longrightarrow> ptr |\<in>| object_ptr_kinds h \<Longrightarrow> known_ptr ptr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.a_known_ptrs h; ptr |\<in>| object_ptr_kinds h\<rbrakk> \<Longrightarrow> known_ptr ptr
[PROOF STEP]
apply(simp add: a_known_ptrs_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>ptr\<in>fset (object_ptr_kinds h). known_ptr ptr; ptr |\<in>| object_ptr_kinds h\<rbrakk> \<Longrightarrow> known_ptr ptr
[PROOF STEP]
using notin_fset
[PROOF STATE]
proof (prove)
using this:
(?x |\<notin>| ?S) = (?x \<notin> fset ?S)

goal (1 subgoal):
 1. \<lbrakk>\<forall>ptr\<in>fset (object_ptr_kinds h). known_ptr ptr; ptr |\<in>| object_ptr_kinds h\<rbrakk> \<Longrightarrow> known_ptr ptr
[PROOF STEP]
by fastforce


[STATEMENT]
lemma known_ptrs_preserved:
  "object_ptr_kinds h = object_ptr_kinds h' \<Longrightarrow> a_known_ptrs h = a_known_ptrs h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. object_ptr_kinds h = object_ptr_kinds h' \<Longrightarrow> local.a_known_ptrs h = local.a_known_ptrs h'
[PROOF STEP]
by(auto simp add: a_known_ptrs_def)


[STATEMENT]
lemma known_ptrs_subset:
  "object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<Longrightarrow> a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h; local.a_known_ptrs h\<rbrakk> \<Longrightarrow> local.a_known_ptrs h'
[PROOF STEP]
by(simp add: a_known_ptrs_def less_eq_fset.rep_eq subsetD)


[STATEMENT]
lemma known_ptrs_new_ptr:
  "object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<Longrightarrow> known_ptr new_ptr \<Longrightarrow>
a_known_ptrs h \<Longrightarrow> a_known_ptrs h'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|}; known_ptr new_ptr; local.a_known_ptrs h\<rbrakk> \<Longrightarrow> local.a_known_ptrs h'
[PROOF STEP]
by(simp add: a_known_ptrs_def)


[STATEMENT]
lemma known_ptrs_is_l_known_ptrs  [instances]: "l_known_ptrs known_ptr known_ptrs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l_known_ptrs DocumentClass.known_ptr DocumentClass.known_ptrs
[PROOF STEP]
using known_ptrs_known_ptr known_ptrs_preserved l_known_ptrs_def known_ptrs_subset known_ptrs_new_ptr
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>DocumentClass.known_ptrs ?h; ?ptr |\<in>| object_ptr_kinds ?h\<rbrakk> \<Longrightarrow> DocumentClass.known_ptr ?ptr
object_ptr_kinds ?h = object_ptr_kinds ?h' \<Longrightarrow> DocumentClass.known_ptrs ?h = DocumentClass.known_ptrs ?h'
l_known_ptrs ?known_ptr ?known_ptrs \<equiv> ((\<forall>h ptr. ?known_ptrs h \<longrightarrow> ptr |\<in>| object_ptr_kinds h \<longrightarrow> ?known_ptr ptr) \<and> (\<forall>h h'. object_ptr_kinds h = object_ptr_kinds h' \<longrightarrow> ?known_ptrs h = ?known_ptrs h')) \<and> (\<forall>h' h. object_ptr_kinds h' |\<subseteq>| object_ptr_kinds h \<longrightarrow> ?known_ptrs h \<longrightarrow> ?known_ptrs h') \<and> (\<forall>h' h new_ptr. object_ptr_kinds h' = object_ptr_kinds h |\<union>| {|new_ptr|} \<longrightarrow> ?known_ptr new_ptr \<longrightarrow> ?known_ptrs h \<longrightarrow> ?known_ptrs h')
\<lbrakk>object_ptr_kinds ?h' |\<subseteq>| object_ptr_kinds ?h; DocumentClass.known_ptrs ?h\<rbrakk> \<Longrightarrow> DocumentClass.known_ptrs ?h'
\<lbrakk>object_ptr_kinds ?h' = object_ptr_kinds ?h |\<union>| {|?new_ptr|}; DocumentClass.known_ptr ?new_ptr; DocumentClass.known_ptrs ?h\<rbrakk> \<Longrightarrow> DocumentClass.known_ptrs ?h'

goal (1 subgoal):
 1. l_known_ptrs DocumentClass.known_ptr DocumentClass.known_ptrs
[PROOF STEP]
by blast


[STATEMENT]
lemma degree_smult_eq_iff:
  "degree (smult a p) = degree p \<longleftrightarrow> degree p = 0 \<or> a * lead_coeff p \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (degree (Polynomial.smult a p) = degree p) = (degree p = 0 \<or> a * lead_coeff p \<noteq> (0::'a))
[PROOF STEP]
by (metis (no_types, lifting) coeff_smult degree_0 degree_smult_le le_antisym
      le_degree le_zero_eq leading_coeff_0_iff)


[STATEMENT]
lemma degree_smult_eqI[intro!]:
  assumes "degree p \<noteq> 0 \<Longrightarrow> a * lead_coeff p \<noteq> 0"
  shows "degree (smult a p) = degree p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (Polynomial.smult a p) = degree p
[PROOF STEP]
using assms degree_smult_eq_iff
[PROOF STATE]
proof (prove)
using this:
degree p \<noteq> 0 \<Longrightarrow> a * lead_coeff p \<noteq> (0::'a)
(degree (Polynomial.smult ?a ?p) = degree ?p) = (degree ?p = 0 \<or> ?a * lead_coeff ?p \<noteq> (0::?'a))

goal (1 subgoal):
 1. degree (Polynomial.smult a p) = degree p
[PROOF STEP]
by auto


[STATEMENT]
lemma degree_mult_eq2:
  assumes lc: "lead_coeff p * lead_coeff q \<noteq> 0"
  shows "degree (p * q) = degree p + degree q" (is "_ = ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (p * q) = degree p + degree q
[PROOF STEP]
proof(intro antisym[OF degree_mult_le] le_degree, unfold coeff_mult)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) \<noteq> (0::'a)
[PROOF STEP]
let ?f = "\<lambda>i. coeff p i * coeff q (?r - i)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) \<noteq> (0::'a)
[PROOF STEP]
have "(\<Sum>i\<le>?r. ?f i) = sum ?f {..degree p} + sum ?f {Suc (degree p)..?r}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (\<Sum>i\<le>degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) + (\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i))
[PROOF STEP]
by (rule sum_up_index_split)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (\<Sum>i\<le>degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) + (\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i))

goal (1 subgoal):
 1. (\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) \<noteq> (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (\<Sum>i\<le>degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) + (\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i))

goal (1 subgoal):
 1. (\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) \<noteq> (0::'a)
[PROOF STEP]
have "sum ?f {Suc (degree p)..?r} = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
assume "x > degree p"
[PROOF STATE]
proof (state)
this:
degree p < x

goal (1 subgoal):
 1. (\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
degree p < x
[PROOF STEP]
have "coeff p x = 0"
[PROOF STATE]
proof (prove)
using this:
degree p < x

goal (1 subgoal):
 1. poly.coeff p x = (0::'a)
[PROOF STEP]
by (rule coeff_eq_0)
[PROOF STATE]
proof (state)
this:
poly.coeff p x = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly.coeff p x = (0::'a)
[PROOF STEP]
have "?f x = 0"
[PROOF STATE]
proof (prove)
using this:
poly.coeff p x = (0::'a)

goal (1 subgoal):
 1. poly.coeff p x * poly.coeff q (degree p + degree q - x) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly.coeff p x * poly.coeff q (degree p + degree q - x) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
degree p < ?x2 \<Longrightarrow> poly.coeff p ?x2 * poly.coeff q (degree p + degree q - ?x2) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
degree p < ?x2 \<Longrightarrow> poly.coeff p ?x2 * poly.coeff q (degree p + degree q - ?x2) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
degree p < ?x2 \<Longrightarrow> poly.coeff p ?x2 * poly.coeff q (degree p + degree q - ?x2) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
by (intro sum.neutral, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) \<noteq> (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i = Suc (degree p)..degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) \<noteq> (0::'a)
[PROOF STEP]
have "sum ?f {..degree p} = sum ?f {..<degree p} + ?f (degree p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<le>degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (\<Sum>i<degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) + lead_coeff p * poly.coeff q (degree p + degree q - degree p)
[PROOF STEP]
by(fold lessThan_Suc_atMost, unfold sum.lessThan_Suc, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (\<Sum>i<degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) + lead_coeff p * poly.coeff q (degree p + degree q - degree p)

goal (1 subgoal):
 1. (\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) \<noteq> (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (\<Sum>i<degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) + lead_coeff p * poly.coeff q (degree p + degree q - degree p)

goal (1 subgoal):
 1. (\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) \<noteq> (0::'a)
[PROOF STEP]
have "sum ?f {..<degree p} = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i<degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i<degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>i<degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
assume "x < degree p"
[PROOF STATE]
proof (state)
this:
x < degree p

goal (1 subgoal):
 1. (\<Sum>i<degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x < degree p
[PROOF STEP]
have "coeff q (?r - x) = 0"
[PROOF STATE]
proof (prove)
using this:
x < degree p

goal (1 subgoal):
 1. poly.coeff q (degree p + degree q - x) = (0::'a)
[PROOF STEP]
by (intro coeff_eq_0, auto)
[PROOF STATE]
proof (state)
this:
poly.coeff q (degree p + degree q - x) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i<degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly.coeff q (degree p + degree q - x) = (0::'a)
[PROOF STEP]
have "?f x = 0"
[PROOF STATE]
proof (prove)
using this:
poly.coeff q (degree p + degree q - x) = (0::'a)

goal (1 subgoal):
 1. poly.coeff p x * poly.coeff q (degree p + degree q - x) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly.coeff p x * poly.coeff q (degree p + degree q - x) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i<degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?x2 < degree p \<Longrightarrow> poly.coeff p ?x2 * poly.coeff q (degree p + degree q - ?x2) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i<degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x2 < degree p \<Longrightarrow> poly.coeff p ?x2 * poly.coeff q (degree p + degree q - ?x2) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
?x2 < degree p \<Longrightarrow> poly.coeff p ?x2 * poly.coeff q (degree p + degree q - ?x2) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i<degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)
[PROOF STEP]
by (intro sum.neutral, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i<degree p. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a)

goal (1 subgoal):
 1. (\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) \<noteq> (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a) + lead_coeff p * poly.coeff q (degree p + degree q - degree p) + (0::'a)
[PROOF STEP]
show "(\<Sum>i\<le>?r. ?f i) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a) + lead_coeff p * poly.coeff q (degree p + degree q - degree p) + (0::'a)

goal (1 subgoal):
 1. (\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) \<noteq> (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) = (0::'a) + lead_coeff p * poly.coeff q (degree p + degree q - degree p) + (0::'a)
lead_coeff p * lead_coeff q \<noteq> (0::'a)

goal (1 subgoal):
 1. (\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) \<noteq> (0::'a)
[PROOF STEP]
by (auto simp:)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<le>degree p + degree q. poly.coeff p i * poly.coeff q (degree p + degree q - i)) \<noteq> (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma degree_mult_eq_left_unit:
  fixes p q :: "'a :: comm_semiring_1 poly"
  assumes unit: "lead_coeff p dvd 1" and q0: "q \<noteq> 0"
  shows "degree (p * q) = degree p + degree q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (p * q) = degree p + degree q
[PROOF STEP]
proof(intro degree_mult_eq2 notI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lead_coeff p * lead_coeff q = (0::'a) \<Longrightarrow> False
[PROOF STEP]
from unit
[PROOF STATE]
proof (chain)
picking this:
lead_coeff p dvd (1::'a)
[PROOF STEP]
obtain c where "lead_coeff p * c = 1"
[PROOF STATE]
proof (prove)
using this:
lead_coeff p dvd (1::'a)

goal (1 subgoal):
 1. (\<And>c. lead_coeff p * c = (1::'a) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim dvdE,auto)
[PROOF STATE]
proof (state)
this:
lead_coeff p * c = (1::'a)

goal (1 subgoal):
 1. lead_coeff p * lead_coeff q = (0::'a) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lead_coeff p * c = (1::'a)
[PROOF STEP]
have "c * lead_coeff p = 1"
[PROOF STATE]
proof (prove)
using this:
lead_coeff p * c = (1::'a)

goal (1 subgoal):
 1. c * lead_coeff p = (1::'a)
[PROOF STEP]
by (auto simp: ac_simps)
[PROOF STATE]
proof (state)
this:
c * lead_coeff p = (1::'a)

goal (1 subgoal):
 1. lead_coeff p * lead_coeff q = (0::'a) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
c * lead_coeff p = (1::'a)

goal (1 subgoal):
 1. lead_coeff p * lead_coeff q = (0::'a) \<Longrightarrow> False
[PROOF STEP]
assume "lead_coeff p * lead_coeff q = 0"
[PROOF STATE]
proof (state)
this:
lead_coeff p * lead_coeff q = (0::'a)

goal (1 subgoal):
 1. lead_coeff p * lead_coeff q = (0::'a) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
lead_coeff p * lead_coeff q = (0::'a)
[PROOF STEP]
have "c * lead_coeff p * lead_coeff q = 0"
[PROOF STATE]
proof (prove)
using this:
lead_coeff p * lead_coeff q = (0::'a)

goal (1 subgoal):
 1. c * lead_coeff p * lead_coeff q = (0::'a)
[PROOF STEP]
by (auto simp: ac_simps)
[PROOF STATE]
proof (state)
this:
c * lead_coeff p * lead_coeff q = (0::'a)

goal (1 subgoal):
 1. lead_coeff p * lead_coeff q = (0::'a) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
c * lead_coeff p = (1::'a)
c * lead_coeff p * lead_coeff q = (0::'a)
[PROOF STEP]
have "lead_coeff q = 0"
[PROOF STATE]
proof (prove)
using this:
c * lead_coeff p = (1::'a)
c * lead_coeff p * lead_coeff q = (0::'a)

goal (1 subgoal):
 1. lead_coeff q = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
lead_coeff q = (0::'a)

goal (1 subgoal):
 1. lead_coeff p * lead_coeff q = (0::'a) \<Longrightarrow> False
[PROOF STEP]
with q0
[PROOF STATE]
proof (chain)
picking this:
q \<noteq> 0
lead_coeff q = (0::'a)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
q \<noteq> 0
lead_coeff q = (0::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma monic_degree_map_poly_hom: "monic p \<Longrightarrow> degree (map_poly hom p) = degree p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monic p \<Longrightarrow> degree (map_poly hom p) = degree p
[PROOF STEP]
by (auto intro: degree_map_poly)


[STATEMENT]
lemma monic_map_poly_hom: "monic p \<Longrightarrow> monic (map_poly hom p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monic p \<Longrightarrow> monic (map_poly hom p)
[PROOF STEP]
by (simp add: monic_degree_map_poly_hom)


[STATEMENT]
lemma of_nat_zero:
  assumes "CARD('a::nontriv) dvd n"
  shows "(of_nat n :: 'a mod_ring) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat n = 0
[PROOF STEP]
apply (transfer fixing: n)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int n mod int CARD('a) = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
CARD('a) dvd n

goal (1 subgoal):
 1. int n mod int CARD('a) = 0
[PROOF STEP]
by (presburger)


[STATEMENT]
lemma rebase_self [simp]:
  "@x = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. @x = x
[PROOF STEP]
by (simp add: of_int_of_int_mod_ring)


[STATEMENT]
lemma map_poly_rebase [simp]:
  "map_poly rebase p = #p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_poly rebase p = #p
[PROOF STEP]
by (induct p) simp_all


[STATEMENT]
lemma rebase_poly_0: "#0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. #0 = 0
[PROOF STEP]
by simp


[STATEMENT]
lemma rebase_poly_1: "#1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. #1 = 1
[PROOF STEP]
by simp


[STATEMENT]
lemma rebase_poly_pCons[simp]: "#pCons a p = pCons (@a) (#p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. #pCons a p = pCons (@a) (#p)
[PROOF STEP]
by(cases "a = 0 \<and> p = 0", simp, fold map_poly_rebase, subst map_poly_pCons, auto)


[STATEMENT]
lemma rebase_poly_self[simp]: "#p = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. #p = p
[PROOF STEP]
by (induct p, auto)


[STATEMENT]
lemma degree_rebase_poly_le: "degree (#p) \<le> degree p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (#p) \<le> degree p
[PROOF STEP]
by (fold map_poly_rebase, subst degree_map_poly_le, auto)


[STATEMENT]
lemma rebase_poly_eq_0_iff:
  "(#p :: 'a :: nontriv mod_ring poly) = 0 \<longleftrightarrow> (\<forall>i. (@coeff p i :: 'a mod_ring) = 0)" (is "?l \<longleftrightarrow> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (#p = 0) = (\<forall>i. @poly.coeff p i = 0)
[PROOF STEP]
proof(intro iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. #p = 0 \<Longrightarrow> \<forall>i. @poly.coeff p i = 0
 2. \<forall>i. @poly.coeff p i = 0 \<Longrightarrow> #p = 0
[PROOF STEP]
assume ?l
[PROOF STATE]
proof (state)
this:
#p = 0

goal (2 subgoals):
 1. #p = 0 \<Longrightarrow> \<forall>i. @poly.coeff p i = 0
 2. \<forall>i. @poly.coeff p i = 0 \<Longrightarrow> #p = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
#p = 0
[PROOF STEP]
have "coeff (#p :: 'a mod_ring poly) i = 0" for i
[PROOF STATE]
proof (prove)
using this:
#p = 0

goal (1 subgoal):
 1. poly.coeff (#p) i = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly.coeff (#p) ?i = 0

goal (2 subgoals):
 1. #p = 0 \<Longrightarrow> \<forall>i. @poly.coeff p i = 0
 2. \<forall>i. @poly.coeff p i = 0 \<Longrightarrow> #p = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly.coeff (#p) ?i = 0
[PROOF STEP]
show ?r
[PROOF STATE]
proof (prove)
using this:
poly.coeff (#p) ?i = 0

goal (1 subgoal):
 1. \<forall>i. @poly.coeff p i = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>i. @poly.coeff p i = 0

goal (1 subgoal):
 1. \<forall>i. @poly.coeff p i = 0 \<Longrightarrow> #p = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>i. @poly.coeff p i = 0 \<Longrightarrow> #p = 0
[PROOF STEP]
assume ?r
[PROOF STATE]
proof (state)
this:
\<forall>i. @poly.coeff p i = 0

goal (1 subgoal):
 1. \<forall>i. @poly.coeff p i = 0 \<Longrightarrow> #p = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. @poly.coeff p i = 0
[PROOF STEP]
have "coeff (#p :: 'a mod_ring poly) i = 0" for i
[PROOF STATE]
proof (prove)
using this:
\<forall>i. @poly.coeff p i = 0

goal (1 subgoal):
 1. poly.coeff (#p) i = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly.coeff (#p) ?i = 0

goal (1 subgoal):
 1. \<forall>i. @poly.coeff p i = 0 \<Longrightarrow> #p = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly.coeff (#p) ?i = 0
[PROOF STEP]
show ?l
[PROOF STATE]
proof (prove)
using this:
poly.coeff (#p) ?i = 0

goal (1 subgoal):
 1. #p = 0
[PROOF STEP]
by (intro poly_eqI, auto)
[PROOF STATE]
proof (state)
this:
#p = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mod_mod_le:
  assumes ab: "(a::int) \<le> b" and a0: "0 < a" and c0: "c \<ge> 0" shows "(c mod a) mod b = c mod a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c mod a mod b = c mod a
[PROOF STEP]
by (meson Divides.pos_mod_bound Divides.pos_mod_sign a0 ab less_le_trans mod_pos_pos_trivial)


[STATEMENT]
lemma ab: "int CARD('a) \<le> CARD('b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int CARD('a) \<le> int CARD('b)
[PROOF STEP]
using card
[PROOF STATE]
proof (prove)
using this:
CARD('a) \<le> CARD('b)

goal (1 subgoal):
 1. int CARD('a) \<le> int CARD('b)
[PROOF STEP]
by auto


[STATEMENT]
lemma rebase_eq_0[simp]:
  shows "(@(x :: 'a mod_ring) :: 'b mod_ring) = 0 \<longleftrightarrow> x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (@x = 0) = (x = 0)
[PROOF STEP]
using card
[PROOF STATE]
proof (prove)
using this:
CARD('a) \<le> CARD('b)

goal (1 subgoal):
 1. (@x = 0) = (x = 0)
[PROOF STEP]
by (transfer, auto)


[STATEMENT]
lemma degree_rebase_poly_eq[simp]:
  shows "degree (#(p :: 'a mod_ring poly) :: 'b mod_ring poly) = degree p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. degree (#p) = degree p
[PROOF STEP]
by (subst degree_map_poly; simp)


[STATEMENT]
lemma lead_coeff_rebase_poly[simp]:
  "lead_coeff (#(p::'a mod_ring poly) :: 'b mod_ring poly) = @lead_coeff p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lead_coeff (#p) = @lead_coeff p
[PROOF STEP]
by simp


[STATEMENT]
lemma to_int_mod_ring_rebase: "to_int_mod_ring(@(x :: 'a mod_ring)::'b mod_ring) = to_int_mod_ring x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. to_int_mod_ring (@x) = to_int_mod_ring x
[PROOF STEP]
using card
[PROOF STATE]
proof (prove)
using this:
CARD('a) \<le> CARD('b)

goal (1 subgoal):
 1. to_int_mod_ring (@x) = to_int_mod_ring x
[PROOF STEP]
by (transfer, auto)


[STATEMENT]
lemma rebase_id[simp]: "@(@(x::'a mod_ring) :: 'b mod_ring) = @x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. @@x = @x
[PROOF STEP]
using card
[PROOF STATE]
proof (prove)
using this:
CARD('a) \<le> CARD('b)

goal (1 subgoal):
 1. @@x = @x
[PROOF STEP]
by (transfer, auto)


[STATEMENT]
lemma rebase_poly_id[simp]: "#(#(p::'a mod_ring poly) :: 'b mod_ring poly) = #p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ##p = #p
[PROOF STEP]
by (induct p, auto)


[STATEMENT]
lemma ab: "CARD('a) \<ge> CARD('b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('b) \<le> CARD('a)
[PROOF STEP]
by (rule dvd_imp_le[OF dvd], auto)


[STATEMENT]
lemma rebase_id[simp]: "@(@(x::'b mod_ring) :: 'a mod_ring) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. @@x = x
[PROOF STEP]
using ab
[PROOF STATE]
proof (prove)
using this:
CARD('b) \<le> CARD('a)

goal (1 subgoal):
 1. @@x = x
[PROOF STEP]
by (transfer, auto)


[STATEMENT]
lemma rebase_poly_id[simp]: "#(#(p::'b mod_ring poly) :: 'a mod_ring poly) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ##p = p
[PROOF STEP]
by (induct p, auto)


[STATEMENT]
lemma rebase_of_nat[simp]: "(@(of_nat n :: 'a mod_ring) :: 'b mod_ring) = of_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. @of_nat n = of_nat n
[PROOF STEP]
apply transfer
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. int n mod int CARD('a) mod int CARD('b) = int n mod int CARD('b)
[PROOF STEP]
apply (rule mod_mod_cancel)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>n. int CARD('b) dvd int CARD('a)
[PROOF STEP]
using dvd
[PROOF STATE]
proof (prove)
using this:
CARD('b) dvd CARD('a)

goal (1 subgoal):
 1. \<And>n. int CARD('b) dvd int CARD('a)
[PROOF STEP]
by presburger


[STATEMENT]
lemma mod_1_lift_nat:
  assumes "(of_int (int x) :: 'a mod_ring) = 1"
  shows "(of_int (int x) :: 'b mod_ring) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (int x) = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_int (int x) = 1
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
of_int (int x) = 1
[PROOF STEP]
have "int x mod CARD('a) = 1"
[PROOF STATE]
proof (prove)
using this:
of_int (int x) = 1

goal (1 subgoal):
 1. int x mod int CARD('a) = 1
[PROOF STEP]
by transfer
[PROOF STATE]
proof (state)
this:
int x mod int CARD('a) = 1

goal (1 subgoal):
 1. of_int (int x) = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
int x mod int CARD('a) = 1
[PROOF STEP]
have "x mod CARD('a) = 1"
[PROOF STATE]
proof (prove)
using this:
int x mod int CARD('a) = 1

goal (1 subgoal):
 1. x mod CARD('a) = 1
[PROOF STEP]
by (simp add: of_nat_mod [symmetric])
[PROOF STATE]
proof (state)
this:
x mod CARD('a) = 1

goal (1 subgoal):
 1. of_int (int x) = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x mod CARD('a) = 1
[PROOF STEP]
have "x mod CARD('b) = 1"
[PROOF STATE]
proof (prove)
using this:
x mod CARD('a) = 1

goal (1 subgoal):
 1. x mod CARD('b) = 1
[PROOF STEP]
by (metis dvd mod_mod_cancel one_mod_card)
[PROOF STATE]
proof (state)
this:
x mod CARD('b) = 1

goal (1 subgoal):
 1. of_int (int x) = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x mod CARD('b) = 1
[PROOF STEP]
have "int x mod CARD('b) = 1"
[PROOF STATE]
proof (prove)
using this:
x mod CARD('b) = 1

goal (1 subgoal):
 1. int x mod int CARD('b) = 1
[PROOF STEP]
by (simp add: of_nat_mod [symmetric])
[PROOF STATE]
proof (state)
this:
int x mod int CARD('b) = 1

goal (1 subgoal):
 1. of_int (int x) = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
int x mod int CARD('b) = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
int x mod int CARD('b) = 1

goal (1 subgoal):
 1. of_int (int x) = 1
[PROOF STEP]
by transfer
[PROOF STATE]
proof (state)
this:
of_int (int x) = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_nat_CARD_eq_0[simp]: "(of_nat CARD('a) :: 'b mod_ring) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat CARD('a) = 0
[PROOF STEP]
using dvd
[PROOF STATE]
proof (prove)
using this:
CARD('b) dvd CARD('a)

goal (1 subgoal):
 1. of_nat CARD('a) = 0
[PROOF STEP]
by (transfer, presburger)


[STATEMENT]
lemma poly_rebase[simp]: "@poly p x = poly (#(p :: 'a mod_ring poly) :: 'b mod_ring poly) (@(x::'a mod_ring) :: 'b mod_ring)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. @poly p x = poly (#p) (@x)
[PROOF STEP]
by (fold map_poly_rebase poly_map_poly, rule)


[STATEMENT]
lemma rebase_poly_smult[simp]: "(#(smult a p :: 'a mod_ring poly) :: 'b mod_ring poly) = smult (@a) (#p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. #Polynomial.smult a p = Polynomial.smult (@a) (#p)
[PROOF STEP]
by(induct p, auto simp: hom_distribs)


[STATEMENT]
lemma rebase_mult_eq[simp]: "(of_nat CARD('d) * a :: 'a mod_ring) = of_nat CARD('d) * a' \<longleftrightarrow> (@a :: 'b mod_ring) = @a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (of_nat CARD('d) * a = of_nat CARD('d) * a') = (@a = @a')
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (of_nat CARD('d) * a = of_nat CARD('d) * a') = (@a = @a')
[PROOF STEP]
from dvd
[PROOF STATE]
proof (chain)
picking this:
CARD('b) dvd CARD('a)
[PROOF STEP]
obtain d' where "CARD('a) = d' * CARD('b)"
[PROOF STATE]
proof (prove)
using this:
CARD('b) dvd CARD('a)

goal (1 subgoal):
 1. (\<And>d'. CARD('a) = d' * CARD('b) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim dvdE, auto)
[PROOF STATE]
proof (state)
this:
CARD('a) = d' * CARD('b)

goal (1 subgoal):
 1. (of_nat CARD('d) * a = of_nat CARD('d) * a') = (@a = @a')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
CARD('a) = d' * CARD('b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
CARD('a) = d' * CARD('b)

goal (1 subgoal):
 1. (of_nat CARD('d) * a = of_nat CARD('d) * a') = (@a = @a')
[PROOF STEP]
by (transfer, auto simp:d)
[PROOF STATE]
proof (state)
this:
(of_nat CARD('d) * a = of_nat CARD('d) * a') = (@a = @a')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rebase_poly_smult_eq[simp]:
  fixes a a' :: "'a mod_ring poly"
  defines "d \<equiv> of_nat CARD('d) :: 'a mod_ring"
  shows "smult d a = smult d a' \<longleftrightarrow> (#a :: 'b mod_ring poly) = #a'" (is "?l \<longleftrightarrow> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Polynomial.smult d a = Polynomial.smult d a') = (#a = #a')
[PROOF STEP]
proof (intro iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Polynomial.smult d a = Polynomial.smult d a' \<Longrightarrow> #a = #a'
 2. #a = #a' \<Longrightarrow> Polynomial.smult d a = Polynomial.smult d a'
[PROOF STEP]
assume l: ?l
[PROOF STATE]
proof (state)
this:
Polynomial.smult d a = Polynomial.smult d a'

goal (2 subgoals):
 1. Polynomial.smult d a = Polynomial.smult d a' \<Longrightarrow> #a = #a'
 2. #a = #a' \<Longrightarrow> Polynomial.smult d a = Polynomial.smult d a'
[PROOF STEP]
show "?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. #a = #a'
[PROOF STEP]
proof (intro poly_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. poly.coeff (#a) n = poly.coeff (#a') n
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. poly.coeff (#a) n = poly.coeff (#a') n
[PROOF STEP]
from l
[PROOF STATE]
proof (chain)
picking this:
Polynomial.smult d a = Polynomial.smult d a'
[PROOF STEP]
have "coeff (smult d a) n = coeff (smult d a') n"
[PROOF STATE]
proof (prove)
using this:
Polynomial.smult d a = Polynomial.smult d a'

goal (1 subgoal):
 1. poly.coeff (Polynomial.smult d a) n = poly.coeff (Polynomial.smult d a') n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly.coeff (Polynomial.smult d a) n = poly.coeff (Polynomial.smult d a') n

goal (1 subgoal):
 1. \<And>n. poly.coeff (#a) n = poly.coeff (#a') n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly.coeff (Polynomial.smult d a) n = poly.coeff (Polynomial.smult d a') n
[PROOF STEP]
have "d * coeff a n = d * coeff a' n"
[PROOF STATE]
proof (prove)
using this:
poly.coeff (Polynomial.smult d a) n = poly.coeff (Polynomial.smult d a') n

goal (1 subgoal):
 1. d * poly.coeff a n = d * poly.coeff a' n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
d * poly.coeff a n = d * poly.coeff a' n

goal (1 subgoal):
 1. \<And>n. poly.coeff (#a) n = poly.coeff (#a') n
[PROOF STEP]
from this[unfolded d_def rebase_mult_eq]
[PROOF STATE]
proof (chain)
picking this:
@poly.coeff a n = @poly.coeff a' n
[PROOF STEP]
show "coeff (#a :: 'b mod_ring poly) n = coeff (#a') n"
[PROOF STATE]
proof (prove)
using this:
@poly.coeff a n = @poly.coeff a' n

goal (1 subgoal):
 1. poly.coeff (#a) n = poly.coeff (#a') n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly.coeff (#a) n = poly.coeff (#a') n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
#a = #a'

goal (1 subgoal):
 1. #a = #a' \<Longrightarrow> Polynomial.smult d a = Polynomial.smult d a'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. #a = #a' \<Longrightarrow> Polynomial.smult d a = Polynomial.smult d a'
[PROOF STEP]
assume r: ?r
[PROOF STATE]
proof (state)
this:
#a = #a'

goal (1 subgoal):
 1. #a = #a' \<Longrightarrow> Polynomial.smult d a = Polynomial.smult d a'
[PROOF STEP]
show ?l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Polynomial.smult d a = Polynomial.smult d a'
[PROOF STEP]
proof(intro poly_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. poly.coeff (Polynomial.smult d a) n = poly.coeff (Polynomial.smult d a') n
[PROOF STEP]
fix n
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. poly.coeff (Polynomial.smult d a) n = poly.coeff (Polynomial.smult d a') n
[PROOF STEP]
from r
[PROOF STATE]
proof (chain)
picking this:
#a = #a'
[PROOF STEP]
have "coeff (#a :: 'b mod_ring poly) n = coeff (#a') n"
[PROOF STATE]
proof (prove)
using this:
#a = #a'

goal (1 subgoal):
 1. poly.coeff (#a) n = poly.coeff (#a') n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly.coeff (#a) n = poly.coeff (#a') n

goal (1 subgoal):
 1. \<And>n. poly.coeff (Polynomial.smult d a) n = poly.coeff (Polynomial.smult d a') n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
poly.coeff (#a) n = poly.coeff (#a') n
[PROOF STEP]
have "(@coeff a n :: 'b mod_ring) = @coeff a' n"
[PROOF STATE]
proof (prove)
using this:
poly.coeff (#a) n = poly.coeff (#a') n

goal (1 subgoal):
 1. @poly.coeff a n = @poly.coeff a' n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
@poly.coeff a n = @poly.coeff a' n

goal (1 subgoal):
 1. \<And>n. poly.coeff (Polynomial.smult d a) n = poly.coeff (Polynomial.smult d a') n
[PROOF STEP]
from this[folded d_def rebase_mult_eq]
[PROOF STATE]
proof (chain)
picking this:
d * poly.coeff a n = d * poly.coeff a' n
[PROOF STEP]
show "coeff (smult d a) n = coeff (smult d a') n"
[PROOF STATE]
proof (prove)
using this:
d * poly.coeff a n = d * poly.coeff a' n

goal (1 subgoal):
 1. poly.coeff (Polynomial.smult d a) n = poly.coeff (Polynomial.smult d a') n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
poly.coeff (Polynomial.smult d a) n = poly.coeff (Polynomial.smult d a') n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Polynomial.smult d a = Polynomial.smult d a'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rebase_eq_0_imp_ex_mult:
  "(@(a :: 'a mod_ring) :: 'b mod_ring) = 0 \<Longrightarrow> (\<exists>c :: 'd mod_ring. a = of_nat CARD('b) * @c)" (is "?l \<Longrightarrow> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. @a = 0 \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
proof(cases "CARD('a) = CARD('b)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>@a = 0; CARD('a) = CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
 2. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
CARD('a) = CARD('b)

goal (2 subgoals):
 1. \<lbrakk>@a = 0; CARD('a) = CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
 2. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
CARD('a) = CARD('b)
[PROOF STEP]
show "?l \<Longrightarrow> ?r"
[PROOF STATE]
proof (prove)
using this:
CARD('a) = CARD('b)

goal (1 subgoal):
 1. @a = 0 \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
by (transfer, auto)
[PROOF STATE]
proof (state)
this:
@a = 0 \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
CARD('a) \<noteq> CARD('b)

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
have [simp]: "int CARD('b) mod int CARD('a) = int CARD('b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int CARD('b) mod int CARD('a) = int CARD('b)
[PROOF STEP]
by(rule mod_pos_pos_trivial, insert ab False, auto)
[PROOF STATE]
proof (state)
this:
int CARD('b) mod int CARD('a) = int CARD('b)

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
int CARD('b) mod int CARD('a) = int CARD('b)

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
assume a: "0 \<le> a" "a < int CARD('a)" and mod: "a mod int CARD('b) = 0"
[PROOF STATE]
proof (state)
this:
0 \<le> a
a < int CARD('a)
a mod int CARD('b) = 0

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
from mod
[PROOF STATE]
proof (chain)
picking this:
a mod int CARD('b) = 0
[PROOF STEP]
have "int CARD('b) dvd a"
[PROOF STATE]
proof (prove)
using this:
a mod int CARD('b) = 0

goal (1 subgoal):
 1. int CARD('b) dvd a
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
int CARD('b) dvd a

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
int CARD('b) dvd a
[PROOF STEP]
obtain i where *: "a = int CARD('b) * i"
[PROOF STATE]
proof (prove)
using this:
int CARD('b) dvd a

goal (1 subgoal):
 1. (\<And>i. a = int CARD('b) * i \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim dvdE, auto)
[PROOF STATE]
proof (state)
this:
a = int CARD('b) * i

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
from * a
[PROOF STATE]
proof (chain)
picking this:
a = int CARD('b) * i
0 \<le> a
a < int CARD('a)
[PROOF STEP]
have "i < int CARD('d)"
[PROOF STATE]
proof (prove)
using this:
a = int CARD('b) * i
0 \<le> a
a < int CARD('a)

goal (1 subgoal):
 1. i < int CARD('d)
[PROOF STEP]
by (simp add:d)
[PROOF STATE]
proof (state)
this:
i < int CARD('d)

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i < int CARD('d)

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
hence "(i mod int CARD('a)) = i"
[PROOF STATE]
proof (prove)
using this:
i < int CARD('d)

goal (1 subgoal):
 1. i mod int CARD('a) = i
[PROOF STEP]
by (metis dual_order.order_iff_strict less_le_trans not_le of_nat_less_iff "*" a(1) a(2)
             mod_pos_pos_trivial mult_less_cancel_right1 nat_neq_iff nontriv of_nat_1)
[PROOF STATE]
proof (state)
this:
i mod int CARD('a) = i

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
with * a
[PROOF STATE]
proof (chain)
picking this:
a = int CARD('b) * i
0 \<le> a
a < int CARD('a)
i mod int CARD('a) = i
[PROOF STEP]
have "a = int CARD('b) * (i mod int CARD('a)) mod int CARD('a)"
[PROOF STATE]
proof (prove)
using this:
a = int CARD('b) * i
0 \<le> a
a < int CARD('a)
i mod int CARD('a) = i

goal (1 subgoal):
 1. a = int CARD('b) * (i mod int CARD('a)) mod int CARD('a)
[PROOF STEP]
by (auto simp:d)
[PROOF STATE]
proof (state)
this:
a = int CARD('b) * (i mod int CARD('a)) mod int CARD('a)

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a = int CARD('b) * (i mod int CARD('a)) mod int CARD('a)

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
from * a
[PROOF STATE]
proof (chain)
picking this:
a = int CARD('b) * i
0 \<le> a
a < int CARD('a)
[PROOF STEP]
have "0 \<le> i"
[PROOF STATE]
proof (prove)
using this:
a = int CARD('b) * i
0 \<le> a
a < int CARD('a)

goal (1 subgoal):
 1. 0 \<le> i
[PROOF STEP]
using linordered_semiring_strict_class.mult_pos_neg of_nat_0_less_iff zero_less_card_finite
[PROOF STATE]
proof (prove)
using this:
a = int CARD('b) * i
0 \<le> a
a < int CARD('a)
\<lbrakk>(0::?'a) < ?a; ?b < (0::?'a)\<rbrakk> \<Longrightarrow> ?a * ?b < (0::?'a)
((0::?'a) < of_nat ?n) = (0 < ?n)
0 < CARD(?'a)

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

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i < int CARD('d)
a = int CARD('b) * (i mod int CARD('a)) mod int CARD('a)
0 \<le> i
[PROOF STEP]
have "\<exists>i\<ge>0. i < int CARD('d) \<and> a = int CARD('b) * (i mod int CARD('a)) mod int CARD('a)"
[PROOF STATE]
proof (prove)
using this:
i < int CARD('d)
a = int CARD('b) * (i mod int CARD('a)) mod int CARD('a)
0 \<le> i

goal (1 subgoal):
 1. \<exists>i\<ge>0. i < int CARD('d) \<and> a = int CARD('b) * (i mod int CARD('a)) mod int CARD('a)
[PROOF STEP]
by (auto intro: exI[of _ i])
[PROOF STATE]
proof (state)
this:
\<exists>i\<ge>0. i < int CARD('d) \<and> a = int CARD('b) * (i mod int CARD('a)) mod int CARD('a)

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>0 \<le> ?aa2; ?aa2 < int CARD('a); ?aa2 mod int CARD('b) = 0\<rbrakk> \<Longrightarrow> \<exists>i\<ge>0. i < int CARD('d) \<and> ?aa2 = int CARD('b) * (i mod int CARD('a)) mod int CARD('a)

goal (1 subgoal):
 1. \<lbrakk>@a = 0; CARD('a) \<noteq> CARD('b)\<rbrakk> \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>0 \<le> ?aa2; ?aa2 < int CARD('a); ?aa2 mod int CARD('b) = 0\<rbrakk> \<Longrightarrow> \<exists>i\<ge>0. i < int CARD('d) \<and> ?aa2 = int CARD('b) * (i mod int CARD('a)) mod int CARD('a)
[PROOF STEP]
show "?l \<Longrightarrow> ?r"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> ?aa2; ?aa2 < int CARD('a); ?aa2 mod int CARD('b) = 0\<rbrakk> \<Longrightarrow> \<exists>i\<ge>0. i < int CARD('d) \<and> ?aa2 = int CARD('b) * (i mod int CARD('a)) mod int CARD('a)

goal (1 subgoal):
 1. @a = 0 \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
by (transfer, auto simp:d)
[PROOF STATE]
proof (state)
this:
@a = 0 \<Longrightarrow> \<exists>c. a = of_nat CARD('b) * @c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rebase_poly_eq_0_imp_ex_smult:
  "(#(p :: 'a mod_ring poly) :: 'b mod_ring poly) = 0 \<Longrightarrow>
   (\<exists>p' :: 'd mod_ring poly. (p = 0 \<longleftrightarrow> p' = 0) \<and> degree p' \<le> degree p \<and> p = smult (of_nat CARD('b)) (#p'))"
  (is "?l \<Longrightarrow> ?r")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
proof(induct p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. #0 = 0 \<Longrightarrow> \<exists>p'. (0 = 0) = (p' = 0) \<and> degree p' \<le> degree 0 \<and> 0 = Polynomial.smult (of_nat CARD('b)) (#p')
 2. \<And>a p. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p'); #pCons a p = 0\<rbrakk> \<Longrightarrow> \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
#0 = 0

goal (2 subgoals):
 1. #0 = 0 \<Longrightarrow> \<exists>p'. (0 = 0) = (p' = 0) \<and> degree p' \<le> degree 0 \<and> 0 = Polynomial.smult (of_nat CARD('b)) (#p')
 2. \<And>a p. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p'); #pCons a p = 0\<rbrakk> \<Longrightarrow> \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
#0 = 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
#0 = 0

goal (1 subgoal):
 1. \<exists>p'. (0 = 0) = (p' = 0) \<and> degree p' \<le> degree 0 \<and> 0 = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
by (intro exI[of _ 0],auto)
[PROOF STATE]
proof (state)
this:
\<exists>p'. (0 = 0) = (p' = 0) \<and> degree p' \<le> degree 0 \<and> 0 = Polynomial.smult (of_nat CARD('b)) (#p')

goal (1 subgoal):
 1. \<And>a p. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p'); #pCons a p = 0\<rbrakk> \<Longrightarrow> \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a p. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p'); #pCons a p = 0\<rbrakk> \<Longrightarrow> \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
case IH: (pCons a p)
[PROOF STATE]
proof (state)
this:
a \<noteq> 0 \<or> p \<noteq> 0
#p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p')
#pCons a p = 0

goal (1 subgoal):
 1. \<And>a p. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p'); #pCons a p = 0\<rbrakk> \<Longrightarrow> \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
from IH(3)
[PROOF STATE]
proof (chain)
picking this:
#pCons a p = 0
[PROOF STEP]
have "(#p :: 'b mod_ring poly) = 0"
[PROOF STATE]
proof (prove)
using this:
#pCons a p = 0

goal (1 subgoal):
 1. #p = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
#p = 0

goal (1 subgoal):
 1. \<And>a p. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p'); #pCons a p = 0\<rbrakk> \<Longrightarrow> \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
from IH(2)[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
obtain p' :: "'d mod_ring poly"
  where *: "p = 0 \<longleftrightarrow> p' = 0" "degree p' \<le> degree p" "p = smult (of_nat CARD('b)) (#p')"
[PROOF STATE]
proof (prove)
using this:
\<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p')

goal (1 subgoal):
 1. (\<And>p'. \<lbrakk>(p = 0) = (p' = 0); degree p' \<le> degree p; p = Polynomial.smult (of_nat CARD('b)) (#p')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (elim exE conjE)
[PROOF STATE]
proof (state)
this:
(p = 0) = (p' = 0)
degree p' \<le> degree p
p = Polynomial.smult (of_nat CARD('b)) (#p')

goal (1 subgoal):
 1. \<And>a p. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p'); #pCons a p = 0\<rbrakk> \<Longrightarrow> \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
from IH
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> 0 \<or> p \<noteq> 0
#p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p')
#pCons a p = 0
[PROOF STEP]
have "(@a :: 'b mod_ring) = 0"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0 \<or> p \<noteq> 0
#p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p')
#pCons a p = 0

goal (1 subgoal):
 1. @a = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
@a = 0

goal (1 subgoal):
 1. \<And>a p. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p'); #pCons a p = 0\<rbrakk> \<Longrightarrow> \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
from rebase_eq_0_imp_ex_mult[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. a = of_nat CARD('b) * @c
[PROOF STEP]
obtain a' :: "'d mod_ring" where a': "of_nat CARD('b) * (@a') = a"
[PROOF STATE]
proof (prove)
using this:
\<exists>c. a = of_nat CARD('b) * @c

goal (1 subgoal):
 1. (\<And>a'. of_nat CARD('b) * @a' = a \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_nat CARD('b) * @a' = a

goal (1 subgoal):
 1. \<And>a p. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p'); #pCons a p = 0\<rbrakk> \<Longrightarrow> \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
from IH(1)
[PROOF STATE]
proof (chain)
picking this:
a \<noteq> 0 \<or> p \<noteq> 0
[PROOF STEP]
have "pCons a p \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
a \<noteq> 0 \<or> p \<noteq> 0

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

goal (1 subgoal):
 1. \<And>a p. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p'); #pCons a p = 0\<rbrakk> \<Longrightarrow> \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
pCons a p \<noteq> 0

goal (1 subgoal):
 1. \<And>a p. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p'); #pCons a p = 0\<rbrakk> \<Longrightarrow> \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
from *(1,2)
[PROOF STATE]
proof (chain)
picking this:
(p = 0) = (p' = 0)
degree p' \<le> degree p
[PROOF STEP]
have "degree (pCons a' p') \<le> degree (pCons a p)"
[PROOF STATE]
proof (prove)
using this:
(p = 0) = (p' = 0)
degree p' \<le> degree p

goal (1 subgoal):
 1. degree (pCons a' p') \<le> degree (pCons a p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
degree (pCons a' p') \<le> degree (pCons a p)

goal (1 subgoal):
 1. \<And>a p. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p'); #pCons a p = 0\<rbrakk> \<Longrightarrow> \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
degree (pCons a' p') \<le> degree (pCons a p)

goal (1 subgoal):
 1. \<And>a p. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p'); #pCons a p = 0\<rbrakk> \<Longrightarrow> \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
from a' *(3)
[PROOF STATE]
proof (chain)
picking this:
of_nat CARD('b) * @a' = a
p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
have "pCons a p = smult (of_nat CARD('b)) (#pCons a' p')"
[PROOF STATE]
proof (prove)
using this:
of_nat CARD('b) * @a' = a
p = Polynomial.smult (of_nat CARD('b)) (#p')

goal (1 subgoal):
 1. pCons a p = Polynomial.smult (of_nat CARD('b)) (#pCons a' p')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pCons a p = Polynomial.smult (of_nat CARD('b)) (#pCons a' p')

goal (1 subgoal):
 1. \<And>a p. \<lbrakk>a \<noteq> 0 \<or> p \<noteq> 0; #p = 0 \<Longrightarrow> \<exists>p'. (p = 0) = (p' = 0) \<and> degree p' \<le> degree p \<and> p = Polynomial.smult (of_nat CARD('b)) (#p'); #pCons a p = 0\<rbrakk> \<Longrightarrow> \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
pCons a p \<noteq> 0
degree (pCons a' p') \<le> degree (pCons a p)
pCons a p = Polynomial.smult (of_nat CARD('b)) (#pCons a' p')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
pCons a p \<noteq> 0
degree (pCons a' p') \<le> degree (pCons a p)
pCons a p = Polynomial.smult (of_nat CARD('b)) (#pCons a' p')

goal (1 subgoal):
 1. \<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')
[PROOF STEP]
by (intro exI[of _ "pCons a' p'"], auto)
[PROOF STATE]
proof (state)
this:
\<exists>p'. (pCons a p = 0) = (p' = 0) \<and> degree p' \<le> degree (pCons a p) \<and> pCons a p = Polynomial.smult (of_nat CARD('b)) (#p')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mod_mod_nat[simp]: "a mod b mod (b * c :: nat) = a mod b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a mod b mod (b * c) = a mod b
[PROOF STEP]
by (simp add: Divides.mod_mult2_eq)


[STATEMENT]
lemma p[simp]: "p \<equiv> CARD('p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<equiv> CARD('p)
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. if ty_p = ty_p then CARD('p) else undefined \<equiv> CARD('p)
[PROOF STEP]
by auto


[STATEMENT]
lemma q[simp]: "q = CARD('q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q = CARD('q)
[PROOF STEP]
unfolding q_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if ty_q = ty_q then CARD('q) else undefined) = CARD('q)
[PROOF STEP]
by auto


[STATEMENT]
lemma p1: "int p > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < int p
[PROOF STEP]
using nontriv [where ?'a = 'p] p
[PROOF STATE]
proof (prove)
using this:
1 < CARD('p)
p \<equiv> CARD('p)

goal (1 subgoal):
 1. 1 < int p
[PROOF STEP]
by simp


[STATEMENT]
lemma q1: "int q > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < int q
[PROOF STEP]
using nontriv [where ?'a = 'q] q
[PROOF STATE]
proof (prove)
using this:
1 < CARD('q)
q = CARD('q)

goal (1 subgoal):
 1. 1 < int q
[PROOF STEP]
by simp


[STATEMENT]
lemma q0: "int q > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < int q
[PROOF STEP]
using q1
[PROOF STATE]
proof (prove)
using this:
1 < int q

goal (1 subgoal):
 1. 0 < int q
[PROOF STEP]
by auto


[STATEMENT]
lemma pq2[simp]: "CARD('pq) = p * q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('pq) = p * q
[PROOF STEP]
using pq
[PROOF STATE]
proof (prove)
using this:
CARD('pq) = CARD('p) * CARD('q)

goal (1 subgoal):
 1. CARD('pq) = p * q
[PROOF STEP]
by simp


[STATEMENT]
lemma qq_eq_0[simp]: "(of_nat CARD('q) * of_nat CARD('q) :: 'pq mod_ring) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat CARD('q) * of_nat CARD('q) = 0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. of_nat CARD('q) * of_nat CARD('q) = 0
[PROOF STEP]
have "(of_nat (q * q) :: 'pq mod_ring) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat (q * q) = 0
[PROOF STEP]
by (rule of_nat_zero, auto simp: p_dvd_q)
[PROOF STATE]
proof (state)
this:
of_nat (q * q) = 0

goal (1 subgoal):
 1. of_nat CARD('q) * of_nat CARD('q) = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
of_nat (q * q) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
of_nat (q * q) = 0

goal (1 subgoal):
 1. of_nat CARD('q) * of_nat CARD('q) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
of_nat CARD('q) * of_nat CARD('q) = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma of_nat_q[simp]: "of_nat q :: 'q mod_ring \<equiv> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat q \<equiv> 0
[PROOF STEP]
by (fold of_nat_card_eq_0, auto)


[STATEMENT]
lemma rebase_rebase[simp]: "(@(@(x::'pq mod_ring) :: 'q mod_ring) :: 'p mod_ring) = @x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. @@x = @x
[PROOF STEP]
using p_dvd_q
[PROOF STATE]
proof (prove)
using this:
CARD('p) dvd CARD('q)

goal (1 subgoal):
 1. @@x = @x
[PROOF STEP]
by (transfer) (simp add: mod_mod_cancel)


[STATEMENT]
lemma rebase_rebase_poly[simp]: "(#(#(f::'pq mod_ring poly) :: 'q mod_ring poly) :: 'p mod_ring poly) = #f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ##f = #f
[PROOF STEP]
by (induct f, auto)