src/HOL/UNITY/Comp/Handshake.thy
changeset 60773 d09c66a0ea10
parent 37936 1e4c5015a72e
child 67613 ce654b0e6d69
     1.1 --- a/src/HOL/UNITY/Comp/Handshake.thy	Thu Jul 23 16:40:47 2015 +0200
     1.2 +++ b/src/HOL/UNITY/Comp/Handshake.thy	Thu Jul 23 22:13:42 2015 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4          invFG_def [THEN def_set_simp, simp]
     1.5  
     1.6  
     1.7 -lemma invFG: "(F Join G) : Always invFG"
     1.8 +lemma invFG: "(F \<squnion> G) : Always invFG"
     1.9  apply (rule AlwaysI)
    1.10  apply force
    1.11  apply (rule constrains_imp_Constrains [THEN StableI])
    1.12 @@ -56,25 +56,25 @@
    1.13  apply (unfold G_def, safety) 
    1.14  done
    1.15  
    1.16 -lemma lemma2_1: "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo  
    1.17 +lemma lemma2_1: "(F \<squnion> G) : ({s. NF s = k} - {s. BB s}) LeadsTo  
    1.18                                ({s. NF s = k} Int {s. BB s})"
    1.19  apply (rule stable_Join_ensures1[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
    1.20   apply (unfold F_def, safety) 
    1.21  apply (unfold G_def, ensures_tac "cmdG") 
    1.22  done
    1.23  
    1.24 -lemma lemma2_2: "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo 
    1.25 +lemma lemma2_2: "(F \<squnion> G) : ({s. NF s = k} Int {s. BB s}) LeadsTo 
    1.26                                {s. k < NF s}"
    1.27  apply (rule stable_Join_ensures2[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
    1.28   apply (unfold F_def, ensures_tac "cmdF") 
    1.29  apply (unfold G_def, safety) 
    1.30  done
    1.31  
    1.32 -lemma progress: "(F Join G) : UNIV LeadsTo {s. m < NF s}"
    1.33 +lemma progress: "(F \<squnion> G) : UNIV LeadsTo {s. m < NF s}"
    1.34  apply (rule LeadsTo_weaken_R)
    1.35  apply (rule_tac f = "NF" and l = "Suc m" and B = "{}" 
    1.36         in GreaterThan_bounded_induct)
    1.37 -(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
    1.38 +(*The inductive step is (F \<squnion> G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
    1.39  apply (auto intro!: lemma2_1 lemma2_2
    1.40              intro: LeadsTo_Trans LeadsTo_Diff simp add: vimage_def)
    1.41  done