[STATEMENT]
lemma (in FiniteLinorderEnvironment) trans_MapOps:
  "MapOps (\<lambda>k. (clock_simAbs (fst k), snd k)) (Clock.jkbpSEC \<times> UNIV) trans_MapOps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MapOps (\<lambda>k. (clock_simAbs (fst k), snd k)) ((\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV) trans_MapOps
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. (clock_simAbs (fst k), snd k) \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV \<Longrightarrow> MapOps.lookup trans_MapOps (MapOps.empty trans_MapOps) k = None
 2. \<And>e k k' M. \<lbrakk>(clock_simAbs (fst k), snd k) \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV; (clock_simAbs (fst k'), snd k') \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV\<rbrakk> \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. (clock_simAbs (fst k), snd k) \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV \<Longrightarrow> MapOps.lookup trans_MapOps (MapOps.empty trans_MapOps) k = None
 2. \<And>e k k' M. \<lbrakk>(clock_simAbs (fst k), snd k) \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV; (clock_simAbs (fst k'), snd k') \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV\<rbrakk> \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
show "MapOps.lookup trans_MapOps (MapOps.empty trans_MapOps) k = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MapOps.lookup trans_MapOps (MapOps.empty trans_MapOps) k = None
[PROOF STEP]
unfolding trans_MapOps_def trans_MapOps_lookup_def trie_odlist_lookup_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MapOps.lookup \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind ((lookup_trie m \<circ> toList) (fst (fst k))) (\<lambda>m. Option.bind ((lookup_trie m \<circ> toList) (snd (fst k))) (\<lambda>m. Mapping.lookup m (snd k))), update = trans_MapOps_update\<rparr> (MapOps.empty \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind ((lookup_trie m \<circ> toList) (fst (fst k))) (\<lambda>m. Option.bind ((lookup_trie m \<circ> toList) (snd (fst k))) (\<lambda>m. Mapping.lookup m (snd k))), update = trans_MapOps_update\<rparr>) k = None
[PROOF STEP]
by (auto split: prod.split)
[PROOF STATE]
proof (state)
this:
MapOps.lookup trans_MapOps (MapOps.empty trans_MapOps) k = None

goal (1 subgoal):
 1. \<And>e k k' M. \<lbrakk>(clock_simAbs (fst k), snd k) \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV; (clock_simAbs (fst k'), snd k') \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV\<rbrakk> \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e k k' M. \<lbrakk>(clock_simAbs (fst k), snd k) \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV; (clock_simAbs (fst k'), snd k') \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV\<rbrakk> \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
fix e k k' M
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e k k' M. \<lbrakk>(clock_simAbs (fst k), snd k) \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV; (clock_simAbs (fst k'), snd k') \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV\<rbrakk> \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
assume k: "(clock_simAbs (fst k), snd k) \<in> Clock.jkbpSEC \<times> (UNIV :: 'z set)"
     and k': "(clock_simAbs (fst k'), snd k') \<in> Clock.jkbpSEC \<times> (UNIV :: 'z set)"
[PROOF STATE]
proof (state)
this:
(clock_simAbs (fst k), snd k) \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV
(clock_simAbs (fst k'), snd k') \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV

goal (1 subgoal):
 1. \<And>e k k' M. \<lbrakk>(clock_simAbs (fst k), snd k) \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV; (clock_simAbs (fst k'), snd k') \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV\<rbrakk> \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
show "MapOps.lookup trans_MapOps (MapOps.update trans_MapOps k e M) k'
         = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k)
             then Some e else MapOps.lookup trans_MapOps M k')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
proof(cases "(clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
 2. (clock_simAbs (fst k'), snd k') \<noteq> (clock_simAbs (fst k), snd k) \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
(clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k)

goal (2 subgoals):
 1. (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
 2. (clock_simAbs (fst k'), snd k') \<noteq> (clock_simAbs (fst k), snd k) \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
hence "k = k'"
[PROOF STATE]
proof (prove)
using this:
(clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k)

goal (1 subgoal):
 1. k = k'
[PROOF STEP]
using inj_onD[OF clock_simAbs_inj_on] k k'
[PROOF STATE]
proof (prove)
using this:
(clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k)
\<lbrakk>clock_simAbs ?x = clock_simAbs ?y; ?x \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); ?y \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC))\<rbrakk> \<Longrightarrow> ?x = ?y
(clock_simAbs (fst k), snd k) \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV
(clock_simAbs (fst k'), snd k') \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<times> UNIV

goal (1 subgoal):
 1. k = k'
[PROOF STEP]
by (auto iff: prod_eqI)
[PROOF STATE]
proof (state)
this:
k = k'

goal (2 subgoals):
 1. (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
 2. (clock_simAbs (fst k'), snd k') \<noteq> (clock_simAbs (fst k), snd k) \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
k = k'

goal (1 subgoal):
 1. MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
unfolding trans_MapOps_def trans_MapOps_lookup_def trans_MapOps_update_def trie_odlist_lookup_def trie_odlist_update_with_def
[PROOF STATE]
proof (prove)
using this:
k = k'

goal (1 subgoal):
 1. MapOps.lookup \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind ((lookup_trie m \<circ> toList) (fst (fst k))) (\<lambda>m. Option.bind ((lookup_trie m \<circ> toList) (snd (fst k))) (\<lambda>m. Mapping.lookup m (snd k))), update = \<lambda>k v m. trie_update_with' (toList (fst (fst k))) m empty_trie (trie_update_with (toList (snd (fst k))) Mapping.empty (Mapping.update (snd k) v))\<rparr> (update \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind ((lookup_trie m \<circ> toList) (fst (fst k))) (\<lambda>m. Option.bind ((lookup_trie m \<circ> toList) (snd (fst k))) (\<lambda>m. Mapping.lookup m (snd k))), update = \<lambda>k v m. trie_update_with' (toList (fst (fst k))) m empty_trie (trie_update_with (toList (snd (fst k))) Mapping.empty (Mapping.update (snd k) v))\<rparr> k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind ((lookup_trie m \<circ> toList) (fst (fst k))) (\<lambda>m. Option.bind ((lookup_trie m \<circ> toList) (snd (fst k))) (\<lambda>m. Mapping.lookup m (snd k))), update = \<lambda>k v m. trie_update_with' (toList (fst (fst k))) m empty_trie (trie_update_with (toList (snd (fst k))) Mapping.empty (Mapping.update (snd k) v))\<rparr> M k')
[PROOF STEP]
by (simp add: lookup_trie_update_with lookup_update split: option.split prod.split)
[PROOF STATE]
proof (state)
this:
MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')

goal (1 subgoal):
 1. (clock_simAbs (fst k'), snd k') \<noteq> (clock_simAbs (fst k), snd k) \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (clock_simAbs (fst k'), snd k') \<noteq> (clock_simAbs (fst k), snd k) \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
(clock_simAbs (fst k'), snd k') \<noteq> (clock_simAbs (fst k), snd k)

goal (1 subgoal):
 1. (clock_simAbs (fst k'), snd k') \<noteq> (clock_simAbs (fst k), snd k) \<Longrightarrow> MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(clock_simAbs (fst k'), snd k') \<noteq> (clock_simAbs (fst k), snd k)

goal (1 subgoal):
 1. MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')
[PROOF STEP]
unfolding trans_MapOps_def trans_MapOps_lookup_def trans_MapOps_update_def trie_odlist_lookup_def trie_odlist_update_with_def
[PROOF STATE]
proof (prove)
using this:
(clock_simAbs (fst k'), snd k') \<noteq> (clock_simAbs (fst k), snd k)

goal (1 subgoal):
 1. MapOps.lookup \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind ((lookup_trie m \<circ> toList) (fst (fst k))) (\<lambda>m. Option.bind ((lookup_trie m \<circ> toList) (snd (fst k))) (\<lambda>m. Mapping.lookup m (snd k))), update = \<lambda>k v m. trie_update_with' (toList (fst (fst k))) m empty_trie (trie_update_with (toList (snd (fst k))) Mapping.empty (Mapping.update (snd k) v))\<rparr> (update \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind ((lookup_trie m \<circ> toList) (fst (fst k))) (\<lambda>m. Option.bind ((lookup_trie m \<circ> toList) (snd (fst k))) (\<lambda>m. Mapping.lookup m (snd k))), update = \<lambda>k v m. trie_update_with' (toList (fst (fst k))) m empty_trie (trie_update_with (toList (snd (fst k))) Mapping.empty (Mapping.update (snd k) v))\<rparr> k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind ((lookup_trie m \<circ> toList) (fst (fst k))) (\<lambda>m. Option.bind ((lookup_trie m \<circ> toList) (snd (fst k))) (\<lambda>m. Mapping.lookup m (snd k))), update = \<lambda>k v m. trie_update_with' (toList (fst (fst k))) m empty_trie (trie_update_with (toList (snd (fst k))) Mapping.empty (Mapping.update (snd k) v))\<rparr> M k')
[PROOF STEP]
by (cases "fst k = fst k'")
       (auto simp add: lookup_empty lookup_update_neq prod_eq_iff lookup_trie_update_with split: option.split prod.split)
[PROOF STATE]
proof (state)
this:
MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
MapOps.lookup trans_MapOps (update trans_MapOps k e M) k' = (if (clock_simAbs (fst k'), snd k') = (clock_simAbs (fst k), snd k) then Some e else MapOps.lookup trans_MapOps M k')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in FiniteLinorderEnvironment) acts_MapOps:
  "MapOps clock_simAbs Clock.jkbpSEC acts_MapOps"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MapOps clock_simAbs (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) acts_MapOps
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. clock_simAbs k \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<Longrightarrow> MapOps.lookup acts_MapOps (MapOps.empty acts_MapOps) k = None
 2. \<And>e k k' M. \<lbrakk>clock_simAbs k \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC); clock_simAbs k' \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)\<rbrakk> \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
fix k
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. clock_simAbs k \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC) \<Longrightarrow> MapOps.lookup acts_MapOps (MapOps.empty acts_MapOps) k = None
 2. \<And>e k k' M. \<lbrakk>clock_simAbs k \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC); clock_simAbs k' \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)\<rbrakk> \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
show "MapOps.lookup acts_MapOps (MapOps.empty acts_MapOps) k = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MapOps.lookup acts_MapOps (MapOps.empty acts_MapOps) k = None
[PROOF STEP]
unfolding acts_MapOps_def acts_MapOps_lookup_def trie_odlist_lookup_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MapOps.lookup \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind ((lookup_trie m \<circ> toList) (fst k)) (\<lambda>m. (lookup_trie m \<circ> toList) (snd k)), update = acts_MapOps_update\<rparr> (MapOps.empty \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind ((lookup_trie m \<circ> toList) (fst k)) (\<lambda>m. (lookup_trie m \<circ> toList) (snd k)), update = acts_MapOps_update\<rparr>) k = None
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
MapOps.lookup acts_MapOps (MapOps.empty acts_MapOps) k = None

goal (1 subgoal):
 1. \<And>e k k' M. \<lbrakk>clock_simAbs k \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC); clock_simAbs k' \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)\<rbrakk> \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e k k' M. \<lbrakk>clock_simAbs k \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC); clock_simAbs k' \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)\<rbrakk> \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
fix e k k' M
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>e k k' M. \<lbrakk>clock_simAbs k \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC); clock_simAbs k' \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)\<rbrakk> \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
assume k: "clock_simAbs k \<in> Clock.jkbpSEC"
     and k': "clock_simAbs k' \<in> Clock.jkbpSEC"
[PROOF STATE]
proof (state)
this:
clock_simAbs k \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)
clock_simAbs k' \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)

goal (1 subgoal):
 1. \<And>e k k' M. \<lbrakk>clock_simAbs k \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC); clock_simAbs k' \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)\<rbrakk> \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
show "MapOps.lookup acts_MapOps (MapOps.update acts_MapOps k e M) k'
         = (if clock_simAbs k' = clock_simAbs k
             then Some e else MapOps.lookup acts_MapOps M k')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
proof(cases "clock_simAbs k' = clock_simAbs k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. clock_simAbs k' = clock_simAbs k \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
 2. clock_simAbs k' \<noteq> clock_simAbs k \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
clock_simAbs k' = clock_simAbs k

goal (2 subgoals):
 1. clock_simAbs k' = clock_simAbs k \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
 2. clock_simAbs k' \<noteq> clock_simAbs k \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
hence "k = k'"
[PROOF STATE]
proof (prove)
using this:
clock_simAbs k' = clock_simAbs k

goal (1 subgoal):
 1. k = k'
[PROOF STEP]
using inj_onD[OF clock_simAbs_inj_on] k k'
[PROOF STATE]
proof (prove)
using this:
clock_simAbs k' = clock_simAbs k
\<lbrakk>clock_simAbs ?x = clock_simAbs ?y; ?x \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)); ?y \<in> rel_ext (\<lambda>x. clock_simAbs x \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC))\<rbrakk> \<Longrightarrow> ?x = ?y
clock_simAbs k \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)
clock_simAbs k' \<in> (\<Union>a. Clock.sim_equiv_class a ` Clock.jkbpC)

goal (1 subgoal):
 1. k = k'
[PROOF STEP]
by (auto iff: prod_eqI)
[PROOF STATE]
proof (state)
this:
k = k'

goal (2 subgoals):
 1. clock_simAbs k' = clock_simAbs k \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
 2. clock_simAbs k' \<noteq> clock_simAbs k \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
k = k'

goal (1 subgoal):
 1. MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
unfolding acts_MapOps_def acts_MapOps_lookup_def acts_MapOps_update_def
[PROOF STATE]
proof (prove)
using this:
k = k'

goal (1 subgoal):
 1. MapOps.lookup \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind (trie_odlist_lookup m (fst k)) (\<lambda>m. trie_odlist_lookup m (snd k)), update = \<lambda>k v m. trie_odlist_update_with (fst k) m empty_trie (trie_odlist_update (snd k) v)\<rparr> (update \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind (trie_odlist_lookup m (fst k)) (\<lambda>m. trie_odlist_lookup m (snd k)), update = \<lambda>k v m. trie_odlist_update_with (fst k) m empty_trie (trie_odlist_update (snd k) v)\<rparr> k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind (trie_odlist_lookup m (fst k)) (\<lambda>m. trie_odlist_lookup m (snd k)), update = \<lambda>k v m. trie_odlist_update_with (fst k) m empty_trie (trie_odlist_update (snd k) v)\<rparr> M k')
[PROOF STEP]
by (auto simp: lookup_trie_update lookup_trie_update_with
                     trie_odlist_update_with_def trie_odlist_update_def trie_odlist_lookup_def)
[PROOF STATE]
proof (state)
this:
MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')

goal (1 subgoal):
 1. clock_simAbs k' \<noteq> clock_simAbs k \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. clock_simAbs k' \<noteq> clock_simAbs k \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
clock_simAbs k' \<noteq> clock_simAbs k

goal (1 subgoal):
 1. clock_simAbs k' \<noteq> clock_simAbs k \<Longrightarrow> MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
clock_simAbs k' \<noteq> clock_simAbs k

goal (1 subgoal):
 1. MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')
[PROOF STEP]
unfolding acts_MapOps_def acts_MapOps_lookup_def acts_MapOps_update_def
[PROOF STATE]
proof (prove)
using this:
clock_simAbs k' \<noteq> clock_simAbs k

goal (1 subgoal):
 1. MapOps.lookup \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind (trie_odlist_lookup m (fst k)) (\<lambda>m. trie_odlist_lookup m (snd k)), update = \<lambda>k v m. trie_odlist_update_with (fst k) m empty_trie (trie_odlist_update (snd k) v)\<rparr> (update \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind (trie_odlist_lookup m (fst k)) (\<lambda>m. trie_odlist_lookup m (snd k)), update = \<lambda>k v m. trie_odlist_update_with (fst k) m empty_trie (trie_odlist_update (snd k) v)\<rparr> k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup \<lparr>MapOps.empty = empty_trie, lookup = \<lambda>m k. Option.bind (trie_odlist_lookup m (fst k)) (\<lambda>m. trie_odlist_lookup m (snd k)), update = \<lambda>k v m. trie_odlist_update_with (fst k) m empty_trie (trie_odlist_update (snd k) v)\<rparr> M k')
[PROOF STEP]
by (auto simp: lookup_trie_update lookup_trie_update_with
                     trie_odlist_update_with_def trie_odlist_update_def trie_odlist_lookup_def
               dest: prod_eqI
              split: option.split)
[PROOF STATE]
proof (state)
this:
MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
MapOps.lookup acts_MapOps (update acts_MapOps k e M) k' = (if clock_simAbs k' = clock_simAbs k then Some e else MapOps.lookup acts_MapOps M k')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in FiniteLinorderEnvironment) mkClockAuto_implements:
  "Clock.implements
    (mkClockAuto agents jkbp envInit envAction envTrans envVal envObs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Clock.implements (mkClockAuto agents jkbp envInit envAction envTrans envVal envObs)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Clock.implements (mkClockAuto agents jkbp envInit envAction envTrans envVal envObs)
[PROOF STEP]
using Clock.k_mkAlgAuto_implements
[PROOF STATE]
proof (prove)
using this:
Clock.implements Clock.k_mkAlgAuto

goal (1 subgoal):
 1. Clock.implements (mkClockAuto agents jkbp envInit envAction envTrans envVal envObs)
[PROOF STEP]
unfolding mkClockAuto_def mkAlgAuto_def Clock.k_frontier_def
[PROOF STATE]
proof (prove)
using this:
Clock.implements (\<lambda>a. let auto = alg_dfs acts_MapOps trans_MapOps (local.clock_simObs a) (local.clock_simTrans a) (local.clock_simAction a) (map (local.clock_simInit a \<circ> envObs a) envInit) in \<lparr>pInit = local.clock_simInit a, pTrans = \<lambda>obs ec. the (MapOps.lookup trans_MapOps (aTrans auto) (ec, obs)), pAct = \<lambda>ec. the (MapOps.lookup acts_MapOps (aActs auto) ec)\<rparr>)

goal (1 subgoal):
 1. Clock.implements (\<lambda>a. let auto = alg_dfs acts_MapOps trans_MapOps (local.clock_simObs a) (local.clock_simTrans a) (local.clock_simAction a) (map (local.clock_simInit a \<circ> envObs a) envInit) in \<lparr>pInit = local.clock_simInit a, pTrans = \<lambda>obs ec. the (MapOps.lookup trans_MapOps (aTrans auto) (ec, obs)), pAct = \<lambda>ec. the (MapOps.lookup acts_MapOps (aActs auto) ec)\<rparr>)
[PROOF STEP]
by simp


[STATEMENT]
lemma (in FiniteLinorderEnvironment)
  "mkClockAuto agents jkbp envInit envAction envTrans envVal envObs
 = (\<lambda>a. alg_mk_auto acts_MapOps trans_MapOps (clock_simInit a) (ClockAutoDFS agents jkbp envInit envAction envTrans envVal envObs a))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mkClockAuto agents jkbp envInit envAction envTrans envVal envObs = (\<lambda>a. alg_mk_auto acts_MapOps trans_MapOps (local.clock_simInit a) (ClockAutoDFS agents jkbp envInit envAction envTrans envVal envObs a))
[PROOF STEP]
unfolding mkClockAuto_def ClockAutoDFS_def mkAlgAuto_def alg_mk_auto_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>a. let auto = alg_dfs acts_MapOps trans_MapOps (local.clock_simObs a) (local.clock_simTrans a) (local.clock_simAction a) (map (local.clock_simInit a \<circ> envObs a) envInit) in \<lparr>pInit = local.clock_simInit a, pTrans = \<lambda>obs ec. the (MapOps.lookup trans_MapOps (aTrans auto) (ec, obs)), pAct = \<lambda>ec. the (MapOps.lookup acts_MapOps (aActs auto) ec)\<rparr>) = (\<lambda>a. \<lparr>pInit = local.clock_simInit a, pTrans = \<lambda>obs ec. the (MapOps.lookup trans_MapOps (aTrans (alg_dfs acts_MapOps trans_MapOps (local.clock_simObs a) (local.clock_simTrans a) (local.clock_simAction a) (map (local.clock_simInit a \<circ> envObs a) envInit))) (ec, obs)), pAct = \<lambda>ec. the (MapOps.lookup acts_MapOps (aActs (alg_dfs acts_MapOps trans_MapOps (local.clock_simObs a) (local.clock_simTrans a) (local.clock_simAction a) (map (local.clock_simInit a \<circ> envObs a) envInit))) ec)\<rparr>)
[PROOF STEP]
by (simp add: Let_def)


[STATEMENT]
lemma initiali_aodv [intro!, simp]: "initiali i (init (opaodv i)) (init (paodv i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. initiali i (init (opaodv i)) (init (paodv i))
[PROOF STEP]
unfolding \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V_def \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. initiali i (init \<lparr>init = {(aodv_init, \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V PAodv)}, trans = oseqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V i\<rparr>) (init \<lparr>init = {(aodv_init i, \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V PAodv)}, trans = seqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V\<rparr>)
[PROOF STEP]
by rule simp_all


[STATEMENT]
lemma oaodv_control_within [simp]: "control_within \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (init (opaodv i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. control_within \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (init (opaodv i))
[PROOF STEP]
unfolding \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. control_within \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V (init \<lparr>init = {(aodv_init, \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V PAodv)}, trans = oseqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V i\<rparr>)
[PROOF STEP]
by (rule control_withinI) (auto simp del: \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V_simps)


[STATEMENT]
lemma \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V'_labels [simp]: "(\<sigma>, p) \<in> \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V' \<Longrightarrow>  labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p = {PAodv-:0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, p) \<in> \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V' \<Longrightarrow> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p = {PAodv-:0}
[PROOF STEP]
unfolding \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, p) \<in> {(aodv_init, \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V PAodv)} \<Longrightarrow> labels \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V p = {PAodv-:0}
[PROOF STEP]
by simp


[STATEMENT]
lemma oaodv_init_kD_empty [simp]:
  "(\<sigma>, p) \<in> \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V' \<Longrightarrow> kD (rt (\<sigma> i)) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, p) \<in> \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V' \<Longrightarrow> kD (rt (\<sigma> i)) = {}
[PROOF STEP]
unfolding \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V'_def kD_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, p) \<in> {(aodv_init, \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V PAodv)} \<Longrightarrow> {dip. rt (\<sigma> i) dip \<noteq> None} = {}
[PROOF STEP]
by simp


[STATEMENT]
lemma oaodv_init_vD_empty [simp]:
  "(\<sigma>, p) \<in> \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V' \<Longrightarrow> vD (rt (\<sigma> i)) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, p) \<in> \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V' \<Longrightarrow> vD (rt (\<sigma> i)) = {}
[PROOF STEP]
unfolding \<sigma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V'_def vD_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, p) \<in> {(aodv_init, \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V PAodv)} \<Longrightarrow> {dip. flag (rt (\<sigma> i)) dip = Some val} = {}
[PROOF STEP]
by simp


[STATEMENT]
lemma oaodv_trans: "trans (opaodv i) = oseqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. automaton.trans (opaodv i) = oseqp_sos \<Gamma>\<^sub>A\<^sub>O\<^sub>D\<^sub>V i
[PROOF STEP]
by simp


[STATEMENT]
lemma dcd_pdg: assumes \<open>n dcd\<^bsup>\<pi>,v\<^esup>\<rightarrow> m via \<pi>' m'\<close> obtains l where \<open>(\<pi> m,l)\<in> pdg\<close> and \<open>(l,\<pi> n)\<in>pdg\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>(\<pi> m, l) \<in> pdg; (l, \<pi> n) \<in> pdg\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>l. \<lbrakk>(\<pi> m, l) \<in> pdg; (l, \<pi> n) \<in> pdg\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume r: \<open>(\<And>l. (\<pi> m, l) \<in> pdg \<Longrightarrow> (l, \<pi> n) \<in> pdg \<Longrightarrow> thesis)\<close>
[PROOF STATE]
proof (state)
this:
\<lbrakk>(\<pi> m, ?l1) \<in> pdg; (?l1, \<pi> n) \<in> pdg\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>(\<pi> m, l) \<in> pdg; (l, \<pi> n) \<in> pdg\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
obtain l' n' where ln: \<open>cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m' \<and> cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n' \<and> n' dd\<^bsup>\<pi>',v\<^esup>\<rightarrow> l' \<and> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m'\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n' l'. cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m' \<and> cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n' \<and> n' dd\<^bsup>\<pi>',v\<^esup>\<rightarrow> l' \<and> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
n dcd\<^bsup>\<pi>,v\<^esup>\<rightarrow> m via \<pi>' m'

goal (1 subgoal):
 1. (\<And>n' l'. cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m' \<and> cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n' \<and> n' dd\<^bsup>\<pi>',v\<^esup>\<rightarrow> l' \<and> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_dcdi_via_def
[PROOF STATE]
proof (prove)
using this:
is_path \<pi> \<and> m < n \<and> (\<exists>l' n'. cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m' \<and> cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n' \<and> n' dd\<^bsup>\<pi>',v\<^esup>\<rightarrow> l' \<and> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m') \<and> (\<forall>l\<in>{m..<n}. v \<notin> local.writes (\<pi> l))

goal (1 subgoal):
 1. (\<And>n' l'. cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m' \<and> cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n' \<and> n' dd\<^bsup>\<pi>',v\<^esup>\<rightarrow> l' \<and> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m' \<and> cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n' \<and> n' dd\<^bsup>\<pi>',v\<^esup>\<rightarrow> l' \<and> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m'

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>(\<pi> m, l) \<in> pdg; (l, \<pi> n) \<in> pdg\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
hence  mn: \<open>\<pi>' m' = \<pi> m \<and> \<pi>' n' = \<pi> n\<close>
[PROOF STATE]
proof (prove)
using this:
cs\<^bsup>\<pi>\<^esup> m = cs\<^bsup>\<pi>'\<^esup> m' \<and> cs\<^bsup>\<pi>\<^esup> n = cs\<^bsup>\<pi>'\<^esup> n' \<and> n' dd\<^bsup>\<pi>',v\<^esup>\<rightarrow> l' \<and> l' cd\<^bsup>\<pi>'\<^esup>\<rightarrow> m'

goal (1 subgoal):
 1. \<pi>' m' = \<pi> m \<and> \<pi>' n' = \<pi> n
[PROOF STEP]
by (metis last_cs ln)
[PROOF STATE]
proof (state)
this:
\<pi>' m' = \<pi> m \<and> \<pi>' n' = \<pi> n

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>(\<pi> m, l) \<in> pdg; (l, \<pi> n) \<in> pdg\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have 1: \<open>(\<pi> m, \<pi>' l') \<in> pdg\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi> m, \<pi>' l') \<in> pdg
[PROOF STEP]
by (metis ln mn pdg.intros(1))
[PROOF STATE]
proof (state)
this:
(\<pi> m, \<pi>' l') \<in> pdg

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>(\<pi> m, l) \<in> pdg; (l, \<pi> n) \<in> pdg\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have 2: \<open>(\<pi>' l', \<pi> n) \<in> pdg\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi>' l', \<pi> n) \<in> pdg
[PROOF STEP]
by (metis ln mn pdg.intros(2))
[PROOF STATE]
proof (state)
this:
(\<pi>' l', \<pi> n) \<in> pdg

goal (1 subgoal):
 1. (\<And>l. \<lbrakk>(\<pi> m, l) \<in> pdg; (l, \<pi> n) \<in> pdg\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
using 1 2 r
[PROOF STATE]
proof (prove)
using this:
(\<pi> m, \<pi>' l') \<in> pdg
(\<pi>' l', \<pi> n) \<in> pdg
\<lbrakk>(\<pi> m, ?l1) \<in> pdg; (?l1, \<pi> n) \<in> pdg\<rbrakk> \<Longrightarrow> thesis

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scp_slice: \<open>(\<pi>, i)\<in> scp \<Longrightarrow> \<pi> i \<in> slice\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi>, i) \<in> scp \<Longrightarrow> \<pi> i \<in> slice
[PROOF STEP]
apply (induction rule: scp.induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>h \<sigma> n. \<lbrakk>h \<in> local.hvars; h \<in> local.reads (path \<sigma> n); \<forall>k<n. h \<notin> local.writes (path \<sigma> k)\<rbrakk> \<Longrightarrow> path \<sigma> n \<in> slice
 2. \<And>\<pi> m n. \<lbrakk>(\<pi>, m) \<in> scp; \<pi> m \<in> slice; n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> \<pi> n \<in> slice
 3. \<And>\<pi> m n v. \<lbrakk>(\<pi>, m) \<in> scp; \<pi> m \<in> slice; n dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> \<pi> n \<in> slice
 4. \<And>\<pi> m \<pi>' m' n v. \<lbrakk>(\<pi>, m) \<in> scp; \<pi> m \<in> slice; (\<pi>', m') \<in> scp; \<pi>' m' \<in> slice; n dcd\<^bsup>\<pi>,v\<^esup>\<rightarrow> m via \<pi>' m'\<rbrakk> \<Longrightarrow> \<pi> n \<in> slice
[PROOF STEP]
apply (simp add: path_in_nodes slice.intros(1) sources.intros)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>\<pi> m n. \<lbrakk>(\<pi>, m) \<in> scp; \<pi> m \<in> slice; n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> \<pi> n \<in> slice
 2. \<And>\<pi> m n v. \<lbrakk>(\<pi>, m) \<in> scp; \<pi> m \<in> slice; n dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> \<pi> n \<in> slice
 3. \<And>\<pi> m \<pi>' m' n v. \<lbrakk>(\<pi>, m) \<in> scp; \<pi> m \<in> slice; (\<pi>', m') \<in> scp; \<pi>' m' \<in> slice; n dcd\<^bsup>\<pi>,v\<^esup>\<rightarrow> m via \<pi>' m'\<rbrakk> \<Longrightarrow> \<pi> n \<in> slice
[PROOF STEP]
using pdg.intros(1) slice.intros(2)
[PROOF STATE]
proof (prove)
using this:
?i cd\<^bsup>?\<pi>\<^esup>\<rightarrow> ?k \<Longrightarrow> (?\<pi> ?k, ?\<pi> ?i) \<in> pdg
\<lbrakk>?m \<in> slice; (?m, ?n) \<in> pdg\<rbrakk> \<Longrightarrow> ?n \<in> slice

goal (3 subgoals):
 1. \<And>\<pi> m n. \<lbrakk>(\<pi>, m) \<in> scp; \<pi> m \<in> slice; n cd\<^bsup>\<pi>\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> \<pi> n \<in> slice
 2. \<And>\<pi> m n v. \<lbrakk>(\<pi>, m) \<in> scp; \<pi> m \<in> slice; n dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> \<pi> n \<in> slice
 3. \<And>\<pi> m \<pi>' m' n v. \<lbrakk>(\<pi>, m) \<in> scp; \<pi> m \<in> slice; (\<pi>', m') \<in> scp; \<pi>' m' \<in> slice; n dcd\<^bsup>\<pi>,v\<^esup>\<rightarrow> m via \<pi>' m'\<rbrakk> \<Longrightarrow> \<pi> n \<in> slice
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<pi> m n v. \<lbrakk>(\<pi>, m) \<in> scp; \<pi> m \<in> slice; n dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> \<pi> n \<in> slice
 2. \<And>\<pi> m \<pi>' m' n v. \<lbrakk>(\<pi>, m) \<in> scp; \<pi> m \<in> slice; (\<pi>', m') \<in> scp; \<pi>' m' \<in> slice; n dcd\<^bsup>\<pi>,v\<^esup>\<rightarrow> m via \<pi>' m'\<rbrakk> \<Longrightarrow> \<pi> n \<in> slice
[PROOF STEP]
using pdg.intros(2) slice.intros(2)
[PROOF STATE]
proof (prove)
using this:
?i dd\<^bsup>?\<pi>,?v\<^esup>\<rightarrow> ?k \<Longrightarrow> (?\<pi> ?k, ?\<pi> ?i) \<in> pdg
\<lbrakk>?m \<in> slice; (?m, ?n) \<in> pdg\<rbrakk> \<Longrightarrow> ?n \<in> slice

goal (2 subgoals):
 1. \<And>\<pi> m n v. \<lbrakk>(\<pi>, m) \<in> scp; \<pi> m \<in> slice; n dd\<^bsup>\<pi>,v\<^esup>\<rightarrow> m\<rbrakk> \<Longrightarrow> \<pi> n \<in> slice
 2. \<And>\<pi> m \<pi>' m' n v. \<lbrakk>(\<pi>, m) \<in> scp; \<pi> m \<in> slice; (\<pi>', m') \<in> scp; \<pi>' m' \<in> slice; n dcd\<^bsup>\<pi>,v\<^esup>\<rightarrow> m via \<pi>' m'\<rbrakk> \<Longrightarrow> \<pi> n \<in> slice
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<pi> m \<pi>' m' n v. \<lbrakk>(\<pi>, m) \<in> scp; \<pi> m \<in> slice; (\<pi>', m') \<in> scp; \<pi>' m' \<in> slice; n dcd\<^bsup>\<pi>,v\<^esup>\<rightarrow> m via \<pi>' m'\<rbrakk> \<Longrightarrow> \<pi> n \<in> slice
[PROOF STEP]
by (metis dcd_pdg slice.intros(2))


[STATEMENT]
lemma scop_slice: \<open>(\<pi>, i) \<in> scop \<Longrightarrow> \<pi> i \<in> slice \<inter> dom(att)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<pi>, i) \<in> scop \<Longrightarrow> \<pi> i \<in> slice \<inter> dom local.att
[PROOF STEP]
by (metis IntI scop.cases scp_slice)


[STATEMENT]
lemma pdg_correct: assumes \<open>slice \<inter> dom(att) = {}\<close> shows \<open>secure\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. secure
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> secure \<Longrightarrow> False
[PROOF STEP]
assume \<open>\<not> secure\<close>
[PROOF STATE]
proof (state)
this:
\<not> secure

goal (1 subgoal):
 1. \<not> secure \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> secure
[PROOF STEP]
obtain \<pi> i where \<open>(\<pi>, i) \<in> scop\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> secure

goal (1 subgoal):
 1. (\<And>\<pi> i. (\<pi>, i) \<in> scop \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using scop_correct
[PROOF STATE]
proof (prove)
using this:
\<not> secure
scop = {} \<Longrightarrow> secure

goal (1 subgoal):
 1. (\<And>\<pi> i. (\<pi>, i) \<in> scop \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(\<pi>, i) \<in> scop

goal (1 subgoal):
 1. \<not> secure \<Longrightarrow> False
[PROOF STEP]
thus \<open>False\<close>
[PROOF STATE]
proof (prove)
using this:
(\<pi>, i) \<in> scop

goal (1 subgoal):
 1. False
[PROOF STEP]
using scop_slice assms
[PROOF STATE]
proof (prove)
using this:
(\<pi>, i) \<in> scop
(?\<pi>, ?i) \<in> scop \<Longrightarrow> ?\<pi> ?i \<in> slice \<inter> dom local.att
slice \<inter> dom local.att = {}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eq_refl: "eq\<cdot>x\<cdot>x \<noteq> \<bottom> \<Longrightarrow> eq\<cdot>x\<cdot>x = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq\<cdot>x\<cdot>x \<noteq> \<bottom> \<Longrightarrow> eq\<cdot>x\<cdot>x = TT
[PROOF STEP]
by (cases "eq\<cdot>x\<cdot>x") simp+


[STATEMENT]
lemma eqD [dest]:
  "eq\<cdot>x\<cdot>y = TT \<Longrightarrow> x = y"
  "eq\<cdot>x\<cdot>y = FF \<Longrightarrow> x \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (eq\<cdot>x\<cdot>y = TT \<Longrightarrow> x = y) &&& (eq\<cdot>x\<cdot>y = FF \<Longrightarrow> x \<noteq> y)
[PROOF STEP]
by (auto elim: eq_TT_dest)


[STATEMENT]
lemma eq_ONE_ONE [simp]: "eq\<cdot>ONE\<cdot>ONE = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq\<cdot>ONE\<cdot>ONE = TT
[PROOF STEP]
unfolding ONE_def eq_lift_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Lambda> (Def x) (Def y). Def (x = y))\<cdot>(Def ())\<cdot>(Def ()) = TT
[PROOF STEP]
by simp


[STATEMENT]
lemma oppOrdering_simps [simp]:
  "oppOrdering\<cdot>LT = GT"
  "oppOrdering\<cdot>EQ = EQ"
  "oppOrdering\<cdot>GT = LT"
  "oppOrdering\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (oppOrdering\<cdot>LT = GT &&& oppOrdering\<cdot>EQ = EQ) &&& oppOrdering\<cdot>GT = LT &&& oppOrdering\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
unfolding oppOrdering_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Abs_cfun (Rep_cfun (Ordering_case\<cdot>GT\<cdot>EQ\<cdot>LT))\<cdot>LT = GT &&& Abs_cfun (Rep_cfun (Ordering_case\<cdot>GT\<cdot>EQ\<cdot>LT))\<cdot>EQ = EQ) &&& Abs_cfun (Rep_cfun (Ordering_case\<cdot>GT\<cdot>EQ\<cdot>LT))\<cdot>GT = LT &&& Abs_cfun (Rep_cfun (Ordering_case\<cdot>GT\<cdot>EQ\<cdot>LT))\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by simp_all


[STATEMENT]
lemma lt_eq_TT_iff: "lt\<cdot>x\<cdot>y = TT \<longleftrightarrow> compare\<cdot>x\<cdot>y = LT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lt\<cdot>x\<cdot>y = TT) = (compare\<cdot>x\<cdot>y = LT)
[PROOF STEP]
by (cases "compare\<cdot>x\<cdot>y") (simp add: lt_def)+


[STATEMENT]
lemma lt_strict [simp]:
  shows "lt\<cdot>\<bottom>\<cdot>x = \<bottom>"
    and "lt\<cdot>x\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lt\<cdot>\<bottom>\<cdot>x = \<bottom> &&& lt\<cdot>x\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by (simp add: lt_def)+


[STATEMENT]
lemma le_strict [simp]:
  shows "le\<cdot>\<bottom>\<cdot>x = \<bottom>"
    and "le\<cdot>x\<cdot>\<bottom> = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le\<cdot>\<bottom>\<cdot>x = \<bottom> &&& le\<cdot>x\<cdot>\<bottom> = \<bottom>
[PROOF STEP]
by (simp add: le_def)+


[STATEMENT]
lemma eq_TT_dest: "eq\<cdot>x\<cdot>y = TT \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eq\<cdot>x\<cdot>y = TT \<Longrightarrow> x = y
[PROOF STEP]
by (cases "compare\<cdot>x\<cdot>y") (auto dest: compare_EQ_dest simp: eq_conv_compare)+


[STATEMENT]
lemma le_iff_lt_or_eq:
  "le\<cdot>x\<cdot>y = TT \<longleftrightarrow> lt\<cdot>x\<cdot>y = TT \<or> eq\<cdot>x\<cdot>y = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (le\<cdot>x\<cdot>y = TT) = (lt\<cdot>x\<cdot>y = TT \<or> eq\<cdot>x\<cdot>y = TT)
[PROOF STEP]
by (cases "compare\<cdot>x\<cdot>y") (simp add: le_def lt_def eq_conv_compare)+


[STATEMENT]
lemma compare_sym:
  "compare\<cdot>x\<cdot>y = (case compare\<cdot>y\<cdot>x of LT \<Rightarrow> GT | EQ \<Rightarrow> EQ | GT \<Rightarrow> LT)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compare\<cdot>x\<cdot>y = (case compare\<cdot>y\<cdot>x of LT \<Rightarrow> GT | EQ \<Rightarrow> EQ | GT \<Rightarrow> LT)
[PROOF STEP]
by (subst oppOrdering_compare [symmetric]) (simp add: oppOrdering_def)


[STATEMENT]
lemma compare_self_neq_LT [simp]: "compare\<cdot>x\<cdot>x \<noteq> LT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compare\<cdot>x\<cdot>x \<noteq> LT
[PROOF STEP]
using compare_self_below_EQ [of x]
[PROOF STATE]
proof (prove)
using this:
compare\<cdot>x\<cdot>x \<sqsubseteq> EQ

goal (1 subgoal):
 1. compare\<cdot>x\<cdot>x \<noteq> LT
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma compare_self_neq_GT [simp]: "compare\<cdot>x\<cdot>x \<noteq> GT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. compare\<cdot>x\<cdot>x \<noteq> GT
[PROOF STEP]
using compare_self_below_EQ [of x]
[PROOF STATE]
proof (prove)
using this:
compare\<cdot>x\<cdot>x \<sqsubseteq> EQ

goal (1 subgoal):
 1. compare\<cdot>x\<cdot>x \<noteq> GT
[PROOF STEP]
by clarsimp


[STATEMENT]
lemma lt_trans: "lt\<cdot>x\<cdot>y = TT \<Longrightarrow> lt\<cdot>y\<cdot>z = TT \<Longrightarrow> lt\<cdot>x\<cdot>z = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>lt\<cdot>x\<cdot>y = TT; lt\<cdot>y\<cdot>z = TT\<rbrakk> \<Longrightarrow> lt\<cdot>x\<cdot>z = TT
[PROOF STEP]
unfolding lt_eq_TT_iff
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>compare\<cdot>x\<cdot>y = LT; compare\<cdot>y\<cdot>z = LT\<rbrakk> \<Longrightarrow> compare\<cdot>x\<cdot>z = LT
[PROOF STEP]
by (rule compare_LT_trans)


[STATEMENT]
lemma compare_GT_iff_LT: "compare\<cdot>x\<cdot>y = GT \<longleftrightarrow> compare\<cdot>y\<cdot>x = LT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (compare\<cdot>x\<cdot>y = GT) = (compare\<cdot>y\<cdot>x = LT)
[PROOF STEP]
by (cases "compare\<cdot>x\<cdot>y", simp_all add: compare_sym [of y x])


[STATEMENT]
lemma compare_GT_trans:
  "compare\<cdot>x\<cdot>y = GT \<Longrightarrow> compare\<cdot>y\<cdot>z = GT \<Longrightarrow> compare\<cdot>x\<cdot>z = GT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>compare\<cdot>x\<cdot>y = GT; compare\<cdot>y\<cdot>z = GT\<rbrakk> \<Longrightarrow> compare\<cdot>x\<cdot>z = GT
[PROOF STEP]
unfolding compare_GT_iff_LT
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>compare\<cdot>y\<cdot>x = LT; compare\<cdot>z\<cdot>y = LT\<rbrakk> \<Longrightarrow> compare\<cdot>z\<cdot>x = LT
[PROOF STEP]
by (rule compare_LT_trans)


[STATEMENT]
lemma compare_EQ_iff_eq_TT:
  "compare\<cdot>x\<cdot>y = EQ \<longleftrightarrow> eq\<cdot>x\<cdot>y = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (compare\<cdot>x\<cdot>y = EQ) = (eq\<cdot>x\<cdot>y = TT)
[PROOF STEP]
by (cases "compare\<cdot>x\<cdot>y") (simp add: is_EQ_def eq_conv_compare)+


[STATEMENT]
lemma compare_EQ_trans:
  "compare\<cdot>x\<cdot>y = EQ \<Longrightarrow> compare\<cdot>y\<cdot>z = EQ \<Longrightarrow> compare\<cdot>x\<cdot>z = EQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>compare\<cdot>x\<cdot>y = EQ; compare\<cdot>y\<cdot>z = EQ\<rbrakk> \<Longrightarrow> compare\<cdot>x\<cdot>z = EQ
[PROOF STEP]
by (blast dest: compare_EQ_dest)


[STATEMENT]
lemma le_trans:
  "le\<cdot>x\<cdot>y = TT \<Longrightarrow> le\<cdot>y\<cdot>z = TT \<Longrightarrow> le\<cdot>x\<cdot>z = TT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>le\<cdot>x\<cdot>y = TT; le\<cdot>y\<cdot>z = TT\<rbrakk> \<Longrightarrow> le\<cdot>x\<cdot>z = TT
[PROOF STEP]
by (auto dest: eq_TT_dest lt_trans simp: le_iff_lt_or_eq)


[STATEMENT]
lemma neg_lt: "neg\<cdot>(lt\<cdot>x\<cdot>y) = le\<cdot>y\<cdot>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neg\<cdot>(lt\<cdot>x\<cdot>y) = le\<cdot>y\<cdot>x
[PROOF STEP]
by (cases "compare\<cdot>x\<cdot>y", simp_all add: le_def lt_def compare_sym [of y x])


[STATEMENT]
lemma neg_le: "neg\<cdot>(le\<cdot>x\<cdot>y) = lt\<cdot>y\<cdot>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. neg\<cdot>(le\<cdot>x\<cdot>y) = lt\<cdot>y\<cdot>x
[PROOF STEP]
by (cases "compare\<cdot>x\<cdot>y", simp_all add: le_def lt_def compare_sym [of y x])


[STATEMENT]
lemma thenOrdering_simps [simp]:
  "thenOrdering\<cdot>LT\<cdot>y = LT"
  "thenOrdering\<cdot>EQ\<cdot>y = y"
  "thenOrdering\<cdot>GT\<cdot>y = GT"
  "thenOrdering\<cdot>\<bottom>\<cdot>y = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (thenOrdering\<cdot>LT\<cdot>y = LT &&& thenOrdering\<cdot>EQ\<cdot>y = y) &&& thenOrdering\<cdot>GT\<cdot>y = GT &&& thenOrdering\<cdot>\<bottom>\<cdot>y = \<bottom>
[PROOF STEP]
unfolding thenOrdering_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<Lambda> x y. case x of LT \<Rightarrow> LT | EQ \<Rightarrow> y | GT \<Rightarrow> GT)\<cdot>LT\<cdot>y = LT &&& (\<Lambda> x y. case x of LT \<Rightarrow> LT | EQ \<Rightarrow> y | GT \<Rightarrow> GT)\<cdot>EQ\<cdot>y = y) &&& (\<Lambda> x y. case x of LT \<Rightarrow> LT | EQ \<Rightarrow> y | GT \<Rightarrow> GT)\<cdot>GT\<cdot>y = GT &&& (\<Lambda> x y. case x of LT \<Rightarrow> LT | EQ \<Rightarrow> y | GT \<Rightarrow> GT)\<cdot>\<bottom>\<cdot>y = \<bottom>
[PROOF STEP]
by simp_all


[STATEMENT]
lemma thenOrdering_LT_iff [simp]:
  "thenOrdering\<cdot>x\<cdot>y = LT \<longleftrightarrow> x = LT \<or> x = EQ \<and> y = LT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (thenOrdering\<cdot>x\<cdot>y = LT) = (x = LT \<or> x = EQ \<and> y = LT)
[PROOF STEP]
by (cases x, simp_all)


[STATEMENT]
lemma thenOrdering_EQ_iff [simp]:
  "thenOrdering\<cdot>x\<cdot>y = EQ \<longleftrightarrow> x = EQ \<and> y = EQ"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (thenOrdering\<cdot>x\<cdot>y = EQ) = (x = EQ \<and> y = EQ)
[PROOF STEP]
by (cases x, simp_all)


[STATEMENT]
lemma thenOrdering_GT_iff [simp]:
  "thenOrdering\<cdot>x\<cdot>y = GT \<longleftrightarrow> x = GT \<or> x = EQ \<and> y = GT"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (thenOrdering\<cdot>x\<cdot>y = GT) = (x = GT \<or> x = EQ \<and> y = GT)
[PROOF STEP]
by (cases x, simp_all)


[STATEMENT]
lemma thenOrdering_below_EQ_iff [simp]:
  "thenOrdering\<cdot>x\<cdot>y \<sqsubseteq> EQ \<longleftrightarrow> x \<sqsubseteq> EQ \<and> (x = \<bottom> \<or> y \<sqsubseteq> EQ)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (thenOrdering\<cdot>x\<cdot>y \<sqsubseteq> EQ) = (x \<sqsubseteq> EQ \<and> (x = \<bottom> \<or> y \<sqsubseteq> EQ))
[PROOF STEP]
by (cases x) simp_all


[STATEMENT]
lemma is_EQ_thenOrdering [simp]:
  "is_EQ\<cdot>(thenOrdering\<cdot>x\<cdot>y) = (is_EQ\<cdot>x andalso is_EQ\<cdot>y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_EQ\<cdot>(thenOrdering\<cdot>x\<cdot>y) = (is_EQ\<cdot>x andalso is_EQ\<cdot>y)
[PROOF STEP]
by (cases x) simp_all


[STATEMENT]
lemma oppOrdering_thenOrdering:
  "oppOrdering\<cdot>(thenOrdering\<cdot>x\<cdot>y) =
    thenOrdering\<cdot>(oppOrdering\<cdot>x)\<cdot>(oppOrdering\<cdot>y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oppOrdering\<cdot>(thenOrdering\<cdot>x\<cdot>y) = thenOrdering\<cdot>(oppOrdering\<cdot>x)\<cdot>(oppOrdering\<cdot>y)
[PROOF STEP]
by (cases x) simp_all


[STATEMENT]
lemma lt_le:
  "lt\<cdot>(x::'a::Ord_linear)\<cdot>y = (le\<cdot>x\<cdot>y andalso neq\<cdot>x\<cdot>y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lt\<cdot>x\<cdot>y = (le\<cdot>x\<cdot>y andalso neq\<cdot>x\<cdot>y)
[PROOF STEP]
by (cases "compare\<cdot>x\<cdot>y")
     (auto simp: lt_def le_def eq_conv_compare)


[STATEMENT]
lemma game_induct [case_names Game Assign ODE Test Choice Compose Loop Dual]:
   "(\<And>a. P (Game a))
    \<Longrightarrow> (\<And>x \<theta>. P (Assign x \<theta>))
    \<Longrightarrow> (\<And>x \<theta>. P (ODE x \<theta>))
    \<Longrightarrow> (\<And>\<phi>. P (? \<phi>))
    \<Longrightarrow> (\<And>\<alpha> \<beta>. P \<alpha> \<Longrightarrow> P \<beta> \<Longrightarrow> P (\<alpha> \<union>\<union> \<beta>))
    \<Longrightarrow> (\<And>\<alpha> \<beta>. P \<alpha> \<Longrightarrow> P \<beta> \<Longrightarrow> P (\<alpha> ;; \<beta>))
    \<Longrightarrow> (\<And>\<alpha>. P \<alpha> \<Longrightarrow> P (\<alpha>**))
    \<Longrightarrow> (\<And>\<alpha>. P \<alpha> \<Longrightarrow> P (\<alpha>^d))
    \<Longrightarrow> P \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. P (Game a); \<And>x \<theta>. P (x := \<theta>); \<And>x \<theta>. P (ODE x \<theta>); \<And>\<phi>. P (? \<phi>); \<And>\<alpha> \<beta>. \<lbrakk>P \<alpha>; P \<beta>\<rbrakk> \<Longrightarrow> P (\<alpha> \<union>\<union> \<beta>); \<And>\<alpha> \<beta>. \<lbrakk>P \<alpha>; P \<beta>\<rbrakk> \<Longrightarrow> P (\<alpha> ;; \<beta>); \<And>\<alpha>. P \<alpha> \<Longrightarrow> P \<alpha>**; \<And>\<alpha>. P \<alpha> \<Longrightarrow> P \<alpha>^d\<rbrakk> \<Longrightarrow> P \<alpha>
[PROOF STEP]
by(induction rule: game.induct) (auto)


[STATEMENT]
lemma fml_induct [case_names Pred Geq Not And Exists Diamond]:
  "(\<And>x \<theta>. P (Pred x \<theta>))
  \<Longrightarrow> (\<And>\<theta> \<eta>. P (Geq \<theta> \<eta>))
  \<Longrightarrow> (\<And>\<phi>. P \<phi> \<Longrightarrow> P (Not \<phi>))
  \<Longrightarrow> (\<And>\<phi> \<psi>. P \<phi> \<Longrightarrow> P \<psi> \<Longrightarrow> P (And \<phi> \<psi>))
  \<Longrightarrow> (\<And>x \<phi>. P \<phi> \<Longrightarrow> P (Exists x \<phi>))
  \<Longrightarrow> (\<And>\<alpha> \<phi>. P \<phi> \<Longrightarrow> P (Diamond \<alpha> \<phi>))
  \<Longrightarrow> P \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x \<theta>. P (Pred x \<theta>); \<And>\<theta> \<eta>. P (Geq \<theta> \<eta>); \<And>\<phi>. P \<phi> \<Longrightarrow> P (! \<phi>); \<And>\<phi> \<psi>. \<lbrakk>P \<phi>; P \<psi>\<rbrakk> \<Longrightarrow> P (\<phi> && \<psi>); \<And>x \<phi>. P \<phi> \<Longrightarrow> P (Exists x \<phi>); \<And>\<alpha> \<phi>. P \<phi> \<Longrightarrow> P (\<langle> \<alpha> \<rangle> \<phi>)\<rbrakk> \<Longrightarrow> P \<phi>
[PROOF STEP]
by (induction rule: fml.induct) (auto)


[STATEMENT]
lemma iR_prop_rules [simp]: "sset prop_rules = {allI, allE, impI, impE}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sset prop_rules = {allI, allE, impI, impE}
[PROOF STEP]
unfolding prop_rules_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sset (cycle [allI, allE, impI, impE]) = {allI, allE, impI, impE}
[PROOF STEP]
by simp


[STATEMENT]
lemma bytes_takefill_rep_eq[code abstract]:
  "Rep_bytes (bytes_takefill b n bs) = takefill b n (Rep_bytes bs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_bytes (bytes_takefill b n bs) = takefill b n (Rep_bytes bs)
[PROOF STEP]
using bytes_takefill.rep_eq Rep_uint8_inverse
[PROOF STATE]
proof (prove)
using this:
Rep_bytes (bytes_takefill ?x ?xa ?xb) = takefill (Abs_uint8 (Rep_uint8 ?x)) ?xa (Rep_bytes ?xb)
Abs_uint8 (Rep_uint8 ?x) = ?x

goal (1 subgoal):
 1. Rep_bytes (bytes_takefill b n bs) = takefill b n (Rep_bytes bs)
[PROOF STEP]
by simp


[STATEMENT]
lemma bytes_replicate_rep_eq[code abstract]:
  "Rep_bytes (bytes_replicate n b) = replicate n b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_bytes (bytes_replicate n b) = replicate n b
[PROOF STEP]
using bytes_replicate.rep_eq Rep_uint8_inverse
[PROOF STATE]
proof (prove)
using this:
Rep_bytes (bytes_replicate ?x ?xa) = replicate ?x (Abs_uint8 (Rep_uint8 ?xa))
Abs_uint8 (Rep_uint8 ?x) = ?x

goal (1 subgoal):
 1. Rep_bytes (bytes_replicate n b) = replicate n b
[PROOF STEP]
by simp


[STATEMENT]
lemma extended_simps [simp]:
  "(\<turnstile> < x) = (x \<noteq> \<turnstile>)"
  "(\<lbrakk>x'\<rbrakk> < \<lbrakk>y'\<rbrakk>) = (x' < y')"
  "\<lbrakk>x'\<rbrakk> < \<stileturn>"
  "\<not>(\<lbrakk>x'\<rbrakk> < \<turnstile>)"
  "\<not>(\<stileturn> < x)"
  "\<turnstile> \<le> x"
  "(\<lbrakk>x'\<rbrakk> \<le> \<lbrakk>y'\<rbrakk>) = ((x' :: '\<I> :: linorder) \<le> y')"
  "x \<le> \<stileturn>"
  "\<not>(\<lbrakk>x'\<rbrakk> \<le> \<turnstile>)"
  "(\<stileturn> \<le> x) = (x = \<stileturn>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (((\<turnstile> < x) = (x \<noteq> \<turnstile>) &&& (\<lbrakk>x'\<rbrakk> < \<lbrakk>y'\<rbrakk>) = (x' < y')) &&& \<lbrakk>x'\<rbrakk> < \<stileturn> &&& \<not> \<lbrakk>x'\<rbrakk> < \<turnstile> &&& \<not> \<stileturn> < x) &&& (\<turnstile> \<le> x &&& (\<lbrakk>x'\<rbrakk> \<le> \<lbrakk>y'\<rbrakk>) = (x' \<le> y')) &&& x \<le> \<stileturn> &&& \<not> \<lbrakk>x'\<rbrakk> \<le> \<turnstile> &&& (\<stileturn> \<le> x) = (x = \<stileturn>)
[PROOF STEP]
by (case_tac [!] x, simp_all add:less_extended_def less_eq_extended_def le_less)


[STATEMENT]
lemma position_cases:
  assumes "\<And> y z. x = \<lbrakk>NonFinal (y,Left) z\<rbrakk> \<Longrightarrow> p"
  assumes "\<And> y z. x = \<lbrakk>NonFinal (y,Right) z\<rbrakk> \<Longrightarrow> p"
  assumes "\<And> y. x = \<lbrakk>Final y\<rbrakk> \<Longrightarrow> p"
  assumes "x = \<turnstile> \<Longrightarrow> p"
  assumes "x = \<stileturn> \<Longrightarrow> p"
  shows "p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p
[PROOF STEP]
by (metis assms embed_dir.cases extended_size.cases sort_key_embedding.cases)


[STATEMENT]
lemma derive_pos_mono: "x \<le> y \<Longrightarrow> derive_pos h x \<le> derive_pos h y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> derive_pos h x \<le> derive_pos h y
[PROOF STEP]
apply (cases h, cases "snd h")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 2. \<And>a b. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Right\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
[PROOF STEP]
apply (rule_tac [!] position_cases [where x=x])
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>a b ya z. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<lbrakk>NonFinal (ya, sort_dir.Left) z\<rbrakk>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 2. \<And>a b ya z. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<lbrakk>NonFinal (ya, sort_dir.Right) z\<rbrakk>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 3. \<And>a b ya. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<lbrakk>Final ya\<rbrakk>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 4. \<And>a b. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<turnstile>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 5. \<And>a b. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<stileturn>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 6. \<And>a b ya z. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Right; x = \<lbrakk>NonFinal (ya, sort_dir.Left) z\<rbrakk>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 7. \<And>a b ya z. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Right; x = \<lbrakk>NonFinal (ya, sort_dir.Right) z\<rbrakk>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 8. \<And>a b ya. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Right; x = \<lbrakk>Final ya\<rbrakk>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 9. \<And>a b. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Right; x = \<turnstile>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 10. \<And>a b. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Right; x = \<stileturn>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
[PROOF STEP]
apply (rule_tac [!] position_cases [where x=y])
[PROOF STATE]
proof (prove)
goal (50 subgoals):
 1. \<And>a b ya z yaa za. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<lbrakk>NonFinal (ya, sort_dir.Left) z\<rbrakk>; y = \<lbrakk>NonFinal (yaa, sort_dir.Left) za\<rbrakk>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 2. \<And>a b ya z yaa za. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<lbrakk>NonFinal (ya, sort_dir.Left) z\<rbrakk>; y = \<lbrakk>NonFinal (yaa, sort_dir.Right) za\<rbrakk>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 3. \<And>a b ya z yaa. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<lbrakk>NonFinal (ya, sort_dir.Left) z\<rbrakk>; y = \<lbrakk>Final yaa\<rbrakk>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 4. \<And>a b ya z. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<lbrakk>NonFinal (ya, sort_dir.Left) z\<rbrakk>; y = \<turnstile>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 5. \<And>a b ya z. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<lbrakk>NonFinal (ya, sort_dir.Left) z\<rbrakk>; y = \<stileturn>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 6. \<And>a b ya z yaa za. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<lbrakk>NonFinal (ya, sort_dir.Right) z\<rbrakk>; y = \<lbrakk>NonFinal (yaa, sort_dir.Left) za\<rbrakk>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 7. \<And>a b ya z yaa za. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<lbrakk>NonFinal (ya, sort_dir.Right) z\<rbrakk>; y = \<lbrakk>NonFinal (yaa, sort_dir.Right) za\<rbrakk>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 8. \<And>a b ya z yaa. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<lbrakk>NonFinal (ya, sort_dir.Right) z\<rbrakk>; y = \<lbrakk>Final yaa\<rbrakk>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 9. \<And>a b ya z. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<lbrakk>NonFinal (ya, sort_dir.Right) z\<rbrakk>; y = \<turnstile>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
 10. \<And>a b ya z. \<lbrakk>x \<le> y; h = (a, b); snd h = sort_dir.Left; x = \<lbrakk>NonFinal (ya, sort_dir.Right) z\<rbrakk>; y = \<stileturn>\<rbrakk> \<Longrightarrow> derive_pos h x \<le> derive_pos h y
A total of 50 subgoals...
[PROOF STEP]
by (simp_all, auto)


[STATEMENT]
lemma derive_size:
  "\<lbrakk>Final i\<rbrakk> \<le> fst x \<and> is_interval x \<Longrightarrow> int_size (derive_left x) < int_size x"
  "snd x \<le> \<lbrakk>Final i\<rbrakk> \<and> is_interval x \<Longrightarrow> int_size (derive_right x) < int_size x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>Final i\<rbrakk> \<le> fst x \<and> is_interval x \<Longrightarrow> int_size (derive_left x) < int_size x) &&& (snd x \<le> \<lbrakk>Final i\<rbrakk> \<and> is_interval x \<Longrightarrow> int_size (derive_right x) < int_size x)
[PROOF STEP]
by (interval_split x, simp_all add:less_SucI)


[STATEMENT]
lemma derive_interval:
  "\<lbrakk>Final i\<rbrakk> \<le> fst x \<Longrightarrow> is_interval x \<Longrightarrow> is_interval (derive_left x)"
  "snd x \<le> \<lbrakk>Final i\<rbrakk> \<Longrightarrow> is_interval x \<Longrightarrow> is_interval (derive_right x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<lbrakk>Final i\<rbrakk> \<le> fst x; is_interval x\<rbrakk> \<Longrightarrow> is_interval (derive_left x)) &&& (\<lbrakk>snd x \<le> \<lbrakk>Final i\<rbrakk>; is_interval x\<rbrakk> \<Longrightarrow> is_interval (derive_right x))
[PROOF STEP]
by (interval_split x, simp_all, auto)


[STATEMENT]
lemma poly_diff_val:
  assumes "f \<in> carrier Zp_x"
  assumes "a \<in> carrier Zp"
  assumes "b \<in> carrier Zp"
  shows "val_Zp (f\<bullet>a \<ominus> f\<bullet>b) \<ge> val_Zp (a \<ominus> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (a \<ominus> b) \<le> val_Zp (f \<bullet> a \<ominus> f \<bullet> b)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (a \<ominus> b) \<le> val_Zp (f \<bullet> a \<ominus> f \<bullet> b)
[PROOF STEP]
obtain c where c_def: "c \<in> carrier Zp \<and> (f\<bullet>a \<ominus> f\<bullet>b) = (a \<ominus> b) \<otimes> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>c. c \<in> carrier Zp \<and> f \<bullet> a \<ominus> f \<bullet> b = (a \<ominus> b) \<otimes> c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f \<in> carrier (UP Zp)
a \<in> carrier Zp
b \<in> carrier Zp

goal (1 subgoal):
 1. (\<And>c. c \<in> carrier Zp \<and> f \<bullet> a \<ominus> f \<bullet> b = (a \<ominus> b) \<otimes> c \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (meson to_fun_diff_factor)
[PROOF STATE]
proof (state)
this:
c \<in> carrier Zp \<and> f \<bullet> a \<ominus> f \<bullet> b = (a \<ominus> b) \<otimes> c

goal (1 subgoal):
 1. val_Zp (a \<ominus> b) \<le> val_Zp (f \<bullet> a \<ominus> f \<bullet> b)
[PROOF STEP]
have 1: "val_Zp c \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> val_Zp c
[PROOF STEP]
using c_def val_pos
[PROOF STATE]
proof (prove)
using this:
c \<in> carrier Zp \<and> f \<bullet> a \<ominus> f \<bullet> b = (a \<ominus> b) \<otimes> c
?x \<in> carrier Zp \<Longrightarrow> 0 \<le> val_Zp ?x

goal (1 subgoal):
 1. 0 \<le> val_Zp c
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
0 \<le> val_Zp c

goal (1 subgoal):
 1. val_Zp (a \<ominus> b) \<le> val_Zp (f \<bullet> a \<ominus> f \<bullet> b)
[PROOF STEP]
have 2: "val_Zp (f\<bullet>a \<ominus> f\<bullet>b) = val_Zp (a \<ominus> b) + (val_Zp c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f \<bullet> a \<ominus> f \<bullet> b) = val_Zp (a \<ominus> b) + val_Zp c
[PROOF STEP]
using c_def val_Zp_mult
[PROOF STATE]
proof (prove)
using this:
c \<in> carrier Zp \<and> f \<bullet> a \<ominus> f \<bullet> b = (a \<ominus> b) \<otimes> c
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> val_Zp (?x \<otimes> ?y) = val_Zp ?x + val_Zp ?y

goal (1 subgoal):
 1. val_Zp (f \<bullet> a \<ominus> f \<bullet> b) = val_Zp (a \<ominus> b) + val_Zp c
[PROOF STEP]
by (simp add: assms(2) assms(3))
[PROOF STATE]
proof (state)
this:
val_Zp (f \<bullet> a \<ominus> f \<bullet> b) = val_Zp (a \<ominus> b) + val_Zp c

goal (1 subgoal):
 1. val_Zp (a \<ominus> b) \<le> val_Zp (f \<bullet> a \<ominus> f \<bullet> b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
val_Zp (f \<bullet> a \<ominus> f \<bullet> b) = val_Zp (a \<ominus> b) + val_Zp c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> a \<ominus> f \<bullet> b) = val_Zp (a \<ominus> b) + val_Zp c

goal (1 subgoal):
 1. val_Zp (a \<ominus> b) \<le> val_Zp (f \<bullet> a \<ominus> f \<bullet> b)
[PROOF STEP]
using "1"
[PROOF STATE]
proof (prove)
using this:
val_Zp (f \<bullet> a \<ominus> f \<bullet> b) = val_Zp (a \<ominus> b) + val_Zp c
0 \<le> val_Zp c

goal (1 subgoal):
 1. val_Zp (a \<ominus> b) \<le> val_Zp (f \<bullet> a \<ominus> f \<bullet> b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
val_Zp (a \<ominus> b) \<le> val_Zp (f \<bullet> a \<ominus> f \<bullet> b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma divide_closed:
  assumes "x \<in> carrier Zp"
  assumes "y \<in> carrier Zp"
  assumes "y \<noteq> \<zero>"
  shows "divide x y \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide x y \<in> carrier Zp
[PROOF STEP]
unfolding divide_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if x = \<zero> then \<zero> else [p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x \<otimes> inv ac_Zp y) \<in> carrier Zp
[PROOF STEP]
apply(cases "x = \<zero>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x = \<zero> \<Longrightarrow> (if x = \<zero> then \<zero> else [p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x \<otimes> inv ac_Zp y) \<in> carrier Zp
 2. x \<noteq> \<zero> \<Longrightarrow> (if x = \<zero> then \<zero> else [p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x \<otimes> inv ac_Zp y) \<in> carrier Zp
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> \<zero> \<Longrightarrow> (if x = \<zero> then \<zero> else [p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x \<otimes> inv ac_Zp y) \<in> carrier Zp
[PROOF STEP]
using assms ac_Zp_is_Unit
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier Zp
y \<in> carrier Zp
y \<noteq> \<zero>
\<lbrakk>?x \<in> carrier Zp; ?x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ac_Zp ?x \<in> Units Zp

goal (1 subgoal):
 1. x \<noteq> \<zero> \<Longrightarrow> (if x = \<zero> then \<zero> else [p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x \<otimes> inv ac_Zp y) \<in> carrier Zp
[PROOF STEP]
by (simp add: ac_Zp_in_Zp)


[STATEMENT]
lemma divide_formula:
  assumes "x \<in> carrier Zp"
  assumes "y \<in> carrier Zp"
  assumes "y \<noteq> \<zero>"
  assumes "val_Zp x \<ge> val_Zp y"
  shows "y \<otimes> divide x y = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<otimes> local.divide x y = x
[PROOF STEP]
apply(cases "x = \<zero>")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x = \<zero> \<Longrightarrow> y \<otimes> local.divide x y = x
 2. x \<noteq> \<zero> \<Longrightarrow> y \<otimes> local.divide x y = x
[PROOF STEP]
apply (simp add: divide_def mult_zero_l)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> \<zero> \<Longrightarrow> y \<otimes> local.divide x y = x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> \<zero> \<Longrightarrow> y \<otimes> local.divide x y = x
[PROOF STEP]
assume A: "x \<noteq> \<zero>"
[PROOF STATE]
proof (state)
this:
x \<noteq> \<zero>

goal (1 subgoal):
 1. x \<noteq> \<zero> \<Longrightarrow> y \<otimes> local.divide x y = x
[PROOF STEP]
have 0: "y \<otimes> divide x y = \<p>[^] nat (ord_Zp y) \<otimes> ac_Zp y \<otimes> (\<p>[^](nat (ord_Zp x - ord_Zp y)) \<otimes> ac_Zp x \<otimes> (inv ac_Zp y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<otimes> local.divide x y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> ac_Zp y \<otimes> ([p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x \<otimes> inv ac_Zp y)
[PROOF STEP]
using assms ac_Zp_factors_x[of x] ac_Zp_factors_x[of y] A divide_def
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier Zp
y \<in> carrier Zp
y \<noteq> \<zero>
val_Zp y \<le> val_Zp x
\<lbrakk>x \<in> carrier Zp; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x = [p] \<cdot> \<one> [^] nat (ord_Zp x) \<otimes> ac_Zp x
\<lbrakk>x \<in> carrier Zp; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> x = [p] \<cdot> \<one> [^] ord_Zp x \<otimes> ac_Zp x
\<lbrakk>y \<in> carrier Zp; y \<noteq> \<zero>\<rbrakk> \<Longrightarrow> y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> ac_Zp y
\<lbrakk>y \<in> carrier Zp; y \<noteq> \<zero>\<rbrakk> \<Longrightarrow> y = [p] \<cdot> \<one> [^] ord_Zp y \<otimes> ac_Zp y
x \<noteq> \<zero>
local.divide ?x ?y = (if ?x = \<zero> then \<zero> else [p] \<cdot> \<one> [^] nat (ord_Zp ?x - ord_Zp ?y) \<otimes> ac_Zp ?x \<otimes> inv ac_Zp ?y)

goal (1 subgoal):
 1. y \<otimes> local.divide x y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> ac_Zp y \<otimes> ([p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x \<otimes> inv ac_Zp y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<otimes> local.divide x y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> ac_Zp y \<otimes> ([p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x \<otimes> inv ac_Zp y)

goal (1 subgoal):
 1. x \<noteq> \<zero> \<Longrightarrow> y \<otimes> local.divide x y = x
[PROOF STEP]
hence  1: "y \<otimes> divide x y = \<p>[^] nat (ord_Zp  y) \<otimes> (\<p>[^](nat (ord_Zp  x - ord_Zp  y)) \<otimes>  ac_Zp x \<otimes> ac_Zp y \<otimes>  (inv ac_Zp y))"
[PROOF STATE]
proof (prove)
using this:
y \<otimes> local.divide x y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> ac_Zp y \<otimes> ([p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x \<otimes> inv ac_Zp y)

goal (1 subgoal):
 1. y \<otimes> local.divide x y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> ([p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x \<otimes> ac_Zp y \<otimes> inv ac_Zp y)
[PROOF STEP]
using mult_assoc mult_comm
[PROOF STATE]
proof (prove)
using this:
y \<otimes> local.divide x y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> ac_Zp y \<otimes> ([p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x \<otimes> inv ac_Zp y)
?a \<otimes> ?b \<otimes> ?c = ?a \<otimes> (?b \<otimes> ?c)
?a \<otimes> ?b = ?b \<otimes> ?a

goal (1 subgoal):
 1. y \<otimes> local.divide x y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> ([p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x \<otimes> ac_Zp y \<otimes> inv ac_Zp y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<otimes> local.divide x y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> ([p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x \<otimes> ac_Zp y \<otimes> inv ac_Zp y)

goal (1 subgoal):
 1. x \<noteq> \<zero> \<Longrightarrow> y \<otimes> local.divide x y = x
[PROOF STEP]
have 2: "(nat (ord_Zp  y) + nat (ord_Zp  x - ord_Zp  y)) = nat (ord_Zp  x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat (ord_Zp y) + nat (ord_Zp x - ord_Zp y) = nat (ord_Zp x)
[PROOF STEP]
using assms ord_pos[of x] ord_pos[of y] A val_ord_Zp
[PROOF STATE]
proof (prove)
using this:
x \<in> carrier Zp
y \<in> carrier Zp
y \<noteq> \<zero>
val_Zp y \<le> val_Zp x
\<lbrakk>x \<in> carrier Zp; x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 0 \<le> ord_Zp x
\<lbrakk>y \<in> carrier Zp; y \<noteq> \<zero>\<rbrakk> \<Longrightarrow> 0 \<le> ord_Zp y
x \<noteq> \<zero>
?a \<noteq> \<zero> \<Longrightarrow> val_Zp ?a = eint (ord_Zp ?a)

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

goal (1 subgoal):
 1. x \<noteq> \<zero> \<Longrightarrow> y \<otimes> local.divide x y = x
[PROOF STEP]
have "y \<otimes> divide x y = \<p>[^] nat (ord_Zp  y) \<otimes> \<p>[^](nat (ord_Zp  x - ord_Zp  y)) \<otimes>  ac_Zp x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<otimes> local.divide x y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> [p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x
[PROOF STEP]
using 1 A assms
[PROOF STATE]
proof (prove)
using this:
y \<otimes> local.divide x y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> ([p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x \<otimes> ac_Zp y \<otimes> inv ac_Zp y)
x \<noteq> \<zero>
x \<in> carrier Zp
y \<in> carrier Zp
y \<noteq> \<zero>
val_Zp y \<le> val_Zp x

goal (1 subgoal):
 1. y \<otimes> local.divide x y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> [p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x
[PROOF STEP]
by (simp add: ac_Zp_in_Zp ac_Zp_is_Unit mult_assoc)
[PROOF STATE]
proof (state)
this:
y \<otimes> local.divide x y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> [p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x

goal (1 subgoal):
 1. x \<noteq> \<zero> \<Longrightarrow> y \<otimes> local.divide x y = x
[PROOF STEP]
thus "y \<otimes> divide x y = x"
[PROOF STATE]
proof (prove)
using this:
y \<otimes> local.divide x y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> [p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x

goal (1 subgoal):
 1. y \<otimes> local.divide x y = x
[PROOF STEP]
using "2" A ac_Zp_factors_x(1) assms(1) p_natpow_prod
[PROOF STATE]
proof (prove)
using this:
y \<otimes> local.divide x y = [p] \<cdot> \<one> [^] nat (ord_Zp y) \<otimes> [p] \<cdot> \<one> [^] nat (ord_Zp x - ord_Zp y) \<otimes> ac_Zp x
nat (ord_Zp y) + nat (ord_Zp x - ord_Zp y) = nat (ord_Zp x)
x \<noteq> \<zero>
\<lbrakk>?x \<in> carrier Zp; ?x \<noteq> \<zero>\<rbrakk> \<Longrightarrow> ?x = [p] \<cdot> \<one> [^] nat (ord_Zp ?x) \<otimes> ac_Zp ?x
x \<in> carrier Zp
[p] \<cdot> \<one> [^] ?n \<otimes> [p] \<cdot> \<one> [^] ?m = [p] \<cdot> \<one> [^] (?n + ?m)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma divide_nonzero:
  assumes "x \<in> nonzero Zp"
  assumes "y \<in> nonzero Zp"
  assumes "val_Zp x \<ge> val_Zp y"
  shows "divide x y \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide x y \<in> nonzero Zp
[PROOF STEP]
by (metis assms(1) assms(2) assms(3) divide_closed divide_formula mult_zero_l nonzero_closed nonzero_memE(2) nonzero_memI)


[STATEMENT]
lemma val_of_divide:
  assumes "x \<in> carrier Zp"
  assumes "y \<in> nonzero Zp"
  assumes "val_Zp x \<ge> val_Zp y"
  shows "val_Zp (divide x y) = val_Zp x - val_Zp y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (local.divide x y) = val_Zp x - val_Zp y
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. val_Zp (local.divide x y) = val_Zp x - val_Zp y
[PROOF STEP]
have 0: "y \<otimes> divide x y = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<otimes> local.divide x y = x
[PROOF STEP]
by (simp add: assms(1) assms(2) assms(3) divide_formula nonzero_closed nonzero_memE(2))
[PROOF STATE]
proof (state)
this:
y \<otimes> local.divide x y = x

goal (1 subgoal):
 1. val_Zp (local.divide x y) = val_Zp x - val_Zp y
[PROOF STEP]
hence "val_Zp y + val_Zp (divide x y) = val_Zp x"
[PROOF STATE]
proof (prove)
using this:
y \<otimes> local.divide x y = x

goal (1 subgoal):
 1. val_Zp y + val_Zp (local.divide x y) = val_Zp x
[PROOF STEP]
using assms(1) assms(2) divide_closed nonzero_closed not_nonzero_memI val_Zp_mult
[PROOF STATE]
proof (prove)
using this:
y \<otimes> local.divide x y = x
x \<in> carrier Zp
y \<in> nonzero Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?y \<noteq> \<zero>\<rbrakk> \<Longrightarrow> local.divide ?x ?y \<in> carrier Zp
?a \<in> nonzero Zp \<Longrightarrow> ?a \<in> carrier Zp
?a = \<zero> \<Longrightarrow> ?a \<notin> nonzero Zp
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp\<rbrakk> \<Longrightarrow> val_Zp (?x \<otimes> ?y) = val_Zp ?x + val_Zp ?y

goal (1 subgoal):
 1. val_Zp y + val_Zp (local.divide x y) = val_Zp x
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
val_Zp y + val_Zp (local.divide x y) = val_Zp x

goal (1 subgoal):
 1. val_Zp (local.divide x y) = val_Zp x - val_Zp y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
val_Zp y + val_Zp (local.divide x y) = val_Zp x

goal (1 subgoal):
 1. val_Zp (local.divide x y) = val_Zp x - val_Zp y
[PROOF STEP]
by (smt Zp_def add.commute add.left_neutral add.right_neutral add_diff_assoc_eint assms(1)
        assms(2) divide_nonzero eSuc_minus_eSuc iadd_Suc idiff_0_right mult_zero(1) mult_zero_l
        nonzero_closed ord_pos order_refl padic_integers.Zp_int_inc_closed padic_integers.mult_comm
        padic_integers.ord_of_nonzero(2) padic_integers_axioms val_Zp_eq_frac_0 val_Zp_mult val_Zp_p)
[PROOF STATE]
proof (state)
this:
val_Zp (local.divide x y) = val_Zp x - val_Zp y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma val_of_divide':
  assumes "x \<in> carrier Zp"
  assumes "y \<in> carrier  Zp"
  assumes "y \<noteq> \<zero>"
  assumes "val_Zp x \<ge> val_Zp y"
  shows "val_Zp (divide x y) = val_Zp x - val_Zp y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (local.divide x y) = val_Zp x - val_Zp y
[PROOF STEP]
using Zp_def assms(1) assms(2) assms(3) assms(4) padic_integers.not_nonzero_Zp
    padic_integers.val_of_divide padic_integers_axioms
[PROOF STATE]
proof (prove)
using this:
Zp \<equiv> padic_int p
x \<in> carrier Zp
y \<in> carrier Zp
y \<noteq> \<zero>
val_Zp y \<le> val_Zp x
\<lbrakk>padic_integers ?p; ?x \<in> carrier (padic_int ?p); ?x \<notin> nonzero (padic_int ?p)\<rbrakk> \<Longrightarrow> ?x = \<zero>\<^bsub>padic_int ?p\<^esub>
\<lbrakk>padic_integers ?p; ?x \<in> carrier (padic_int ?p); ?y \<in> nonzero (padic_int ?p); padic_integers.val_Zp ?p ?y \<le> padic_integers.val_Zp ?p ?x\<rbrakk> \<Longrightarrow> padic_integers.val_Zp ?p (padic_integers.divide ?p ?x ?y) = padic_integers.val_Zp ?p ?x - padic_integers.val_Zp ?p ?y
padic_integers p

goal (1 subgoal):
 1. val_Zp (local.divide x y) = val_Zp x - val_Zp y
[PROOF STEP]
by blast


[STATEMENT]
lemma f'_closed:
"f' \<in> carrier Zp_x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<in> carrier (UP Zp)
[PROOF STEP]
using f_closed pderiv_closed
[PROOF STATE]
proof (prove)
using this:
f \<in> carrier (UP Zp)
?p \<in> carrier (UP Zp) \<Longrightarrow> pderiv ?p \<in> carrier (UP Zp)

goal (1 subgoal):
 1. f' \<in> carrier (UP Zp)
[PROOF STEP]
by blast


[STATEMENT]
lemma f'_vals_closed:
  assumes "a \<in> carrier Zp"
  shows "f'\<bullet>a \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> a \<in> carrier Zp
[PROOF STEP]
by (simp add: UP_cring.to_fun_closed Zp_x_is_UP_cring f'_closed)


[STATEMENT]
lemma fa_closed:
"(f\<bullet>a) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> a \<in> carrier Zp
[PROOF STEP]
by (simp add: UP_cring.to_fun_closed Zp_x_is_UP_cring)


[STATEMENT]
lemma f'a_closed:
"(f'\<bullet>a) \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> a \<in> carrier Zp
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f' \<bullet> a \<in> carrier Zp
[PROOF STEP]
have "f' \<in> carrier Zp_x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<in> carrier (UP Zp)
[PROOF STEP]
by (simp add: f'_closed)
[PROOF STATE]
proof (state)
this:
f' \<in> carrier (UP Zp)

goal (1 subgoal):
 1. f' \<bullet> a \<in> carrier Zp
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f' \<in> carrier (UP Zp)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f' \<in> carrier (UP Zp)

goal (1 subgoal):
 1. f' \<bullet> a \<in> carrier Zp
[PROOF STEP]
by (simp add: f'_vals_closed)
[PROOF STATE]
proof (state)
this:
f' \<bullet> a \<in> carrier Zp

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fa_nonzero':
"(f\<bullet>a) \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<bullet> a \<in> nonzero Zp
[PROOF STEP]
using fa_closed fa_nonzero not_nonzero_Zp
[PROOF STATE]
proof (prove)
using this:
f \<bullet> a \<in> carrier Zp
f \<bullet> a \<noteq> \<zero>
\<lbrakk>?x \<in> carrier Zp; ?x \<notin> nonzero Zp\<rbrakk> \<Longrightarrow> ?x = \<zero>

goal (1 subgoal):
 1. f \<bullet> a \<in> nonzero Zp
[PROOF STEP]
by blast


[STATEMENT]
lemma f'a_nonzero[simp]:
"(f'\<bullet>a) \<noteq> \<zero>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> a \<noteq> \<zero>
[PROOF STEP]
proof(rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> f' \<bullet> a \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (f'\<bullet>a) \<noteq> \<zero>"
[PROOF STATE]
proof (state)
this:
\<not> f' \<bullet> a \<noteq> \<zero>

goal (1 subgoal):
 1. \<not> f' \<bullet> a \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> f' \<bullet> a \<noteq> \<zero>
[PROOF STEP]
have "(f'\<bullet>a) = \<zero>"
[PROOF STATE]
proof (prove)
using this:
\<not> f' \<bullet> a \<noteq> \<zero>

goal (1 subgoal):
 1. f' \<bullet> a = \<zero>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f' \<bullet> a = \<zero>

goal (1 subgoal):
 1. \<not> f' \<bullet> a \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f' \<bullet> a = \<zero>
[PROOF STEP]
have "\<infinity> < val_Zp (f\<bullet>a)"
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> a = \<zero>

goal (1 subgoal):
 1. \<infinity> < val_Zp (f \<bullet> a)
[PROOF STEP]
using hensel_hypothesis
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> a = \<zero>
eint 2 * val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)

goal (1 subgoal):
 1. \<infinity> < val_Zp (f \<bullet> a)
[PROOF STEP]
by (simp add: val_Zp_def)
[PROOF STATE]
proof (state)
this:
\<infinity> < val_Zp (f \<bullet> a)

goal (1 subgoal):
 1. \<not> f' \<bullet> a \<noteq> \<zero> \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
\<infinity> < val_Zp (f \<bullet> a)

goal (1 subgoal):
 1. False
[PROOF STEP]
using eint_ord_simps(6)
[PROOF STATE]
proof (prove)
using this:
\<infinity> < val_Zp (f \<bullet> a)
(\<infinity> < ?q) = False

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma f'a_nonzero':
"(f'\<bullet>a) \<in> nonzero Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f' \<bullet> a \<in> nonzero Zp
[PROOF STEP]
using f'a_closed f'a_nonzero not_nonzero_Zp
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> a \<in> carrier Zp
f' \<bullet> a \<noteq> \<zero>
\<lbrakk>?x \<in> carrier Zp; ?x \<notin> nonzero Zp\<rbrakk> \<Longrightarrow> ?x = \<zero>

goal (1 subgoal):
 1. f' \<bullet> a \<in> nonzero Zp
[PROOF STEP]
by blast


[STATEMENT]
lemma f'a_not_infinite[simp]:
"val_Zp (f'\<bullet>a) \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. val_Zp (f' \<bullet> a) \<noteq> \<infinity>
[PROOF STEP]
by (metis eint_ord_code(3) hensel_hypothesis linorder_not_less times_eint_simps(4))


[STATEMENT]
lemma f'a_nonneg_val[simp]:
"val_Zp ((f'\<bullet>a)) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> val_Zp (f' \<bullet> a)
[PROOF STEP]
using f'a_closed val_pos
[PROOF STATE]
proof (prove)
using this:
f' \<bullet> a \<in> carrier Zp
?x \<in> carrier Zp \<Longrightarrow> 0 \<le> val_Zp ?x

goal (1 subgoal):
 1. 0 \<le> val_Zp (f' \<bullet> a)
[PROOF STEP]
by blast


[STATEMENT]
lemma newton_step_closed:
  "newton_step a \<in> carrier Zp"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. newton_step a \<in> carrier Zp
[PROOF STEP]
using  divide_closed
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?y \<noteq> \<zero>\<rbrakk> \<Longrightarrow> local.divide ?x ?y \<in> carrier Zp

goal (1 subgoal):
 1. newton_step a \<in> carrier Zp
[PROOF STEP]
unfolding newton_step_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?y \<noteq> \<zero>\<rbrakk> \<Longrightarrow> local.divide ?x ?y \<in> carrier Zp

goal (1 subgoal):
 1. a \<ominus> local.divide (f \<bullet> a) (f' \<bullet> a) \<in> carrier Zp
[PROOF STEP]
using f'a_closed f'a_nonzero fa_closed local.a_closed
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?y \<noteq> \<zero>\<rbrakk> \<Longrightarrow> local.divide ?x ?y \<in> carrier Zp
f' \<bullet> a \<in> carrier Zp
f' \<bullet> a \<noteq> \<zero>
f \<bullet> a \<in> carrier Zp
a \<in> carrier Zp

goal (1 subgoal):
 1. a \<ominus> local.divide (f \<bullet> a) (f' \<bullet> a) \<in> carrier Zp
[PROOF STEP]
by blast


[STATEMENT]
lemma hensel_factor_id:
"(divide (f\<bullet>a) (f'\<bullet>a)) \<otimes> ((f'\<bullet>a)) = (f\<bullet>a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.divide (f \<bullet> a) (f' \<bullet> a) \<otimes> (f' \<bullet> a) = f \<bullet> a
[PROOF STEP]
using hensel_hypothesis hensel_axioms divide_formula f'a_closed
        fa_closed hensel_hypothesis_weakened mult_comm
[PROOF STATE]
proof (prove)
using this:
eint 2 * val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)
hensel p f a
\<lbrakk>?x \<in> carrier Zp; ?y \<in> carrier Zp; ?y \<noteq> \<zero>; val_Zp ?y \<le> val_Zp ?x\<rbrakk> \<Longrightarrow> ?y \<otimes> local.divide ?x ?y = ?x
f' \<bullet> a \<in> carrier Zp
f \<bullet> a \<in> carrier Zp
val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)
?a \<otimes> ?b = ?b \<otimes> ?a

goal (1 subgoal):
 1. local.divide (f \<bullet> a) (f' \<bullet> a) \<otimes> (f' \<bullet> a) = f \<bullet> a
[PROOF STEP]
by auto


[STATEMENT]
lemma t_pos[simp]:
"t > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < t
[PROOF STEP]
using hensel_factor_def hensel_hypothesis
[PROOF STATE]
proof (prove)
using this:
t = val_Zp (f \<bullet> a) - eint 2 * val_Zp (f' \<bullet> a)
eint 2 * val_Zp (f' \<bullet> a) < val_Zp (f \<bullet> a)

goal (1 subgoal):
 1. 0 < t
[PROOF STEP]
by (simp add: eint_minus_le)


[STATEMENT]
lemma t_neq_infty[simp]:
"t \<noteq> \<infinity>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<noteq> \<infinity>
[PROOF STEP]
by (simp add: hensel_factor_def val_Zp_def)


[STATEMENT]
lemma t_times_pow_pos[simp]:
"(2^(n::nat))*t > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < eint (2 ^ n) * t
[PROOF STEP]
apply(cases "n = 0")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> 0 < eint (2 ^ n) * t
 2. n \<noteq> 0 \<Longrightarrow> 0 < eint (2 ^ n) * t
[PROOF STEP]
using one_eint_def
[PROOF STATE]
proof (prove)
using this:
1 = eint 1

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> 0 < eint (2 ^ n) * t
 2. n \<noteq> 0 \<Longrightarrow> 0 < eint (2 ^ n) * t
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> 0 < eint (2 ^ n) * t
[PROOF STEP]
using eint_mult_mono'[of t 1 "2^n"] t_pos
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> t \<and> t \<noteq> \<infinity>; 1 < eint (2 ^ n)\<rbrakk> \<Longrightarrow> 1 * t \<le> eint (2 ^ n) * t
0 < t

goal (1 subgoal):
 1. n \<noteq> 0 \<Longrightarrow> 0 < eint (2 ^ n) * t
[PROOF STEP]
by (smt eint_ord_simps(2) linorder_not_less mult_one_left neq0_conv one_eint_def order_less_le order_trans self_le_power t_neq_infty)