author | wenzelm |
Thu, 22 Jul 2010 18:08:39 +0200 | |
changeset 37936 | 1e4c5015a72e |
parent 35416 | d8d7d1b785af |
child 42463 | f270e3e18be5 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/UNITY/Simple/Channel.thy |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Copyright 1998 University of Cambridge |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
Unordered Channel |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
From Misra, "A Logic for Concurrent Programming" (1994), section 13.3 |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
8 |
*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
9 |
|
18556 | 10 |
theory Channel imports "../UNITY_Main" begin |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
12 |
types state = "nat set" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
13 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
14 |
consts |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
15 |
F :: "state program" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
16 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
18556
diff
changeset
|
17 |
definition minSet :: "nat set => nat option" where |
13806 | 18 |
"minSet A == if A={} then None else Some (LEAST x. x \<in> A)" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
|
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
20 |
axioms |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
21 |
|
13806 | 22 |
UC1: "F \<in> (minSet -` {Some x}) co (minSet -` (Some`atLeast x))" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
23 |
|
13806 | 24 |
(* UC1 "F \<in> {s. minSet s = x} co {s. x \<subseteq> minSet s}" *) |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
25 |
|
13806 | 26 |
UC2: "F \<in> (minSet -` {Some x}) leadsTo {s. x \<notin> s}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
27 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
28 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
29 |
(*None represents "infinity" while Some represents proper integers*) |
13806 | 30 |
lemma minSet_eq_SomeD: "minSet A = Some x ==> x \<in> A" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
31 |
apply (unfold minSet_def) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
32 |
apply (simp split: split_if_asm) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
33 |
apply (fast intro: LeastI) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
34 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
35 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
36 |
lemma minSet_empty [simp]: " minSet{} = None" |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
37 |
by (unfold minSet_def, simp) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
38 |
|
13806 | 39 |
lemma minSet_nonempty: "x \<in> A ==> minSet A = Some (LEAST x. x \<in> A)" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
40 |
by (unfold minSet_def, auto) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
41 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
42 |
lemma minSet_greaterThan: |
13806 | 43 |
"F \<in> (minSet -` {Some x}) leadsTo (minSet -` (Some`greaterThan x))" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
44 |
apply (rule leadsTo_weaken) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
45 |
apply (rule_tac x1=x in psp [OF UC2 UC1], safe) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
46 |
apply (auto dest: minSet_eq_SomeD simp add: linorder_neq_iff) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
47 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
48 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
49 |
(*The induction*) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
50 |
lemma Channel_progress_lemma: |
13806 | 51 |
"F \<in> (UNIV-{{}}) leadsTo (minSet -` (Some`atLeast y))" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
52 |
apply (rule leadsTo_weaken_R) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
53 |
apply (rule_tac l = y and f = "the o minSet" and B = "{}" |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
54 |
in greaterThan_bounded_induct, safe) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
55 |
apply (simp_all (no_asm_simp)) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
56 |
apply (drule_tac [2] minSet_nonempty) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
57 |
prefer 2 apply simp |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
58 |
apply (rule minSet_greaterThan [THEN leadsTo_weaken], safe) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
59 |
apply simp_all |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
60 |
apply (drule minSet_nonempty, simp) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
61 |
done |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
62 |
|
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
63 |
|
13806 | 64 |
lemma Channel_progress: "!!y::nat. F \<in> (UNIV-{{}}) leadsTo {s. y \<notin> s}" |
13785
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
65 |
apply (rule Channel_progress_lemma [THEN leadsTo_weaken_R], clarify) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
66 |
apply (frule minSet_nonempty) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
67 |
apply (auto dest: Suc_le_lessD not_less_Least) |
e2fcd88be55d
Partial conversion of UNITY to Isar new-style theories
paulson
parents:
12919
diff
changeset
|
68 |
done |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
69 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
70 |
end |