equal
deleted
inserted
replaced
1 (* Title: HOL/UNITY/Progress |
1 (* Title: HOL/UNITY/Progress |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 2003 University of Cambridge |
3 Copyright 2003 University of Cambridge |
5 |
4 |
6 David Meier's thesis |
5 David Meier's thesis |
7 *) |
6 *) |
11 theory Progress imports "../UNITY_Main" begin |
10 theory Progress imports "../UNITY_Main" begin |
12 |
11 |
13 subsection {*The Composition of Two Single-Assignment Programs*} |
12 subsection {*The Composition of Two Single-Assignment Programs*} |
14 text{*Thesis Section 4.4.2*} |
13 text{*Thesis Section 4.4.2*} |
15 |
14 |
16 constdefs |
15 definition FF :: "int program" where |
17 FF :: "int program" |
|
18 "FF == mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)" |
16 "FF == mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)" |
19 |
17 |
20 GG :: "int program" |
18 definition GG :: "int program" where |
21 "GG == mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)" |
19 "GG == mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)" |
22 |
20 |
23 subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*} |
21 subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*} |
24 |
22 |
25 lemma Domain_actFF: "Domain (range (\<lambda>x::int. (x, x + 1))) = UNIV" |
23 lemma Domain_actFF: "Domain (range (\<lambda>x::int. (x, x + 1))) = UNIV" |