src/HOL/UNITY/Union.thy
changeset 36866 426d5781bb25
parent 35434 a4babce15c67
child 44928 7ef6505bde7f
     1.1 --- a/src/HOL/UNITY/Union.thy	Wed May 12 15:25:58 2010 +0200
     1.2 +++ b/src/HOL/UNITY/Union.thy	Wed May 12 16:44:49 2010 +0200
     1.3 @@ -9,31 +9,35 @@
     1.4  
     1.5  theory Union imports SubstAx FP begin
     1.6  
     1.7 -constdefs
     1.8 -
     1.9    (*FIXME: conjoin Init F \<inter> Init G \<noteq> {} *) 
    1.10 +definition
    1.11    ok :: "['a program, 'a program] => bool"      (infixl "ok" 65)
    1.12 -    "F ok G == Acts F \<subseteq> AllowedActs G &
    1.13 +  where "F ok G == Acts F \<subseteq> AllowedActs G &
    1.14                 Acts G \<subseteq> AllowedActs F"
    1.15  
    1.16    (*FIXME: conjoin (\<Inter>i \<in> I. Init (F i)) \<noteq> {} *) 
    1.17 +definition
    1.18    OK  :: "['a set, 'a => 'b program] => bool"
    1.19 -    "OK I F == (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts (F i) \<subseteq> AllowedActs (F j))"
    1.20 +  where "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts (F i) \<subseteq> AllowedActs (F j))"
    1.21  
    1.22 +definition
    1.23    JOIN  :: "['a set, 'a => 'b program] => 'b program"
    1.24 -    "JOIN I F == mk_program (\<Inter>i \<in> I. Init (F i), \<Union>i \<in> I. Acts (F i),
    1.25 +  where "JOIN I F = mk_program (\<Inter>i \<in> I. Init (F i), \<Union>i \<in> I. Acts (F i),
    1.26                               \<Inter>i \<in> I. AllowedActs (F i))"
    1.27  
    1.28 +definition
    1.29    Join :: "['a program, 'a program] => 'a program"      (infixl "Join" 65)
    1.30 -    "F Join G == mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
    1.31 +  where "F Join G = mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
    1.32                               AllowedActs F \<inter> AllowedActs G)"
    1.33  
    1.34 +definition
    1.35    SKIP :: "'a program"
    1.36 -    "SKIP == mk_program (UNIV, {}, UNIV)"
    1.37 +  where "SKIP = mk_program (UNIV, {}, UNIV)"
    1.38  
    1.39    (*Characterizes safety properties.  Used with specifying Allowed*)
    1.40 +definition
    1.41    safety_prop :: "'a program set => bool"
    1.42 -    "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
    1.43 +  where "safety_prop X <-> SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
    1.44  
    1.45  notation (xsymbols)
    1.46    SKIP  ("\<bottom>") and
    1.47 @@ -420,12 +424,12 @@
    1.48  by (simp add: Allowed_def) 
    1.49  
    1.50  lemma def_total_prg_Allowed:
    1.51 -     "[| F == mk_total_program (init, acts, UNION X Acts) ; safety_prop X |]  
    1.52 +     "[| F = mk_total_program (init, acts, UNION X Acts) ; safety_prop X |]  
    1.53        ==> Allowed F = X"
    1.54  by (simp add: mk_total_program_def def_prg_Allowed) 
    1.55  
    1.56  lemma def_UNION_ok_iff:
    1.57 -     "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |]  
    1.58 +     "[| F = mk_program(init,acts,UNION X Acts); safety_prop X |]  
    1.59        ==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)"
    1.60  by (auto simp add: ok_def safety_prop_Acts_iff)
    1.61