equal
deleted
inserted
replaced
866 proof(rule_tac x = i in exI, rule_tac x = ?f in exI, clarsimp) |
866 proof(rule_tac x = i in exI, rule_tac x = ?f in exI, clarsimp) |
867 fix x |
867 fix x |
868 assume h[rule_format]: |
868 assume h[rule_format]: |
869 "\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = i" |
869 "\<forall>k<length (sts' - sts). (sts' - sts) ! k = Bound \<longrightarrow> x ! k = i" |
870 from h1 h3 have p1: "l < length (sts' - sts)" |
870 from h1 h3 have p1: "l < length (sts' - sts)" |
871 by (metis length_list_update min_max.inf.idem minus_list_len) |
871 by (metis length_list_update min.idem minus_list_len) |
872 from p1 h2 h3 have p2: "(sts' - sts)!l = Bound" |
872 from p1 h2 h3 have p2: "(sts' - sts)!l = Bound" |
873 by (metis h1 minus_status.simps(2) nth_list_update_eq nth_sts_minus) |
873 by (metis h1 minus_status.simps(2) nth_list_update_eq nth_sts_minus) |
874 from h[OF p1 p2] have "(<(i = x ! l)>) 0" |
874 from h[OF p1 p2] have "(<(i = x ! l)>) 0" |
875 by (simp add:set_ins_def) |
875 by (simp add:set_ins_def) |
876 thus "\<exists> s. (<(i = x ! l)>) s" by auto |
876 thus "\<exists> s. (<(i = x ! l)>) s" by auto |
1672 lemma sts_list_plus_commut: |
1672 lemma sts_list_plus_commut: |
1673 shows "sts1 + sts2 = sts2 + (sts1:: status list)" |
1673 shows "sts1 + sts2 = sts2 + (sts1:: status list)" |
1674 proof(induct rule:nth_equalityI) |
1674 proof(induct rule:nth_equalityI) |
1675 case 1 |
1675 case 1 |
1676 show ?case |
1676 show ?case |
1677 by (metis min_max.inf.commute plus_list_len) |
1677 by (metis min.commute plus_list_len) |
1678 next |
1678 next |
1679 case 2 |
1679 case 2 |
1680 { fix i |
1680 { fix i |
1681 assume lt_i1: "i<length (sts1 + sts2)" |
1681 assume lt_i1: "i<length (sts1 + sts2)" |
1682 hence lt_i2: "i < length (sts2 + sts1)" |
1682 hence lt_i2: "i < length (sts2 + sts1)" |