21 |
21 |
22 Goalw [minSet_def] "x:A ==> minSet A = Some (LEAST x. x: A)"; |
22 Goalw [minSet_def] "x:A ==> minSet A = Some (LEAST x. x: A)"; |
23 by Auto_tac; |
23 by Auto_tac; |
24 qed_spec_mp "minSet_nonempty"; |
24 qed_spec_mp "minSet_nonempty"; |
25 |
25 |
26 Goal "F : (minSet -`` {Some x}) leadsTo (minSet -`` (Some``greaterThan x))"; |
26 Goal "F : (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))"; |
27 by (rtac leadsTo_weaken 1); |
27 by (rtac leadsTo_weaken 1); |
28 by (res_inst_tac [("x1","x")] ([UC2, UC1] MRS psp) 1); |
28 by (res_inst_tac [("x1","x")] ([UC2, UC1] MRS psp) 1); |
29 by Safe_tac; |
29 by Safe_tac; |
30 by (auto_tac (claset() addDs [minSet_eq_SomeD], |
30 by (auto_tac (claset() addDs [minSet_eq_SomeD], |
31 simpset() addsimps [linorder_neq_iff])); |
31 simpset() addsimps [linorder_neq_iff])); |
32 qed "minSet_greaterThan"; |
32 qed "minSet_greaterThan"; |
33 |
33 |
34 (*The induction*) |
34 (*The induction*) |
35 Goal "F : (UNIV-{{}}) leadsTo (minSet -`` (Some``atLeast y))"; |
35 Goal "F : (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))"; |
36 by (rtac leadsTo_weaken_R 1); |
36 by (rtac leadsTo_weaken_R 1); |
37 by (res_inst_tac [("l", "y"), ("f", "the o minSet"), ("B", "{}")] |
37 by (res_inst_tac [("l", "y"), ("f", "the o minSet"), ("B", "{}")] |
38 greaterThan_bounded_induct 1); |
38 greaterThan_bounded_induct 1); |
39 by Safe_tac; |
39 by Safe_tac; |
40 by (ALLGOALS Asm_simp_tac); |
40 by (ALLGOALS Asm_simp_tac); |