src/HOL/UNITY/Union.ML
changeset 5867 1c4806b4bf43
parent 5804 8e0a4c4fd67b
child 5898 3e34e7aa7479
equal deleted inserted replaced
5866:de6a1856c74a 5867:1c4806b4bf43
     7 
     7 
     8 From Misra's Chapter 5: Asynchronous Compositions of Programs
     8 From Misra's Chapter 5: Asynchronous Compositions of Programs
     9 *)
     9 *)
    10 
    10 
    11 
    11 
       
    12 (** SKIP **)
       
    13 
    12 Goal "Init SKIP = UNIV";
    14 Goal "Init SKIP = UNIV";
    13 by (simp_tac (simpset() addsimps [SKIP_def]) 1);
    15 by (simp_tac (simpset() addsimps [SKIP_def]) 1);
    14 qed "Init_SKIP";
    16 qed "Init_SKIP";
    15 
    17 
    16 Goal "Acts SKIP = {Id}";
    18 Goal "Acts SKIP = {Id}";
    17 by (simp_tac (simpset() addsimps [SKIP_def]) 1);
    19 by (simp_tac (simpset() addsimps [SKIP_def]) 1);
    18 qed "Acts_SKIP";
    20 qed "Acts_SKIP";
    19 
    21 
    20 Addsimps [Init_SKIP, Acts_SKIP];
    22 Addsimps [Init_SKIP, Acts_SKIP];
    21 
    23 
       
    24 Goal "reachable SKIP = UNIV";
       
    25 by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
       
    26 qed "reachable_SKIP";
       
    27 
       
    28 Addsimps [reachable_SKIP];
       
    29 
       
    30 
       
    31 (** Join and JN **)
       
    32 
    22 Goal "Init (F Join G) = Init F Int Init G";
    33 Goal "Init (F Join G) = Init F Int Init G";
    23 by (simp_tac (simpset() addsimps [Join_def]) 1);
    34 by (simp_tac (simpset() addsimps [Join_def]) 1);
    24 qed "Init_Join";
    35 qed "Init_Join";
    25 
    36 
    26 Goal "Acts (F Join G) = Acts F Un Acts G";
    37 Goal "Acts (F Join G) = Acts F Un Acts G";
    35 by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
    46 by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
    36 qed "Acts_JN";
    47 qed "Acts_JN";
    37 
    48 
    38 Addsimps [Init_Join, Init_JN];
    49 Addsimps [Init_Join, Init_JN];
    39 
    50 
       
    51 Goalw [JOIN_def, SKIP_def] "(JN i:{}. F i) = SKIP";
       
    52 by Auto_tac;
       
    53 qed "JN_empty";
       
    54 
    40 Goal "(JN x:insert a A. B x) = (B a) Join (JN x:A. B x)";
    55 Goal "(JN x:insert a A. B x) = (B a) Join (JN x:A. B x)";
    41 by (rtac program_equalityI 1);
    56 by (rtac program_equalityI 1);
    42 by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def])));
    57 by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def])));
    43 qed "JN_insert";
    58 qed "JN_insert";
    44 Addsimps[JN_insert];
    59 Addsimps[JN_empty, JN_insert];
    45 
    60 
    46 
    61 
    47 (** Algebraic laws **)
    62 (** Algebraic laws **)
    48 
    63 
    49 Goal "F Join G = G Join F";
    64 Goal "F Join G = G Join F";
    70 by (rtac program_equalityI 1);
    85 by (rtac program_equalityI 1);
    71 by Auto_tac;
    86 by Auto_tac;
    72 qed "Join_absorb";
    87 qed "Join_absorb";
    73 
    88 
    74 Addsimps [Join_absorb];
    89 Addsimps [Join_absorb];
    75 
       
    76 Goal "(JN G:{}. G) = SKIP";
       
    77 by (simp_tac (simpset() addsimps [JOIN_def, SKIP_def]) 1);
       
    78 qed "JN_empty";
       
    79 Addsimps [JN_empty];
       
    80 
    90 
    81 
    91 
    82 
    92 
    83 
    93 
    84 (*** Safety: constrains, stable, FP ***)
    94 (*** Safety: constrains, stable, FP ***)