src/HOL/UNITY/Channel.ML
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
permissions -rw-r--r--
New UNITY theory
paulson@4776
     1
(*  Title:      HOL/UNITY/Channel
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
Unordered Channel
paulson@4776
     7
paulson@4776
     8
From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
paulson@4776
     9
*)
paulson@4776
    10
paulson@4776
    11
open Channel;
paulson@4776
    12
paulson@4776
    13
AddIffs [skip];
paulson@4776
    14
paulson@4776
    15
paulson@4776
    16
(*None represents "infinity" while Some represents proper integers*)
paulson@4776
    17
goalw thy [minSet_def] "!!A. minSet A = Some x --> x : A";
paulson@4776
    18
by (Simp_tac 1);
paulson@4776
    19
by (fast_tac (claset() addIs [LeastI]) 1);
paulson@4776
    20
qed_spec_mp "minSet_eq_SomeD";
paulson@4776
    21
paulson@4776
    22
goalw thy [minSet_def] " minSet{} = None";
paulson@4776
    23
by (Asm_simp_tac 1);
paulson@4776
    24
qed_spec_mp "minSet_empty";
paulson@4776
    25
Addsimps [minSet_empty];
paulson@4776
    26
paulson@4776
    27
goalw thy [minSet_def] "!!A. x:A ==> minSet A = Some (LEAST x. x: A)";
paulson@4776
    28
by (ALLGOALS Asm_simp_tac);
paulson@4776
    29
by (Blast_tac 1);
paulson@4776
    30
qed_spec_mp "minSet_nonempty";
paulson@4776
    31
paulson@4776
    32
goal thy
paulson@4776
    33
    "leadsTo Acts (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
paulson@4776
    34
by (rtac leadsTo_weaken 1);
paulson@4776
    35
by (rtac ([UC2, UC1] MRS PSP) 1);
paulson@4776
    36
by (ALLGOALS Asm_simp_tac);
paulson@4776
    37
by (Blast_tac 1);
paulson@4776
    38
by Safe_tac;
paulson@4776
    39
by (auto_tac (claset() addDs [minSet_eq_SomeD], 
paulson@4776
    40
	      simpset() addsimps [le_def, nat_neq_iff]));
paulson@4776
    41
qed "minSet_greaterThan";
paulson@4776
    42
paulson@4776
    43
paulson@4776
    44
(*The induction*)
paulson@4776
    45
goal thy "leadsTo Acts (UNIV-{{}}) (minSet -`` (Some``atLeast y))";
paulson@4776
    46
by (rtac leadsTo_weaken_R 1);
paulson@4776
    47
by (res_inst_tac  [("l", "y"), ("f", "the o minSet"), ("B", "{}")]
paulson@4776
    48
     greaterThan_bounded_induct 1);
paulson@4776
    49
by Safe_tac;
paulson@4776
    50
by (ALLGOALS Asm_simp_tac);
paulson@4776
    51
by (dtac minSet_nonempty 2);
paulson@4776
    52
by (Asm_full_simp_tac 2);
paulson@4776
    53
by (rtac (minSet_greaterThan RS leadsTo_weaken) 1);
paulson@4776
    54
by Safe_tac;
paulson@4776
    55
by (ALLGOALS Asm_full_simp_tac);
paulson@4776
    56
by (dtac minSet_nonempty 1);
paulson@4776
    57
by (Asm_full_simp_tac 1);
paulson@4776
    58
val lemma = result();
paulson@4776
    59
paulson@4776
    60
paulson@4776
    61
goal thy "!!y::nat. leadsTo Acts (UNIV-{{}}) {s. y ~: s}";
paulson@4776
    62
by (rtac (lemma RS leadsTo_weaken_R) 1);
paulson@4776
    63
by (Clarify_tac 1);
paulson@4776
    64
by (forward_tac [minSet_nonempty] 1);
paulson@4776
    65
by (asm_full_simp_tac (simpset() addsimps [Suc_le_eq]) 1);
paulson@4776
    66
by (blast_tac (claset() addDs [Suc_le_lessD, not_less_Least]) 1);
paulson@4776
    67
qed "Channel_progress";