--- a/src/HOLCF/Cfun.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/Cfun.thy Sun Oct 21 16:27:42 2007 +0200
@@ -435,18 +435,18 @@
subsection {* Identity and composition *}
-consts
- ID :: "'a \<rightarrow> 'a"
- cfcomp :: "('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c"
+definition
+ ID :: "'a \<rightarrow> 'a" where
+ "ID = (\<Lambda> x. x)"
+
+definition
+ cfcomp :: "('b \<rightarrow> 'c) \<rightarrow> ('a \<rightarrow> 'b) \<rightarrow> 'a \<rightarrow> 'c" where
+ oo_def: "cfcomp = (\<Lambda> f g x. f\<cdot>(g\<cdot>x))"
abbreviation
cfcomp_syn :: "['b \<rightarrow> 'c, 'a \<rightarrow> 'b] \<Rightarrow> 'a \<rightarrow> 'c" (infixr "oo" 100) where
"f oo g == cfcomp\<cdot>f\<cdot>g"
-defs
- ID_def: "ID \<equiv> (\<Lambda> x. x)"
- oo_def: "cfcomp \<equiv> (\<Lambda> f g x. f\<cdot>(g\<cdot>x))"
-
lemma ID1 [simp]: "ID\<cdot>x = x"
by (simp add: ID_def)
--- a/src/HOLCF/IOA/ABP/Abschannel.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Abschannel.thy Sun Oct 21 16:27:42 2007 +0200
@@ -12,90 +12,79 @@
datatype 'a abs_action = S 'a | R 'a
-consts
-
-ch_asig :: "'a abs_action signature"
-ch_trans :: "('a abs_action, 'a list)transition set"
-ch_ioa :: "('a abs_action, 'a list)ioa"
-
-rsch_actions :: "'m action => bool abs_action option"
-srch_actions :: "'m action =>(bool * 'm) abs_action option"
-
-srch_asig :: "'m action signature"
-rsch_asig :: "'m action signature"
-
-srch_trans :: "('m action, 'm packet list)transition set"
-rsch_trans :: "('m action, bool list)transition set"
-
-srch_ioa :: "('m action, 'm packet list)ioa"
-rsch_ioa :: "('m action, bool list)ioa"
-
-
-defs
-
-srch_asig_def: "srch_asig == asig_of(srch_ioa)"
-rsch_asig_def: "rsch_asig == asig_of(rsch_ioa)"
-
-srch_trans_def: "srch_trans == trans_of(srch_ioa)"
-rsch_trans_def: "rsch_trans == trans_of(rsch_ioa)"
-
-srch_ioa_def: "srch_ioa == rename ch_ioa srch_actions"
-rsch_ioa_def: "rsch_ioa == rename ch_ioa rsch_actions"
-
-
(**********************************************************
G e n e r i c C h a n n e l
*********************************************************)
-ch_asig_def: "ch_asig == (UN b. {S(b)}, UN b. {R(b)}, {})"
+definition
+ ch_asig :: "'a abs_action signature" where
+ "ch_asig = (UN b. {S(b)}, UN b. {R(b)}, {})"
-ch_trans_def: "ch_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in
- case fst(snd(tr))
- of S(b) => ((t = s) | (t = s @ [b])) |
- R(b) => s ~= [] &
- b = hd(s) &
- ((t = s) | (t = tl(s))) }"
+definition
+ ch_trans :: "('a abs_action, 'a list)transition set" where
+ "ch_trans =
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of S(b) => ((t = s) | (t = s @ [b])) |
+ R(b) => s ~= [] &
+ b = hd(s) &
+ ((t = s) | (t = tl(s)))}"
-ch_ioa_def: "ch_ioa == (ch_asig, {[]}, ch_trans,{},{})"
+definition
+ ch_ioa :: "('a abs_action, 'a list)ioa" where
+ "ch_ioa = (ch_asig, {[]}, ch_trans,{},{})"
+
(**********************************************************
C o n c r e t e C h a n n e l s b y R e n a m i n g
*********************************************************)
-rsch_actions_def: "rsch_actions (akt) ==
- case akt of
+definition
+ rsch_actions :: "'m action => bool abs_action option" where
+ "rsch_actions (akt) =
+ (case akt of
Next => None |
S_msg(m) => None |
R_msg(m) => None |
S_pkt(packet) => None |
R_pkt(packet) => None |
S_ack(b) => Some(S(b)) |
- R_ack(b) => Some(R(b))"
+ R_ack(b) => Some(R(b)))"
-srch_actions_def: "srch_actions (akt) ==
- case akt of
+definition
+ srch_actions :: "'m action =>(bool * 'm) abs_action option" where
+ "srch_actions akt =
+ (case akt of
Next => None |
S_msg(m) => None |
R_msg(m) => None |
S_pkt(p) => Some(S(p)) |
R_pkt(p) => Some(R(p)) |
S_ack(b) => None |
- R_ack(b) => None"
+ R_ack(b) => None)"
+
+definition
+ srch_ioa :: "('m action, 'm packet list)ioa" where
+ "srch_ioa = rename ch_ioa srch_actions"
+definition
+ rsch_ioa :: "('m action, bool list)ioa" where
+ "rsch_ioa = rename ch_ioa rsch_actions"
+
+definition
+ srch_asig :: "'m action signature" where
+ "srch_asig = asig_of(srch_ioa)"
+
+definition
+ rsch_asig :: "'m action signature" where
+ "rsch_asig = asig_of(rsch_ioa)"
+
+definition
+ srch_trans :: "('m action, 'm packet list)transition set" where
+ "srch_trans = trans_of(srch_ioa)"
+definition
+ rsch_trans :: "('m action, bool list)transition set" where
+ "rsch_trans = trans_of(rsch_ioa)"
end
-
-
-
-
-
-
-
-
-
-
-
-
-
--- a/src/HOLCF/IOA/ABP/Abschannel_finite.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Abschannel_finite.thy Sun Oct 21 16:27:42 2007 +0200
@@ -9,54 +9,54 @@
imports Abschannel IOA Action Lemmas
begin
-consts
-
-ch_fin_asig :: "'a abs_action signature"
-
-ch_fin_trans :: "('a abs_action, 'a list)transition set"
-
-ch_fin_ioa :: "('a abs_action, 'a list)ioa"
-
-srch_fin_asig :: "'m action signature"
-rsch_fin_asig :: "'m action signature"
-
-srch_fin_trans :: "('m action, 'm packet list)transition set"
-rsch_fin_trans :: "('m action, bool list)transition set"
-
-srch_fin_ioa :: "('m action, 'm packet list)ioa"
-rsch_fin_ioa :: "('m action, bool list)ioa"
-
-reverse :: "'a list => 'a list"
-
+consts reverse :: "'a list => 'a list"
primrec
reverse_Nil: "reverse([]) = []"
reverse_Cons: "reverse(x#xs) = reverse(xs)@[x]"
-defs
-
-srch_fin_asig_def: "srch_fin_asig == asig_of(srch_fin_ioa)"
-rsch_fin_asig_def: "rsch_fin_asig == asig_of(rsch_fin_ioa)"
+definition
+ ch_fin_asig :: "'a abs_action signature" where
+ "ch_fin_asig = ch_asig"
-srch_fin_trans_def: "srch_fin_trans == trans_of(srch_fin_ioa)"
-rsch_fin_trans_def: "rsch_fin_trans == trans_of(rsch_fin_ioa)"
+definition
+ ch_fin_trans :: "('a abs_action, 'a list)transition set" where
+ "ch_fin_trans =
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of S(b) => ((t = s) |
+ (if (b=hd(reverse(s)) & s~=[]) then t=s else t=s@[b])) |
+ R(b) => s ~= [] &
+ b = hd(s) &
+ ((t = s) | (t = tl(s)))}"
-srch_fin_ioa_def: "srch_fin_ioa == rename ch_fin_ioa srch_actions"
-rsch_fin_ioa_def: "rsch_fin_ioa == rename ch_fin_ioa rsch_actions"
-
+definition
+ ch_fin_ioa :: "('a abs_action, 'a list)ioa" where
+ "ch_fin_ioa = (ch_fin_asig, {[]}, ch_fin_trans,{},{})"
-ch_fin_asig_def: "ch_fin_asig == ch_asig"
+definition
+ srch_fin_ioa :: "('m action, 'm packet list)ioa" where
+ "srch_fin_ioa = rename ch_fin_ioa srch_actions"
+
+definition
+ rsch_fin_ioa :: "('m action, bool list)ioa" where
+ "rsch_fin_ioa = rename ch_fin_ioa rsch_actions"
+
+definition
+ srch_fin_asig :: "'m action signature" where
+ "srch_fin_asig = asig_of(srch_fin_ioa)"
-ch_fin_trans_def: "ch_fin_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in
- case fst(snd(tr))
- of S(b) => ((t = s) |
- (if (b=hd(reverse(s)) & s~=[]) then t=s else t=s@[b])) |
- R(b) => s ~= [] &
- b = hd(s) &
- ((t = s) | (t = tl(s))) }"
+definition
+ rsch_fin_asig :: "'m action signature" where
+ "rsch_fin_asig = asig_of(rsch_fin_ioa)"
-ch_fin_ioa_def: "ch_fin_ioa == (ch_fin_asig, {[]}, ch_fin_trans,{},{})"
+definition
+ srch_fin_trans :: "('m action, 'm packet list)transition set" where
+ "srch_fin_trans = trans_of(srch_fin_ioa)"
+
+definition
+ rsch_fin_trans :: "('m action, bool list)transition set" where
+ "rsch_fin_trans = trans_of(rsch_fin_ioa)"
end
--- a/src/HOLCF/IOA/ABP/Spec.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/ABP/Spec.thy Sun Oct 21 16:27:42 2007 +0200
@@ -9,32 +9,30 @@
imports IOA Action
begin
-consts
-
-spec_sig :: "'m action signature"
-spec_trans :: "('m action, 'm list)transition set"
-spec_ioa :: "('m action, 'm list)ioa"
-
-defs
-
-sig_def: "spec_sig == (UN m.{S_msg(m)},
- UN m.{R_msg(m)} Un {Next},
- {})"
+definition
+ spec_sig :: "'m action signature" where
+ sig_def: "spec_sig = (UN m.{S_msg(m)},
+ UN m.{R_msg(m)} Un {Next},
+ {})"
-trans_def: "spec_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in
- case fst(snd(tr))
- of
- Next => t=s | (* Note that there is condition as in Sender *)
- S_msg(m) => t = s@[m] |
- R_msg(m) => s = (m#t) |
- S_pkt(pkt) => False |
- R_pkt(pkt) => False |
- S_ack(b) => False |
- R_ack(b) => False}"
+definition
+ spec_trans :: "('m action, 'm list)transition set" where
+ trans_def: "spec_trans =
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in
+ case fst(snd(tr))
+ of
+ Next => t=s | (* Note that there is condition as in Sender *)
+ S_msg(m) => t = s@[m] |
+ R_msg(m) => s = (m#t) |
+ S_pkt(pkt) => False |
+ R_pkt(pkt) => False |
+ S_ack(b) => False |
+ R_ack(b) => False}"
-ioa_def: "spec_ioa == (spec_sig, {[]}, spec_trans)"
+definition
+ spec_ioa :: "('m action, 'm list)ioa" where
+ ioa_def: "spec_ioa = (spec_sig, {[]}, spec_trans)"
end
--- a/src/HOLCF/IOA/ex/TrivEx.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/ex/TrivEx.thy Sun Oct 21 16:27:42 2007 +0200
@@ -11,53 +11,42 @@
datatype action = INC
-consts
-
-C_asig :: "action signature"
-C_trans :: "(action, nat)transition set"
-C_ioa :: "(action, nat)ioa"
-
-A_asig :: "action signature"
-A_trans :: "(action, bool)transition set"
-A_ioa :: "(action, bool)ioa"
-
-h_abs :: "nat => bool"
-
-defs
-
-C_asig_def:
- "C_asig == ({},{INC},{})"
-
-C_trans_def: "C_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in case fst(snd(tr))
- of
- INC => t = Suc(s)}"
+definition
+ C_asig :: "action signature" where
+ "C_asig = ({},{INC},{})"
+definition
+ C_trans :: "(action, nat)transition set" where
+ "C_trans =
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in case fst(snd(tr))
+ of
+ INC => t = Suc(s)}"
+definition
+ C_ioa :: "(action, nat)ioa" where
+ "C_ioa = (C_asig, {0}, C_trans,{},{})"
-C_ioa_def: "C_ioa ==
- (C_asig, {0}, C_trans,{},{})"
-
-A_asig_def:
- "A_asig == ({},{INC},{})"
+definition
+ A_asig :: "action signature" where
+ "A_asig = ({},{INC},{})"
+definition
+ A_trans :: "(action, bool)transition set" where
+ "A_trans =
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in case fst(snd(tr))
+ of
+ INC => t = True}"
+definition
+ A_ioa :: "(action, bool)ioa" where
+ "A_ioa = (A_asig, {False}, A_trans,{},{})"
-A_trans_def: "A_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in case fst(snd(tr))
- of
- INC => t = True}"
+definition
+ h_abs :: "nat => bool" where
+ "h_abs n = (n~=0)"
-A_ioa_def: "A_ioa ==
- (A_asig, {False}, A_trans,{},{})"
-
-h_abs_def:
- "h_abs n == n~=0"
-
-axioms
-
-MC_result:
- "validIOA A_ioa (<>[] <%(b,a,c). b>)"
+axiomatization where
+ MC_result: "validIOA A_ioa (<>[] <%(b,a,c). b>)"
lemma h_abs_is_abstraction:
"is_abstraction h_abs C_ioa A_ioa"
--- a/src/HOLCF/IOA/ex/TrivEx2.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/ex/TrivEx2.thy Sun Oct 21 16:27:42 2007 +0200
@@ -11,62 +11,48 @@
datatype action = INC
-consts
-
-C_asig :: "action signature"
-C_trans :: "(action, nat)transition set"
-C_ioa :: "(action, nat)ioa"
-C_live_ioa :: "(action, nat)live_ioa"
-
-A_asig :: "action signature"
-A_trans :: "(action, bool)transition set"
-A_ioa :: "(action, bool)ioa"
-A_live_ioa :: "(action, bool)live_ioa"
-
-h_abs :: "nat => bool"
-
-defs
-
-C_asig_def:
- "C_asig == ({},{INC},{})"
-
-C_trans_def: "C_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in case fst(snd(tr))
- of
- INC => t = Suc(s)}"
+definition
+ C_asig :: "action signature" where
+ "C_asig = ({},{INC},{})"
+definition
+ C_trans :: "(action, nat)transition set" where
+ "C_trans =
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in case fst(snd(tr))
+ of
+ INC => t = Suc(s)}"
+definition
+ C_ioa :: "(action, nat)ioa" where
+ "C_ioa = (C_asig, {0}, C_trans,{},{})"
+definition
+ C_live_ioa :: "(action, nat)live_ioa" where
+ "C_live_ioa = (C_ioa, WF C_ioa {INC})"
-C_ioa_def: "C_ioa ==
- (C_asig, {0}, C_trans,{},{})"
-
-C_live_ioa_def:
- "C_live_ioa == (C_ioa, WF C_ioa {INC})"
-
-A_asig_def:
- "A_asig == ({},{INC},{})"
+definition
+ A_asig :: "action signature" where
+ "A_asig = ({},{INC},{})"
+definition
+ A_trans :: "(action, bool)transition set" where
+ "A_trans =
+ {tr. let s = fst(tr);
+ t = snd(snd(tr))
+ in case fst(snd(tr))
+ of
+ INC => t = True}"
+definition
+ A_ioa :: "(action, bool)ioa" where
+ "A_ioa = (A_asig, {False}, A_trans,{},{})"
+definition
+ A_live_ioa :: "(action, bool)live_ioa" where
+ "A_live_ioa = (A_ioa, WF A_ioa {INC})"
-A_trans_def: "A_trans ==
- {tr. let s = fst(tr);
- t = snd(snd(tr))
- in case fst(snd(tr))
- of
- INC => t = True}"
-
-A_ioa_def: "A_ioa ==
- (A_asig, {False}, A_trans,{},{})"
+definition
+ h_abs :: "nat => bool" where
+ "h_abs n = (n~=0)"
-A_live_ioa_def:
- "A_live_ioa == (A_ioa, WF A_ioa {INC})"
-
-
-h_abs_def:
- "h_abs n == n~=0"
-
-axioms
-
-MC_result:
- "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
+axiomatization where
+ MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
lemma h_abs_is_abstraction:
--- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Sun Oct 21 16:27:42 2007 +0200
@@ -12,69 +12,57 @@
defaultsort type
-consts
+definition
+ cex_abs :: "('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" where
+ "cex_abs f ex = (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))"
+definition
+ -- {* equals cex_abs on Sequences -- after ex2seq application *}
+ cex_absSeq :: "('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq" where
+ "cex_absSeq f = (%s. Map (%(s,a,t). (f s,a,f t))$s)"
- cex_abs ::"('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution"
- cex_absSeq ::"('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq"
-
- is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
+definition
+ is_abstraction ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where
+ "is_abstraction f C A =
+ ((!s:starts_of(C). f(s):starts_of(A)) &
+ (!s t a. reachable C s & s -a--C-> t
+ --> (f s) -a--A-> (f t)))"
- weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool"
- temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool"
- temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool"
+definition
+ weakeningIOA :: "('a,'s2)ioa => ('a,'s1)ioa => ('s1 => 's2) => bool" where
+ "weakeningIOA A C h = (!ex. ex : executions C --> cex_abs h ex : executions A)"
+definition
+ temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where
+ "temp_strengthening Q P h = (!ex. (cex_abs h ex |== Q) --> (ex |== P))"
+definition
+ temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where
+ "temp_weakening Q P h = temp_strengthening (.~ Q) (.~ P) h"
- state_weakening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool"
- state_strengthening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool"
+definition
+ state_strengthening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where
+ "state_strengthening Q P h = (!s t a. Q (h(s),a,h(t)) --> P (s,a,t))"
+definition
+ state_weakening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where
+ "state_weakening Q P h = state_strengthening (.~Q) (.~P) h"
- is_live_abstraction :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
+definition
+ is_live_abstraction :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
+ "is_live_abstraction h CL AM =
+ (is_abstraction h (fst CL) (fst AM) &
+ temp_weakening (snd AM) (snd CL) h)"
-defs
-
-is_abstraction_def:
- "is_abstraction f C A ==
- (!s:starts_of(C). f(s):starts_of(A)) &
- (!s t a. reachable C s & s -a--C-> t
- --> (f s) -a--A-> (f t))"
-
-is_live_abstraction_def:
- "is_live_abstraction h CL AM ==
- is_abstraction h (fst CL) (fst AM) &
- temp_weakening (snd AM) (snd CL) h"
-
-cex_abs_def:
- "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))"
-
-(* equals cex_abs on Sequneces -- after ex2seq application -- *)
-cex_absSeq_def:
- "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))$s"
-
-weakeningIOA_def:
- "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A"
-
-temp_weakening_def:
- "temp_weakening Q P h == temp_strengthening (.~ Q) (.~ P) h"
-
-temp_strengthening_def:
- "temp_strengthening Q P h == ! ex. (cex_abs h ex |== Q) --> (ex |== P)"
-
-state_weakening_def:
- "state_weakening Q P h == state_strengthening (.~Q) (.~P) h"
-
-state_strengthening_def:
- "state_strengthening Q P h == ! s t a. Q (h(s),a,h(t)) --> P (s,a,t)"
-
-axioms
-
+axiomatization where
(* thm about ex2seq which is not provable by induction as ex2seq is not continous *)
ex2seq_abs_cex:
"ex2seq (cex_abs h ex) = cex_absSeq h (ex2seq ex)"
+axiomatization where
(* analog to the proved thm strength_Box - proof skipped as trivial *)
weak_Box:
"temp_weakening P Q h
==> temp_weakening ([] P) ([] Q) h"
+axiomatization where
(* analog to the proved thm strength_Next - proof skipped as trivial *)
weak_Next:
"temp_weakening P Q h
@@ -82,7 +70,7 @@
subsection "cex_abs"
-
+
lemma cex_abs_UU: "cex_abs f (s,UU) = (f s, UU)"
by (simp add: cex_abs_def)
@@ -94,7 +82,7 @@
declare cex_abs_UU [simp] cex_abs_nil [simp] cex_abs_cons [simp]
-
+
subsection "lemmas"
lemma temp_weakening_def2: "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))"
@@ -110,9 +98,9 @@
subsection "Abstraction Rules for Properties"
-lemma exec_frag_abstraction [rule_format]:
- "[| is_abstraction h C A |] ==>
- !s. reachable C s & is_exec_frag C (s,xs)
+lemma exec_frag_abstraction [rule_format]:
+ "[| is_abstraction h C A |] ==>
+ !s. reachable C s & is_exec_frag C (s,xs)
--> is_exec_frag A (cex_abs h (s,xs))"
apply (unfold cex_abs_def)
apply simp
@@ -139,7 +127,7 @@
done
-lemma AbsRuleT1: "[|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |]
+lemma AbsRuleT1: "[|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |]
==> validIOA C P"
apply (drule abs_is_weakening)
apply (simp add: weakeningIOA_def validIOA_def temp_strengthening_def)
@@ -165,9 +153,9 @@
declare IMPLIES_temp_sat [simp] AND_temp_sat [simp] OR_temp_sat [simp] NOT_temp_sat [simp]
-lemma AbsRuleT2:
- "[|is_live_abstraction h (C,L) (A,M);
- validLIOA (A,M) Q; temp_strengthening Q P h |]
+lemma AbsRuleT2:
+ "[|is_live_abstraction h (C,L) (A,M);
+ validLIOA (A,M) Q; temp_strengthening Q P h |]
==> validLIOA (C,L) P"
apply (unfold is_live_abstraction_def)
apply auto
@@ -178,10 +166,10 @@
done
-lemma AbsRuleTImprove:
- "[|is_live_abstraction h (C,L) (A,M);
- validLIOA (A,M) (H1 .--> Q); temp_strengthening Q P h;
- temp_weakening H1 H2 h; validLIOA (C,L) H2 |]
+lemma AbsRuleTImprove:
+ "[|is_live_abstraction h (C,L) (A,M);
+ validLIOA (A,M) (H1 .--> Q); temp_strengthening Q P h;
+ temp_weakening H1 H2 h; validLIOA (C,L) H2 |]
==> validLIOA (C,L) P"
apply (unfold is_live_abstraction_def)
apply auto
@@ -194,7 +182,7 @@
subsection "Correctness of safe abstraction"
-lemma abstraction_is_ref_map:
+lemma abstraction_is_ref_map:
"is_abstraction h C A ==> is_ref_map h C A"
apply (unfold is_abstraction_def is_ref_map_def)
apply (tactic "safe_tac set_cs")
@@ -203,8 +191,8 @@
done
-lemma abs_safety: "[| inp(C)=inp(A); out(C)=out(A);
- is_abstraction h C A |]
+lemma abs_safety: "[| inp(C)=inp(A); out(C)=out(A);
+ is_abstraction h C A |]
==> C =<| A"
apply (simp add: ioa_implements_def)
apply (rule trace_inclusion)
@@ -218,8 +206,8 @@
(* Reduces to Filter (Map fst x) = Filter (Map fst (Map (%(a,t). (a,x)) x),
that is to special Map Lemma *)
-lemma traces_coincide_abs:
- "ext C = ext A
+lemma traces_coincide_abs:
+ "ext C = ext A
==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))"
apply (unfold cex_abs_def mk_trace_def filter_act_def)
apply simp
@@ -231,8 +219,8 @@
is_live_abstraction includes temp_strengthening which is necessarily based
on cex_abs and not on corresp_ex. Thus, the proof is redoone in a more specific
way for cex_abs *)
-lemma abs_liveness: "[| inp(C)=inp(A); out(C)=out(A);
- is_live_abstraction h (C,M) (A,L) |]
+lemma abs_liveness: "[| inp(C)=inp(A); out(C)=out(A);
+ is_live_abstraction h (C,M) (A,L) |]
==> live_implements (C,M) (A,L)"
apply (simp add: is_live_abstraction_def live_implements_def livetraces_def liveexecutions_def)
apply (tactic "safe_tac set_cs")
@@ -243,25 +231,25 @@
apply (rule traces_coincide_abs)
apply (simp (no_asm) add: externals_def)
apply (auto)[1]
-
+
(* cex_abs is execution *)
apply (tactic {* pair_tac "ex" 1 *})
apply (simp add: executions_def)
- (* start state *)
+ (* start state *)
apply (rule conjI)
apply (simp add: is_abstraction_def cex_abs_def)
(* is-execution-fragment *)
apply (erule exec_frag_abstraction)
apply (simp add: reachable.reachable_0)
- (* Liveness *)
+ (* Liveness *)
apply (simp add: temp_weakening_def2)
apply (tactic {* pair_tac "ex" 1 *})
done
(* FIX: NAch Traces.ML bringen *)
-lemma implements_trans:
+lemma implements_trans:
"[| A =<| B; B =<| C|] ==> A =<| C"
apply (unfold ioa_implements_def)
apply auto
@@ -270,11 +258,11 @@
subsection "Abstraction Rules for Automata"
-lemma AbsRuleA1: "[| inp(C)=inp(A); out(C)=out(A);
- inp(Q)=inp(P); out(Q)=out(P);
- is_abstraction h1 C A;
- A =<| Q ;
- is_abstraction h2 Q P |]
+lemma AbsRuleA1: "[| inp(C)=inp(A); out(C)=out(A);
+ inp(Q)=inp(P); out(Q)=out(P);
+ is_abstraction h1 C A;
+ A =<| Q ;
+ is_abstraction h2 Q P |]
==> C =<| P"
apply (drule abs_safety)
apply assumption+
@@ -286,11 +274,11 @@
done
-lemma AbsRuleA2: "!!LC. [| inp(C)=inp(A); out(C)=out(A);
- inp(Q)=inp(P); out(Q)=out(P);
- is_live_abstraction h1 (C,LC) (A,LA);
- live_implements (A,LA) (Q,LQ) ;
- is_live_abstraction h2 (Q,LQ) (P,LP) |]
+lemma AbsRuleA2: "!!LC. [| inp(C)=inp(A); out(C)=out(A);
+ inp(Q)=inp(P); out(Q)=out(P);
+ is_live_abstraction h1 (C,LC) (A,LA);
+ live_implements (A,LA) (Q,LQ) ;
+ is_live_abstraction h2 (Q,LQ) (P,LP) |]
==> live_implements (C,LC) (P,LP)"
apply (drule abs_liveness)
apply assumption+
@@ -307,64 +295,64 @@
subsection "Localizing Temporal Strengthenings and Weakenings"
-lemma strength_AND:
-"[| temp_strengthening P1 Q1 h;
- temp_strengthening P2 Q2 h |]
+lemma strength_AND:
+"[| temp_strengthening P1 Q1 h;
+ temp_strengthening P2 Q2 h |]
==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h"
apply (unfold temp_strengthening_def)
apply auto
done
-lemma strength_OR:
-"[| temp_strengthening P1 Q1 h;
- temp_strengthening P2 Q2 h |]
+lemma strength_OR:
+"[| temp_strengthening P1 Q1 h;
+ temp_strengthening P2 Q2 h |]
==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h"
apply (unfold temp_strengthening_def)
apply auto
done
-lemma strength_NOT:
-"[| temp_weakening P Q h |]
+lemma strength_NOT:
+"[| temp_weakening P Q h |]
==> temp_strengthening (.~ P) (.~ Q) h"
apply (unfold temp_strengthening_def)
apply (simp add: temp_weakening_def2)
apply auto
done
-lemma strength_IMPLIES:
-"[| temp_weakening P1 Q1 h;
- temp_strengthening P2 Q2 h |]
+lemma strength_IMPLIES:
+"[| temp_weakening P1 Q1 h;
+ temp_strengthening P2 Q2 h |]
==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h"
apply (unfold temp_strengthening_def)
apply (simp add: temp_weakening_def2)
done
-lemma weak_AND:
-"[| temp_weakening P1 Q1 h;
- temp_weakening P2 Q2 h |]
+lemma weak_AND:
+"[| temp_weakening P1 Q1 h;
+ temp_weakening P2 Q2 h |]
==> temp_weakening (P1 .& P2) (Q1 .& Q2) h"
apply (simp add: temp_weakening_def2)
done
-lemma weak_OR:
-"[| temp_weakening P1 Q1 h;
- temp_weakening P2 Q2 h |]
+lemma weak_OR:
+"[| temp_weakening P1 Q1 h;
+ temp_weakening P2 Q2 h |]
==> temp_weakening (P1 .| P2) (Q1 .| Q2) h"
apply (simp add: temp_weakening_def2)
done
-lemma weak_NOT:
-"[| temp_strengthening P Q h |]
+lemma weak_NOT:
+"[| temp_strengthening P Q h |]
==> temp_weakening (.~ P) (.~ Q) h"
apply (unfold temp_strengthening_def)
apply (simp add: temp_weakening_def2)
apply auto
done
-lemma weak_IMPLIES:
-"[| temp_strengthening P1 Q1 h;
- temp_weakening P2 Q2 h |]
+lemma weak_IMPLIES:
+"[| temp_strengthening P1 Q1 h;
+ temp_weakening P2 Q2 h |]
==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h"
apply (unfold temp_strengthening_def)
apply (simp add: temp_weakening_def2)
@@ -379,7 +367,7 @@
done
lemma ex2seqConc [rule_format]:
-"Finite s1 -->
+"Finite s1 -->
(! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))"
apply (rule impI)
apply (tactic {* Seq_Finite_induct_tac 1 *})
@@ -399,7 +387,7 @@
(* important property of ex2seq: can be shiftet, as defined "pointwise" *)
-lemma ex2seq_tsuffix:
+lemma ex2seq_tsuffix:
"tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')"
apply (unfold tsuffix_def suffix_def)
apply auto
@@ -419,10 +407,10 @@
done
-(* important property of cex_absSeq: As it is a 1to1 correspondence,
+(* important property of cex_absSeq: As it is a 1to1 correspondence,
properties carry over *)
-lemma cex_absSeq_tsuffix:
+lemma cex_absSeq_tsuffix:
"tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)"
apply (unfold tsuffix_def suffix_def cex_absSeq_def)
apply auto
@@ -433,8 +421,8 @@
done
-lemma strength_Box:
-"[| temp_strengthening P Q h |]
+lemma strength_Box:
+"[| temp_strengthening P Q h |]
==> temp_strengthening ([] P) ([] Q) h"
apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Box_def)
apply (tactic "clarify_tac set_cs 1")
@@ -447,10 +435,10 @@
subsubsection {* Init *}
-lemma strength_Init:
-"[| state_strengthening P Q h |]
+lemma strength_Init:
+"[| state_strengthening P Q h |]
==> temp_strengthening (Init P) (Init Q) h"
-apply (unfold temp_strengthening_def state_strengthening_def
+apply (unfold temp_strengthening_def state_strengthening_def
temp_sat_def satisfies_def Init_def unlift_def)
apply (tactic "safe_tac set_cs")
apply (tactic {* pair_tac "ex" 1 *})
@@ -461,7 +449,7 @@
subsubsection {* Next *}
-lemma TL_ex2seq_UU:
+lemma TL_ex2seq_UU:
"(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)"
apply (tactic {* pair_tac "ex" 1 *})
apply (tactic {* Seq_case_simp_tac "y" 1 *})
@@ -470,7 +458,7 @@
apply (tactic {* pair_tac "a" 1 *})
done
-lemma TL_ex2seq_nil:
+lemma TL_ex2seq_nil:
"(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)"
apply (tactic {* pair_tac "ex" 1 *})
apply (tactic {* Seq_case_simp_tac "y" 1 *})
@@ -484,10 +472,10 @@
apply (tactic {* Seq_induct_tac "s" [] 1 *})
done
-(* important property of cex_absSeq: As it is a 1to1 correspondence,
+(* important property of cex_absSeq: As it is a 1to1 correspondence,
properties carry over *)
-lemma cex_absSeq_TL:
+lemma cex_absSeq_TL:
"cex_absSeq h (TL$s) = (TL$(cex_absSeq h s))"
apply (unfold cex_absSeq_def)
apply (simp add: MapTL)
@@ -502,7 +490,7 @@
apply auto
done
-
+
lemma ex2seqnilTL: "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)"
apply (tactic {* pair_tac "ex" 1 *})
apply (tactic {* Seq_case_simp_tac "y" 1 *})
@@ -512,8 +500,8 @@
done
-lemma strength_Next:
-"[| temp_strengthening P Q h |]
+lemma strength_Next:
+"[| temp_strengthening P Q h |]
==> temp_strengthening (Next P) (Next Q) h"
apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Next_def)
apply simp
@@ -533,8 +521,8 @@
text {* Localizing Temporal Weakenings - 2 *}
-lemma weak_Init:
-"[| state_weakening P Q h |]
+lemma weak_Init:
+"[| state_weakening P Q h |]
==> temp_weakening (Init P) (Init Q) h"
apply (simp add: temp_weakening_def2 state_weakening_def2
temp_sat_def satisfies_def Init_def unlift_def)
@@ -547,8 +535,8 @@
text {* Localizing Temproal Strengthenings - 3 *}
-lemma strength_Diamond:
-"[| temp_strengthening P Q h |]
+lemma strength_Diamond:
+"[| temp_strengthening P Q h |]
==> temp_strengthening (<> P) (<> Q) h"
apply (unfold Diamond_def)
apply (rule strength_NOT)
@@ -556,9 +544,9 @@
apply (erule weak_NOT)
done
-lemma strength_Leadsto:
-"[| temp_weakening P1 P2 h;
- temp_strengthening Q1 Q2 h |]
+lemma strength_Leadsto:
+"[| temp_weakening P1 P2 h;
+ temp_strengthening Q1 Q2 h |]
==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h"
apply (unfold Leadsto_def)
apply (rule strength_Box)
@@ -569,8 +557,8 @@
text {* Localizing Temporal Weakenings - 3 *}
-lemma weak_Diamond:
-"[| temp_weakening P Q h |]
+lemma weak_Diamond:
+"[| temp_weakening P Q h |]
==> temp_weakening (<> P) (<> Q) h"
apply (unfold Diamond_def)
apply (rule weak_NOT)
@@ -578,9 +566,9 @@
apply (erule strength_NOT)
done
-lemma weak_Leadsto:
-"[| temp_strengthening P1 P2 h;
- temp_weakening Q1 Q2 h |]
+lemma weak_Leadsto:
+"[| temp_strengthening P1 P2 h;
+ temp_weakening Q1 Q2 h |]
==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h"
apply (unfold Leadsto_def)
apply (rule weak_Box)
@@ -588,8 +576,8 @@
apply (erule weak_Diamond)
done
-lemma weak_WF:
- " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|]
+lemma weak_WF:
+ " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|]
==> temp_weakening (WF A acts) (WF C acts) h"
apply (unfold WF_def)
apply (rule weak_IMPLIES)
@@ -603,8 +591,8 @@
xt2_def plift_def option_lift_def NOT_def)
done
-lemma weak_SF:
- " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|]
+lemma weak_SF:
+ " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|]
==> temp_weakening (SF A acts) (SF C acts) h"
apply (unfold SF_def)
apply (rule weak_IMPLIES)
@@ -626,18 +614,10 @@
strength_Diamond strength_Leadsto weak_WF weak_SF
ML {*
-
-local
- val weak_strength_lemmas = thms "weak_strength_lemmas"
- val state_strengthening_def = thm "state_strengthening_def"
- val state_weakening_def = thm "state_weakening_def"
-in
-
-fun abstraction_tac i =
+fun abstraction_tac i =
SELECT_GOAL (CLASIMPSET (fn (cs, ss) =>
- auto_tac (cs addSIs weak_strength_lemmas,
- ss addsimps [state_strengthening_def, state_weakening_def]))) i
-end
+ auto_tac (cs addSIs @{thms weak_strength_lemmas},
+ ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))) i
*}
use "ioa_package.ML"
--- a/src/HOLCF/IOA/meta_theory/Asig.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Asig.thy Sun Oct 21 16:27:42 2007 +0200
@@ -12,47 +12,47 @@
types
'a signature = "('a set * 'a set * 'a set)"
-consts
- actions :: "'action signature => 'action set"
- inputs :: "'action signature => 'action set"
- outputs :: "'action signature => 'action set"
- internals :: "'action signature => 'action set"
- externals :: "'action signature => 'action set"
- locals :: "'action signature => 'action set"
- is_asig ::"'action signature => bool"
- mk_ext_asig ::"'action signature => 'action signature"
+definition
+ inputs :: "'action signature => 'action set" where
+ asig_inputs_def: "inputs = fst"
-defs
+definition
+ outputs :: "'action signature => 'action set" where
+ asig_outputs_def: "outputs = (fst o snd)"
+
+definition
+ internals :: "'action signature => 'action set" where
+ asig_internals_def: "internals = (snd o snd)"
-asig_inputs_def: "inputs == fst"
-asig_outputs_def: "outputs == (fst o snd)"
-asig_internals_def: "internals == (snd o snd)"
+definition
+ actions :: "'action signature => 'action set" where
+ "actions(asig) = (inputs(asig) Un outputs(asig) Un internals(asig))"
-actions_def:
- "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
+definition
+ externals :: "'action signature => 'action set" where
+ "externals(asig) = (inputs(asig) Un outputs(asig))"
-externals_def:
- "externals(asig) == (inputs(asig) Un outputs(asig))"
+definition
+ locals :: "'action signature => 'action set" where
+ "locals asig = ((internals asig) Un (outputs asig))"
-locals_def:
- "locals asig == ((internals asig) Un (outputs asig))"
-
-is_asig_def:
- "is_asig(triple) ==
- ((inputs(triple) Int outputs(triple) = {}) &
+definition
+ is_asig :: "'action signature => bool" where
+ "is_asig(triple) =
+ ((inputs(triple) Int outputs(triple) = {}) &
(outputs(triple) Int internals(triple) = {}) &
(inputs(triple) Int internals(triple) = {}))"
-
-mk_ext_asig_def:
- "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
+definition
+ mk_ext_asig :: "'action signature => 'action signature" where
+ "mk_ext_asig(triple) = (inputs(triple), outputs(triple), {})"
lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
-lemma asig_triple_proj:
- "(outputs (a,b,c) = b) &
- (inputs (a,b,c) = a) &
+lemma asig_triple_proj:
+ "(outputs (a,b,c) = b) &
+ (inputs (a,b,c) = a) &
(internals (a,b,c) = c)"
apply (simp add: asig_projections)
done
@@ -91,7 +91,7 @@
apply blast
done
-lemma int_is_not_ext:
+lemma int_is_not_ext:
"[| is_asig (S); x:internals S |] ==> x~:externals S"
apply (unfold externals_def actions_def is_asig_def)
apply simp
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Sun Oct 21 16:27:42 2007 +0200
@@ -9,49 +9,33 @@
imports Traces
begin
-consts
+definition
+ ProjA2 :: "('a,'s * 't)pairs -> ('a,'s)pairs" where
+ "ProjA2 = Map (%x.(fst x,fst(snd x)))"
- ProjA ::"('a,'s * 't)execution => ('a,'s)execution"
- ProjA2 ::"('a,'s * 't)pairs -> ('a,'s)pairs"
- ProjB ::"('a,'s * 't)execution => ('a,'t)execution"
- ProjB2 ::"('a,'s * 't)pairs -> ('a,'t)pairs"
- Filter_ex ::"'a signature => ('a,'s)execution => ('a,'s)execution"
- Filter_ex2 ::"'a signature => ('a,'s)pairs -> ('a,'s)pairs"
- stutter ::"'a signature => ('a,'s)execution => bool"
- stutter2 ::"'a signature => ('a,'s)pairs -> ('s => tr)"
+definition
+ ProjA :: "('a,'s * 't)execution => ('a,'s)execution" where
+ "ProjA ex = (fst (fst ex), ProjA2$(snd ex))"
- par_execs ::"[('a,'s)execution_module,('a,'t)execution_module] => ('a,'s*'t)execution_module"
-
-
-defs
-
-
-ProjA_def:
- "ProjA ex == (fst (fst ex), ProjA2$(snd ex))"
+definition
+ ProjB2 :: "('a,'s * 't)pairs -> ('a,'t)pairs" where
+ "ProjB2 = Map (%x.(fst x,snd(snd x)))"
-ProjB_def:
- "ProjB ex == (snd (fst ex), ProjB2$(snd ex))"
-
+definition
+ ProjB :: "('a,'s * 't)execution => ('a,'t)execution" where
+ "ProjB ex = (snd (fst ex), ProjB2$(snd ex))"
-ProjA2_def:
- "ProjA2 == Map (%x.(fst x,fst(snd x)))"
-
-ProjB2_def:
- "ProjB2 == Map (%x.(fst x,snd(snd x)))"
-
+definition
+ Filter_ex2 :: "'a signature => ('a,'s)pairs -> ('a,'s)pairs" where
+ "Filter_ex2 sig = Filter (%x. fst x:actions sig)"
-Filter_ex_def:
- "Filter_ex sig ex == (fst ex,Filter_ex2 sig$(snd ex))"
-
+definition
+ Filter_ex :: "'a signature => ('a,'s)execution => ('a,'s)execution" where
+ "Filter_ex sig ex = (fst ex,Filter_ex2 sig$(snd ex))"
-Filter_ex2_def:
- "Filter_ex2 sig == Filter (%x. fst x:actions sig)"
-
-stutter_def:
- "stutter sig ex == ((stutter2 sig$(snd ex)) (fst ex) ~= FF)"
-
-stutter2_def:
- "stutter2 sig ==(fix$(LAM h ex. (%s. case ex of
+definition
+ stutter2 :: "'a signature => ('a,'s)pairs -> ('s => tr)" where
+ "stutter2 sig = (fix$(LAM h ex. (%s. case ex of
nil => TT
| x##xs => (flift1
(%p.(If Def ((fst p)~:actions sig)
@@ -61,9 +45,14 @@
$x)
)))"
-par_execs_def:
- "par_execs ExecsA ExecsB ==
- let exA = fst ExecsA; sigA = snd ExecsA;
+definition
+ stutter :: "'a signature => ('a,'s)execution => bool" where
+ "stutter sig ex = ((stutter2 sig$(snd ex)) (fst ex) ~= FF)"
+
+definition
+ par_execs :: "[('a,'s)execution_module,('a,'t)execution_module] => ('a,'s*'t)execution_module" where
+ "par_execs ExecsA ExecsB =
+ (let exA = fst ExecsA; sigA = snd ExecsA;
exB = fst ExecsB; sigB = snd ExecsB
in
( {ex. Filter_ex sigA (ProjA ex) : exA}
@@ -71,8 +60,7 @@
Int {ex. stutter sigA (ProjA ex)}
Int {ex. stutter sigB (ProjB ex)}
Int {ex. Forall (%x. fst x:(actions sigA Un actions sigB)) (snd ex)},
- asig_comp sigA sigB)"
-
+ asig_comp sigA sigB))"
lemmas [simp del] = ex_simps all_simps split_paired_All
@@ -131,9 +119,9 @@
apply (simp add: Filter_ex2_def)
done
-lemma Filter_ex2_cons: "Filter_ex2 sig$(at >> xs) =
- (if (fst at:actions sig)
- then at >> (Filter_ex2 sig$xs)
+lemma Filter_ex2_cons: "Filter_ex2 sig$(at >> xs) =
+ (if (fst at:actions sig)
+ then at >> (Filter_ex2 sig$xs)
else Filter_ex2 sig$xs)"
apply (simp add: Filter_ex2_def)
@@ -145,18 +133,18 @@
(* ---------------------------------------------------------------- *)
-lemma stutter2_unfold: "stutter2 sig = (LAM ex. (%s. case ex of
- nil => TT
- | x##xs => (flift1
- (%p.(If Def ((fst p)~:actions sig)
- then Def (s=(snd p))
- else TT fi)
- andalso (stutter2 sig$xs) (snd p))
- $x)
+lemma stutter2_unfold: "stutter2 sig = (LAM ex. (%s. case ex of
+ nil => TT
+ | x##xs => (flift1
+ (%p.(If Def ((fst p)~:actions sig)
+ then Def (s=(snd p))
+ else TT fi)
+ andalso (stutter2 sig$xs) (snd p))
+ $x)
))"
apply (rule trans)
apply (rule fix_eq2)
-apply (rule stutter2_def)
+apply (simp only: stutter2_def)
apply (rule beta_cfun)
apply (simp add: flift1_def)
done
@@ -171,8 +159,8 @@
apply simp
done
-lemma stutter2_cons: "(stutter2 sig$(at>>xs)) s =
- ((if (fst at)~:actions sig then Def (s=snd at) else TT)
+lemma stutter2_cons: "(stutter2 sig$(at>>xs)) s =
+ ((if (fst at)~:actions sig then Def (s=snd at) else TT)
andalso (stutter2 sig$xs) (snd at))"
apply (rule trans)
apply (subst stutter2_unfold)
@@ -196,7 +184,7 @@
apply (simp add: stutter_def)
done
-lemma stutter_cons: "stutter sig (s, (a,t)>>ex) =
+lemma stutter_cons: "stutter sig (s, (a,t)>>ex) =
((a~:actions sig --> (s=t)) & stutter sig (t,ex))"
apply (simp add: stutter_def)
done
@@ -224,8 +212,8 @@
(* Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B *)
(* --------------------------------------------------------------------- *)
-lemma lemma_1_1a: "!s. is_exec_frag (A||B) (s,xs)
- --> is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &
+lemma lemma_1_1a: "!s. is_exec_frag (A||B) (s,xs)
+ --> is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &
is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))"
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
@@ -240,8 +228,8 @@
(* Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections *)
(* --------------------------------------------------------------------- *)
-lemma lemma_1_1b: "!s. is_exec_frag (A||B) (s,xs)
- --> stutter (asig_of A) (fst s,ProjA2$xs) &
+lemma lemma_1_1b: "!s. is_exec_frag (A||B) (s,xs)
+ --> stutter (asig_of A) (fst s,ProjA2$xs) &
stutter (asig_of B) (snd s,ProjB2$xs)"
apply (tactic {* pair_induct_tac "xs" [thm "stutter_def", thm "is_exec_frag_def"] 1 *})
@@ -255,7 +243,7 @@
(* Lemma_1_1c : Executions of A||B have only A- or B-actions *)
(* --------------------------------------------------------------------- *)
-lemma lemma_1_1c: "!s. (is_exec_frag (A||B) (s,xs)
+lemma lemma_1_1c: "!s. (is_exec_frag (A||B) (s,xs)
--> Forall (%x. fst x:act (A||B)) xs)"
apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
@@ -270,12 +258,12 @@
(* Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B) *)
(* ----------------------------------------------------------------------- *)
-lemma lemma_1_2:
-"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)$(ProjA2$xs)) &
- is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) &
- stutter (asig_of A) (fst s,(ProjA2$xs)) &
- stutter (asig_of B) (snd s,(ProjB2$xs)) &
- Forall (%x. fst x:act (A||B)) xs
+lemma lemma_1_2:
+"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)$(ProjA2$xs)) &
+ is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) &
+ stutter (asig_of A) (fst s,(ProjA2$xs)) &
+ stutter (asig_of B) (snd s,(ProjB2$xs)) &
+ Forall (%x. fst x:act (A||B)) xs
--> is_exec_frag (A||B) (s,xs)"
apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
@@ -289,11 +277,11 @@
subsection {* COMPOSITIONALITY on EXECUTION Level -- Main Theorem *}
-lemma compositionality_ex:
-"(ex:executions(A||B)) =
- (Filter_ex (asig_of A) (ProjA ex) : executions A &
- Filter_ex (asig_of B) (ProjB ex) : executions B &
- stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &
+lemma compositionality_ex:
+"(ex:executions(A||B)) =
+ (Filter_ex (asig_of A) (ProjA ex) : executions A &
+ Filter_ex (asig_of B) (ProjB ex) : executions B &
+ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &
Forall (%x. fst x:act (A||B)) (snd ex))"
apply (simp (no_asm) add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par)
@@ -310,7 +298,7 @@
subsection {* COMPOSITIONALITY on EXECUTION Level -- for Modules *}
-lemma compositionality_ex_modules:
+lemma compositionality_ex_modules:
"Execs (A||B) = par_execs (Execs A) (Execs B)"
apply (unfold Execs_def par_execs_def)
apply (simp add: asig_of_par)
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Sun Oct 21 16:27:42 2007 +0200
@@ -9,25 +9,11 @@
imports CompoExecs
begin
-consts
-
- mkex ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq =>
- ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution"
- mkex2 ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq ->
+definition
+ mkex2 :: "('a,'s)ioa => ('a,'t)ioa => 'a Seq ->
('a,'s)pairs -> ('a,'t)pairs ->
- ('s => 't => ('a,'s*'t)pairs)"
- par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module"
-
-
-defs
-
-mkex_def:
- "mkex A B sch exA exB ==
- ((fst exA,fst exB),
- (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))"
-
-mkex2_def:
- "mkex2 A B == (fix$(LAM h sch exA exB. (%s t. case sch of
+ ('s => 't => ('a,'s*'t)pairs)" where
+ "mkex2 A B = (fix$(LAM h sch exA exB. (%s t. case sch of
nil => nil
| x##xs =>
(case x of
@@ -60,15 +46,23 @@
)
))))"
-par_scheds_def:
- "par_scheds SchedsA SchedsB ==
- let schA = fst SchedsA; sigA = snd SchedsA;
+definition
+ mkex :: "('a,'s)ioa => ('a,'t)ioa => 'a Seq =>
+ ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution" where
+ "mkex A B sch exA exB =
+ ((fst exA,fst exB),
+ (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))"
+
+definition
+ par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module" where
+ "par_scheds SchedsA SchedsB =
+ (let schA = fst SchedsA; sigA = snd SchedsA;
schB = fst SchedsB; sigB = snd SchedsB
in
( {sch. Filter (%a. a:actions sigA)$sch : schA}
Int {sch. Filter (%a. a:actions sigB)$sch : schB}
Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
- asig_comp sigA sigB)"
+ asig_comp sigA sigB))"
declare surjective_pairing [symmetric, simp]
@@ -78,41 +72,41 @@
lemma mkex2_unfold:
-"mkex2 A B = (LAM sch exA exB. (%s t. case sch of
- nil => nil
- | x##xs =>
- (case x of
- UU => UU
- | Def y =>
- (if y:act A then
- (if y:act B then
- (case HD$exA of
- UU => UU
- | Def a => (case HD$exB of
- UU => UU
- | Def b =>
- (y,(snd a,snd b))>>
- (mkex2 A B$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
- else
- (case HD$exA of
- UU => UU
- | Def a =>
- (y,(snd a,t))>>(mkex2 A B$xs$(TL$exA)$exB) (snd a) t)
- )
- else
- (if y:act B then
- (case HD$exB of
- UU => UU
- | Def b =>
- (y,(s,snd b))>>(mkex2 A B$xs$exA$(TL$exB)) s (snd b))
- else
- UU
- )
- )
+"mkex2 A B = (LAM sch exA exB. (%s t. case sch of
+ nil => nil
+ | x##xs =>
+ (case x of
+ UU => UU
+ | Def y =>
+ (if y:act A then
+ (if y:act B then
+ (case HD$exA of
+ UU => UU
+ | Def a => (case HD$exB of
+ UU => UU
+ | Def b =>
+ (y,(snd a,snd b))>>
+ (mkex2 A B$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
+ else
+ (case HD$exA of
+ UU => UU
+ | Def a =>
+ (y,(snd a,t))>>(mkex2 A B$xs$(TL$exA)$exB) (snd a) t)
+ )
+ else
+ (if y:act B then
+ (case HD$exB of
+ UU => UU
+ | Def b =>
+ (y,(s,snd b))>>(mkex2 A B$xs$exA$(TL$exB)) s (snd b))
+ else
+ UU
+ )
+ )
)))"
apply (rule trans)
apply (rule fix_eq2)
-apply (rule mkex2_def)
+apply (simp only: mkex2_def)
apply (rule beta_cfun)
apply simp
done
@@ -127,8 +121,8 @@
apply simp
done
-lemma mkex2_cons_1: "[| x:act A; x~:act B; HD$exA=Def a|]
- ==> (mkex2 A B$(x>>sch)$exA$exB) s t =
+lemma mkex2_cons_1: "[| x:act A; x~:act B; HD$exA=Def a|]
+ ==> (mkex2 A B$(x>>sch)$exA$exB) s t =
(x,snd a,t) >> (mkex2 A B$sch$(TL$exA)$exB) (snd a) t"
apply (rule trans)
apply (subst mkex2_unfold)
@@ -136,8 +130,8 @@
apply (simp add: Consq_def)
done
-lemma mkex2_cons_2: "[| x~:act A; x:act B; HD$exB=Def b|]
- ==> (mkex2 A B$(x>>sch)$exA$exB) s t =
+lemma mkex2_cons_2: "[| x~:act A; x:act B; HD$exB=Def b|]
+ ==> (mkex2 A B$(x>>sch)$exA$exB) s t =
(x,s,snd b) >> (mkex2 A B$sch$exA$(TL$exB)) s (snd b)"
apply (rule trans)
apply (subst mkex2_unfold)
@@ -145,9 +139,9 @@
apply (simp add: Consq_def)
done
-lemma mkex2_cons_3: "[| x:act A; x:act B; HD$exA=Def a;HD$exB=Def b|]
- ==> (mkex2 A B$(x>>sch)$exA$exB) s t =
- (x,snd a,snd b) >>
+lemma mkex2_cons_3: "[| x:act A; x:act B; HD$exA=Def a;HD$exB=Def b|]
+ ==> (mkex2 A B$(x>>sch)$exA$exB) s t =
+ (x,snd a,snd b) >>
(mkex2 A B$sch$(TL$exA)$(TL$exB)) (snd a) (snd b)"
apply (rule trans)
apply (subst mkex2_unfold)
@@ -169,24 +163,24 @@
apply (simp add: mkex_def)
done
-lemma mkex_cons_1: "[| x:act A; x~:act B |]
- ==> mkex A B (x>>sch) (s,a>>exA) (t,exB) =
+lemma mkex_cons_1: "[| x:act A; x~:act B |]
+ ==> mkex A B (x>>sch) (s,a>>exA) (t,exB) =
((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))"
apply (simp (no_asm) add: mkex_def)
apply (cut_tac exA = "a>>exA" in mkex2_cons_1)
apply auto
done
-lemma mkex_cons_2: "[| x~:act A; x:act B |]
- ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) =
+lemma mkex_cons_2: "[| x~:act A; x:act B |]
+ ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) =
((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))"
apply (simp (no_asm) add: mkex_def)
apply (cut_tac exB = "b>>exB" in mkex2_cons_2)
apply auto
done
-lemma mkex_cons_3: "[| x:act A; x:act B |]
- ==> mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) =
+lemma mkex_cons_3: "[| x:act A; x:act B |]
+ ==> mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) =
((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))"
apply (simp (no_asm) add: mkex_def)
apply (cut_tac exB = "b>>exB" and exA = "a>>exA" in mkex2_cons_3)
@@ -209,8 +203,8 @@
(* Lemma_2_1 : tfilter(ex) and filter_act are commutative *)
(* --------------------------------------------------------------------- *)
-lemma lemma_2_1a:
- "filter_act$(Filter_ex2 (asig_of A)$xs)=
+lemma lemma_2_1a:
+ "filter_act$(Filter_ex2 (asig_of A)$xs)=
Filter (%a. a:act A)$(filter_act$xs)"
apply (unfold filter_act_def Filter_ex2_def)
@@ -222,8 +216,8 @@
(* Lemma_2_2 : State-projections do not affect filter_act *)
(* --------------------------------------------------------------------- *)
-lemma lemma_2_1b:
- "filter_act$(ProjA2$xs) =filter_act$xs &
+lemma lemma_2_1b:
+ "filter_act$(ProjA2$xs) =filter_act$xs &
filter_act$(ProjB2$xs) =filter_act$xs"
apply (tactic {* pair_induct_tac "xs" [] 1 *})
done
@@ -237,7 +231,7 @@
an ex is in A or B, but after projecting it onto the action schedule. Of course, this
is the same proposition, but we cannot change this one, when then rather lemma_1_1c *)
-lemma sch_actions_in_AorB: "!s. is_exec_frag (A||B) (s,xs)
+lemma sch_actions_in_AorB: "!s. is_exec_frag (A||B) (s,xs)
--> Forall (%x. x:act (A||B)) (filter_act$xs)"
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def", thm "Forall_def",
@@ -255,10 +249,10 @@
structural induction
--------------------------------------------------------------------------- *)
-lemma Mapfst_mkex_is_sch: "! exA exB s t.
- Forall (%x. x:act (A||B)) sch &
- Filter (%a. a:act A)$sch << filter_act$exA &
- Filter (%a. a:act B)$sch << filter_act$exB
+lemma Mapfst_mkex_is_sch: "! exA exB s t.
+ Forall (%x. x:act (A||B)) sch &
+ Filter (%a. a:act A)$sch << filter_act$exA &
+ Filter (%a. a:act B)$sch << filter_act$exB
--> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch"
apply (tactic {* Seq_induct_tac "sch" [thm "Filter_def", thm "Forall_def",
@@ -327,20 +321,20 @@
structural induction
--------------------------------------------------------------------------- *)
-lemma stutterA_mkex: "! exA exB s t.
- Forall (%x. x:act (A||B)) sch &
- Filter (%a. a:act A)$sch << filter_act$exA &
- Filter (%a. a:act B)$sch << filter_act$exB
+lemma stutterA_mkex: "! exA exB s t.
+ Forall (%x. x:act (A||B)) sch &
+ Filter (%a. a:act A)$sch << filter_act$exA &
+ Filter (%a. a:act B)$sch << filter_act$exB
--> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))"
apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
done
-lemma stutter_mkex_on_A: "[|
- Forall (%x. x:act (A||B)) sch ;
- Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
- Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
+lemma stutter_mkex_on_A: "[|
+ Forall (%x. x:act (A||B)) sch ;
+ Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
+ Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))"
apply (cut_tac stutterA_mkex)
@@ -357,19 +351,19 @@
structural induction
--------------------------------------------------------------------------- *)
-lemma stutterB_mkex: "! exA exB s t.
- Forall (%x. x:act (A||B)) sch &
- Filter (%a. a:act A)$sch << filter_act$exA &
- Filter (%a. a:act B)$sch << filter_act$exB
+lemma stutterB_mkex: "! exA exB s t.
+ Forall (%x. x:act (A||B)) sch &
+ Filter (%a. a:act A)$sch << filter_act$exA &
+ Filter (%a. a:act B)$sch << filter_act$exB
--> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))"
apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
done
-lemma stutter_mkex_on_B: "[|
- Forall (%x. x:act (A||B)) sch ;
- Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
- Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
+lemma stutter_mkex_on_B: "[|
+ Forall (%x. x:act (A||B)) sch ;
+ Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
+ Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))"
apply (cut_tac stutterB_mkex)
apply (simp add: stutter_def ProjB_def mkex_def)
@@ -387,11 +381,11 @@
structural induction
--------------------------------------------------------------------------- *)
-lemma filter_mkex_is_exA_tmp: "! exA exB s t.
- Forall (%x. x:act (A||B)) sch &
- Filter (%a. a:act A)$sch << filter_act$exA &
- Filter (%a. a:act B)$sch << filter_act$exB
- --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) =
+lemma filter_mkex_is_exA_tmp: "! exA exB s t.
+ Forall (%x. x:act (A||B)) sch &
+ Filter (%a. a:act A)$sch << filter_act$exA &
+ Filter (%a. a:act B)$sch << filter_act$exB
+ --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) =
Zip$(Filter (%a. a:act A)$sch)$(Map snd$exA)"
apply (tactic {* mkex_induct_tac "sch" "exB" "exA" *})
done
@@ -411,8 +405,8 @@
lemma for eliminating non admissible equations in assumptions
--------------------------------------------------------------------------- *)
-lemma trick_against_eq_in_ass: "!! sch ex.
- Filter (%a. a:act AB)$sch = filter_act$ex
+lemma trick_against_eq_in_ass: "!! sch ex.
+ Filter (%a. a:act AB)$sch = filter_act$ex
==> ex = Zip$(Filter (%a. a:act AB)$sch)$(Map snd$ex)"
apply (simp add: filter_act_def)
apply (rule Zip_Map_fst_snd [symmetric])
@@ -424,10 +418,10 @@
--------------------------------------------------------------------------- *)
-lemma filter_mkex_is_exA: "!!sch exA exB.
- [| Forall (%a. a:act (A||B)) sch ;
- Filter (%a. a:act A)$sch = filter_act$(snd exA) ;
- Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
+lemma filter_mkex_is_exA: "!!sch exA exB.
+ [| Forall (%a. a:act (A||B)) sch ;
+ Filter (%a. a:act A)$sch = filter_act$(snd exA) ;
+ Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
apply (simp add: ProjA_def Filter_ex_def)
apply (tactic {* pair_tac "exA" 1 *})
@@ -448,11 +442,11 @@
structural induction
--------------------------------------------------------------------------- *)
-lemma filter_mkex_is_exB_tmp: "! exA exB s t.
- Forall (%x. x:act (A||B)) sch &
- Filter (%a. a:act A)$sch << filter_act$exA &
- Filter (%a. a:act B)$sch << filter_act$exB
- --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) =
+lemma filter_mkex_is_exB_tmp: "! exA exB s t.
+ Forall (%x. x:act (A||B)) sch &
+ Filter (%a. a:act A)$sch << filter_act$exA &
+ Filter (%a. a:act B)$sch << filter_act$exB
+ --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) =
Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)"
(* notice necessary change of arguments exA and exB *)
@@ -466,10 +460,10 @@
--------------------------------------------------------------------------- *)
-lemma filter_mkex_is_exB: "!!sch exA exB.
- [| Forall (%a. a:act (A||B)) sch ;
- Filter (%a. a:act A)$sch = filter_act$(snd exA) ;
- Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
+lemma filter_mkex_is_exB: "!!sch exA exB.
+ [| Forall (%a. a:act (A||B)) sch ;
+ Filter (%a. a:act A)$sch = filter_act$(snd exA) ;
+ Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
apply (simp add: ProjB_def Filter_ex_def)
apply (tactic {* pair_tac "exA" 1 *})
@@ -487,11 +481,11 @@
(* --------------------------------------------------------------------- *)
-lemma mkex_actions_in_AorB: "!s t exA exB.
- Forall (%x. x : act (A || B)) sch &
- Filter (%a. a:act A)$sch << filter_act$exA &
- Filter (%a. a:act B)$sch << filter_act$exB
- --> Forall (%x. fst x : act (A ||B))
+lemma mkex_actions_in_AorB: "!s t exA exB.
+ Forall (%x. x : act (A || B)) sch &
+ Filter (%a. a:act A)$sch << filter_act$exA &
+ Filter (%a. a:act B)$sch << filter_act$exB
+ --> Forall (%x. fst x : act (A ||B))
(snd (mkex A B sch (s,exA) (t,exB)))"
apply (tactic {* mkex_induct_tac "sch" "exA" "exB" *})
done
@@ -502,10 +496,10 @@
(* Main Theorem *)
(* ------------------------------------------------------------------ *)
-lemma compositionality_sch:
-"(sch : schedules (A||B)) =
- (Filter (%a. a:act A)$sch : schedules A &
- Filter (%a. a:act B)$sch : schedules B &
+lemma compositionality_sch:
+"(sch : schedules (A||B)) =
+ (Filter (%a. a:act A)$sch : schedules A &
+ Filter (%a. a:act B)$sch : schedules B &
Forall (%x. x:act (A||B)) sch)"
apply (simp (no_asm) add: schedules_def has_schedule_def)
apply (tactic "safe_tac set_cs")
@@ -545,7 +539,7 @@
subsection {* COMPOSITIONALITY on SCHEDULE Level -- for Modules *}
-lemma compositionality_sch_modules:
+lemma compositionality_sch_modules:
"Scheds (A||B) = par_scheds (Scheds A) (Scheds B)"
apply (unfold Scheds_def par_scheds_def)
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.thy Sun Oct 21 16:27:42 2007 +0200
@@ -14,54 +14,40 @@
types
('a, 's) live_ioa = "('a,'s)ioa * ('a,'s)ioa_temp"
-consts
-
-validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp => bool"
-
-WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp"
-SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp"
+definition
+ validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp => bool" where
+ "validLIOA AL P = validIOA (fst AL) ((snd AL) .--> P)"
-liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set"
-livetraces :: "('a,'s)live_ioa => 'a trace set"
-live_implements :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
-is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool"
-
-
-defs
-
-validLIOA_def:
- "validLIOA AL P == validIOA (fst AL) ((snd AL) .--> P)"
-
+definition
+ WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
+ "WF A acts = (<> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>)"
+definition
+ SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
+ "SF A acts = ([] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>)"
-WF_def:
- "WF A acts == <> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
-
-SF_def:
- "SF A acts == [] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>"
-
-
-liveexecutions_def:
- "liveexecutions AP == {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
-
-livetraces_def:
- "livetraces AP == {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
-
-live_implements_def:
- "live_implements CL AM == (inp (fst CL) = inp (fst AM)) &
+definition
+ liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where
+ "liveexecutions AP = {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
+definition
+ livetraces :: "('a,'s)live_ioa => 'a trace set" where
+ "livetraces AP = {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
+definition
+ live_implements :: "('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
+ "live_implements CL AM = ((inp (fst CL) = inp (fst AM)) &
(out (fst CL) = out (fst AM)) &
- livetraces CL <= livetraces AM"
-
-is_live_ref_map_def:
- "is_live_ref_map f CL AM ==
- is_ref_map f (fst CL ) (fst AM) &
+ livetraces CL <= livetraces AM)"
+definition
+ is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
+ "is_live_ref_map f CL AM =
+ (is_ref_map f (fst CL ) (fst AM) &
(! exec : executions (fst CL). (exec |== (snd CL)) -->
- ((corresp_ex (fst AM) f exec) |== (snd AM)))"
+ ((corresp_ex (fst AM) f exec) |== (snd AM))))"
declare split_paired_Ex [simp del]
-lemma live_implements_trans:
-"!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |]
+lemma live_implements_trans:
+"!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |]
==> live_implements (A,LA) (C,LC)"
apply (unfold live_implements_def)
apply auto
@@ -69,9 +55,9 @@
subsection "Correctness of live refmap"
-
-lemma live_implements: "[| inp(C)=inp(A); out(C)=out(A);
- is_live_ref_map f (C,M) (A,L) |]
+
+lemma live_implements: "[| inp(C)=inp(A); out(C)=out(A);
+ is_live_ref_map f (C,M) (A,L) |]
==> live_implements (C,M) (A,L)"
apply (simp add: is_live_ref_map_def live_implements_def livetraces_def liveexecutions_def)
apply (tactic "safe_tac set_cs")
@@ -83,11 +69,11 @@
apply (simp (no_asm) add: externals_def)
apply (auto)[1]
apply (simp add: executions_def reachable.reachable_0)
-
+
(* corresp_ex is execution, Lemma 2 *)
apply (tactic {* pair_tac "ex" 1 *})
apply (simp add: executions_def)
- (* start state *)
+ (* start state *)
apply (rule conjI)
apply (simp add: is_ref_map_def corresp_ex_def)
(* is-execution-fragment *)
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Sun Oct 21 16:27:42 2007 +0200
@@ -9,48 +9,42 @@
imports RefMappings
begin
-consts
-
- corresp_ex ::"('a,'s2)ioa => ('s1 => 's2) =>
- ('a,'s1)execution => ('a,'s2)execution"
- corresp_exC ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
- -> ('s1 => ('a,'s2)pairs)"
- is_fair_ref_map :: "('s1 => 's2) => ('a,'s1)ioa => ('a,'s2)ioa => bool"
-
-defs
-
-corresp_ex_def:
- "corresp_ex A f ex == (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))"
-
-
-corresp_exC_def:
- "corresp_exC A f == (fix$(LAM h ex. (%s. case ex of
+definition
+ corresp_exC :: "('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs
+ -> ('s1 => ('a,'s2)pairs)" where
+ "corresp_exC A f = (fix$(LAM h ex. (%s. case ex of
nil => nil
| x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))
@@ ((h$xs) (snd pr)))
$x) )))"
+definition
+ corresp_ex :: "('a,'s2)ioa => ('s1 => 's2) =>
+ ('a,'s1)execution => ('a,'s2)execution" where
+ "corresp_ex A f ex = (f (fst ex),(corresp_exC A f$(snd ex)) (fst ex))"
-is_fair_ref_map_def:
- "is_fair_ref_map f C A ==
- is_ref_map f C A &
- (! ex : executions(C). fair_ex C ex --> fair_ex A (corresp_ex A f ex))"
+definition
+ is_fair_ref_map :: "('s1 => 's2) => ('a,'s1)ioa => ('a,'s2)ioa => bool" where
+ "is_fair_ref_map f C A =
+ (is_ref_map f C A &
+ (! ex : executions(C). fair_ex C ex --> fair_ex A (corresp_ex A f ex)))"
-
-
-axioms
(* Axioms for fair trace inclusion proof support, not for the correctness proof
of refinement mappings!
Note: Everything is superseded by LiveIOA.thy! *)
+axiomatization where
corresp_laststate:
"Finite ex ==> laststate (corresp_ex A f (s,ex)) = f (laststate (s,ex))"
+axiomatization where
corresp_Finite:
"Finite (snd (corresp_ex A f (s,ex))) = Finite ex"
+axiomatization where
FromAtoC:
"fin_often (%x. P (snd x)) (snd (corresp_ex A f (s,ex))) ==> fin_often (%y. P (f (snd y))) ex"
+axiomatization where
FromCtoA:
"inf_often (%y. P (fst y)) ex ==> inf_often (%x. P (fst x)) (snd (corresp_ex A f (s,ex)))"
@@ -59,10 +53,12 @@
an index i from which on no W in ex. But W inf enabled, ie at least once after i
W is enabled. As W does not occur after i and W is enabling_persistent, W keeps
enabled until infinity, ie. indefinitely *)
+axiomatization where
persistent:
"[|inf_often (%x. Enabled A W (snd x)) ex; en_persistent A W|]
==> inf_often (%x. fst x :W) ex | fin_often (%x. ~Enabled A W (snd x)) ex"
+axiomatization where
infpostcond:
"[| is_exec_frag A (s,ex); inf_often (%x. fst x:W) ex|]
==> inf_often (% x. set_was_enabled A W (snd x)) ex"
@@ -70,14 +66,14 @@
subsection "corresp_ex"
-lemma corresp_exC_unfold: "corresp_exC A f = (LAM ex. (%s. case ex of
- nil => nil
- | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))
- @@ ((corresp_exC A f $xs) (snd pr)))
+lemma corresp_exC_unfold: "corresp_exC A f = (LAM ex. (%s. case ex of
+ nil => nil
+ | x##xs => (flift1 (%pr. (@cex. move A cex (f s) (fst pr) (f (snd pr)))
+ @@ ((corresp_exC A f $xs) (snd pr)))
$x) ))"
apply (rule trans)
apply (rule fix_eq2)
-apply (rule corresp_exC_def)
+apply (simp only: corresp_exC_def)
apply (rule beta_cfun)
apply (simp add: flift1_def)
done
@@ -92,8 +88,8 @@
apply simp
done
-lemma corresp_exC_cons: "(corresp_exC A f$(at>>xs)) s =
- (@cex. move A cex (f s) (fst at) (f (snd at)))
+lemma corresp_exC_cons: "(corresp_exC A f$(at>>xs)) s =
+ (@cex. move A cex (f s) (fst at) (f (snd at)))
@@ ((corresp_exC A f$xs) (snd at))"
apply (rule trans)
apply (subst corresp_exC_unfold)
@@ -108,8 +104,8 @@
subsection "properties of move"
-lemma move_is_move:
- "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
+lemma move_is_move:
+ "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
move A (@x. move A x (f s) a (f t)) (f s) a (f t)"
apply (unfold is_ref_map_def)
apply (subgoal_tac "? ex. move A ex (f s) a (f t) ")
@@ -120,8 +116,8 @@
apply assumption
done
-lemma move_subprop1:
- "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
+lemma move_subprop1:
+ "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
is_exec_frag A (f s,@x. move A x (f s) a (f t))"
apply (cut_tac move_is_move)
defer
@@ -129,8 +125,8 @@
apply (simp add: move_def)
done
-lemma move_subprop2:
- "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
+lemma move_subprop2:
+ "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
Finite ((@x. move A x (f s) a (f t)))"
apply (cut_tac move_is_move)
defer
@@ -138,8 +134,8 @@
apply (simp add: move_def)
done
-lemma move_subprop3:
- "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
+lemma move_subprop3:
+ "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
laststate (f s,@x. move A x (f s) a (f t)) = (f t)"
apply (cut_tac move_is_move)
defer
@@ -147,9 +143,9 @@
apply (simp add: move_def)
done
-lemma move_subprop4:
- "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
- mk_trace A$((@x. move A x (f s) a (f t))) =
+lemma move_subprop4:
+ "[|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>
+ mk_trace A$((@x. move A x (f s) a (f t))) =
(if a:ext A then a>>nil else nil)"
apply (cut_tac move_is_move)
defer
@@ -180,9 +176,9 @@
------------------------------------------------------- *)
declare split_if [split del]
-lemma lemma_1:
- "[|is_ref_map f C A; ext C = ext A|] ==>
- !s. reachable C s & is_exec_frag C (s,xs) -->
+lemma lemma_1:
+ "[|is_ref_map f C A; ext C = ext A|] ==>
+ !s. reachable C s & is_exec_frag C (s,xs) -->
mk_trace C$xs = mk_trace A$(snd (corresp_ex A f (s,xs)))"
apply (unfold corresp_ex_def)
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
@@ -209,10 +205,10 @@
(* Lemma 2.1 *)
(* -------------------------------------------------- *)
-lemma lemma_2_1 [rule_format (no_asm)]:
-"Finite xs -->
- (!s .is_exec_frag A (s,xs) & is_exec_frag A (t,ys) &
- t = laststate (s,xs)
+lemma lemma_2_1 [rule_format (no_asm)]:
+"Finite xs -->
+ (!s .is_exec_frag A (s,xs) & is_exec_frag A (t,ys) &
+ t = laststate (s,xs)
--> is_exec_frag A (s,xs @@ ys))"
apply (rule impI)
@@ -229,9 +225,9 @@
-lemma lemma_2:
- "[| is_ref_map f C A |] ==>
- !s. reachable C s & is_exec_frag C (s,xs)
+lemma lemma_2:
+ "[| is_ref_map f C A |] ==>
+ !s. reachable C s & is_exec_frag C (s,xs)
--> is_exec_frag A (corresp_ex A f (s,xs))"
apply (unfold corresp_ex_def)
@@ -267,8 +263,8 @@
subsection "Main Theorem: TRACE - INCLUSION"
-lemma trace_inclusion:
- "[| ext C = ext A; is_ref_map f C A |]
+lemma trace_inclusion:
+ "[| ext C = ext A; is_ref_map f C A |]
==> traces C <= traces A"
apply (unfold traces_def)
@@ -305,14 +301,14 @@
done
-lemma WF_alt: "is_wfair A W (s,ex) =
+lemma WF_alt: "is_wfair A W (s,ex) =
(fin_often (%x. ~Enabled A W (snd x)) ex --> inf_often (%x. fst x :W) ex)"
apply (simp add: is_wfair_def fin_often_def)
apply auto
done
-lemma WF_persistent: "[|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex;
- en_persistent A W|]
+lemma WF_persistent: "[|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex;
+ en_persistent A W|]
==> inf_often (%x. fst x :W) ex"
apply (drule persistent)
apply assumption
@@ -321,9 +317,9 @@
done
-lemma fair_trace_inclusion: "!! C A.
- [| is_ref_map f C A; ext C = ext A;
- !! ex. [| ex:executions C; fair_ex C ex|] ==> fair_ex A (corresp_ex A f ex) |]
+lemma fair_trace_inclusion: "!! C A.
+ [| is_ref_map f C A; ext C = ext A;
+ !! ex. [| ex:executions C; fair_ex C ex|] ==> fair_ex A (corresp_ex A f ex) |]
==> fairtraces C <= fairtraces A"
apply (simp (no_asm) add: fairtraces_def fairexecutions_def)
apply (tactic "safe_tac set_cs")
@@ -350,9 +346,9 @@
apply auto
done
-lemma fair_trace_inclusion2: "!! C A.
- [| inp(C) = inp(A); out(C)=out(A);
- is_fair_ref_map f C A |]
+lemma fair_trace_inclusion2: "!! C A.
+ [| inp(C) = inp(A); out(C)=out(A);
+ is_fair_ref_map f C A |]
==> fair_implements C A"
apply (simp add: is_fair_ref_map_def fair_implements_def fairtraces_def fairexecutions_def)
apply (tactic "safe_tac set_cs")
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Sun Oct 21 16:27:42 2007 +0200
@@ -11,35 +11,30 @@
defaultsort type
-consts
- move ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool"
- is_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
- is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool"
-
-
-defs
-
-move_def:
- "move ioa ex s a t ==
+definition
+ move :: "[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" where
+ "move ioa ex s a t =
(is_exec_frag ioa (s,ex) & Finite ex &
laststate (s,ex)=t &
mk_trace ioa$ex = (if a:ext(ioa) then a>>nil else nil))"
-is_ref_map_def:
- "is_ref_map f C A ==
- (!s:starts_of(C). f(s):starts_of(A)) &
+definition
+ is_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where
+ "is_ref_map f C A =
+ ((!s:starts_of(C). f(s):starts_of(A)) &
(!s t a. reachable C s &
s -a--C-> t
- --> (? ex. move A ex (f s) a (f t)))"
+ --> (? ex. move A ex (f s) a (f t))))"
-is_weak_ref_map_def:
- "is_weak_ref_map f C A ==
- (!s:starts_of(C). f(s):starts_of(A)) &
+definition
+ is_weak_ref_map :: "[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" where
+ "is_weak_ref_map f C A =
+ ((!s:starts_of(C). f(s):starts_of(A)) &
(!s t a. reachable C s &
s -a--C-> t
--> (if a:ext(C)
then (f s) -a--A-> (f t)
- else (f s)=(f t)))"
+ else (f s)=(f t))))"
subsection "transitions and moves"
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Sun Oct 21 16:27:42 2007 +0200
@@ -14,28 +14,9 @@
that has the same trace as ex, but its schedule ends with an external action.
*}
-consts
-
-(* LastActExtex ::"('a,'s)ioa => ('a,'s) pairs => bool"*)
- LastActExtsch ::"('a,'s)ioa => 'a Seq => bool"
-
- Cut ::"('a => bool) => 'a Seq => 'a Seq"
-
- oraclebuild ::"('a => bool) => 'a Seq -> 'a Seq -> 'a Seq"
-
-defs
-
-LastActExtsch_def:
- "LastActExtsch A sch == (Cut (%x. x: ext A) sch = sch)"
-
-(* LastActExtex_def:
- "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *)
-
-Cut_def:
- "Cut P s == oraclebuild P$s$(Filter P$s)"
-
-oraclebuild_def:
- "oraclebuild P == (fix$(LAM h s t. case t of
+definition
+ oraclebuild :: "('a => bool) => 'a Seq -> 'a Seq -> 'a Seq" where
+ "oraclebuild P = (fix$(LAM h s t. case t of
nil => nil
| x##xs =>
(case x of
@@ -45,18 +26,26 @@
)
))"
-
-axioms
+definition
+ Cut :: "('a => bool) => 'a Seq => 'a Seq" where
+ "Cut P s = oraclebuild P$s$(Filter P$s)"
-Cut_prefixcl_Finite:
- "Finite s ==> (? y. s = Cut P s @@ y)"
+definition
+ LastActExtsch :: "('a,'s)ioa => 'a Seq => bool" where
+ "LastActExtsch A sch = (Cut (%x. x: ext A) sch = sch)"
-LastActExtsmall1:
- "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))"
+(* LastActExtex ::"('a,'s)ioa => ('a,'s) pairs => bool"*)
+(* LastActExtex_def:
+ "LastActExtex A ex == LastActExtsch A (filter_act$ex)" *)
-LastActExtsmall2:
- "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
+axiomatization where
+ Cut_prefixcl_Finite: "Finite s ==> (? y. s = Cut P s @@ y)"
+axiomatization where
+ LastActExtsmall1: "LastActExtsch A sch ==> LastActExtsch A (TL$(Dropwhile P$sch))"
+
+axiomatization where
+ LastActExtsmall2: "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
ML {*
@@ -71,9 +60,9 @@
lemma oraclebuild_unfold:
-"oraclebuild P = (LAM s t. case t of
+"oraclebuild P = (LAM s t. case t of
nil => nil
- | x##xs =>
+ | x##xs =>
(case x of
UU => UU
| Def y => (Takewhile (%a.~ P a)$s)
@@ -82,7 +71,7 @@
)"
apply (rule trans)
apply (rule fix_eq2)
-apply (rule oraclebuild_def)
+apply (simp only: oraclebuild_def)
apply (rule beta_cfun)
apply simp
done
@@ -97,8 +86,8 @@
apply simp
done
-lemma oraclebuild_cons: "oraclebuild P$s$(x>>t) =
- (Takewhile (%a.~ P a)$s)
+lemma oraclebuild_cons: "oraclebuild P$s$(x>>t) =
+ (Takewhile (%a.~ P a)$s)
@@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))"
apply (rule trans)
apply (subst oraclebuild_unfold)
@@ -109,8 +98,8 @@
subsection "Cut rewrite rules"
-lemma Cut_nil:
-"[| Forall (%a.~ P a) s; Finite s|]
+lemma Cut_nil:
+"[| Forall (%a.~ P a) s; Finite s|]
==> Cut P s =nil"
apply (unfold Cut_def)
apply (subgoal_tac "Filter P$s = nil")
@@ -119,8 +108,8 @@
apply assumption+
done
-lemma Cut_UU:
-"[| Forall (%a.~ P a) s; ~Finite s|]
+lemma Cut_UU:
+"[| Forall (%a.~ P a) s; ~Finite s|]
==> Cut P s =UU"
apply (unfold Cut_def)
apply (subgoal_tac "Filter P$s= UU")
@@ -129,9 +118,9 @@
apply assumption+
done
-lemma Cut_Cons:
-"[| P t; Forall (%x.~ P x) ss; Finite ss|]
- ==> Cut P (ss @@ (t>> rs))
+lemma Cut_Cons:
+"[| P t; Forall (%x.~ P x) ss; Finite ss|]
+ ==> Cut P (ss @@ (t>> rs))
= ss @@ (t >> Cut P rs)"
apply (unfold Cut_def)
apply (simp add: ForallQFilterPnil oraclebuild_cons TakewhileConc DropwhileConc)
@@ -227,10 +216,10 @@
subsection "Main Cut Theorem"
-lemma exists_LastActExtsch:
- "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|]
- ==> ? sch. sch : schedules A &
- tr = Filter (%a. a:ext A)$sch &
+lemma exists_LastActExtsch:
+ "[|sch : schedules A ; tr = Filter (%a. a:ext A)$sch|]
+ ==> ? sch. sch : schedules A &
+ tr = Filter (%a. a:ext A)$sch &
LastActExtsch A sch"
apply (unfold schedules_def has_schedule_def)
@@ -265,8 +254,8 @@
subsection "Further Cut lemmas"
-lemma LastActExtimplnil:
- "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |]
+lemma LastActExtimplnil:
+ "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = nil |]
==> sch=nil"
apply (unfold LastActExtsch_def)
apply (drule FilternPnilForallP)
@@ -276,8 +265,8 @@
apply simp
done
-lemma LastActExtimplUU:
- "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |]
+lemma LastActExtimplUU:
+ "[| LastActExtsch A sch; Filter (%x. x:ext A)$sch = UU |]
==> sch=UU"
apply (unfold LastActExtsch_def)
apply (drule FilternPUUForallP)
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Sun Oct 21 16:27:42 2007 +0200
@@ -9,25 +9,11 @@
imports Simulations
begin
-consts
-
- corresp_ex_sim ::"('a,'s2)ioa => (('s1 *'s2)set) =>
- ('a,'s1)execution => ('a,'s2)execution"
+definition
(* Note: s2 instead of s1 in last argument type !! *)
- corresp_ex_simC ::"('a,'s2)ioa => (('s1 * 's2)set) => ('a,'s1)pairs
- -> ('s2 => ('a,'s2)pairs)"
-
-
-defs
-
-corresp_ex_sim_def:
- "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A)
- in
- (S',(corresp_ex_simC A R$(snd ex)) S')"
-
-
-corresp_ex_simC_def:
- "corresp_ex_simC A R == (fix$(LAM h ex. (%s. case ex of
+ corresp_ex_simC :: "('a,'s2)ioa => (('s1 * 's2)set) => ('a,'s1)pairs
+ -> ('s2 => ('a,'s2)pairs)" where
+ "corresp_ex_simC A R = (fix$(LAM h ex. (%s. case ex of
nil => nil
| x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr);
T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
@@ -36,20 +22,27 @@
@@ ((h$xs) T'))
$x) )))"
+definition
+ corresp_ex_sim :: "('a,'s2)ioa => (('s1 *'s2)set) =>
+ ('a,'s1)execution => ('a,'s2)execution" where
+ "corresp_ex_sim A R ex == let S'= (@s'.(fst ex,s'):R & s': starts_of A)
+ in
+ (S',(corresp_ex_simC A R$(snd ex)) S')"
+
subsection "corresp_ex_sim"
-lemma corresp_ex_simC_unfold: "corresp_ex_simC A R = (LAM ex. (%s. case ex of
- nil => nil
- | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr);
- T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
- in
- (@cex. move A cex s a T')
- @@ ((corresp_ex_simC A R $xs) T'))
+lemma corresp_ex_simC_unfold: "corresp_ex_simC A R = (LAM ex. (%s. case ex of
+ nil => nil
+ | x##xs => (flift1 (%pr. let a = (fst pr); t = (snd pr);
+ T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
+ in
+ (@cex. move A cex s a T')
+ @@ ((corresp_ex_simC A R $xs) T'))
$x) ))"
apply (rule trans)
apply (rule fix_eq2)
-apply (rule corresp_ex_simC_def)
+apply (simp only: corresp_ex_simC_def)
apply (rule beta_cfun)
apply (simp add: flift1_def)
done
@@ -64,10 +57,10 @@
apply simp
done
-lemma corresp_ex_simC_cons: "(corresp_ex_simC A R$((a,t)>>xs)) s =
- (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
- in
- (@cex. move A cex s a T')
+lemma corresp_ex_simC_cons: "(corresp_ex_simC A R$((a,t)>>xs)) s =
+ (let T' = @t'. ? ex1. (t,t'):R & move A ex1 s a t'
+ in
+ (@cex. move A cex s a T')
@@ ((corresp_ex_simC A R$xs) T'))"
apply (rule trans)
apply (subst corresp_ex_simC_unfold)
@@ -83,9 +76,9 @@
declare Let_def [simp del]
-lemma move_is_move_sim:
- "[|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>
- let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
+lemma move_is_move_sim:
+ "[|is_simulation R C A; reachable C s; s -a--C-> t; (s,s'):R|] ==>
+ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
(t,T'): R & move A (@ex2. move A ex2 s' a T') s' a T'"
apply (unfold is_simulation_def)
@@ -113,9 +106,9 @@
declare Let_def [simp]
-lemma move_subprop1_sim:
- "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
- let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
+lemma move_subprop1_sim:
+ "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
+ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
is_exec_frag A (s',@x. move A x s' a T')"
apply (cut_tac move_is_move_sim)
defer
@@ -123,9 +116,9 @@
apply (simp add: move_def)
done
-lemma move_subprop2_sim:
- "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
- let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
+lemma move_subprop2_sim:
+ "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
+ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
Finite (@x. move A x s' a T')"
apply (cut_tac move_is_move_sim)
defer
@@ -133,9 +126,9 @@
apply (simp add: move_def)
done
-lemma move_subprop3_sim:
- "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
- let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
+lemma move_subprop3_sim:
+ "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
+ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
laststate (s',@x. move A x s' a T') = T'"
apply (cut_tac move_is_move_sim)
defer
@@ -143,10 +136,10 @@
apply (simp add: move_def)
done
-lemma move_subprop4_sim:
- "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
- let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
- mk_trace A$((@x. move A x s' a T')) =
+lemma move_subprop4_sim:
+ "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
+ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
+ mk_trace A$((@x. move A x s' a T')) =
(if a:ext A then a>>nil else nil)"
apply (cut_tac move_is_move_sim)
defer
@@ -154,9 +147,9 @@
apply (simp add: move_def)
done
-lemma move_subprop5_sim:
- "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
- let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
+lemma move_subprop5_sim:
+ "[|is_simulation R C A; reachable C s; s-a--C-> t; (s,s'):R|] ==>
+ let T' = @t'. ? ex1. (t,t'):R & move A ex1 s' a t' in
(t,T'):R"
apply (cut_tac move_is_move_sim)
defer
@@ -174,9 +167,9 @@
------------------------------------------------------- *)
declare split_if [split del]
-lemma traces_coincide_sim [rule_format (no_asm)]:
- "[|is_simulation R C A; ext C = ext A|] ==>
- !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R -->
+lemma traces_coincide_sim [rule_format (no_asm)]:
+ "[|is_simulation R C A; ext C = ext A|] ==>
+ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R -->
mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')"
apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *})
@@ -200,9 +193,9 @@
(* ----------------------------------------------------------- *)
-lemma correspsim_is_execution [rule_format (no_asm)]:
- "[| is_simulation R C A |] ==>
- !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R
+lemma correspsim_is_execution [rule_format (no_asm)]:
+ "[| is_simulation R C A |] ==>
+ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R
--> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')"
apply (tactic {* pair_induct_tac "ex" [thm "is_exec_frag_def"] 1 *})
@@ -244,9 +237,9 @@
traces_coincide_sim, the second for the start state case.
S':= @s'. (s,s'):R & s':starts_of A, where s:starts_of C *)
-lemma simulation_starts:
-"[| is_simulation R C A; s:starts_of C |]
- ==> let S' = @s'. (s,s'):R & s':starts_of A in
+lemma simulation_starts:
+"[| is_simulation R C A; s:starts_of C |]
+ ==> let S' = @s'. (s,s'):R & s':starts_of A in
(s,S'):R & S':starts_of A"
apply (simp add: is_simulation_def corresp_ex_sim_def Int_non_empty Image_def)
apply (erule conjE)+
@@ -262,8 +255,8 @@
lemmas sim_starts2 = simulation_starts [unfolded Let_def, THEN conjunct2, standard]
-lemma trace_inclusion_for_simulations:
- "[| ext C = ext A; is_simulation R C A |]
+lemma trace_inclusion_for_simulations:
+ "[| ext C = ext A; is_simulation R C A |]
==> traces C <= traces A"
apply (unfold traces_def)
--- a/src/HOLCF/IOA/meta_theory/Simulations.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/IOA/meta_theory/Simulations.thy Sun Oct 21 16:27:42 2007 +0200
@@ -11,56 +11,51 @@
defaultsort type
-consts
-
- is_simulation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
- is_backward_simulation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
- is_forw_back_simulation ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
- is_back_forw_simulation ::"[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
- is_history_relation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
- is_prophecy_relation ::"[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool"
-
-defs
-
-is_simulation_def:
- "is_simulation R C A ==
- (!s:starts_of C. R``{s} Int starts_of A ~= {}) &
+definition
+ is_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
+ "is_simulation R C A =
+ ((!s:starts_of C. R``{s} Int starts_of A ~= {}) &
(!s s' t a. reachable C s &
s -a--C-> t &
(s,s') : R
- --> (? t' ex. (t,t'):R & move A ex s' a t'))"
+ --> (? t' ex. (t,t'):R & move A ex s' a t')))"
-is_backward_simulation_def:
- "is_backward_simulation R C A ==
- (!s:starts_of C. R``{s} <= starts_of A) &
+definition
+ is_backward_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
+ "is_backward_simulation R C A =
+ ((!s:starts_of C. R``{s} <= starts_of A) &
(!s t t' a. reachable C s &
s -a--C-> t &
(t,t') : R
- --> (? ex s'. (s,s'):R & move A ex s' a t'))"
+ --> (? ex s'. (s,s'):R & move A ex s' a t')))"
-is_forw_back_simulation_def:
- "is_forw_back_simulation R C A ==
- (!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) &
+definition
+ is_forw_back_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
+ "is_forw_back_simulation R C A =
+ ((!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) &
(!s S' t a. reachable C s &
s -a--C-> t &
(s,S') : R
- --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t')))"
+ --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t'))))"
-is_back_forw_simulation_def:
- "is_back_forw_simulation R C A ==
- (!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) &
+definition
+ is_back_forw_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
+ "is_back_forw_simulation R C A =
+ ((!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) &
(!s t T' a. reachable C s &
s -a--C-> t &
(t,T') : R
- --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t')))"
+ --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t'))))"
-is_history_relation_def:
- "is_history_relation R C A == is_simulation R C A &
- is_ref_map (%x.(@y. (x,y):(R^-1))) A C"
+definition
+ is_history_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
+ "is_history_relation R C A = (is_simulation R C A &
+ is_ref_map (%x.(@y. (x,y):(R^-1))) A C)"
-is_prophecy_relation_def:
- "is_prophecy_relation R C A == is_backward_simulation R C A &
- is_ref_map (%x.(@y. (x,y):(R^-1))) A C"
+definition
+ is_prophecy_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where
+ "is_prophecy_relation R C A = (is_backward_simulation R C A &
+ is_ref_map (%x.(@y. (x,y):(R^-1))) A C)"
lemma set_non_empty: "(A~={}) = (? x. x:A)"
@@ -72,7 +67,7 @@
done
-lemma Sim_start_convert:
+lemma Sim_start_convert:
"(R``{x} Int S ~= {}) = (? y. (x,y):R & y:S)"
apply (unfold Image_def)
apply (simp add: Int_non_empty)
@@ -81,7 +76,7 @@
declare Sim_start_convert [simp]
-lemma ref_map_is_simulation:
+lemma ref_map_is_simulation:
"!! f. is_ref_map f C A ==> is_simulation {p. (snd p) = f (fst p)} C A"
apply (unfold is_ref_map_def is_simulation_def)
--- a/src/HOLCF/Sprod.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/Sprod.thy Sun Oct 21 16:27:42 2007 +0200
@@ -30,22 +30,25 @@
subsection {* Definitions of constants *}
-consts
- sfst :: "('a ** 'b) \<rightarrow> 'a"
- ssnd :: "('a ** 'b) \<rightarrow> 'b"
- spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)"
- ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c"
+definition
+ sfst :: "('a ** 'b) \<rightarrow> 'a" where
+ "sfst = (\<Lambda> p. cfst\<cdot>(Rep_Sprod p))"
+
+definition
+ ssnd :: "('a ** 'b) \<rightarrow> 'b" where
+ "ssnd = (\<Lambda> p. csnd\<cdot>(Rep_Sprod p))"
-defs
- sfst_def: "sfst \<equiv> \<Lambda> p. cfst\<cdot>(Rep_Sprod p)"
- ssnd_def: "ssnd \<equiv> \<Lambda> p. csnd\<cdot>(Rep_Sprod p)"
- spair_def: "spair \<equiv> \<Lambda> a b. Abs_Sprod
- <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
- ssplit_def: "ssplit \<equiv> \<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p))"
+definition
+ spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" where
+ "spair = (\<Lambda> a b. Abs_Sprod
+ <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>)"
-syntax
+definition
+ ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where
+ "ssplit = (\<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
+
+syntax
"@stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))")
-
translations
"(:x, y, z:)" == "(:x, (:y, z:):)"
"(:x, y:)" == "CONST spair\<cdot>x\<cdot>y"
@@ -53,6 +56,7 @@
translations
"\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)"
+
subsection {* Case analysis *}
lemma spair_Abs_Sprod:
@@ -92,7 +96,7 @@
lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>"
by (erule contrapos_np, auto)
-lemma spair_defined [simp]:
+lemma spair_defined [simp]:
"\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>"
by (simp add: spair_Abs_Sprod Abs_Sprod_defined Sprod_def)
--- a/src/HOLCF/Tr.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/Tr.thy Sun Oct 21 16:27:42 2007 +0200
@@ -17,47 +17,55 @@
tr = "bool lift"
translations
- "tr" <= (type) "bool lift"
+ "tr" <= (type) "bool lift"
+
+definition
+ TT :: "tr" where
+ "TT = Def True"
-consts
- TT :: "tr"
- FF :: "tr"
- trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c"
- trand :: "tr \<rightarrow> tr \<rightarrow> tr"
- tror :: "tr \<rightarrow> tr \<rightarrow> tr"
- neg :: "tr \<rightarrow> tr"
- If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c"
+definition
+ FF :: "tr" where
+ "FF = Def False"
+definition
+ trifte :: "'c \<rightarrow> 'c \<rightarrow> tr \<rightarrow> 'c" where
+ ifte_def: "trifte = (\<Lambda> t e. FLIFT b. if b then t else e)"
abbreviation
cifte_syn :: "[tr, 'c, 'c] \<Rightarrow> 'c" ("(3If _/ (then _/ else _) fi)" 60) where
"If b then e1 else e2 fi == trifte\<cdot>e1\<cdot>e2\<cdot>b"
+definition
+ trand :: "tr \<rightarrow> tr \<rightarrow> tr" where
+ andalso_def: "trand = (\<Lambda> x y. If x then y else FF fi)"
abbreviation
andalso_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ andalso _" [36,35] 35) where
"x andalso y == trand\<cdot>x\<cdot>y"
+definition
+ tror :: "tr \<rightarrow> tr \<rightarrow> tr" where
+ orelse_def: "tror = (\<Lambda> x y. If x then TT else y fi)"
abbreviation
orelse_syn :: "tr \<Rightarrow> tr \<Rightarrow> tr" ("_ orelse _" [31,30] 30) where
"x orelse y == tror\<cdot>x\<cdot>y"
-
-translations
- "\<Lambda> TT. t" == "trifte\<cdot>t\<cdot>\<bottom>"
- "\<Lambda> FF. t" == "trifte\<cdot>\<bottom>\<cdot>t"
+
+definition
+ neg :: "tr \<rightarrow> tr" where
+ "neg = flift2 Not"
-defs
- TT_def: "TT \<equiv> Def True"
- FF_def: "FF \<equiv> Def False"
- neg_def: "neg \<equiv> flift2 Not"
- ifte_def: "trifte \<equiv> \<Lambda> t e. FLIFT b. if b then t else e"
- andalso_def: "trand \<equiv> \<Lambda> x y. If x then y else FF fi"
- orelse_def: "tror \<equiv> \<Lambda> x y. If x then TT else y fi"
- If2_def: "If2 Q x y \<equiv> If Q then x else y fi"
+definition
+ If2 :: "[tr, 'c, 'c] \<Rightarrow> 'c" where
+ "If2 Q x y = (If Q then x else y fi)"
+
+translations
+ "\<Lambda> (CONST TT). t" == "CONST trifte\<cdot>t\<cdot>\<bottom>"
+ "\<Lambda> (CONST FF). t" == "CONST trifte\<cdot>\<bottom>\<cdot>t"
+
text {* Exhaustion and Elimination for type @{typ tr} *}
lemma Exh_tr: "t = \<bottom> \<or> t = TT \<or> t = FF"
apply (unfold FF_def TT_def)
-apply (induct_tac "t")
+apply (induct t)
apply fast
apply fast
done
@@ -78,7 +86,7 @@
(fn prems =>
[
(res_inst_tac [("p","y")] trE 1),
- (REPEAT(asm_simp_tac (simpset() addsimps
+ (REPEAT(asm_simp_tac (simpset() addsimps
[o_def,flift1_def,flift2_def,inst_lift_po]@tr_defs) 1))
])
*)
@@ -129,8 +137,8 @@
by (simp_all add: neg_def TT_def FF_def)
text {* split-tac for If via If2 because the constant has to be a constant *}
-
-lemma split_If2:
+
+lemma split_If2:
"P (If2 Q x y) = ((Q = \<bottom> \<longrightarrow> P \<bottom>) \<and> (Q = TT \<longrightarrow> P x) \<and> (Q = FF \<longrightarrow> P y))"
apply (unfold If2_def)
apply (rule_tac p = "Q" in trE)
@@ -139,13 +147,13 @@
ML {*
val split_If_tac =
- simp_tac (HOL_basic_ss addsimps [symmetric (thm "If2_def")])
- THEN' (split_tac [thm "split_If2"])
+ simp_tac (HOL_basic_ss addsimps [@{thm If2_def} RS sym])
+ THEN' (split_tac [@{thm split_If2}])
*}
subsection "Rewriting of HOLCF operations to HOL functions"
-lemma andalso_or:
+lemma andalso_or:
"t \<noteq> \<bottom> \<Longrightarrow> ((t andalso s) = FF) = (t = FF \<or> s = FF)"
apply (rule_tac p = "t" in trE)
apply simp_all
@@ -169,7 +177,7 @@
lemma Def_bool4 [simp]: "(Def x \<noteq> TT) = (\<not> x)"
by (simp add: TT_def)
-lemma If_and_if:
+lemma If_and_if:
"(If Def P then A else B fi) = (if P then A else B)"
apply (rule_tac p = "Def P" in trE)
apply (auto simp add: TT_def[symmetric] FF_def[symmetric])
--- a/src/HOLCF/ex/Dagstuhl.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/ex/Dagstuhl.thy Sun Oct 21 16:27:42 2007 +0200
@@ -4,7 +4,7 @@
imports Stream
begin
-consts
+axiomatization
y :: "'a"
definition
--- a/src/HOLCF/ex/Fix2.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/ex/Fix2.thy Sun Oct 21 16:27:42 2007 +0200
@@ -10,11 +10,9 @@
imports HOLCF
begin
-consts
- gix :: "('a->'a)->'a"
-
-axioms
- gix1_def: "F$(gix$F) = gix$F"
+axiomatization
+ gix :: "('a->'a)->'a" where
+ gix1_def: "F$(gix$F) = gix$F" and
gix2_def: "F$y=y ==> gix$F << y"
--- a/src/HOLCF/ex/Focus_ex.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/ex/Focus_ex.thy Sun Oct 21 16:27:42 2007 +0200
@@ -107,7 +107,7 @@
typedecl ('a, 'b) tc
arities tc:: (pcpo, pcpo) pcpo
-consts
+axiomatization
Rf :: "('b stream * ('b,'c) tc stream * 'c stream * ('b,'c) tc stream) => bool"
definition
--- a/src/HOLCF/ex/Hoare.thy Sun Oct 21 14:53:44 2007 +0200
+++ b/src/HOLCF/ex/Hoare.thy Sun Oct 21 16:27:42 2007 +0200
@@ -24,9 +24,9 @@
imports HOLCF
begin
-consts
- b1 :: "'a -> tr"
- b2 :: "'a -> tr"
+axiomatization
+ b1 :: "'a -> tr" and
+ b2 :: "'a -> tr" and
g :: "'a -> 'a"
definition