[STATEMENT]
lemma (in list_alloc)
  shows
  "\<Gamma>,\<Theta>\<turnstile> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and>
       set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>
  WHILE \<acute>p \<noteq> Null
  INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next  ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and>
               rev ps @ qs = rev Ps @ Qs \<and>
               set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace>
  DO \<acute>r :== \<acute>p;;
     \<lbrace>\<acute>p\<noteq>Null \<and> \<acute>p\<in>set \<acute>alloc\<rbrace>\<longmapsto> \<acute>p :== \<acute>p\<rightarrow> \<acute>next;;
     \<lbrace>\<acute>r\<noteq>Null \<and> \<acute>r\<in>set \<acute>alloc\<rbrace>\<longmapsto> \<acute>r\<rightarrow>\<acute>next :== \<acute>q;;
     \<acute>q :== \<acute>r OD
 \<lbrace>List \<acute>q \<acute>next (rev Ps @ Qs) \<and> set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> \<lbrace>List \<acute>p \<acute>next Ps \<and> List \<acute>q \<acute>next Qs \<and> set Ps \<inter> set Qs = {} \<and> set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace> WHILE \<acute>p \<noteq> Null INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace> DO \<acute>r :== \<acute>p;; (False, \<lbrace>\<acute>p \<noteq> Null \<and> \<acute>p \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; (False, \<lbrace>\<acute>r \<noteq> Null \<and> \<acute>r \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>r\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>r OD \<lbrace>List \<acute>q \<acute>next (rev Ps @ Qs) \<and> set Ps \<subseteq> set \<acute>alloc \<and> set Qs \<subseteq> set \<acute>alloc\<rbrace>
[PROOF STEP]
apply (rule CombineStrip' [OF rev_moduloGuards rev_noFault])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. WHILE \<acute>p \<noteq> Null INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace> DO \<acute>r :== \<acute>p;; (False, \<lbrace>\<acute>p \<noteq> Null \<and> \<acute>p \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; (False, \<lbrace>\<acute>r \<noteq> Null \<and> \<acute>r \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>r\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>r OD = mark_guards False (strip_guards (- {True}) (WHILE \<acute>p \<noteq> Null INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace> DO \<acute>r :== \<acute>p;; (True, \<lbrace>\<acute>p \<noteq> Null \<and> \<acute>p \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; (True, \<lbrace>\<acute>r \<noteq> Null \<and> \<acute>r \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>r\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>r OD))
 2. WHILE \<acute>p \<noteq> Null INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace> DO \<acute>r :== \<acute>p;; (False, \<lbrace>\<acute>p \<noteq> Null \<and> \<acute>p \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; (False, \<lbrace>\<acute>r \<noteq> Null \<and> \<acute>r \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>r\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>r OD = mark_guards False (WHILE \<acute>p \<noteq> Null INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace> DO \<acute>r :== \<acute>p;; (True, \<lbrace>\<acute>p \<noteq> Null \<and> \<acute>p \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; (True, \<lbrace>\<acute>r \<noteq> Null \<and> \<acute>r \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>r\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>r OD)
[PROOF STEP]
apply  simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. WHILE \<acute>p \<noteq> Null INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace> DO \<acute>r :== \<acute>p;; (False, \<lbrace>\<acute>p \<noteq> Null \<and> \<acute>p \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; (False, \<lbrace>\<acute>r \<noteq> Null \<and> \<acute>r \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>r\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>r OD = mark_guards False (WHILE \<acute>p \<noteq> Null INV \<lbrace>\<exists>ps qs. List \<acute>p \<acute>next ps \<and> List \<acute>q \<acute>next qs \<and> set ps \<inter> set qs = {} \<and> rev ps @ qs = rev Ps @ Qs \<and> set ps \<subseteq> set \<acute>alloc \<and> set qs \<subseteq> set \<acute>alloc\<rbrace> DO \<acute>r :== \<acute>p;; (True, \<lbrace>\<acute>p \<noteq> Null \<and> \<acute>p \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; (True, \<lbrace>\<acute>r \<noteq> Null \<and> \<acute>r \<in> set \<acute>alloc\<rbrace>)\<longmapsto> \<acute>r\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>r OD)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma neq_dP: "\<lbrakk>p \<noteq> q; Path p h q Ps; distinct Ps\<rbrakk> \<Longrightarrow>
 \<exists>Qs. p\<noteq>Null \<and> Ps = p#Qs \<and> p \<notin> set Qs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<noteq> q; Path p h q Ps; distinct Ps\<rbrakk> \<Longrightarrow> \<exists>Qs. p \<noteq> Null \<and> Ps = p # Qs \<and> p \<notin> set Qs
[PROOF STEP]
by (cases Ps, auto)


[STATEMENT]
lemma (in list_alloc) circular_list_rev_I:
  "\<Gamma>,\<Theta>\<turnstile> \<lbrace>\<acute>root = r \<and>  distPath \<acute>root \<acute>next \<acute>root (r#Ps)\<rbrace>
   \<acute>p :== \<acute>root;; \<acute>q :== \<acute>root\<rightarrow>\<acute>next;;
  WHILE \<acute>q \<noteq> \<acute>root
  INV \<lbrace>\<exists> ps qs. distPath \<acute>p \<acute>next \<acute>root ps  \<and> distPath \<acute>q \<acute>next \<acute>root qs \<and>
             \<acute>root = r \<and> r\<noteq>Null \<and> r \<notin> set Ps  \<and> set ps \<inter> set qs = {} \<and>
             Ps = (rev ps) @ qs \<rbrace>
  DO \<acute>tmp :== \<acute>q;; \<acute>q :== \<acute>q\<rightarrow>\<acute>next;; \<acute>tmp\<rightarrow>\<acute>next :== \<acute>p;; \<acute>p:==\<acute>tmp OD;;
  \<acute>root\<rightarrow>\<acute>next :== \<acute>p
  \<lbrace>\<acute>root = r \<and> distPath \<acute>root \<acute>next \<acute>root (r#rev Ps)\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> \<lbrace>\<acute>root = r \<and> distPath \<acute>root \<acute>next \<acute>root (r # Ps)\<rbrace> \<acute>p :== \<acute>root;; \<acute>q :== \<acute>root\<rightarrow>\<acute>next;; WHILE \<acute>q \<noteq> \<acute>root INV \<lbrace>\<exists>ps qs. distPath \<acute>p \<acute>next \<acute>root ps \<and> distPath \<acute>q \<acute>next \<acute>root qs \<and> \<acute>root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs\<rbrace> DO \<acute>tmp :== \<acute>q;; \<acute>q :== \<acute>q\<rightarrow>\<acute>next;; \<acute>tmp\<rightarrow>\<acute>next :== \<acute>p;; \<acute>p :== \<acute>tmp OD;; \<acute>root\<rightarrow>\<acute>next :== \<acute>p \<lbrace>\<acute>root = r \<and> distPath \<acute>root \<acute>next \<acute>root (r # rev Ps)\<rbrace>
[PROOF STEP]
apply (simp only:distPath_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> \<lbrace>\<acute>root = r \<and> Path \<acute>root \<acute>next \<acute>root (r # Ps) \<and> distinct (r # Ps)\<rbrace> \<acute>p :== \<acute>root;; \<acute>q :== \<acute>root\<rightarrow>\<acute>next;; WHILE \<acute>q \<noteq> \<acute>root INV \<lbrace>\<exists>ps qs. (Path \<acute>p \<acute>next \<acute>root ps \<and> distinct ps) \<and> (Path \<acute>q \<acute>next \<acute>root qs \<and> distinct qs) \<and> \<acute>root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs\<rbrace> DO \<acute>tmp :== \<acute>q;; \<acute>q :== \<acute>q\<rightarrow>\<acute>next;; \<acute>tmp\<rightarrow>\<acute>next :== \<acute>p;; \<acute>p :== \<acute>tmp OD;; \<acute>root\<rightarrow>\<acute>next :== \<acute>p \<lbrace>\<acute>root = r \<and> Path \<acute>root \<acute>next \<acute>root (r # rev Ps) \<and> distinct (r # rev Ps)\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>next root. \<lbrakk>Path root next root (root # Ps); distinct (root # Ps)\<rbrakk> \<Longrightarrow> \<exists>ps qs. Path root next root ps \<and> distinct ps \<and> Path (next root) next root qs \<and> distinct qs \<and> root = root \<and> root \<noteq> Null \<and> root \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs
 2. \<And>next p q root. \<lbrakk>\<exists>ps qs. Path p next root ps \<and> distinct ps \<and> Path q next root qs \<and> distinct qs \<and> root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs; q \<noteq> root\<rbrakk> \<Longrightarrow> \<exists>ps qs. Path q (next(q := p)) root ps \<and> distinct ps \<and> Path (next q) (next(q := p)) root qs \<and> distinct qs \<and> root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs
 3. \<And>next p q root. \<lbrakk>\<exists>ps qs. Path p next root ps \<and> distinct ps \<and> Path q next root qs \<and> distinct qs \<and> root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs; \<not> q \<noteq> root\<rbrakk> \<Longrightarrow> root = r \<and> Path root (next(root := p)) root (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply   (rule_tac x="[]" in exI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>next root. \<lbrakk>Path root next root (root # Ps); distinct (root # Ps)\<rbrakk> \<Longrightarrow> \<exists>qs. Path root next root [] \<and> distinct [] \<and> Path (next root) next root qs \<and> distinct qs \<and> root = root \<and> root \<noteq> Null \<and> root \<notin> set Ps \<and> set [] \<inter> set qs = {} \<and> Ps = rev [] @ qs
 2. \<And>next p q root. \<lbrakk>\<exists>ps qs. Path p next root ps \<and> distinct ps \<and> Path q next root qs \<and> distinct qs \<and> root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs; q \<noteq> root\<rbrakk> \<Longrightarrow> \<exists>ps qs. Path q (next(q := p)) root ps \<and> distinct ps \<and> Path (next q) (next(q := p)) root qs \<and> distinct qs \<and> root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs
 3. \<And>next p q root. \<lbrakk>\<exists>ps qs. Path p next root ps \<and> distinct ps \<and> Path q next root qs \<and> distinct qs \<and> root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs; \<not> q \<noteq> root\<rbrakk> \<Longrightarrow> root = r \<and> Path root (next(root := p)) root (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply   fastforce
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q root. \<lbrakk>\<exists>ps qs. Path p next root ps \<and> distinct ps \<and> Path q next root qs \<and> distinct qs \<and> root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs; q \<noteq> root\<rbrakk> \<Longrightarrow> \<exists>ps qs. Path q (next(q := p)) root ps \<and> distinct ps \<and> Path (next q) (next(q := p)) root qs \<and> distinct qs \<and> root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs
 2. \<And>next p q root. \<lbrakk>\<exists>ps qs. Path p next root ps \<and> distinct ps \<and> Path q next root qs \<and> distinct qs \<and> root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs; \<not> q \<noteq> root\<rbrakk> \<Longrightarrow> root = r \<and> Path root (next(root := p)) root (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q ps qs. \<lbrakk>q \<noteq> r; Path p next r ps; distinct ps; Path q next r qs; distinct qs; r \<noteq> Null; set ps \<inter> set qs = {}; Ps = rev ps @ qs; r \<notin> set ps; r \<notin> set qs\<rbrakk> \<Longrightarrow> \<exists>psa. Path q (next(q := p)) r psa \<and> distinct psa \<and> (\<exists>qsa. Path (next q) (next(q := p)) r qsa \<and> distinct qsa \<and> set psa \<inter> set qsa = {} \<and> rev ps @ qs = rev psa @ qsa)
 2. \<And>next p q root. \<lbrakk>\<exists>ps qs. Path p next root ps \<and> distinct ps \<and> Path q next root qs \<and> distinct qs \<and> root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs; \<not> q \<noteq> root\<rbrakk> \<Longrightarrow> root = r \<and> Path root (next(root := p)) root (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  (drule (2) neq_dP)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q ps qs. \<lbrakk>Path p next r ps; distinct ps; Path q next r qs; distinct qs; r \<noteq> Null; set ps \<inter> set qs = {}; Ps = rev ps @ qs; r \<notin> set ps; r \<notin> set qs; \<exists>Qs. q \<noteq> Null \<and> qs = q # Qs \<and> q \<notin> set Qs\<rbrakk> \<Longrightarrow> \<exists>psa. Path q (next(q := p)) r psa \<and> distinct psa \<and> (\<exists>qsa. Path (next q) (next(q := p)) r qsa \<and> distinct qsa \<and> set psa \<inter> set qsa = {} \<and> rev ps @ qs = rev psa @ qsa)
 2. \<And>next p q root. \<lbrakk>\<exists>ps qs. Path p next root ps \<and> distinct ps \<and> Path q next root qs \<and> distinct qs \<and> root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs; \<not> q \<noteq> root\<rbrakk> \<Longrightarrow> root = r \<and> Path root (next(root := p)) root (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  (rule_tac x="q # ps" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q ps qs. \<lbrakk>Path p next r ps; distinct ps; Path q next r qs; distinct qs; r \<noteq> Null; set ps \<inter> set qs = {}; Ps = rev ps @ qs; r \<notin> set ps; r \<notin> set qs; \<exists>Qs. q \<noteq> Null \<and> qs = q # Qs \<and> q \<notin> set Qs\<rbrakk> \<Longrightarrow> Path q (next(q := p)) r (q # ps) \<and> distinct (q # ps) \<and> (\<exists>qsa. Path (next q) (next(q := p)) r qsa \<and> distinct qsa \<and> set (q # ps) \<inter> set qsa = {} \<and> rev ps @ qs = rev (q # ps) @ qsa)
 2. \<And>next p q root. \<lbrakk>\<exists>ps qs. Path p next root ps \<and> distinct ps \<and> Path q next root qs \<and> distinct qs \<and> root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs; \<not> q \<noteq> root\<rbrakk> \<Longrightarrow> root = r \<and> Path root (next(root := p)) root (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>next p q root. \<lbrakk>\<exists>ps qs. Path p next root ps \<and> distinct ps \<and> Path q next root qs \<and> distinct qs \<and> root = r \<and> r \<noteq> Null \<and> r \<notin> set Ps \<and> set ps \<inter> set qs = {} \<and> Ps = rev ps @ qs; \<not> q \<noteq> root\<rbrakk> \<Longrightarrow> root = r \<and> Path root (next(root := p)) root (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma path_is_list:"\<And>a next b. \<lbrakk>Path b next a Ps ; a \<notin> set Ps; a\<noteq>Null\<rbrakk>
\<Longrightarrow> List b (next(a := Null)) (Ps @ [a])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a next b. \<lbrakk>Path b next a Ps; a \<notin> set Ps; a \<noteq> Null\<rbrakk> \<Longrightarrow> List b (next(a := Null)) (Ps @ [a])
[PROOF STEP]
apply (induct Ps)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a next b. \<lbrakk>Path b next a []; a \<notin> set []; a \<noteq> Null\<rbrakk> \<Longrightarrow> List b (next(a := Null)) ([] @ [a])
 2. \<And>a Ps aa next b. \<lbrakk>\<And>a next b. \<lbrakk>Path b next a Ps; a \<notin> set Ps; a \<noteq> Null\<rbrakk> \<Longrightarrow> List b (next(a := Null)) (Ps @ [a]); Path b next aa (a # Ps); aa \<notin> set (a # Ps); aa \<noteq> Null\<rbrakk> \<Longrightarrow> List b (next(aa := Null)) ((a # Ps) @ [aa])
[PROOF STEP]
apply (auto simp add:fun_upd_apply)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in list_alloc) circular_list_rev_II:
 "\<Gamma>,\<Theta>\<turnstile>
 \<lbrace>\<acute>p = r \<and> distPath \<acute>p \<acute>next \<acute>p (r#Ps)\<rbrace>
\<acute>q:==Null;;
WHILE \<acute>p \<noteq> Null
INV
 \<lbrace> ((\<acute>q = Null) \<longrightarrow> (\<exists>ps. distPath \<acute>p \<acute>next r ps  \<and>  ps = r#Ps)) \<and>
  ((\<acute>q \<noteq> Null) \<longrightarrow> (\<exists>ps qs. distPath \<acute>q \<acute>next r qs  \<and> List \<acute>p \<acute>next ps  \<and>
                   set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps@[r])) \<and>
  \<not> (\<acute>p = Null \<and> \<acute>q = Null \<and> r = Null )
   \<rbrace>
DO
  \<acute>tmp :== \<acute>p;; \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; \<acute>tmp\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q:==\<acute>tmp
OD
 \<lbrace>\<acute>q = r \<and> distPath \<acute>q \<acute>next \<acute>q (r # rev Ps)\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> \<lbrace>\<acute>p = r \<and> distPath \<acute>p \<acute>next \<acute>p (r # Ps)\<rbrace> \<acute>q :== Null;; WHILE \<acute>p \<noteq> Null INV \<lbrace>(\<acute>q = Null \<longrightarrow> (\<exists>ps. distPath \<acute>p \<acute>next r ps \<and> ps = r # Ps)) \<and> (\<acute>q \<noteq> Null \<longrightarrow> (\<exists>ps qs. distPath \<acute>q \<acute>next r qs \<and> List \<acute>p \<acute>next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r])) \<and> \<not> (\<acute>p = Null \<and> \<acute>q = Null \<and> r = Null)\<rbrace> DO \<acute>tmp :== \<acute>p;; \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; \<acute>tmp\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>tmp OD \<lbrace>\<acute>q = r \<and> distPath \<acute>q \<acute>next \<acute>q (r # rev Ps)\<rbrace>
[PROOF STEP]
apply (simp only:distPath_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>,\<Theta>\<turnstile> \<lbrace>\<acute>p = r \<and> Path \<acute>p \<acute>next \<acute>p (r # Ps) \<and> distinct (r # Ps)\<rbrace> \<acute>q :== Null;; WHILE \<acute>p \<noteq> Null INV \<lbrace>(\<acute>q = Null \<longrightarrow> (\<exists>ps. (Path \<acute>p \<acute>next r ps \<and> distinct ps) \<and> ps = r # Ps)) \<and> (\<acute>q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (Path \<acute>q \<acute>next r qs \<and> distinct qs) \<and> List \<acute>p \<acute>next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r])) \<and> \<not> (\<acute>p = Null \<and> \<acute>q = Null \<and> r = Null)\<rbrace> DO \<acute>tmp :== \<acute>p;; \<acute>p :== \<acute>p\<rightarrow>\<acute>next;; \<acute>tmp\<rightarrow>\<acute>next :== \<acute>q;; \<acute>q :== \<acute>tmp OD \<lbrace>\<acute>q = r \<and> Path \<acute>q \<acute>next \<acute>q (r # rev Ps) \<and> distinct (r # rev Ps)\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>next p. \<lbrakk>Path p next p (p # Ps); distinct (p # Ps)\<rbrakk> \<Longrightarrow> (Null = Null \<longrightarrow> (\<exists>ps. Path p next p ps \<and> distinct ps \<and> ps = p # Ps)) \<and> (Null \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path Null next p qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [p])) \<and> \<not> (p = Null \<and> Null = Null \<and> p = Null)
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); p \<noteq> Null\<rbrakk> \<Longrightarrow> (p = Null \<longrightarrow> (\<exists>ps. Path (next p) (next(p := q)) r ps \<and> distinct ps \<and> ps = r # Ps)) \<and> (p \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path p (next(p := q)) r qs \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r])) \<and> \<not> (next p = Null \<and> p = Null \<and> r = Null)
 3. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply   clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); p \<noteq> Null\<rbrakk> \<Longrightarrow> (p = Null \<longrightarrow> (\<exists>ps. Path (next p) (next(p := q)) r ps \<and> distinct ps \<and> ps = r # Ps)) \<and> (p \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path p (next(p := q)) r qs \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r])) \<and> \<not> (next p = Null \<and> p = Null \<and> r = Null)
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  clarsimp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps)) \<and> distinct qs \<and> (\<exists>psa. ps = p # psa \<and> List (next p) next psa) \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); p \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  (case_tac "(q = Null)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps)) \<and> distinct qs \<and> (\<exists>psa. ps = p # psa \<and> List (next p) next psa) \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); p \<noteq> Null; q = Null\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps)) \<and> distinct qs \<and> (\<exists>psa. ps = p # psa \<and> List (next p) next psa) \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); p \<noteq> Null; q \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 3. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply   (fastforce intro: path_is_list)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; q \<noteq> Null \<longrightarrow> (\<exists>ps qs. (qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps)) \<and> distinct qs \<and> (\<exists>psa. ps = p # psa \<and> List (next p) next psa) \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); p \<noteq> Null; q \<noteq> Null\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  clarify
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q ps qs psa. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; p \<noteq> Null; q \<noteq> Null; qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps); distinct qs; set (p # psa) \<inter> set qs = {}; rev qs @ p # psa = Ps @ [r]; List (next p) next psa\<rbrakk> \<Longrightarrow> \<exists>ps qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  (rule_tac x="psa" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q ps qs psa. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; p \<noteq> Null; q \<noteq> Null; qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps); distinct qs; set (p # psa) \<inter> set qs = {}; rev qs @ p # psa = Ps @ [r]; List (next p) next psa\<rbrakk> \<Longrightarrow> \<exists>qs. (qs = [] \<and> r = p \<or> (\<exists>ps. qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct qs \<and> List (next p) (next(p := q)) psa \<and> set psa \<inter> set qs = {} \<and> rev qs @ psa = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  (rule_tac x=" p # qs" in exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>next p q ps qs psa. \<lbrakk>q = Null \<longrightarrow> r = p \<and> Path (next p) next r Ps \<and> r \<notin> set Ps \<and> distinct Ps; p \<noteq> Null; q \<noteq> Null; qs = [] \<and> r = q \<or> (\<exists>ps. qs = q # ps \<and> Path (next q) next r ps); distinct qs; set (p # psa) \<inter> set qs = {}; rev qs @ p # psa = Ps @ [r]; List (next p) next psa\<rbrakk> \<Longrightarrow> (p # qs = [] \<and> r = p \<or> (\<exists>ps. p # qs = p # ps \<and> Path q (next(p := q)) r ps)) \<and> distinct (p # qs) \<and> List (next p) (next(p := q)) psa \<and> set psa \<inter> set (p # qs) = {} \<and> rev (p # qs) @ psa = Ps @ [r]
 2. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply  force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>next p q. \<lbrakk>q = Null \<longrightarrow> (\<exists>ps. Path p next r ps \<and> distinct ps \<and> ps = r # Ps); q \<noteq> Null \<longrightarrow> (\<exists>ps qs. Path q next r qs \<and> distinct qs \<and> List p next ps \<and> set ps \<inter> set qs = {} \<and> rev qs @ ps = Ps @ [r]); \<not> (p = Null \<and> q = Null \<and> r = Null); \<not> p \<noteq> Null\<rbrakk> \<Longrightarrow> q = r \<and> Path q next q (r # rev Ps) \<and> distinct (r # rev Ps)
[PROOF STEP]
apply fastforce
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space) "\<Gamma>\<turnstile> {\<sigma>}
            \<acute>I :== \<acute>M;;
            ANNO \<tau>. \<lbrace>\<tau>. \<acute>I = \<^bsup>\<sigma>\<^esup>M\<rbrace>
                      \<acute>M :== \<acute>N;; \<acute>N :== \<acute>I
                    \<lbrace>\<acute>M = \<^bsup>\<tau>\<^esup>N \<and> \<acute>N = \<^bsup>\<tau>\<^esup>I\<rbrace>
            \<lbrace>\<acute>M = \<^bsup>\<sigma>\<^esup>N \<and> \<acute>N = \<^bsup>\<sigma>\<^esup>M\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> {\<sigma>} \<acute>I :== \<acute>M;; ANNO \<tau>. \<lbrace>\<tau>. \<acute>I = \<^bsup>\<sigma>\<^esup>M\<rbrace> \<acute>M :== \<acute>N;; \<acute>N :== \<acute>I \<lbrace>\<acute>M = \<^bsup>\<tau>\<^esup>N \<and> \<acute>N = \<^bsup>\<tau>\<^esup>I\<rbrace>,{} \<lbrace>\<acute>M = \<^bsup>\<sigma>\<^esup>N \<and> \<acute>N = \<^bsup>\<sigma>\<^esup>M\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M N. M = M \<and> (\<forall>Ma Na. Ma = N \<and> Na = M \<longrightarrow> N = N \<and> M = M)
 2. \<And>M I N. I = M \<Longrightarrow> N = N \<and> I = I
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space) "\<Gamma>\<turnstile> ({\<sigma>} \<inter> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>)
      (ANNO \<tau>. ({\<tau>} \<inter> \<lbrace>\<acute>A=\<^bsup>\<sigma>\<^esup>A \<and> \<acute>I=\<^bsup>\<sigma>\<^esup>I \<and> \<acute>M=0 \<and> \<acute>S=0\<rbrace>)
      WHILE \<acute>M \<noteq> \<acute>A
      INV \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A=\<^bsup>\<tau>\<^esup>A \<and> \<acute>I=\<^bsup>\<tau>\<^esup>I\<rbrace>
      DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>M :== \<acute>M + 1 OD
      \<lbrace>\<acute>S = \<^bsup>\<tau>\<^esup>A * \<^bsup>\<tau>\<^esup>I\<rbrace>)
      \<lbrace>\<acute>S = \<^bsup>\<sigma>\<^esup>A * \<^bsup>\<sigma>\<^esup>I\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> ({\<sigma>} \<inter> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace>) ANNO \<tau>. ({\<tau>} \<inter> \<lbrace>\<acute>A = \<^bsup>\<sigma>\<^esup>A \<and> \<acute>I = \<^bsup>\<sigma>\<^esup>I \<and> \<acute>M = 0 \<and> \<acute>S = 0\<rbrace>) WHILE \<acute>M \<noteq> \<acute>A INV \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I\<rbrace> DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = \<^bsup>\<tau>\<^esup>A * \<^bsup>\<tau>\<^esup>I\<rbrace>,{} \<lbrace>\<acute>S = \<^bsup>\<sigma>\<^esup>A * \<^bsup>\<sigma>\<^esup>I\<rbrace>
[PROOF STEP]
apply vcg_step
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {\<sigma>} \<inter> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> \<subseteq> \<lbrace>\<acute>A = \<^bsup>\<sigma>\<^esup>A \<and> \<acute>I = \<^bsup>\<sigma>\<^esup>I \<and> \<acute>M = 0 \<and> \<acute>S = 0 \<and> (\<forall>t. \<^bsup>t\<^esup>S = \<acute>A * \<acute>I \<longrightarrow> \<acute>A * \<acute>I = \<^bsup>\<sigma>\<^esup>A * \<^bsup>\<sigma>\<^esup>I)\<rbrace>
 2. \<And>\<tau>. \<Gamma>\<turnstile> ({\<tau>} \<inter> \<lbrace>\<acute>A = \<^bsup>\<sigma>\<^esup>A \<and> \<acute>I = \<^bsup>\<sigma>\<^esup>I \<and> \<acute>M = 0 \<and> \<acute>S = 0\<rbrace>) WHILE \<acute>M \<noteq> \<acute>A INV \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I\<rbrace> DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = \<^bsup>\<tau>\<^esup>A * \<^bsup>\<tau>\<^esup>I\<rbrace>
[PROOF STEP]
apply vcg_step
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A I M S. \<lbrakk>M = 0; S = 0\<rbrakk> \<Longrightarrow> A = A \<and> I = I \<and> M = 0 \<and> S = 0 \<and> (\<forall>S. S = A * I \<longrightarrow> A * I = A * I)
 2. \<And>\<tau>. \<Gamma>\<turnstile> ({\<tau>} \<inter> \<lbrace>\<acute>A = \<^bsup>\<sigma>\<^esup>A \<and> \<acute>I = \<^bsup>\<sigma>\<^esup>I \<and> \<acute>M = 0 \<and> \<acute>S = 0\<rbrace>) WHILE \<acute>M \<noteq> \<acute>A INV \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I\<rbrace> DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = \<^bsup>\<tau>\<^esup>A * \<^bsup>\<tau>\<^esup>I\<rbrace>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. \<Gamma>\<turnstile> ({\<tau>} \<inter> \<lbrace>\<acute>A = \<^bsup>\<sigma>\<^esup>A \<and> \<acute>I = \<^bsup>\<sigma>\<^esup>I \<and> \<acute>M = 0 \<and> \<acute>S = 0\<rbrace>) WHILE \<acute>M \<noteq> \<acute>A INV \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I\<rbrace> DO \<acute>S :== \<acute>S + \<acute>I;; \<acute>M :== \<acute>M + 1 OD \<lbrace>\<acute>S = \<^bsup>\<tau>\<^esup>A * \<^bsup>\<tau>\<^esup>I\<rbrace>
[PROOF STEP]
apply vcg_step
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>\<tau>. \<lbrace>\<tau>. \<acute>A = \<^bsup>\<sigma>\<^esup>A \<and> \<acute>I = \<^bsup>\<sigma>\<^esup>I \<and> \<acute>M = 0 \<and> \<acute>S = 0\<rbrace> \<subseteq> \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I\<rbrace>
 2. \<And>\<tau>. \<Gamma>\<turnstile> (\<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I\<rbrace> \<inter> \<lbrace>\<acute>M \<noteq> \<acute>A\<rbrace>) \<acute>S :== \<acute>S + \<acute>I;; \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I\<rbrace>
 3. \<And>\<tau>. \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I \<and> \<not> \<acute>M \<noteq> \<acute>A\<rbrace> \<subseteq> \<lbrace>\<acute>S = \<^bsup>\<tau>\<^esup>A * \<^bsup>\<tau>\<^esup>I\<rbrace>
[PROOF STEP]
apply vcg_step
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>A I Aa Ia M S. \<lbrakk>Aa = A; Ia = I; M = 0; S = 0\<rbrakk> \<Longrightarrow> S = M * Ia \<and> Aa = Aa \<and> Ia = Ia
 2. \<And>\<tau>. \<Gamma>\<turnstile> (\<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I\<rbrace> \<inter> \<lbrace>\<acute>M \<noteq> \<acute>A\<rbrace>) \<acute>S :== \<acute>S + \<acute>I;; \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I\<rbrace>
 3. \<And>\<tau>. \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I \<and> \<not> \<acute>M \<noteq> \<acute>A\<rbrace> \<subseteq> \<lbrace>\<acute>S = \<^bsup>\<tau>\<^esup>A * \<^bsup>\<tau>\<^esup>I\<rbrace>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>\<tau>. \<Gamma>\<turnstile> (\<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I\<rbrace> \<inter> \<lbrace>\<acute>M \<noteq> \<acute>A\<rbrace>) \<acute>S :== \<acute>S + \<acute>I;; \<acute>M :== \<acute>M + 1 \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I\<rbrace>
 2. \<And>\<tau>. \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I \<and> \<not> \<acute>M \<noteq> \<acute>A\<rbrace> \<subseteq> \<lbrace>\<acute>S = \<^bsup>\<tau>\<^esup>A * \<^bsup>\<tau>\<^esup>I\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A I Aa Ia M S. \<lbrakk>S = M * Ia; Aa = A; Ia = I; M \<noteq> Aa\<rbrakk> \<Longrightarrow> S + Ia = (M + 1) * Ia \<and> Aa = A \<and> Ia = I
 2. \<And>\<tau>. \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I \<and> \<not> \<acute>M \<noteq> \<acute>A\<rbrace> \<subseteq> \<lbrace>\<acute>S = \<^bsup>\<tau>\<^esup>A * \<^bsup>\<tau>\<^esup>I\<rbrace>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I \<and> \<not> \<acute>M \<noteq> \<acute>A\<rbrace> \<subseteq> \<lbrace>\<acute>S = \<^bsup>\<tau>\<^esup>A * \<^bsup>\<tau>\<^esup>I\<rbrace>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<tau>. \<lbrace>\<acute>S = \<acute>M * \<acute>I \<and> \<acute>A = \<^bsup>\<tau>\<^esup>A \<and> \<acute>I = \<^bsup>\<tau>\<^esup>I \<and> \<acute>M = \<acute>A\<rbrace> \<subseteq> \<lbrace>\<acute>S = \<^bsup>\<tau>\<^esup>A * \<^bsup>\<tau>\<^esup>I\<rbrace>
[PROOF STEP]
apply vcg_step
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>A I Aa Ia M S. \<lbrakk>S = M * Ia; Aa = A; Ia = I; M = Aa\<rbrakk> \<Longrightarrow> S = A * I
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in state_space) "\<Gamma>\<turnstile>\<lbrace>True\<rbrace> WHILE \<lbrace>P \<acute>N \<rbrace>\<surd>, \<lbrace>Q \<acute>M\<rbrace>#, \<lbrace>R \<acute>N\<rbrace>\<longmapsto> \<acute>N < \<acute>M
                    INV \<lbrace>\<acute>N < 2\<rbrace> DO
                    \<acute>N :== \<acute>M
                  OD
           \<lbrace>hard\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<lbrace>True\<rbrace> WHILE (True, \<lbrace>P \<acute>N\<rbrace>), \<lbrace>Q \<acute>M\<rbrace>#, (False, \<lbrace>R \<acute>N\<rbrace>)\<longmapsto> \<acute>N < \<acute>M INV \<lbrace>\<acute>N < 2\<rbrace> DO \<acute>N :== \<acute>M OD \<lbrace>hard\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>M N. True \<Longrightarrow> P N \<and> Q M \<and> R N \<and> P N \<and> Q M \<and> R N \<and> N < 2
 2. \<And>M N. \<lbrakk>P N; Q M; R N; N < 2; N < M\<rbrakk> \<Longrightarrow> P M \<and> Q M \<and> R M \<and> P M \<and> Q M \<and> R M \<and> M < 2
 3. \<And>M N. \<lbrakk>P N; Q M; R N; N < 2; \<not> N < M\<rbrakk> \<Longrightarrow> hard
[PROOF STEP]
oops


[STATEMENT]
lemma (in state_space) "\<Gamma>\<turnstile>\<^bsub>/{True}\<^esub> \<lbrace>True\<rbrace> WHILE \<lbrace>P \<acute>N \<rbrace>\<surd>, \<lbrace>Q \<acute>M\<rbrace>#, \<lbrace>R \<acute>N\<rbrace>\<longmapsto> \<acute>N < \<acute>M
                    INV \<lbrace>\<acute>N < 2\<rbrace> DO
                    \<acute>N :== \<acute>M
                  OD
           \<lbrace>hard\<rbrace>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/{True}\<^esub> \<lbrace>True\<rbrace> WHILE (True, \<lbrace>P \<acute>N\<rbrace>), \<lbrace>Q \<acute>M\<rbrace>#, (False, \<lbrace>R \<acute>N\<rbrace>)\<longmapsto> \<acute>N < \<acute>M INV \<lbrace>\<acute>N < 2\<rbrace> DO \<acute>N :== \<acute>M OD \<lbrace>hard\<rbrace>
[PROOF STEP]
apply vcg
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>N. True \<Longrightarrow> P N \<longrightarrow> R N \<and> N < 2
 2. \<And>M N. \<lbrakk>P N; R N; N < 2; N < M\<rbrakk> \<Longrightarrow> P M \<longrightarrow> R M \<and> M < 2
 3. \<And>M N. \<lbrakk>P N; R N; N < 2; \<not> N < M\<rbrakk> \<Longrightarrow> hard
[PROOF STEP]
oops


[STATEMENT]
lemma fplus_fzero_left:
  fixes m :: "'a\<cdot>'f::functor_zero_plus"
  shows "fplus\<cdot>fzero\<cdot>m = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fplus\<cdot>fzero\<cdot>m = m
[PROOF STEP]
unfolding fplus_def fzero_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COERCE(udom\<cdot>'f \<rightarrow> udom\<cdot>'f \<rightarrow> udom\<cdot>'f, 'a\<cdot>'f \<rightarrow> 'a\<cdot>'f \<rightarrow> 'a\<cdot>'f)\<cdot>plusU\<cdot>(COERCE(udom\<cdot>'f, 'a\<cdot>'f)\<cdot>zeroU)\<cdot>m = m
[PROOF STEP]
by (simp add: coerce_simp plusU_zeroU_left)


[STATEMENT]
lemma fplus_fzero_right:
  fixes m :: "'a\<cdot>'f::functor_zero_plus"
  shows "fplus\<cdot>m\<cdot>fzero = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fplus\<cdot>m\<cdot>fzero = m
[PROOF STEP]
unfolding fplus_def fzero_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. COERCE(udom\<cdot>'f \<rightarrow> udom\<cdot>'f \<rightarrow> udom\<cdot>'f, 'a\<cdot>'f \<rightarrow> 'a\<cdot>'f \<rightarrow> 'a\<cdot>'f)\<cdot>plusU\<cdot>m\<cdot>(COERCE(udom\<cdot>'f, 'a\<cdot>'f)\<cdot>zeroU) = m
[PROOF STEP]
by (simp add: coerce_simp plusU_zeroU_right)


[STATEMENT]
lemma has_ell2_norm_bdd_above: \<open>has_ell2_norm x \<longleftrightarrow> bdd_above (sum (\<lambda>xa. norm ((x xa)\<^sup>2)) ` Collect finite)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_ell2_norm x = bdd_above (sum (\<lambda>xa. cmod ((x xa)\<^sup>2)) ` Collect finite)
[PROOF STEP]
by (simp add: has_ell2_norm_def abs_summable_iff_bdd_above)


[STATEMENT]
lemma has_ell2_norm_L2_set: "has_ell2_norm x = bdd_above (L2_set (norm o x) ` Collect finite)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_ell2_norm x = bdd_above (L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
proof (rule iffI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. has_ell2_norm x \<Longrightarrow> bdd_above (L2_set (cmod \<circ> x) ` Collect finite)
 2. bdd_above (L2_set (cmod \<circ> x) ` Collect finite) \<Longrightarrow> has_ell2_norm x
[PROOF STEP]
have \<open>mono sqrt\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono sqrt
[PROOF STEP]
using monoI real_sqrt_le_mono
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> ?f x \<le> ?f y) \<Longrightarrow> mono ?f
?x \<le> ?y \<Longrightarrow> sqrt ?x \<le> sqrt ?y

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

goal (2 subgoals):
 1. has_ell2_norm x \<Longrightarrow> bdd_above (L2_set (cmod \<circ> x) ` Collect finite)
 2. bdd_above (L2_set (cmod \<circ> x) ` Collect finite) \<Longrightarrow> has_ell2_norm x
[PROOF STEP]
assume \<open>has_ell2_norm x\<close>
[PROOF STATE]
proof (state)
this:
has_ell2_norm x

goal (2 subgoals):
 1. has_ell2_norm x \<Longrightarrow> bdd_above (L2_set (cmod \<circ> x) ` Collect finite)
 2. bdd_above (L2_set (cmod \<circ> x) ` Collect finite) \<Longrightarrow> has_ell2_norm x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
has_ell2_norm x
[PROOF STEP]
have *: \<open>bdd_above (sum (\<lambda>xa. norm ((x xa)\<^sup>2)) ` Collect finite)\<close>
[PROOF STATE]
proof (prove)
using this:
has_ell2_norm x

goal (1 subgoal):
 1. bdd_above (sum (\<lambda>xa. cmod ((x xa)\<^sup>2)) ` Collect finite)
[PROOF STEP]
by (subst (asm) has_ell2_norm_bdd_above)
[PROOF STATE]
proof (state)
this:
bdd_above (sum (\<lambda>xa. cmod ((x xa)\<^sup>2)) ` Collect finite)

goal (2 subgoals):
 1. has_ell2_norm x \<Longrightarrow> bdd_above (L2_set (cmod \<circ> x) ` Collect finite)
 2. bdd_above (L2_set (cmod \<circ> x) ` Collect finite) \<Longrightarrow> has_ell2_norm x
[PROOF STEP]
have \<open>bdd_above ((\<lambda>F. sqrt (sum (\<lambda>xa. norm ((x xa)\<^sup>2)) F)) ` Collect finite)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above ((\<lambda>F. sqrt (\<Sum>xa\<in>F. cmod ((x xa)\<^sup>2))) ` Collect finite)
[PROOF STEP]
using bdd_above_image_mono[OF \<open>mono sqrt\<close> *]
[PROOF STATE]
proof (prove)
using this:
bdd_above (sqrt ` sum (\<lambda>xa. cmod ((x xa)\<^sup>2)) ` Collect finite)

goal (1 subgoal):
 1. bdd_above ((\<lambda>F. sqrt (\<Sum>xa\<in>F. cmod ((x xa)\<^sup>2))) ` Collect finite)
[PROOF STEP]
by (auto simp: image_image)
[PROOF STATE]
proof (state)
this:
bdd_above ((\<lambda>F. sqrt (\<Sum>xa\<in>F. cmod ((x xa)\<^sup>2))) ` Collect finite)

goal (2 subgoals):
 1. has_ell2_norm x \<Longrightarrow> bdd_above (L2_set (cmod \<circ> x) ` Collect finite)
 2. bdd_above (L2_set (cmod \<circ> x) ` Collect finite) \<Longrightarrow> has_ell2_norm x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bdd_above ((\<lambda>F. sqrt (\<Sum>xa\<in>F. cmod ((x xa)\<^sup>2))) ` Collect finite)
[PROOF STEP]
show \<open>bdd_above (L2_set (norm o x) ` Collect finite)\<close>
[PROOF STATE]
proof (prove)
using this:
bdd_above ((\<lambda>F. sqrt (\<Sum>xa\<in>F. cmod ((x xa)\<^sup>2))) ` Collect finite)

goal (1 subgoal):
 1. bdd_above (L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
by (auto simp: L2_set_def norm_power)
[PROOF STATE]
proof (state)
this:
bdd_above (L2_set (cmod \<circ> x) ` Collect finite)

goal (1 subgoal):
 1. bdd_above (L2_set (cmod \<circ> x) ` Collect finite) \<Longrightarrow> has_ell2_norm x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bdd_above (L2_set (cmod \<circ> x) ` Collect finite) \<Longrightarrow> has_ell2_norm x
[PROOF STEP]
define p2 where \<open>p2 x = (if x < 0 then 0 else x^2)\<close> for x :: real
[PROOF STATE]
proof (state)
this:
p2 ?x = (if ?x < 0 then 0 else ?x\<^sup>2)

goal (1 subgoal):
 1. bdd_above (L2_set (cmod \<circ> x) ` Collect finite) \<Longrightarrow> has_ell2_norm x
[PROOF STEP]
have \<open>mono p2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono p2
[PROOF STEP]
by (simp add: monoI p2_def)
[PROOF STATE]
proof (state)
this:
mono p2

goal (1 subgoal):
 1. bdd_above (L2_set (cmod \<circ> x) ` Collect finite) \<Longrightarrow> has_ell2_norm x
[PROOF STEP]
have [simp]: \<open>p2 (L2_set f F) = (\<Sum>i\<in>F. (f i)\<^sup>2)\<close> for f and F :: \<open>'a set\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p2 (L2_set f F) = (\<Sum>i\<in>F. (f i)\<^sup>2)
[PROOF STEP]
by (smt (verit) L2_set_def L2_set_nonneg p2_def power2_less_0 real_sqrt_pow2 sum.cong sum_nonneg)
[PROOF STATE]
proof (state)
this:
p2 (L2_set ?f ?F) = (\<Sum>i\<in>?F. (?f i)\<^sup>2)

goal (1 subgoal):
 1. bdd_above (L2_set (cmod \<circ> x) ` Collect finite) \<Longrightarrow> has_ell2_norm x
[PROOF STEP]
assume *: \<open>bdd_above (L2_set (norm o x) ` Collect finite)\<close>
[PROOF STATE]
proof (state)
this:
bdd_above (L2_set (cmod \<circ> x) ` Collect finite)

goal (1 subgoal):
 1. bdd_above (L2_set (cmod \<circ> x) ` Collect finite) \<Longrightarrow> has_ell2_norm x
[PROOF STEP]
have \<open>bdd_above (p2 ` L2_set (norm o x) ` Collect finite)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above (p2 ` L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
using bdd_above_image_mono[OF \<open>mono p2\<close> *]
[PROOF STATE]
proof (prove)
using this:
bdd_above (p2 ` L2_set (cmod \<circ> x) ` Collect finite)

goal (1 subgoal):
 1. bdd_above (p2 ` L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bdd_above (p2 ` L2_set (cmod \<circ> x) ` Collect finite)

goal (1 subgoal):
 1. bdd_above (L2_set (cmod \<circ> x) ` Collect finite) \<Longrightarrow> has_ell2_norm x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
bdd_above (p2 ` L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
show \<open>has_ell2_norm x\<close>
[PROOF STATE]
proof (prove)
using this:
bdd_above (p2 ` L2_set (cmod \<circ> x) ` Collect finite)

goal (1 subgoal):
 1. has_ell2_norm x
[PROOF STEP]
apply (simp add: image_image has_ell2_norm_def abs_summable_iff_bdd_above)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite) \<Longrightarrow> bdd_above (sum (\<lambda>xa. cmod ((x xa)\<^sup>2)) ` {F. finite F})
[PROOF STEP]
by (simp add: norm_power)
[PROOF STATE]
proof (state)
this:
has_ell2_norm x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ell2_norm_SUP:
  assumes \<open>has_ell2_norm x\<close>
  shows "ell2_norm x = sqrt (SUP F\<in>{F. finite F}. sum (\<lambda>i. norm (x i)^2) F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ell2_norm x = sqrt (\<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` {F. finite F}))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
has_ell2_norm x

goal (1 subgoal):
 1. ell2_norm x = sqrt (\<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` {F. finite F}))
[PROOF STEP]
apply (auto simp add: ell2_norm_def has_ell2_norm_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>xa. (x xa)\<^sup>2) abs_summable_on UNIV \<Longrightarrow> (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2) = \<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)
[PROOF STEP]
apply (subst infsum_nonneg_is_SUPREMUM_real)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. (\<lambda>xa. (x xa)\<^sup>2) abs_summable_on UNIV \<Longrightarrow> (\<lambda>i. (cmod (x i))\<^sup>2) summable_on UNIV
 2. \<And>xa. \<lbrakk>(\<lambda>xa. (x xa)\<^sup>2) abs_summable_on UNIV; xa \<in> UNIV\<rbrakk> \<Longrightarrow> 0 \<le> (cmod (x xa))\<^sup>2
 3. (\<lambda>xa. (x xa)\<^sup>2) abs_summable_on UNIV \<Longrightarrow> \<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` {F. finite F \<and> F \<subseteq> UNIV}) = \<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)
[PROOF STEP]
by (auto simp: norm_power)


[STATEMENT]
lemma ell2_norm_L2_set:
  assumes "has_ell2_norm x"
  shows "ell2_norm x = (SUP F\<in>{F. finite F}. L2_set (norm o x) F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ell2_norm x = \<Squnion> (L2_set (cmod \<circ> x) ` {F. finite F})
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ell2_norm x = \<Squnion> (L2_set (cmod \<circ> x) ` {F. finite F})
[PROOF STEP]
have "sqrt (\<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)) =
      (SUP F\<in>{F. finite F}. sqrt (\<Sum>i\<in>F. (cmod (x i))\<^sup>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (\<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)) = (\<Squnion>F\<in>{F. finite F}. sqrt (\<Sum>i\<in>F. (cmod (x i))\<^sup>2))
[PROOF STEP]
proof (subst continuous_at_Sup_mono)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. mono sqrt
 2. continuous (at_left (\<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite))) sqrt
 3. sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite \<noteq> {}
 4. bdd_above (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)
 5. \<Squnion> (sqrt ` sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite) = (\<Squnion>F\<in>Collect finite. sqrt (\<Sum>i\<in>F. (cmod (x i))\<^sup>2))
[PROOF STEP]
show "mono sqrt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono sqrt
[PROOF STEP]
by (simp add: mono_def)
[PROOF STATE]
proof (state)
this:
mono sqrt

goal (4 subgoals):
 1. continuous (at_left (\<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite))) sqrt
 2. sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite \<noteq> {}
 3. bdd_above (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)
 4. \<Squnion> (sqrt ` sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite) = (\<Squnion>F\<in>Collect finite. sqrt (\<Sum>i\<in>F. (cmod (x i))\<^sup>2))
[PROOF STEP]
show "continuous (at_left (\<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite))) sqrt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous (at_left (\<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite))) sqrt
[PROOF STEP]
using continuous_at_split isCont_real_sqrt
[PROOF STATE]
proof (prove)
using this:
isCont ?f ?x = (continuous (at_left ?x) ?f \<and> continuous (at_right ?x) ?f)
isCont sqrt ?x

goal (1 subgoal):
 1. continuous (at_left (\<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite))) sqrt
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
continuous (at_left (\<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite))) sqrt

goal (3 subgoals):
 1. sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite \<noteq> {}
 2. bdd_above (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)
 3. \<Squnion> (sqrt ` sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite) = (\<Squnion>F\<in>Collect finite. sqrt (\<Sum>i\<in>F. (cmod (x i))\<^sup>2))
[PROOF STEP]
show "sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite \<noteq> {}

goal (2 subgoals):
 1. bdd_above (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)
 2. \<Squnion> (sqrt ` sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite) = (\<Squnion>F\<in>Collect finite. sqrt (\<Sum>i\<in>F. (cmod (x i))\<^sup>2))
[PROOF STEP]
show "bdd_above (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)
[PROOF STEP]
using has_ell2_norm_bdd_above[THEN iffD1, OF assms]
[PROOF STATE]
proof (prove)
using this:
bdd_above (sum (\<lambda>xa. cmod ((x xa)\<^sup>2)) ` Collect finite)

goal (1 subgoal):
 1. bdd_above (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)
[PROOF STEP]
by (auto simp: norm_power)
[PROOF STATE]
proof (state)
this:
bdd_above (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)

goal (1 subgoal):
 1. \<Squnion> (sqrt ` sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite) = (\<Squnion>F\<in>Collect finite. sqrt (\<Sum>i\<in>F. (cmod (x i))\<^sup>2))
[PROOF STEP]
show "\<Squnion> (sqrt ` sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite) = (SUP F\<in>Collect finite. sqrt (\<Sum>i\<in>F. (cmod (x i))\<^sup>2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> (sqrt ` sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite) = (\<Squnion>F\<in>Collect finite. sqrt (\<Sum>i\<in>F. (cmod (x i))\<^sup>2))
[PROOF STEP]
by (metis image_image)
[PROOF STATE]
proof (state)
this:
\<Squnion> (sqrt ` sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite) = (\<Squnion>F\<in>Collect finite. sqrt (\<Sum>i\<in>F. (cmod (x i))\<^sup>2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sqrt (\<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)) = (\<Squnion>F\<in>{F. finite F}. sqrt (\<Sum>i\<in>F. (cmod (x i))\<^sup>2))

goal (1 subgoal):
 1. ell2_norm x = \<Squnion> (L2_set (cmod \<circ> x) ` {F. finite F})
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sqrt (\<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)) = (\<Squnion>F\<in>{F. finite F}. sqrt (\<Sum>i\<in>F. (cmod (x i))\<^sup>2))

goal (1 subgoal):
 1. ell2_norm x = \<Squnion> (L2_set (cmod \<circ> x) ` {F. finite F})
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sqrt (\<Squnion> (sum (\<lambda>i. (cmod (x i))\<^sup>2) ` Collect finite)) = (\<Squnion>F\<in>{F. finite F}. sqrt (\<Sum>i\<in>F. (cmod (x i))\<^sup>2))
has_ell2_norm x

goal (1 subgoal):
 1. ell2_norm x = \<Squnion> (L2_set (cmod \<circ> x) ` {F. finite F})
[PROOF STEP]
by (auto simp: ell2_norm_SUP L2_set_def)
[PROOF STATE]
proof (state)
this:
ell2_norm x = \<Squnion> (L2_set (cmod \<circ> x) ` {F. finite F})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma has_ell2_norm_finite[simp]: "has_ell2_norm (x::'a::finite\<Rightarrow>_)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_ell2_norm x
[PROOF STEP]
unfolding has_ell2_norm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>xa. (x xa)\<^sup>2) abs_summable_on UNIV
[PROOF STEP]
by simp


[STATEMENT]
lemma ell2_norm_finite:
  "ell2_norm (x::'a::finite\<Rightarrow>complex) = sqrt (sum (\<lambda>i. (norm(x i))^2) UNIV)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ell2_norm x = sqrt (\<Sum>i\<in>UNIV. (cmod (x i))\<^sup>2)
[PROOF STEP]
by (simp add: ell2_norm_def)


[STATEMENT]
lemma ell2_norm_finite_L2_set: "ell2_norm (x::'a::finite\<Rightarrow>complex) = L2_set (norm o x) UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ell2_norm x = L2_set (cmod \<circ> x) UNIV
[PROOF STEP]
by (simp add: ell2_norm_finite L2_set_def)


[STATEMENT]
lemma ell2_norm_square: \<open>(ell2_norm x)\<^sup>2 = (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ell2_norm x)\<^sup>2 = (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2)
[PROOF STEP]
unfolding ell2_norm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sqrt (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2))\<^sup>2 = (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2)
[PROOF STEP]
apply (subst real_sqrt_pow2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. 0 \<le> (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2)
 2. (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2) = (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2)
[PROOF STEP]
by (simp_all add: infsum_nonneg)


[STATEMENT]
lemma ell2_ket:
  fixes a
  defines \<open>f \<equiv> (\<lambda>i. if a = i then 1 else 0)\<close>
  shows has_ell2_norm_ket: \<open>has_ell2_norm f\<close>
    and ell2_norm_ket: \<open>ell2_norm f = 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_ell2_norm f &&& ell2_norm f = 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. has_ell2_norm f
 2. ell2_norm f = 1
[PROOF STEP]
have \<open>(\<lambda>x. (f x)\<^sup>2) abs_summable_on {a}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. (f x)\<^sup>2) abs_summable_on {a}
[PROOF STEP]
apply (rule summable_on_finite)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {a}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>x. (f x)\<^sup>2) abs_summable_on {a}

goal (2 subgoals):
 1. has_ell2_norm f
 2. ell2_norm f = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>x. (f x)\<^sup>2) abs_summable_on {a}
[PROOF STEP]
show \<open>has_ell2_norm f\<close>
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (f x)\<^sup>2) abs_summable_on {a}

goal (1 subgoal):
 1. has_ell2_norm f
[PROOF STEP]
unfolding has_ell2_norm_def
[PROOF STATE]
proof (prove)
using this:
(\<lambda>x. (f x)\<^sup>2) abs_summable_on {a}

goal (1 subgoal):
 1. (\<lambda>x. (f x)\<^sup>2) abs_summable_on UNIV
[PROOF STEP]
apply (rule summable_on_cong_neutral[THEN iffD1, rotated -1])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> UNIV - {a} \<Longrightarrow> cmod ((f x)\<^sup>2) = 0
 2. \<And>x. x \<in> {a} - UNIV \<Longrightarrow> cmod ((f x)\<^sup>2) = 0
 3. \<And>x. x \<in> {a} \<inter> UNIV \<Longrightarrow> cmod ((f x)\<^sup>2) = cmod ((f x)\<^sup>2)
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. x \<in> UNIV - {a} \<Longrightarrow> cmod ((if a = x then 1 else 0)\<^sup>2) = 0
 2. \<And>x. x \<in> {a} - UNIV \<Longrightarrow> cmod ((if a = x then 1 else 0)\<^sup>2) = 0
 3. \<And>x. x \<in> {a} \<inter> UNIV \<Longrightarrow> cmod ((if a = x then 1 else 0)\<^sup>2) = cmod ((if a = x then 1 else 0)\<^sup>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
has_ell2_norm f

goal (1 subgoal):
 1. ell2_norm f = 1
[PROOF STEP]
have \<open>(\<Sum>\<^sub>\<infinity>x\<in>{a}. (f x)\<^sup>2) = 1\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>\<infinity>x\<in>{a}. (f x)\<^sup>2) = 1
[PROOF STEP]
apply (subst infsum_finite)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. finite {a}
 2. (\<Sum>x\<in>{a}. (f x)\<^sup>2) = 1
[PROOF STEP]
by (auto simp: f_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>\<infinity>x\<in>{a}. (f x)\<^sup>2) = 1

goal (1 subgoal):
 1. ell2_norm f = 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>\<^sub>\<infinity>x\<in>{a}. (f x)\<^sup>2) = 1
[PROOF STEP]
show \<open>ell2_norm f = 1\<close>
[PROOF STATE]
proof (prove)
using this:
(\<Sum>\<^sub>\<infinity>x\<in>{a}. (f x)\<^sup>2) = 1

goal (1 subgoal):
 1. ell2_norm f = 1
[PROOF STEP]
unfolding ell2_norm_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>\<^sub>\<infinity>x\<in>{a}. (f x)\<^sup>2) = 1

goal (1 subgoal):
 1. sqrt (\<Sum>\<^sub>\<infinity>i. (cmod (f i))\<^sup>2) = 1
[PROOF STEP]
apply (subst infsum_cong_neutral[where T=\<open>{a}\<close> and g=\<open>\<lambda>x. (cmod (f x))\<^sup>2\<close>])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>(\<Sum>\<^sub>\<infinity>x\<in>{a}. (f x)\<^sup>2) = 1; x \<in> {a} - UNIV\<rbrakk> \<Longrightarrow> (cmod (f x))\<^sup>2 = 0
 2. \<And>x. \<lbrakk>(\<Sum>\<^sub>\<infinity>x\<in>{a}. (f x)\<^sup>2) = 1; x \<in> UNIV - {a}\<rbrakk> \<Longrightarrow> (cmod (f x))\<^sup>2 = 0
 3. \<And>x. \<lbrakk>(\<Sum>\<^sub>\<infinity>x\<in>{a}. (f x)\<^sup>2) = 1; x \<in> UNIV \<inter> {a}\<rbrakk> \<Longrightarrow> (cmod (f x))\<^sup>2 = (cmod (f x))\<^sup>2
 4. (\<Sum>\<^sub>\<infinity>x\<in>{a}. (f x)\<^sup>2) = 1 \<Longrightarrow> sqrt (\<Sum>\<^sub>\<infinity>x\<in>{a}. (cmod (f x))\<^sup>2) = 1
[PROOF STEP]
by (auto simp: f_def)
[PROOF STATE]
proof (state)
this:
ell2_norm f = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ell2_norm_geq0: \<open>ell2_norm x \<ge> 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> ell2_norm x
[PROOF STEP]
by (auto simp: ell2_norm_def intro!: infsum_nonneg)


[STATEMENT]
lemma ell2_norm_point_bound:
  assumes \<open>has_ell2_norm x\<close>
  shows \<open>ell2_norm x \<ge> cmod (x i)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
have \<open>(cmod (x i))\<^sup>2 = norm ((x i)\<^sup>2)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cmod (x i))\<^sup>2 = cmod ((x i)\<^sup>2)
[PROOF STEP]
by (simp add: norm_power)
[PROOF STATE]
proof (state)
this:
(cmod (x i))\<^sup>2 = cmod ((x i)\<^sup>2)

goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(cmod (x i))\<^sup>2 = cmod ((x i)\<^sup>2)

goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
have \<open>norm ((x i)\<^sup>2) = sum (\<lambda>i. (norm ((x i)\<^sup>2))) {i}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod ((x i)\<^sup>2) = (\<Sum>i\<in>{i}. cmod ((x i)\<^sup>2))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cmod ((x i)\<^sup>2) = (\<Sum>i\<in>{i}. cmod ((x i)\<^sup>2))

goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod ((x i)\<^sup>2) = (\<Sum>i\<in>{i}. cmod ((x i)\<^sup>2))

goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
have \<open>\<dots> = infsum (\<lambda>i. (norm ((x i)\<^sup>2))) {i}\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>{i}. cmod ((x i)\<^sup>2)) = (\<Sum>\<^sub>\<infinity>i\<in>{i}. cmod ((x i)\<^sup>2))
[PROOF STEP]
by (rule infsum_finite[symmetric], simp)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i}. cmod ((x i)\<^sup>2)) = (\<Sum>\<^sub>\<infinity>i\<in>{i}. cmod ((x i)\<^sup>2))

goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>{i}. cmod ((x i)\<^sup>2)) = (\<Sum>\<^sub>\<infinity>i\<in>{i}. cmod ((x i)\<^sup>2))

goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
have \<open>\<dots> \<le> infsum (\<lambda>i. (norm ((x i)\<^sup>2))) UNIV\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>\<infinity>i\<in>{i}. cmod ((x i)\<^sup>2)) \<le> (\<Sum>\<^sub>\<infinity>i. cmod ((x i)\<^sup>2))
[PROOF STEP]
apply (rule infsum_mono_neutral)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. (\<lambda>i. (x i)\<^sup>2) abs_summable_on {i}
 2. (\<lambda>i. (x i)\<^sup>2) abs_summable_on UNIV
 3. \<And>xa. xa \<in> {i} \<inter> UNIV \<Longrightarrow> cmod ((x xa)\<^sup>2) \<le> cmod ((x xa)\<^sup>2)
 4. \<And>xa. xa \<in> {i} - UNIV \<Longrightarrow> cmod ((x xa)\<^sup>2) \<le> 0
 5. \<And>xa. xa \<in> UNIV - {i} \<Longrightarrow> 0 \<le> cmod ((x xa)\<^sup>2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
has_ell2_norm x

goal (5 subgoals):
 1. (\<lambda>i. (x i)\<^sup>2) abs_summable_on {i}
 2. (\<lambda>i. (x i)\<^sup>2) abs_summable_on UNIV
 3. \<And>xa. xa \<in> {i} \<inter> UNIV \<Longrightarrow> cmod ((x xa)\<^sup>2) \<le> cmod ((x xa)\<^sup>2)
 4. \<And>xa. xa \<in> {i} - UNIV \<Longrightarrow> cmod ((x xa)\<^sup>2) \<le> 0
 5. \<And>xa. xa \<in> UNIV - {i} \<Longrightarrow> 0 \<le> cmod ((x xa)\<^sup>2)
[PROOF STEP]
by (auto simp: has_ell2_norm_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>\<infinity>i\<in>{i}. cmod ((x i)\<^sup>2)) \<le> (\<Sum>\<^sub>\<infinity>i. cmod ((x i)\<^sup>2))

goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>\<infinity>i\<in>{i}. cmod ((x i)\<^sup>2)) \<le> (\<Sum>\<^sub>\<infinity>i. cmod ((x i)\<^sup>2))

goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
have \<open>\<dots> = (ell2_norm x)\<^sup>2\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>\<^sub>\<infinity>i. cmod ((x i)\<^sup>2)) = (ell2_norm x)\<^sup>2
[PROOF STEP]
by (metis (no_types, lifting) ell2_norm_def ell2_norm_geq0 infsum_cong norm_power real_sqrt_eq_iff real_sqrt_unique)
[PROOF STATE]
proof (state)
this:
(\<Sum>\<^sub>\<infinity>i. cmod ((x i)\<^sup>2)) = (ell2_norm x)\<^sup>2

goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(cmod (x i))\<^sup>2 \<le> (ell2_norm x)\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(cmod (x i))\<^sup>2 \<le> (ell2_norm x)\<^sup>2

goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
using ell2_norm_geq0 power2_le_imp_le
[PROOF STATE]
proof (prove)
using this:
(cmod (x i))\<^sup>2 \<le> (ell2_norm x)\<^sup>2
0 \<le> ell2_norm ?x
\<lbrakk>?x\<^sup>2 \<le> ?y\<^sup>2; (0::?'a) \<le> ?y\<rbrakk> \<Longrightarrow> ?x \<le> ?y

goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
cmod (x i) \<le> ell2_norm x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ell2_norm_0:
  assumes "has_ell2_norm x"
  shows "ell2_norm x = 0 \<longleftrightarrow> x = (\<lambda>_. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ell2_norm x = 0) = (x = (\<lambda>_. 0))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ell2_norm x = 0 \<Longrightarrow> x = (\<lambda>_. 0)
 2. x = (\<lambda>_. 0) \<Longrightarrow> ell2_norm x = 0
[PROOF STEP]
assume u1: "x = (\<lambda>_. 0)"
[PROOF STATE]
proof (state)
this:
x = (\<lambda>_. 0)

goal (2 subgoals):
 1. ell2_norm x = 0 \<Longrightarrow> x = (\<lambda>_. 0)
 2. x = (\<lambda>_. 0) \<Longrightarrow> ell2_norm x = 0
[PROOF STEP]
have u2: "(SUP x::'a set\<in>Collect finite. (0::real)) = 0"
    if "x = (\<lambda>_. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Squnion>x\<in>Collect finite. 0) = 0
[PROOF STEP]
by (metis cSUP_const empty_Collect_eq finite.emptyI)
[PROOF STATE]
proof (state)
this:
x = (\<lambda>_. 0) \<Longrightarrow> (\<Squnion>x\<in>Collect finite. 0) = 0

goal (2 subgoals):
 1. ell2_norm x = 0 \<Longrightarrow> x = (\<lambda>_. 0)
 2. x = (\<lambda>_. 0) \<Longrightarrow> ell2_norm x = 0
[PROOF STEP]
show "ell2_norm x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ell2_norm x = 0
[PROOF STEP]
unfolding ell2_norm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sqrt (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2) = 0
[PROOF STEP]
using u1 u2
[PROOF STATE]
proof (prove)
using this:
x = (\<lambda>_. 0)
x = (\<lambda>_. 0) \<Longrightarrow> (\<Squnion>x\<in>Collect finite. 0) = 0

goal (1 subgoal):
 1. sqrt (\<Sum>\<^sub>\<infinity>i. (cmod (x i))\<^sup>2) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ell2_norm x = 0

goal (1 subgoal):
 1. ell2_norm x = 0 \<Longrightarrow> x = (\<lambda>_. 0)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ell2_norm x = 0 \<Longrightarrow> x = (\<lambda>_. 0)
[PROOF STEP]
assume norm0: "ell2_norm x = 0"
[PROOF STATE]
proof (state)
this:
ell2_norm x = 0

goal (1 subgoal):
 1. ell2_norm x = 0 \<Longrightarrow> x = (\<lambda>_. 0)
[PROOF STEP]
show "x = (\<lambda>_. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = (\<lambda>_. 0)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>uu_. x uu_ = 0
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>uu_. x uu_ = 0
[PROOF STEP]
have \<open>cmod (x i) \<le> ell2_norm x\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
has_ell2_norm x

goal (1 subgoal):
 1. cmod (x i) \<le> ell2_norm x
[PROOF STEP]
by (rule ell2_norm_point_bound)
[PROOF STATE]
proof (state)
this:
cmod (x i) \<le> ell2_norm x

goal (1 subgoal):
 1. \<And>uu_. x uu_ = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cmod (x i) \<le> ell2_norm x

goal (1 subgoal):
 1. \<And>uu_. x uu_ = 0
[PROOF STEP]
have \<open>\<dots> = 0\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ell2_norm x = 0
[PROOF STEP]
by (fact norm0)
[PROOF STATE]
proof (state)
this:
ell2_norm x = 0

goal (1 subgoal):
 1. \<And>uu_. x uu_ = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cmod (x i) \<le> 0
[PROOF STEP]
show "x i = 0"
[PROOF STATE]
proof (prove)
using this:
cmod (x i) \<le> 0

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x = (\<lambda>_. 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ell2_norm_smult:
  assumes "has_ell2_norm x"
  shows "has_ell2_norm (\<lambda>i. c * x i)" and "ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_ell2_norm (\<lambda>i. c * x i) &&& ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. has_ell2_norm (\<lambda>i. c * x i)
 2. ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x
[PROOF STEP]
have L2_set_mul: "L2_set (cmod \<circ> (\<lambda>i. c * x i)) F = cmod c * L2_set (cmod \<circ> x) F" for F
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. c * x i)) F = cmod c * L2_set (cmod \<circ> x) F
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. c * x i)) F = cmod c * L2_set (cmod \<circ> x) F
[PROOF STEP]
have "L2_set (cmod \<circ> (\<lambda>i. c * x i)) F = L2_set (\<lambda>i. (cmod c * (cmod o x) i)) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. c * x i)) F = L2_set (\<lambda>i. cmod c * (cmod \<circ> x) i) F
[PROOF STEP]
by (metis comp_def norm_mult)
[PROOF STATE]
proof (state)
this:
L2_set (cmod \<circ> (\<lambda>i. c * x i)) F = L2_set (\<lambda>i. cmod c * (cmod \<circ> x) i) F

goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. c * x i)) F = cmod c * L2_set (cmod \<circ> x) F
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
L2_set (cmod \<circ> (\<lambda>i. c * x i)) F = L2_set (\<lambda>i. cmod c * (cmod \<circ> x) i) F

goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. c * x i)) F = cmod c * L2_set (cmod \<circ> x) F
[PROOF STEP]
have "\<dots> = cmod c * L2_set (cmod o x) F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L2_set (\<lambda>i. cmod c * (cmod \<circ> x) i) F = cmod c * L2_set (cmod \<circ> x) F
[PROOF STEP]
by (metis norm_ge_zero L2_set_right_distrib)
[PROOF STATE]
proof (state)
this:
L2_set (\<lambda>i. cmod c * (cmod \<circ> x) i) F = cmod c * L2_set (cmod \<circ> x) F

goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. c * x i)) F = cmod c * L2_set (cmod \<circ> x) F
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
L2_set (cmod \<circ> (\<lambda>i. c * x i)) F = cmod c * L2_set (cmod \<circ> x) F
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
L2_set (cmod \<circ> (\<lambda>i. c * x i)) F = cmod c * L2_set (cmod \<circ> x) F

goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. c * x i)) F = cmod c * L2_set (cmod \<circ> x) F
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
L2_set (cmod \<circ> (\<lambda>i. c * x i)) F = cmod c * L2_set (cmod \<circ> x) F

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
L2_set (cmod \<circ> (\<lambda>i. c * x i)) ?F = cmod c * L2_set (cmod \<circ> x) ?F

goal (2 subgoals):
 1. has_ell2_norm (\<lambda>i. c * x i)
 2. ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
has_ell2_norm x
[PROOF STEP]
obtain M where M: "M \<ge> L2_set (cmod o x) F" if "finite F" for F
[PROOF STATE]
proof (prove)
using this:
has_ell2_norm x

goal (1 subgoal):
 1. (\<And>M. (\<And>F. finite F \<Longrightarrow> L2_set (cmod \<circ> x) F \<le> M) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding has_ell2_norm_L2_set bdd_above_def
[PROOF STATE]
proof (prove)
using this:
\<exists>M. \<forall>x\<in>L2_set (cmod \<circ> x) ` Collect finite. x \<le> M

goal (1 subgoal):
 1. (\<And>M. (\<And>F. finite F \<Longrightarrow> L2_set (cmod \<circ> x) F \<le> M) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> x) ?F \<le> M

goal (2 subgoals):
 1. has_ell2_norm (\<lambda>i. c * x i)
 2. ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x
[PROOF STEP]
hence "cmod c * M \<ge> L2_set (cmod o (\<lambda>i. c * x i)) F" if "finite F" for F
[PROOF STATE]
proof (prove)
using this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> x) ?F \<le> M

goal (1 subgoal):
 1. L2_set (cmod \<circ> (\<lambda>i. c * x i)) F \<le> cmod c * M
[PROOF STEP]
unfolding L2_set_mul
[PROOF STATE]
proof (prove)
using this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> x) ?F \<le> M

goal (1 subgoal):
 1. cmod c * L2_set (cmod \<circ> x) F \<le> cmod c * M
[PROOF STEP]
by (simp add: ordered_comm_semiring_class.comm_mult_left_mono that)
[PROOF STATE]
proof (state)
this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> (\<lambda>i. c * x i)) ?F \<le> cmod c * M

goal (2 subgoals):
 1. has_ell2_norm (\<lambda>i. c * x i)
 2. ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x
[PROOF STEP]
thus has: "has_ell2_norm (\<lambda>i. c * x i)"
[PROOF STATE]
proof (prove)
using this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> (\<lambda>i. c * x i)) ?F \<le> cmod c * M

goal (1 subgoal):
 1. has_ell2_norm (\<lambda>i. c * x i)
[PROOF STEP]
unfolding has_ell2_norm_L2_set bdd_above_def
[PROOF STATE]
proof (prove)
using this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> (\<lambda>i. c * x i)) ?F \<le> cmod c * M

goal (1 subgoal):
 1. \<exists>M. \<forall>x\<in>L2_set (cmod \<circ> (\<lambda>i. c * x i)) ` Collect finite. x \<le> M
[PROOF STEP]
using L2_set_mul[symmetric]
[PROOF STATE]
proof (prove)
using this:
finite ?F \<Longrightarrow> L2_set (cmod \<circ> (\<lambda>i. c * x i)) ?F \<le> cmod c * M
cmod c * L2_set (cmod \<circ> x) ?F = L2_set (cmod \<circ> (\<lambda>i. c * x i)) ?F

goal (1 subgoal):
 1. \<exists>M. \<forall>x\<in>L2_set (cmod \<circ> (\<lambda>i. c * x i)) ` Collect finite. x \<le> M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
has_ell2_norm (\<lambda>i. c * x i)

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x
[PROOF STEP]
have "ell2_norm (\<lambda>i. c * x i) = (SUP F \<in> Collect finite. (L2_set (cmod \<circ> (\<lambda>i. c * x i)) F))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ell2_norm (\<lambda>i. c * x i) = \<Squnion> (L2_set (cmod \<circ> (\<lambda>i. c * x i)) ` Collect finite)
[PROOF STEP]
by (simp add: ell2_norm_L2_set has)
[PROOF STATE]
proof (state)
this:
ell2_norm (\<lambda>i. c * x i) = \<Squnion> (L2_set (cmod \<circ> (\<lambda>i. c * x i)) ` Collect finite)

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ell2_norm (\<lambda>i. c * x i) = \<Squnion> (L2_set (cmod \<circ> (\<lambda>i. c * x i)) ` Collect finite)

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x
[PROOF STEP]
have "\<dots> = (SUP F \<in> Collect finite. (cmod c * L2_set (cmod \<circ> x) F))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Squnion> (L2_set (cmod \<circ> (\<lambda>i. c * x i)) ` Collect finite) = (\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F)
[PROOF STEP]
using L2_set_mul
[PROOF STATE]
proof (prove)
using this:
L2_set (cmod \<circ> (\<lambda>i. c * x i)) ?F = cmod c * L2_set (cmod \<circ> x) ?F

goal (1 subgoal):
 1. \<Squnion> (L2_set (cmod \<circ> (\<lambda>i. c * x i)) ` Collect finite) = (\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<Squnion> (L2_set (cmod \<circ> (\<lambda>i. c * x i)) ` Collect finite) = (\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F)

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Squnion> (L2_set (cmod \<circ> (\<lambda>i. c * x i)) ` Collect finite) = (\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F)

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x
[PROOF STEP]
have "\<dots> = cmod c * ell2_norm x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = cmod c * ell2_norm x
[PROOF STEP]
proof (subst ell2_norm_L2_set)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. has_ell2_norm x
 2. (\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = cmod c * \<Squnion> (L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
show "has_ell2_norm x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_ell2_norm x
[PROOF STEP]
by (simp add: assms)
[PROOF STATE]
proof (state)
this:
has_ell2_norm x

goal (1 subgoal):
 1. (\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = cmod c * \<Squnion> (L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
show "(SUP F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = cmod c * \<Squnion> (L2_set (cmod \<circ> x) ` Collect finite)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = cmod c * \<Squnion> (L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
proof (subst continuous_at_Sup_mono [where f = "\<lambda>x. cmod c * x"])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. mono ((*) (cmod c))
 2. continuous (at_left (\<Squnion> (L2_set (cmod \<circ> x) ` Collect finite))) ((*) (cmod c))
 3. L2_set (cmod \<circ> x) ` Collect finite \<noteq> {}
 4. bdd_above (L2_set (cmod \<circ> x) ` Collect finite)
 5. (\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = \<Squnion> ((*) (cmod c) ` L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
show "mono ((*) (cmod c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono ((*) (cmod c))
[PROOF STEP]
by (simp add: mono_def ordered_comm_semiring_class.comm_mult_left_mono)
[PROOF STATE]
proof (state)
this:
mono ((*) (cmod c))

goal (4 subgoals):
 1. continuous (at_left (\<Squnion> (L2_set (cmod \<circ> x) ` Collect finite))) ((*) (cmod c))
 2. L2_set (cmod \<circ> x) ` Collect finite \<noteq> {}
 3. bdd_above (L2_set (cmod \<circ> x) ` Collect finite)
 4. (\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = \<Squnion> ((*) (cmod c) ` L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
show "continuous (at_left (\<Squnion> (L2_set (cmod \<circ> x) ` Collect finite))) ((*) (cmod c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous (at_left (\<Squnion> (L2_set (cmod \<circ> x) ` Collect finite))) ((*) (cmod c))
[PROOF STEP]
proof (rule continuous_mult)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. continuous (at_left (\<Squnion> (L2_set (cmod \<circ> x) ` Collect finite))) (\<lambda>x. cmod c)
 2. continuous (at_left (\<Squnion> (L2_set (cmod \<circ> x) ` Collect finite))) (\<lambda>x. x)
[PROOF STEP]
show "continuous (at_left (\<Squnion> (L2_set (cmod \<circ> x) ` Collect finite))) (\<lambda>x. cmod c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous (at_left (\<Squnion> (L2_set (cmod \<circ> x) ` Collect finite))) (\<lambda>x. cmod c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
continuous (at_left (\<Squnion> (L2_set (cmod \<circ> x) ` Collect finite))) (\<lambda>x. cmod c)

goal (1 subgoal):
 1. continuous (at_left (\<Squnion> (L2_set (cmod \<circ> x) ` Collect finite))) (\<lambda>x. x)
[PROOF STEP]
show "continuous (at_left (\<Squnion> (L2_set (cmod \<circ> x) ` Collect finite))) (\<lambda>x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. continuous (at_left (\<Squnion> (L2_set (cmod \<circ> x) ` Collect finite))) (\<lambda>x. x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
continuous (at_left (\<Squnion> (L2_set (cmod \<circ> x) ` Collect finite))) (\<lambda>x. x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
continuous (at_left (\<Squnion> (L2_set (cmod \<circ> x) ` Collect finite))) ((*) (cmod c))

goal (3 subgoals):
 1. L2_set (cmod \<circ> x) ` Collect finite \<noteq> {}
 2. bdd_above (L2_set (cmod \<circ> x) ` Collect finite)
 3. (\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = \<Squnion> ((*) (cmod c) ` L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
show "L2_set (cmod \<circ> x) ` Collect finite \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. L2_set (cmod \<circ> x) ` Collect finite \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
L2_set (cmod \<circ> x) ` Collect finite \<noteq> {}

goal (2 subgoals):
 1. bdd_above (L2_set (cmod \<circ> x) ` Collect finite)
 2. (\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = \<Squnion> ((*) (cmod c) ` L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
show "bdd_above (L2_set (cmod \<circ> x) ` Collect finite)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bdd_above (L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
by (meson assms has_ell2_norm_L2_set)
[PROOF STATE]
proof (state)
this:
bdd_above (L2_set (cmod \<circ> x) ` Collect finite)

goal (1 subgoal):
 1. (\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = \<Squnion> ((*) (cmod c) ` L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
show "(SUP F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = \<Squnion> ((*) (cmod c) ` L2_set (cmod \<circ> x) ` Collect finite)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = \<Squnion> ((*) (cmod c) ` L2_set (cmod \<circ> x) ` Collect finite)
[PROOF STEP]
by (metis image_image)
[PROOF STATE]
proof (state)
this:
(\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = \<Squnion> ((*) (cmod c) ` L2_set (cmod \<circ> x) ` Collect finite)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = cmod c * \<Squnion> (L2_set (cmod \<circ> x) ` Collect finite)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Squnion>F\<in>Collect finite. cmod c * L2_set (cmod \<circ> x) F) = cmod c * ell2_norm x

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x
[PROOF STEP]
show "ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x"
[PROOF STATE]
proof (prove)
using this:
ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x

goal (1 subgoal):
 1. ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ell2_norm (\<lambda>i. c * x i) = cmod c * ell2_norm x

goal:
No subgoals!
[PROOF STEP]
qed