74 subsection "properties of move" |
74 subsection "properties of move" |
75 |
75 |
76 declare Let_def [simp del] |
76 declare Let_def [simp del] |
77 |
77 |
78 lemma move_is_move_sim: |
78 lemma move_is_move_sim: |
79 "[|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==> |
79 "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==> |
80 let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
80 let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
81 (t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'" |
81 (t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'" |
82 apply (unfold is_simulation_def) |
82 apply (unfold is_simulation_def) |
83 |
83 |
84 (* Does not perform conditional rewriting on assumptions automatically as |
84 (* Does not perform conditional rewriting on assumptions automatically as |
103 done |
103 done |
104 |
104 |
105 declare Let_def [simp] |
105 declare Let_def [simp] |
106 |
106 |
107 lemma move_subprop1_sim: |
107 lemma move_subprop1_sim: |
108 "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> |
108 "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==> |
109 let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
109 let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
110 is_exec_frag A (s',@x. move A x s' a T')" |
110 is_exec_frag A (s',@x. move A x s' a T')" |
111 apply (cut_tac move_is_move_sim) |
111 apply (cut_tac move_is_move_sim) |
112 defer |
112 defer |
113 apply assumption+ |
113 apply assumption+ |
114 apply (simp add: move_def) |
114 apply (simp add: move_def) |
115 done |
115 done |
116 |
116 |
117 lemma move_subprop2_sim: |
117 lemma move_subprop2_sim: |
118 "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> |
118 "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==> |
119 let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
119 let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
120 Finite (@x. move A x s' a T')" |
120 Finite (@x. move A x s' a T')" |
121 apply (cut_tac move_is_move_sim) |
121 apply (cut_tac move_is_move_sim) |
122 defer |
122 defer |
123 apply assumption+ |
123 apply assumption+ |
124 apply (simp add: move_def) |
124 apply (simp add: move_def) |
125 done |
125 done |
126 |
126 |
127 lemma move_subprop3_sim: |
127 lemma move_subprop3_sim: |
128 "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> |
128 "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==> |
129 let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
129 let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
130 laststate (s',@x. move A x s' a T') = T'" |
130 laststate (s',@x. move A x s' a T') = T'" |
131 apply (cut_tac move_is_move_sim) |
131 apply (cut_tac move_is_move_sim) |
132 defer |
132 defer |
133 apply assumption+ |
133 apply assumption+ |
134 apply (simp add: move_def) |
134 apply (simp add: move_def) |
135 done |
135 done |
136 |
136 |
137 lemma move_subprop4_sim: |
137 lemma move_subprop4_sim: |
138 "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> |
138 "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==> |
139 let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
139 let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
140 mk_trace A$((@x. move A x s' a T')) = |
140 mk_trace A$((@x. move A x s' a T')) = |
141 (if a:ext A then a\<leadsto>nil else nil)" |
141 (if a:ext A then a\<leadsto>nil else nil)" |
142 apply (cut_tac move_is_move_sim) |
142 apply (cut_tac move_is_move_sim) |
143 defer |
143 defer |
144 apply assumption+ |
144 apply assumption+ |
145 apply (simp add: move_def) |
145 apply (simp add: move_def) |
146 done |
146 done |
147 |
147 |
148 lemma move_subprop5_sim: |
148 lemma move_subprop5_sim: |
149 "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==> |
149 "[|is_simulation R C A; reachable C s; s \<midarrow>a\<midarrow>C\<rightarrow> t; (s,s'):R|] ==> |
150 let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
150 let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in |
151 (t,T'):R" |
151 (t,T'):R" |
152 apply (cut_tac move_is_move_sim) |
152 apply (cut_tac move_is_move_sim) |
153 defer |
153 defer |
154 apply assumption+ |
154 apply assumption+ |