[STATEMENT]
lemma normalize_replace_primitive_matchexpr_preserves_normalized_not_has_disc:
    assumes n: "normalized_nnf_match m"
      and wf_disc_sel: "wf_disc_sel (disc, sel) C"
      and nodisc: "\<not> has_disc disc2 m"
      and replace_f: "\<And>a. \<not> has_disc disc2 (replace_f a)"
     shows "m'\<in> set (normalize_match (replace_primitive_matchexpr (disc,sel) replace_f m))
      \<Longrightarrow> \<not> has_disc disc2 m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_match (replace_primitive_matchexpr (disc, sel) replace_f m)) \<Longrightarrow> \<not> has_disc disc2 m'
[PROOF STEP]
apply(simp add: replace_primitive_matchexpr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_match (case primitive_extractor (disc, sel) m of (as, rst) \<Rightarrow> if as = [] then m else MatchAnd (andfold_MatchExp (map replace_f as)) rst)) \<Longrightarrow> \<not> has_disc disc2 m'
[PROOF STEP]
apply(case_tac "primitive_extractor (disc, sel) m", rename_tac as rst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst. \<lbrakk>m' \<in> set (normalize_match (case primitive_extractor (disc, sel) m of (as, rst) \<Rightarrow> if as = [] then m else MatchAnd (andfold_MatchExp (map replace_f as)) rst)); primitive_extractor (disc, sel) m = (as, rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 m'
[PROOF STEP]
apply(simp split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = ([], rst); as = []; m' \<in> set (normalize_match m)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 m'
 2. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<exists>x\<in>set (normalize_match (andfold_MatchExp (map replace_f as))). m' \<in> MatchAnd x ` set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 m'
[PROOF STEP]
using nodisc normalize_match_preserves_nodisc
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc disc2 m
\<lbrakk>\<not> has_disc ?disc ?m; ?m' \<in> set (normalize_match ?m)\<rbrakk> \<Longrightarrow> \<not> has_disc ?disc ?m'

goal (2 subgoals):
 1. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = ([], rst); as = []; m' \<in> set (normalize_match m)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 m'
 2. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<exists>x\<in>set (normalize_match (andfold_MatchExp (map replace_f as))). m' \<in> MatchAnd x ` set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 m'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<exists>x\<in>set (normalize_match (andfold_MatchExp (map replace_f as))). m' \<in> MatchAnd x ` set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 m'
[PROOF STEP]
apply(frule primitive_extractor_correct(4)[OF n wf_disc_sel])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<exists>x\<in>set (normalize_match (andfold_MatchExp (map replace_f as))). m' \<in> MatchAnd x ` set (normalize_match rst); \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 m'
[PROOF STEP]
apply(elim bexE, rename_tac x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst x. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' \<in> MatchAnd x ` set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 m'
[PROOF STEP]
apply(erule Set.imageE, rename_tac xright)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 m'
[PROOF STEP]
(*m' = MatchAnd x xright*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 m'
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 x \<and> \<not> has_disc disc2 xright
[PROOF STEP]
apply(intro conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 x
 2. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 xright
[PROOF STEP]
apply(rule normalize_match_preserves_nodisc, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (andfold_MatchExp (map replace_f as))
 2. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 xright
[PROOF STEP]
apply(rule andfold_MatchExp_not_discI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<forall>m\<in>set as. \<not> has_disc disc2 (replace_f m)
 2. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 xright
[PROOF STEP]
using replace_f
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc disc2 (replace_f ?a)

goal (2 subgoals):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<forall>m\<in>set as. \<not> has_disc disc2 (replace_f m)
 2. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 xright
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 xright
[PROOF STEP]
apply(rule normalize_match_preserves_nodisc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (?m85 as rst x xright)
 2. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> xright \<in> set (normalize_match (?m85 as rst x xright))
[PROOF STEP]
apply(insert nodisc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst); \<not> has_disc disc2 m\<rbrakk> \<Longrightarrow> \<not> has_disc disc2 (?m85 as rst x xright)
 2. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc disc2 m \<longrightarrow> \<not> has_disc disc2 rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst); \<not> has_disc disc2 m\<rbrakk> \<Longrightarrow> xright \<in> set (normalize_match (?m85 as rst x xright))
[PROOF STEP]
by(simp_all)


[STATEMENT]
lemma normalize_replace_primitive_matchexpr_preserves_normalized_not_has_disc_negated:
    assumes n: "normalized_nnf_match m"
      and wf_disc_sel: "wf_disc_sel (disc, sel) C"
      and nodisc: "\<not> has_disc_negated disc2 neg m"
      and replace_f: "\<And>a. \<not> has_disc_negated disc2 neg (replace_f a)"
     shows "m'\<in> set (normalize_match (replace_primitive_matchexpr (disc,sel) replace_f m))
      \<Longrightarrow> \<not> has_disc_negated disc2 neg m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_match (replace_primitive_matchexpr (disc, sel) replace_f m)) \<Longrightarrow> \<not> has_disc_negated disc2 neg m'
[PROOF STEP]
apply(simp add: replace_primitive_matchexpr_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_match (case primitive_extractor (disc, sel) m of (as, rst) \<Rightarrow> if as = [] then m else MatchAnd (andfold_MatchExp (map replace_f as)) rst)) \<Longrightarrow> \<not> has_disc_negated disc2 neg m'
[PROOF STEP]
apply(case_tac "primitive_extractor (disc, sel) m", rename_tac as rst)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst. \<lbrakk>m' \<in> set (normalize_match (case primitive_extractor (disc, sel) m of (as, rst) \<Rightarrow> if as = [] then m else MatchAnd (andfold_MatchExp (map replace_f as)) rst)); primitive_extractor (disc, sel) m = (as, rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg m'
[PROOF STEP]
apply(simp split: if_split_asm)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = ([], rst); as = []; m' \<in> set (normalize_match m)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg m'
 2. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<exists>x\<in>set (normalize_match (andfold_MatchExp (map replace_f as))). m' \<in> MatchAnd x ` set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg m'
[PROOF STEP]
using nodisc not_has_disc_normalize_match
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc_negated disc2 neg m
\<lbrakk>\<not> has_disc_negated ?disc ?neg ?m; ?m' \<in> set (normalize_match ?m)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated ?disc ?neg ?m'

goal (2 subgoals):
 1. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = ([], rst); as = []; m' \<in> set (normalize_match m)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg m'
 2. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<exists>x\<in>set (normalize_match (andfold_MatchExp (map replace_f as))). m' \<in> MatchAnd x ` set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg m'
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<exists>x\<in>set (normalize_match (andfold_MatchExp (map replace_f as))). m' \<in> MatchAnd x ` set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg m'
[PROOF STEP]
apply(frule primitive_extractor_correct(6)[OF n wf_disc_sel, where neg=neg])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<exists>x\<in>set (normalize_match (andfold_MatchExp (map replace_f as))). m' \<in> MatchAnd x ` set (normalize_match rst); \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg m'
[PROOF STEP]
apply(elim bexE, rename_tac x)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst x. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' \<in> MatchAnd x ` set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg m'
[PROOF STEP]
apply(erule Set.imageE, rename_tac xright)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg m'
[PROOF STEP]
(*m' = MatchAnd x xright*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg m'
[PROOF STEP]
apply(simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg x \<and> \<not> has_disc_negated disc2 neg xright
[PROOF STEP]
apply(intro conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg x
 2. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg xright
[PROOF STEP]
apply(rule not_has_disc_normalize_match, simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg (andfold_MatchExp (map replace_f as))
 2. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg xright
[PROOF STEP]
apply(rule andfold_MatchExp_not_disc_negatedI, simp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<forall>m\<in>set as. \<not> has_disc_negated disc2 neg (replace_f m)
 2. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg xright
[PROOF STEP]
using replace_f
[PROOF STATE]
proof (prove)
using this:
\<not> has_disc_negated disc2 neg (replace_f ?a)

goal (2 subgoals):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<forall>m\<in>set as. \<not> has_disc_negated disc2 neg (replace_f m)
 2. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg xright
[PROOF STEP]
apply blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg xright
[PROOF STEP]
apply(rule not_has_disc_normalize_match)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg (?m86 as rst x xright)
 2. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst)\<rbrakk> \<Longrightarrow> xright \<in> set (normalize_match (?m86 as rst x xright))
[PROOF STEP]
apply(insert nodisc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst); \<not> has_disc_negated disc2 neg m\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc2 neg (?m86 as rst x xright)
 2. \<And>as rst x xright. \<lbrakk>primitive_extractor (disc, sel) m = (as, rst); as \<noteq> []; \<forall>disc2. \<not> has_disc_negated disc2 neg m \<longrightarrow> \<not> has_disc_negated disc2 neg rst; x \<in> set (normalize_match (andfold_MatchExp (map replace_f as))); m' = MatchAnd x xright; xright \<in> set (normalize_match rst); \<not> has_disc_negated disc2 neg m\<rbrakk> \<Longrightarrow> xright \<in> set (normalize_match (?m86 as rst x xright))
[PROOF STEP]
by(simp_all)


[STATEMENT]
lemma rewrite_MultiportPorts_one:
  assumes generic: "primitive_matcher_generic \<beta>" and n: "normalized_nnf_match m"
  shows
    "matches (\<beta>, \<alpha>) (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m) a p \<longleftrightarrow>
      matches (\<beta>, \<alpha>) m a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. matches (\<beta>, \<alpha>) (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(rule replace_primitive_matchexpr[OF n wf_disc_sel_common_primitive(11)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>pt. matches (\<beta>, \<alpha>) (rewrite_MultiportPorts_one pt) a p = matches (\<beta>, \<alpha>) (negation_type_to_match_expr_f MultiportPorts pt) a p
[PROOF STEP]
apply(rule allI, rename_tac pt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pt. matches (\<beta>, \<alpha>) (rewrite_MultiportPorts_one pt) a p = matches (\<beta>, \<alpha>) (negation_type_to_match_expr_f MultiportPorts pt) a p
[PROOF STEP]
apply(case_tac pt)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>pt x1. pt = Pos x1 \<Longrightarrow> matches (\<beta>, \<alpha>) (rewrite_MultiportPorts_one pt) a p = matches (\<beta>, \<alpha>) (negation_type_to_match_expr_f MultiportPorts pt) a p
 2. \<And>pt x2. pt = Neg x2 \<Longrightarrow> matches (\<beta>, \<alpha>) (rewrite_MultiportPorts_one pt) a p = matches (\<beta>, \<alpha>) (negation_type_to_match_expr_f MultiportPorts pt) a p
[PROOF STEP]
apply(simp add: primitive_matcher_generic.MultiportPorts_single_rewrite_MatchOr[OF generic]; fail)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pt x2. pt = Neg x2 \<Longrightarrow> matches (\<beta>, \<alpha>) (rewrite_MultiportPorts_one pt) a p = matches (\<beta>, \<alpha>) (negation_type_to_match_expr_f MultiportPorts pt) a p
[PROOF STEP]
apply(simp add: primitive_matcher_generic.MultiportPorts_single_not_rewrite_MatchAnd[OF generic]; fail)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma "\<forall>a. \<not> disc (Src_Ports a) \<Longrightarrow> \<forall>a. \<not> disc (Dst_Ports a) \<Longrightarrow>
          normalized_n_primitive (disc, sel) f m \<Longrightarrow>
         \<forall>m' \<in> set (normalize_match (rewrite_MultiportPorts_one a)).
            normalized_n_primitive (disc, sel) f m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>a. \<not> disc (Src_Ports a); \<forall>a. \<not> disc (Dst_Ports a); normalized_n_primitive (disc, sel) f m\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_match (rewrite_MultiportPorts_one a)). normalized_n_primitive (disc, sel) f m'
[PROOF STEP]
apply(cases a)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x1. \<lbrakk>\<forall>a. \<not> disc (Src_Ports a); \<forall>a. \<not> disc (Dst_Ports a); normalized_n_primitive (disc, sel) f m; a = Pos x1\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_match (rewrite_MultiportPorts_one a)). normalized_n_primitive (disc, sel) f m'
 2. \<And>x2. \<lbrakk>\<forall>a. \<not> disc (Src_Ports a); \<forall>a. \<not> disc (Dst_Ports a); normalized_n_primitive (disc, sel) f m; a = Neg x2\<rbrakk> \<Longrightarrow> \<forall>m'\<in>set (normalize_match (rewrite_MultiportPorts_one a)). normalized_n_primitive (disc, sel) f m'
[PROOF STEP]
by(simp_all add: MatchOr_def)


[STATEMENT]
lemma rewrite_MultiportPorts_one_nodisc:
    "\<forall>a. \<not> disc (Src_Ports a) \<Longrightarrow> \<forall>a. \<not> disc (Dst_Ports a) \<Longrightarrow>
          \<not> has_disc disc (rewrite_MultiportPorts_one a)"
    "\<forall>a. \<not> disc (Src_Ports a) \<Longrightarrow> \<forall>a. \<not> disc (Dst_Ports a) \<Longrightarrow>
          \<not> has_disc_negated disc neg (rewrite_MultiportPorts_one a)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>\<forall>a. \<not> disc (Src_Ports a); \<forall>a. \<not> disc (Dst_Ports a)\<rbrakk> \<Longrightarrow> \<not> has_disc disc (rewrite_MultiportPorts_one a)) &&& (\<lbrakk>\<forall>a. \<not> disc (Src_Ports a); \<forall>a. \<not> disc (Dst_Ports a)\<rbrakk> \<Longrightarrow> \<not> has_disc_negated disc neg (rewrite_MultiportPorts_one a))
[PROOF STEP]
by(cases a, simp_all add: MatchOr_def)+


[STATEMENT]
lemma rewrite_MultiportPorts:
    assumes generic: "primitive_matcher_generic \<beta>"
    and n: "normalized_nnf_match m"
    shows
        "match_list (\<beta>, \<alpha>) (rewrite_MultiportPorts m) a p \<longleftrightarrow> matches (\<beta>, \<alpha>) m a p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_list (\<beta>, \<alpha>) (rewrite_MultiportPorts m) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
unfolding rewrite_MultiportPorts_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. match_list (\<beta>, \<alpha>) (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
apply(intro normalize_replace_primitive_matchexpr[OF n])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. normalized_nnf_match m \<Longrightarrow> matches (\<beta>, \<alpha>) (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m) a p = matches (\<beta>, \<alpha>) m a p
[PROOF STEP]
by(simp add: rewrite_MultiportPorts_one[OF generic])


[STATEMENT]
lemma rewrite_MultiportPorts_normalized_nnf_match:
      "m' \<in> set (rewrite_MultiportPorts m) \<Longrightarrow> normalized_nnf_match m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (rewrite_MultiportPorts m) \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
apply(simp add: rewrite_MultiportPorts_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
using normalized_nnf_match_normalize_match
[PROOF STATE]
proof (prove)
using this:
\<forall>m'\<in>set (normalize_match ?m). normalized_nnf_match m'

goal (1 subgoal):
 1. m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) \<Longrightarrow> normalized_nnf_match m'
[PROOF STEP]
by blast


[STATEMENT]
lemma rewrite_MultiportPorts_unchanged_if_not_has_disc:
  assumes n: "normalized_nnf_match m"
  and noDisc: "\<not> has_disc is_MultiportPorts m"
  shows "rewrite_MultiportPorts m = [m]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rewrite_MultiportPorts m = [m]
[PROOF STEP]
apply(simp add: rewrite_MultiportPorts_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m) = [m]
[PROOF STEP]
apply(subst replace_primitive_matchexpr_unchanged_if_not_has_disc[OF n
            wf_disc_sel_common_primitive(11) noDisc])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize_match m = [m]
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
normalized_nnf_match m

goal (1 subgoal):
 1. normalize_match m = [m]
[PROOF STEP]
by(fact normalize_match_already_normalized)


[STATEMENT]
lemma rewrite_MultiportPorts_preserves_normalized_n_primitive:
    assumes n: "normalized_nnf_match m"
      and disc2_noSrcPorts: "\<forall>a. \<not> disc2 (Src_Ports a)"
      and disc2_noDstPorts: "\<forall>a. \<not> disc2 (Dst_Ports a)"
    shows "m' \<in> set (rewrite_MultiportPorts m) \<Longrightarrow>
         normalized_n_primitive (disc2, sel2) f  m \<Longrightarrow>
          normalized_n_primitive (disc2, sel2) f m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<in> set (rewrite_MultiportPorts m); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
unfolding rewrite_MultiportPorts_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'
[PROOF STEP]
apply(rule normalize_replace_primitive_matchexpr_preserves_normalized_n_primitive[OF
                  n wf_disc_sel_common_primitive(11)])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a m'a. \<lbrakk>m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)); normalized_n_primitive (disc2, sel2) f m; m'a \<in> set (normalize_match (?replace_f a))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'a
 2. \<lbrakk>m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m
 3. \<lbrakk>m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)); normalized_n_primitive (disc2, sel2) f m\<rbrakk> \<Longrightarrow> m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) ?replace_f m))
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a m'a. \<lbrakk>m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)); normalized_n_primitive (disc2, sel2) f m; m'a \<in> set (normalize_match (rewrite_MultiportPorts_one a))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f m'a
[PROOF STEP]
apply(rename_tac a a')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a a'. \<lbrakk>m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)); normalized_n_primitive (disc2, sel2) f m; a' \<in> set (normalize_match (rewrite_MultiportPorts_one a))\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a'
[PROOF STEP]
apply(case_tac a)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a' x1. \<lbrakk>m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)); normalized_n_primitive (disc2, sel2) f m; a' \<in> set (normalize_match (rewrite_MultiportPorts_one a)); a = Pos x1\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a'
 2. \<And>a a' x2. \<lbrakk>m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)); normalized_n_primitive (disc2, sel2) f m; a' \<in> set (normalize_match (rewrite_MultiportPorts_one a)); a = Neg x2\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a'
[PROOF STEP]
apply(simp_all add: MatchOr_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a a' x1. \<lbrakk>m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)); normalized_n_primitive (disc2, sel2) f m; a' = Match (Src_Ports x1) \<or> a' = Match (Dst_Ports x1); a = Pos x1\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a'
 2. \<And>a a' x2. \<lbrakk>m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)); normalized_n_primitive (disc2, sel2) f m; a' = MatchAnd (MatchNot (Match (Src_Ports x2))) (MatchNot (Match (Dst_Ports x2))); a = Neg x2\<rbrakk> \<Longrightarrow> \<not> disc2 (Src_Ports x2) \<and> (\<not> disc2 (Src_Ports x2) \<longrightarrow> \<not> disc2 (Dst_Ports x2))
[PROOF STEP]
using disc2_noSrcPorts disc2_noDstPorts
[PROOF STATE]
proof (prove)
using this:
\<forall>a. \<not> disc2 (Src_Ports a)
\<forall>a. \<not> disc2 (Dst_Ports a)

goal (2 subgoals):
 1. \<And>a a' x1. \<lbrakk>m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)); normalized_n_primitive (disc2, sel2) f m; a' = Match (Src_Ports x1) \<or> a' = Match (Dst_Ports x1); a = Pos x1\<rbrakk> \<Longrightarrow> normalized_n_primitive (disc2, sel2) f a'
 2. \<And>a a' x2. \<lbrakk>m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)); normalized_n_primitive (disc2, sel2) f m; a' = MatchAnd (MatchNot (Match (Src_Ports x2))) (MatchNot (Match (Dst_Ports x2))); a = Neg x2\<rbrakk> \<Longrightarrow> \<not> disc2 (Src_Ports x2) \<and> (\<not> disc2 (Src_Ports x2) \<longrightarrow> \<not> disc2 (Dst_Ports x2))
[PROOF STEP]
by fastforce+


[STATEMENT]
lemma rewrite_MultiportPorts_preserves_normalized_not_has_disc:
    assumes n: "normalized_nnf_match m"
      and nodisc: "\<not> has_disc disc2 m"
      and disc2_noSrcPorts: "\<forall>a. \<not> disc2 (Src_Ports a)"
      and disc2_noDstPorts: "\<forall>a. \<not> disc2 (Dst_Ports a)"
     shows "m'\<in> set (rewrite_MultiportPorts m)
      \<Longrightarrow> \<not> has_disc disc2 m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (rewrite_MultiportPorts m) \<Longrightarrow> \<not> has_disc disc2 m'
[PROOF STEP]
apply(simp add: rewrite_MultiportPorts_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) \<Longrightarrow> \<not> has_disc disc2 m'
[PROOF STEP]
apply(rule normalize_replace_primitive_matchexpr_preserves_normalized_not_has_disc[OF n wf_disc_sel_common_primitive(11) nodisc])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) \<Longrightarrow> \<not> has_disc disc2 (?replace_f a)
 2. m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) \<Longrightarrow> m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) ?replace_f m))
[PROOF STEP]
by(simp_all add: rewrite_MultiportPorts_one_nodisc disc2_noSrcPorts disc2_noDstPorts)


[STATEMENT]
lemma rewrite_MultiportPorts_preserves_normalized_not_has_disc_negated:
    assumes n: "normalized_nnf_match m"
      and nodisc: "\<not> has_disc_negated disc2 neg m"
      and disc2_noSrcPorts: "\<forall>a. \<not> disc2 (Src_Ports a)"
      and disc2_noDstPorts: "\<forall>a. \<not> disc2 (Dst_Ports a)"
     shows "m'\<in> set (rewrite_MultiportPorts m)
      \<Longrightarrow> \<not> has_disc_negated disc2 neg m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (rewrite_MultiportPorts m) \<Longrightarrow> \<not> has_disc_negated disc2 neg m'
[PROOF STEP]
apply(simp add: rewrite_MultiportPorts_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) \<Longrightarrow> \<not> has_disc_negated disc2 neg m'
[PROOF STEP]
apply(rule normalize_replace_primitive_matchexpr_preserves_normalized_not_has_disc_negated[OF n wf_disc_sel_common_primitive(11) nodisc])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) \<Longrightarrow> \<not> has_disc_negated disc2 neg (?replace_f a)
 2. m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) \<Longrightarrow> m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) ?replace_f m))
[PROOF STEP]
by(simp_all add: rewrite_MultiportPorts_one_nodisc disc2_noSrcPorts disc2_noDstPorts)


[STATEMENT]
lemma rewrite_MultiportPorts_removes_MultiportsPorts:
    assumes n: "normalized_nnf_match m"
    shows "m' \<in> set (rewrite_MultiportPorts m) \<Longrightarrow> \<not> has_disc is_MultiportPorts m'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (rewrite_MultiportPorts m) \<Longrightarrow> \<not> has_disc is_MultiportPorts m'
[PROOF STEP]
apply(simp add: rewrite_MultiportPorts_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) \<Longrightarrow> \<not> has_disc is_MultiportPorts m'
[PROOF STEP]
apply(rule normalize_match_preserves_nodisc)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) \<Longrightarrow> \<not> has_disc is_MultiportPorts ?m
 2. m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) \<Longrightarrow> m' \<in> set (normalize_match ?m)
[PROOF STEP]
apply(simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) \<Longrightarrow> \<not> has_disc is_MultiportPorts (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)
[PROOF STEP]
apply(rule replace_primitive_matchexpr_replaces_disc[OF n wf_disc_sel_common_primitive(11)])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) \<Longrightarrow> \<forall>a. \<not> has_disc is_MultiportPorts (rewrite_MultiportPorts_one a)
[PROOF STEP]
apply(intro allI, rename_tac a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a. m' \<in> set (normalize_match (replace_primitive_matchexpr (is_MultiportPorts, multiportports_sel) rewrite_MultiportPorts_one m)) \<Longrightarrow> \<not> has_disc is_MultiportPorts (rewrite_MultiportPorts_one a)
[PROOF STEP]
by(case_tac a, simp_all add: MatchOr_def)


[STATEMENT]
lemma utility_le: "x \<preceq>[le] y \<Longrightarrow> u x \<le> u y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. le x y \<Longrightarrow> u x \<le> u y
[PROOF STEP]
using not_outside[of x y] utility_le_iff
[PROOF STATE]
proof (prove)
using this:
le x y \<Longrightarrow> x \<in> carrier
le x y \<Longrightarrow> y \<in> carrier
\<lbrakk>?x \<in> carrier; ?y \<in> carrier\<rbrakk> \<Longrightarrow> (u ?x \<le> u ?y) = le ?x ?y

goal (1 subgoal):
 1. le x y \<Longrightarrow> u x \<le> u y
[PROOF STEP]
by simp


[STATEMENT]
lemma utility_less_iff:
  "x \<in> carrier \<Longrightarrow> y \<in> carrier \<Longrightarrow> u x < u y \<longleftrightarrow> x \<prec>[le] y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier; y \<in> carrier\<rbrakk> \<Longrightarrow> (u x < u y) = x \<prec>[le] y
[PROOF STEP]
using utility_le_iff[of x y] utility_le_iff[of y x]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<in> carrier; y \<in> carrier\<rbrakk> \<Longrightarrow> (u x \<le> u y) = le x y
\<lbrakk>y \<in> carrier; x \<in> carrier\<rbrakk> \<Longrightarrow> (u y \<le> u x) = le y x

goal (1 subgoal):
 1. \<lbrakk>x \<in> carrier; y \<in> carrier\<rbrakk> \<Longrightarrow> (u x < u y) = x \<prec>[le] y
[PROOF STEP]
by (auto simp: strongly_preferred_def)


[STATEMENT]
lemma utility_less: "x \<prec>[le] y \<Longrightarrow> u x < u y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<prec>[le] y \<Longrightarrow> u x < u y
[PROOF STEP]
using not_outside[of x y] utility_less_iff
[PROOF STATE]
proof (prove)
using this:
le x y \<Longrightarrow> x \<in> carrier
le x y \<Longrightarrow> y \<in> carrier
\<lbrakk>?x \<in> carrier; ?y \<in> carrier\<rbrakk> \<Longrightarrow> (u ?x < u ?y) = ?x \<prec>[le] ?y

goal (1 subgoal):
 1. x \<prec>[le] y \<Longrightarrow> u x < u y
[PROOF STEP]
by (simp add: strongly_preferred_def)


[STATEMENT]
lemma expected_utility_weak_ranking:
  assumes "p \<in> lotteries_on carrier"
  shows   "measure_pmf.expectation p u =
             (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
p \<in> lotteries_on carrier
[PROOF STEP]
have "measure_pmf.expectation p u = (\<Sum>a\<in>carrier. u a * pmf p a)"
[PROOF STATE]
proof (prove)
using this:
p \<in> lotteries_on carrier

goal (1 subgoal):
 1. measure_pmf.expectation p u = (\<Sum>a\<in>carrier. u a * pmf p a)
[PROOF STEP]
by (subst integral_measure_pmf[OF finite_carrier])
       (auto simp: lotteries_on_def ac_simps)
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation p u = (\<Sum>a\<in>carrier. u a * pmf p a)

goal (1 subgoal):
 1. measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation p u = (\<Sum>a\<in>carrier. u a * pmf p a)

goal (1 subgoal):
 1. measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)
[PROOF STEP]
have carrier: "carrier = \<Union>(set (weak_ranking le))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. carrier = \<Union> (set (weak_ranking le))
[PROOF STEP]
by (simp add: weak_ranking_Union)
[PROOF STATE]
proof (state)
this:
carrier = \<Union> (set (weak_ranking le))

goal (1 subgoal):
 1. measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
carrier = \<Union> (set (weak_ranking le))

goal (1 subgoal):
 1. measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)
[PROOF STEP]
from carrier
[PROOF STATE]
proof (chain)
picking this:
carrier = \<Union> (set (weak_ranking le))
[PROOF STEP]
have finite: "finite A" if "A \<in> set (weak_ranking le)" for A
[PROOF STATE]
proof (prove)
using this:
carrier = \<Union> (set (weak_ranking le))

goal (1 subgoal):
 1. finite A
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
carrier = \<Union> (set (weak_ranking le))
A \<in> set (weak_ranking le)

goal (1 subgoal):
 1. finite A
[PROOF STEP]
by (blast intro!: finite_subset[OF _ finite_carrier, of A])
[PROOF STATE]
proof (state)
this:
?A \<in> set (weak_ranking le) \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)
[PROOF STEP]
hence "(\<Sum>a\<in>\<Union>(set (weak_ranking le)). u a * pmf p a) =
           (\<Sum>A\<leftarrow>weak_ranking le. \<Sum>a\<in>A. u a * pmf p a)" (is "_ = sum_list ?xs")
[PROOF STATE]
proof (prove)
using this:
?A \<in> set (weak_ranking le) \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. (\<Sum>a\<in>\<Union> (set (weak_ranking le)). u a * pmf p a) = sum_list (map (sum (\<lambda>a. u a * pmf p a)) (weak_ranking le))
[PROOF STEP]
using weak_ranking_total_preorder
[PROOF STATE]
proof (prove)
using this:
?A \<in> set (weak_ranking le) \<Longrightarrow> finite ?A
is_weak_ranking (weak_ranking le)
of_weak_ranking (weak_ranking le) = le

goal (1 subgoal):
 1. (\<Sum>a\<in>\<Union> (set (weak_ranking le)). u a * pmf p a) = sum_list (map (sum (\<lambda>a. u a * pmf p a)) (weak_ranking le))
[PROOF STEP]
by (subst sum.Union_disjoint)
       (auto simp: is_weak_ranking_iff disjoint_def sum.distinct_set_conv_list)
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>\<Union> (set (weak_ranking le)). u a * pmf p a) = sum_list (map (sum (\<lambda>a. u a * pmf p a)) (weak_ranking le))

goal (1 subgoal):
 1. measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>a\<in>\<Union> (set (weak_ranking le)). u a * pmf p a) = sum_list (map (sum (\<lambda>a. u a * pmf p a)) (weak_ranking le))

goal (1 subgoal):
 1. measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)
[PROOF STEP]
have "?xs  = map (\<lambda>A. \<Sum>a\<in>A. u (SOME a. a\<in>A) * pmf p a) (weak_ranking le)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (sum (\<lambda>a. u a * pmf p a)) (weak_ranking le) = map (\<lambda>A. \<Sum>a\<in>A. u (SOME a. a \<in> A) * pmf p a) (weak_ranking le)
[PROOF STEP]
proof (intro map_cong HOL.refl sum.cong)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> set (weak_ranking le); xa \<in> x\<rbrakk> \<Longrightarrow> u xa * pmf p xa = u (SOME a. a \<in> x) * pmf p xa
[PROOF STEP]
fix x A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> set (weak_ranking le); xa \<in> x\<rbrakk> \<Longrightarrow> u xa * pmf p xa = u (SOME a. a \<in> x) * pmf p xa
[PROOF STEP]
assume x: "x \<in> A" and A: "A \<in> set (weak_ranking le)"
[PROOF STATE]
proof (state)
this:
x \<in> A
A \<in> set (weak_ranking le)

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> set (weak_ranking le); xa \<in> x\<rbrakk> \<Longrightarrow> u xa * pmf p xa = u (SOME a. a \<in> x) * pmf p xa
[PROOF STEP]
have "(SOME x. x \<in> A) \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SOME x. x \<in> A) \<in> A
[PROOF STEP]
by (rule someI_ex) (insert x, blast)
[PROOF STATE]
proof (state)
this:
(SOME x. x \<in> A) \<in> A

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> set (weak_ranking le); xa \<in> x\<rbrakk> \<Longrightarrow> u xa * pmf p xa = u (SOME a. a \<in> x) * pmf p xa
[PROOF STEP]
from weak_ranking_eqclass1[OF A x this] weak_ranking_eqclass1[OF A this x] x this A
[PROOF STATE]
proof (chain)
picking this:
le x (SOME x. x \<in> A)
le (SOME x. x \<in> A) x
x \<in> A
(SOME x. x \<in> A) \<in> A
A \<in> set (weak_ranking le)
[PROOF STEP]
have "u x = u (SOME x. x \<in> A)"
[PROOF STATE]
proof (prove)
using this:
le x (SOME x. x \<in> A)
le (SOME x. x \<in> A) x
x \<in> A
(SOME x. x \<in> A) \<in> A
A \<in> set (weak_ranking le)

goal (1 subgoal):
 1. u x = u (SOME x. x \<in> A)
[PROOF STEP]
by (intro antisym; subst utility_le_iff) (auto simp: carrier)
[PROOF STATE]
proof (state)
this:
u x = u (SOME x. x \<in> A)

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>x \<in> set (weak_ranking le); xa \<in> x\<rbrakk> \<Longrightarrow> u xa * pmf p xa = u (SOME a. a \<in> x) * pmf p xa
[PROOF STEP]
thus "u x * pmf p x = u (SOME x. x \<in> A) * pmf p x"
[PROOF STATE]
proof (prove)
using this:
u x = u (SOME x. x \<in> A)

goal (1 subgoal):
 1. u x * pmf p x = u (SOME x. x \<in> A) * pmf p x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
u x * pmf p x = u (SOME x. x \<in> A) * pmf p x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map (sum (\<lambda>a. u a * pmf p a)) (weak_ranking le) = map (\<lambda>A. \<Sum>a\<in>A. u (SOME a. a \<in> A) * pmf p a) (weak_ranking le)

goal (1 subgoal):
 1. measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map (sum (\<lambda>a. u a * pmf p a)) (weak_ranking le) = map (\<lambda>A. \<Sum>a\<in>A. u (SOME a. a \<in> A) * pmf p a) (weak_ranking le)

goal (1 subgoal):
 1. measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)
[PROOF STEP]
have "\<dots> = map (\<lambda>A. u (SOME a. a \<in> A) * measure_pmf.prob p A) (weak_ranking le)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>A. \<Sum>a\<in>A. u (SOME a. a \<in> A) * pmf p a) (weak_ranking le) = map (\<lambda>A. u (SOME a. a \<in> A) * measure_pmf.prob p A) (weak_ranking le)
[PROOF STEP]
using finite
[PROOF STATE]
proof (prove)
using this:
?A \<in> set (weak_ranking le) \<Longrightarrow> finite ?A

goal (1 subgoal):
 1. map (\<lambda>A. \<Sum>a\<in>A. u (SOME a. a \<in> A) * pmf p a) (weak_ranking le) = map (\<lambda>A. u (SOME a. a \<in> A) * measure_pmf.prob p A) (weak_ranking le)
[PROOF STEP]
by (intro map_cong HOL.refl)
                    (auto simp: sum_distrib_left measure_measure_pmf_finite)
[PROOF STATE]
proof (state)
this:
map (\<lambda>A. \<Sum>a\<in>A. u (SOME a. a \<in> A) * pmf p a) (weak_ranking le) = map (\<lambda>A. u (SOME a. a \<in> A) * measure_pmf.prob p A) (weak_ranking le)

goal (1 subgoal):
 1. measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME a. a \<in> A) * measure_pmf.prob p A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME a. a \<in> A) * measure_pmf.prob p A)

goal (1 subgoal):
 1. measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
measure_pmf.expectation p u = (\<Sum>A\<leftarrow>weak_ranking le. u (SOME x. x \<in> A) * measure_pmf.prob p A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma scaled: "c > 0 \<Longrightarrow> vnm_utility carrier le (\<lambda>x. c * u x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < c \<Longrightarrow> vnm_utility carrier le (\<lambda>x. c * u x)
[PROOF STEP]
by unfold_locales (insert utility_le_iff, auto)


[STATEMENT]
lemma add_right:
  assumes "\<And>x y. le x y \<Longrightarrow> f x \<le> f y"
  shows   "vnm_utility carrier le (\<lambda>x. u x + f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vnm_utility carrier le (\<lambda>x. u x + f x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier; y \<in> carrier\<rbrakk> \<Longrightarrow> (u x + f x \<le> u y + f y) = le x y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier; y \<in> carrier\<rbrakk> \<Longrightarrow> (u x + f x \<le> u y + f y) = le x y
[PROOF STEP]
assume xy: "x \<in> carrier" "y \<in> carrier"
[PROOF STATE]
proof (state)
this:
x \<in> carrier
y \<in> carrier

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier; y \<in> carrier\<rbrakk> \<Longrightarrow> (u x + f x \<le> u y + f y) = le x y
[PROOF STEP]
from assms[of x y] utility_le_iff[OF xy] assms[of y x] utility_le_iff[OF xy(2,1)]
[PROOF STATE]
proof (chain)
picking this:
le x y \<Longrightarrow> f x \<le> f y
(u x \<le> u y) = le x y
le y x \<Longrightarrow> f y \<le> f x
(u y \<le> u x) = le y x
[PROOF STEP]
show "(u x + f x \<le> u y + f y) = le x y"
[PROOF STATE]
proof (prove)
using this:
le x y \<Longrightarrow> f x \<le> f y
(u x \<le> u y) = le x y
le y x \<Longrightarrow> f y \<le> f x
(u y \<le> u x) = le y x

goal (1 subgoal):
 1. (u x + f x \<le> u y + f y) = le x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u x + f x \<le> u y + f y) = le x y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma add_left:
  "(\<And>x y. le x y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> vnm_utility carrier le (\<lambda>x. f x + u x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. le x y \<Longrightarrow> f x \<le> f y) \<Longrightarrow> vnm_utility carrier le (\<lambda>x. f x + u x)
[PROOF STEP]
by (subst add.commute) (rule add_right)


[STATEMENT]
lemma add_epsilon:
  assumes A: "\<And>x y. le x y \<Longrightarrow> le y x \<Longrightarrow> f x = f y"
  shows "\<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
let ?A = "{(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f x > f y}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
have "?A = (\<lambda>(x,y). (u y - u x) / (f x - f y)) ` {(x,y) |x y. x \<prec>[le] y \<and> f x > f y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x} = (\<lambda>(x, y). (u y - u x) / (f x - f y)) ` {(x, y) |x y. x \<prec>[le] y \<and> f y < f x}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x} = (\<lambda>(x, y). (u y - u x) / (f x - f y)) ` {(x, y) |x y. x \<prec>[le] y \<and> f y < f x}

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x} = (\<lambda>(x, y). (u y - u x) / (f x - f y)) ` {(x, y) |x y. x \<prec>[le] y \<and> f y < f x}

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
have "finite {(x,y) |x y. x \<prec>[le] y \<and> f x > f y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {(x, y) |x y. x \<prec>[le] y \<and> f y < f x}
[PROOF STEP]
by (rule finite_subset[of _ "carrier \<times> carrier"])
       (insert not_outside, auto simp: strongly_preferred_def)
[PROOF STATE]
proof (state)
this:
finite {(x, y) |x y. x \<prec>[le] y \<and> f y < f x}

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
hence "finite ((\<lambda>(x,y). (u y - u x) / (f x - f y)) ` {(x,y) |x y. x \<prec>[le] y \<and> f x > f y})"
[PROOF STATE]
proof (prove)
using this:
finite {(x, y) |x y. x \<prec>[le] y \<and> f y < f x}

goal (1 subgoal):
 1. finite ((\<lambda>(x, y). (u y - u x) / (f x - f y)) ` {(x, y) |x y. x \<prec>[le] y \<and> f y < f x})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite ((\<lambda>(x, y). (u y - u x) / (f x - f y)) ` {(x, y) |x y. x \<prec>[le] y \<and> f y < f x})

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
finite {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}
[PROOF STEP]
have finite: "finite ?A"
[PROOF STATE]
proof (prove)
using this:
finite {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}

goal (1 subgoal):
 1. finite {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
finite {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
define \<epsilon> where "\<epsilon> = Min (insert 1 ?A) / 2"
[PROOF STATE]
proof (state)
this:
\<epsilon> = Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}) / 2

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
from finite
[PROOF STATE]
proof (chain)
picking this:
finite {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}
[PROOF STEP]
have "Min (insert 1 ?A) > 0"
[PROOF STATE]
proof (prove)
using this:
finite {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}

goal (1 subgoal):
 1. 0 < Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x})
[PROOF STEP]
by (auto intro!: divide_pos_pos simp: utility_less)
[PROOF STATE]
proof (state)
this:
0 < Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x})

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
hence \<epsilon>: "\<epsilon> > 0"
[PROOF STATE]
proof (prove)
using this:
0 < Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x})

goal (1 subgoal):
 1. 0 < \<epsilon>
[PROOF STEP]
unfolding \<epsilon>_def
[PROOF STATE]
proof (prove)
using this:
0 < Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x})

goal (1 subgoal):
 1. 0 < Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}) / 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < \<epsilon>

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
have mono: "u x + \<epsilon> * f x < u y + \<epsilon> * f y" if xy: "x \<prec>[le] y" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u x + \<epsilon> * f x < u y + \<epsilon> * f y
[PROOF STEP]
proof (cases "f x > f y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f y < f x \<Longrightarrow> u x + \<epsilon> * f x < u y + \<epsilon> * f y
 2. \<not> f y < f x \<Longrightarrow> u x + \<epsilon> * f x < u y + \<epsilon> * f y
[PROOF STEP]
assume less: "f x > f y"
[PROOF STATE]
proof (state)
this:
f y < f x

goal (2 subgoals):
 1. f y < f x \<Longrightarrow> u x + \<epsilon> * f x < u y + \<epsilon> * f y
 2. \<not> f y < f x \<Longrightarrow> u x + \<epsilon> * f x < u y + \<epsilon> * f y
[PROOF STEP]
from \<epsilon>
[PROOF STATE]
proof (chain)
picking this:
0 < \<epsilon>
[PROOF STEP]
have "\<epsilon> < Min (insert 1 ?A)"
[PROOF STATE]
proof (prove)
using this:
0 < \<epsilon>

goal (1 subgoal):
 1. \<epsilon> < Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x})
[PROOF STEP]
unfolding \<epsilon>_def
[PROOF STATE]
proof (prove)
using this:
0 < Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}) / 2

goal (1 subgoal):
 1. Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}) / 2 < Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x})
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<epsilon> < Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x})

goal (2 subgoals):
 1. f y < f x \<Longrightarrow> u x + \<epsilon> * f x < u y + \<epsilon> * f y
 2. \<not> f y < f x \<Longrightarrow> u x + \<epsilon> * f x < u y + \<epsilon> * f y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<epsilon> < Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x})

goal (2 subgoals):
 1. f y < f x \<Longrightarrow> u x + \<epsilon> * f x < u y + \<epsilon> * f y
 2. \<not> f y < f x \<Longrightarrow> u x + \<epsilon> * f x < u y + \<epsilon> * f y
[PROOF STEP]
from less xy finite
[PROOF STATE]
proof (chain)
picking this:
f y < f x
x \<prec>[le] y
finite {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}
[PROOF STEP]
have "Min (insert 1 ?A) \<le> (u y - u x) / (f x - f y)"
[PROOF STATE]
proof (prove)
using this:
f y < f x
x \<prec>[le] y
finite {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}

goal (1 subgoal):
 1. Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}) \<le> (u y - u x) / (f x - f y)
[PROOF STEP]
unfolding \<epsilon>_def
[PROOF STATE]
proof (prove)
using this:
f y < f x
x \<prec>[le] y
finite {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}

goal (1 subgoal):
 1. Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}) \<le> (u y - u x) / (f x - f y)
[PROOF STEP]
by (intro Min_le) auto
[PROOF STATE]
proof (state)
this:
Min (insert 1 {(u y - u x) / (f x - f y) |x y. x \<prec>[le] y \<and> f y < f x}) \<le> (u y - u x) / (f x - f y)

goal (2 subgoals):
 1. f y < f x \<Longrightarrow> u x + \<epsilon> * f x < u y + \<epsilon> * f y
 2. \<not> f y < f x \<Longrightarrow> u x + \<epsilon> * f x < u y + \<epsilon> * f y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<epsilon> < (u y - u x) / (f x - f y)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<epsilon> < (u y - u x) / (f x - f y)

goal (1 subgoal):
 1. u x + \<epsilon> * f x < u y + \<epsilon> * f y
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
\<epsilon> < (u y - u x) / (f x - f y)
f y < f x

goal (1 subgoal):
 1. u x + \<epsilon> * f x < u y + \<epsilon> * f y
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
u x + \<epsilon> * f x < u y + \<epsilon> * f y

goal (1 subgoal):
 1. \<not> f y < f x \<Longrightarrow> u x + \<epsilon> * f x < u y + \<epsilon> * f y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> f y < f x \<Longrightarrow> u x + \<epsilon> * f x < u y + \<epsilon> * f y
[PROOF STEP]
assume "\<not>f x > f y"
[PROOF STATE]
proof (state)
this:
\<not> f y < f x

goal (1 subgoal):
 1. \<not> f y < f x \<Longrightarrow> u x + \<epsilon> * f x < u y + \<epsilon> * f y
[PROOF STEP]
with utility_less[OF xy] \<epsilon>
[PROOF STATE]
proof (chain)
picking this:
u x < u y
0 < \<epsilon>
\<not> f y < f x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
u x < u y
0 < \<epsilon>
\<not> f y < f x

goal (1 subgoal):
 1. u x + \<epsilon> * f x < u y + \<epsilon> * f y
[PROOF STEP]
by (simp add: algebra_simps not_less add_less_le_mono)
[PROOF STATE]
proof (state)
this:
u x + \<epsilon> * f x < u y + \<epsilon> * f y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?x \<prec>[le] ?y \<Longrightarrow> u ?x + \<epsilon> * f ?x < u ?y + \<epsilon> * f ?y

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
have eq: "u x + \<epsilon> * f x = u y + \<epsilon> * f y" if xy: "x \<preceq>[le] y" "y \<preceq>[le] x" for x y
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u x + \<epsilon> * f x = u y + \<epsilon> * f y
[PROOF STEP]
using xy[THEN utility_le] A[OF xy]
[PROOF STATE]
proof (prove)
using this:
u x \<le> u y
u y \<le> u x
f x = f y

goal (1 subgoal):
 1. u x + \<epsilon> * f x = u y + \<epsilon> * f y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>le ?x ?y; le ?y ?x\<rbrakk> \<Longrightarrow> u ?x + \<epsilon> * f ?x = u ?y + \<epsilon> * f ?y

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
have "vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier; y \<in> carrier\<rbrakk> \<Longrightarrow> (u x + \<epsilon> * f x \<le> u y + \<epsilon> * f y) = le x y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier; y \<in> carrier\<rbrakk> \<Longrightarrow> (u x + \<epsilon> * f x \<le> u y + \<epsilon> * f y) = le x y
[PROOF STEP]
assume xy: "x \<in> carrier" "y \<in> carrier"
[PROOF STATE]
proof (state)
this:
x \<in> carrier
y \<in> carrier

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> carrier; y \<in> carrier\<rbrakk> \<Longrightarrow> (u x + \<epsilon> * f x \<le> u y + \<epsilon> * f y) = le x y
[PROOF STEP]
show "(u x + \<epsilon> * f x \<le> u y + \<epsilon> * f y) \<longleftrightarrow> le x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u x + \<epsilon> * f x \<le> u y + \<epsilon> * f y) = le x y
[PROOF STEP]
using total[OF xy] mono[of x y] mono[of y x] eq[of x y]
[PROOF STATE]
proof (prove)
using this:
le x y \<or> le y x
x \<prec>[le] y \<Longrightarrow> u x + \<epsilon> * f x < u y + \<epsilon> * f y
y \<prec>[le] x \<Longrightarrow> u y + \<epsilon> * f y < u x + \<epsilon> * f x
\<lbrakk>le x y; le y x\<rbrakk> \<Longrightarrow> u x + \<epsilon> * f x = u y + \<epsilon> * f y

goal (1 subgoal):
 1. (u x + \<epsilon> * f x \<le> u y + \<epsilon> * f y) = le x y
[PROOF STEP]
by (cases "le x y"; cases "le y x") (auto simp: strongly_preferred_def)
[PROOF STATE]
proof (state)
this:
(u x + \<epsilon> * f x \<le> u y + \<epsilon> * f y) = le x y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
from \<epsilon> this
[PROOF STATE]
proof (chain)
picking this:
0 < \<epsilon>
vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < \<epsilon>
vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * f x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diff_epsilon:
  assumes "\<And>x y. le x y \<Longrightarrow> le y x \<Longrightarrow> f x = f y"
  shows "\<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x - \<epsilon> * f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x - \<epsilon> * f x)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x - \<epsilon> * f x)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>le ?x ?y; le ?y ?x\<rbrakk> \<Longrightarrow> f ?x = f ?y
[PROOF STEP]
have "\<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * -f x)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>le ?x ?y; le ?y ?x\<rbrakk> \<Longrightarrow> f ?x = f ?y

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * - f x)
[PROOF STEP]
by (intro add_epsilon) (subst neg_equal_iff_equal)
[PROOF STATE]
proof (state)
this:
\<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * - f x)

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x - \<epsilon> * f x)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x + \<epsilon> * - f x)

goal (1 subgoal):
 1. \<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x - \<epsilon> * f x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>\<epsilon>>0. vnm_utility carrier le (\<lambda>x. u x - \<epsilon> * f x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma euclid:
  "rel_nabla (
    \<lceil>\<lambda>s::nat store. 0 < s ''y''\<rceil> ;
      ((''z'' ::= (\<lambda>s. s ''y'')) ;
      (''y'' ::= (\<lambda>s. s ''x'' mod s ''y'')) ;
      (''x'' ::= (\<lambda>s. s ''z''))))
    = {}
    \<Longrightarrow>
  PRE (\<lambda>s::nat store. s ''x'' = x \<and> s ''y'' = y)
   (WHILE (\<lambda>s. s ''y'' \<noteq> 0) INV (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y)
    DO
     (''z'' ::= (\<lambda>s. s ''y''));
     (''y'' ::= (\<lambda>s. s ''x'' mod s ''y''));
     (''x'' ::= (\<lambda>s. s ''z''))
    OD)
   POST (\<lambda>s. s ''x'' = gcd x y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_nabla (\<lceil>\<lambda>s. 0 < s ''y''\<rceil> ; ((''z'' ::= (\<lambda>s. s ''y'')) ; (''y'' ::= (\<lambda>s. s ''x'' mod s ''y'')) ; (''x'' ::= (\<lambda>s. s ''z'')))) = {} \<Longrightarrow> rdom \<lceil>\<lambda>s. s ''x'' = x \<and> s ''y'' = y\<rceil> \<subseteq> wp (WHILE (\<lambda>s. s ''y'' \<noteq> 0) INV (\<lambda>s. gcd (s ''x'') (s ''y'') = gcd x y) DO (''z'' ::= (\<lambda>s. s ''y'')) ; (''y'' ::= (\<lambda>s. s ''x'' mod s ''y'')) ; (''x'' ::= (\<lambda>s. s ''z'')) OD) \<lceil>\<lambda>s. s ''x'' = gcd x y\<rceil>
[PROOF STEP]
apply (subst rel_fdivka.fbox_arden_whilei[symmetric], simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_nabla (\<lceil>\<lambda>s. 0 < s ''y''\<rceil> ; ((''z'' ::= (\<lambda>s. s ''y'')) ; (''y'' ::= (\<lambda>s. s ''x'' mod s ''y'')) ; (''x'' ::= (\<lambda>s. s ''z'')))) = {} \<Longrightarrow> \<forall>s. (gcd (s ''x'') (s ''y'') = gcd x y) = ((0 < s ''y'' \<or> s ''x'' = gcd x y) \<and> (s ''y'' = 0 \<or> gcd (s ''y'') (s ''x'' mod s ''y'') = gcd x y))
[PROOF STEP]
using gcd_red_nat gr0I
[PROOF STATE]
proof (prove)
using this:
gcd ?x ?y = gcd ?y (?x mod ?y)
(?n = 0 \<Longrightarrow> False) \<Longrightarrow> 0 < ?n

goal (1 subgoal):
 1. rel_nabla (\<lceil>\<lambda>s. 0 < s ''y''\<rceil> ; ((''z'' ::= (\<lambda>s. s ''y'')) ; (''y'' ::= (\<lambda>s. s ''x'' mod s ''y'')) ; (''x'' ::= (\<lambda>s. s ''z'')))) = {} \<Longrightarrow> \<forall>s. (gcd (s ''x'') (s ''y'') = gcd x y) = ((0 < s ''y'' \<or> s ''x'' = gcd x y) \<and> (s ''y'' = 0 \<or> gcd (s ''y'') (s ''x'' mod s ''y'') = gcd x y))
[PROOF STEP]
by force


[STATEMENT]
lemma ren_init: "rc (init_config w) = ren.init_config (map ra w)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rc (init_config w) = ren.init_config (map ra w)
[PROOF STEP]
unfolding init_config_def ren.init_config_def rc.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Config\<^sub>S (rq s) (ra \<circ> (\<lambda>n. if n = 0 then LE else if n \<le> length w then w ! (n - 1) else blank)) 0 = Config\<^sub>S (rq s) (\<lambda>n. if n = 0 then ra LE else if n \<le> length (map ra w) then map ra w ! (n - 1) else ra blank) 0
[PROOF STEP]
by auto


[STATEMENT]
lemma ren_step: assumes "(c,c') \<in> step"
  shows "(rc c, rc c') \<in> ren.step"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rc c, rc c') \<in> ren.step
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(c, c') \<in> step

goal (1 subgoal):
 1. (rc c, rc c') \<in> ren.step
[PROOF STEP]
proof (cases rule: step.cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q ts n q' a dir. \<lbrakk>c = Config\<^sub>S q ts n; c' = Config\<^sub>S q' (ts(n := a)) (go_dir dir n); (q, ts n, q', a, dir) \<in> \<delta>\<rbrakk> \<Longrightarrow> (rc c, rc c') \<in> ren.step
[PROOF STEP]
case (step q ts n q' a dir)
[PROOF STATE]
proof (state)
this:
c = Config\<^sub>S q ts n
c' = Config\<^sub>S q' (ts(n := a)) (go_dir dir n)
(q, ts n, q', a, dir) \<in> \<delta>

goal (1 subgoal):
 1. \<And>q ts n q' a dir. \<lbrakk>c = Config\<^sub>S q ts n; c' = Config\<^sub>S q' (ts(n := a)) (go_dir dir n); (q, ts n, q', a, dir) \<in> \<delta>\<rbrakk> \<Longrightarrow> (rc c, rc c') \<in> ren.step
[PROOF STEP]
from step(3)
[PROOF STATE]
proof (chain)
picking this:
(q, ts n, q', a, dir) \<in> \<delta>
[PROOF STEP]
have mem: "(rq q, ra (ts n), rq q', ra a, dir) \<in> rd ` \<delta>"
[PROOF STATE]
proof (prove)
using this:
(q, ts n, q', a, dir) \<in> \<delta>

goal (1 subgoal):
 1. (rq q, ra (ts n), rq q', ra a, dir) \<in> rd ` \<delta>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(rq q, ra (ts n), rq q', ra a, dir) \<in> rd ` \<delta>

goal (1 subgoal):
 1. \<And>q ts n q' a dir. \<lbrakk>c = Config\<^sub>S q ts n; c' = Config\<^sub>S q' (ts(n := a)) (go_dir dir n); (q, ts n, q', a, dir) \<in> \<delta>\<rbrakk> \<Longrightarrow> (rc c, rc c') \<in> ren.step
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rc c, rc c') \<in> ren.step
[PROOF STEP]
unfolding step rc.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Config\<^sub>S (rq q) (ra \<circ> ts) n, Config\<^sub>S (rq q') (ra \<circ> ts(n := a)) (go_dir dir n)) \<in> ren.step
[PROOF STEP]
by (intro ren.stepI[OF mem], auto)
[PROOF STATE]
proof (state)
this:
(rc c, rc c') \<in> ren.step

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ren_steps: assumes "(c,c') \<in> step^*"
  shows "(rc c, rc c') \<in> ren.step^*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rc c, rc c') \<in> ren.step\<^sup>*
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(c, c') \<in> step\<^sup>*

goal (1 subgoal):
 1. (rc c, rc c') \<in> ren.step\<^sup>*
[PROOF STEP]
by (induct, insert ren_step, force+)


[STATEMENT]
lemma ren_steps_count: assumes "(c,c') \<in> step^^n"
  shows "(rc c, rc c') \<in> ren.step^^n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rc c, rc c') \<in> ren.step ^^ n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(c, c') \<in> step ^^ n

goal (1 subgoal):
 1. (rc c, rc c') \<in> ren.step ^^ n
[PROOF STEP]
by (induct n arbitrary: c c', insert ren_step, force+)


[STATEMENT]
lemma ren_Lang_forward: assumes "w \<in> Lang"
  shows "map ra w \<in> ren.Lang"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ra w \<in> ren.Lang
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map ra w \<in> ren.Lang
[PROOF STEP]
from assms[unfolded Lang_def, simplified]
[PROOF STATE]
proof (chain)
picking this:
set w \<subseteq> \<Sigma> \<and> (\<exists>w' n. (init_config w, Config\<^sub>S t w' n) \<in> step\<^sup>*)
[PROOF STEP]
obtain w' n where w: "set w \<subseteq> \<Sigma>" and steps: "(init_config w, Config\<^sub>S t w' n) \<in> step^*"
[PROOF STATE]
proof (prove)
using this:
set w \<subseteq> \<Sigma> \<and> (\<exists>w' n. (init_config w, Config\<^sub>S t w' n) \<in> step\<^sup>*)

goal (1 subgoal):
 1. (\<And>w' n. \<lbrakk>set w \<subseteq> \<Sigma>; (init_config w, Config\<^sub>S t w' n) \<in> step\<^sup>*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set w \<subseteq> \<Sigma>
(init_config w, Config\<^sub>S t w' n) \<in> step\<^sup>*

goal (1 subgoal):
 1. map ra w \<in> ren.Lang
[PROOF STEP]
from ren_steps[OF steps, unfolded ren_init, unfolded rc.simps] w
[PROOF STATE]
proof (chain)
picking this:
(ren.init_config (map ra w), Config\<^sub>S (rq t) (ra \<circ> w') n) \<in> ren.step\<^sup>*
set w \<subseteq> \<Sigma>
[PROOF STEP]
show "map ra w \<in> ren.Lang"
[PROOF STATE]
proof (prove)
using this:
(ren.init_config (map ra w), Config\<^sub>S (rq t) (ra \<circ> w') n) \<in> ren.step\<^sup>*
set w \<subseteq> \<Sigma>

goal (1 subgoal):
 1. map ra w \<in> ren.Lang
[PROOF STEP]
unfolding ren.Lang_def
[PROOF STATE]
proof (prove)
using this:
(ren.init_config (map ra w), Config\<^sub>S (rq t) (ra \<circ> w') n) \<in> ren.step\<^sup>*
set w \<subseteq> \<Sigma>

goal (1 subgoal):
 1. map ra w \<in> {w. set w \<subseteq> ra ` \<Sigma> \<and> (\<exists>w' n. (ren.init_config w, Config\<^sub>S (rq t) w' n) \<in> ren.step\<^sup>*)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map ra w \<in> ren.Lang

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_ren_Sigma: "ira ` ra ` \<Sigma> = \<Sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ira ` ra ` \<Sigma> = \<Sigma>
[PROOF STEP]
using inv_simps(1)[OF set_mp[OF \<Sigma>_sub_\<Gamma>]]
[PROOF STATE]
proof (prove)
using this:
?x \<in> \<Sigma> \<Longrightarrow> ira (ra ?x) = ?x

goal (1 subgoal):
 1. ira ` ra ` \<Sigma> = \<Sigma>
[PROOF STEP]
by (smt (verit, best) equalityI imageE image_subset_iff subsetI)


[STATEMENT]
lemma inv_ren_Gamma: "ira ` ra ` \<Gamma> = \<Gamma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ira ` ra ` \<Gamma> = \<Gamma>
[PROOF STEP]
using inv_simps(1)
[PROOF STATE]
proof (prove)
using this:
?x \<in> \<Gamma> \<Longrightarrow> ira (ra ?x) = ?x

goal (1 subgoal):
 1. ira ` ra ` \<Gamma> = \<Gamma>
[PROOF STEP]
by (smt (verit, best) equalityI imageE image_subset_iff subsetI)


[STATEMENT]
lemma inv_ren_t: "irq (rq t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irq (rq t) = t
[PROOF STEP]
using tQ
[PROOF STATE]
proof (prove)
using this:
t \<in> Q

goal (1 subgoal):
 1. irq (rq t) = t
[PROOF STEP]
by simp


[STATEMENT]
lemma inv_ren_s: "irq (rq s) = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irq (rq s) = s
[PROOF STEP]
using sQ
[PROOF STATE]
proof (prove)
using this:
s \<in> Q

goal (1 subgoal):
 1. irq (rq s) = s
[PROOF STEP]
by simp


[STATEMENT]
lemma inv_ren_r: "irq (rq r) = r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irq (rq r) = r
[PROOF STEP]
using rQ
[PROOF STATE]
proof (prove)
using this:
r \<in> Q

goal (1 subgoal):
 1. irq (rq r) = r
[PROOF STEP]
by simp


[STATEMENT]
lemma inv_ren_blank: "ira (ra blank) = blank"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ira (ra blank) = blank
[PROOF STEP]
using tm
[PROOF STATE]
proof (prove)
using this:
s \<in> Q
\<Sigma> \<subseteq> \<Gamma>
blank \<in> \<Gamma>
LE \<in> \<Gamma>

goal (1 subgoal):
 1. ira (ra blank) = blank
[PROOF STEP]
by simp


[STATEMENT]
lemma inv_ren_LE: "ira (ra LE) = LE"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ira (ra LE) = LE
[PROOF STEP]
using tm
[PROOF STATE]
proof (prove)
using this:
s \<in> Q
\<Sigma> \<subseteq> \<Gamma>
blank \<in> \<Gamma>
LE \<in> \<Gamma>

goal (1 subgoal):
 1. ira (ra LE) = LE
[PROOF STEP]
by simp


[STATEMENT]
lemma inv_ren_\<delta>: "inv.rd ` rd ` \<delta> = \<delta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
fix trans :: "('q \<times> 'a \<times> 'q \<times> 'a \<times> dir)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
obtain q a p b d where trans: "trans = (q,a,p,b,d)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q a p b d. trans = (q, a, p, b, d) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases trans, auto)
[PROOF STATE]
proof (state)
this:
trans = (q, a, p, b, d)

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
trans = (q, a, p, b, d)

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
assume t: "trans \<in> \<delta>"
[PROOF STATE]
proof (state)
this:
trans \<in> \<delta>

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
note mem = \<delta>[OF this[unfolded trans]]
[PROOF STATE]
proof (state)
this:
q \<in> Q
a \<in> \<Gamma>
p \<in> Q
b \<in> \<Gamma>

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
from t
[PROOF STATE]
proof (chain)
picking this:
trans \<in> \<delta>
[PROOF STEP]
have "inv.rd (rd trans) \<in> inv.rd ` rd ` \<delta>"
[PROOF STATE]
proof (prove)
using this:
trans \<in> \<delta>

goal (1 subgoal):
 1. inv.rd (rd trans) \<in> inv.rd ` rd ` \<delta>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inv.rd (rd trans) \<in> inv.rd ` rd ` \<delta>

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
inv.rd (rd trans) \<in> inv.rd ` rd ` \<delta>

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
have "inv.rd (rd trans) = trans"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv.rd (rd trans) = trans
[PROOF STEP]
unfolding trans
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv.rd (rd (q, a, p, b, d)) = (q, a, p, b, d)
[PROOF STEP]
using mem
[PROOF STATE]
proof (prove)
using this:
q \<in> Q
a \<in> \<Gamma>
p \<in> Q
b \<in> \<Gamma>

goal (1 subgoal):
 1. inv.rd (rd (q, a, p, b, d)) = (q, a, p, b, d)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
inv.rd (rd trans) = trans

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
trans \<in> inv.rd ` rd ` \<delta>
[PROOF STEP]
have "trans \<in> inv.rd ` rd ` \<delta>"
[PROOF STATE]
proof (prove)
using this:
trans \<in> inv.rd ` rd ` \<delta>

goal (1 subgoal):
 1. trans \<in> inv.rd ` rd ` \<delta>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
trans \<in> inv.rd ` rd ` \<delta>

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
trans \<in> \<delta> \<Longrightarrow> trans \<in> inv.rd ` rd ` \<delta>

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
trans \<in> \<delta> \<Longrightarrow> trans \<in> inv.rd ` rd ` \<delta>

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
trans \<in> \<delta> \<Longrightarrow> trans \<in> inv.rd ` rd ` \<delta>

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
assume t: "trans \<in> inv.rd ` rd ` \<delta>"
[PROOF STATE]
proof (state)
this:
trans \<in> inv.rd ` rd ` \<delta>

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
trans \<in> inv.rd ` rd ` \<delta>
[PROOF STEP]
obtain t' where t'd: "t' \<in> \<delta>" and tra: "trans = inv.rd (rd t')"
[PROOF STATE]
proof (prove)
using this:
trans \<in> inv.rd ` rd ` \<delta>

goal (1 subgoal):
 1. (\<And>t'. \<lbrakk>t' \<in> \<delta>; trans = inv.rd (rd t')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
t' \<in> \<delta>
trans = inv.rd (rd t')

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
obtain q' a' p' b' d' where t': "t' = (q',a',p',b',d')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q' a' p' b' d'. t' = (q', a', p', b', d') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases t', auto)
[PROOF STATE]
proof (state)
this:
t' = (q', a', p', b', d')

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
note mem = \<delta>[OF t'd[unfolded t']]
[PROOF STATE]
proof (state)
this:
q' \<in> Q
a' \<in> \<Gamma>
p' \<in> Q
b' \<in> \<Gamma>

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
from tra[unfolded trans t'] mem
[PROOF STATE]
proof (chain)
picking this:
(q, a, p, b, d) = inv.rd (rd (q', a', p', b', d'))
q' \<in> Q
a' \<in> \<Gamma>
p' \<in> Q
b' \<in> \<Gamma>
[PROOF STEP]
have id: "q' = q" "a' = a" "p' = p" "b' = b" "d' = d"
[PROOF STATE]
proof (prove)
using this:
(q, a, p, b, d) = inv.rd (rd (q', a', p', b', d'))
q' \<in> Q
a' \<in> \<Gamma>
p' \<in> Q
b' \<in> \<Gamma>

goal (1 subgoal):
 1. (q' = q &&& a' = a) &&& p' = p &&& b' = b &&& d' = d
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q' = q
a' = a
p' = p
b' = b
d' = d

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
with trans t'd t'
[PROOF STATE]
proof (chain)
picking this:
trans = (q, a, p, b, d)
t' \<in> \<delta>
t' = (q', a', p', b', d')
q' = q
a' = a
p' = p
b' = b
d' = d
[PROOF STEP]
have "trans \<in> \<delta>"
[PROOF STATE]
proof (prove)
using this:
trans = (q, a, p, b, d)
t' \<in> \<delta>
t' = (q', a', p', b', d')
q' = q
a' = a
p' = p
b' = b
d' = d

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

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
trans \<in> inv.rd ` rd ` \<delta> \<Longrightarrow> trans \<in> \<delta>

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
trans \<in> \<delta> \<Longrightarrow> trans \<in> inv.rd ` rd ` \<delta>
trans \<in> inv.rd ` rd ` \<delta> \<Longrightarrow> trans \<in> \<delta>
[PROOF STEP]
have "trans \<in> inv.rd ` rd ` \<delta> \<longleftrightarrow> trans \<in> \<delta>"
[PROOF STATE]
proof (prove)
using this:
trans \<in> \<delta> \<Longrightarrow> trans \<in> inv.rd ` rd ` \<delta>
trans \<in> inv.rd ` rd ` \<delta> \<Longrightarrow> trans \<in> \<delta>

goal (1 subgoal):
 1. (trans \<in> inv.rd ` rd ` \<delta>) = (trans \<in> \<delta>)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(trans \<in> inv.rd ` rd ` \<delta>) = (trans \<in> \<delta>)

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?trans2 \<in> inv.rd ` rd ` \<delta>) = (?trans2 \<in> \<delta>)

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(?trans2 \<in> inv.rd ` rd ` \<delta>) = (?trans2 \<in> \<delta>)

goal (1 subgoal):
 1. inv.rd ` rd ` \<delta> = \<delta>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inv.rd ` rd ` \<delta> = \<delta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_ren_Lang: "inv.ren.Lang = Lang"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv.ren.Lang = Lang
[PROOF STEP]
unfolding inv_ren
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Lang = Lang
[PROOF STEP]
..


[STATEMENT]
lemma ren_Lang_backward: assumes "v \<in> ren.Lang"
  shows "\<exists> w. v = map ra w \<and> w \<in> Lang"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>w. v = map ra w \<and> w \<in> Lang
[PROOF STEP]
proof (intro exI conjI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v = map ra ?w
 2. ?w \<in> Lang
[PROOF STEP]
let ?w = "map ira v"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v = map ra ?w
 2. ?w \<in> Lang
[PROOF STEP]
from inv.ren_Lang_forward[OF assms, unfolded inv_ren_Lang]
[PROOF STATE]
proof (chain)
picking this:
map ira v \<in> Lang
[PROOF STEP]
show "?w \<in> Lang"
[PROOF STATE]
proof (prove)
using this:
map ira v \<in> Lang

goal (1 subgoal):
 1. map ira v \<in> Lang
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
map ira v \<in> Lang

goal (1 subgoal):
 1. v = map ra (map ira v)
[PROOF STEP]
show "v = map ra ?w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = map ra (map ira v)
[PROOF STEP]
unfolding map_map o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v = map (\<lambda>x. ra (ira x)) v
[PROOF STEP]
proof (subst map_idI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> set v \<Longrightarrow> ra (ira x) = x
 2. v = v
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> set v \<Longrightarrow> ra (ira x) = x
 2. v = v
[PROOF STEP]
assume "b \<in> set v"
[PROOF STATE]
proof (state)
this:
b \<in> set v

goal (2 subgoals):
 1. \<And>x. x \<in> set v \<Longrightarrow> ra (ira x) = x
 2. v = v
[PROOF STEP]
with assms[unfolded ren.Lang_def] \<Sigma>_sub_\<Gamma>
[PROOF STATE]
proof (chain)
picking this:
v \<in> {w. set w \<subseteq> ra ` \<Sigma> \<and> (\<exists>w' n. (ren.init_config w, Config\<^sub>S (rq t) w' n) \<in> ren.step\<^sup>*)}
\<Sigma> \<subseteq> \<Gamma>
b \<in> set v
[PROOF STEP]
obtain a where a: "a \<in> \<Gamma>" and b: "b = ra a"
[PROOF STATE]
proof (prove)
using this:
v \<in> {w. set w \<subseteq> ra ` \<Sigma> \<and> (\<exists>w' n. (ren.init_config w, Config\<^sub>S (rq t) w' n) \<in> ren.step\<^sup>*)}
\<Sigma> \<subseteq> \<Gamma>
b \<in> set v

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> \<Gamma>; b = ra a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> \<Gamma>
b = ra a

goal (2 subgoals):
 1. \<And>x. x \<in> set v \<Longrightarrow> ra (ira x) = x
 2. v = v
[PROOF STEP]
show "ra (ira b) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ra (ira b) = b
[PROOF STEP]
unfolding b
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ra (ira (ra a)) = ra a
[PROOF STEP]
using a
[PROOF STATE]
proof (prove)
using this:
a \<in> \<Gamma>

goal (1 subgoal):
 1. ra (ira (ra a)) = ra a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ra (ira b) = b

goal (1 subgoal):
 1. v = v
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
v = map ra (map ira v)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ren_Lang: "ren.Lang = map ra ` Lang"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ren.Lang = map ra ` Lang
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ren.Lang \<subseteq> map ra ` Lang
 2. map ra ` Lang \<subseteq> ren.Lang
[PROOF STEP]
show "map ra ` Lang \<subseteq> ren.Lang"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ra ` Lang \<subseteq> ren.Lang
[PROOF STEP]
using ren_Lang_forward
[PROOF STATE]
proof (prove)
using this:
?w \<in> Lang \<Longrightarrow> map ra ?w \<in> ren.Lang

goal (1 subgoal):
 1. map ra ` Lang \<subseteq> ren.Lang
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map ra ` Lang \<subseteq> ren.Lang

goal (1 subgoal):
 1. ren.Lang \<subseteq> map ra ` Lang
[PROOF STEP]
show "ren.Lang \<subseteq> map ra ` Lang"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ren.Lang \<subseteq> map ra ` Lang
[PROOF STEP]
using ren_Lang_backward
[PROOF STATE]
proof (prove)
using this:
?v \<in> ren.Lang \<Longrightarrow> \<exists>w. ?v = map ra w \<and> w \<in> Lang

goal (1 subgoal):
 1. ren.Lang \<subseteq> map ra ` Lang
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ren.Lang \<subseteq> map ra ` Lang

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ren_det: assumes "deterministic"
  shows "ren.deterministic"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ren.deterministic
[PROOF STEP]
unfolding ren.deterministic_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>q a p1 b1 d1 p2 b2 d2. (q, a, p1, b1, d1) \<in> rd ` \<delta> \<longrightarrow> (q, a, p2, b2, d2) \<in> rd ` \<delta> \<longrightarrow> (p1, b1, d1) = (p2, b2, d2)
[PROOF STEP]
proof (intro allI impI, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q a p1 b1 d1 p2 b2 d2. \<lbrakk>(q, a, p1, b1, d1) \<in> rd ` \<delta>; (q, a, p2, b2, d2) \<in> rd ` \<delta>\<rbrakk> \<Longrightarrow> (p1, b1, d1) = (p2, b2, d2)
[PROOF STEP]
case (1 q a p1 b1 d1 p2 b2 d2)
[PROOF STATE]
proof (state)
this:
(q, a, p1, b1, d1) \<in> rd ` \<delta>
(q, a, p2, b2, d2) \<in> rd ` \<delta>

goal (1 subgoal):
 1. \<And>q a p1 b1 d1 p2 b2 d2. \<lbrakk>(q, a, p1, b1, d1) \<in> rd ` \<delta>; (q, a, p2, b2, d2) \<in> rd ` \<delta>\<rbrakk> \<Longrightarrow> (p1, b1, d1) = (p2, b2, d2)
[PROOF STEP]
let ?t1 = "(q, a, p1, b1, d1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q a p1 b1 d1 p2 b2 d2. \<lbrakk>(q, a, p1, b1, d1) \<in> rd ` \<delta>; (q, a, p2, b2, d2) \<in> rd ` \<delta>\<rbrakk> \<Longrightarrow> (p1, b1, d1) = (p2, b2, d2)
[PROOF STEP]
let ?t2 = "(q, a, p2, b2, d2)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q a p1 b1 d1 p2 b2 d2. \<lbrakk>(q, a, p1, b1, d1) \<in> rd ` \<delta>; (q, a, p2, b2, d2) \<in> rd ` \<delta>\<rbrakk> \<Longrightarrow> (p1, b1, d1) = (p2, b2, d2)
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
(q, a, p1, b1, d1) \<in> rd ` \<delta>
(q, a, p2, b2, d2) \<in> rd ` \<delta>
[PROOF STEP]
have t1: "inv.rd ?t1 \<in> inv.rd ` rd ` \<delta>"
[PROOF STATE]
proof (prove)
using this:
(q, a, p1, b1, d1) \<in> rd ` \<delta>
(q, a, p2, b2, d2) \<in> rd ` \<delta>

goal (1 subgoal):
 1. inv.rd (q, a, p1, b1, d1) \<in> inv.rd ` rd ` \<delta>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
inv.rd (q, a, p1, b1, d1) \<in> inv.rd ` rd ` \<delta>

goal (1 subgoal):
 1. \<And>q a p1 b1 d1 p2 b2 d2. \<lbrakk>(q, a, p1, b1, d1) \<in> rd ` \<delta>; (q, a, p2, b2, d2) \<in> rd ` \<delta>\<rbrakk> \<Longrightarrow> (p1, b1, d1) = (p2, b2, d2)
[PROOF STEP]
from 1
[PROOF STATE]
proof (chain)
picking this:
(q, a, p1, b1, d1) \<in> rd ` \<delta>
(q, a, p2, b2, d2) \<in> rd ` \<delta>
[PROOF STEP]
have t2: "inv.rd ?t2 \<in> inv.rd ` rd ` \<delta>"
[PROOF STATE]
proof (prove)
using this:
(q, a, p1, b1, d1) \<in> rd ` \<delta>
(q, a, p2, b2, d2) \<in> rd ` \<delta>

goal (1 subgoal):
 1. inv.rd (q, a, p2, b2, d2) \<in> inv.rd ` rd ` \<delta>
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
inv.rd (q, a, p2, b2, d2) \<in> inv.rd ` rd ` \<delta>

goal (1 subgoal):
 1. \<And>q a p1 b1 d1 p2 b2 d2. \<lbrakk>(q, a, p1, b1, d1) \<in> rd ` \<delta>; (q, a, p2, b2, d2) \<in> rd ` \<delta>\<rbrakk> \<Longrightarrow> (p1, b1, d1) = (p2, b2, d2)
[PROOF STEP]
from t1 t2
[PROOF STATE]
proof (chain)
picking this:
inv.rd (q, a, p1, b1, d1) \<in> inv.rd ` rd ` \<delta>
inv.rd (q, a, p2, b2, d2) \<in> inv.rd ` rd ` \<delta>
[PROOF STEP]
have "(irq q, ira a, irq p1, ira b1, d1) \<in> \<delta>"  "(irq q, ira a, irq p2, ira b2, d2) \<in> \<delta>"
[PROOF STATE]
proof (prove)
using this:
inv.rd (q, a, p1, b1, d1) \<in> inv.rd ` rd ` \<delta>
inv.rd (q, a, p2, b2, d2) \<in> inv.rd ` rd ` \<delta>

goal (1 subgoal):
 1. (irq q, ira a, irq p1, ira b1, d1) \<in> \<delta> &&& (irq q, ira a, irq p2, ira b2, d2) \<in> \<delta>
[PROOF STEP]
unfolding inv_ren
[PROOF STATE]
proof (prove)
using this:
inv.rd (q, a, p1, b1, d1) \<in> \<delta>
inv.rd (q, a, p2, b2, d2) \<in> \<delta>

goal (1 subgoal):
 1. (irq q, ira a, irq p1, ira b1, d1) \<in> \<delta> &&& (irq q, ira a, irq p2, ira b2, d2) \<in> \<delta>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(irq q, ira a, irq p1, ira b1, d1) \<in> \<delta>
(irq q, ira a, irq p2, ira b2, d2) \<in> \<delta>

goal (1 subgoal):
 1. \<And>q a p1 b1 d1 p2 b2 d2. \<lbrakk>(q, a, p1, b1, d1) \<in> rd ` \<delta>; (q, a, p2, b2, d2) \<in> rd ` \<delta>\<rbrakk> \<Longrightarrow> (p1, b1, d1) = (p2, b2, d2)
[PROOF STEP]
from assms[unfolded deterministic_def, rule_format, OF this]
[PROOF STATE]
proof (chain)
picking this:
(irq p1, ira b1, d1) = (irq p2, ira b2, d2)
[PROOF STEP]
have id: "irq p1 = irq p2" "ira b1 = ira b2" and d: "d1 = d2"
[PROOF STATE]
proof (prove)
using this:
(irq p1, ira b1, d1) = (irq p2, ira b2, d2)

goal (1 subgoal):
 1. (irq p1 = irq p2 &&& ira b1 = ira b2) &&& d1 = d2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
irq p1 = irq p2
ira b1 = ira b2
d1 = d2

goal (1 subgoal):
 1. \<And>q a p1 b1 d1 p2 b2 d2. \<lbrakk>(q, a, p1, b1, d1) \<in> rd ` \<delta>; (q, a, p2, b2, d2) \<in> rd ` \<delta>\<rbrakk> \<Longrightarrow> (p1, b1, d1) = (p2, b2, d2)
[PROOF STEP]
from inj_onD[OF inv.rq id(1)] ren.\<delta>[OF 1(1)] ren.\<delta>[OF 1(2)]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>p1 \<in> rq ` Q; p2 \<in> rq ` Q\<rbrakk> \<Longrightarrow> p1 = p2
q \<in> rq ` Q
a \<in> ra ` \<Gamma>
p1 \<in> rq ` Q
b1 \<in> ra ` \<Gamma>
q \<in> rq ` Q
a \<in> ra ` \<Gamma>
p2 \<in> rq ` Q
b2 \<in> ra ` \<Gamma>
[PROOF STEP]
have p: "p1 = p2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>p1 \<in> rq ` Q; p2 \<in> rq ` Q\<rbrakk> \<Longrightarrow> p1 = p2
q \<in> rq ` Q
a \<in> ra ` \<Gamma>
p1 \<in> rq ` Q
b1 \<in> ra ` \<Gamma>
q \<in> rq ` Q
a \<in> ra ` \<Gamma>
p2 \<in> rq ` Q
b2 \<in> ra ` \<Gamma>

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

goal (1 subgoal):
 1. \<And>q a p1 b1 d1 p2 b2 d2. \<lbrakk>(q, a, p1, b1, d1) \<in> rd ` \<delta>; (q, a, p2, b2, d2) \<in> rd ` \<delta>\<rbrakk> \<Longrightarrow> (p1, b1, d1) = (p2, b2, d2)
[PROOF STEP]
from inj_onD[OF inv.ra id(2)] ren.\<delta>[OF 1(1)] ren.\<delta>[OF 1(2)]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>b1 \<in> ra ` \<Gamma>; b2 \<in> ra ` \<Gamma>\<rbrakk> \<Longrightarrow> b1 = b2
q \<in> rq ` Q
a \<in> ra ` \<Gamma>
p1 \<in> rq ` Q
b1 \<in> ra ` \<Gamma>
q \<in> rq ` Q
a \<in> ra ` \<Gamma>
p2 \<in> rq ` Q
b2 \<in> ra ` \<Gamma>
[PROOF STEP]
have b: "b1 = b2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>b1 \<in> ra ` \<Gamma>; b2 \<in> ra ` \<Gamma>\<rbrakk> \<Longrightarrow> b1 = b2
q \<in> rq ` Q
a \<in> ra ` \<Gamma>
p1 \<in> rq ` Q
b1 \<in> ra ` \<Gamma>
q \<in> rq ` Q
a \<in> ra ` \<Gamma>
p2 \<in> rq ` Q
b2 \<in> ra ` \<Gamma>

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

goal (1 subgoal):
 1. \<And>q a p1 b1 d1 p2 b2 d2. \<lbrakk>(q, a, p1, b1, d1) \<in> rd ` \<delta>; (q, a, p2, b2, d2) \<in> rd ` \<delta>\<rbrakk> \<Longrightarrow> (p1, b1, d1) = (p2, b2, d2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p1, b1, d1) = (p2, b2, d2)
[PROOF STEP]
unfolding b p d
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p2, b2, d2) = (p2, b2, d2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(p1, b1, d1) = (p2, b2, d2)

goal:
No subgoals!
[PROOF STEP]
qed