[STATEMENT]
lemma Call_lemma:
 assumes
 Call: "\<forall>q \<in> dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub>
                 {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
                    \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma>}
                 (Call q)
                {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t},
                {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
 shows "\<And>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub>
              ({\<sigma>} \<inter> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
                                 \<Gamma>\<turnstile>the (\<Gamma> p)\<down>Normal s})
                 the (\<Gamma> p)
              {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t},
              {t. \<Gamma>\<turnstile>\<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s}) the (\<Gamma> p) {t. \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t}
[PROOF STEP]
apply (rule conseqPre)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (?P' Z) the (\<Gamma> p) {t. \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t}
 2. \<And>Z. {\<sigma>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s} \<subseteq> ?P' Z
[PROOF STEP]
apply (rule Call_lemma')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Z. \<forall>q\<in>dom \<Gamma>. \<forall>Za. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Za \<and> \<Gamma>\<turnstile> \<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call q \<down> Normal s \<and> ((s, q), ?\<sigma>3 Z, ?p3 Z) \<in> termi_call_steps \<Gamma>} Call q {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Za\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>Call q,Normal Za\<rangle> \<Rightarrow> Abrupt t}
 2. \<And>Z. {\<sigma>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s} \<subseteq> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>the (\<Gamma> (?p3 Z)) \<down> Normal (?\<sigma>3 Z) \<and> (\<exists>cs css. \<Gamma>\<turnstile> ([the (\<Gamma> (?p3 Z))], [], Normal (?\<sigma>3 Z)) \<rightarrow>\<^sup>* (the (\<Gamma> p) # cs, css, Normal s))}
[PROOF STEP]
apply (rule Call)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Z. {\<sigma>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s} \<subseteq> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal \<sigma> \<and> (\<exists>cs css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal \<sigma>) \<rightarrow>\<^sup>* (the (\<Gamma> p) # cs, css, Normal s))}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Call_lemma_switch_Call_body:
 assumes
 call: "\<forall>q \<in> dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub>
                 {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
                    \<Gamma>\<turnstile>Call q\<down>Normal s \<and> ((s,q),(\<sigma>,p)) \<in> termi_call_steps \<Gamma>}
                 (Call q)
                {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t},
                {t. \<Gamma>\<turnstile>\<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
 assumes p_defined: "p \<in> dom \<Gamma>"
 shows "\<And>Z. \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub>
              ({\<sigma>} \<inter> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
                                 \<Gamma>\<turnstile>Call p\<down>Normal s})
                 the (\<Gamma> p)
              {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
              {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call p \<down> Normal s}) the (\<Gamma> p) {t. \<Gamma>\<turnstile> \<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}
[PROOF STEP]
apply (simp only: exec_Call_body' [OF p_defined] noFaultStuck_Call_body' [OF p_defined] terminates_Normal_Call_body [OF p_defined])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<sigma>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s}) the (\<Gamma> p) {t. \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t}
[PROOF STEP]
apply (rule conseqPre)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> (?P' Z) the (\<Gamma> p) {t. \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal Z\<rangle> \<Rightarrow> Abrupt t}
 2. \<And>Z. {\<sigma>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s} \<subseteq> ?P' Z
[PROOF STEP]
apply (rule Call_lemma')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Z. \<forall>q\<in>dom \<Gamma>. \<forall>Za. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Za \<and> \<Gamma>\<turnstile> \<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call q \<down> Normal s \<and> ((s, q), ?\<sigma>3 Z, ?p3 Z) \<in> termi_call_steps \<Gamma>} Call q {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Za\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>Call q,Normal Za\<rangle> \<Rightarrow> Abrupt t}
 2. \<And>Z. {\<sigma>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s} \<subseteq> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>the (\<Gamma> (?p3 Z)) \<down> Normal (?\<sigma>3 Z) \<and> (\<exists>cs css. \<Gamma>\<turnstile> ([the (\<Gamma> (?p3 Z))], [], Normal (?\<sigma>3 Z)) \<rightarrow>\<^sup>* (the (\<Gamma> p) # cs, css, Normal s))}
[PROOF STEP]
apply (rule call)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>Z. {\<sigma>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal s} \<subseteq> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>the (\<Gamma> p),Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>the (\<Gamma> p) \<down> Normal \<sigma> \<and> (\<exists>cs css. \<Gamma>\<turnstile> ([the (\<Gamma> p)], [], Normal \<sigma>) \<rightarrow>\<^sup>* (the (\<Gamma> p) # cs, css, Normal s))}
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma MGT_Call:
"\<forall>p \<in> dom \<Gamma>. \<forall>Z.
  \<Gamma>,\<Theta> \<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
             \<Gamma>\<turnstile>(Call p)\<down>Normal s}
           (Call p)
          {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},
          {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p\<in>dom \<Gamma>. \<forall>Z. \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call p \<down> Normal s} Call p {t. \<Gamma>\<turnstile> \<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}
[PROOF STEP]
apply (intro ballI allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p Z. p \<in> dom \<Gamma> \<Longrightarrow> \<Gamma>,\<Theta>\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call p \<down> Normal s} Call p {t. \<Gamma>\<turnstile> \<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}
[PROOF STEP]
apply (rule CallRec' [where Procs="dom \<Gamma>" and
    P="\<lambda>p Z. {s. s=Z \<and> \<Gamma>\<turnstile>\<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>({Stuck} \<union> Fault ` (-F)) \<and>
                    \<Gamma>\<turnstile>Call p\<down>Normal s}" and
    Q="\<lambda>p Z. {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t}" and
    A="\<lambda>p Z. {t. \<Gamma>\<turnstile>\<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}" and
    r="termi_call_steps \<Gamma>"
    ])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>p Z. p \<in> dom \<Gamma> \<Longrightarrow> p \<in> dom \<Gamma>
 2. \<And>p Z. p \<in> dom \<Gamma> \<Longrightarrow> dom \<Gamma> \<subseteq> dom \<Gamma>
 3. \<And>p Z. p \<in> dom \<Gamma> \<Longrightarrow> wf (termi_call_steps \<Gamma>)
 4. \<And>p Z. p \<in> dom \<Gamma> \<Longrightarrow> \<forall>p\<in>dom \<Gamma>. \<forall>\<tau> Z. \<Gamma>,\<Theta> \<union> (\<Union>q\<in>dom \<Gamma>. \<Union>Z. {({s. s = Z \<and> \<Gamma>\<turnstile> \<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call q \<down> Normal s} \<inter> {s. ((s, q), \<tau>, p) \<in> termi_call_steps \<Gamma>}, q, {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t})})\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call p \<down> Normal s}) the (\<Gamma> p) {t. \<Gamma>\<turnstile> \<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}
[PROOF STEP]
apply    simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>p Z. p \<in> dom \<Gamma> \<Longrightarrow> dom \<Gamma> \<subseteq> dom \<Gamma>
 2. \<And>p Z. p \<in> dom \<Gamma> \<Longrightarrow> wf (termi_call_steps \<Gamma>)
 3. \<And>p Z. p \<in> dom \<Gamma> \<Longrightarrow> \<forall>p\<in>dom \<Gamma>. \<forall>\<tau> Z. \<Gamma>,\<Theta> \<union> (\<Union>q\<in>dom \<Gamma>. \<Union>Z. {({s. s = Z \<and> \<Gamma>\<turnstile> \<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call q \<down> Normal s} \<inter> {s. ((s, q), \<tau>, p) \<in> termi_call_steps \<Gamma>}, q, {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t})})\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call p \<down> Normal s}) the (\<Gamma> p) {t. \<Gamma>\<turnstile> \<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}
[PROOF STEP]
apply   simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p Z. p \<in> dom \<Gamma> \<Longrightarrow> wf (termi_call_steps \<Gamma>)
 2. \<And>p Z. p \<in> dom \<Gamma> \<Longrightarrow> \<forall>p\<in>dom \<Gamma>. \<forall>\<tau> Z. \<Gamma>,\<Theta> \<union> (\<Union>q\<in>dom \<Gamma>. \<Union>Z. {({s. s = Z \<and> \<Gamma>\<turnstile> \<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call q \<down> Normal s} \<inter> {s. ((s, q), \<tau>, p) \<in> termi_call_steps \<Gamma>}, q, {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t})})\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call p \<down> Normal s}) the (\<Gamma> p) {t. \<Gamma>\<turnstile> \<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}
[PROOF STEP]
apply  (rule wf_termi_call_steps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p Z. p \<in> dom \<Gamma> \<Longrightarrow> \<forall>p\<in>dom \<Gamma>. \<forall>\<tau> Z. \<Gamma>,\<Theta> \<union> (\<Union>q\<in>dom \<Gamma>. \<Union>Z. {({s. s = Z \<and> \<Gamma>\<turnstile> \<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call q \<down> Normal s} \<inter> {s. ((s, q), \<tau>, p) \<in> termi_call_steps \<Gamma>}, q, {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t})})\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>Call p,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call p \<down> Normal s}) the (\<Gamma> p) {t. \<Gamma>\<turnstile> \<langle>Call p,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>Call p,Normal Z\<rangle> \<Rightarrow> Abrupt t}
[PROOF STEP]
apply (intro ballI allI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p Z pa \<tau> Za. \<lbrakk>p \<in> dom \<Gamma>; pa \<in> dom \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta> \<union> (\<Union>q\<in>dom \<Gamma>. \<Union>Z. {({s. s = Z \<and> \<Gamma>\<turnstile> \<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call q \<down> Normal s} \<inter> {s. ((s, q), \<tau>, pa) \<in> termi_call_steps \<Gamma>}, q, {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t})})\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> {s. s = Za \<and> \<Gamma>\<turnstile> \<langle>Call pa,Normal s\<rangle> \<Rightarrow>\<notin>{Stuck} \<union> Fault ` (- F) \<and> \<Gamma>\<turnstile>Call pa \<down> Normal s}) the (\<Gamma> pa) {t. \<Gamma>\<turnstile> \<langle>Call pa,Normal Za\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>Call pa,Normal Za\<rangle> \<Rightarrow> Abrupt t}
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p pa \<tau> Za. \<lbrakk>p \<in> dom \<Gamma>; pa \<in> dom \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta> \<union> (\<Union>x\<in>dom \<Gamma>. \<Union>xa. {({s. s = xa \<and> \<Gamma>\<turnstile> \<langle>Call x,Normal s\<rangle> \<Rightarrow>\<notin>insert Stuck (Fault ` (- F)) \<and> \<Gamma>\<turnstile>Call x \<down> Normal s} \<inter> {s. ((s, x), \<tau>, pa) \<in> termi_call_steps \<Gamma>}, x, {t. \<Gamma>\<turnstile> \<langle>Call x,Normal xa\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile> \<langle>Call x,Normal xa\<rangle> \<Rightarrow> Abrupt t})})\<turnstile>\<^sub>t\<^bsub>/F\<^esub> ({\<tau>} \<inter> {s. s = Za \<and> \<Gamma>\<turnstile> \<langle>Call pa,Normal s\<rangle> \<Rightarrow>\<notin>insert Stuck (Fault ` (- F)) \<and> \<Gamma>\<turnstile>Call pa \<down> Normal s}) the (\<Gamma> pa) {t. \<Gamma>\<turnstile> \<langle>Call pa,Normal Za\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>Call pa,Normal Za\<rangle> \<Rightarrow> Abrupt t}
[PROOF STEP]
apply (rule Call_lemma_switch_Call_body [rule_format, simplified])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p pa \<tau> Za q Z. \<lbrakk>p \<in> dom \<Gamma>; pa \<in> dom \<Gamma>; q \<in> dom \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma>,\<Theta> \<union> (\<Union>x\<in>dom \<Gamma>. \<Union>xa. {({s. s = xa \<and> \<Gamma>\<turnstile> \<langle>Call x,Normal s\<rangle> \<Rightarrow>\<notin>insert Stuck (Fault ` (- F)) \<and> \<Gamma>\<turnstile>Call x \<down> Normal s} \<inter> {s. ((s, x), \<tau>, pa) \<in> termi_call_steps \<Gamma>}, x, {t. \<Gamma>\<turnstile> \<langle>Call x,Normal xa\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile> \<langle>Call x,Normal xa\<rangle> \<Rightarrow> Abrupt t})})\<turnstile>\<^sub>t\<^bsub>/F\<^esub> {s. s = Z \<and> \<Gamma>\<turnstile> \<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>insert Stuck (Fault ` (- F)) \<and> \<Gamma>\<turnstile>Call q \<down> Normal s \<and> ((s, q), \<tau>, pa) \<in> termi_call_steps \<Gamma>} Call q {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t},{t. \<Gamma>\<turnstile> \<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}
 2. \<And>p pa \<tau> Za. \<lbrakk>p \<in> dom \<Gamma>; pa \<in> dom \<Gamma>\<rbrakk> \<Longrightarrow> pa \<in> dom \<Gamma>
[PROOF STEP]
apply  (rule hoaret.Asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>p pa \<tau> Za q Z. \<lbrakk>p \<in> dom \<Gamma>; pa \<in> dom \<Gamma>; q \<in> dom \<Gamma>\<rbrakk> \<Longrightarrow> ({s. s = Z \<and> \<Gamma>\<turnstile> \<langle>Call q,Normal s\<rangle> \<Rightarrow>\<notin>insert Stuck (Fault ` (- F)) \<and> \<Gamma>\<turnstile>Call q \<down> Normal s \<and> ((s, q), \<tau>, pa) \<in> termi_call_steps \<Gamma>}, q, {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Z\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile> \<langle>Call q,Normal Z\<rangle> \<Rightarrow> Abrupt t}) \<in> \<Theta> \<union> (\<Union>x\<in>dom \<Gamma>. \<Union>xa. {({s. s = xa \<and> \<Gamma>\<turnstile> \<langle>Call x,Normal s\<rangle> \<Rightarrow>\<notin>insert Stuck (Fault ` (- F)) \<and> \<Gamma>\<turnstile>Call x \<down> Normal s} \<inter> {s. ((s, x), \<tau>, pa) \<in> termi_call_steps \<Gamma>}, x, {t. \<Gamma>\<turnstile> \<langle>Call x,Normal xa\<rangle> \<Rightarrow> Normal t}, {t. \<Gamma>\<turnstile> \<langle>Call x,Normal xa\<rangle> \<Rightarrow> Abrupt t})})
 2. \<And>p pa \<tau> Za. \<lbrakk>p \<in> dom \<Gamma>; pa \<in> dom \<Gamma>\<rbrakk> \<Longrightarrow> pa \<in> dom \<Gamma>
[PROOF STEP]
apply  fastforce
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p pa \<tau> Za. \<lbrakk>p \<in> dom \<Gamma>; pa \<in> dom \<Gamma>\<rbrakk> \<Longrightarrow> pa \<in> dom \<Gamma>
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma CollInt_iff: "{s. P s} \<inter> {s. Q s} = {s. P s \<and> Q s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {s. P s} \<inter> {s. Q s} = {s. P s \<and> Q s}
[PROOF STEP]
by auto


[STATEMENT]
lemma image_Un_conv: "f ` (\<Union>p\<in>dom \<Gamma>. \<Union>Z. {x p Z}) =  (\<Union>p\<in>dom \<Gamma>. \<Union>Z. {f (x p Z)})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` (\<Union>p\<in>dom \<Gamma>. \<Union>Z. {x p Z}) = (\<Union>p\<in>dom \<Gamma>. \<Union>Z. {f (x p Z)})
[PROOF STEP]
by (auto iff: not_None_eq)


[STATEMENT]
lemma BaseUnits:
  "is_base_unit metre" "is_base_unit second" "is_base_unit kilogram" "is_base_unit ampere"
  "is_base_unit kelvin" "is_base_unit mole" "is_base_unit candela"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_base_unit metre &&& is_base_unit second &&& is_base_unit kilogram) &&& (is_base_unit ampere &&& is_base_unit kelvin) &&& is_base_unit mole &&& is_base_unit candela
[PROOF STEP]
by (simp_all add: mk_base_unit)


[STATEMENT]
lemma "(metre \<^bold>\<cdot> second\<^sup>-\<^sup>\<one>) \<^bold>\<cdot> second \<cong>\<^sub>Q metre"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. metre \<^bold>\<cdot> second\<^sup>-\<^sup>\<one> \<^bold>\<cdot> second \<cong>\<^sub>Q metre
[PROOF STEP]
by (si_calc)


[STATEMENT]
lemma qmconv_self: "QMC('s::metrifiable \<rightarrow> 's) = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. QMC('s \<rightarrow> 's) = id
[PROOF STEP]
by (simp add: fun_eq_iff)


[STATEMENT]
lemma srrstep_ground:
  assumes "ground_sys \<R>"
    and "(s, t) \<in> srrstep \<F> \<R>"
  shows "ground s" "ground t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground s &&& ground t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ground_sys \<R>
(s, t) \<in> srrstep \<F> \<R>

goal (1 subgoal):
 1. ground s &&& ground t
[PROOF STEP]
by (auto simp: sig_step_def ground_subst_apply vars_term_subst elim!: rrstep_subst)


[STATEMENT]
lemma srstep_pres_ground_l:
  assumes "ground_sys \<R>" "ground s"
    and "(s, t) \<in> srstep \<F> \<R>"
  shows "ground t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ground_sys \<R>
ground s
(s, t) \<in> srstep \<F> \<R>

goal (1 subgoal):
 1. ground t
[PROOF STEP]
by (auto simp: sig_step_def ground_subst_apply dest!: rstep_imp_C_s_r)


[STATEMENT]
lemma srstep_pres_ground_r:
  assumes "ground_sys \<R>" "ground t"
    and "(s, t) \<in> srstep \<F> \<R>"
  shows "ground s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ground_sys \<R>
ground t
(s, t) \<in> srstep \<F> \<R>

goal (1 subgoal):
 1. ground s
[PROOF STEP]
by (auto simp: ground_vars_term_empty vars_term_subst sig_step_def vars_term_ctxt_apply ground_subst_apply dest!: rstep_imp_C_s_r)


[STATEMENT]
lemma srsteps_pres_ground_l:
  assumes "ground_sys \<R>" "ground s"
   and  "(s, t) \<in> (srstep \<F> \<R>)\<^sup>+"
  shows "ground t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground t
[PROOF STEP]
using assms(3, 2) srstep_pres_ground_l[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> (srstep \<F> \<R>)\<^sup>+
ground s
\<lbrakk>ground ?s; (?s, ?t) \<in> srstep ?\<F> \<R>\<rbrakk> \<Longrightarrow> ground ?t

goal (1 subgoal):
 1. ground t
[PROOF STEP]
by (induct rule: converse_trancl_induct) auto


[STATEMENT]
lemma srsteps_pres_ground_r:
  assumes "ground_sys \<R>" "ground t"
    and "(s, t) \<in> (srstep \<F> \<R>)\<^sup>+"
  shows "ground s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground s
[PROOF STEP]
using assms(3, 2) srstep_pres_ground_r[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> (srstep \<F> \<R>)\<^sup>+
ground t
\<lbrakk>ground ?t; (?s, ?t) \<in> srstep ?\<F> \<R>\<rbrakk> \<Longrightarrow> ground ?s

goal (1 subgoal):
 1. ground s
[PROOF STEP]
by (induct rule: converse_trancl_induct) auto


[STATEMENT]
lemma srsteps_eq_pres_ground_l:
  assumes "ground_sys \<R>" "ground s"
   and  "(s, t) \<in> (srstep \<F> \<R>)\<^sup>*"
  shows "ground t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground t
[PROOF STEP]
using srsteps_pres_ground_l[OF assms(1, 2)] assms(2, 3)
[PROOF STATE]
proof (prove)
using this:
(s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>+ \<Longrightarrow> ground ?t
ground s
(s, t) \<in> (srstep \<F> \<R>)\<^sup>*

goal (1 subgoal):
 1. ground t
[PROOF STEP]
by (auto simp: rtrancl_eq_or_trancl)


[STATEMENT]
lemma srsteps_eq_pres_ground_r:
  assumes "ground_sys \<R>" "ground t"
    and "(s, t) \<in> (srstep \<F> \<R>)\<^sup>*"
  shows "ground s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground s
[PROOF STEP]
using srsteps_pres_ground_r[OF assms(1, 2)] assms(2, 3)
[PROOF STATE]
proof (prove)
using this:
(?s, t) \<in> (srstep ?\<F> \<R>)\<^sup>+ \<Longrightarrow> ground ?s
ground t
(s, t) \<in> (srstep \<F> \<R>)\<^sup>*

goal (1 subgoal):
 1. ground s
[PROOF STEP]
by (auto simp: rtrancl_eq_or_trancl)


[STATEMENT]
lemma srsteps_with_root_step_ground:
  assumes "ground_sys \<R>"
    and "(s, t) \<in> srsteps_with_root_step \<F> \<R>"
  shows "ground s" "ground t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground s &&& ground t
[PROOF STEP]
using srrstep_ground[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> ground ?s
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> ground ?t

goal (1 subgoal):
 1. ground s &&& ground t
[PROOF STEP]
using srsteps_eq_pres_ground_l[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> ground ?s
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> ground ?t
\<lbrakk>ground ?s; (?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>*\<rbrakk> \<Longrightarrow> ground ?t

goal (1 subgoal):
 1. ground s &&& ground t
[PROOF STEP]
using srsteps_eq_pres_ground_r[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> ground ?s
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> ground ?t
\<lbrakk>ground ?s; (?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>*\<rbrakk> \<Longrightarrow> ground ?t
\<lbrakk>ground ?t; (?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>*\<rbrakk> \<Longrightarrow> ground ?s

goal (1 subgoal):
 1. ground s &&& ground t
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> ground ?s
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> ground ?t
\<lbrakk>ground ?s; (?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>*\<rbrakk> \<Longrightarrow> ground ?t
\<lbrakk>ground ?t; (?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>*\<rbrakk> \<Longrightarrow> ground ?s
(s, t) \<in> srsteps_with_root_step \<F> \<R>

goal (1 subgoal):
 1. ground s &&& ground t
[PROOF STEP]
unfolding srsteps_with_root_step_def
[PROOF STATE]
proof (prove)
using this:
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> ground ?s
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> ground ?t
\<lbrakk>ground ?s; (?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>*\<rbrakk> \<Longrightarrow> ground ?t
\<lbrakk>ground ?t; (?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>*\<rbrakk> \<Longrightarrow> ground ?s
(s, t) \<in> (srstep \<F> \<R>)\<^sup>* O srrstep \<F> \<R> O (srstep \<F> \<R>)\<^sup>*

goal (1 subgoal):
 1. ground s &&& ground t
[PROOF STEP]
by (meson relcomp.cases)+


[STATEMENT]
lemma srrstep_funas:
  assumes "ground_sys \<R>"
    and "(s, t) \<in> srrstep \<F> \<R>"
  shows "funas_term s \<subseteq> funas_rel \<R>" "funas_term t \<subseteq> funas_rel \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_term s \<subseteq> funas_rel \<R> &&& funas_term t \<subseteq> funas_rel \<R>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ground_sys \<R>
(s, t) \<in> srrstep \<F> \<R>

goal (1 subgoal):
 1. funas_term s \<subseteq> funas_rel \<R> &&& funas_term t \<subseteq> funas_rel \<R>
[PROOF STEP]
by (auto simp: sig_step_def funas_term_subst ground_vars_term_empty funas_rel_def split: prod.splits elim!: rrstep_subst)


[STATEMENT]
lemma srstep_funas_l:
  assumes "ground_sys \<R>"
    and "(s, t) \<in> srstep \<F> \<R>"
  shows "funas_term t \<subseteq> funas_term s \<union> funas_rel \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_term t \<subseteq> funas_term s \<union> funas_rel \<R>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ground_sys \<R>
(s, t) \<in> srstep \<F> \<R>

goal (1 subgoal):
 1. funas_term t \<subseteq> funas_term s \<union> funas_rel \<R>
[PROOF STEP]
by (auto simp: ground_vars_term_empty vars_term_subst sig_step_def vars_term_ctxt_apply
     funas_term_subst funas_rel_def split: prod.splits dest!: rstep_imp_C_s_r)


[STATEMENT]
lemma srstep_funas_r:
  assumes "ground_sys \<R>"
    and "(s, t) \<in> srstep \<F> \<R>"
  shows "funas_term s \<subseteq> funas_term t \<union> funas_rel \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_term s \<subseteq> funas_term t \<union> funas_rel \<R>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ground_sys \<R>
(s, t) \<in> srstep \<F> \<R>

goal (1 subgoal):
 1. funas_term s \<subseteq> funas_term t \<union> funas_rel \<R>
[PROOF STEP]
by (auto simp: ground_vars_term_empty vars_term_subst sig_step_def vars_term_ctxt_apply
     funas_term_subst funas_rel_def split: prod.splits dest!: rstep_imp_C_s_r)


[STATEMENT]
lemma srsteps_funas_l:
  assumes "ground_sys \<R>"
   and  "(s, t) \<in> (srstep \<F> \<R>)\<^sup>+"
  shows "funas_term t \<subseteq> funas_term s \<union> funas_rel \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_term t \<subseteq> funas_term s \<union> funas_rel \<R>
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> (srstep \<F> \<R>)\<^sup>+

goal (1 subgoal):
 1. funas_term t \<subseteq> funas_term s \<union> funas_rel \<R>
[PROOF STEP]
by (induct rule: converse_trancl_induct) (auto dest: srstep_funas_l[OF assms(1)])


[STATEMENT]
lemma srsteps_funas_r:
  assumes "ground_sys \<R>"
    and "(s, t) \<in> (srstep \<F> \<R>)\<^sup>+"
  shows "funas_term s \<subseteq> funas_term t \<union> funas_rel \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_term s \<subseteq> funas_term t \<union> funas_rel \<R>
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(s, t) \<in> (srstep \<F> \<R>)\<^sup>+

goal (1 subgoal):
 1. funas_term s \<subseteq> funas_term t \<union> funas_rel \<R>
[PROOF STEP]
by (induct rule: converse_trancl_induct) (auto dest: srstep_funas_r[OF assms(1)])


[STATEMENT]
lemma srsteps_eq_funas_l:
  assumes "ground_sys \<R>"
    and "(s, t) \<in> (srstep \<F> \<R>)\<^sup>*"
  shows "funas_term t \<subseteq> funas_term s \<union> funas_rel \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_term t \<subseteq> funas_term s \<union> funas_rel \<R>
[PROOF STEP]
using srsteps_funas_l[OF assms(1)] assms(2)
[PROOF STATE]
proof (prove)
using this:
(?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>+ \<Longrightarrow> funas_term ?t \<subseteq> funas_term ?s \<union> funas_rel \<R>
(s, t) \<in> (srstep \<F> \<R>)\<^sup>*

goal (1 subgoal):
 1. funas_term t \<subseteq> funas_term s \<union> funas_rel \<R>
[PROOF STEP]
by (auto simp: rtrancl_eq_or_trancl)


[STATEMENT]
lemma srsteps_eq_funas_r:
  assumes "ground_sys \<R>"
    and "(s, t) \<in> (srstep \<F> \<R>)\<^sup>*"
  shows "funas_term s \<subseteq> funas_term t \<union> funas_rel \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_term s \<subseteq> funas_term t \<union> funas_rel \<R>
[PROOF STEP]
using srsteps_funas_r[OF assms(1)] assms(2)
[PROOF STATE]
proof (prove)
using this:
(?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>+ \<Longrightarrow> funas_term ?s \<subseteq> funas_term ?t \<union> funas_rel \<R>
(s, t) \<in> (srstep \<F> \<R>)\<^sup>*

goal (1 subgoal):
 1. funas_term s \<subseteq> funas_term t \<union> funas_rel \<R>
[PROOF STEP]
by (auto simp: rtrancl_eq_or_trancl)


[STATEMENT]
lemma srsteps_with_root_step_funas:
  assumes "ground_sys \<R>"
    and "(s, t) \<in> srsteps_with_root_step \<F> \<R>"
  shows "funas_term s \<subseteq> funas_rel \<R>" "funas_term t \<subseteq> funas_rel \<R>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_term s \<subseteq> funas_rel \<R> &&& funas_term t \<subseteq> funas_rel \<R>
[PROOF STEP]
using srrstep_funas[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> funas_term ?s \<subseteq> funas_rel \<R>
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> funas_term ?t \<subseteq> funas_rel \<R>

goal (1 subgoal):
 1. funas_term s \<subseteq> funas_rel \<R> &&& funas_term t \<subseteq> funas_rel \<R>
[PROOF STEP]
using srsteps_eq_funas_l[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> funas_term ?s \<subseteq> funas_rel \<R>
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> funas_term ?t \<subseteq> funas_rel \<R>
(?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>* \<Longrightarrow> funas_term ?t \<subseteq> funas_term ?s \<union> funas_rel \<R>

goal (1 subgoal):
 1. funas_term s \<subseteq> funas_rel \<R> &&& funas_term t \<subseteq> funas_rel \<R>
[PROOF STEP]
using srsteps_eq_funas_r[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> funas_term ?s \<subseteq> funas_rel \<R>
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> funas_term ?t \<subseteq> funas_rel \<R>
(?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>* \<Longrightarrow> funas_term ?t \<subseteq> funas_term ?s \<union> funas_rel \<R>
(?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>* \<Longrightarrow> funas_term ?s \<subseteq> funas_term ?t \<union> funas_rel \<R>

goal (1 subgoal):
 1. funas_term s \<subseteq> funas_rel \<R> &&& funas_term t \<subseteq> funas_rel \<R>
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> funas_term ?s \<subseteq> funas_rel \<R>
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> funas_term ?t \<subseteq> funas_rel \<R>
(?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>* \<Longrightarrow> funas_term ?t \<subseteq> funas_term ?s \<union> funas_rel \<R>
(?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>* \<Longrightarrow> funas_term ?s \<subseteq> funas_term ?t \<union> funas_rel \<R>
(s, t) \<in> srsteps_with_root_step \<F> \<R>

goal (1 subgoal):
 1. funas_term s \<subseteq> funas_rel \<R> &&& funas_term t \<subseteq> funas_rel \<R>
[PROOF STEP]
unfolding srsteps_with_root_step_def
[PROOF STATE]
proof (prove)
using this:
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> funas_term ?s \<subseteq> funas_rel \<R>
(?s, ?t) \<in> srrstep ?\<F> \<R> \<Longrightarrow> funas_term ?t \<subseteq> funas_rel \<R>
(?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>* \<Longrightarrow> funas_term ?t \<subseteq> funas_term ?s \<union> funas_rel \<R>
(?s, ?t) \<in> (srstep ?\<F> \<R>)\<^sup>* \<Longrightarrow> funas_term ?s \<subseteq> funas_term ?t \<union> funas_rel \<R>
(s, t) \<in> (srstep \<F> \<R>)\<^sup>* O srrstep \<F> \<R> O (srstep \<F> \<R>)\<^sup>*

goal (1 subgoal):
 1. funas_term s \<subseteq> funas_rel \<R> &&& funas_term t \<subseteq> funas_rel \<R>
[PROOF STEP]
by (metis relcompEpair sup_absorb2)+


[STATEMENT]
lemma asimp_pretty:
"asimp (Less r cs) =
 (if \<forall>c\<in> set cs. c = 0
  then if r<0 then TrueF else FalseF
  else Atom(Less r cs))"
"asimp (Eq r cs) =
 (if \<forall>c\<in> set cs. c = 0
  then if r=0 then TrueF else FalseF
  else Atom(Eq r cs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. asimp (Less r cs) = (if \<forall>c\<in>set cs. c = 0 then if r < 0 then TrueF else FalseF else Atom (Less r cs)) &&& asimp (Eq r cs) = (if \<forall>c\<in>set cs. c = 0 then if r = 0 then TrueF else FalseF else Atom (Eq r cs))
[PROOF STEP]
by(auto simp:asimp_def)


[STATEMENT]
lemma I_asimp: "R.I (asimp a) xs = I\<^sub>R a xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R.I (asimp a) xs = I\<^sub>R a xs
[PROOF STEP]
by(simp add:asimp_def iprod0_if_coeffs0 split:atom.split)


[STATEMENT]
lemma I_qe_FMo\<^sub>1: "R.I (qe_FMo\<^sub>1 as) xs = R.I (qe_FM\<^sub>1 as) xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R.I (qe_FMo\<^sub>1 as) xs = R.I (qe_FM\<^sub>1 as) xs
[PROOF STEP]
by(simp add:qe_FM\<^sub>1_def qe_FMo\<^sub>1_def I_asimp)


[STATEMENT]
lemma qfree_qe_FMo\<^sub>1: "qfree (qe_FMo\<^sub>1 as)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qfree (qe_FMo\<^sub>1 as)
[PROOF STEP]
by(auto simp:qe_FM\<^sub>1_def qe_FMo\<^sub>1_def asimp_def intro!:qfree_list_conj
        split:atom.split)


[STATEMENT]
theorem qfree_qe_FMo: "qfree (qe_FMo f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. qfree (qe_FMo f)
[PROOF STEP]
by(simp add:qe_FMo_def R\<^sub>e.qfree_lift_dnfeq_qe qfree_qe_FMo\<^sub>1)


[STATEMENT]
lemma sub_points: "x \<in> \<U> \<Longrightarrow> x \<in> \<V>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<U> \<Longrightarrow> x \<in> \<V>
[PROOF STEP]
using points_subset
[PROOF STATE]
proof (prove)
using this:
\<U> \<subseteq> \<V>

goal (1 subgoal):
 1. x \<in> \<U> \<Longrightarrow> x \<in> \<V>
[PROOF STEP]
by auto


[STATEMENT]
lemma sub_blocks: "bl \<in># \<A> \<Longrightarrow> bl \<in># \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bl \<in># \<A> \<Longrightarrow> bl \<in># \<B>
[PROOF STEP]
using blocks_subset
[PROOF STATE]
proof (prove)
using this:
\<A> \<subseteq># \<B>

goal (1 subgoal):
 1. bl \<in># \<A> \<Longrightarrow> bl \<in># \<B>
[PROOF STEP]
by auto


[STATEMENT]
lemma sub_blocks_count: "count \<A> b \<le> count \<B> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count \<A> b \<le> multiplicity b
[PROOF STEP]
by (simp add: mset_subset_eq_count blocks_subset)


[STATEMENT]
lemma sub_non_empty_blocks: "A \<in># \<A> \<Longrightarrow> A \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A \<in># \<A> \<Longrightarrow> A \<noteq> {}
[PROOF STEP]
using des.blocks_nempty sub_blocks
[PROOF STATE]
proof (prove)
using this:
?bl \<in># \<B> \<Longrightarrow> ?bl \<noteq> {}
?bl \<in># \<A> \<Longrightarrow> ?bl \<in># \<B>

goal (1 subgoal):
 1. A \<in># \<A> \<Longrightarrow> A \<noteq> {}
[PROOF STEP]
by simp


[STATEMENT]
lemma point_sets_ne: "\<U> \<noteq> \<V>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<U> \<noteq> \<V>
[PROOF STEP]
using points_psubset
[PROOF STATE]
proof (prove)
using this:
\<U> \<subset> \<V>

goal (1 subgoal):
 1. \<U> \<noteq> \<V>
[PROOF STEP]
by auto


[STATEMENT]
lemma sub_is_proper: "\<U> \<noteq> \<V> \<Longrightarrow> proper_sub_set_system \<U> \<A> \<V> \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<U> \<noteq> \<V> \<Longrightarrow> proper_sub_set_system \<U> \<A> \<V> \<B>
[PROOF STEP]
using blocks_subset incidence_system_axioms
[PROOF STATE]
proof (prove)
using this:
\<A> \<subseteq># \<B>
incidence_system \<V> \<B>

goal (1 subgoal):
 1. \<U> \<noteq> \<V> \<Longrightarrow> proper_sub_set_system \<U> \<A> \<V> \<B>
[PROOF STEP]
by (simp add: points_subset proper_sub_set_system.intro proper_sub_set_system_axioms_def psubsetI)


[STATEMENT]
lemma sub_is_proper: "\<U> \<noteq> \<V> \<Longrightarrow> proper_sub_incidence_system \<U> \<A> \<V> \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<U> \<noteq> \<V> \<Longrightarrow> proper_sub_incidence_system \<U> \<A> \<V> \<B>
[PROOF STEP]
by (simp add: ins.incidence_system_axioms proper_sub_incidence_system_def sub_is_proper)


[STATEMENT]
lemma sub_is_proper: "\<U> \<noteq> \<V> \<Longrightarrow> proper_sub_design \<U> \<A> \<V> \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<U> \<noteq> \<V> \<Longrightarrow> proper_sub_design \<U> \<A> \<V> \<B>
[PROOF STEP]
by (simp add: des.wf_design proper_sub_design.intro sub_is_proper)


[STATEMENT]
lemma ss_proper_implies_sub [intro]: "proper_sub_set_system \<U> \<A> \<V> \<B> \<Longrightarrow> sub_set_system \<U> \<A> \<V> \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_sub_set_system \<U> \<A> \<V> \<B> \<Longrightarrow> sub_set_system \<U> \<A> \<V> \<B>
[PROOF STEP]
using proper_sub_set_system.axioms(1) proper_sub_set_system.blocks_subset psubsetE
[PROOF STATE]
proof (prove)
using this:
proper_sub_set_system ?\<U> ?\<A> ?\<V> ?\<B> \<Longrightarrow> incidence_system ?\<V> ?\<B>
proper_sub_set_system ?\<U> ?\<A> ?\<V> ?\<B> \<Longrightarrow> ?\<A> \<subseteq># ?\<B>
\<lbrakk>?A \<subset> ?B; \<lbrakk>?A \<subseteq> ?B; \<not> ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R

goal (1 subgoal):
 1. proper_sub_set_system \<U> \<A> \<V> \<B> \<Longrightarrow> sub_set_system \<U> \<A> \<V> \<B>
[PROOF STEP]
by (metis proper_sub_set_system.points_psubset sub_set_system.intro sub_set_system_axioms_def)


[STATEMENT]
lemma sub_ssI [intro!]: "incidence_system \<V> \<B> \<Longrightarrow> \<U> \<subseteq> \<V> \<Longrightarrow> \<A> \<subseteq># \<B> \<Longrightarrow> sub_set_system \<U> \<A> \<V> \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>incidence_system \<V> \<B>; \<U> \<subseteq> \<V>; \<A> \<subseteq># \<B>\<rbrakk> \<Longrightarrow> sub_set_system \<U> \<A> \<V> \<B>
[PROOF STEP]
using incidence_system_def subset_iff
[PROOF STATE]
proof (prove)
using this:
incidence_system ?point_set ?block_collection \<equiv> \<forall>b. b \<in># ?block_collection \<longrightarrow> b \<subseteq> ?point_set
(?A \<subseteq> ?B) = (\<forall>t. t \<in> ?A \<longrightarrow> t \<in> ?B)

goal (1 subgoal):
 1. \<lbrakk>incidence_system \<V> \<B>; \<U> \<subseteq> \<V>; \<A> \<subseteq># \<B>\<rbrakk> \<Longrightarrow> sub_set_system \<U> \<A> \<V> \<B>
[PROOF STEP]
by (unfold_locales) (simp_all add: incidence_system.wellformed)


[STATEMENT]
lemma sub_ss_equality:
  assumes "sub_set_system \<U> \<A> \<V> \<B>"
    and "sub_set_system \<V> \<B> \<U> \<A>"
  shows "\<U> = \<V>" and "\<A> = \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<U> = \<V> &&& \<A> = \<B>
[PROOF STEP]
using assms(1) assms(2) sub_set_system.points_subset
[PROOF STATE]
proof (prove)
using this:
sub_set_system \<U> \<A> \<V> \<B>
sub_set_system \<V> \<B> \<U> \<A>
sub_set_system ?\<U> ?\<A> ?\<V> ?\<B> \<Longrightarrow> ?\<U> \<subseteq> ?\<V>

goal (1 subgoal):
 1. \<U> = \<V> &&& \<A> = \<B>
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<A> = \<B>
[PROOF STEP]
by (meson assms(1) assms(2) sub_set_system.blocks_subset subset_mset.eq_iff)


[STATEMENT]
lemma sub_sys_block_sizes: "ins.sys_block_sizes \<subseteq> sys_block_sizes"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ins.sys_block_sizes \<subseteq> sys_block_sizes
[PROOF STEP]
by (auto simp add: sys_block_sizes_def ins.sys_block_sizes_def blocks_subset sub_blocks)


[STATEMENT]
lemma sub_point_rep_number_le: "x \<in> \<U> \<Longrightarrow> \<A> rep x \<le> \<B> rep x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<U> \<Longrightarrow> \<A> rep x \<le> \<B> rep x
[PROOF STEP]
by (simp add: point_replication_number_def blocks_subset multiset_filter_mono size_mset_mono)


[STATEMENT]
lemma sub_point_index_le: "ps \<subseteq> \<U> \<Longrightarrow> \<A> index ps \<le> \<B> index ps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ps \<subseteq> \<U> \<Longrightarrow> \<A> index ps \<le> \<B> index ps
[PROOF STEP]
by (simp add: points_index_def blocks_subset multiset_filter_mono size_mset_mono)


[STATEMENT]
lemma sub_sys_intersection_numbers: "ins.intersection_numbers \<subseteq> intersection_numbers"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ins.intersection_numbers \<subseteq> intersection_numbers
[PROOF STEP]
apply (auto simp add: intersection_numbers_def ins.intersection_numbers_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b1 b2. \<lbrakk>b1 \<in># \<A>; b2 \<in># remove1_mset b1 \<A>\<rbrakk> \<Longrightarrow> \<exists>b1a b2a. b1 |\<inter>| b2 = b1a |\<inter>| b2a \<and> b1a \<in># \<B> \<and> b2a \<in># remove1_mset b1a \<B>
[PROOF STEP]
by (metis blocks_subset insert_DiffM insert_subset_eq_iff)


[STATEMENT]
lemma sub_set_sysI[intro]: "\<U> \<subseteq> \<V> \<Longrightarrow> \<A> \<subseteq># \<B> \<Longrightarrow> sub_set_system \<U> \<A> \<V> \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<U> \<subseteq> \<V>; \<A> \<subseteq># \<B>\<rbrakk> \<Longrightarrow> sub_set_system \<U> \<A> \<V> \<B>
[PROOF STEP]
by (simp add: sub_ssI incidence_system_axioms)


[STATEMENT]
lemma sub_inc_sysI[intro]: "incidence_system \<U> \<A> \<Longrightarrow> \<U> \<subseteq> \<V> \<Longrightarrow> \<A> \<subseteq># \<B> \<Longrightarrow>
    sub_incidence_system \<U> \<A> \<V> \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>incidence_system \<U> \<A>; \<U> \<subseteq> \<V>; \<A> \<subseteq># \<B>\<rbrakk> \<Longrightarrow> sub_incidence_system \<U> \<A> \<V> \<B>
[PROOF STEP]
by (simp add: sub_incidence_system.intro sub_set_sysI)


[STATEMENT]
lemma multiple_orig_sub_system:
  assumes "n > 0"
  shows "sub_incidence_system \<V> \<B> \<V> (multiple_blocks n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_incidence_system \<V> \<B> \<V> (multiple_blocks n)
[PROOF STEP]
using multiple_block_in_original wellformed multiple_blocks_sub assms
[PROOF STATE]
proof (prove)
using this:
?b \<in># multiple_blocks ?n \<Longrightarrow> ?b \<in># \<B>
?b \<in># \<B> \<Longrightarrow> ?b \<subseteq> \<V>
0 < ?n \<Longrightarrow> \<B> \<subseteq># multiple_blocks ?n
0 < n

goal (1 subgoal):
 1. sub_incidence_system \<V> \<B> \<V> (multiple_blocks n)
[PROOF STEP]
by (unfold_locales) simp_all


[STATEMENT]
lemma add_point_sub_sys: "sub_incidence_system \<V> \<B> (add_point p) \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_incidence_system \<V> \<B> (add_point p) \<B>
[PROOF STEP]
using add_point_wf add_point_def
[PROOF STATE]
proof (prove)
using this:
incidence_system (add_point ?p) \<B>
add_point ?p \<equiv> insert ?p \<V>

goal (1 subgoal):
 1. sub_incidence_system \<V> \<B> (add_point p) \<B>
[PROOF STEP]
by (simp add: sub_ssI subset_insertI incidence_system_axioms sub_incidence_system.intro)


[STATEMENT]
lemma strong_del_point_sub_sys: "sub_incidence_system (del_point p) (str_del_point_blocks p) \<V> \<B> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_incidence_system (del_point p) (str_del_point_blocks p) \<V> \<B>
[PROOF STEP]
using strong_del_point_incidence_wf wf_invalid_point del_point_def str_del_point_blocks_def
[PROOF STATE]
proof (prove)
using this:
incidence_system (del_point ?p) (str_del_point_blocks ?p)
\<lbrakk>?x \<notin> \<V>; ?b \<in># \<B>\<rbrakk> \<Longrightarrow> ?x \<notin> ?b
del_point ?p \<equiv> \<V> - {?p}
str_del_point_blocks ?p \<equiv> filter_mset ((\<notin>) ?p) \<B>

goal (1 subgoal):
 1. sub_incidence_system (del_point p) (str_del_point_blocks p) \<V> \<B>
[PROOF STEP]
by (unfold_locales) (auto)


[STATEMENT]
lemma add_block_sub_sys: "sub_incidence_system \<V> \<B> (\<V> \<union> b) (add_block b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_incidence_system \<V> \<B> (\<V> \<union> b) (add_block b)
[PROOF STEP]
using add_block_wf wf_invalid_point add_block_def
[PROOF STATE]
proof (prove)
using this:
incidence_system (\<V> \<union> ?b) (add_block ?b)
\<lbrakk>?x \<notin> \<V>; ?b \<in># \<B>\<rbrakk> \<Longrightarrow> ?x \<notin> ?b
add_block ?b \<equiv> \<B> + {#?b#}

goal (1 subgoal):
 1. sub_incidence_system \<V> \<B> (\<V> \<union> b) (add_block b)
[PROOF STEP]
by (unfold_locales) (auto)


[STATEMENT]
lemma delete_block_sub_sys: "sub_incidence_system \<V> (del_block b)  \<V> \<B> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_incidence_system \<V> (del_block b) \<V> \<B>
[PROOF STEP]
using delete_block_wf delete_block_subset incidence_system_def
[PROOF STATE]
proof (prove)
using this:
incidence_system \<V> (del_block ?b)
del_block ?b \<subseteq># \<B>
incidence_system ?point_set ?block_collection \<equiv> \<forall>b. b \<in># ?block_collection \<longrightarrow> b \<subseteq> ?point_set

goal (1 subgoal):
 1. sub_incidence_system \<V> (del_block b) \<V> \<B>
[PROOF STEP]
by (unfold_locales, auto)


[STATEMENT]
lemma (in two_set_systems) combine_sub_sys: "sub_incidence_system \<V> \<B> \<V>\<^sup>+ \<B>\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_incidence_system \<V> \<B> \<V>\<^sup>+ \<B>\<^sup>+
[PROOF STEP]
by (unfold_locales) (simp_all)


[STATEMENT]
lemma (in two_set_systems) combine_sub_sys_alt: "sub_incidence_system \<V>' \<B>' \<V>\<^sup>+ \<B>\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_incidence_system \<V>' \<B>' \<V>\<^sup>+ \<B>\<^sup>+
[PROOF STEP]
by (unfold_locales) (simp_all)


[STATEMENT]
lemma sub_designI [intro]: "design \<U> \<A> \<Longrightarrow> sub_incidence_system \<U> \<A> \<V> \<B> \<Longrightarrow> sub_design \<U> \<A> \<V> \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>design \<U> \<A>; sub_incidence_system \<U> \<A> \<V> \<B>\<rbrakk> \<Longrightarrow> sub_design \<U> \<A> \<V> \<B>
[PROOF STEP]
by (simp add: sub_design.intro wf_design)


[STATEMENT]
lemma sub_designII [intro]: "design \<U> \<A> \<Longrightarrow> sub_incidence_system \<V> \<B> \<U> \<A> \<Longrightarrow> sub_design \<V> \<B> \<U> \<A>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>design \<U> \<A>; sub_incidence_system \<V> \<B> \<U> \<A>\<rbrakk> \<Longrightarrow> sub_design \<V> \<B> \<U> \<A>
[PROOF STEP]
by (simp add: sub_design_def)


[STATEMENT]
lemma multiple_orig_sub_des:
  assumes "n > 0"
  shows "sub_design \<V> \<B> \<V> (multiple_blocks n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_design \<V> \<B> \<V> (multiple_blocks n)
[PROOF STEP]
using multiple_is_design assms multiple_orig_sub_system
[PROOF STATE]
proof (prove)
using this:
design \<V> (multiple_blocks ?n)
0 < n
0 < ?n \<Longrightarrow> sub_incidence_system \<V> \<B> \<V> (multiple_blocks ?n)

goal (1 subgoal):
 1. sub_design \<V> \<B> \<V> (multiple_blocks n)
[PROOF STEP]
by (simp add: sub_design.intro)


[STATEMENT]
lemma add_point_sub_des: "sub_design \<V> \<B> (add_point p) \<B>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_design \<V> \<B> (add_point p) \<B>
[PROOF STEP]
using add_point_design add_point_sub_sys sub_design.intro
[PROOF STATE]
proof (prove)
using this:
design (add_point ?p) \<B>
sub_incidence_system \<V> \<B> (add_point ?p) \<B>
\<lbrakk>sub_incidence_system ?\<U> ?\<A> ?\<V> ?\<B>; design ?\<V> ?\<B>\<rbrakk> \<Longrightarrow> sub_design ?\<U> ?\<A> ?\<V> ?\<B>

goal (1 subgoal):
 1. sub_design \<V> \<B> (add_point p) \<B>
[PROOF STEP]
by fastforce


[STATEMENT]
lemma strong_del_point_sub_des: "sub_design (del_point p) (str_del_point_blocks p) \<V> \<B> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_design (del_point p) (str_del_point_blocks p) \<V> \<B>
[PROOF STEP]
using strong_del_point_sub_sys sub_design.intro wf_design
[PROOF STATE]
proof (prove)
using this:
sub_incidence_system (del_point ?p) (str_del_point_blocks ?p) \<V> \<B>
\<lbrakk>sub_incidence_system ?\<U> ?\<A> ?\<V> ?\<B>; design ?\<V> ?\<B>\<rbrakk> \<Longrightarrow> sub_design ?\<U> ?\<A> ?\<V> ?\<B>
design \<V> \<B>

goal (1 subgoal):
 1. sub_design (del_point p) (str_del_point_blocks p) \<V> \<B>
[PROOF STEP]
by blast


[STATEMENT]
lemma add_block_sub_des: "finite b \<Longrightarrow> b \<noteq> {} \<Longrightarrow> sub_design \<V> \<B> (\<V> \<union> b) (add_block b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite b; b \<noteq> {}\<rbrakk> \<Longrightarrow> sub_design \<V> \<B> (\<V> \<union> b) (add_block b)
[PROOF STEP]
using add_block_sub_sys add_block_design sub_designII
[PROOF STATE]
proof (prove)
using this:
sub_incidence_system \<V> \<B> (\<V> \<union> ?b) (add_block ?b)
\<lbrakk>finite ?bl; ?bl \<noteq> {}\<rbrakk> \<Longrightarrow> design (\<V> \<union> ?bl) (add_block ?bl)
\<lbrakk>design ?\<U> ?\<A>; sub_incidence_system \<V> \<B> ?\<U> ?\<A>\<rbrakk> \<Longrightarrow> sub_design \<V> \<B> ?\<U> ?\<A>

goal (1 subgoal):
 1. \<lbrakk>finite b; b \<noteq> {}\<rbrakk> \<Longrightarrow> sub_design \<V> \<B> (\<V> \<union> b) (add_block b)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma delete_block_sub_des: "sub_design \<V> (del_block b) \<V> \<B> "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_design \<V> (del_block b) \<V> \<B>
[PROOF STEP]
using delete_block_design delete_block_sub_sys sub_designI
[PROOF STATE]
proof (prove)
using this:
design \<V> (del_block ?bl)
sub_incidence_system \<V> (del_block ?b) \<V> \<B>
\<lbrakk>design ?\<U> ?\<A>; sub_incidence_system ?\<U> ?\<A> \<V> \<B>\<rbrakk> \<Longrightarrow> sub_design ?\<U> ?\<A> \<V> \<B>

goal (1 subgoal):
 1. sub_design \<V> (del_block b) \<V> \<B>
[PROOF STEP]
by auto


[STATEMENT]
lemma (in two_designs) combine_sub_des: "sub_design \<V> \<B> \<V>\<^sup>+ \<B>\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_design \<V> \<B> \<V>\<^sup>+ \<B>\<^sup>+
[PROOF STEP]
by (unfold_locales) (simp_all)


[STATEMENT]
lemma (in two_designs) combine_sub_des_alt: "sub_design \<V>' \<B>' \<V>\<^sup>+ \<B>\<^sup>+"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sub_design \<V>' \<B>' \<V>\<^sup>+ \<B>\<^sup>+
[PROOF STEP]
by (unfold_locales) (simp_all)


[STATEMENT]
lemma rt_fun:
  "R\<^sup>*\<^sup>* t t' \<Longrightarrow> R\<^sup>*\<^sup>* (app t u) (app t' u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R\<^sup>*\<^sup>* t t' \<Longrightarrow> R\<^sup>*\<^sup>* (app t u) (app t' u)
[PROOF STEP]
by (induct rule: rtranclp.induct) (auto intro: rtranclp.rtrancl_into_rtrancl R_fun)


[STATEMENT]
lemma rt_arg:
  "R\<^sup>*\<^sup>* u u' \<Longrightarrow> R\<^sup>*\<^sup>* (app t u) (app t u')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R\<^sup>*\<^sup>* u u' \<Longrightarrow> R\<^sup>*\<^sup>* (app t u) (app t u')
[PROOF STEP]
by (induct rule: rtranclp.induct) (auto intro: rtranclp.rtrancl_into_rtrancl R_arg)


[STATEMENT]
lemma rt_comb:
  "R\<^sup>*\<^sup>* t\<^sub>1 u\<^sub>1 \<Longrightarrow> R\<^sup>*\<^sup>* t\<^sub>2 u\<^sub>2 \<Longrightarrow> R\<^sup>*\<^sup>* (app t\<^sub>1 t\<^sub>2) (app u\<^sub>1 u\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>R\<^sup>*\<^sup>* t\<^sub>1 u\<^sub>1; R\<^sup>*\<^sup>* t\<^sub>2 u\<^sub>2\<rbrakk> \<Longrightarrow> R\<^sup>*\<^sup>* (app t\<^sub>1 t\<^sub>2) (app u\<^sub>1 u\<^sub>2)
[PROOF STEP]
by (metis rt_fun rt_arg rtranclp_trans)


[STATEMENT]
lemma rt_list_comb:
  assumes "list_all2 R\<^sup>*\<^sup>* ts us" "R\<^sup>*\<^sup>* t u"
  shows "R\<^sup>*\<^sup>* (list_comb t ts) (list_comb u us)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R\<^sup>*\<^sup>* (list_comb t ts) (list_comb u us)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
list_all2 R\<^sup>*\<^sup>* ts us
R\<^sup>*\<^sup>* t u

goal (1 subgoal):
 1. R\<^sup>*\<^sup>* (list_comb t ts) (list_comb u us)
[PROOF STEP]
by (induction ts us arbitrary: t u rule: list.rel_induct) (auto intro: rt_comb)


[STATEMENT]
lemma (in group) order_one_triv_iff:
  shows "(order G = 1) = (carrier G = {\<one>})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (order G = 1) = (carrier G = {\<one>})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. order G = 1 \<Longrightarrow> carrier G = {\<one>}
 2. carrier G = {\<one>} \<Longrightarrow> order G = 1
[PROOF STEP]
assume order:"order G = 1"
[PROOF STATE]
proof (state)
this:
order G = 1

goal (2 subgoals):
 1. order G = 1 \<Longrightarrow> carrier G = {\<one>}
 2. carrier G = {\<one>} \<Longrightarrow> order G = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
order G = 1
[PROOF STEP]
obtain x where x:"carrier G = {x}"
[PROOF STATE]
proof (prove)
using this:
order G = 1

goal (1 subgoal):
 1. (\<And>x. carrier G = {x} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
using this:
card (carrier G) = 1

goal (1 subgoal):
 1. (\<And>x. carrier G = {x} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp add: card_Suc_eq)
[PROOF STATE]
proof (state)
this:
carrier G = {x}

goal (2 subgoals):
 1. order G = 1 \<Longrightarrow> carrier G = {\<one>}
 2. carrier G = {\<one>} \<Longrightarrow> order G = 1
[PROOF STEP]
hence "\<one> = x"
[PROOF STATE]
proof (prove)
using this:
carrier G = {x}

goal (1 subgoal):
 1. \<one> = x
[PROOF STEP]
using one_closed
[PROOF STATE]
proof (prove)
using this:
carrier G = {x}
\<one> \<in> carrier G

goal (1 subgoal):
 1. \<one> = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<one> = x

goal (2 subgoals):
 1. order G = 1 \<Longrightarrow> carrier G = {\<one>}
 2. carrier G = {\<one>} \<Longrightarrow> order G = 1
[PROOF STEP]
with x
[PROOF STATE]
proof (chain)
picking this:
carrier G = {x}
\<one> = x
[PROOF STEP]
show "carrier G = {\<one>}"
[PROOF STATE]
proof (prove)
using this:
carrier G = {x}
\<one> = x

goal (1 subgoal):
 1. carrier G = {\<one>}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
carrier G = {\<one>}

goal (1 subgoal):
 1. carrier G = {\<one>} \<Longrightarrow> order G = 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. carrier G = {\<one>} \<Longrightarrow> order G = 1
[PROOF STEP]
assume "carrier G = {\<one>}"
[PROOF STATE]
proof (state)
this:
carrier G = {\<one>}

goal (1 subgoal):
 1. carrier G = {\<one>} \<Longrightarrow> order G = 1
[PROOF STEP]
thus "order G = 1"
[PROOF STATE]
proof (prove)
using this:
carrier G = {\<one>}

goal (1 subgoal):
 1. order G = 1
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
using this:
carrier G = {\<one>}

goal (1 subgoal):
 1. card (carrier G) = 1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
order G = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) finite_pos_order:
  assumes finite:"finite (carrier G)"
  shows "0 < order G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < order G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < order G
[PROOF STEP]
from one_closed finite
[PROOF STATE]
proof (chain)
picking this:
\<one> \<in> carrier G
finite (carrier G)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<one> \<in> carrier G
finite (carrier G)

goal (1 subgoal):
 1. 0 < order G
[PROOF STEP]
unfolding order_def
[PROOF STATE]
proof (prove)
using this:
\<one> \<in> carrier G
finite (carrier G)

goal (1 subgoal):
 1. 0 < card (carrier G)
[PROOF STEP]
by (metis card_gt_0_iff subgroup_nonempty subgroup_self)
[PROOF STATE]
proof (state)
this:
0 < order G

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iso_order_closed:
  assumes "\<phi> \<in> iso G H"
  shows "order G = order H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. order G = order H
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> Group.iso G H

goal (1 subgoal):
 1. order G = order H
[PROOF STEP]
unfolding order_def iso_def
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> {h \<in> hom G H. bij_betw h (carrier G) (carrier H)}

goal (1 subgoal):
 1. card (carrier G) = card (carrier H)
[PROOF STEP]
by (metis (no_types) bij_betw_same_card mem_Collect_eq)


[STATEMENT]
lemma (in subgroup) subgroup_of_restricted_group:
  assumes "subgroup U (G\<lparr> carrier := H\<rparr>)"
  shows "U \<subseteq> H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U \<subseteq> H
[PROOF STEP]
using assms subgroup.subset
[PROOF STATE]
proof (prove)
using this:
subgroup U (G\<lparr>carrier := H\<rparr>)
subgroup ?H ?G \<Longrightarrow> ?H \<subseteq> carrier ?G

goal (1 subgoal):
 1. U \<subseteq> H
[PROOF STEP]
by force


[STATEMENT]
lemma (in subgroup) subgroup_of_subgroup:
  assumes "group G"
  assumes "subgroup U (G\<lparr> carrier := H\<rparr>)"
  shows "subgroup U G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup U G
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. U \<subseteq> carrier G
 2. \<And>x y. \<lbrakk>x \<in> U; y \<in> U\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> U
 3. \<one> \<in> U
 4. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
subgroup U (G\<lparr>carrier := H\<rparr>)
[PROOF STEP]
have "U \<subseteq> H"
[PROOF STATE]
proof (prove)
using this:
subgroup U (G\<lparr>carrier := H\<rparr>)

goal (1 subgoal):
 1. U \<subseteq> H
[PROOF STEP]
by (rule subgroup_of_restricted_group)
[PROOF STATE]
proof (state)
this:
U \<subseteq> H

goal (4 subgoals):
 1. U \<subseteq> carrier G
 2. \<And>x y. \<lbrakk>x \<in> U; y \<in> U\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> U
 3. \<one> \<in> U
 4. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
thus "U \<subseteq> carrier G"
[PROOF STATE]
proof (prove)
using this:
U \<subseteq> H

goal (1 subgoal):
 1. U \<subseteq> carrier G
[PROOF STEP]
by (auto simp:subset)
[PROOF STATE]
proof (state)
this:
U \<subseteq> carrier G

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> U; y \<in> U\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> U
 2. \<one> \<in> U
 3. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> U; y \<in> U\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> U
 2. \<one> \<in> U
 3. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> U; y \<in> U\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> U
 2. \<one> \<in> U
 3. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
have a:"x \<otimes> y = x \<otimes>\<^bsub>G\<lparr> carrier := H\<rparr>\<^esub> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<otimes> y = x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<otimes> y = x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> U; y \<in> U\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> U
 2. \<one> \<in> U
 3. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
assume "x \<in> U" "y \<in> U"
[PROOF STATE]
proof (state)
this:
x \<in> U
y \<in> U

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> U; y \<in> U\<rbrakk> \<Longrightarrow> x \<otimes> y \<in> U
 2. \<one> \<in> U
 3. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
with assms a
[PROOF STATE]
proof (chain)
picking this:
Group.group G
subgroup U (G\<lparr>carrier := H\<rparr>)
x \<otimes> y = x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y
x \<in> U
y \<in> U
[PROOF STEP]
show " x \<otimes> y \<in> U"
[PROOF STATE]
proof (prove)
using this:
Group.group G
subgroup U (G\<lparr>carrier := H\<rparr>)
x \<otimes> y = x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y
x \<in> U
y \<in> U

goal (1 subgoal):
 1. x \<otimes> y \<in> U
[PROOF STEP]
by (metis subgroup.m_closed)
[PROOF STATE]
proof (state)
this:
x \<otimes> y \<in> U

goal (2 subgoals):
 1. \<one> \<in> U
 2. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<one> \<in> U
 2. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
have "\<one>\<^bsub>G\<lparr> carrier := H\<rparr>\<^esub> = \<one>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<one>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> = \<one>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> = \<one>

goal (2 subgoals):
 1. \<one> \<in> U
 2. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
Group.group G
subgroup U (G\<lparr>carrier := H\<rparr>)
\<one>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> = \<one>
[PROOF STEP]
show "\<one> \<in> U"
[PROOF STATE]
proof (prove)
using this:
Group.group G
subgroup U (G\<lparr>carrier := H\<rparr>)
\<one>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> = \<one>

goal (1 subgoal):
 1. \<one> \<in> U
[PROOF STEP]
by (metis subgroup.one_closed)
[PROOF STATE]
proof (state)
this:
\<one> \<in> U

goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
have "subgroup H G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup H G
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
subgroup H G

goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
assume "x \<in> U"
[PROOF STATE]
proof (state)
this:
x \<in> U

goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
subgroup U (G\<lparr>carrier := H\<rparr>)
x \<in> U
[PROOF STEP]
have "inv\<^bsub>G\<lparr> carrier := H\<rparr>\<^esub> x \<in> U"
[PROOF STATE]
proof (prove)
using this:
subgroup U (G\<lparr>carrier := H\<rparr>)
x \<in> U

goal (1 subgoal):
 1. inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> U
[PROOF STEP]
by (rule subgroup.m_inv_closed)
[PROOF STATE]
proof (state)
this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> U

goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> U

goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
from assms \<open>x \<in> U\<close>
[PROOF STATE]
proof (chain)
picking this:
Group.group G
subgroup U (G\<lparr>carrier := H\<rparr>)
x \<in> U
[PROOF STEP]
have "x \<in> H"
[PROOF STATE]
proof (prove)
using this:
Group.group G
subgroup U (G\<lparr>carrier := H\<rparr>)
x \<in> U

goal (1 subgoal):
 1. x \<in> H
[PROOF STEP]
by (metis in_mono subgroup_of_restricted_group)
[PROOF STATE]
proof (state)
this:
x \<in> H

goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
with assms(1) \<open>subgroup H G\<close>
[PROOF STATE]
proof (chain)
picking this:
Group.group G
subgroup H G
x \<in> H
[PROOF STEP]
have "inv\<^bsub>G\<lparr> carrier := H\<rparr>\<^esub> x = inv x"
[PROOF STATE]
proof (prove)
using this:
Group.group G
subgroup H G
x \<in> H

goal (1 subgoal):
 1. inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x = inv x
[PROOF STEP]
by (rule group.m_inv_consistent)
[PROOF STATE]
proof (state)
this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x = inv x

goal (1 subgoal):
 1. \<And>x. x \<in> U \<Longrightarrow> inv x \<in> U
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> U
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x = inv x
[PROOF STEP]
show "inv x \<in> U"
[PROOF STATE]
proof (prove)
using this:
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x \<in> U
inv\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> x = inv x

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in subgroup) surj_hom_subgroup:
  assumes \<phi>:"group_hom G F \<phi>"
  assumes \<phi>surj:"\<phi> ` (carrier G) = carrier F"
  shows "subgroup (\<phi> ` H) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup (\<phi> ` H) F
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<phi> ` H \<subseteq> carrier F
 2. \<And>x y. \<lbrakk>x \<in> \<phi> ` H; y \<in> \<phi> ` H\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>F\<^esub> y \<in> \<phi> ` H
 3. \<one>\<^bsub>F\<^esub> \<in> \<phi> ` H
 4. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
from \<phi>surj
[PROOF STATE]
proof (chain)
picking this:
\<phi> ` carrier G = carrier F
[PROOF STEP]
show img_subset:"\<phi> ` H \<subseteq> carrier F"
[PROOF STATE]
proof (prove)
using this:
\<phi> ` carrier G = carrier F

goal (1 subgoal):
 1. \<phi> ` H \<subseteq> carrier F
[PROOF STEP]
unfolding iso_def bij_betw_def
[PROOF STATE]
proof (prove)
using this:
\<phi> ` carrier G = carrier F

goal (1 subgoal):
 1. \<phi> ` H \<subseteq> carrier F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> ` H \<subseteq> carrier F

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<phi> ` H; y \<in> \<phi> ` H\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>F\<^esub> y \<in> \<phi> ` H
 2. \<one>\<^bsub>F\<^esub> \<in> \<phi> ` H
 3. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<phi> ` H; y \<in> \<phi> ` H\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>F\<^esub> y \<in> \<phi> ` H
 2. \<one>\<^bsub>F\<^esub> \<in> \<phi> ` H
 3. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
fix f f'
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<phi> ` H; y \<in> \<phi> ` H\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>F\<^esub> y \<in> \<phi> ` H
 2. \<one>\<^bsub>F\<^esub> \<in> \<phi> ` H
 3. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
assume h:"f \<in> \<phi> ` H" and h':"f' \<in> \<phi> ` H"
[PROOF STATE]
proof (state)
this:
f \<in> \<phi> ` H
f' \<in> \<phi> ` H

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<phi> ` H; y \<in> \<phi> ` H\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>F\<^esub> y \<in> \<phi> ` H
 2. \<one>\<^bsub>F\<^esub> \<in> \<phi> ` H
 3. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
with \<phi>surj
[PROOF STATE]
proof (chain)
picking this:
\<phi> ` carrier G = carrier F
f \<in> \<phi> ` H
f' \<in> \<phi> ` H
[PROOF STEP]
obtain g g' where g:"g \<in> H" "f = \<phi> g" and g':"g' \<in> H" "f' = \<phi> g'"
[PROOF STATE]
proof (prove)
using this:
\<phi> ` carrier G = carrier F
f \<in> \<phi> ` H
f' \<in> \<phi> ` H

goal (1 subgoal):
 1. (\<And>g g'. \<lbrakk>g \<in> H; f = \<phi> g; g' \<in> H; f' = \<phi> g'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> H
f = \<phi> g
g' \<in> H
f' = \<phi> g'

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<phi> ` H; y \<in> \<phi> ` H\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>F\<^esub> y \<in> \<phi> ` H
 2. \<one>\<^bsub>F\<^esub> \<in> \<phi> ` H
 3. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
hence "g \<otimes>\<^bsub>G\<^esub> g' \<in> H"
[PROOF STATE]
proof (prove)
using this:
g \<in> H
f = \<phi> g
g' \<in> H
f' = \<phi> g'

goal (1 subgoal):
 1. g \<otimes> g' \<in> H
[PROOF STEP]
by (metis m_closed)
[PROOF STATE]
proof (state)
this:
g \<otimes> g' \<in> H

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<phi> ` H; y \<in> \<phi> ` H\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>F\<^esub> y \<in> \<phi> ` H
 2. \<one>\<^bsub>F\<^esub> \<in> \<phi> ` H
 3. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
hence "\<phi> (g \<otimes>\<^bsub>G\<^esub> g') \<in> \<phi> ` H"
[PROOF STATE]
proof (prove)
using this:
g \<otimes> g' \<in> H

goal (1 subgoal):
 1. \<phi> (g \<otimes> g') \<in> \<phi> ` H
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> (g \<otimes> g') \<in> \<phi> ` H

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> \<phi> ` H; y \<in> \<phi> ` H\<rbrakk> \<Longrightarrow> x \<otimes>\<^bsub>F\<^esub> y \<in> \<phi> ` H
 2. \<one>\<^bsub>F\<^esub> \<in> \<phi> ` H
 3. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
with g g' \<phi>
[PROOF STATE]
proof (chain)
picking this:
g \<in> H
f = \<phi> g
g' \<in> H
f' = \<phi> g'
group_hom G F \<phi>
\<phi> (g \<otimes> g') \<in> \<phi> ` H
[PROOF STEP]
show "f \<otimes>\<^bsub>F\<^esub> f' \<in> \<phi> ` H"
[PROOF STATE]
proof (prove)
using this:
g \<in> H
f = \<phi> g
g' \<in> H
f' = \<phi> g'
group_hom G F \<phi>
\<phi> (g \<otimes> g') \<in> \<phi> ` H

goal (1 subgoal):
 1. f \<otimes>\<^bsub>F\<^esub> f' \<in> \<phi> ` H
[PROOF STEP]
using group_hom.hom_mult
[PROOF STATE]
proof (prove)
using this:
g \<in> H
f = \<phi> g
g' \<in> H
f' = \<phi> g'
group_hom G F \<phi>
\<phi> (g \<otimes> g') \<in> \<phi> ` H
\<lbrakk>group_hom ?G ?H ?h; ?x \<in> carrier ?G; ?y \<in> carrier ?G\<rbrakk> \<Longrightarrow> ?h (?x \<otimes>\<^bsub>?G\<^esub> ?y) = ?h ?x \<otimes>\<^bsub>?H\<^esub> ?h ?y

goal (1 subgoal):
 1. f \<otimes>\<^bsub>F\<^esub> f' \<in> \<phi> ` H
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
f \<otimes>\<^bsub>F\<^esub> f' \<in> \<phi> ` H

goal (2 subgoals):
 1. \<one>\<^bsub>F\<^esub> \<in> \<phi> ` H
 2. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<one>\<^bsub>F\<^esub> \<in> \<phi> ` H
 2. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
have "\<phi> \<one> \<in> \<phi> ` H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> \<one> \<in> \<phi> ` H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> \<one> \<in> \<phi> ` H

goal (2 subgoals):
 1. \<one>\<^bsub>F\<^esub> \<in> \<phi> ` H
 2. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
with \<phi>
[PROOF STATE]
proof (chain)
picking this:
group_hom G F \<phi>
\<phi> \<one> \<in> \<phi> ` H
[PROOF STEP]
show  "\<one>\<^bsub>F\<^esub> \<in> \<phi> ` H"
[PROOF STATE]
proof (prove)
using this:
group_hom G F \<phi>
\<phi> \<one> \<in> \<phi> ` H

goal (1 subgoal):
 1. \<one>\<^bsub>F\<^esub> \<in> \<phi> ` H
[PROOF STEP]
by (metis group_hom.hom_one)
[PROOF STATE]
proof (state)
this:
\<one>\<^bsub>F\<^esub> \<in> \<phi> ` H

goal (1 subgoal):
 1. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
assume f:"f \<in> \<phi> ` H"
[PROOF STATE]
proof (state)
this:
f \<in> \<phi> ` H

goal (1 subgoal):
 1. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in> \<phi> ` H
[PROOF STEP]
obtain g where g:"g \<in> H" "f = \<phi> g"
[PROOF STATE]
proof (prove)
using this:
f \<in> \<phi> ` H

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> H; f = \<phi> g\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<in> H
f = \<phi> g

goal (1 subgoal):
 1. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
hence "inv g \<in> H"
[PROOF STATE]
proof (prove)
using this:
g \<in> H
f = \<phi> g

goal (1 subgoal):
 1. inv g \<in> H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv g \<in> H

goal (1 subgoal):
 1. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
hence "\<phi> (inv g) \<in> \<phi> ` H"
[PROOF STATE]
proof (prove)
using this:
inv g \<in> H

goal (1 subgoal):
 1. \<phi> (inv g) \<in> \<phi> ` H
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> (inv g) \<in> \<phi> ` H

goal (1 subgoal):
 1. \<And>x. x \<in> \<phi> ` H \<Longrightarrow> inv\<^bsub>F\<^esub> x \<in> \<phi> ` H
[PROOF STEP]
with \<phi> g subset
[PROOF STATE]
proof (chain)
picking this:
group_hom G F \<phi>
g \<in> H
f = \<phi> g
H \<subseteq> carrier G
\<phi> (inv g) \<in> \<phi> ` H
[PROOF STEP]
show "inv\<^bsub>F\<^esub> f \<in> \<phi> ` H"
[PROOF STATE]
proof (prove)
using this:
group_hom G F \<phi>
g \<in> H
f = \<phi> g
H \<subseteq> carrier G
\<phi> (inv g) \<in> \<phi> ` H

goal (1 subgoal):
 1. inv\<^bsub>F\<^esub> f \<in> \<phi> ` H
[PROOF STEP]
using group_hom.hom_inv
[PROOF STATE]
proof (prove)
using this:
group_hom G F \<phi>
g \<in> H
f = \<phi> g
H \<subseteq> carrier G
\<phi> (inv g) \<in> \<phi> ` H
\<lbrakk>group_hom ?G ?H ?h; ?x \<in> carrier ?G\<rbrakk> \<Longrightarrow> ?h (inv\<^bsub>?G\<^esub> ?x) = inv\<^bsub>?H\<^esub> ?h ?x

goal (1 subgoal):
 1. inv\<^bsub>F\<^esub> f \<in> \<phi> ` H
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
inv\<^bsub>F\<^esub> f \<in> \<phi> ` H

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iso_subgroup:
  assumes groups:"group G" "group F"
  assumes HG:"subgroup H G"
  assumes \<phi>:"\<phi> \<in> iso G F"
  shows "subgroup (\<phi> ` H) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup (\<phi> ` H) F
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. subgroup (\<phi> ` H) F
[PROOF STEP]
from groups \<phi>
[PROOF STATE]
proof (chain)
picking this:
Group.group G
Group.group F
\<phi> \<in> Group.iso G F
[PROOF STEP]
have "group_hom G F \<phi>"
[PROOF STATE]
proof (prove)
using this:
Group.group G
Group.group F
\<phi> \<in> Group.iso G F

goal (1 subgoal):
 1. group_hom G F \<phi>
[PROOF STEP]
unfolding group_hom_def group_hom_axioms_def iso_def
[PROOF STATE]
proof (prove)
using this:
Group.group G
Group.group F
\<phi> \<in> {h \<in> hom G F. bij_betw h (carrier G) (carrier F)}

goal (1 subgoal):
 1. Group.group G \<and> Group.group F \<and> \<phi> \<in> hom G F
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
group_hom G F \<phi>

goal (1 subgoal):
 1. subgroup (\<phi> ` H) F
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
group_hom G F \<phi>

goal (1 subgoal):
 1. subgroup (\<phi> ` H) F
[PROOF STEP]
from \<phi>
[PROOF STATE]
proof (chain)
picking this:
\<phi> \<in> Group.iso G F
[PROOF STEP]
have "\<phi> ` (carrier G) = carrier F"
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> Group.iso G F

goal (1 subgoal):
 1. \<phi> ` carrier G = carrier F
[PROOF STEP]
unfolding iso_def bij_betw_def
[PROOF STATE]
proof (prove)
using this:
\<phi> \<in> {h \<in> hom G F. inj_on h (carrier G) \<and> h ` carrier G = carrier F}

goal (1 subgoal):
 1. \<phi> ` carrier G = carrier F
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<phi> ` carrier G = carrier F

goal (1 subgoal):
 1. subgroup (\<phi> ` H) F
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<phi> ` carrier G = carrier F

goal (1 subgoal):
 1. subgroup (\<phi> ` H) F
[PROOF STEP]
note HG
[PROOF STATE]
proof (state)
this:
subgroup H G

goal (1 subgoal):
 1. subgroup (\<phi> ` H) F
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
group_hom G F \<phi>
\<phi> ` carrier G = carrier F
subgroup H G
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
group_hom G F \<phi>
\<phi> ` carrier G = carrier F
subgroup H G

goal (1 subgoal):
 1. subgroup (\<phi> ` H) F
[PROOF STEP]
by (metis subgroup.surj_hom_subgroup)
[PROOF STATE]
proof (state)
this:
subgroup (\<phi> ` H) F

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iso_restrict:
  assumes groups:"group G" "group F"
  assumes HG:"subgroup H G"
  assumes \<phi>:"\<phi> \<in> iso G F"
  shows "(restrict \<phi> H) \<in> iso (G\<lparr>carrier := H\<rparr>) (F\<lparr>carrier := \<phi> ` H\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict \<phi> H \<in> Group.iso (G\<lparr>carrier := H\<rparr>) (F\<lparr>carrier := \<phi> ` H\<rparr>)
[PROOF STEP]
unfolding iso_def hom_def bij_betw_def inj_on_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. restrict \<phi> H \<in> {h \<in> {h \<in> carrier (G\<lparr>carrier := H\<rparr>) \<rightarrow> carrier (F\<lparr>carrier := \<phi> ` H\<rparr>). \<forall>x\<in>carrier (G\<lparr>carrier := H\<rparr>). \<forall>y\<in>carrier (G\<lparr>carrier := H\<rparr>). h (x \<otimes>\<^bsub>G\<lparr>carrier := H\<rparr>\<^esub> y) = h x \<otimes>\<^bsub>F\<lparr>carrier := \<phi> ` H\<rparr>\<^esub> h y}. (\<forall>x\<in>carrier (G\<lparr>carrier := H\<rparr>). \<forall>y\<in>carrier (G\<lparr>carrier := H\<rparr>). h x = h y \<longrightarrow> x = y) \<and> h ` carrier (G\<lparr>carrier := H\<rparr>) = carrier (F\<lparr>carrier := \<phi> ` H\<rparr>)}
[PROOF STEP]
proof auto
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<in> H\<rbrakk> \<Longrightarrow> \<phi> (x \<otimes>\<^bsub>G\<^esub> y) = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y
 2. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<notin> H\<rbrakk> \<Longrightarrow> undefined = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y
 3. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix g h
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<in> H\<rbrakk> \<Longrightarrow> \<phi> (x \<otimes>\<^bsub>G\<^esub> y) = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y
 2. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<notin> H\<rbrakk> \<Longrightarrow> undefined = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y
 3. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume "g \<in> H" "h \<in> H"
[PROOF STATE]
proof (state)
this:
g \<in> H
h \<in> H

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<in> H\<rbrakk> \<Longrightarrow> \<phi> (x \<otimes>\<^bsub>G\<^esub> y) = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y
 2. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<notin> H\<rbrakk> \<Longrightarrow> undefined = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y
 3. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "g \<in> carrier G" "h \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
g \<in> H
h \<in> H

goal (1 subgoal):
 1. g \<in> carrier G &&& h \<in> carrier G
[PROOF STEP]
by (metis HG subgroup.mem_carrier)+
[PROOF STATE]
proof (state)
this:
g \<in> carrier G
h \<in> carrier G

goal (3 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<in> H\<rbrakk> \<Longrightarrow> \<phi> (x \<otimes>\<^bsub>G\<^esub> y) = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y
 2. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<notin> H\<rbrakk> \<Longrightarrow> undefined = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y
 3. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
thus "\<phi> (g \<otimes>\<^bsub>G\<^esub> h) = \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> h"
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
h \<in> carrier G

goal (1 subgoal):
 1. \<phi> (g \<otimes>\<^bsub>G\<^esub> h) = \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> h
[PROOF STEP]
using \<phi>
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
h \<in> carrier G
\<phi> \<in> Group.iso G F

goal (1 subgoal):
 1. \<phi> (g \<otimes>\<^bsub>G\<^esub> h) = \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> h
[PROOF STEP]
unfolding iso_def hom_def
[PROOF STATE]
proof (prove)
using this:
g \<in> carrier G
h \<in> carrier G
\<phi> \<in> {h \<in> {h \<in> carrier G \<rightarrow> carrier F. \<forall>x\<in>carrier G. \<forall>y\<in>carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>F\<^esub> h y}. bij_betw h (carrier G) (carrier F)}

goal (1 subgoal):
 1. \<phi> (g \<otimes>\<^bsub>G\<^esub> h) = \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> h
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<phi> (g \<otimes>\<^bsub>G\<^esub> h) = \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> h

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<notin> H\<rbrakk> \<Longrightarrow> undefined = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y
 2. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<notin> H\<rbrakk> \<Longrightarrow> undefined = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y
 2. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix g h
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<notin> H\<rbrakk> \<Longrightarrow> undefined = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y
 2. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume "g \<in> H" "h \<in> H" "g \<otimes>\<^bsub>G\<^esub> h \<notin> H"
[PROOF STATE]
proof (state)
this:
g \<in> H
h \<in> H
g \<otimes>\<^bsub>G\<^esub> h \<notin> H

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<notin> H\<rbrakk> \<Longrightarrow> undefined = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y
 2. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "False"
[PROOF STATE]
proof (prove)
using this:
g \<in> H
h \<in> H
g \<otimes>\<^bsub>G\<^esub> h \<notin> H

goal (1 subgoal):
 1. False
[PROOF STEP]
using HG
[PROOF STATE]
proof (prove)
using this:
g \<in> H
h \<in> H
g \<otimes>\<^bsub>G\<^esub> h \<notin> H
subgroup H G

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding subgroup_def
[PROOF STATE]
proof (prove)
using this:
g \<in> H
h \<in> H
g \<otimes>\<^bsub>G\<^esub> h \<notin> H
(H \<subseteq> carrier G \<and> (\<forall>x y. x \<in> H \<longrightarrow> y \<in> H \<longrightarrow> x \<otimes>\<^bsub>G\<^esub> y \<in> H)) \<and> \<one>\<^bsub>G\<^esub> \<in> H \<and> (\<forall>x. x \<in> H \<longrightarrow> inv\<^bsub>G\<^esub> x \<in> H)

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

goal (2 subgoals):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; x \<otimes>\<^bsub>G\<^esub> y \<notin> H\<rbrakk> \<Longrightarrow> undefined = \<phi> x \<otimes>\<^bsub>F\<^esub> \<phi> y
 2. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
thus "undefined = \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> h"
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. undefined = \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> h
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
undefined = \<phi> g \<otimes>\<^bsub>F\<^esub> \<phi> h

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix g h
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume g:"g \<in> H" and h:"h \<in> H" and eq:"\<phi> g = \<phi> h"
[PROOF STATE]
proof (state)
this:
g \<in> H
h \<in> H
\<phi> g = \<phi> h

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
hence "g \<in> carrier G" "h \<in> carrier G"
[PROOF STATE]
proof (prove)
using this:
g \<in> H
h \<in> H
\<phi> g = \<phi> h

goal (1 subgoal):
 1. g \<in> carrier G &&& h \<in> carrier G
[PROOF STEP]
by (metis HG subgroup.mem_carrier)+
[PROOF STATE]
proof (state)
this:
g \<in> carrier G
h \<in> carrier G

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> H; y \<in> H; \<phi> x = \<phi> y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
with eq
[PROOF STATE]
proof (chain)
picking this:
\<phi> g = \<phi> h
g \<in> carrier G
h \<in> carrier G
[PROOF STEP]
show "g = h"
[PROOF STATE]
proof (prove)
using this:
\<phi> g = \<phi> h
g \<in> carrier G
h \<in> carrier G

goal (1 subgoal):
 1. g = h
[PROOF STEP]
using \<phi>
[PROOF STATE]
proof (prove)
using this:
\<phi> g = \<phi> h
g \<in> carrier G
h \<in> carrier G
\<phi> \<in> Group.iso G F

goal (1 subgoal):
 1. g = h
[PROOF STEP]
unfolding iso_def bij_betw_def inj_on_def
[PROOF STATE]
proof (prove)
using this:
\<phi> g = \<phi> h
g \<in> carrier G
h \<in> carrier G
\<phi> \<in> {h \<in> hom G F. (\<forall>x\<in>carrier G. \<forall>y\<in>carrier G. h x = h y \<longrightarrow> x = y) \<and> h ` carrier G = carrier F}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in group) subgroup_intersect:
  assumes "subgroup H G"
  assumes "subgroup H' G"
  shows "subgroup (H \<inter> H') G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. subgroup (H \<inter> H') G
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
subgroup H G
subgroup H' G

goal (1 subgoal):
 1. subgroup (H \<inter> H') G
[PROOF STEP]
unfolding subgroup_def
[PROOF STATE]
proof (prove)
using this:
(H \<subseteq> carrier G \<and> (\<forall>x y. x \<in> H \<longrightarrow> y \<in> H \<longrightarrow> x \<otimes> y \<in> H)) \<and> \<one> \<in> H \<and> (\<forall>x. x \<in> H \<longrightarrow> inv x \<in> H)
(H' \<subseteq> carrier G \<and> (\<forall>x y. x \<in> H' \<longrightarrow> y \<in> H' \<longrightarrow> x \<otimes> y \<in> H')) \<and> \<one> \<in> H' \<and> (\<forall>x. x \<in> H' \<longrightarrow> inv x \<in> H')

goal (1 subgoal):
 1. (H \<inter> H' \<subseteq> carrier G \<and> (\<forall>x y. x \<in> H \<inter> H' \<longrightarrow> y \<in> H \<inter> H' \<longrightarrow> x \<otimes> y \<in> H \<inter> H')) \<and> \<one> \<in> H \<inter> H' \<and> (\<forall>x. x \<in> H \<inter> H' \<longrightarrow> inv x \<in> H \<inter> H')
[PROOF STEP]
by auto


[STATEMENT]
lemma (in normal) is_normal:
  shows "H \<lhd> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H \<lhd> G
[PROOF STEP]
by (metis coset_eq is_subgroup normalI)