src/HOL/UNITY/Comp/TimerArray.thy
changeset 67613 ce654b0e6d69
parent 61943 7fba644ed827
     1.1 --- a/src/HOL/UNITY/Comp/TimerArray.thy	Tue Feb 13 14:24:50 2018 +0100
     1.2 +++ b/src/HOL/UNITY/Comp/TimerArray.thy	Thu Feb 15 12:11:00 2018 +0100
     1.3 @@ -24,14 +24,14 @@
     1.4  declare count_def [simp] decr_def [simp]
     1.5  
     1.6  (*Demonstrates induction, but not used in the following proof*)
     1.7 -lemma Timer_leadsTo_zero: "Timer : UNIV leadsTo {s. count s = 0}"
     1.8 +lemma Timer_leadsTo_zero: "Timer \<in> UNIV leadsTo {s. count s = 0}"
     1.9  apply (rule_tac f = count in lessThan_induct, simp)
    1.10  apply (case_tac "m")
    1.11   apply (force intro!: subset_imp_leadsTo)
    1.12  apply (unfold Timer_def, ensures_tac "decr")
    1.13  done
    1.14  
    1.15 -lemma Timer_preserves_snd [iff]: "Timer : preserves snd"
    1.16 +lemma Timer_preserves_snd [iff]: "Timer \<in> preserves snd"
    1.17  apply (rule preservesI)
    1.18  apply (unfold Timer_def, safety)
    1.19  done
    1.20 @@ -41,8 +41,8 @@
    1.21  
    1.22  lemma TimerArray_leadsTo_zero:
    1.23       "finite I  
    1.24 -      ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}"
    1.25 -apply (erule_tac A'1 = "%i. lift_set i ({0} \<times> UNIV)" 
    1.26 +      \<Longrightarrow> (plam i: I. Timer) \<in> UNIV leadsTo {(s,uu). \<forall>i\<in>I. s i = 0}"
    1.27 +apply (erule_tac A'1 = "\<lambda>i. lift_set i ({0} \<times> UNIV)" 
    1.28         in finite_stable_completion [THEN leadsTo_weaken])
    1.29  apply auto
    1.30  (*Safety property, already reduced to the single Timer case*)