src/HOL/UNITY/Transformers.thy
changeset 13851 f6923453953a
parent 13832 e7649436869c
child 13853 89131afa9f01
     1.1 --- a/src/HOL/UNITY/Transformers.thy	Thu Mar 06 15:03:16 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Transformers.thy	Thu Mar 06 15:08:38 2003 +0100
     1.3 @@ -44,6 +44,10 @@
     1.4  lemma wp_Id [simp]: "wp Id B = B"
     1.5  by (simp add: wp_def) 
     1.6  
     1.7 +lemma wp_totalize_act:
     1.8 +     "wp (totalize_act act) B = (wp act B \<inter> Domain act) \<union> (B - Domain act)"
     1.9 +by (simp add: wp_def totalize_act_def, blast)
    1.10 +
    1.11  lemma awp_Int_eq: "awp F (A\<inter>B) = awp F A \<inter> awp F B"
    1.12  by (simp add: awp_def wp_def, blast) 
    1.13  
    1.14 @@ -164,8 +168,7 @@
    1.15  
    1.16  lemma leadsTo_imp_wens_set: "F \<in> A leadsTo B ==> \<exists>C \<in> wens_set F B. A \<subseteq> C"
    1.17  apply (erule leadsTo_induct_pre)
    1.18 -  apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens)
    1.19 - apply clarify 
    1.20 +  apply (blast dest!: ensures_imp_wens intro: wens_set.Basis wens_set.Wens, clarify) 
    1.21   apply (drule ensures_weaken_R, assumption)  
    1.22   apply (blast dest!: ensures_imp_wens intro: wens_set.Wens)
    1.23  apply (case_tac "S={}") 
    1.24 @@ -236,8 +239,7 @@
    1.25  apply (rule_tac B = "wens (F\<squnion>G) act (T\<inter>X)" in subset_trans) 
    1.26   prefer 2 apply (blast intro!: wens_mono)
    1.27  apply (subst wens_Int_eq, assumption+) 
    1.28 -apply (rule subset_wens_Join [of _ T])
    1.29 -  apply simp 
    1.30 +apply (rule subset_wens_Join [of _ T], simp) 
    1.31   apply blast
    1.32  apply (subgoal_tac "T \<inter> wens F act (T\<inter>X) \<union> T\<inter>X = T \<inter> wens F act X")
    1.33   prefer 2
    1.34 @@ -274,8 +276,7 @@
    1.35  apply (rule leadsTo [THEN leadsTo_imp_wens_set, THEN bexE]) 
    1.36  apply (rule wens_Union [THEN bexE]) 
    1.37     apply (rule awpF) 
    1.38 -  apply (erule awpG) 
    1.39 - apply assumption
    1.40 +  apply (erule awpG, assumption)
    1.41  apply (blast intro: wens_set_imp_leadsTo [THEN leadsTo_weaken_L])  
    1.42  done
    1.43  
    1.44 @@ -334,10 +335,13 @@
    1.45  lemma atMost_nat_nonempty: "atMost (k::nat) \<noteq> {}"
    1.46  by force
    1.47  
    1.48 +lemma wens_single_finite_0 [simp]: "wens_single_finite act B 0 = B"
    1.49 +by (simp add: wens_single_finite_def)
    1.50 +
    1.51  lemma wens_single_finite_Suc:
    1.52        "single_valued act
    1.53         ==> wens_single_finite act B (Suc k) =
    1.54 -           wens_single_finite act B k \<union> wp act (wens_single_finite act B k) "
    1.55 +           wens_single_finite act B k \<union> wp act (wens_single_finite act B k)"
    1.56  apply (simp add: wens_single_finite_def image_def 
    1.57                   wp_UN_eq [OF _ atMost_nat_nonempty]) 
    1.58  apply (force elim!: le_SucE)
    1.59 @@ -350,6 +354,12 @@
    1.60                  (wens_single_finite act B k)"
    1.61  by (simp add: wens_single_finite_Suc wens_single_eq) 
    1.62  
    1.63 +lemma def_wens_single_finite_Suc_eq_wens:
    1.64 +     "[|F = mk_program (init, {act}, allowed); single_valued act|]
    1.65 +       ==> wens_single_finite act B (Suc k) =
    1.66 +           wens F act (wens_single_finite act B k)"
    1.67 +by (simp add: wens_single_finite_Suc_eq_wens) 
    1.68 +
    1.69  lemma wens_single_finite_Un_eq:
    1.70        "single_valued act
    1.71         ==> wens_single_finite act B k \<union> wp act (wens_single_finite act B k)
    1.72 @@ -377,8 +387,9 @@
    1.73  lemma subset_wens_single_finite:
    1.74        "[|W \<subseteq> wens_single_finite act B ` (atMost k); single_valued act; W\<noteq>{}|]
    1.75         ==> \<exists>m. \<Union>W = wens_single_finite act B m"
    1.76 -apply (induct k) 
    1.77 - apply (simp, blast) 
    1.78 +apply (induct k)
    1.79 + apply (rule_tac x=0 in exI, simp) 
    1.80 + apply blast 
    1.81  apply (auto simp add: atMost_Suc) 
    1.82  apply (case_tac "wens_single_finite act B (Suc n) \<in> W") 
    1.83   prefer 2 apply blast 
    1.84 @@ -398,11 +409,10 @@
    1.85  apply (case_tac "wens_single act B \<in> W")
    1.86   apply (blast dest: wens_single_finite_subset_wens_single [THEN subsetD]) 
    1.87  apply (simp add: wens_single_eq_Union) 
    1.88 -apply (rule equalityI)
    1.89 - apply blast 
    1.90 +apply (rule equalityI, blast) 
    1.91  apply (simp add: UN_subset_iff, clarify)
    1.92  apply (subgoal_tac "\<exists>y\<in>W. \<exists>n. y = wens_single_finite act B n & i\<le>n")  
    1.93 - apply (blast intro: wens_single_finite_mono [THEN subsetD] ) 
    1.94 + apply (blast intro: wens_single_finite_mono [THEN subsetD]) 
    1.95  apply (drule_tac x=i in spec)
    1.96  apply (force simp add: atMost_def)
    1.97  done
    1.98 @@ -447,12 +457,12 @@
    1.99  
   1.100  text{*Theorem (4.29)*}
   1.101  theorem wens_set_single_eq:
   1.102 -      "single_valued act
   1.103 -       ==> wens_set (mk_program (init, {act}, allowed)) B =
   1.104 -           insert (wens_single act B) (range (wens_single_finite act B))"
   1.105 +     "[|F = mk_program (init, {act}, allowed); single_valued act|]
   1.106 +      ==> wens_set F B =
   1.107 +          insert (wens_single act B) (range (wens_single_finite act B))"
   1.108  apply (rule equalityI)
   1.109 -apply (erule wens_set_subset_single) 
   1.110 -apply (erule single_subset_wens_set) 
   1.111 + apply (simp add: wens_set_subset_single) 
   1.112 +apply (erule ssubst, erule single_subset_wens_set) 
   1.113  done
   1.114  
   1.115  end