1(* Title: ZF/UNITY/Increasing.thy 2 Author: Sidi O Ehmety, Cambridge University Computer Laboratory 3 Copyright 2001 University of Cambridge 4 5Increasing's parameters are a state function f, a domain A and an order 6relation r over the domain A. 7*) 8 9section\<open>Charpentier's "Increasing" Relation\<close> 10 11theory Increasing imports Constrains Monotonicity begin 12 13definition 14 increasing :: "[i, i, i=>i] => i" ("increasing[_]'(_, _')") where 15 "increasing[A](r, f) == 16 {F \<in> program. (\<forall>k \<in> A. F \<in> stable({s \<in> state. <k, f(s)> \<in> r})) & 17 (\<forall>x \<in> state. f(x):A)}" 18 19definition 20 Increasing :: "[i, i, i=>i] => i" ("Increasing[_]'(_, _')") where 21 "Increasing[A](r, f) == 22 {F \<in> program. (\<forall>k \<in> A. F \<in> Stable({s \<in> state. <k, f(s)> \<in> r})) & 23 (\<forall>x \<in> state. f(x):A)}" 24 25abbreviation (input) 26 IncWrt :: "[i=>i, i, i] => i" ("(_ IncreasingWrt _ '/ _)" [60, 0, 60] 60) where 27 "f IncreasingWrt r/A == Increasing[A](r,f)" 28 29 30(** increasing **) 31 32lemma increasing_type: "increasing[A](r, f) \<subseteq> program" 33by (unfold increasing_def, blast) 34 35lemma increasing_into_program: "F \<in> increasing[A](r, f) ==> F \<in> program" 36by (unfold increasing_def, blast) 37 38lemma increasing_imp_stable: 39"[| F \<in> increasing[A](r, f); x \<in> A |] ==>F \<in> stable({s \<in> state. <x, f(s)>:r})" 40by (unfold increasing_def, blast) 41 42lemma increasingD: 43"F \<in> increasing[A](r,f) ==> F \<in> program & (\<exists>a. a \<in> A) & (\<forall>s \<in> state. f(s):A)" 44apply (unfold increasing_def) 45apply (subgoal_tac "\<exists>x. x \<in> state") 46apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state) 47done 48 49lemma increasing_constant [simp]: 50 "F \<in> increasing[A](r, %s. c) \<longleftrightarrow> F \<in> program & c \<in> A" 51apply (unfold increasing_def stable_def) 52apply (subgoal_tac "\<exists>x. x \<in> state") 53apply (auto dest: stable_type [THEN subsetD] intro: st0_in_state) 54done 55 56lemma subset_increasing_comp: 57"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> 58 increasing[A](r, f) \<subseteq> increasing[B](s, g comp f)" 59apply (unfold increasing_def stable_def part_order_def 60 constrains_def mono1_def metacomp_def, clarify, simp) 61apply clarify 62apply (subgoal_tac "xa \<in> state") 63prefer 2 apply (blast dest!: ActsD) 64apply (subgoal_tac "<f (xb), f (xb) >:r") 65prefer 2 apply (force simp add: refl_def) 66apply (rotate_tac 5) 67apply (drule_tac x = "f (xb) " in bspec) 68apply (rotate_tac [2] -1) 69apply (drule_tac [2] x = act in bspec, simp_all) 70apply (drule_tac A = "act``u" and c = xa for u in subsetD, blast) 71apply (drule_tac x = "f(xa) " and x1 = "f(xb)" in bspec [THEN bspec]) 72apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD) 73apply simp_all 74done 75 76lemma imp_increasing_comp: 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)" 79by (rule subset_increasing_comp [THEN subsetD], auto) 80 81lemma strict_increasing: 82 "increasing[nat](Le, f) \<subseteq> increasing[nat](Lt, f)" 83by (unfold increasing_def Lt_def, auto) 84 85lemma strict_gt_increasing: 86 "increasing[nat](Ge, f) \<subseteq> increasing[nat](Gt, f)" 87apply (unfold increasing_def Gt_def Ge_def, auto) 88apply (erule natE) 89apply (auto simp add: stable_def) 90done 91 92(** Increasing **) 93 94lemma increasing_imp_Increasing: 95 "F \<in> increasing[A](r, f) ==> F \<in> Increasing[A](r, f)" 96 97apply (unfold increasing_def Increasing_def) 98apply (auto intro: stable_imp_Stable) 99done 100 101lemma Increasing_type: "Increasing[A](r, f) \<subseteq> program" 102by (unfold Increasing_def, auto) 103 104lemma Increasing_into_program: "F \<in> Increasing[A](r, f) ==> F \<in> program" 105by (unfold Increasing_def, auto) 106 107lemma Increasing_imp_Stable: 108"[| F \<in> Increasing[A](r, f); a \<in> A |] ==> F \<in> Stable({s \<in> state. <a,f(s)>:r})" 109by (unfold Increasing_def, blast) 110 111lemma IncreasingD: 112"F \<in> Increasing[A](r, f) ==> F \<in> program & (\<exists>a. a \<in> A) & (\<forall>s \<in> state. f(s):A)" 113apply (unfold Increasing_def) 114apply (subgoal_tac "\<exists>x. x \<in> state") 115apply (auto intro: st0_in_state) 116done 117 118lemma Increasing_constant [simp]: 119 "F \<in> Increasing[A](r, %s. c) \<longleftrightarrow> F \<in> program & (c \<in> A)" 120apply (subgoal_tac "\<exists>x. x \<in> state") 121apply (auto dest!: IncreasingD intro: st0_in_state increasing_imp_Increasing) 122done 123 124lemma subset_Increasing_comp: 125"[| mono1(A, r, B, s, g); refl(A, r); trans[B](s) |] ==> 126 Increasing[A](r, f) \<subseteq> Increasing[B](s, g comp f)" 127apply (unfold Increasing_def Stable_def Constrains_def part_order_def 128 constrains_def mono1_def metacomp_def, safe) 129apply (simp_all add: ActsD) 130apply (subgoal_tac "xb \<in> state & xa \<in> state") 131 prefer 2 apply (simp add: ActsD) 132apply (subgoal_tac "<f (xb), f (xb) >:r") 133prefer 2 apply (force simp add: refl_def) 134apply (rotate_tac 5) 135apply (drule_tac x = "f (xb) " in bspec) 136apply simp_all 137apply clarify 138apply (rotate_tac -2) 139apply (drule_tac x = act in bspec) 140apply (drule_tac [2] A = "act``u" and c = xa for u in subsetD, simp_all, blast) 141apply (drule_tac x = "f(xa)" and x1 = "f(xb)" in bspec [THEN bspec]) 142apply (rule_tac [3] b = "g (f (xb))" and A = B in trans_onD) 143apply simp_all 144done 145 146lemma imp_Increasing_comp: 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)" 149apply (rule subset_Increasing_comp [THEN subsetD], auto) 150done 151 152lemma strict_Increasing: "Increasing[nat](Le, f) \<subseteq> Increasing[nat](Lt, f)" 153by (unfold Increasing_def Lt_def, auto) 154 155lemma strict_gt_Increasing: "Increasing[nat](Ge, f)<= Increasing[nat](Gt, f)" 156apply (unfold Increasing_def Ge_def Gt_def, auto) 157apply (erule natE) 158apply (auto simp add: Stable_def) 159done 160 161(** Two-place monotone operations **) 162 163lemma imp_increasing_comp2: 164"[| F \<in> increasing[A](r, f); F \<in> increasing[B](s, g); 165 mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |] 166 ==> F \<in> increasing[C](t, %x. h(f(x), g(x)))" 167apply (unfold increasing_def stable_def 168 part_order_def constrains_def mono2_def, clarify, simp) 169apply clarify 170apply (rename_tac xa xb) 171apply (subgoal_tac "xb \<in> state & xa \<in> state") 172 prefer 2 apply (blast dest!: ActsD) 173apply (subgoal_tac "<f (xb), f (xb) >:r & <g (xb), g (xb) >:s") 174prefer 2 apply (force simp add: refl_def) 175apply (rotate_tac 6) 176apply (drule_tac x = "f (xb) " in bspec) 177apply (rotate_tac [2] 1) 178apply (drule_tac [2] x = "g (xb) " in bspec) 179apply simp_all 180apply (rotate_tac -1) 181apply (drule_tac x = act in bspec) 182apply (rotate_tac [2] -3) 183apply (drule_tac [2] x = act in bspec, simp_all) 184apply (drule_tac A = "act``u" and c = xa for u in subsetD) 185apply (drule_tac [2] A = "act``u" and c = xa for u in subsetD, blast, blast) 186apply (rotate_tac -4) 187apply (drule_tac x = "f (xa) " and x1 = "f (xb) " in bspec [THEN bspec]) 188apply (rotate_tac [3] -1) 189apply (drule_tac [3] x = "g (xa) " and x1 = "g (xb) " in bspec [THEN bspec]) 190apply simp_all 191apply (rule_tac b = "h (f (xb), g (xb))" and A = C in trans_onD) 192apply simp_all 193done 194 195lemma imp_Increasing_comp2: 196"[| F \<in> Increasing[A](r, f); F \<in> Increasing[B](s, g); 197 mono2(A, r, B, s, C, t, h); refl(A, r); refl(B, s); trans[C](t) |] ==> 198 F \<in> Increasing[C](t, %x. h(f(x), g(x)))" 199apply (unfold Increasing_def stable_def 200 part_order_def constrains_def mono2_def Stable_def Constrains_def, safe) 201apply (simp_all add: ActsD) 202apply (subgoal_tac "xa \<in> state & x \<in> state") 203prefer 2 apply (blast dest!: ActsD) 204apply (subgoal_tac "<f (xa), f (xa) >:r & <g (xa), g (xa) >:s") 205prefer 2 apply (force simp add: refl_def) 206apply (rotate_tac 6) 207apply (drule_tac x = "f (xa) " in bspec) 208apply (rotate_tac [2] 1) 209apply (drule_tac [2] x = "g (xa) " in bspec) 210apply simp_all 211apply clarify 212apply (rotate_tac -2) 213apply (drule_tac x = act in bspec) 214apply (rotate_tac [2] -3) 215apply (drule_tac [2] x = act in bspec, simp_all) 216apply (drule_tac A = "act``u" and c = x for u in subsetD) 217apply (drule_tac [2] A = "act``u" and c = x for u in subsetD, blast, blast) 218apply (rotate_tac -9) 219apply (drule_tac x = "f (x) " and x1 = "f (xa) " in bspec [THEN bspec]) 220apply (rotate_tac [3] -1) 221apply (drule_tac [3] x = "g (x) " and x1 = "g (xa) " in bspec [THEN bspec]) 222apply simp_all 223apply (rule_tac b = "h (f (xa), g (xa))" and A = C in trans_onD) 224apply simp_all 225done 226 227end 228