[STATEMENT]
lemma has_fields_fun:
  assumes "P \<turnstile> C has_fields FDTs" and "P \<turnstile> C has_fields FDTs'"
  shows "FDTs' = FDTs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. FDTs' = FDTs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C has_fields FDTs
P \<turnstile> C has_fields FDTs'

goal (1 subgoal):
 1. FDTs' = FDTs
[PROOF STEP]
proof(induction arbitrary: FDTs')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C D fs ms FDTs FDTs' FDTs'a. \<lbrakk>class P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; P \<turnstile> D has_fields FDTs; \<And>FDTs'. P \<turnstile> D has_fields FDTs' \<Longrightarrow> FDTs' = FDTs; FDTs' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ FDTs; P \<turnstile> C has_fields FDTs'a\<rbrakk> \<Longrightarrow> FDTs'a = FDTs'
 2. \<And>D fs ms FDTs FDTs'. \<lbrakk>class P Object = \<lfloor>(D, fs, ms)\<rfloor>; FDTs = map (\<lambda>(F, T). ((F, Object), T)) fs; P \<turnstile> Object has_fields FDTs'\<rbrakk> \<Longrightarrow> FDTs' = FDTs
[PROOF STEP]
case has_fields_Object
[PROOF STATE]
proof (state)
this:
class P Object = \<lfloor>(D_, fs_, ms_)\<rfloor>
FDTs_ = map (\<lambda>(F, T). ((F, Object), T)) fs_
P \<turnstile> Object has_fields FDTs'

goal (2 subgoals):
 1. \<And>C D fs ms FDTs FDTs' FDTs'a. \<lbrakk>class P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; P \<turnstile> D has_fields FDTs; \<And>FDTs'. P \<turnstile> D has_fields FDTs' \<Longrightarrow> FDTs' = FDTs; FDTs' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ FDTs; P \<turnstile> C has_fields FDTs'a\<rbrakk> \<Longrightarrow> FDTs'a = FDTs'
 2. \<And>D fs ms FDTs FDTs'. \<lbrakk>class P Object = \<lfloor>(D, fs, ms)\<rfloor>; FDTs = map (\<lambda>(F, T). ((F, Object), T)) fs; P \<turnstile> Object has_fields FDTs'\<rbrakk> \<Longrightarrow> FDTs' = FDTs
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
class P Object = \<lfloor>(D_, fs_, ms_)\<rfloor>
FDTs_ = map (\<lambda>(F, T). ((F, Object), T)) fs_
P \<turnstile> Object has_fields FDTs'

goal (1 subgoal):
 1. FDTs' = FDTs_
[PROOF STEP]
by(auto elim: Fields.cases)
[PROOF STATE]
proof (state)
this:
FDTs' = FDTs_

goal (1 subgoal):
 1. \<And>C D fs ms FDTs FDTs' FDTs'a. \<lbrakk>class P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; P \<turnstile> D has_fields FDTs; \<And>FDTs'. P \<turnstile> D has_fields FDTs' \<Longrightarrow> FDTs' = FDTs; FDTs' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ FDTs; P \<turnstile> C has_fields FDTs'a\<rbrakk> \<Longrightarrow> FDTs'a = FDTs'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C D fs ms FDTs FDTs' FDTs'a. \<lbrakk>class P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; P \<turnstile> D has_fields FDTs; \<And>FDTs'. P \<turnstile> D has_fields FDTs' \<Longrightarrow> FDTs' = FDTs; FDTs' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ FDTs; P \<turnstile> C has_fields FDTs'a\<rbrakk> \<Longrightarrow> FDTs'a = FDTs'
[PROOF STEP]
case (has_fields_rec C D fs ms Dres Cres Cres')
[PROOF STATE]
proof (state)
this:
class P C = \<lfloor>(D, fs, ms)\<rfloor>
C \<noteq> Object
P \<turnstile> D has_fields Dres
Cres = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ Dres
P \<turnstile> D has_fields ?FDTs' \<Longrightarrow> ?FDTs' = Dres
P \<turnstile> C has_fields Cres'

goal (1 subgoal):
 1. \<And>C D fs ms FDTs FDTs' FDTs'a. \<lbrakk>class P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; P \<turnstile> D has_fields FDTs; \<And>FDTs'. P \<turnstile> D has_fields FDTs' \<Longrightarrow> FDTs' = FDTs; FDTs' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ FDTs; P \<turnstile> C has_fields FDTs'a\<rbrakk> \<Longrightarrow> FDTs'a = FDTs'
[PROOF STEP]
from \<open>P \<turnstile> C has_fields Cres'\<close> \<open>C \<noteq> Object\<close> \<open>class P C = Some (D, fs, ms)\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<turnstile> C has_fields Cres'
C \<noteq> Object
class P C = \<lfloor>(D, fs, ms)\<rfloor>
[PROOF STEP]
obtain Dres' where DFields': "P \<turnstile> D has_fields Dres'"
    and Cres': "Cres' = map (\<lambda>(F,Tm). ((F,C),Tm)) fs @ Dres'"
[PROOF STATE]
proof (prove)
using this:
P \<turnstile> C has_fields Cres'
C \<noteq> Object
class P C = \<lfloor>(D, fs, ms)\<rfloor>

goal (1 subgoal):
 1. (\<And>Dres'. \<lbrakk>P \<turnstile> D has_fields Dres'; Cres' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ Dres'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by cases auto
[PROOF STATE]
proof (state)
this:
P \<turnstile> D has_fields Dres'
Cres' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ Dres'

goal (1 subgoal):
 1. \<And>C D fs ms FDTs FDTs' FDTs'a. \<lbrakk>class P C = \<lfloor>(D, fs, ms)\<rfloor>; C \<noteq> Object; P \<turnstile> D has_fields FDTs; \<And>FDTs'. P \<turnstile> D has_fields FDTs' \<Longrightarrow> FDTs' = FDTs; FDTs' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ FDTs; P \<turnstile> C has_fields FDTs'a\<rbrakk> \<Longrightarrow> FDTs'a = FDTs'
[PROOF STEP]
from has_fields_rec.IH[OF DFields'] \<open>Cres = map (\<lambda>(F,Tm). ((F,C),Tm)) fs @ Dres\<close> Cres'
[PROOF STATE]
proof (chain)
picking this:
Dres' = Dres
Cres = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ Dres
Cres' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ Dres'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Dres' = Dres
Cres = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ Dres
Cres' = map (\<lambda>(F, Tm). ((F, C), Tm)) fs @ Dres'

goal (1 subgoal):
 1. Cres' = Cres
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Cres' = Cres

goal:
No subgoals!
[PROOF STEP]
qed