107 by (case_tac "s x --> s y" 1); |
107 by (case_tac "s x --> s y" 1); |
108 by (auto_tac (claset() addIs [less_imp_le], |
108 by (auto_tac (claset() addIs [less_imp_le], |
109 simpset() addsimps [fun_upd_idem])); |
109 simpset() addsimps [fun_upd_idem])); |
110 qed "metric_le"; |
110 qed "metric_le"; |
111 |
111 |
112 Goal "Rprg : LeadsTo ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))"; |
112 Goal "Rprg : ((metric-``{m}) - fixedpoint) LeadsTo (metric-``(lessThan m))"; |
113 by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1); |
113 by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1); |
114 by (rtac LeadsTo_UN 1); |
114 by (rtac LeadsTo_UN 1); |
115 by Auto_tac; |
115 by Auto_tac; |
116 by (ensures_tac "asgt a b" 1); |
116 by (ensures_tac "asgt a b" 1); |
117 by (Blast_tac 2); |
117 by (Blast_tac 2); |
119 by (dtac (metric_le RS le_anti_sym) 1); |
119 by (dtac (metric_le RS le_anti_sym) 1); |
120 by (auto_tac (claset() addEs [less_not_refl3 RSN (2, rev_notE)], |
120 by (auto_tac (claset() addEs [less_not_refl3 RSN (2, rev_notE)], |
121 simpset())); |
121 simpset())); |
122 qed "LeadsTo_Diff_fixedpoint"; |
122 qed "LeadsTo_Diff_fixedpoint"; |
123 |
123 |
124 Goal "Rprg : LeadsTo (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)"; |
124 Goal "Rprg : (metric-``{m}) LeadsTo (metric-``(lessThan m) Un fixedpoint)"; |
125 by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R, |
125 by (rtac ([LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R, |
126 subset_imp_LeadsTo] MRS LeadsTo_Diff) 1); |
126 subset_imp_LeadsTo] MRS LeadsTo_Diff) 1); |
127 by Auto_tac; |
127 by Auto_tac; |
128 qed "LeadsTo_Un_fixedpoint"; |
128 qed "LeadsTo_Un_fixedpoint"; |
129 |
129 |
130 |
130 |
131 (*Execution in any state leads to a fixedpoint (i.e. can terminate)*) |
131 (*Execution in any state leads to a fixedpoint (i.e. can terminate)*) |
132 Goal "Rprg : LeadsTo UNIV fixedpoint"; |
132 Goal "Rprg : UNIV LeadsTo fixedpoint"; |
133 by (rtac LessThan_induct 1); |
133 by (rtac LessThan_induct 1); |
134 by Auto_tac; |
134 by Auto_tac; |
135 by (rtac LeadsTo_Un_fixedpoint 1); |
135 by (rtac LeadsTo_Un_fixedpoint 1); |
136 qed "LeadsTo_fixedpoint"; |
136 qed "LeadsTo_fixedpoint"; |
137 |
137 |
138 Goal "Rprg : LeadsTo UNIV { %v. (init, v) : edges^* }"; |
138 Goal "Rprg : UNIV LeadsTo { %v. (init, v) : edges^* }"; |
139 by (stac (fixedpoint_invariant_correct RS sym) 1); |
139 by (stac (fixedpoint_invariant_correct RS sym) 1); |
140 by (rtac ([reach_invariant, LeadsTo_fixedpoint] |
140 by (rtac ([reach_invariant, LeadsTo_fixedpoint] |
141 MRS Invariant_LeadsTo_weaken) 1); |
141 MRS Invariant_LeadsTo_weaken) 1); |
142 by Auto_tac; |
142 by Auto_tac; |
143 qed "LeadsTo_correct"; |
143 qed "LeadsTo_correct"; |