src/HOL/UNITY/Comp.ML
author paulson
Thu, 01 Oct 1998 18:28:47 +0200
changeset 5597 a12b25c53df1
child 5612 e981ca6f7332
permissions -rw-r--r--
composition theory
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5597
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Comp.thy
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     5
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     6
Composition
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     7
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     8
From Chandy and Sanders, "Reasoning About Program Composition"
a12b25c53df1 composition theory
paulson
parents:
diff changeset
     9
*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    10
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    11
Addsimps [Join_SKIP, Join_absorb];
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    12
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    13
(*split_all_tac causes a big blow-up*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    14
claset_ref() := claset() delSWrapper "split_all_tac";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    15
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    16
Delsimps [split_paired_All];
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    17
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    18
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    19
(*** component ***)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    20
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    21
Goalw [component_def] "component F F";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    22
by (blast_tac (claset() addIs [Join_SKIP]) 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    23
qed "component_refl";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    24
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    25
AddIffs [component_refl];
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    26
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    27
Goalw [component_def] "[| component F G; component G H |] ==> component F H";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    28
by (blast_tac (claset() addIs [Join_assoc RS sym]) 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    29
qed "component_trans";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    30
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    31
Goalw [component_def,Join_def] "component F G ==> Acts F <= Acts G";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    32
auto();
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    33
qed "componet_Acts";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    34
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    35
Goalw [component_def,Join_def] "component F G ==> Init G <= Init F";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    36
auto();
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    37
qed "componet_Init";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    38
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    39
Goal "[| component F G; component G F |] ==> F=G";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    40
by (asm_simp_tac (simpset() addsimps [program_equalityI, equalityI, 
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    41
				      componet_Acts, componet_Init]) 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    42
qed "component_anti_sym";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    43
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    44
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    45
(*** existential properties ***)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    46
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    47
Goalw [ex_prop_def]
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    48
     "[| ex_prop X; finite GG |] ==> GG Int X ~= {} --> (JN G:GG. G) : X";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    49
by (etac finite_induct 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    50
by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    51
qed_spec_mp "ex1";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    52
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    53
Goalw [ex_prop_def]
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    54
     "ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X  \
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    55
\      ==> ex_prop X";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    56
by (Clarify_tac 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    57
by (dres_inst_tac [("x", "{F,G}")] spec 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    58
auto();
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    59
qed "ex2";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    60
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    61
(*Chandy & Sanders take this as a definition*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    62
Goal "ex_prop X = (ALL GG. finite GG & GG Int X ~= {} --> (JN G:GG. G) : X)";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    63
by (blast_tac (claset() addIs [ex1,ex2]) 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    64
qed "ex_prop_finite";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    65
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    66
(*Their "equivalent definition" given at the end of section 3*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    67
Goal "ex_prop X = (ALL G. G:X = (ALL H. component G H --> H: X))";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    68
auto();
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    69
bws [ex_prop_def, component_def];
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    70
by (Blast_tac 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    71
by Safe_tac;
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    72
by (stac Join_commute 2);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    73
by (ALLGOALS Blast_tac);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    74
qed "ex_prop_equiv";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    75
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    76
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    77
(*** universal properties ***)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    78
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    79
Goalw [uv_prop_def]
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    80
     "[| uv_prop X; finite GG |] ==> GG <= X --> (JN G:GG. G) : X";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    81
by (etac finite_induct 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    82
by (auto_tac (claset(), simpset() addsimps [Int_insert_left]));
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    83
qed_spec_mp "uv1";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    84
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    85
Goalw [uv_prop_def]
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    86
     "ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X  ==> uv_prop X";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    87
br conjI 1;
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    88
by (Clarify_tac 2);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    89
by (dres_inst_tac [("x", "{F,G}")] spec 2);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    90
by (dres_inst_tac [("x", "{}")] spec 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    91
auto();
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    92
qed "uv2";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    93
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    94
(*Chandy & Sanders take this as a definition*)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    95
Goal "uv_prop X = (ALL GG. finite GG & GG <= X --> (JN G:GG. G) : X)";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    96
by (blast_tac (claset() addIs [uv1,uv2]) 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    97
qed "uv_prop_finite";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    98
a12b25c53df1 composition theory
paulson
parents:
diff changeset
    99
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   100
(*** guarantees ***)
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   101
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   102
Goalw [guarantees_def] "X <= Y ==> X guarantees Y = UNIV";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   103
by (Blast_tac 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   104
qed "subset_imp_guarantees";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   105
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   106
Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guarantees Y)";
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   107
ex_prop_equiv
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   108
by (Blast_tac 1);
a12b25c53df1 composition theory
paulson
parents:
diff changeset
   109
qed "subset_imp_guarantees";