src/HOL/TLA/TLA.thy
changeset 44890 22f665a2e91c
parent 42814 5af15f1e2ef6
child 45605 a89b4bc311a5
     1.1 --- a/src/HOL/TLA/TLA.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/TLA/TLA.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -251,7 +251,7 @@
     1.4    assumes prem: "|- F --> G"
     1.5    shows "|- <>F --> <>G"
     1.6    apply (unfold dmd_def)
     1.7 -  apply (fastsimp intro!: prem [temp_use] elim!: STL4E [temp_use])
     1.8 +  apply (fastforce intro!: prem [temp_use] elim!: STL4E [temp_use])
     1.9    done
    1.10  
    1.11  lemma DmdImplE: "[| sigma |= <>F; |- F --> G |] ==> sigma |= <>G"
    1.12 @@ -262,7 +262,7 @@
    1.13    apply auto
    1.14    apply (subgoal_tac "sigma |= [] (G --> (F & G))")
    1.15       apply (erule normalT [temp_use])
    1.16 -     apply (fastsimp elim!: STL4E [temp_use])+
    1.17 +     apply (fastforce elim!: STL4E [temp_use])+
    1.18    done
    1.19  
    1.20  (* rewrite rule to split conjunctions under boxes *)
    1.21 @@ -322,7 +322,7 @@
    1.22  
    1.23  lemma DmdOr: "|- (<>(F | G)) = (<>F | <>G)"
    1.24    apply (auto simp add: dmd_def split_box_conj [try_rewrite])
    1.25 -  apply (erule contrapos_np, merge_box, fastsimp elim!: STL4E [temp_use])+
    1.26 +  apply (erule contrapos_np, merge_box, fastforce elim!: STL4E [temp_use])+
    1.27    done
    1.28  
    1.29  lemma exT: "|- (EX x. <>(F x)) = (<>(EX x. F x))"
    1.30 @@ -343,7 +343,7 @@
    1.31    apply auto
    1.32    apply (erule notE)
    1.33    apply merge_box
    1.34 -  apply (fastsimp elim!: STL4E [temp_use])
    1.35 +  apply (fastforce elim!: STL4E [temp_use])
    1.36    done
    1.37  
    1.38  lemma InfImpl:
    1.39 @@ -354,7 +354,7 @@
    1.40    apply (insert 1 2)
    1.41    apply (erule_tac F = G in dup_boxE)
    1.42    apply merge_box
    1.43 -  apply (fastsimp elim!: STL4E [temp_use] DmdImpl2 [temp_use] intro!: 3 [temp_use])
    1.44 +  apply (fastforce elim!: STL4E [temp_use] DmdImpl2 [temp_use] intro!: 3 [temp_use])
    1.45    done
    1.46  
    1.47  (* ------------------------ STL6 ------------------------------------------- *)
    1.48 @@ -365,7 +365,7 @@
    1.49    apply (erule dup_boxE)
    1.50    apply merge_box
    1.51    apply (erule contrapos_np)
    1.52 -  apply (fastsimp elim!: STL4E [temp_use])
    1.53 +  apply (fastforce elim!: STL4E [temp_use])
    1.54    done
    1.55  
    1.56  (* weaker than BoxDmd, but more polymorphic (and often just right) *)
    1.57 @@ -373,14 +373,14 @@
    1.58    apply (unfold dmd_def)
    1.59    apply clarsimp
    1.60    apply merge_box
    1.61 -  apply (fastsimp elim!: notE STL4E [temp_use])
    1.62 +  apply (fastforce elim!: notE STL4E [temp_use])
    1.63    done
    1.64  
    1.65  lemma BoxDmd2_simple: "|- []F & <>G --> <>(G & F)"
    1.66    apply (unfold dmd_def)
    1.67    apply clarsimp
    1.68    apply merge_box
    1.69 -  apply (fastsimp elim!: notE STL4E [temp_use])
    1.70 +  apply (fastforce elim!: notE STL4E [temp_use])
    1.71    done
    1.72  
    1.73  lemma DmdImpldup:
    1.74 @@ -406,7 +406,7 @@
    1.75    apply (drule BoxDmd [temp_use])
    1.76     apply assumption
    1.77    apply (erule thin_rl)
    1.78 -  apply (fastsimp elim!: DmdImplE [temp_use])
    1.79 +  apply (fastforce elim!: DmdImplE [temp_use])
    1.80    done
    1.81  
    1.82  
    1.83 @@ -467,7 +467,7 @@
    1.84  (* ------------------------ Miscellaneous ----------------------------------- *)
    1.85  
    1.86  lemma BoxOr: "!!sigma. [| sigma |= []F | []G |] ==> sigma |= [](F | G)"
    1.87 -  by (fastsimp elim!: STL4E [temp_use])
    1.88 +  by (fastforce elim!: STL4E [temp_use])
    1.89  
    1.90  (* "persistently implies infinitely often" *)
    1.91  lemma DBImplBD: "|- <>[]F --> []<>F"
    1.92 @@ -487,7 +487,7 @@
    1.93     apply assumption
    1.94    apply (subgoal_tac "sigma |= <>[]~F")
    1.95     apply (force simp: dmd_def)
    1.96 -  apply (fastsimp elim: DmdImplE [temp_use] STL4E [temp_use])
    1.97 +  apply (fastforce elim: DmdImplE [temp_use] STL4E [temp_use])
    1.98    done
    1.99  
   1.100  
   1.101 @@ -498,7 +498,7 @@
   1.102  
   1.103  (* ------------------------ TLA2 ------------------------------------------- *)
   1.104  lemma STL2_pr: "|- []P --> Init P & Init P`"
   1.105 -  by (fastsimp intro!: STL2_gen [temp_use] primeI [temp_use])
   1.106 +  by (fastforce intro!: STL2_gen [temp_use] primeI [temp_use])
   1.107  
   1.108  (* Auxiliary lemma allows priming of boxed actions *)
   1.109  lemma BoxPrime: "|- []P --> []($P & P$)"
   1.110 @@ -523,7 +523,7 @@
   1.111  
   1.112  lemma DmdPrime: "|- (<>P`) --> (<>P)"
   1.113    apply (unfold dmd_def)
   1.114 -  apply (fastsimp elim!: TLA2E [temp_use])
   1.115 +  apply (fastforce elim!: TLA2E [temp_use])
   1.116    done
   1.117  
   1.118  lemmas PrimeDmd = InitDmd_gen [temp_use, THEN DmdPrime [temp_use], standard]
   1.119 @@ -557,7 +557,7 @@
   1.120  lemma StableT: 
   1.121      "!!P. |- $P & A --> P` ==> |- []A --> stable P"
   1.122    apply (unfold stable_def)
   1.123 -  apply (fastsimp elim!: STL4E [temp_use])
   1.124 +  apply (fastforce elim!: STL4E [temp_use])
   1.125    done
   1.126  
   1.127  lemma Stable: "[| sigma |= []A; |- $P & A --> P` |] ==> sigma |= stable P"
   1.128 @@ -617,7 +617,7 @@
   1.129    apply (clarsimp dest!: BoxPrime [temp_use])
   1.130    apply merge_box
   1.131    apply (erule contrapos_np)
   1.132 -  apply (fastsimp elim!: Stable [temp_use])
   1.133 +  apply (fastforce elim!: Stable [temp_use])
   1.134    done
   1.135  
   1.136  
   1.137 @@ -627,7 +627,7 @@
   1.138  (* Recursive expansions of [] and <> for state predicates *)
   1.139  lemma BoxRec: "|- ([]P) = (Init P & []P`)"
   1.140    apply (auto intro!: STL2_gen [temp_use])
   1.141 -   apply (fastsimp elim!: TLA2E [temp_use])
   1.142 +   apply (fastforce elim!: TLA2E [temp_use])
   1.143    apply (auto simp: stable_def elim!: INV1 [temp_use] STL4E [temp_use])
   1.144    done
   1.145  
   1.146 @@ -645,12 +645,12 @@
   1.147     apply (rule classical)
   1.148     apply (rule DBImplBD [temp_use])
   1.149     apply (subgoal_tac "sigma |= <>[]P")
   1.150 -    apply (fastsimp elim!: DmdImplE [temp_use] TLA2E [temp_use])
   1.151 +    apply (fastforce elim!: DmdImplE [temp_use] TLA2E [temp_use])
   1.152     apply (subgoal_tac "sigma |= <>[] (<>P & []~P`)")
   1.153      apply (force simp: boxInit_stp [temp_use]
   1.154        elim!: DmdImplE [temp_use] STL4E [temp_use] DmdRec2 [temp_use])
   1.155     apply (force intro!: STL6 [temp_use] simp: more_temp_simps3)
   1.156 -  apply (fastsimp intro: DmdPrime [temp_use] elim!: STL4E [temp_use])
   1.157 +  apply (fastforce intro: DmdPrime [temp_use] elim!: STL4E [temp_use])
   1.158    done
   1.159  
   1.160  lemma InfiniteEnsures:
   1.161 @@ -666,12 +666,12 @@
   1.162  (* alternative definitions of fairness *)
   1.163  lemma WF_alt: "|- WF(A)_v = ([]<>~Enabled(<A>_v) | []<><A>_v)"
   1.164    apply (unfold WF_def dmd_def)
   1.165 -  apply fastsimp
   1.166 +  apply fastforce
   1.167    done
   1.168  
   1.169  lemma SF_alt: "|- SF(A)_v = (<>[]~Enabled(<A>_v) | []<><A>_v)"
   1.170    apply (unfold SF_def dmd_def)
   1.171 -  apply fastsimp
   1.172 +  apply fastforce
   1.173    done
   1.174  
   1.175  (* theorems to "box" fairness conditions *)
   1.176 @@ -679,19 +679,19 @@
   1.177    by (auto simp: WF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
   1.178  
   1.179  lemma WF_Box: "|- ([]WF(A)_v) = WF(A)_v"
   1.180 -  by (fastsimp intro!: BoxWFI [temp_use] dest!: STL2 [temp_use])
   1.181 +  by (fastforce intro!: BoxWFI [temp_use] dest!: STL2 [temp_use])
   1.182  
   1.183  lemma BoxSFI: "|- SF(A)_v --> []SF(A)_v"
   1.184    by (auto simp: SF_alt [try_rewrite] more_temp_simps3 intro!: BoxOr [temp_use])
   1.185  
   1.186  lemma SF_Box: "|- ([]SF(A)_v) = SF(A)_v"
   1.187 -  by (fastsimp intro!: BoxSFI [temp_use] dest!: STL2 [temp_use])
   1.188 +  by (fastforce intro!: BoxSFI [temp_use] dest!: STL2 [temp_use])
   1.189  
   1.190  lemmas more_temp_simps = more_temp_simps3 WF_Box [temp_rewrite] SF_Box [temp_rewrite]
   1.191  
   1.192  lemma SFImplWF: "|- SF(A)_v --> WF(A)_v"
   1.193    apply (unfold SF_def WF_def)
   1.194 -  apply (fastsimp dest!: DBImplBD [temp_use])
   1.195 +  apply (fastforce dest!: DBImplBD [temp_use])
   1.196    done
   1.197  
   1.198  (* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *)
   1.199 @@ -716,13 +716,13 @@
   1.200    apply (unfold leadsto_def)
   1.201    apply auto
   1.202      apply (simp add: more_temp_simps)
   1.203 -    apply (fastsimp elim!: DmdImplE [temp_use] STL4E [temp_use])
   1.204 -   apply (fastsimp intro!: InitDmd [temp_use] elim!: STL4E [temp_use])
   1.205 +    apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use])
   1.206 +   apply (fastforce intro!: InitDmd [temp_use] elim!: STL4E [temp_use])
   1.207    apply (subgoal_tac "sigma |= []<><>G")
   1.208     apply (simp add: more_temp_simps)
   1.209    apply (drule BoxDmdDmdBox [temp_use])
   1.210     apply assumption
   1.211 -  apply (fastsimp elim!: DmdImplE [temp_use] STL4E [temp_use])
   1.212 +  apply (fastforce elim!: DmdImplE [temp_use] STL4E [temp_use])
   1.213    done
   1.214  
   1.215  lemma leadsto_infinite: "|- []<>F & (F ~> G) --> []<>G"
   1.216 @@ -880,7 +880,7 @@
   1.217    apply clarsimp
   1.218    apply (subgoal_tac "sigma |= (B | C) ~> D")
   1.219    apply (erule_tac G = "LIFT (B | C)" in LatticeTransitivity [temp_use])
   1.220 -   apply (fastsimp intro!: LatticeDisjunctionIntro [temp_use])+
   1.221 +   apply (fastforce intro!: LatticeDisjunctionIntro [temp_use])+
   1.222    done
   1.223  
   1.224  lemma LatticeTriangle: "|- (A ~> D | B) & (B ~> D) --> (A ~> D)"