src/HOL/TLA/Action.thy
changeset 60587 0318b43ee95c
parent 59582 0fbed69ff081
child 60588 750c533459b1
     1.1 --- a/src/HOL/TLA/Action.thy	Fri Jun 26 11:07:04 2015 +0200
     1.2 +++ b/src/HOL/TLA/Action.thy	Fri Jun 26 11:44:22 2015 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      HOL/TLA/Action.thy 
     1.5 +(*  Title:      HOL/TLA/Action.thy
     1.6      Author:     Stephan Merz
     1.7      Copyright:  1998 University of Munich
     1.8  *)
     1.9 @@ -66,9 +66,9 @@
    1.10  
    1.11  defs
    1.12    square_def:    "ACT [A]_v == ACT (A | unchanged v)"
    1.13 -  angle_def:     "ACT <A>_v == ACT (A & ~ unchanged v)"
    1.14 +  angle_def:     "ACT <A>_v == ACT (A & \<not> unchanged v)"
    1.15  
    1.16 -  enabled_def:   "s |= Enabled A  ==  EX u. (s,u) |= A"
    1.17 +  enabled_def:   "s |= Enabled A  ==  \<exists>u. (s,u) |= A"
    1.18  
    1.19  
    1.20  (* The following assertion specializes "intI" for any world type
    1.21 @@ -76,7 +76,7 @@
    1.22  *)
    1.23  
    1.24  lemma actionI [intro!]:
    1.25 -  assumes "!!s t. (s,t) |= A"
    1.26 +  assumes "\<And>s t. (s,t) |= A"
    1.27    shows "|- A"
    1.28    apply (rule assms intI prod.induct)+
    1.29    done
    1.30 @@ -87,11 +87,11 @@
    1.31  
    1.32  lemma pr_rews [int_rewrite]:
    1.33    "|- (#c)` = #c"
    1.34 -  "!!f. |- f<x>` = f<x` >"
    1.35 -  "!!f. |- f<x,y>` = f<x`,y` >"
    1.36 -  "!!f. |- f<x,y,z>` = f<x`,y`,z` >"
    1.37 -  "|- (! x. P x)` = (! x. (P x)`)"
    1.38 -  "|- (? x. P x)` = (? x. (P x)`)"
    1.39 +  "\<And>f. |- f<x>` = f<x` >"
    1.40 +  "\<And>f. |- f<x,y>` = f<x`,y` >"
    1.41 +  "\<And>f. |- f<x,y,z>` = f<x`,y`,z` >"
    1.42 +  "|- (\<forall>x. P x)` = (\<forall>x. (P x)`)"
    1.43 +  "|- (\<exists>x. P x)` = (\<exists>x. (P x)`)"
    1.44    by (rule actionI, unfold unl_after intensional_rews, rule refl)+
    1.45  
    1.46  
    1.47 @@ -137,7 +137,7 @@
    1.48  
    1.49  lemma busy_squareI: "(s,t) |= A ==> (s,t) |= [A]_v"
    1.50    by (simp add: square_def)
    1.51 -  
    1.52 +
    1.53  lemma squareE [elim]:
    1.54    "[| (s,t) |= [A]_v; A (s,t) ==> B (s,t); v t = v s ==> B (s,t) |] ==> B (s,t)"
    1.55    apply (unfold square_def action_rews)
    1.56 @@ -145,34 +145,34 @@
    1.57    apply simp_all
    1.58    done
    1.59  
    1.60 -lemma squareCI [intro]: "[| v t ~= v s ==> A (s,t) |] ==> (s,t) |= [A]_v"
    1.61 +lemma squareCI [intro]: "[| v t \<noteq> v s ==> A (s,t) |] ==> (s,t) |= [A]_v"
    1.62    apply (unfold square_def action_rews)
    1.63    apply (rule disjCI)
    1.64    apply (erule (1) meta_mp)
    1.65    done
    1.66  
    1.67 -lemma angleI [intro]: "!!s t. [| A (s,t); v t ~= v s |] ==> (s,t) |= <A>_v"
    1.68 +lemma angleI [intro]: "\<And>s t. [| A (s,t); v t \<noteq> v s |] ==> (s,t) |= <A>_v"
    1.69    by (simp add: angle_def)
    1.70  
    1.71 -lemma angleE [elim]: "[| (s,t) |= <A>_v; [| A (s,t); v t ~= v s |] ==> R |] ==> R"
    1.72 +lemma angleE [elim]: "[| (s,t) |= <A>_v; [| A (s,t); v t \<noteq> v s |] ==> R |] ==> R"
    1.73    apply (unfold angle_def action_rews)
    1.74    apply (erule conjE)
    1.75    apply simp
    1.76    done
    1.77  
    1.78  lemma square_simulation:
    1.79 -   "!!f. [| |- unchanged f & ~B --> unchanged g;    
    1.80 -            |- A & ~unchanged g --> B               
    1.81 +   "\<And>f. [| |- unchanged f & \<not>B --> unchanged g;
    1.82 +            |- A & \<not>unchanged g --> B
    1.83           |] ==> |- [A]_f --> [B]_g"
    1.84    apply clarsimp
    1.85    apply (erule squareE)
    1.86    apply (auto simp add: square_def)
    1.87    done
    1.88  
    1.89 -lemma not_square: "|- (~ [A]_v) = <~A>_v"
    1.90 +lemma not_square: "|- (\<not> [A]_v) = <\<not>A>_v"
    1.91    by (auto simp: square_def angle_def)
    1.92  
    1.93 -lemma not_angle: "|- (~ <A>_v) = [~A]_v"
    1.94 +lemma not_angle: "|- (\<not> <A>_v) = [\<not>A]_v"
    1.95    by (auto simp: square_def angle_def)
    1.96  
    1.97  
    1.98 @@ -181,13 +181,13 @@
    1.99  lemma enabledI: "|- A --> $Enabled A"
   1.100    by (auto simp add: enabled_def)
   1.101  
   1.102 -lemma enabledE: "[| s |= Enabled A; !!u. A (s,u) ==> Q |] ==> Q"
   1.103 +lemma enabledE: "[| s |= Enabled A; \<And>u. A (s,u) ==> Q |] ==> Q"
   1.104    apply (unfold enabled_def)
   1.105    apply (erule exE)
   1.106    apply simp
   1.107    done
   1.108  
   1.109 -lemma notEnabledD: "|- ~$Enabled G --> ~ G"
   1.110 +lemma notEnabledD: "|- \<not>$Enabled G --> \<not> G"
   1.111    by (auto simp add: enabled_def)
   1.112  
   1.113  (* Monotonicity *)
   1.114 @@ -203,7 +203,7 @@
   1.115  (* stronger variant *)
   1.116  lemma enabled_mono2:
   1.117    assumes min: "s |= Enabled F"
   1.118 -    and maj: "!!t. F (s,t) ==> G (s,t)"
   1.119 +    and maj: "\<And>t. F (s,t) ==> G (s,t)"
   1.120    shows "s |= Enabled G"
   1.121    apply (rule min [THEN enabledE])
   1.122    apply (rule enabledI [action_use])
   1.123 @@ -239,13 +239,13 @@
   1.124    apply (erule disjE enabled_disj1 [action_use] enabled_disj2 [action_use])+
   1.125    done
   1.126  
   1.127 -lemma enabled_ex: "|- Enabled (EX x. F x) = (EX x. Enabled (F x))"
   1.128 +lemma enabled_ex: "|- Enabled (\<exists>x. F x) = (\<exists>x. Enabled (F x))"
   1.129    by (force simp add: enabled_def)
   1.130  
   1.131  
   1.132  (* A rule that combines enabledI and baseE, but generates fewer instantiations *)
   1.133  lemma base_enabled:
   1.134 -    "[| basevars vs; EX c. ! u. vs u = c --> A(s,u) |] ==> s |= Enabled A"
   1.135 +    "[| basevars vs; \<exists>c. \<forall>u. vs u = c --> A(s,u) |] ==> s |= Enabled A"
   1.136    apply (erule exE)
   1.137    apply (erule baseE)
   1.138    apply (rule enabledI [action_use])