27 "f IncreasingWrt r/A == Increasing[A](r,f)" |
27 "f IncreasingWrt r/A == Increasing[A](r,f)" |
28 |
28 |
29 |
29 |
30 (** increasing **) |
30 (** increasing **) |
31 |
31 |
32 lemma increasing_type: "increasing[A](r, f) <= program" |
32 lemma increasing_type: "increasing[A](r, f) \<subseteq> program" |
33 by (unfold increasing_def, blast) |
33 by (unfold increasing_def, blast) |
34 |
34 |
35 lemma increasing_into_program: "F \<in> increasing[A](r, f) ==> F \<in> program" |
35 lemma increasing_into_program: "F \<in> increasing[A](r, f) ==> F \<in> program" |
36 by (unfold increasing_def, blast) |
36 by (unfold increasing_def, blast) |
37 |
37 |
45 apply (subgoal_tac "\<exists>x. x \<in> state") |
45 apply (subgoal_tac "\<exists>x. x \<in> state") |
46 apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state) |
46 apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state) |
47 done |
47 done |
48 |
48 |
49 lemma increasing_constant [simp]: |
49 lemma increasing_constant [simp]: |
50 "F \<in> increasing[A](r, %s. c) <-> F \<in> program & c \<in> A" |
50 "F \<in> increasing[A](r, %s. c) \<longleftrightarrow> F \<in> program & c \<in> A" |
51 apply (unfold increasing_def stable_def) |
51 apply (unfold increasing_def stable_def) |
52 apply (subgoal_tac "\<exists>x. x \<in> state") |
52 apply (subgoal_tac "\<exists>x. x \<in> state") |
53 apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state) |
53 apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state) |
54 done |
54 done |
55 |
55 |
56 lemma subset_increasing_comp: |
56 lemma subset_increasing_comp: |
57 "[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> |
57 "[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> |
58 increasing[A](r, f) <= increasing[B](s, g comp f)" |
58 increasing[A](r, f) \<subseteq> increasing[B](s, g comp f)" |
59 apply (unfold increasing_def stable_def part_order_def |
59 apply (unfold increasing_def stable_def part_order_def |
60 constrains_def mono1_def metacomp_def, clarify, simp) |
60 constrains_def mono1_def metacomp_def, clarify, simp) |
61 apply clarify |
61 apply clarify |
62 apply (subgoal_tac "xa \<in> state") |
62 apply (subgoal_tac "xa \<in> state") |
63 prefer 2 apply (blast dest!: ActsD) |
63 prefer 2 apply (blast dest!: ActsD) |
77 "[| F \<in> increasing[A](r, f); mono1(A, r, B, s, g); |
77 "[| F \<in> increasing[A](r, f); mono1(A, r, B, s, g); |
78 refl(A, r); trans[B](s) |] ==> F \<in> increasing[B](s, g comp f)" |
78 refl(A, r); trans[B](s) |] ==> F \<in> increasing[B](s, g comp f)" |
79 by (rule subset_increasing_comp [THEN subsetD], auto) |
79 by (rule subset_increasing_comp [THEN subsetD], auto) |
80 |
80 |
81 lemma strict_increasing: |
81 lemma strict_increasing: |
82 "increasing[nat](Le, f) <= increasing[nat](Lt, f)" |
82 "increasing[nat](Le, f) \<subseteq> increasing[nat](Lt, f)" |
83 by (unfold increasing_def Lt_def, auto) |
83 by (unfold increasing_def Lt_def, auto) |
84 |
84 |
85 lemma strict_gt_increasing: |
85 lemma strict_gt_increasing: |
86 "increasing[nat](Ge, f) <= increasing[nat](Gt, f)" |
86 "increasing[nat](Ge, f) \<subseteq> increasing[nat](Gt, f)" |
87 apply (unfold increasing_def Gt_def Ge_def, auto) |
87 apply (unfold increasing_def Gt_def Ge_def, auto) |
88 apply (erule natE) |
88 apply (erule natE) |
89 apply (auto simp add: stable_def) |
89 apply (auto simp add: stable_def) |
90 done |
90 done |
91 |
91 |
96 |
96 |
97 apply (unfold increasing_def Increasing_def) |
97 apply (unfold increasing_def Increasing_def) |
98 apply (auto intro: stable_imp_Stable) |
98 apply (auto intro: stable_imp_Stable) |
99 done |
99 done |
100 |
100 |
101 lemma Increasing_type: "Increasing[A](r, f) <= program" |
101 lemma Increasing_type: "Increasing[A](r, f) \<subseteq> program" |
102 by (unfold Increasing_def, auto) |
102 by (unfold Increasing_def, auto) |
103 |
103 |
104 lemma Increasing_into_program: "F \<in> Increasing[A](r, f) ==> F \<in> program" |
104 lemma Increasing_into_program: "F \<in> Increasing[A](r, f) ==> F \<in> program" |
105 by (unfold Increasing_def, auto) |
105 by (unfold Increasing_def, auto) |
106 |
106 |
114 apply (subgoal_tac "\<exists>x. x \<in> state") |
114 apply (subgoal_tac "\<exists>x. x \<in> state") |
115 apply (auto intro: st0_in_state) |
115 apply (auto intro: st0_in_state) |
116 done |
116 done |
117 |
117 |
118 lemma Increasing_constant [simp]: |
118 lemma Increasing_constant [simp]: |
119 "F \<in> Increasing[A](r, %s. c) <-> F \<in> program & (c \<in> A)" |
119 "F \<in> Increasing[A](r, %s. c) \<longleftrightarrow> F \<in> program & (c \<in> A)" |
120 apply (subgoal_tac "\<exists>x. x \<in> state") |
120 apply (subgoal_tac "\<exists>x. x \<in> state") |
121 apply (auto dest!: IncreasingD intro: st0_in_state increasing_imp_Increasing) |
121 apply (auto dest!: IncreasingD intro: st0_in_state increasing_imp_Increasing) |
122 done |
122 done |
123 |
123 |
124 lemma subset_Increasing_comp: |
124 lemma subset_Increasing_comp: |
125 "[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> |
125 "[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> |
126 Increasing[A](r, f) <= Increasing[B](s, g comp f)" |
126 Increasing[A](r, f) \<subseteq> Increasing[B](s, g comp f)" |
127 apply (unfold Increasing_def Stable_def Constrains_def part_order_def |
127 apply (unfold Increasing_def Stable_def Constrains_def part_order_def |
128 constrains_def mono1_def metacomp_def, safe) |
128 constrains_def mono1_def metacomp_def, safe) |
129 apply (simp_all add: ActsD) |
129 apply (simp_all add: ActsD) |
130 apply (subgoal_tac "xb \<in> state & xa \<in> state") |
130 apply (subgoal_tac "xb \<in> state & xa \<in> state") |
131 prefer 2 apply (simp add: ActsD) |
131 prefer 2 apply (simp add: ActsD) |
147 "[| F \<in> Increasing[A](r, f); mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] |
147 "[| F \<in> Increasing[A](r, f); mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] |
148 ==> F \<in> Increasing[B](s, g comp f)" |
148 ==> F \<in> Increasing[B](s, g comp f)" |
149 apply (rule subset_Increasing_comp [THEN subsetD], auto) |
149 apply (rule subset_Increasing_comp [THEN subsetD], auto) |
150 done |
150 done |
151 |
151 |
152 lemma strict_Increasing: "Increasing[nat](Le, f) <= Increasing[nat](Lt, f)" |
152 lemma strict_Increasing: "Increasing[nat](Le, f) \<subseteq> Increasing[nat](Lt, f)" |
153 by (unfold Increasing_def Lt_def, auto) |
153 by (unfold Increasing_def Lt_def, auto) |
154 |
154 |
155 lemma strict_gt_Increasing: "Increasing[nat](Ge, f)<= Increasing[nat](Gt, f)" |
155 lemma strict_gt_Increasing: "Increasing[nat](Ge, f)<= Increasing[nat](Gt, f)" |
156 apply (unfold Increasing_def Ge_def Gt_def, auto) |
156 apply (unfold Increasing_def Ge_def Gt_def, auto) |
157 apply (erule natE) |
157 apply (erule natE) |