src/HOL/UNITY/Channel.ML
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/Channel.ML	Fri Apr 03 12:34:33 1998 +0200
     1.3 @@ -0,0 +1,67 @@
     1.4 +(*  Title:      HOL/UNITY/Channel
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +Unordered Channel
    1.10 +
    1.11 +From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
    1.12 +*)
    1.13 +
    1.14 +open Channel;
    1.15 +
    1.16 +AddIffs [skip];
    1.17 +
    1.18 +
    1.19 +(*None represents "infinity" while Some represents proper integers*)
    1.20 +goalw thy [minSet_def] "!!A. minSet A = Some x --> x : A";
    1.21 +by (Simp_tac 1);
    1.22 +by (fast_tac (claset() addIs [LeastI]) 1);
    1.23 +qed_spec_mp "minSet_eq_SomeD";
    1.24 +
    1.25 +goalw thy [minSet_def] " minSet{} = None";
    1.26 +by (Asm_simp_tac 1);
    1.27 +qed_spec_mp "minSet_empty";
    1.28 +Addsimps [minSet_empty];
    1.29 +
    1.30 +goalw thy [minSet_def] "!!A. x:A ==> minSet A = Some (LEAST x. x: A)";
    1.31 +by (ALLGOALS Asm_simp_tac);
    1.32 +by (Blast_tac 1);
    1.33 +qed_spec_mp "minSet_nonempty";
    1.34 +
    1.35 +goal thy
    1.36 +    "leadsTo Acts (minSet -`` {Some x}) (minSet -`` (Some``greaterThan x))";
    1.37 +by (rtac leadsTo_weaken 1);
    1.38 +by (rtac ([UC2, UC1] MRS PSP) 1);
    1.39 +by (ALLGOALS Asm_simp_tac);
    1.40 +by (Blast_tac 1);
    1.41 +by Safe_tac;
    1.42 +by (auto_tac (claset() addDs [minSet_eq_SomeD], 
    1.43 +	      simpset() addsimps [le_def, nat_neq_iff]));
    1.44 +qed "minSet_greaterThan";
    1.45 +
    1.46 +
    1.47 +(*The induction*)
    1.48 +goal thy "leadsTo Acts (UNIV-{{}}) (minSet -`` (Some``atLeast y))";
    1.49 +by (rtac leadsTo_weaken_R 1);
    1.50 +by (res_inst_tac  [("l", "y"), ("f", "the o minSet"), ("B", "{}")]
    1.51 +     greaterThan_bounded_induct 1);
    1.52 +by Safe_tac;
    1.53 +by (ALLGOALS Asm_simp_tac);
    1.54 +by (dtac minSet_nonempty 2);
    1.55 +by (Asm_full_simp_tac 2);
    1.56 +by (rtac (minSet_greaterThan RS leadsTo_weaken) 1);
    1.57 +by Safe_tac;
    1.58 +by (ALLGOALS Asm_full_simp_tac);
    1.59 +by (dtac minSet_nonempty 1);
    1.60 +by (Asm_full_simp_tac 1);
    1.61 +val lemma = result();
    1.62 +
    1.63 +
    1.64 +goal thy "!!y::nat. leadsTo Acts (UNIV-{{}}) {s. y ~: s}";
    1.65 +by (rtac (lemma RS leadsTo_weaken_R) 1);
    1.66 +by (Clarify_tac 1);
    1.67 +by (forward_tac [minSet_nonempty] 1);
    1.68 +by (asm_full_simp_tac (simpset() addsimps [Suc_le_eq]) 1);
    1.69 +by (blast_tac (claset() addDs [Suc_le_lessD, not_less_Least]) 1);
    1.70 +qed "Channel_progress";