equal
deleted
inserted
replaced
115 with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0" |
115 with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0" |
116 by (clarsimp simp add: not_Err_eq) |
116 by (clarsimp simp add: not_Err_eq) |
117 |
117 |
118 from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def) |
118 from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def) |
119 also from w have "phi' = map OK (map ok_val phi')" |
119 also from w have "phi' = map OK (map ok_val phi')" |
120 apply (clarsimp simp add: wt_step_def not_Err_eq) |
120 by (auto simp add: wt_step_def not_Err_eq intro!: nth_equalityI) |
121 apply (rule map_id [symmetric]) |
|
122 apply (erule allE, erule impE, assumption) |
|
123 apply clarsimp |
|
124 done |
|
125 finally |
121 finally |
126 have check_types: |
122 have check_types: |
127 "check_types G maxs maxr (map OK (map ok_val phi'))" . |
123 "check_types G maxs maxr (map OK (map ok_val phi'))" . |
128 |
124 |
129 from l bounded |
125 from l bounded |