20 by (dres_inst_tac [("x", "g s")] spec 1); |
20 by (dres_inst_tac [("x", "g s")] spec 1); |
21 by (etac LeadsTo_weaken 1); |
21 by (etac LeadsTo_weaken 1); |
22 by (ALLGOALS (blast_tac (claset() addIs [monoD, order_trans]))); |
22 by (ALLGOALS (blast_tac (claset() addIs [monoD, order_trans]))); |
23 qed "mono_LeadsTo_o"; |
23 qed "mono_LeadsTo_o"; |
24 |
24 |
25 (*NOT PROVABLE USING leadsETo because givenBy f <= givenBy (h o f) fails*) |
|
26 Goalw [Follows_def] "mono h ==> f Fols g <= (h o f) Fols (h o g)"; |
25 Goalw [Follows_def] "mono h ==> f Fols g <= (h o f) Fols (h o g)"; |
27 by (Clarify_tac 1); |
26 by (Clarify_tac 1); |
28 by (asm_full_simp_tac |
27 by (asm_full_simp_tac |
29 (simpset() addsimps [impOfSubs mono_Increasing_o, |
28 (simpset() addsimps [impOfSubs mono_Increasing_o, |
30 impOfSubs mono_Always_o, |
29 impOfSubs mono_Always_o, |
31 impOfSubs mono_LeadsTo_o RS INT_D]) 1); |
30 impOfSubs mono_LeadsTo_o RS INT_D]) 1); |
32 qed "mono_Follows_o"; |
31 qed "mono_Follows_o"; |
33 |
32 |
34 (*NOT PROVABLE USING leadsETo since it needs the previous thm*) |
|
35 Goal "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))"; |
33 Goal "mono h ==> f Fols g <= (%x. h (f x)) Fols (%x. h (g x))"; |
36 by (dtac mono_Follows_o 1); |
34 by (dtac mono_Follows_o 1); |
37 by (force_tac (claset(), simpset() addsimps [o_def]) 1); |
35 by (force_tac (claset(), simpset() addsimps [o_def]) 1); |
38 qed "mono_Follows_apply"; |
36 qed "mono_Follows_apply"; |
39 |
37 |
40 (*NOT PROVABLE USING leadsETo since givenBy g doesn't imply givenBy f*) |
|
41 Goalw [Follows_def] |
38 Goalw [Follows_def] |
42 "[| F : f Fols g; F: g Fols h |] ==> F : f Fols h"; |
39 "[| F : f Fols g; F: g Fols h |] ==> F : f Fols h"; |
43 by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1); |
40 by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1); |
44 by (blast_tac (claset() addIs [order_trans, LeadsTo_Trans]) 1); |
41 by (blast_tac (claset() addIs [order_trans, LeadsTo_Trans]) 1); |
45 qed "Follows_trans"; |
42 qed "Follows_trans"; |
46 |
|
47 (* |
|
48 try: |
|
49 by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1); |
|
50 by Auto_tac; |
|
51 by (blast_tac (claset() addIs [order_trans, LeadsETo_Trans]) 1); |
|
52 by (rtac LeadsETo_Trans 1); |
|
53 by (Blast_tac 2); |
|
54 by (dtac spec 1); |
|
55 by (etac LeadsETo_weaken 1); |
|
56 by Auto_tac; |
|
57 by (thin_tac "All ?P" 1); |
|
58 by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1); |
|
59 by Safe_tac; |
|
60 **) |
|
61 |
43 |
62 |
44 |
63 (** Destructiom rules **) |
45 (** Destructiom rules **) |
64 |
46 |
65 Goalw [Follows_def] |
47 Goalw [Follows_def] |
79 |
61 |
80 Goalw [Follows_def] |
62 Goalw [Follows_def] |
81 "F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}"; |
63 "F : f Fols g ==> F : {s. k <= g s} LeadsTo {s. k <= f s}"; |
82 by (Blast_tac 1); |
64 by (Blast_tac 1); |
83 qed "Follows_LeadsTo"; |
65 qed "Follows_LeadsTo"; |
|
66 |
|
67 Goal "F : f Fols g ==> F : {s. k pfixLe g s} LeadsTo {s. k pfixLe f s}"; |
|
68 by (rtac single_LeadsTo_I 1); |
|
69 by (Clarify_tac 1); |
|
70 by (dtac Follows_LeadsTo 1); |
|
71 by (etac LeadsTo_weaken 1); |
|
72 by (blast_tac set_cs 1); |
|
73 by (blast_tac (claset() addIs [pfixLe_trans, prefix_imp_pfixLe]) 1); |
|
74 qed "Follows_LeadsTo_pfixLe"; |
|
75 |
|
76 Goal "F : f Fols g ==> F : {s. k pfixGe g s} LeadsTo {s. k pfixGe f s}"; |
|
77 by (rtac single_LeadsTo_I 1); |
|
78 by (Clarify_tac 1); |
|
79 by (dtac Follows_LeadsTo 1); |
|
80 by (etac LeadsTo_weaken 1); |
|
81 by (blast_tac set_cs 1); |
|
82 by (blast_tac (claset() addIs [pfixGe_trans, prefix_imp_pfixGe]) 1); |
|
83 qed "Follows_LeadsTo_pfixGe"; |
84 |
84 |
85 |
85 |
86 (*Can replace "Un" by any sup. But existing max only works for linorders.*) |
86 (*Can replace "Un" by any sup. But existing max only works for linorders.*) |
87 |
87 |
88 Goalw [increasing_def, stable_def, constrains_def] |
88 Goalw [increasing_def, stable_def, constrains_def] |