equal
deleted
inserted
replaced
107 fix x xs; |
107 fix x xs; |
108 assume "??P xs"; |
108 assume "??P xs"; |
109 show "??P (x # xs)" (is "??Q x"); |
109 show "??P (x # xs)" (is "??Q x"); |
110 proof (induct ??Q x type: instr); |
110 proof (induct ??Q x type: instr); |
111 fix val; show "??Q (Const val)"; by brute_force; |
111 fix val; show "??Q (Const val)"; by brute_force; |
112 next; |
112 next; |
113 fix adr; show "??Q (Load adr)"; by brute_force; |
113 fix adr; show "??Q (Load adr)"; by brute_force; |
114 next; |
114 next; |
115 fix fun; show "??Q (Apply fun)"; by brute_force; |
115 fix fun; show "??Q (Apply fun)"; by brute_force; |
116 qed; |
116 qed; |
117 qed; |
117 qed; |
118 |
118 |
119 lemma exec_comp: |
119 lemma exec_comp: |
120 "ALL stack. exec (comp e) stack env = eval e env # stack" (is "??P e"); |
120 "ALL stack. exec (comp e) stack env = eval e env # stack" (is "??P e"); |
121 proof (induct ??P e type: expr); |
121 proof (induct ??P e type: expr); |
122 |
|
123 fix adr; show "??P (Variable adr)"; by brute_force; |
122 fix adr; show "??P (Variable adr)"; by brute_force; |
124 next; |
123 next; |
125 fix val; show "??P (Constant val)"; by brute_force; |
124 fix val; show "??P (Constant val)"; by brute_force; |
126 next; |
125 next; |
127 fix fun e1 e2; assume "??P e1" "??P e2"; show "??P (Binop fun e1 e2)"; |
126 fix fun e1 e2; assume "??P e1" "??P e2"; show "??P (Binop fun e1 e2)"; |
128 by (brute_force simp add: exec_append); |
127 by (brute_force simp add: exec_append); |
129 qed; |
128 qed; |
130 |
129 |
131 |
130 |