--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Wed Dec 30 22:09:44 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Thu Dec 31 00:07:42 2015 +0100
@@ -10,76 +10,53 @@
default_sort type
-type_synonym
- ('a, 's) transition = "'s * 'a * 's"
-
-type_synonym
- ('a, 's) ioa = "'a signature * 's set * ('a,'s)transition set * ('a set set) * ('a set set)"
-
-consts
-
- (* IO automata *)
-
- asig_of ::"('a,'s)ioa => 'a signature"
- starts_of ::"('a,'s)ioa => 's set"
- trans_of ::"('a,'s)ioa => ('a,'s)transition set"
- wfair_of ::"('a,'s)ioa => ('a set) set"
- sfair_of ::"('a,'s)ioa => ('a set) set"
-
- is_asig_of ::"('a,'s)ioa => bool"
- is_starts_of ::"('a,'s)ioa => bool"
- is_trans_of ::"('a,'s)ioa => bool"
- input_enabled ::"('a,'s)ioa => bool"
- IOA ::"('a,'s)ioa => bool"
-
- (* constraints for fair IOA *)
-
- fairIOA ::"('a,'s)ioa => bool"
- input_resistant::"('a,'s)ioa => bool"
-
- (* enabledness of actions and action sets *)
-
- enabled ::"('a,'s)ioa => 'a => 's => bool"
- Enabled ::"('a,'s)ioa => 'a set => 's => bool"
-
- (* action set keeps enabled until probably disabled by itself *)
-
- en_persistent :: "('a,'s)ioa => 'a set => bool"
-
- (* post_conditions for actions and action sets *)
-
- was_enabled ::"('a,'s)ioa => 'a => 's => bool"
- set_was_enabled ::"('a,'s)ioa => 'a set => 's => bool"
-
- (* invariants *)
- invariant :: "[('a,'s)ioa, 's=>bool] => bool"
-
- (* binary composition of action signatures and automata *)
- asig_comp ::"['a signature, 'a signature] => 'a signature"
- compatible ::"[('a,'s)ioa, ('a,'t)ioa] => bool"
- par ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "\<parallel>" 10)
-
- (* hiding and restricting *)
- hide_asig :: "['a signature, 'a set] => 'a signature"
- hide :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
- restrict_asig :: "['a signature, 'a set] => 'a signature"
- restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
-
- (* renaming *)
- rename_set :: "'a set => ('c => 'a option) => 'c set"
- rename :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
+type_synonym ('a, 's) transition = "'s * 'a * 's"
+type_synonym ('a, 's) ioa =
+ "'a signature * 's set * ('a,'s)transition set * ('a set set) * ('a set set)"
-inductive
- reachable :: "('a, 's) ioa => 's => bool"
- for C :: "('a, 's) ioa"
- where
- reachable_0: "s : starts_of C ==> reachable C s"
- | reachable_n: "[| reachable C s; (s, a, t) : trans_of C |] ==> reachable C t"
+(* --------------------------------- IOA ---------------------------------*)
+
+(* IO automata *)
+
+definition asig_of :: "('a, 's)ioa \<Rightarrow> 'a signature"
+ where "asig_of = fst"
+
+definition starts_of :: "('a, 's) ioa \<Rightarrow> 's set"
+ where "starts_of = (fst \<circ> snd)"
+
+definition trans_of :: "('a, 's) ioa \<Rightarrow> ('a, 's) transition set"
+ where "trans_of = (fst \<circ> snd \<circ> snd)"
+
+abbreviation trans_of_syn ("_ \<midarrow>_\<midarrow>_\<rightarrow> _" [81, 81, 81, 81] 100)
+ where "s \<midarrow>a\<midarrow>A\<rightarrow> t \<equiv> (s, a, t) \<in> trans_of A"
+
+definition wfair_of :: "('a, 's) ioa \<Rightarrow> 'a set set"
+ where "wfair_of = (fst \<circ> snd \<circ> snd \<circ> snd)"
-abbreviation
- trans_of_syn ("_ \<midarrow>_\<midarrow>_\<rightarrow> _" [81,81,81,81] 100) where
- "s \<midarrow>a\<midarrow>A\<rightarrow> t == (s,a,t):trans_of A"
+definition sfair_of :: "('a, 's) ioa \<Rightarrow> 'a set set"
+ where "sfair_of = (snd \<circ> snd \<circ> snd \<circ> snd)"
+
+definition is_asig_of :: "('a, 's) ioa \<Rightarrow> bool"
+ where "is_asig_of A = is_asig (asig_of A)"
+
+definition is_starts_of :: "('a, 's) ioa \<Rightarrow> bool"
+ where "is_starts_of A \<longleftrightarrow> starts_of A \<noteq> {}"
+
+definition is_trans_of :: "('a, 's) ioa \<Rightarrow> bool"
+ where "is_trans_of A \<longleftrightarrow>
+ (\<forall>triple. triple \<in> trans_of A \<longrightarrow> fst (snd triple) \<in> actions (asig_of A))"
+
+definition input_enabled :: "('a, 's) ioa \<Rightarrow> bool"
+ where "input_enabled A \<longleftrightarrow>
+ (\<forall>a. a \<in> inputs (asig_of A) \<longrightarrow> (\<forall>s1. \<exists>s2. (s1, a, s2) \<in> trans_of A))"
+
+definition IOA :: "('a, 's) ioa \<Rightarrow> bool"
+ where "IOA A \<longleftrightarrow>
+ is_asig_of A \<and>
+ is_starts_of A \<and>
+ is_trans_of A \<and>
+ input_enabled A"
abbreviation "act A == actions (asig_of A)"
abbreviation "ext A == externals (asig_of A)"
@@ -88,77 +65,60 @@
abbreviation "out A == outputs (asig_of A)"
abbreviation "local A == locals (asig_of A)"
-defs
-
-(* --------------------------------- IOA ---------------------------------*)
-
-asig_of_def: "asig_of == fst"
-starts_of_def: "starts_of == (fst o snd)"
-trans_of_def: "trans_of == (fst o snd o snd)"
-wfair_of_def: "wfair_of == (fst o snd o snd o snd)"
-sfair_of_def: "sfair_of == (snd o snd o snd o snd)"
-
-is_asig_of_def:
- "is_asig_of A == is_asig (asig_of A)"
-
-is_starts_of_def:
- "is_starts_of A == (~ starts_of A = {})"
+(* invariants *)
+inductive reachable :: "('a, 's) ioa \<Rightarrow> 's \<Rightarrow> bool"
+ for C :: "('a, 's) ioa"
+where
+ reachable_0: "s \<in> starts_of C \<Longrightarrow> reachable C s"
+| reachable_n: "\<lbrakk>reachable C s; (s, a, t) \<in> trans_of C\<rbrakk> \<Longrightarrow> reachable C t"
-is_trans_of_def:
- "is_trans_of A ==
- (!triple. triple:(trans_of A) --> fst(snd(triple)):actions(asig_of A))"
-
-input_enabled_def:
- "input_enabled A ==
- (!a. (a:inputs(asig_of A)) --> (!s1. ? s2. (s1,a,s2):(trans_of A)))"
-
-
-ioa_def:
- "IOA A == (is_asig_of A &
- is_starts_of A &
- is_trans_of A &
- input_enabled A)"
-
-
-invariant_def: "invariant A P == (!s. reachable A s --> P(s))"
+definition invariant :: "[('a, 's) ioa, 's \<Rightarrow> bool] \<Rightarrow> bool"
+ where "invariant A P \<longleftrightarrow> (\<forall>s. reachable A s \<longrightarrow> P s)"
(* ------------------------- parallel composition --------------------------*)
+(* binary composition of action signatures and automata *)
-compatible_def:
- "compatible A B ==
- (((out A Int out B) = {}) &
- ((int A Int act B) = {}) &
- ((int B Int act A) = {}))"
+definition compatible :: "[('a, 's) ioa, ('a, 't) ioa] \<Rightarrow> bool"
+where
+ "compatible A B \<longleftrightarrow>
+ (((out A \<inter> out B) = {}) \<and>
+ ((int A \<inter> act B) = {}) \<and>
+ ((int B \<inter> act A) = {}))"
-asig_comp_def:
- "asig_comp a1 a2 ==
- (((inputs(a1) Un inputs(a2)) - (outputs(a1) Un outputs(a2)),
- (outputs(a1) Un outputs(a2)),
- (internals(a1) Un internals(a2))))"
+definition asig_comp :: "['a signature, 'a signature] \<Rightarrow> 'a signature"
+where
+ "asig_comp a1 a2 =
+ (((inputs(a1) \<union> inputs(a2)) - (outputs(a1) \<union> outputs(a2)),
+ (outputs(a1) \<union> outputs(a2)),
+ (internals(a1) \<union> internals(a2))))"
-par_def:
- "(A \<parallel> B) ==
+definition par :: "[('a, 's) ioa, ('a, 't) ioa] \<Rightarrow> ('a, 's * 't) ioa" (infixr "\<parallel>" 10)
+where
+ "(A \<parallel> B) =
(asig_comp (asig_of A) (asig_of B),
- {pr. fst(pr):starts_of(A) & snd(pr):starts_of(B)},
+ {pr. fst(pr) \<in> starts_of(A) \<and> snd(pr) \<in> starts_of(B)},
{tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
- in (a:act A | a:act B) &
- (if a:act A then
- (fst(s),a,fst(t)):trans_of(A)
+ in (a \<in> act A | a:act B) \<and>
+ (if a \<in> act A then
+ (fst(s), a, fst(t)) \<in> trans_of(A)
else fst(t) = fst(s))
&
- (if a:act B then
- (snd(s),a,snd(t)):trans_of(B)
+ (if a \<in> act B then
+ (snd(s), a, snd(t)) \<in> trans_of(B)
else snd(t) = snd(s))},
- wfair_of A Un wfair_of B,
- sfair_of A Un sfair_of B)"
+ wfair_of A \<union> wfair_of B,
+ sfair_of A \<union> sfair_of B)"
(* ------------------------ hiding -------------------------------------------- *)
-restrict_asig_def:
- "restrict_asig asig actns ==
+(* hiding and restricting *)
+
+definition restrict_asig :: "['a signature, 'a set] \<Rightarrow> 'a signature"
+where
+ "restrict_asig asig actns =
(inputs(asig) Int actns,
outputs(asig) Int actns,
internals(asig) Un (externals(asig) - actns))"
@@ -166,23 +126,25 @@
(* Notice that for wfair_of and sfair_of nothing has to be changed, as
changes from the outputs to the internals does not touch the locals as
a whole, which is of importance for fairness only *)
-
-restrict_def:
- "restrict A actns ==
+definition restrict :: "[('a, 's) ioa, 'a set] \<Rightarrow> ('a, 's) ioa"
+where
+ "restrict A actns =
(restrict_asig (asig_of A) actns,
starts_of A,
trans_of A,
wfair_of A,
sfair_of A)"
-hide_asig_def:
- "hide_asig asig actns ==
+definition hide_asig :: "['a signature, 'a set] \<Rightarrow> 'a signature"
+where
+ "hide_asig asig actns =
(inputs(asig) - actns,
outputs(asig) - actns,
- internals(asig) Un actns)"
+ internals(asig) \<union> actns)"
-hide_def:
- "hide A actns ==
+definition hide :: "[('a, 's) ioa, 'a set] \<Rightarrow> ('a, 's) ioa"
+where
+ "hide A actns =
(hide_asig (asig_of A) actns,
starts_of A,
trans_of A,
@@ -191,49 +153,62 @@
(* ------------------------- renaming ------------------------------------------- *)
-rename_set_def:
- "rename_set A ren == {b. ? x. Some x = ren b & x : A}"
+definition rename_set :: "'a set \<Rightarrow> ('c \<Rightarrow> 'a option) \<Rightarrow> 'c set"
+ where "rename_set A ren = {b. \<exists>x. Some x = ren b \<and> x \<in> A}"
-rename_def:
-"rename ioa ren ==
- ((rename_set (inp ioa) ren,
- rename_set (out ioa) ren,
- rename_set (int ioa) ren),
- starts_of ioa,
- {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
- in
- ? x. Some(x) = ren(a) & (s,x,t):trans_of ioa},
- {rename_set s ren | s. s: wfair_of ioa},
- {rename_set s ren | s. s: sfair_of ioa})"
+definition rename :: "('a, 'b) ioa \<Rightarrow> ('c \<Rightarrow> 'a option) \<Rightarrow> ('c, 'b) ioa"
+where
+ "rename ioa ren =
+ ((rename_set (inp ioa) ren,
+ rename_set (out ioa) ren,
+ rename_set (int ioa) ren),
+ starts_of ioa,
+ {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
+ in
+ \<exists>x. Some(x) = ren(a) \<and> (s,x,t):trans_of ioa},
+ {rename_set s ren | s. s \<in> wfair_of ioa},
+ {rename_set s ren | s. s \<in> sfair_of ioa})"
+
(* ------------------------- fairness ----------------------------- *)
-fairIOA_def:
- "fairIOA A == (! S : wfair_of A. S<= local A) &
- (! S : sfair_of A. S<= local A)"
+(* enabledness of actions and action sets *)
+
+definition enabled :: "('a, 's) ioa \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool"
+ where "enabled A a s \<longleftrightarrow> (\<exists>t. s \<midarrow>a\<midarrow>A\<rightarrow> t)"
+
+definition Enabled :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> 's \<Rightarrow> bool"
+ where "Enabled A W s \<longleftrightarrow> (\<exists>w \<in> W. enabled A w s)"
+
-input_resistant_def:
- "input_resistant A == ! W : sfair_of A. ! s a t.
- reachable A s & reachable A t & a:inp A &
- Enabled A W s & s \<midarrow>a\<midarrow>A\<rightarrow> t
- --> Enabled A W t"
+(* action set keeps enabled until probably disabled by itself *)
-enabled_def:
- "enabled A a s == ? t. s \<midarrow>a\<midarrow>A\<rightarrow> t"
+definition en_persistent :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> bool"
+where
+ "en_persistent A W \<longleftrightarrow>
+ (\<forall>s a t. Enabled A W s \<and> a \<notin> W \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> Enabled A W t)"
+
+
+(* post_conditions for actions and action sets *)
-Enabled_def:
- "Enabled A W s == ? w:W. enabled A w s"
+definition was_enabled :: "('a, 's) ioa \<Rightarrow> 'a \<Rightarrow> 's \<Rightarrow> bool"
+ where "was_enabled A a t \<longleftrightarrow> (\<exists>s. s \<midarrow>a\<midarrow>A\<rightarrow> t)"
+
+definition set_was_enabled :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> 's \<Rightarrow> bool"
+ where "set_was_enabled A W t \<longleftrightarrow> (\<exists>w \<in> W. was_enabled A w t)"
+
+
+(* constraints for fair IOA *)
-en_persistent_def:
- "en_persistent A W == ! s a t. Enabled A W s &
- a ~:W &
- s \<midarrow>a\<midarrow>A\<rightarrow> t
- --> Enabled A W t"
-was_enabled_def:
- "was_enabled A a t == ? s. s \<midarrow>a\<midarrow>A\<rightarrow> t"
+definition fairIOA :: "('a, 's) ioa \<Rightarrow> bool"
+ where "fairIOA A \<longleftrightarrow> (\<forall>S \<in> wfair_of A. S \<subseteq> local A) \<and> (\<forall>S \<in> sfair_of A. S \<subseteq> local A)"
-set_was_enabled_def:
- "set_was_enabled A W t == ? w:W. was_enabled A w t"
+definition input_resistant :: "('a, 's) ioa \<Rightarrow> bool"
+where
+ "input_resistant A \<longleftrightarrow>
+ (\<forall>W \<in> sfair_of A. \<forall>s a t.
+ reachable A s \<and> reachable A t \<and> a \<in> inp A \<and>
+ Enabled A W s \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> Enabled A W t)"
declare split_paired_Ex [simp del]
@@ -243,144 +218,121 @@
subsection "asig_of, starts_of, trans_of"
-lemma ioa_triple_proj:
- "((asig_of (x,y,z,w,s)) = x) &
- ((starts_of (x,y,z,w,s)) = y) &
- ((trans_of (x,y,z,w,s)) = z) &
- ((wfair_of (x,y,z,w,s)) = w) &
+lemma ioa_triple_proj:
+ "((asig_of (x,y,z,w,s)) = x) &
+ ((starts_of (x,y,z,w,s)) = y) &
+ ((trans_of (x,y,z,w,s)) = z) &
+ ((wfair_of (x,y,z,w,s)) = w) &
((sfair_of (x,y,z,w,s)) = s)"
apply (simp add: ioa_projections)
done
-lemma trans_in_actions:
+lemma trans_in_actions:
"[| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A"
-apply (unfold is_trans_of_def actions_def is_asig_def)
- apply (erule allE, erule impE, assumption)
- apply simp
-done
+ apply (unfold is_trans_of_def actions_def is_asig_def)
+ apply (erule allE, erule impE, assumption)
+ apply simp
+ done
-lemma starts_of_par:
-"starts_of(A \<parallel> B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"
- apply (simp add: par_def ioa_projections)
-done
+lemma starts_of_par: "starts_of(A \<parallel> B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"
+ by (simp add: par_def ioa_projections)
-lemma trans_of_par:
-"trans_of(A \<parallel> B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
- in (a:act A | a:act B) &
- (if a:act A then
- (fst(s),a,fst(t)):trans_of(A)
- else fst(t) = fst(s))
- &
- (if a:act B then
- (snd(s),a,snd(t)):trans_of(B)
+lemma trans_of_par:
+"trans_of(A \<parallel> B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
+ in (a:act A | a:act B) &
+ (if a:act A then
+ (fst(s),a,fst(t)):trans_of(A)
+ else fst(t) = fst(s))
+ &
+ (if a:act B then
+ (snd(s),a,snd(t)):trans_of(B)
else snd(t) = snd(s))}"
-
-apply (simp add: par_def ioa_projections)
-done
+ by (simp add: par_def ioa_projections)
subsection "actions and par"
-lemma actions_asig_comp:
- "actions(asig_comp a b) = actions(a) Un actions(b)"
- apply (simp (no_asm) add: actions_def asig_comp_def asig_projections)
+lemma actions_asig_comp: "actions(asig_comp a b) = actions(a) Un actions(b)"
+ by (auto simp add: actions_def asig_comp_def asig_projections)
+
+lemma asig_of_par: "asig_of(A \<parallel> B) = asig_comp (asig_of A) (asig_of B)"
+ by (simp add: par_def ioa_projections)
+
+
+lemma externals_of_par: "ext (A1\<parallel>A2) = (ext A1) Un (ext A2)"
+ apply (simp add: externals_def asig_of_par asig_comp_def
+ asig_inputs_def asig_outputs_def Un_def set_diff_eq)
apply blast
done
-lemma asig_of_par: "asig_of(A \<parallel> B) = asig_comp (asig_of A) (asig_of B)"
- apply (simp add: par_def ioa_projections)
+lemma actions_of_par: "act (A1\<parallel>A2) = (act A1) Un (act A2)"
+ apply (simp add: actions_def asig_of_par asig_comp_def
+ asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
+ apply blast
done
-
-lemma externals_of_par: "ext (A1\<parallel>A2) =
- (ext A1) Un (ext A2)"
-apply (simp add: externals_def asig_of_par asig_comp_def
- asig_inputs_def asig_outputs_def Un_def set_diff_eq)
-apply blast
-done
-
-lemma actions_of_par: "act (A1\<parallel>A2) =
- (act A1) Un (act A2)"
-apply (simp add: actions_def asig_of_par asig_comp_def
- asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
-apply blast
-done
+lemma inputs_of_par: "inp (A1\<parallel>A2) = ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))"
+ by (simp add: actions_def asig_of_par asig_comp_def
+ asig_inputs_def asig_outputs_def Un_def set_diff_eq)
-lemma inputs_of_par: "inp (A1\<parallel>A2) =
- ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))"
-apply (simp add: actions_def asig_of_par asig_comp_def
- asig_inputs_def asig_outputs_def Un_def set_diff_eq)
-done
+lemma outputs_of_par: "out (A1\<parallel>A2) = (out A1) Un (out A2)"
+ by (simp add: actions_def asig_of_par asig_comp_def
+ asig_outputs_def Un_def set_diff_eq)
-lemma outputs_of_par: "out (A1\<parallel>A2) =
- (out A1) Un (out A2)"
-apply (simp add: actions_def asig_of_par asig_comp_def
- asig_outputs_def Un_def set_diff_eq)
-done
-
-lemma internals_of_par: "int (A1\<parallel>A2) =
- (int A1) Un (int A2)"
-apply (simp add: actions_def asig_of_par asig_comp_def
- asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
-done
+lemma internals_of_par: "int (A1\<parallel>A2) = (int A1) Un (int A2)"
+ by (simp add: actions_def asig_of_par asig_comp_def
+ asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
subsection "actions and compatibility"
lemma compat_commute: "compatible A B = compatible B A"
-apply (simp add: compatible_def Int_commute)
-apply auto
-done
+ by (auto simp add: compatible_def Int_commute)
-lemma ext1_is_not_int2:
- "[| compatible A1 A2; a:ext A1|] ==> a~:int A2"
-apply (unfold externals_def actions_def compatible_def)
-apply simp
-apply blast
-done
+lemma ext1_is_not_int2: "[| compatible A1 A2; a:ext A1|] ==> a~:int A2"
+ apply (unfold externals_def actions_def compatible_def)
+ apply simp
+ apply blast
+ done
(* just commuting the previous one: better commute compatible *)
-lemma ext2_is_not_int1:
- "[| compatible A2 A1 ; a:ext A1|] ==> a~:int A2"
-apply (unfold externals_def actions_def compatible_def)
-apply simp
-apply blast
-done
+lemma ext2_is_not_int1: "[| compatible A2 A1 ; a:ext A1|] ==> a~:int A2"
+ apply (unfold externals_def actions_def compatible_def)
+ apply simp
+ apply blast
+ done
lemmas ext1_ext2_is_not_act2 = ext1_is_not_int2 [THEN int_and_ext_is_act]
lemmas ext1_ext2_is_not_act1 = ext2_is_not_int1 [THEN int_and_ext_is_act]
-lemma intA_is_not_extB:
- "[| compatible A B; x:int A |] ==> x~:ext B"
-apply (unfold externals_def actions_def compatible_def)
-apply simp
-apply blast
-done
+lemma intA_is_not_extB: "[| compatible A B; x:int A |] ==> x~:ext B"
+ apply (unfold externals_def actions_def compatible_def)
+ apply simp
+ apply blast
+ done
-lemma intA_is_not_actB:
-"[| compatible A B; a:int A |] ==> a ~: act B"
-apply (unfold externals_def actions_def compatible_def is_asig_def asig_of_def)
-apply simp
-apply blast
-done
+lemma intA_is_not_actB: "[| compatible A B; a:int A |] ==> a ~: act B"
+ apply (unfold externals_def actions_def compatible_def is_asig_def asig_of_def)
+ apply simp
+ apply blast
+ done
(* the only one that needs disjointness of outputs and of internals and _all_ acts *)
-lemma outAactB_is_inpB:
-"[| compatible A B; a:out A ;a:act B|] ==> a : inp B"
-apply (unfold asig_outputs_def asig_internals_def actions_def asig_inputs_def
- compatible_def is_asig_def asig_of_def)
-apply simp
-apply blast
-done
+lemma outAactB_is_inpB: "[| compatible A B; a:out A ;a:act B|] ==> a : inp B"
+ apply (unfold asig_outputs_def asig_internals_def actions_def asig_inputs_def
+ compatible_def is_asig_def asig_of_def)
+ apply simp
+ apply blast
+ done
(* needed for propagation of input_enabledness from A,B to A\<parallel>B *)
-lemma inpAAactB_is_inpBoroutB:
-"[| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B"
-apply (unfold asig_outputs_def asig_internals_def actions_def asig_inputs_def
- compatible_def is_asig_def asig_of_def)
-apply simp
-apply blast
-done
+lemma inpAAactB_is_inpBoroutB:
+ "[| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B"
+ apply (unfold asig_outputs_def asig_internals_def actions_def asig_inputs_def
+ compatible_def is_asig_def asig_of_def)
+ apply simp
+ apply blast
+ done
subsection "input_enabledness and par"
@@ -388,88 +340,88 @@
(* ugly case distinctions. Heart of proof:
1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
-lemma input_enabled_par:
-"[| compatible A B; input_enabled A; input_enabled B|]
- ==> input_enabled (A\<parallel>B)"
-apply (unfold input_enabled_def)
-apply (simp add: Let_def inputs_of_par trans_of_par)
-apply (tactic "safe_tac (Context.raw_transfer @{theory} @{theory_context Fun})")
-apply (simp add: inp_is_act)
-prefer 2
-apply (simp add: inp_is_act)
-(* a: inp A *)
-apply (case_tac "a:act B")
-(* a:act B *)
-apply (erule_tac x = "a" in allE)
-apply simp
-apply (drule inpAAactB_is_inpBoroutB)
-apply assumption
-apply assumption
-apply (erule_tac x = "a" in allE)
-apply simp
-apply (erule_tac x = "aa" in allE)
-apply (erule_tac x = "b" in allE)
-apply (erule exE)
-apply (erule exE)
-apply (rule_tac x = " (s2,s2a) " in exI)
-apply (simp add: inp_is_act)
-(* a~: act B*)
-apply (simp add: inp_is_act)
-apply (erule_tac x = "a" in allE)
-apply simp
-apply (erule_tac x = "aa" in allE)
-apply (erule exE)
-apply (rule_tac x = " (s2,b) " in exI)
-apply simp
-
-(* a:inp B *)
-apply (case_tac "a:act A")
-(* a:act A *)
-apply (erule_tac x = "a" in allE)
-apply (erule_tac x = "a" in allE)
-apply (simp add: inp_is_act)
-apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
-apply (drule inpAAactB_is_inpBoroutB)
-back
-apply assumption
-apply assumption
-apply simp
-apply (erule_tac x = "aa" in allE)
-apply (erule_tac x = "b" in allE)
-apply (erule exE)
-apply (erule exE)
-apply (rule_tac x = " (s2,s2a) " in exI)
-apply (simp add: inp_is_act)
-(* a~: act B*)
-apply (simp add: inp_is_act)
-apply (erule_tac x = "a" in allE)
-apply (erule_tac x = "a" in allE)
-apply simp
-apply (erule_tac x = "b" in allE)
-apply (erule exE)
-apply (rule_tac x = " (aa,s2) " in exI)
-apply simp
-done
+lemma input_enabled_par:
+ "[| compatible A B; input_enabled A; input_enabled B|]
+ ==> input_enabled (A\<parallel>B)"
+ apply (unfold input_enabled_def)
+ apply (simp add: Let_def inputs_of_par trans_of_par)
+ apply (tactic "safe_tac (Context.raw_transfer @{theory} @{theory_context Fun})")
+ apply (simp add: inp_is_act)
+ prefer 2
+ apply (simp add: inp_is_act)
+ (* a: inp A *)
+ apply (case_tac "a:act B")
+ (* a:act B *)
+ apply (erule_tac x = "a" in allE)
+ apply simp
+ apply (drule inpAAactB_is_inpBoroutB)
+ apply assumption
+ apply assumption
+ apply (erule_tac x = "a" in allE)
+ apply simp
+ apply (erule_tac x = "aa" in allE)
+ apply (erule_tac x = "b" in allE)
+ apply (erule exE)
+ apply (erule exE)
+ apply (rule_tac x = " (s2,s2a) " in exI)
+ apply (simp add: inp_is_act)
+ (* a~: act B*)
+ apply (simp add: inp_is_act)
+ apply (erule_tac x = "a" in allE)
+ apply simp
+ apply (erule_tac x = "aa" in allE)
+ apply (erule exE)
+ apply (rule_tac x = " (s2,b) " in exI)
+ apply simp
+
+ (* a:inp B *)
+ apply (case_tac "a:act A")
+ (* a:act A *)
+ apply (erule_tac x = "a" in allE)
+ apply (erule_tac x = "a" in allE)
+ apply (simp add: inp_is_act)
+ apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
+ apply (drule inpAAactB_is_inpBoroutB)
+ back
+ apply assumption
+ apply assumption
+ apply simp
+ apply (erule_tac x = "aa" in allE)
+ apply (erule_tac x = "b" in allE)
+ apply (erule exE)
+ apply (erule exE)
+ apply (rule_tac x = " (s2,s2a) " in exI)
+ apply (simp add: inp_is_act)
+ (* a~: act B*)
+ apply (simp add: inp_is_act)
+ apply (erule_tac x = "a" in allE)
+ apply (erule_tac x = "a" in allE)
+ apply simp
+ apply (erule_tac x = "b" in allE)
+ apply (erule exE)
+ apply (rule_tac x = " (aa,s2) " in exI)
+ apply simp
+ done
subsection "invariants"
lemma invariantI:
- "[| !!s. s:starts_of(A) ==> P(s);
- !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |]
+ "[| !!s. s:starts_of(A) ==> P(s);
+ !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |]
==> invariant A P"
-apply (unfold invariant_def)
-apply (rule allI)
-apply (rule impI)
-apply (rule_tac x = "s" in reachable.induct)
-apply assumption
-apply blast
-apply blast
-done
+ apply (unfold invariant_def)
+ apply (rule allI)
+ apply (rule impI)
+ apply (rule_tac x = "s" in reachable.induct)
+ apply assumption
+ apply blast
+ apply blast
+ done
lemma invariantI1:
- "[| !!s. s : starts_of(A) ==> P(s);
- !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t)
+ "[| !!s. s : starts_of(A) ==> P(s);
+ !!s t a. reachable A s ==> P(s) --> (s,a,t):trans_of(A) --> P(t)
|] ==> invariant A P"
apply (blast intro: invariantI)
done
@@ -486,200 +438,177 @@
lemmas reachable_0 = reachable.reachable_0
and reachable_n = reachable.reachable_n
-lemma cancel_restrict_a: "starts_of(restrict ioa acts) = starts_of(ioa) &
+lemma cancel_restrict_a: "starts_of(restrict ioa acts) = starts_of(ioa) &
trans_of(restrict ioa acts) = trans_of(ioa)"
-apply (simp add: restrict_def ioa_projections)
-done
+ by (simp add: restrict_def ioa_projections)
lemma cancel_restrict_b: "reachable (restrict ioa acts) s = reachable ioa s"
-apply (rule iffI)
-apply (erule reachable.induct)
-apply (simp add: cancel_restrict_a reachable_0)
-apply (erule reachable_n)
-apply (simp add: cancel_restrict_a)
-(* <-- *)
-apply (erule reachable.induct)
-apply (rule reachable_0)
-apply (simp add: cancel_restrict_a)
-apply (erule reachable_n)
-apply (simp add: cancel_restrict_a)
-done
+ apply (rule iffI)
+ apply (erule reachable.induct)
+ apply (simp add: cancel_restrict_a reachable_0)
+ apply (erule reachable_n)
+ apply (simp add: cancel_restrict_a)
+ (* <-- *)
+ apply (erule reachable.induct)
+ apply (rule reachable_0)
+ apply (simp add: cancel_restrict_a)
+ apply (erule reachable_n)
+ apply (simp add: cancel_restrict_a)
+ done
lemma acts_restrict: "act (restrict A acts) = act A"
-apply (simp (no_asm) add: actions_def asig_internals_def
- asig_outputs_def asig_inputs_def externals_def asig_of_def restrict_def restrict_asig_def)
-apply auto
-done
+ apply (simp (no_asm) add: actions_def asig_internals_def
+ asig_outputs_def asig_inputs_def externals_def asig_of_def restrict_def restrict_asig_def)
+ apply auto
+ done
-lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) &
- trans_of(restrict ioa acts) = trans_of(ioa) &
- reachable (restrict ioa acts) s = reachable ioa s &
+lemma cancel_restrict: "starts_of(restrict ioa acts) = starts_of(ioa) &
+ trans_of(restrict ioa acts) = trans_of(ioa) &
+ reachable (restrict ioa acts) s = reachable ioa s &
act (restrict A acts) = act A"
- apply (simp (no_asm) add: cancel_restrict_a cancel_restrict_b acts_restrict)
- done
+ by (simp add: cancel_restrict_a cancel_restrict_b acts_restrict)
subsection "rename"
lemma trans_rename: "s \<midarrow>a\<midarrow>(rename C f)\<rightarrow> t ==> (? x. Some(x) = f(a) & s \<midarrow>x\<midarrow>C\<rightarrow> t)"
-apply (simp add: Let_def rename_def trans_of_def)
-done
+ by (simp add: Let_def rename_def trans_of_def)
lemma reachable_rename: "[| reachable (rename C g) s |] ==> reachable C s"
-apply (erule reachable.induct)
-apply (rule reachable_0)
-apply (simp add: rename_def ioa_projections)
-apply (drule trans_rename)
-apply (erule exE)
-apply (erule conjE)
-apply (erule reachable_n)
-apply assumption
-done
+ apply (erule reachable.induct)
+ apply (rule reachable_0)
+ apply (simp add: rename_def ioa_projections)
+ apply (drule trans_rename)
+ apply (erule exE)
+ apply (erule conjE)
+ apply (erule reachable_n)
+ apply assumption
+ done
subsection "trans_of(A\<parallel>B)"
-
-lemma trans_A_proj: "[|(s,a,t):trans_of (A\<parallel>B); a:act A|]
+lemma trans_A_proj: "[|(s,a,t):trans_of (A\<parallel>B); a:act A|]
==> (fst s,a,fst t):trans_of A"
-apply (simp add: Let_def par_def trans_of_def)
-done
+ by (simp add: Let_def par_def trans_of_def)
-lemma trans_B_proj: "[|(s,a,t):trans_of (A\<parallel>B); a:act B|]
+lemma trans_B_proj: "[|(s,a,t):trans_of (A\<parallel>B); a:act B|]
==> (snd s,a,snd t):trans_of B"
-apply (simp add: Let_def par_def trans_of_def)
-done
+ by (simp add: Let_def par_def trans_of_def)
-lemma trans_A_proj2: "[|(s,a,t):trans_of (A\<parallel>B); a~:act A|]
+lemma trans_A_proj2: "[|(s,a,t):trans_of (A\<parallel>B); a~:act A|]
==> fst s = fst t"
-apply (simp add: Let_def par_def trans_of_def)
-done
+ by (simp add: Let_def par_def trans_of_def)
-lemma trans_B_proj2: "[|(s,a,t):trans_of (A\<parallel>B); a~:act B|]
+lemma trans_B_proj2: "[|(s,a,t):trans_of (A\<parallel>B); a~:act B|]
==> snd s = snd t"
-apply (simp add: Let_def par_def trans_of_def)
-done
+ by (simp add: Let_def par_def trans_of_def)
-lemma trans_AB_proj: "(s,a,t):trans_of (A\<parallel>B)
+lemma trans_AB_proj: "(s,a,t):trans_of (A\<parallel>B)
==> a :act A | a :act B"
-apply (simp add: Let_def par_def trans_of_def)
-done
+ by (simp add: Let_def par_def trans_of_def)
-lemma trans_AB: "[|a:act A;a:act B;
- (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|]
+lemma trans_AB: "[|a:act A;a:act B;
+ (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|]
==> (s,a,t):trans_of (A\<parallel>B)"
-apply (simp add: Let_def par_def trans_of_def)
-done
+ by (simp add: Let_def par_def trans_of_def)
-lemma trans_A_notB: "[|a:act A;a~:act B;
- (fst s,a,fst t):trans_of A;snd s=snd t|]
+lemma trans_A_notB: "[|a:act A;a~:act B;
+ (fst s,a,fst t):trans_of A;snd s=snd t|]
==> (s,a,t):trans_of (A\<parallel>B)"
-apply (simp add: Let_def par_def trans_of_def)
-done
+ by (simp add: Let_def par_def trans_of_def)
-lemma trans_notA_B: "[|a~:act A;a:act B;
- (snd s,a,snd t):trans_of B;fst s=fst t|]
+lemma trans_notA_B: "[|a~:act A;a:act B;
+ (snd s,a,snd t):trans_of B;fst s=fst t|]
==> (s,a,t):trans_of (A\<parallel>B)"
-apply (simp add: Let_def par_def trans_of_def)
-done
+ by (simp add: Let_def par_def trans_of_def)
lemmas trans_of_defs1 = trans_AB trans_A_notB trans_notA_B
and trans_of_defs2 = trans_A_proj trans_B_proj trans_A_proj2 trans_B_proj2 trans_AB_proj
-lemma trans_of_par4:
-"((s,a,t) : trans_of(A \<parallel> B \<parallel> C \<parallel> D)) =
- ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |
- a:actions(asig_of(D))) &
- (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)
- else fst t=fst s) &
- (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B)
- else fst(snd(t))=fst(snd(s))) &
- (if a:actions(asig_of(C)) then
- (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C)
- else fst(snd(snd(t)))=fst(snd(snd(s)))) &
- (if a:actions(asig_of(D)) then
- (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)
+lemma trans_of_par4:
+"((s,a,t) : trans_of(A \<parallel> B \<parallel> C \<parallel> D)) =
+ ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |
+ a:actions(asig_of(D))) &
+ (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)
+ else fst t=fst s) &
+ (if a:actions(asig_of(B)) then (fst(snd(s)),a,fst(snd(t))):trans_of(B)
+ else fst(snd(t))=fst(snd(s))) &
+ (if a:actions(asig_of(C)) then
+ (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C)
+ else fst(snd(snd(t)))=fst(snd(snd(s)))) &
+ (if a:actions(asig_of(D)) then
+ (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)
else snd(snd(snd(t)))=snd(snd(snd(s)))))"
- apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff Let_def ioa_projections)
- done
+ by (simp add: par_def actions_asig_comp prod_eq_iff Let_def ioa_projections)
subsection "proof obligation generator for IOA requirements"
(* without assumptions on A and B because is_trans_of is also incorporated in \<parallel>def *)
lemma is_trans_of_par: "is_trans_of (A\<parallel>B)"
-apply (unfold is_trans_of_def)
-apply (simp add: Let_def actions_of_par trans_of_par)
-done
+ by (simp add: is_trans_of_def Let_def actions_of_par trans_of_par)
+
+lemma is_trans_of_restrict: "is_trans_of A ==> is_trans_of (restrict A acts)"
+ by (simp add: is_trans_of_def cancel_restrict acts_restrict)
-lemma is_trans_of_restrict:
-"is_trans_of A ==> is_trans_of (restrict A acts)"
-apply (unfold is_trans_of_def)
-apply (simp add: cancel_restrict acts_restrict)
-done
+lemma is_trans_of_rename: "is_trans_of A ==> is_trans_of (rename A f)"
+ apply (unfold is_trans_of_def restrict_def restrict_asig_def)
+ apply (simp add: Let_def actions_def trans_of_def asig_internals_def
+ asig_outputs_def asig_inputs_def externals_def asig_of_def rename_def rename_set_def)
+ apply blast
+ done
-lemma is_trans_of_rename:
-"is_trans_of A ==> is_trans_of (rename A f)"
-apply (unfold is_trans_of_def restrict_def restrict_asig_def)
-apply (simp add: Let_def actions_def trans_of_def asig_internals_def
- asig_outputs_def asig_inputs_def externals_def asig_of_def rename_def rename_set_def)
-apply blast
-done
-
-lemma is_asig_of_par: "[| is_asig_of A; is_asig_of B; compatible A B|]
+lemma is_asig_of_par: "[| is_asig_of A; is_asig_of B; compatible A B|]
==> is_asig_of (A\<parallel>B)"
-apply (simp add: is_asig_of_def asig_of_par asig_comp_def compatible_def
- asig_internals_def asig_outputs_def asig_inputs_def actions_def is_asig_def)
-apply (simp add: asig_of_def)
-apply auto
-done
+ apply (simp add: is_asig_of_def asig_of_par asig_comp_def compatible_def
+ asig_internals_def asig_outputs_def asig_inputs_def actions_def is_asig_def)
+ apply (simp add: asig_of_def)
+ apply auto
+ done
-lemma is_asig_of_restrict:
-"is_asig_of A ==> is_asig_of (restrict A f)"
-apply (unfold is_asig_of_def is_asig_def asig_of_def restrict_def restrict_asig_def
- asig_internals_def asig_outputs_def asig_inputs_def externals_def o_def)
-apply simp
-apply auto
-done
+lemma is_asig_of_restrict: "is_asig_of A ==> is_asig_of (restrict A f)"
+ apply (unfold is_asig_of_def is_asig_def asig_of_def restrict_def restrict_asig_def
+ asig_internals_def asig_outputs_def asig_inputs_def externals_def o_def)
+ apply simp
+ apply auto
+ done
lemma is_asig_of_rename: "is_asig_of A ==> is_asig_of (rename A f)"
-apply (simp add: is_asig_of_def rename_def rename_set_def asig_internals_def
- asig_outputs_def asig_inputs_def actions_def is_asig_def asig_of_def)
-apply auto
-apply (drule_tac [!] s = "Some _" in sym)
-apply auto
-done
+ apply (simp add: is_asig_of_def rename_def rename_set_def asig_internals_def
+ asig_outputs_def asig_inputs_def actions_def is_asig_def asig_of_def)
+ apply auto
+ apply (drule_tac [!] s = "Some _" in sym)
+ apply auto
+ done
lemmas [simp] = is_asig_of_par is_asig_of_restrict
is_asig_of_rename is_trans_of_par is_trans_of_restrict is_trans_of_rename
-lemma compatible_par:
-"[|compatible A B; compatible A C |]==> compatible A (B\<parallel>C)"
-apply (unfold compatible_def)
-apply (simp add: internals_of_par outputs_of_par actions_of_par)
-apply auto
-done
+lemma compatible_par: "[|compatible A B; compatible A C |]==> compatible A (B\<parallel>C)"
+ apply (unfold compatible_def)
+ apply (simp add: internals_of_par outputs_of_par actions_of_par)
+ apply auto
+ done
(* better derive by previous one and compat_commute *)
-lemma compatible_par2:
-"[|compatible A C; compatible B C |]==> compatible (A\<parallel>B) C"
-apply (unfold compatible_def)
-apply (simp add: internals_of_par outputs_of_par actions_of_par)
-apply auto
-done
+lemma compatible_par2: "[|compatible A C; compatible B C |]==> compatible (A\<parallel>B) C"
+ apply (unfold compatible_def)
+ apply (simp add: internals_of_par outputs_of_par actions_of_par)
+ apply auto
+ done
-lemma compatible_restrict:
-"[| compatible A B; (ext B - S) Int ext A = {}|]
- ==> compatible A (restrict B S)"
-apply (unfold compatible_def)
-apply (simp add: ioa_triple_proj asig_triple_proj externals_def
- restrict_def restrict_asig_def actions_def)
-apply auto
-done
-
+lemma compatible_restrict:
+ "[| compatible A B; (ext B - S) Int ext A = {}|]
+ ==> compatible A (restrict B S)"
+ apply (unfold compatible_def)
+ apply (simp add: ioa_triple_proj asig_triple_proj externals_def
+ restrict_def restrict_asig_def actions_def)
+ apply auto
+ done
declare split_paired_Ex [simp]
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Dec 30 22:09:44 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Thu Dec 31 00:07:42 2015 +0100
@@ -287,15 +287,8 @@
(* generalizing the proof above to a proof method *)
ML \<open>
-
-local
- val defs = [@{thm Filter_def}, @{thm Forall_def}, @{thm sforall_def}, @{thm mkex_def},
- @{thm stutter_def}]
- val asigs = [@{thm asig_of_par}, @{thm actions_asig_comp}]
-in
-
fun mkex_induct_tac ctxt sch exA exB =
- EVERY'[Seq_induct_tac ctxt sch defs,
+ EVERY'[Seq_induct_tac ctxt sch @{thms Filter_def Forall_def sforall_def mkex_def stutter_def},
asm_full_simp_tac ctxt,
SELECT_GOAL
(safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) @{theory_context Fun})),
@@ -306,10 +299,8 @@
asm_full_simp_tac ctxt,
Seq_case_simp_tac ctxt exB,
asm_full_simp_tac ctxt,
- asm_full_simp_tac (ctxt addsimps asigs)
+ asm_full_simp_tac (ctxt addsimps @{thms asig_of_par actions_asig_comp})
]
-
-end
\<close>
method_setup mkex_induct = \<open>
@@ -496,7 +487,7 @@
(Filter (%a. a:act A)$sch : schedules A &
Filter (%a. a:act B)$sch : schedules B &
Forall (%x. x:act (A\<parallel>B)) sch)"
-apply (simp (no_asm) add: schedules_def has_schedule_def)
+apply (simp add: schedules_def has_schedule_def)
apply auto
(* ==> *)
apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex) " in bexI)
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Dec 30 22:09:44 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Thu Dec 31 00:07:42 2015 +0100
@@ -1,30 +1,23 @@
(* Title: HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
Author: Olaf Müller
-*)
+*)
section \<open>Compositionality on Trace level\<close>
theory CompoTraces
imports CompoScheds ShortExecutions
begin
-
-consts
-
- mksch ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq"
- par_traces ::"['a trace_module,'a trace_module] => 'a trace_module"
-
-defs
-
-mksch_def:
- "mksch A B == (fix$(LAM h tr schA schB. case tr of
+definition mksch :: "('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq"
+where
+ "mksch A B = (fix$(LAM h tr schA schB. case tr of
nil => nil
- | x##xs =>
- (case x of
+ | x##xs =>
+ (case x of
UU => UU
- | Def y =>
- (if y:act A then
- (if y:act B then
+ | Def y =>
+ (if y:act A then
+ (if y:act B then
((Takewhile (%a. a:int A)$schA)
@@ (Takewhile (%a. a:int B)$schB)
@@ (y\<leadsto>(h$xs
@@ -37,8 +30,8 @@
$(TL$(Dropwhile (%a. a:int A)$schA))
$schB)))
)
- else
- (if y:act B then
+ else
+ (if y:act B then
((Takewhile (%a. a:int B)$schB)
@@ (y\<leadsto>(h$xs
$schA
@@ -50,21 +43,21 @@
)
)))"
-
-par_traces_def:
- "par_traces TracesA TracesB ==
- let trA = fst TracesA; sigA = snd TracesA;
- trB = fst TracesB; sigB = snd TracesB
+definition par_traces ::"['a trace_module,'a trace_module] => 'a trace_module"
+where
+ "par_traces TracesA TracesB =
+ (let trA = fst TracesA; sigA = snd TracesA;
+ trB = fst TracesB; sigB = snd TracesB
in
( {tr. Filter (%a. a:actions sigA)$tr : trA}
Int {tr. Filter (%a. a:actions sigB)$tr : trB}
Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
- asig_comp sigA sigB)"
+ asig_comp sigA sigB))"
-axiomatization where
-
-finiteR_mksch:
- "Finite (mksch A B$tr$x$y) \<Longrightarrow> Finite tr"
+axiomatization
+where
+ finiteR_mksch:
+ "Finite (mksch A B$tr$x$y) \<Longrightarrow> Finite tr"
lemma finiteR_mksch': "\<not> Finite tr \<Longrightarrow> \<not> Finite (mksch A B$tr$x$y)"
by (blast intro: finiteR_mksch)
@@ -76,40 +69,40 @@
subsection "mksch rewrite rules"
lemma mksch_unfold:
-"mksch A B = (LAM tr schA schB. case tr of
+"mksch A B = (LAM tr schA schB. case tr of
nil => nil
- | x##xs =>
- (case x of
- UU => UU
- | Def y =>
- (if y:act A then
- (if y:act B then
- ((Takewhile (%a. a:int A)$schA)
- @@(Takewhile (%a. a:int B)$schB)
- @@(y\<leadsto>(mksch A B$xs
- $(TL$(Dropwhile (%a. a:int A)$schA))
- $(TL$(Dropwhile (%a. a:int B)$schB))
- )))
- else
- ((Takewhile (%a. a:int A)$schA)
- @@ (y\<leadsto>(mksch A B$xs
- $(TL$(Dropwhile (%a. a:int A)$schA))
- $schB)))
- )
- else
- (if y:act B then
- ((Takewhile (%a. a:int B)$schB)
- @@ (y\<leadsto>(mksch A B$xs
- $schA
- $(TL$(Dropwhile (%a. a:int B)$schB))
- )))
- else
- UU
- )
- )
+ | x##xs =>
+ (case x of
+ UU => UU
+ | Def y =>
+ (if y:act A then
+ (if y:act B then
+ ((Takewhile (%a. a:int A)$schA)
+ @@(Takewhile (%a. a:int B)$schB)
+ @@(y\<leadsto>(mksch A B$xs
+ $(TL$(Dropwhile (%a. a:int A)$schA))
+ $(TL$(Dropwhile (%a. a:int B)$schB))
+ )))
+ else
+ ((Takewhile (%a. a:int A)$schA)
+ @@ (y\<leadsto>(mksch A B$xs
+ $(TL$(Dropwhile (%a. a:int A)$schA))
+ $schB)))
+ )
+ else
+ (if y:act B then
+ ((Takewhile (%a. a:int B)$schB)
+ @@ (y\<leadsto>(mksch A B$xs
+ $schA
+ $(TL$(Dropwhile (%a. a:int B)$schB))
+ )))
+ else
+ UU
+ )
+ )
))"
apply (rule trans)
-apply (rule fix_eq2)
+apply (rule fix_eq4)
apply (rule mksch_def)
apply (rule beta_cfun)
apply simp
@@ -125,10 +118,10 @@
apply simp
done
-lemma mksch_cons1: "[|x:act A;x~:act B|]
- ==> mksch A B$(x\<leadsto>tr)$schA$schB =
- (Takewhile (%a. a:int A)$schA)
- @@ (x\<leadsto>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))
+lemma mksch_cons1: "[|x:act A;x~:act B|]
+ ==> mksch A B$(x\<leadsto>tr)$schA$schB =
+ (Takewhile (%a. a:int A)$schA)
+ @@ (x\<leadsto>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))
$schB))"
apply (rule trans)
apply (subst mksch_unfold)
@@ -136,10 +129,10 @@
apply (simp add: Consq_def)
done
-lemma mksch_cons2: "[|x~:act A;x:act B|]
- ==> mksch A B$(x\<leadsto>tr)$schA$schB =
- (Takewhile (%a. a:int B)$schB)
- @@ (x\<leadsto>(mksch A B$tr$schA$(TL$(Dropwhile (%a. a:int B)$schB))
+lemma mksch_cons2: "[|x~:act A;x:act B|]
+ ==> mksch A B$(x\<leadsto>tr)$schA$schB =
+ (Takewhile (%a. a:int B)$schB)
+ @@ (x\<leadsto>(mksch A B$tr$schA$(TL$(Dropwhile (%a. a:int B)$schB))
))"
apply (rule trans)
apply (subst mksch_unfold)
@@ -147,12 +140,12 @@
apply (simp add: Consq_def)
done
-lemma mksch_cons3: "[|x:act A;x:act B|]
- ==> mksch A B$(x\<leadsto>tr)$schA$schB =
- (Takewhile (%a. a:int A)$schA)
- @@ ((Takewhile (%a. a:int B)$schB)
- @@ (x\<leadsto>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))
- $(TL$(Dropwhile (%a. a:int B)$schB))))
+lemma mksch_cons3: "[|x:act A;x:act B|]
+ ==> mksch A B$(x\<leadsto>tr)$schA$schB =
+ (Takewhile (%a. a:int A)$schA)
+ @@ ((Takewhile (%a. a:int B)$schB)
+ @@ (x\<leadsto>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))
+ $(TL$(Dropwhile (%a. a:int B)$schB))))
)"
apply (rule trans)
apply (subst mksch_unfold)
@@ -173,7 +166,7 @@
the compatibility of IOA, in particular out of the condition that internals are
really hidden. *)
-lemma compatibility_consequence1: "(eB & ~eA --> ~A) -->
+lemma compatibility_consequence1: "(eB & ~eA --> ~A) -->
(A & (eA | eB)) = (eA & A)"
apply fast
done
@@ -181,7 +174,7 @@
(* very similar to above, only the commutativity of | is used to make a slight change *)
-lemma compatibility_consequence2: "(eB & ~eA --> ~A) -->
+lemma compatibility_consequence2: "(eB & ~eA --> ~A) -->
(A & (eB | eA)) = (eA & A)"
apply fast
done
@@ -198,8 +191,8 @@
by (erule subst)
lemma ForallAorB_mksch [rule_format]:
- "!!A B. compatible A B ==>
- ! schA schB. Forall (%x. x:act (A\<parallel>B)) tr
+ "!!A B. compatible A B ==>
+ ! schA schB. Forall (%x. x:act (A\<parallel>B)) tr
--> Forall (%x. x:act (A\<parallel>B)) (mksch A B$tr$schA$schB)"
apply (tactic \<open>Seq_induct_tac @{context} "tr"
[@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
@@ -226,8 +219,8 @@
apply auto
done
-lemma ForallBnAmksch [rule_format (no_asm)]: "!!A B. compatible B A ==>
- ! schA schB. (Forall (%x. x:act B & x~:act A) tr
+lemma ForallBnAmksch [rule_format (no_asm)]: "!!A B. compatible B A ==>
+ ! schA schB. (Forall (%x. x:act B & x~:act A) tr
--> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"
apply (tactic \<open>Seq_induct_tac @{context} "tr"
[@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
@@ -236,8 +229,8 @@
apply (simp add: intA_is_not_actB int_is_act)
done
-lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>
- ! schA schB. (Forall (%x. x:act A & x~:act B) tr
+lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>
+ ! schA schB. (Forall (%x. x:act A & x~:act B) tr
--> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"
apply (tactic \<open>Seq_induct_tac @{context} "tr"
[@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
@@ -249,11 +242,11 @@
(* safe-tac makes too many case distinctions with this lemma in the next proof *)
declare FiniteConc [simp del]
-lemma FiniteL_mksch [rule_format (no_asm)]: "[| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==>
- ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y &
- Filter (%a. a:ext A)$x = Filter (%a. a:act A)$tr &
- Filter (%a. a:ext B)$y = Filter (%a. a:act B)$tr &
- Forall (%x. x:ext (A\<parallel>B)) tr
+lemma FiniteL_mksch [rule_format (no_asm)]: "[| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==>
+ ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y &
+ Filter (%a. a:ext A)$x = Filter (%a. a:act A)$tr &
+ Filter (%a. a:ext B)$y = Filter (%a. a:act B)$tr &
+ Forall (%x. x:ext (A\<parallel>B)) tr
--> Finite (mksch A B$tr$x$y)"
apply (erule Seq_Finite_ind)
@@ -309,12 +302,12 @@
declare FilterConc [simp del]
-lemma reduceA_mksch1 [rule_format (no_asm)]: " [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>
- ! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &
- Filter (%a. a:ext B)$y = Filter (%a. a:act B)$(bs @@ z)
- --> (? y1 y2. (mksch A B$(bs @@ z)$x$y) = (y1 @@ (mksch A B$z$x$y2)) &
- Forall (%x. x:act B & x~:act A) y1 &
- Finite y1 & y = (y1 @@ y2) &
+lemma reduceA_mksch1 [rule_format (no_asm)]: " [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>
+ ! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &
+ Filter (%a. a:ext B)$y = Filter (%a. a:act B)$(bs @@ z)
+ --> (? y1 y2. (mksch A B$(bs @@ z)$x$y) = (y1 @@ (mksch A B$z$x$y2)) &
+ Forall (%x. x:act B & x~:act A) y1 &
+ Finite y1 & y = (y1 @@ y2) &
Filter (%a. a:ext B)$y1 = bs)"
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
apply (erule Seq_Finite_ind)
@@ -355,12 +348,12 @@
lemmas reduceA_mksch = conjI [THEN [6] conjI [THEN [5] reduceA_mksch1]]
lemma reduceB_mksch1 [rule_format]:
-" [| Finite a_s; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>
- ! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) a_s &
- Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(a_s @@ z)
- --> (? x1 x2. (mksch A B$(a_s @@ z)$x$y) = (x1 @@ (mksch A B$z$x2$y)) &
- Forall (%x. x:act A & x~:act B) x1 &
- Finite x1 & x = (x1 @@ x2) &
+" [| Finite a_s; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>
+ ! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) a_s &
+ Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(a_s @@ z)
+ --> (? x1 x2. (mksch A B$(a_s @@ z)$x$y) = (x1 @@ (mksch A B$z$x2$y)) &
+ Forall (%x. x:act A & x~:act B) x1 &
+ Finite x1 & x = (x1 @@ x2) &
Filter (%a. a:ext A)$x1 = a_s)"
apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
apply (erule Seq_Finite_ind)
@@ -405,13 +398,13 @@
subsection "Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr"
-lemma FilterA_mksch_is_tr:
-"!! A B. [| compatible A B; compatible B A;
- is_asig(asig_of A); is_asig(asig_of B) |] ==>
- ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
- Forall (%x. x:ext (A\<parallel>B)) tr &
- Filter (%a. a:act A)$tr << Filter (%a. a:ext A)$schA &
- Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB
+lemma FilterA_mksch_is_tr:
+"!! A B. [| compatible A B; compatible B A;
+ is_asig(asig_of A); is_asig(asig_of B) |] ==>
+ ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
+ Forall (%x. x:ext (A\<parallel>B)) tr &
+ Filter (%a. a:act A)$tr << Filter (%a. a:ext A)$schA &
+ Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB
--> Filter (%a. a:ext (A\<parallel>B))$(mksch A B$tr$schA$schB) = tr"
apply (tactic \<open>Seq_induct_tac @{context} "tr"
@@ -461,13 +454,13 @@
subsection" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof"
-lemma FilterAmksch_is_schA: "!! A B. [| compatible A B; compatible B A;
- is_asig(asig_of A); is_asig(asig_of B) |] ==>
- Forall (%x. x:ext (A\<parallel>B)) tr &
- Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
- Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &
- Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &
- LastActExtsch A schA & LastActExtsch B schB
+lemma FilterAmksch_is_schA: "!! A B. [| compatible A B; compatible B A;
+ is_asig(asig_of A); is_asig(asig_of B) |] ==>
+ Forall (%x. x:ext (A\<parallel>B)) tr &
+ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
+ Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &
+ Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &
+ LastActExtsch A schA & LastActExtsch B schB
--> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA"
apply (intro strip)
apply (rule seq.take_lemma)
@@ -681,13 +674,13 @@
subsection" Filter of mksch(tr,schA,schB) to B is schB -- take lemma proof"
-lemma FilterBmksch_is_schB: "!! A B. [| compatible A B; compatible B A;
- is_asig(asig_of A); is_asig(asig_of B) |] ==>
- Forall (%x. x:ext (A\<parallel>B)) tr &
- Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
- Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &
- Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &
- LastActExtsch A schA & LastActExtsch B schB
+lemma FilterBmksch_is_schB: "!! A B. [| compatible A B; compatible B A;
+ is_asig(asig_of A); is_asig(asig_of B) |] ==>
+ Forall (%x. x:ext (A\<parallel>B)) tr &
+ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &
+ Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &
+ Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &
+ LastActExtsch A schA & LastActExtsch B schB
--> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB"
apply (intro strip)
apply (rule seq.take_lemma)
@@ -897,12 +890,12 @@
subsection "COMPOSITIONALITY on TRACE Level -- Main Theorem"
-lemma compositionality_tr:
-"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;
- is_asig(asig_of A); is_asig(asig_of B)|]
- ==> (tr: traces(A\<parallel>B)) =
- (Filter (%a. a:act A)$tr : traces A &
- Filter (%a. a:act B)$tr : traces B &
+lemma compositionality_tr:
+"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;
+ is_asig(asig_of A); is_asig(asig_of B)|]
+ ==> (tr: traces(A\<parallel>B)) =
+ (Filter (%a. a:act A)$tr : traces A &
+ Filter (%a. a:act B)$tr : traces B &
Forall (%x. x:ext(A\<parallel>B)) tr)"
apply (simp (no_asm) add: traces_def has_trace_def)
@@ -957,10 +950,10 @@
subsection \<open>COMPOSITIONALITY on TRACE Level -- for Modules\<close>
-lemma compositionality_tr_modules:
+lemma compositionality_tr_modules:
-"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;
- is_asig(asig_of A); is_asig(asig_of B)|]
+"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;
+ is_asig(asig_of A); is_asig(asig_of B)|]
==> Traces (A\<parallel>B) = par_traces (Traces A) (Traces B)"
apply (unfold Traces_def par_traces_def)
--- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy Wed Dec 30 22:09:44 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy Thu Dec 31 00:07:42 2015 +0100
@@ -10,38 +10,24 @@
default_sort type
-type_synonym
- 'a predicate = "'a => bool"
-
-consts
-
-satisfies ::"'a => 'a predicate => bool" ("_ \<Turnstile> _" [100,9] 8)
-valid ::"'a predicate => bool" (* ("|-") *)
+type_synonym 'a predicate = "'a \<Rightarrow> bool"
-NOT ::"'a predicate => 'a predicate" ("\<^bold>\<not> _" [40] 40)
-AND ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<^bold>\<and>" 35)
-OR ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<^bold>\<or>" 30)
-IMPLIES ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<^bold>\<longrightarrow>" 25)
+definition satisfies :: "'a \<Rightarrow> 'a predicate \<Rightarrow> bool" ("_ \<Turnstile> _" [100,9] 8)
+ where "(s \<Turnstile> P) \<longleftrightarrow> P s"
-
-defs
+definition valid :: "'a predicate \<Rightarrow> bool" (* ("|-") *)
+ where "valid P \<longleftrightarrow> (\<forall>s. (s \<Turnstile> P))"
-satisfies_def:
- "s \<Turnstile> P == P s"
+definition NOT :: "'a predicate \<Rightarrow> 'a predicate" ("\<^bold>\<not> _" [40] 40)
+ where "NOT P s \<longleftrightarrow> ~ (P s)"
-valid_def:
- "valid P == (! s. (s \<Turnstile> P))"
-
-NOT_def:
- "NOT P s == ~ (P s)"
+definition AND :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate" (infixr "\<^bold>\<and>" 35)
+ where "(P \<^bold>\<and> Q) s \<longleftrightarrow> P s \<and> Q s"
-AND_def:
- "(P \<^bold>\<and> Q) s == (P s) & (Q s)"
+definition OR :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate" (infixr "\<^bold>\<or>" 30)
+ where "(P \<^bold>\<or> Q) s \<longleftrightarrow> P s \<or> Q s"
-OR_def:
- "(P \<^bold>\<or> Q) s == (P s) | (Q s)"
-
-IMPLIES_def:
- "(P \<^bold>\<longrightarrow> Q) s == (P s) --> (Q s)"
+definition IMPLIES :: "'a predicate \<Rightarrow> 'a predicate \<Rightarrow> 'a predicate" (infixr "\<^bold>\<longrightarrow>" 25)
+ where "(P \<^bold>\<longrightarrow> Q) s \<longleftrightarrow> P s \<longrightarrow> Q s"
end
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Wed Dec 30 22:09:44 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Thu Dec 31 00:07:42 2015 +0100
@@ -12,55 +12,30 @@
type_synonym 'a Seq = "'a lift seq"
-consts
+definition Consq :: "'a \<Rightarrow> 'a Seq \<rightarrow> 'a Seq"
+ where "Consq a = (LAM s. Def a ## s)"
+
+definition Filter :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq"
+ where "Filter P = sfilter $ (flift2 P)"
- Consq ::"'a => 'a Seq -> 'a Seq"
- Filter ::"('a => bool) => 'a Seq -> 'a Seq"
- Map ::"('a => 'b) => 'a Seq -> 'b Seq"
- Forall ::"('a => bool) => 'a Seq => bool"
- Last ::"'a Seq -> 'a lift"
- Dropwhile ::"('a => bool) => 'a Seq -> 'a Seq"
- Takewhile ::"('a => bool) => 'a Seq -> 'a Seq"
- Zip ::"'a Seq -> 'b Seq -> ('a * 'b) Seq"
- Flat ::"('a Seq) seq -> 'a Seq"
+definition Map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a Seq \<rightarrow> 'b Seq"
+ where "Map f = smap $ (flift2 f)"
- Filter2 ::"('a => bool) => 'a Seq -> 'a Seq"
-
-abbreviation
- Consq_syn ("(_/\<leadsto>_)" [66,65] 65) where
- "a\<leadsto>s == Consq a$s"
-
+definition Forall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> bool"
+ where "Forall P = sforall (flift2 P)"
-(* list Enumeration *)
-syntax
- "_totlist" :: "args => 'a Seq" ("[(_)!]")
- "_partlist" :: "args => 'a Seq" ("[(_)?]")
-translations
- "[x, xs!]" == "x\<leadsto>[xs!]"
- "[x!]" == "x\<leadsto>nil"
- "[x, xs?]" == "x\<leadsto>[xs?]"
- "[x?]" == "x\<leadsto>CONST bottom"
+definition Last :: "'a Seq \<rightarrow> 'a lift"
+ where "Last = slast"
-defs
-
-Consq_def: "Consq a == LAM s. Def a ## s"
+definition Dropwhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq"
+ where "Dropwhile P = sdropwhile $ (flift2 P)"
-Filter_def: "Filter P == sfilter$(flift2 P)"
-
-Map_def: "Map f == smap$(flift2 f)"
-
-Forall_def: "Forall P == sforall (flift2 P)"
-
-Last_def: "Last == slast"
+definition Takewhile :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq"
+ where "Takewhile P = stakewhile $ (flift2 P)"
-Dropwhile_def: "Dropwhile P == sdropwhile$(flift2 P)"
-
-Takewhile_def: "Takewhile P == stakewhile$(flift2 P)"
-
-Flat_def: "Flat == sflat"
-
-Zip_def:
- "Zip == (fix$(LAM h t1 t2. case t1 of
+definition Zip :: "'a Seq \<rightarrow> 'b Seq \<rightarrow> ('a * 'b) Seq"
+where
+ "Zip = (fix$(LAM h t1 t2. case t1 of
nil => nil
| x##xs => (case t2 of
nil => UU
@@ -70,160 +45,181 @@
UU => UU
| Def b => Def (a,b)##(h$xs$ys))))))"
-Filter2_def: "Filter2 P == (fix$(LAM h t. case t of
- nil => nil
- | x##xs => (case x of UU => UU | Def y => (if P y
+definition Flat :: "'a Seq seq \<rightarrow> 'a Seq"
+ where "Flat = sflat"
+
+definition Filter2 :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<rightarrow> 'a Seq"
+where
+ "Filter2 P = (fix $ (LAM h t. case t of
+ nil \<Rightarrow> nil
+ | x##xs \<Rightarrow> (case x of UU \<Rightarrow> UU | Def y \<Rightarrow> (if P y
then x##(h$xs)
else h$xs))))"
+abbreviation Consq_syn ("(_/\<leadsto>_)" [66,65] 65)
+ where "a\<leadsto>s \<equiv> Consq a $ s"
+
+
+text \<open>List enumeration\<close>
+syntax
+ "_totlist" :: "args => 'a Seq" ("[(_)!]")
+ "_partlist" :: "args => 'a Seq" ("[(_)?]")
+translations
+ "[x, xs!]" == "x\<leadsto>[xs!]"
+ "[x!]" == "x\<leadsto>nil"
+ "[x, xs?]" == "x\<leadsto>[xs?]"
+ "[x?]" == "x\<leadsto>CONST bottom"
+
+
declare andalso_and [simp]
declare andalso_or [simp]
+
subsection "recursive equations of operators"
subsubsection "Map"
lemma Map_UU: "Map f$UU =UU"
-by (simp add: Map_def)
+ by (simp add: Map_def)
lemma Map_nil: "Map f$nil =nil"
-by (simp add: Map_def)
+ by (simp add: Map_def)
lemma Map_cons: "Map f$(x\<leadsto>xs)=(f x) \<leadsto> Map f$xs"
-by (simp add: Map_def Consq_def flift2_def)
+ by (simp add: Map_def Consq_def flift2_def)
subsubsection \<open>Filter\<close>
lemma Filter_UU: "Filter P$UU =UU"
-by (simp add: Filter_def)
+ by (simp add: Filter_def)
lemma Filter_nil: "Filter P$nil =nil"
-by (simp add: Filter_def)
+ by (simp add: Filter_def)
lemma Filter_cons:
"Filter P$(x\<leadsto>xs)= (if P x then x\<leadsto>(Filter P$xs) else Filter P$xs)"
-by (simp add: Filter_def Consq_def flift2_def If_and_if)
+ by (simp add: Filter_def Consq_def flift2_def If_and_if)
subsubsection \<open>Forall\<close>
lemma Forall_UU: "Forall P UU"
-by (simp add: Forall_def sforall_def)
+ by (simp add: Forall_def sforall_def)
lemma Forall_nil: "Forall P nil"
-by (simp add: Forall_def sforall_def)
+ by (simp add: Forall_def sforall_def)
lemma Forall_cons: "Forall P (x\<leadsto>xs)= (P x & Forall P xs)"
-by (simp add: Forall_def sforall_def Consq_def flift2_def)
+ by (simp add: Forall_def sforall_def Consq_def flift2_def)
subsubsection \<open>Conc\<close>
lemma Conc_cons: "(x\<leadsto>xs) @@ y = x\<leadsto>(xs @@y)"
-by (simp add: Consq_def)
+ by (simp add: Consq_def)
subsubsection \<open>Takewhile\<close>
lemma Takewhile_UU: "Takewhile P$UU =UU"
-by (simp add: Takewhile_def)
+ by (simp add: Takewhile_def)
lemma Takewhile_nil: "Takewhile P$nil =nil"
-by (simp add: Takewhile_def)
+ by (simp add: Takewhile_def)
lemma Takewhile_cons:
"Takewhile P$(x\<leadsto>xs)= (if P x then x\<leadsto>(Takewhile P$xs) else nil)"
-by (simp add: Takewhile_def Consq_def flift2_def If_and_if)
+ by (simp add: Takewhile_def Consq_def flift2_def If_and_if)
subsubsection \<open>DropWhile\<close>
lemma Dropwhile_UU: "Dropwhile P$UU =UU"
-by (simp add: Dropwhile_def)
+ by (simp add: Dropwhile_def)
lemma Dropwhile_nil: "Dropwhile P$nil =nil"
-by (simp add: Dropwhile_def)
+ by (simp add: Dropwhile_def)
lemma Dropwhile_cons:
"Dropwhile P$(x\<leadsto>xs)= (if P x then Dropwhile P$xs else x\<leadsto>xs)"
-by (simp add: Dropwhile_def Consq_def flift2_def If_and_if)
+ by (simp add: Dropwhile_def Consq_def flift2_def If_and_if)
subsubsection \<open>Last\<close>
lemma Last_UU: "Last$UU =UU"
-by (simp add: Last_def)
+ by (simp add: Last_def)
lemma Last_nil: "Last$nil =UU"
-by (simp add: Last_def)
+ by (simp add: Last_def)
lemma Last_cons: "Last$(x\<leadsto>xs)= (if xs=nil then Def x else Last$xs)"
-apply (simp add: Last_def Consq_def)
-apply (cases xs)
-apply simp_all
-done
+ apply (simp add: Last_def Consq_def)
+ apply (cases xs)
+ apply simp_all
+ done
subsubsection \<open>Flat\<close>
lemma Flat_UU: "Flat$UU =UU"
-by (simp add: Flat_def)
+ by (simp add: Flat_def)
lemma Flat_nil: "Flat$nil =nil"
-by (simp add: Flat_def)
+ by (simp add: Flat_def)
lemma Flat_cons: "Flat$(x##xs)= x @@ (Flat$xs)"
-by (simp add: Flat_def Consq_def)
+ by (simp add: Flat_def Consq_def)
subsubsection \<open>Zip\<close>
lemma Zip_unfold:
-"Zip = (LAM t1 t2. case t1 of
- nil => nil
- | x##xs => (case t2 of
- nil => UU
- | y##ys => (case x of
- UU => UU
- | Def a => (case y of
- UU => UU
- | Def b => Def (a,b)##(Zip$xs$ys)))))"
-apply (rule trans)
-apply (rule fix_eq2)
-apply (rule Zip_def)
-apply (rule beta_cfun)
-apply simp
-done
+ "Zip = (LAM t1 t2. case t1 of
+ nil => nil
+ | x##xs => (case t2 of
+ nil => UU
+ | y##ys => (case x of
+ UU => UU
+ | Def a => (case y of
+ UU => UU
+ | Def b => Def (a,b)##(Zip$xs$ys)))))"
+ apply (rule trans)
+ apply (rule fix_eq4)
+ apply (rule Zip_def)
+ apply (rule beta_cfun)
+ apply simp
+ done
lemma Zip_UU1: "Zip$UU$y =UU"
-apply (subst Zip_unfold)
-apply simp
-done
+ apply (subst Zip_unfold)
+ apply simp
+ done
lemma Zip_UU2: "x~=nil ==> Zip$x$UU =UU"
-apply (subst Zip_unfold)
-apply simp
-apply (cases x)
-apply simp_all
-done
+ apply (subst Zip_unfold)
+ apply simp
+ apply (cases x)
+ apply simp_all
+ done
lemma Zip_nil: "Zip$nil$y =nil"
-apply (subst Zip_unfold)
-apply simp
-done
+ apply (subst Zip_unfold)
+ apply simp
+ done
lemma Zip_cons_nil: "Zip$(x\<leadsto>xs)$nil= UU"
-apply (subst Zip_unfold)
-apply (simp add: Consq_def)
-done
+ apply (subst Zip_unfold)
+ apply (simp add: Consq_def)
+ done
lemma Zip_cons: "Zip$(x\<leadsto>xs)$(y\<leadsto>ys)= (x,y) \<leadsto> Zip$xs$ys"
-apply (rule trans)
-apply (subst Zip_unfold)
-apply simp
-apply (simp add: Consq_def)
-done
+ apply (rule trans)
+ apply (subst Zip_unfold)
+ apply simp
+ apply (simp add: Consq_def)
+ done
lemmas [simp del] =
sfilter_UU sfilter_nil sfilter_cons
@@ -250,26 +246,24 @@
section "Cons"
lemma Consq_def2: "a\<leadsto>s = (Def a)##s"
-apply (simp add: Consq_def)
-done
+ by (simp add: Consq_def)
lemma Seq_exhaust: "x = UU | x = nil | (? a s. x = a \<leadsto> s)"
-apply (simp add: Consq_def2)
-apply (cut_tac seq.nchotomy)
-apply (fast dest: not_Undef_is_Def [THEN iffD1])
-done
+ apply (simp add: Consq_def2)
+ apply (cut_tac seq.nchotomy)
+ apply (fast dest: not_Undef_is_Def [THEN iffD1])
+ done
-lemma Seq_cases:
-"!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a \<leadsto> s ==> P |] ==> P"
-apply (cut_tac x="x" in Seq_exhaust)
-apply (erule disjE)
-apply simp
-apply (erule disjE)
-apply simp
-apply (erule exE)+
-apply simp
-done
+lemma Seq_cases: "!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a \<leadsto> s ==> P |] ==> P"
+ apply (cut_tac x="x" in Seq_exhaust)
+ apply (erule disjE)
+ apply simp
+ apply (erule disjE)
+ apply simp
+ apply (erule exE)+
+ apply simp
+ done
(*
fun Seq_case_tac s i = rule_tac x",s)] Seq_cases i
@@ -283,42 +277,37 @@
*)
lemma Cons_not_UU: "a\<leadsto>s ~= UU"
-apply (subst Consq_def2)
-apply simp
-done
+ apply (subst Consq_def2)
+ apply simp
+ done
lemma Cons_not_less_UU: "~(a\<leadsto>x) << UU"
-apply (rule notI)
-apply (drule below_antisym)
-apply simp
-apply (simp add: Cons_not_UU)
-done
+ apply (rule notI)
+ apply (drule below_antisym)
+ apply simp
+ apply (simp add: Cons_not_UU)
+ done
lemma Cons_not_less_nil: "~a\<leadsto>s << nil"
-apply (simp add: Consq_def2)
-done
+ by (simp add: Consq_def2)
lemma Cons_not_nil: "a\<leadsto>s ~= nil"
-apply (simp add: Consq_def2)
-done
+ by (simp add: Consq_def2)
lemma Cons_not_nil2: "nil ~= a\<leadsto>s"
-apply (simp add: Consq_def2)
-done
+ by (simp add: Consq_def2)
lemma Cons_inject_eq: "(a\<leadsto>s = b\<leadsto>t) = (a = b & s = t)"
-apply (simp only: Consq_def2)
-apply (simp add: scons_inject_eq)
-done
+ apply (simp only: Consq_def2)
+ apply (simp add: scons_inject_eq)
+ done
lemma Cons_inject_less_eq: "(a\<leadsto>s<<b\<leadsto>t) = (a = b & s<<t)"
-apply (simp add: Consq_def2)
-done
+ by (simp add: Consq_def2)
lemma seq_take_Cons: "seq_take (Suc n)$(a\<leadsto>x) = a\<leadsto> (seq_take n$x)"
-apply (simp add: Consq_def)
-done
+ by (simp add: Consq_def)
lemmas [simp] =
Cons_not_nil2 Cons_inject_eq Cons_inject_less_eq seq_take_Cons
@@ -327,27 +316,26 @@
subsection "induction"
-lemma Seq_induct:
-"!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a\<leadsto>s)|] ==> P x"
-apply (erule (2) seq.induct)
-apply defined
-apply (simp add: Consq_def)
-done
+lemma Seq_induct: "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a\<leadsto>s)|] ==> P x"
+ apply (erule (2) seq.induct)
+ apply defined
+ apply (simp add: Consq_def)
+ done
lemma Seq_FinitePartial_ind:
-"!! P.[|P UU;P nil; !! a s. P s ==> P(a\<leadsto>s) |]
- ==> seq_finite x --> P x"
-apply (erule (1) seq_finite_ind)
-apply defined
-apply (simp add: Consq_def)
-done
+ "!! P.[|P UU;P nil; !! a s. P s ==> P(a\<leadsto>s) |]
+ ==> seq_finite x --> P x"
+ apply (erule (1) seq_finite_ind)
+ apply defined
+ apply (simp add: Consq_def)
+ done
lemma Seq_Finite_ind:
-"!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a\<leadsto>s) |] ==> P x"
-apply (erule (1) Finite.induct)
-apply defined
-apply (simp add: Consq_def)
-done
+ "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a\<leadsto>s) |] ==> P x"
+ apply (erule (1) Finite.induct)
+ apply defined
+ apply (simp add: Consq_def)
+ done
(* rws are definitions to be unfolded for admissibility check *)
@@ -377,70 +365,69 @@
subsection "HD,TL"
lemma HD_Cons [simp]: "HD$(x\<leadsto>y) = Def x"
-apply (simp add: Consq_def)
-done
+ by (simp add: Consq_def)
lemma TL_Cons [simp]: "TL$(x\<leadsto>y) = y"
-apply (simp add: Consq_def)
-done
+ by (simp add: Consq_def)
(* ------------------------------------------------------------------------------------ *)
subsection "Finite, Partial, Infinite"
lemma Finite_Cons [simp]: "Finite (a\<leadsto>xs) = Finite xs"
-apply (simp add: Consq_def2 Finite_cons)
-done
+ by (simp add: Consq_def2 Finite_cons)
lemma FiniteConc_1: "Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)"
-apply (erule Seq_Finite_ind, simp_all)
-done
+ apply (erule Seq_Finite_ind)
+ apply simp_all
+ done
-lemma FiniteConc_2:
-"Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)"
-apply (erule Seq_Finite_ind)
-(* nil*)
-apply (intro strip)
-apply (rule_tac x="x" in Seq_cases, simp_all)
-(* cons *)
-apply (intro strip)
-apply (rule_tac x="x" in Seq_cases, simp_all)
-apply (rule_tac x="y" in Seq_cases, simp_all)
-done
+lemma FiniteConc_2: "Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)"
+ apply (erule Seq_Finite_ind)
+ (* nil*)
+ apply (intro strip)
+ apply (rule_tac x="x" in Seq_cases, simp_all)
+ (* cons *)
+ apply (intro strip)
+ apply (rule_tac x="x" in Seq_cases, simp_all)
+ apply (rule_tac x="y" in Seq_cases, simp_all)
+ done
lemma FiniteConc [simp]: "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)"
-apply (rule iffI)
-apply (erule FiniteConc_2 [rule_format])
-apply (rule refl)
-apply (rule FiniteConc_1 [rule_format])
-apply auto
-done
+ apply (rule iffI)
+ apply (erule FiniteConc_2 [rule_format])
+ apply (rule refl)
+ apply (rule FiniteConc_1 [rule_format])
+ apply auto
+ done
lemma FiniteMap1: "Finite s ==> Finite (Map f$s)"
-apply (erule Seq_Finite_ind, simp_all)
-done
+ apply (erule Seq_Finite_ind)
+ apply simp_all
+ done
lemma FiniteMap2: "Finite s ==> ! t. (s = Map f$t) --> Finite t"
-apply (erule Seq_Finite_ind)
-apply (intro strip)
-apply (rule_tac x="t" in Seq_cases, simp_all)
-(* main case *)
-apply auto
-apply (rule_tac x="t" in Seq_cases, simp_all)
-done
+ apply (erule Seq_Finite_ind)
+ apply (intro strip)
+ apply (rule_tac x="t" in Seq_cases, simp_all)
+ (* main case *)
+ apply auto
+ apply (rule_tac x="t" in Seq_cases, simp_all)
+ done
lemma Map2Finite: "Finite (Map f$s) = Finite s"
-apply auto
-apply (erule FiniteMap2 [rule_format])
-apply (rule refl)
-apply (erule FiniteMap1)
-done
+ apply auto
+ apply (erule FiniteMap2 [rule_format])
+ apply (rule refl)
+ apply (erule FiniteMap1)
+ done
lemma FiniteFilter: "Finite s ==> Finite (Filter P$s)"
-apply (erule Seq_Finite_ind, simp_all)
-done
+ apply (erule Seq_Finite_ind)
+ apply simp_all
+ done
(* ----------------------------------------------------------------------------------- *)
@@ -448,32 +435,34 @@
subsection "Conc"
lemma Conc_cong: "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)"
-apply (erule Seq_Finite_ind, simp_all)
-done
+ apply (erule Seq_Finite_ind)
+ apply simp_all
+ done
lemma Conc_assoc: "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z"
-apply (rule_tac x="x" in Seq_induct, simp_all)
-done
+ apply (rule_tac x="x" in Seq_induct)
+ apply simp_all
+ done
lemma nilConc [simp]: "s@@ nil = s"
-apply (induct s)
-apply simp
-apply simp
-apply simp
-apply simp
-done
+ apply (induct s)
+ apply simp
+ apply simp
+ apply simp
+ apply simp
+ done
(* should be same as nil_is_Conc2 when all nils are turned to right side !! *)
lemma nil_is_Conc: "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)"
-apply (rule_tac x="x" in Seq_cases)
-apply auto
-done
+ apply (rule_tac x="x" in Seq_cases)
+ apply auto
+ done
lemma nil_is_Conc2: "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)"
-apply (rule_tac x="x" in Seq_cases)
-apply auto
-done
+ apply (rule_tac x="x" in Seq_cases)
+ apply auto
+ done
(* ------------------------------------------------------------------------------------ *)
@@ -481,13 +470,13 @@
subsection "Last"
lemma Finite_Last1: "Finite s ==> s~=nil --> Last$s~=UU"
-apply (erule Seq_Finite_ind, simp_all)
-done
+ apply (erule Seq_Finite_ind, simp_all)
+ done
lemma Finite_Last2: "Finite s ==> Last$s=UU --> s=nil"
-apply (erule Seq_Finite_ind, simp_all)
-apply fast
-done
+ apply (erule Seq_Finite_ind, simp_all)
+ apply fast
+ done
(* ------------------------------------------------------------------------------------ *)
@@ -497,39 +486,39 @@
lemma FilterPQ: "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"
-apply (rule_tac x="s" in Seq_induct, simp_all)
-done
+ apply (rule_tac x="s" in Seq_induct, simp_all)
+ done
lemma FilterConc: "Filter P$(x @@ y) = (Filter P$x @@ Filter P$y)"
-apply (simp add: Filter_def sfiltersconc)
-done
+ apply (simp add: Filter_def sfiltersconc)
+ done
(* ------------------------------------------------------------------------------------ *)
subsection "Map"
lemma MapMap: "Map f$(Map g$s) = Map (f o g)$s"
-apply (rule_tac x="s" in Seq_induct, simp_all)
-done
+ apply (rule_tac x="s" in Seq_induct, simp_all)
+ done
lemma MapConc: "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"
-apply (rule_tac x="x" in Seq_induct, simp_all)
-done
+ apply (rule_tac x="x" in Seq_induct, simp_all)
+ done
lemma MapFilter: "Filter P$(Map f$x) = Map f$(Filter (P o f)$x)"
-apply (rule_tac x="x" in Seq_induct, simp_all)
-done
+ apply (rule_tac x="x" in Seq_induct, simp_all)
+ done
lemma nilMap: "nil = (Map f$s) --> s= nil"
-apply (rule_tac x="s" in Seq_cases, simp_all)
-done
+ apply (rule_tac x="s" in Seq_cases, simp_all)
+ done
lemma ForallMap: "Forall P (Map f$s) = Forall (P o f) s"
-apply (rule_tac x="s" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+ apply (rule_tac x="s" in Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
@@ -538,41 +527,39 @@
subsection "Forall"
-
-lemma ForallPForallQ1: "Forall P ys & (! x. P x --> Q x)
- --> Forall Q ys"
-apply (rule_tac x="ys" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+lemma ForallPForallQ1: "Forall P ys & (! x. P x --> Q x) --> Forall Q ys"
+ apply (rule_tac x="ys" in Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
lemmas ForallPForallQ =
ForallPForallQ1 [THEN mp, OF conjI, OF _ allI, OF _ impI]
lemma Forall_Conc_impl: "(Forall P x & Forall P y) --> Forall P (x @@ y)"
-apply (rule_tac x="x" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+ apply (rule_tac x="x" in Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
lemma Forall_Conc [simp]:
"Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)"
-apply (erule Seq_Finite_ind, simp_all)
-done
+ apply (erule Seq_Finite_ind, simp_all)
+ done
lemma ForallTL1: "Forall P s --> Forall P (TL$s)"
-apply (rule_tac x="s" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+ apply (rule_tac x="s" in Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
lemmas ForallTL = ForallTL1 [THEN mp]
lemma ForallDropwhile1: "Forall P s --> Forall P (Dropwhile Q$s)"
-apply (rule_tac x="s" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+ apply (rule_tac x="s" in Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
lemmas ForallDropwhile = ForallDropwhile1 [THEN mp]
@@ -580,29 +567,27 @@
(* only admissible in t, not if done in s *)
lemma Forall_prefix: "! s. Forall P s --> t<<s --> Forall P t"
-apply (rule_tac x="t" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-apply (intro strip)
-apply (rule_tac x="sa" in Seq_cases)
-apply simp
-apply auto
-done
+ apply (rule_tac x="t" in Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ apply (intro strip)
+ apply (rule_tac x="sa" in Seq_cases)
+ apply simp
+ apply auto
+ done
lemmas Forall_prefixclosed = Forall_prefix [rule_format]
-lemma Forall_postfixclosed:
- "[| Finite h; Forall P s; s= h @@ t |] ==> Forall P t"
-apply auto
-done
+lemma Forall_postfixclosed: "[| Finite h; Forall P s; s= h @@ t |] ==> Forall P t"
+ by auto
lemma ForallPFilterQR1:
"((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q$tr = Filter R$tr"
-apply (rule_tac x="tr" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+ apply (rule_tac x="tr" in Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
lemmas ForallPFilterQR = ForallPFilterQR1 [THEN mp, OF conjI, OF allI]
@@ -613,15 +598,14 @@
lemma ForallPFilterP: "Forall P (Filter P$x)"
-apply (simp add: Filter_def Forall_def forallPsfilterP)
-done
+ by (simp add: Filter_def Forall_def forallPsfilterP)
(* holds also in other direction, then equal to forallPfilterP *)
lemma ForallPFilterPid1: "Forall P x --> Filter P$x = x"
-apply (rule_tac x="x" in Seq_induct)
-apply (simp add: Forall_def sforall_def Filter_def)
-apply simp_all
-done
+ apply (rule_tac x="x" in Seq_induct)
+ apply (simp add: Forall_def sforall_def Filter_def)
+ apply simp_all
+ done
lemmas ForallPFilterPid = ForallPFilterPid1 [THEN mp]
@@ -629,19 +613,18 @@
(* holds also in other direction *)
lemma ForallnPFilterPnil1: "!! ys . Finite ys ==>
Forall (%x. ~P x) ys --> Filter P$ys = nil "
-apply (erule Seq_Finite_ind, simp_all)
-done
+ apply (erule Seq_Finite_ind, simp_all)
+ done
lemmas ForallnPFilterPnil = ForallnPFilterPnil1 [THEN mp]
(* holds also in other direction *)
-lemma ForallnPFilterPUU1: "~Finite ys & Forall (%x. ~P x) ys
- --> Filter P$ys = UU "
-apply (rule_tac x="ys" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+lemma ForallnPFilterPUU1: "~Finite ys & Forall (%x. ~P x) ys --> Filter P$ys = UU"
+ apply (rule_tac x="ys" in Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
lemmas ForallnPFilterPUU = ForallnPFilterPUU1 [THEN mp, OF conjI]
@@ -650,15 +633,15 @@
lemma FilternPnilForallP [rule_format]: "Filter P$ys = nil -->
(Forall (%x. ~P x) ys & Finite ys)"
-apply (rule_tac x="ys" in Seq_induct)
-(* adm *)
-apply (simp add: Forall_def sforall_def)
-(* base cases *)
-apply simp
-apply simp
-(* main case *)
-apply simp
-done
+ apply (rule_tac x="ys" in Seq_induct)
+ (* adm *)
+ apply (simp add: Forall_def sforall_def)
+ (* base cases *)
+ apply simp
+ apply simp
+ (* main case *)
+ apply simp
+ done
(* inverse of ForallnPFilterPUU *)
@@ -691,18 +674,18 @@
lemma ForallQFilterPnil:
"!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|]
==> Filter P$ys = nil"
-apply (erule ForallnPFilterPnil)
-apply (erule ForallPForallQ)
-apply auto
-done
+ apply (erule ForallnPFilterPnil)
+ apply (erule ForallPForallQ)
+ apply auto
+ done
lemma ForallQFilterPUU:
"!! Q P. [| ~Finite ys; Forall Q ys; !!x. Q x ==> ~P x|]
==> Filter P$ys = UU "
-apply (erule ForallnPFilterPUU)
-apply (erule ForallPForallQ)
-apply auto
-done
+ apply (erule ForallnPFilterPUU)
+ apply (erule ForallPForallQ)
+ apply auto
+ done
@@ -712,71 +695,65 @@
lemma ForallPTakewhileP [simp]: "Forall P (Takewhile P$x)"
-apply (simp add: Forall_def Takewhile_def sforallPstakewhileP)
-done
+ by (simp add: Forall_def Takewhile_def sforallPstakewhileP)
-lemma ForallPTakewhileQ [simp]:
-"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q$x)"
-apply (rule ForallPForallQ)
-apply (rule ForallPTakewhileP)
-apply auto
-done
+lemma ForallPTakewhileQ [simp]: "!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q$x)"
+ apply (rule ForallPForallQ)
+ apply (rule ForallPTakewhileP)
+ apply auto
+ done
lemma FilterPTakewhileQnil [simp]:
"!! Q P.[| Finite (Takewhile Q$ys); !!x. Q x ==> ~P x |]
==> Filter P$(Takewhile Q$ys) = nil"
-apply (erule ForallnPFilterPnil)
-apply (rule ForallPForallQ)
-apply (rule ForallPTakewhileP)
-apply auto
-done
+ apply (erule ForallnPFilterPnil)
+ apply (rule ForallPForallQ)
+ apply (rule ForallPTakewhileP)
+ apply auto
+ done
lemma FilterPTakewhileQid [simp]:
"!! Q P. [| !!x. Q x ==> P x |] ==>
Filter P$(Takewhile Q$ys) = (Takewhile Q$ys)"
-apply (rule ForallPFilterPid)
-apply (rule ForallPForallQ)
-apply (rule ForallPTakewhileP)
-apply auto
-done
+ apply (rule ForallPFilterPid)
+ apply (rule ForallPForallQ)
+ apply (rule ForallPTakewhileP)
+ apply auto
+ done
lemma Takewhile_idempotent: "Takewhile P$(Takewhile P$s) = Takewhile P$s"
-apply (rule_tac x="s" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+ apply (rule_tac x="s" in Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
-lemma ForallPTakewhileQnP [simp]:
- "Forall P s --> Takewhile (%x. Q x | (~P x))$s = Takewhile Q$s"
-apply (rule_tac x="s" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+lemma ForallPTakewhileQnP [simp]: "Forall P s --> Takewhile (%x. Q x | (~P x))$s = Takewhile Q$s"
+ apply (rule_tac x="s" in Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
-lemma ForallPDropwhileQnP [simp]:
- "Forall P s --> Dropwhile (%x. Q x | (~P x))$s = Dropwhile Q$s"
-apply (rule_tac x="s" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+lemma ForallPDropwhileQnP [simp]: "Forall P s --> Dropwhile (%x. Q x | (~P x))$s = Dropwhile Q$s"
+ apply (rule_tac x="s" in Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
-lemma TakewhileConc1:
- "Forall P s --> Takewhile P$(s @@ t) = s @@ (Takewhile P$t)"
-apply (rule_tac x="s" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+lemma TakewhileConc1: "Forall P s --> Takewhile P$(s @@ t) = s @@ (Takewhile P$t)"
+ apply (rule_tac x="s" in Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
lemmas TakewhileConc = TakewhileConc1 [THEN mp]
-lemma DropwhileConc1:
- "Finite s ==> Forall P s --> Dropwhile P$(s @@ t) = Dropwhile P$t"
-apply (erule Seq_Finite_ind, simp_all)
-done
+lemma DropwhileConc1: "Finite s ==> Forall P s --> Dropwhile P$(s @@ t) = Dropwhile P$t"
+ apply (erule Seq_Finite_ind, simp_all)
+ done
lemmas DropwhileConc = DropwhileConc1 [THEN mp]
@@ -786,60 +763,56 @@
subsection "coinductive characterizations of Filter"
-
lemma divide_Seq_lemma:
"HD$(Filter P$y) = Def x
--> y = ((Takewhile (%x. ~P x)$y) @@ (x \<leadsto> TL$(Dropwhile (%a. ~P a)$y)))
& Finite (Takewhile (%x. ~ P x)$y) & P x"
+ (* FIX: pay attention: is only admissible with chain-finite package to be added to
+ adm test and Finite f x admissibility *)
+ apply (rule_tac x="y" in Seq_induct)
+ apply (simp add: adm_subst [OF _ adm_Finite])
+ apply simp
+ apply simp
+ apply (case_tac "P a")
+ apply simp
+ apply blast
+ (* ~ P a *)
+ apply simp
+ done
-(* FIX: pay attention: is only admissible with chain-finite package to be added to
- adm test and Finite f x admissibility *)
-apply (rule_tac x="y" in Seq_induct)
-apply (simp add: adm_subst [OF _ adm_Finite])
-apply simp
-apply simp
-apply (case_tac "P a")
- apply simp
- apply blast
-(* ~ P a *)
-apply simp
-done
-
-lemma divide_Seq: "(x\<leadsto>xs) << Filter P$y
+lemma divide_Seq: "(x\<leadsto>xs) << Filter P$y
==> y = ((Takewhile (%a. ~ P a)$y) @@ (x \<leadsto> TL$(Dropwhile (%a. ~ P a)$y)))
& Finite (Takewhile (%a. ~ P a)$y) & P x"
-apply (rule divide_Seq_lemma [THEN mp])
-apply (drule_tac f="HD" and x="x\<leadsto>xs" in monofun_cfun_arg)
-apply simp
-done
+ apply (rule divide_Seq_lemma [THEN mp])
+ apply (drule_tac f="HD" and x="x\<leadsto>xs" in monofun_cfun_arg)
+ apply simp
+ done
-lemma nForall_HDFilter:
- "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)"
-unfolding not_Undef_is_Def [symmetric]
-apply (induct y rule: Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+lemma nForall_HDFilter: "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)"
+ unfolding not_Undef_is_Def [symmetric]
+ apply (induct y rule: Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
lemma divide_Seq2: "~Forall P y
==> ? x. y= (Takewhile P$y @@ (x \<leadsto> TL$(Dropwhile P$y))) &
Finite (Takewhile P$y) & (~ P x)"
-apply (drule nForall_HDFilter [THEN mp])
-apply safe
-apply (rule_tac x="x" in exI)
-apply (cut_tac P1="%x. ~ P x" in divide_Seq_lemma [THEN mp])
-apply auto
-done
+ apply (drule nForall_HDFilter [THEN mp])
+ apply safe
+ apply (rule_tac x="x" in exI)
+ apply (cut_tac P1="%x. ~ P x" in divide_Seq_lemma [THEN mp])
+ apply auto
+ done
lemma divide_Seq3: "~Forall P y
==> ? x bs rs. y= (bs @@ (x\<leadsto>rs)) & Finite bs & Forall P bs & (~ P x)"
-apply (drule divide_Seq2)
-(*Auto_tac no longer proves it*)
-apply fastforce
-done
+ apply (drule divide_Seq2)
+ apply fastforce
+ done
lemmas [simp] = FilterPQ FilterConc Conc_cong
@@ -850,84 +823,82 @@
subsection "take_lemma"
lemma seq_take_lemma: "(!n. seq_take n$x = seq_take n$x') = (x = x')"
-apply (rule iffI)
-apply (rule seq.take_lemma)
-apply auto
-done
+ apply (rule iffI)
+ apply (rule seq.take_lemma)
+ apply auto
+ done
lemma take_reduction1:
-" ! n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2)
+ "\<forall>n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2)
--> seq_take n$(x @@ (t\<leadsto>y1)) = seq_take n$(x @@ (t\<leadsto>y2)))"
-apply (rule_tac x="x" in Seq_induct)
-apply simp_all
-apply (intro strip)
-apply (case_tac "n")
-apply auto
-apply (case_tac "n")
-apply auto
-done
+ apply (rule_tac x="x" in Seq_induct)
+ apply simp_all
+ apply (intro strip)
+ apply (case_tac "n")
+ apply auto
+ apply (case_tac "n")
+ apply auto
+ done
lemma take_reduction:
- "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k$y1 = seq_take k$y2|]
- ==> seq_take n$(x @@ (s\<leadsto>y1)) = seq_take n$(y @@ (t\<leadsto>y2))"
-apply (auto intro!: take_reduction1 [rule_format])
-done
+ "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k$y1 = seq_take k$y2|]
+ ==> seq_take n$(x @@ (s\<leadsto>y1)) = seq_take n$(y @@ (t\<leadsto>y2))"
+ by (auto intro!: take_reduction1 [rule_format])
(* ------------------------------------------------------------------
take-lemma and take_reduction for << instead of =
------------------------------------------------------------------ *)
lemma take_reduction_less1:
-" ! n. ((! k. k < n --> seq_take k$y1 << seq_take k$y2)
+ "\<forall>n. ((! k. k < n --> seq_take k$y1 << seq_take k$y2)
--> seq_take n$(x @@ (t\<leadsto>y1)) << seq_take n$(x @@ (t\<leadsto>y2)))"
-apply (rule_tac x="x" in Seq_induct)
-apply simp_all
-apply (intro strip)
-apply (case_tac "n")
-apply auto
-apply (case_tac "n")
-apply auto
-done
+ apply (rule_tac x="x" in Seq_induct)
+ apply simp_all
+ apply (intro strip)
+ apply (case_tac "n")
+ apply auto
+ apply (case_tac "n")
+ apply auto
+ done
lemma take_reduction_less:
- "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k$y1 << seq_take k$y2|]
- ==> seq_take n$(x @@ (s\<leadsto>y1)) << seq_take n$(y @@ (t\<leadsto>y2))"
-apply (auto intro!: take_reduction_less1 [rule_format])
-done
+ "\<And>n.[| x=y; s=t;!! k. k<n ==> seq_take k$y1 << seq_take k$y2|]
+ ==> seq_take n$(x @@ (s\<leadsto>y1)) << seq_take n$(y @@ (t\<leadsto>y2))"
+ by (auto intro!: take_reduction_less1 [rule_format])
lemma take_lemma_less1:
assumes "!! n. seq_take n$s1 << seq_take n$s2"
shows "s1<<s2"
-apply (rule_tac t="s1" in seq.reach [THEN subst])
-apply (rule_tac t="s2" in seq.reach [THEN subst])
-apply (rule lub_mono)
-apply (rule seq.chain_take [THEN ch2ch_Rep_cfunL])
-apply (rule seq.chain_take [THEN ch2ch_Rep_cfunL])
-apply (rule assms)
-done
+ apply (rule_tac t="s1" in seq.reach [THEN subst])
+ apply (rule_tac t="s2" in seq.reach [THEN subst])
+ apply (rule lub_mono)
+ apply (rule seq.chain_take [THEN ch2ch_Rep_cfunL])
+ apply (rule seq.chain_take [THEN ch2ch_Rep_cfunL])
+ apply (rule assms)
+ done
lemma take_lemma_less: "(!n. seq_take n$x << seq_take n$x') = (x << x')"
-apply (rule iffI)
-apply (rule take_lemma_less1)
-apply auto
-apply (erule monofun_cfun_arg)
-done
+ apply (rule iffI)
+ apply (rule take_lemma_less1)
+ apply auto
+ apply (erule monofun_cfun_arg)
+ done
(* ------------------------------------------------------------------
take-lemma proof principles
------------------------------------------------------------------ *)
lemma take_lemma_principle1:
- "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
+ "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
!! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y\<leadsto>s2)|]
==> (f (s1 @@ y\<leadsto>s2)) = (g (s1 @@ y\<leadsto>s2)) |]
==> A x --> (f x)=(g x)"
-apply (case_tac "Forall Q x")
-apply (auto dest!: divide_Seq3)
-done
+ apply (case_tac "Forall Q x")
+ apply (auto dest!: divide_Seq3)
+ done
lemma take_lemma_principle2:
"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
@@ -935,11 +906,11 @@
==> ! n. seq_take n$(f (s1 @@ y\<leadsto>s2))
= seq_take n$(g (s1 @@ y\<leadsto>s2)) |]
==> A x --> (f x)=(g x)"
-apply (case_tac "Forall Q x")
-apply (auto dest!: divide_Seq3)
-apply (rule seq.take_lemma)
-apply auto
-done
+ apply (case_tac "Forall Q x")
+ apply (auto dest!: divide_Seq3)
+ apply (rule seq.take_lemma)
+ apply auto
+ done
(* Note: in the following proofs the ordering of proof steps is very
@@ -957,18 +928,18 @@
==> seq_take (Suc n)$(f (s1 @@ y\<leadsto>s2))
= seq_take (Suc n)$(g (s1 @@ y\<leadsto>s2)) |]
==> A x --> (f x)=(g x)"
-apply (rule impI)
-apply (rule seq.take_lemma)
-apply (rule mp)
-prefer 2 apply assumption
-apply (rule_tac x="x" in spec)
-apply (rule nat.induct)
-apply simp
-apply (rule allI)
-apply (case_tac "Forall Q xa")
-apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec])
-apply (auto dest!: divide_Seq3)
-done
+ apply (rule impI)
+ apply (rule seq.take_lemma)
+ apply (rule mp)
+ prefer 2 apply assumption
+ apply (rule_tac x="x" in spec)
+ apply (rule nat.induct)
+ apply simp
+ apply (rule allI)
+ apply (case_tac "Forall Q xa")
+ apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec])
+ apply (auto dest!: divide_Seq3)
+ done
lemma take_lemma_less_induct:
@@ -978,17 +949,17 @@
==> seq_take n$(f (s1 @@ y\<leadsto>s2))
= seq_take n$(g (s1 @@ y\<leadsto>s2)) |]
==> A x --> (f x)=(g x)"
-apply (rule impI)
-apply (rule seq.take_lemma)
-apply (rule mp)
-prefer 2 apply assumption
-apply (rule_tac x="x" in spec)
-apply (rule nat_less_induct)
-apply (rule allI)
-apply (case_tac "Forall Q xa")
-apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec])
-apply (auto dest!: divide_Seq3)
-done
+ apply (rule impI)
+ apply (rule seq.take_lemma)
+ apply (rule mp)
+ prefer 2 apply assumption
+ apply (rule_tac x="x" in spec)
+ apply (rule nat_less_induct)
+ apply (rule allI)
+ apply (case_tac "Forall Q xa")
+ apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec])
+ apply (auto dest!: divide_Seq3)
+ done
@@ -1000,17 +971,17 @@
==> seq_take (Suc n)$(f (y\<leadsto>s))
= seq_take (Suc n)$(g (y\<leadsto>s)) |]
==> A x --> (f x)=(g x)"
-apply (rule impI)
-apply (rule seq.take_lemma)
-apply (rule mp)
-prefer 2 apply assumption
-apply (rule_tac x="x" in spec)
-apply (rule nat.induct)
-apply simp
-apply (rule allI)
-apply (rule_tac x="xa" in Seq_cases)
-apply simp_all
-done
+ apply (rule impI)
+ apply (rule seq.take_lemma)
+ apply (rule mp)
+ prefer 2 apply assumption
+ apply (rule_tac x="x" in spec)
+ apply (rule nat.induct)
+ apply simp
+ apply (rule allI)
+ apply (rule_tac x="xa" in Seq_cases)
+ apply simp_all
+ done
(* ------------------------------------------------------------------------------------ *)
@@ -1031,33 +1002,33 @@
--> Filter P$(Filter Q$s) =
Filter (%x. P x & Q x)$s"
-apply (rule_tac x="s" in Seq_induct)
-apply (simp add: Forall_def sforall_def)
-apply simp_all
-done
+ apply (rule_tac x="s" in Seq_induct)
+ apply (simp add: Forall_def sforall_def)
+ apply simp_all
+ done
lemma Filter_lemma2: "Finite s ==>
(Forall (%x. (~P x) | (~ Q x)) s
--> Filter P$(Filter Q$s) = nil)"
-apply (erule Seq_Finite_ind, simp_all)
-done
+ apply (erule Seq_Finite_ind, simp_all)
+ done
lemma Filter_lemma3: "Finite s ==>
Forall (%x. (~P x) | (~ Q x)) s
--> Filter (%x. P x & Q x)$s = nil"
-apply (erule Seq_Finite_ind, simp_all)
-done
+ apply (erule Seq_Finite_ind, simp_all)
+ done
lemma FilterPQ_takelemma: "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"
-apply (rule_tac A1="%x. True" and
- Q1="%x. ~(P x & Q x)" and x1="s" in
- take_lemma_induct [THEN mp])
-(* better support for A = %x. True *)
-apply (simp add: Filter_lemma1)
-apply (simp add: Filter_lemma2 Filter_lemma3)
-apply simp
-done
+ apply (rule_tac A1="%x. True" and
+ Q1="%x. ~(P x & Q x)" and x1="s" in
+ take_lemma_induct [THEN mp])
+ (* better support for A = %x. True *)
+ apply (simp add: Filter_lemma1)
+ apply (simp add: Filter_lemma2 Filter_lemma3)
+ apply simp
+ done
declare FilterPQ [simp]
@@ -1069,10 +1040,10 @@
lemma MapConc_takelemma: "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"
-apply (rule_tac A1="%x. True" and x1="x" in
- take_lemma_in_eq_out [THEN mp])
-apply auto
-done
+ apply (rule_tac A1="%x. True" and x1="x" in
+ take_lemma_in_eq_out [THEN mp])
+ apply auto
+ done
ML \<open>
@@ -1108,7 +1079,6 @@
THEN pair_tac ctxt "a" (i+3)
THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i+1))))
THEN simp_tac (ctxt addsimps rws) i;
-
\<close>
end
--- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed Dec 30 22:09:44 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy Thu Dec 31 00:07:42 2015 +0100
@@ -221,7 +221,7 @@
tr = Filter (%a. a:ext A)$sch &
LastActExtsch A sch"
-apply (unfold schedules_def has_schedule_def)
+apply (unfold schedules_def has_schedule_def [abs_def])
apply auto
apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI)
apply (simp add: executions_def)
--- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy Wed Dec 30 22:09:44 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy Thu Dec 31 00:07:42 2015 +0100
@@ -10,54 +10,35 @@
default_sort type
-type_synonym
- 'a temporal = "'a Seq predicate"
-
+type_synonym 'a temporal = "'a Seq predicate"
-consts
-suffix :: "'a Seq => 'a Seq => bool"
-tsuffix :: "'a Seq => 'a Seq => bool"
-
-validT :: "'a Seq predicate => bool"
-
-unlift :: "'a lift => 'a"
+definition validT :: "'a Seq predicate \<Rightarrow> bool"
+ where "validT P \<longleftrightarrow> (\<forall>s. s \<noteq> UU \<and> s \<noteq> nil \<longrightarrow> (s \<Turnstile> P))"
-Init :: "'a predicate => 'a temporal" ("\<langle>_\<rangle>" [0] 1000)
+definition unlift :: "'a lift \<Rightarrow> 'a"
+ where "unlift x = (case x of Def y \<Rightarrow> y)"
-Box :: "'a temporal => 'a temporal" ("\<box>(_)" [80] 80)
-Diamond :: "'a temporal => 'a temporal" ("\<diamond>(_)" [80] 80)
-Next :: "'a temporal => 'a temporal"
-Leadsto :: "'a temporal => 'a temporal => 'a temporal" (infixr "\<leadsto>" 22)
+definition Init :: "'a predicate \<Rightarrow> 'a temporal" ("\<langle>_\<rangle>" [0] 1000)
+ where "Init P s = P (unlift (HD $ s))"
+ \<comment> \<open>this means that for \<open>nil\<close> and \<open>UU\<close> the effect is unpredictable\<close>
-defs
-
-unlift_def:
- "unlift x == (case x of Def y => y)"
+definition Next :: "'a temporal \<Rightarrow> 'a temporal"
+ where "(Next P) s \<longleftrightarrow> (if TL $ s = UU \<or> TL $ s = nil then P s else P (TL $ s))"
-(* this means that for nil and UU the effect is unpredictable *)
-Init_def:
- "Init P s == (P (unlift (HD$s)))"
+definition suffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool"
+ where "suffix s2 s \<longleftrightarrow> (\<exists>s1. Finite s1 \<and> s = s1 @@ s2)"
-suffix_def:
- "suffix s2 s == ? s1. (Finite s1 & s = s1 @@ s2)"
-
-tsuffix_def:
- "tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s"
+definition tsuffix :: "'a Seq \<Rightarrow> 'a Seq \<Rightarrow> bool"
+ where "tsuffix s2 s \<longleftrightarrow> s2 \<noteq> nil \<and> s2 \<noteq> UU \<and> suffix s2 s"
-Box_def:
- "(\<box>P) s == ! s2. tsuffix s2 s --> P s2"
-
-Next_def:
- "(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)"
+definition Box :: "'a temporal \<Rightarrow> 'a temporal" ("\<box>(_)" [80] 80)
+ where "(\<box>P) s \<longleftrightarrow> (\<forall>s2. tsuffix s2 s \<longrightarrow> P s2)"
-Diamond_def:
- "\<diamond>P == \<^bold>\<not> (\<box>(\<^bold>\<not> P))"
+definition Diamond :: "'a temporal \<Rightarrow> 'a temporal" ("\<diamond>(_)" [80] 80)
+ where "\<diamond>P = (\<^bold>\<not> (\<box>(\<^bold>\<not> P)))"
-Leadsto_def:
- "P \<leadsto> Q == (\<box>(P \<^bold>\<longrightarrow> (\<diamond>Q)))"
-
-validT_def:
- "validT P == ! s. s~=UU & s~=nil --> (s \<Turnstile> P)"
+definition Leadsto :: "'a temporal \<Rightarrow> 'a temporal \<Rightarrow> 'a temporal" (infixr "\<leadsto>" 22)
+ where "(P \<leadsto> Q) = (\<box>(P \<^bold>\<longrightarrow> (\<diamond>Q)))"
lemma simple: "\<box>\<diamond>(\<^bold>\<not> P) = (\<^bold>\<not> \<diamond>\<box>P)"
@@ -143,7 +124,7 @@
subsection "LTL Axioms by Manna/Pnueli"
-lemma tsuffix_TL [rule_format (no_asm)]:
+lemma tsuffix_TL [rule_format (no_asm)]:
"s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s"
apply (unfold tsuffix_def suffix_def)
apply auto
@@ -155,7 +136,7 @@
lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL]
declare split_if [split del]
-lemma LTL1:
+lemma LTL1:
"s~=UU & s~=nil --> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> (F \<^bold>\<and> (Next (\<box>F))))"
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def)
apply auto
@@ -172,19 +153,19 @@
declare split_if [split]
-lemma LTL2a:
+lemma LTL2a:
"s \<Turnstile> \<^bold>\<not> (Next F) \<^bold>\<longrightarrow> (Next (\<^bold>\<not> F))"
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)
apply simp
done
-lemma LTL2b:
+lemma LTL2b:
"s \<Turnstile> (Next (\<^bold>\<not> F)) \<^bold>\<longrightarrow> (\<^bold>\<not> (Next F))"
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)
apply simp
done
-lemma LTL3:
+lemma LTL3:
"ex \<Turnstile> (Next (F \<^bold>\<longrightarrow> G)) \<^bold>\<longrightarrow> (Next F) \<^bold>\<longrightarrow> (Next G)"
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)
apply simp
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Wed Dec 30 22:09:44 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy Thu Dec 31 00:07:42 2015 +0100
@@ -10,75 +10,53 @@
default_sort type
-type_synonym
- ('a, 's) ioa_temp = "('a option,'s)transition temporal"
-
-type_synonym
- ('a, 's) step_pred = "('a option,'s)transition predicate"
-
-type_synonym
- 's state_pred = "'s predicate"
+type_synonym ('a, 's) ioa_temp = "('a option, 's) transition temporal"
-consts
+type_synonym ('a, 's) step_pred = "('a option, 's) transition predicate"
-option_lift :: "('a => 'b) => 'b => ('a option => 'b)"
-plift :: "('a => bool) => ('a option => bool)"
-
-temp_sat :: "('a,'s)execution => ('a,'s)ioa_temp => bool" (infixr "\<TTurnstile>" 22)
-xt1 :: "'s predicate => ('a,'s)step_pred"
-xt2 :: "'a option predicate => ('a,'s)step_pred"
+type_synonym 's state_pred = "'s predicate"
-validTE :: "('a,'s)ioa_temp => bool"
-validIOA :: "('a,'s)ioa => ('a,'s)ioa_temp => bool"
-
-mkfin :: "'a Seq => 'a Seq"
-
-ex2seq :: "('a,'s)execution => ('a option,'s)transition Seq"
-ex2seqC :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)"
-
+definition mkfin :: "'a Seq \<Rightarrow> 'a Seq"
+ where "mkfin s = (if Partial s then SOME t. Finite t \<and> s = t @@ UU else s)"
-defs
+definition option_lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a option \<Rightarrow> 'b"
+ where "option_lift f s y = (case y of None \<Rightarrow> s | Some x \<Rightarrow> f x)"
-mkfin_def:
- "mkfin s == if Partial s then @t. Finite t & s = t @@ UU
- else s"
-
-option_lift_def:
- "option_lift f s y == case y of None => s | Some x => (f x)"
-
+definition plift :: "('a \<Rightarrow> bool) \<Rightarrow> 'a option \<Rightarrow> bool"
(* plift is used to determine that None action is always false in
transition predicates *)
-plift_def:
- "plift P == option_lift P False"
+ where "plift P = option_lift P False"
-temp_sat_def:
- "ex \<TTurnstile> P == ((ex2seq ex) \<Turnstile> P)"
-
-xt1_def:
- "xt1 P tr == P (fst tr)"
+definition xt1 :: "'s predicate \<Rightarrow> ('a, 's) step_pred"
+ where "xt1 P tr = P (fst tr)"
-xt2_def:
- "xt2 P tr == P (fst (snd tr))"
+definition xt2 :: "'a option predicate \<Rightarrow> ('a, 's) step_pred"
+ where "xt2 P tr = P (fst (snd tr))"
-ex2seq_def:
- "ex2seq ex == ((ex2seqC $(mkfin (snd ex))) (fst ex))"
-
-ex2seqC_def:
- "ex2seqC == (fix$(LAM h ex. (%s. case ex of
+definition ex2seqC :: "('a, 's) pairs \<rightarrow> ('s \<Rightarrow> ('a option, 's) transition Seq)"
+where
+ "ex2seqC = (fix$(LAM h ex. (%s. case ex of
nil => (s,None,s)\<leadsto>nil
| x##xs => (flift1 (%pr.
(s,Some (fst pr), snd pr)\<leadsto> (h$xs) (snd pr))
$x)
)))"
-validTE_def:
- "validTE P == ! ex. (ex \<TTurnstile> P)"
+definition ex2seq :: "('a, 's) execution \<Rightarrow> ('a option, 's) transition Seq"
+ where "ex2seq ex = (ex2seqC $ (mkfin (snd ex))) (fst ex)"
+
+definition temp_sat :: "('a, 's) execution \<Rightarrow> ('a, 's) ioa_temp \<Rightarrow> bool" (infixr "\<TTurnstile>" 22)
+ where "(ex \<TTurnstile> P) \<longleftrightarrow> ((ex2seq ex) \<Turnstile> P)"
-validIOA_def:
- "validIOA A P == ! ex : executions A . (ex \<TTurnstile> P)"
+definition validTE :: "('a, 's) ioa_temp \<Rightarrow> bool"
+ where "validTE P \<longleftrightarrow> (\<forall>ex. (ex \<TTurnstile> P))"
+
+definition validIOA :: "('a, 's) ioa \<Rightarrow> ('a, 's) ioa_temp \<Rightarrow> bool"
+ where "validIOA A P \<longleftrightarrow> (\<forall>ex \<in> executions A. (ex \<TTurnstile> P))"
-axiomatization where
+axiomatization
+where
mkfin_UU:
"mkfin UU = nil" and
@@ -97,36 +75,35 @@
subsection \<open>ex2seqC\<close>
-lemma ex2seqC_unfold: "ex2seqC = (LAM ex. (%s. case ex of
- nil => (s,None,s)\<leadsto>nil
- | x##xs => (flift1 (%pr.
- (s,Some (fst pr), snd pr)\<leadsto> (ex2seqC$xs) (snd pr))
- $x)
+lemma ex2seqC_unfold: "ex2seqC = (LAM ex. (%s. case ex of
+ nil => (s,None,s)\<leadsto>nil
+ | x##xs => (flift1 (%pr.
+ (s,Some (fst pr), snd pr)\<leadsto> (ex2seqC$xs) (snd pr))
+ $x)
))"
-apply (rule trans)
-apply (rule fix_eq2)
-apply (rule ex2seqC_def)
-apply (rule beta_cfun)
-apply (simp add: flift1_def)
-done
+ apply (rule trans)
+ apply (rule fix_eq4)
+ apply (rule ex2seqC_def)
+ apply (rule beta_cfun)
+ apply (simp add: flift1_def)
+ done
lemma ex2seqC_UU: "(ex2seqC $UU) s=UU"
-apply (subst ex2seqC_unfold)
-apply simp
-done
+ apply (subst ex2seqC_unfold)
+ apply simp
+ done
lemma ex2seqC_nil: "(ex2seqC $nil) s = (s,None,s)\<leadsto>nil"
-apply (subst ex2seqC_unfold)
-apply simp
-done
+ apply (subst ex2seqC_unfold)
+ apply simp
+ done
-lemma ex2seqC_cons: "(ex2seqC $((a,t)\<leadsto>xs)) s =
- (s,Some a,t)\<leadsto> ((ex2seqC$xs) t)"
-apply (rule trans)
-apply (subst ex2seqC_unfold)
-apply (simp add: Consq_def flift1_def)
-apply (simp add: Consq_def flift1_def)
-done
+lemma ex2seqC_cons: "(ex2seqC $((a,t)\<leadsto>xs)) s = (s,Some a,t)\<leadsto> ((ex2seqC$xs) t)"
+ apply (rule trans)
+ apply (subst ex2seqC_unfold)
+ apply (simp add: Consq_def flift1_def)
+ apply (simp add: Consq_def flift1_def)
+ done
declare ex2seqC_UU [simp] ex2seqC_nil [simp] ex2seqC_cons [simp]
@@ -135,68 +112,65 @@
declare mkfin_UU [simp] mkfin_nil [simp] mkfin_cons [simp]
lemma ex2seq_UU: "ex2seq (s, UU) = (s,None,s)\<leadsto>nil"
-apply (simp add: ex2seq_def)
-done
+ by (simp add: ex2seq_def)
lemma ex2seq_nil: "ex2seq (s, nil) = (s,None,s)\<leadsto>nil"
-apply (simp add: ex2seq_def)
-done
+ by (simp add: ex2seq_def)
lemma ex2seq_cons: "ex2seq (s, (a,t)\<leadsto>ex) = (s,Some a,t) \<leadsto> ex2seq (t, ex)"
-apply (simp add: ex2seq_def)
-done
+ by (simp add: ex2seq_def)
declare ex2seqC_UU [simp del] ex2seqC_nil [simp del] ex2seqC_cons [simp del]
declare ex2seq_UU [simp] ex2seq_nil [simp] ex2seq_cons [simp]
lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
-apply (tactic \<open>pair_tac @{context} "exec" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-done
+ apply (tactic \<open>pair_tac @{context} "exec" 1\<close>)
+ apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+ apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+ done
subsection \<open>Interface TL -- TLS\<close>
-(* uses the fact that in executions states overlap, which is lost in
+(* uses the fact that in executions states overlap, which is lost in
after the translation via ex2seq !! *)
-lemma TL_TLS:
- "[| ! s a t. (P s) & s \<midarrow>a\<midarrow>A\<rightarrow> t --> (Q t) |]
- ==> ex \<TTurnstile> (Init (%(s,a,t). P s) \<^bold>\<and> Init (%(s,a,t). s \<midarrow>a\<midarrow>A\<rightarrow> t)
+lemma TL_TLS:
+ "[| ! s a t. (P s) & s \<midarrow>a\<midarrow>A\<rightarrow> t --> (Q t) |]
+ ==> ex \<TTurnstile> (Init (%(s,a,t). P s) \<^bold>\<and> Init (%(s,a,t). s \<midarrow>a\<midarrow>A\<rightarrow> t)
\<^bold>\<longrightarrow> (Next (Init (%(s,a,t).Q s))))"
-apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
+ apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
-apply clarify
-apply (simp split add: split_if)
-(* TL = UU *)
-apply (rule conjI)
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-(* TL = nil *)
-apply (rule conjI)
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-apply (tactic \<open>Seq_case_tac @{context} "x2" 1\<close>)
-apply (simp add: unlift_def)
-apply fast
-apply (simp add: unlift_def)
-apply fast
-apply (simp add: unlift_def)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-(* TL =cons *)
-apply (simp add: unlift_def)
+ apply clarify
+ apply (simp split add: split_if)
+ (* TL = UU *)
+ apply (rule conjI)
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+ apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+ apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+ apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+ apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+ (* TL = nil *)
+ apply (rule conjI)
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+ apply (tactic \<open>Seq_case_tac @{context} "x2" 1\<close>)
+ apply (simp add: unlift_def)
+ apply fast
+ apply (simp add: unlift_def)
+ apply fast
+ apply (simp add: unlift_def)
+ apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+ apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+ apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+ (* TL =cons *)
+ apply (simp add: unlift_def)
-apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-done
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+ apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+ apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+ apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+ apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+ done
end
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Wed Dec 30 22:09:44 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy Thu Dec 31 00:07:42 2015 +0100
@@ -10,195 +10,143 @@
default_sort type
-type_synonym
- ('a,'s)pairs = "('a * 's) Seq"
-
-type_synonym
- ('a,'s)execution = "'s * ('a,'s)pairs"
-
-type_synonym
- 'a trace = "'a Seq"
-
-type_synonym
- ('a,'s)execution_module = "('a,'s)execution set * 'a signature"
-
-type_synonym
- 'a schedule_module = "'a trace set * 'a signature"
-
-type_synonym
- 'a trace_module = "'a trace set * 'a signature"
-
-consts
-
- (* Executions *)
-
- is_exec_fragC ::"('a,'s)ioa => ('a,'s)pairs -> 's => tr"
- is_exec_frag ::"[('a,'s)ioa, ('a,'s)execution] => bool"
- has_execution ::"[('a,'s)ioa, ('a,'s)execution] => bool"
- executions :: "('a,'s)ioa => ('a,'s)execution set"
-
- (* Schedules and traces *)
- filter_act ::"('a,'s)pairs -> 'a trace"
- has_schedule :: "[('a,'s)ioa, 'a trace] => bool"
- has_trace :: "[('a,'s)ioa, 'a trace] => bool"
- schedules :: "('a,'s)ioa => 'a trace set"
- traces :: "('a,'s)ioa => 'a trace set"
- mk_trace :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace"
-
- laststate ::"('a,'s)execution => 's"
-
- (* A predicate holds infinitely (finitely) often in a sequence *)
-
- inf_often ::"('a => bool) => 'a Seq => bool"
- fin_often ::"('a => bool) => 'a Seq => bool"
-
- (* fairness of executions *)
-
- wfair_ex ::"('a,'s)ioa => ('a,'s)execution => bool"
- sfair_ex ::"('a,'s)ioa => ('a,'s)execution => bool"
- is_wfair ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool"
- is_sfair ::"('a,'s)ioa => 'a set => ('a,'s)execution => bool"
- fair_ex ::"('a,'s)ioa => ('a,'s)execution => bool"
-
- (* fair behavior sets *)
-
- fairexecutions ::"('a,'s)ioa => ('a,'s)execution set"
- fairtraces ::"('a,'s)ioa => 'a trace set"
-
- (* Notions of implementation *)
- ioa_implements :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr "=<|" 12)
- fair_implements :: "('a,'s1)ioa => ('a,'s2)ioa => bool"
-
- (* Execution, schedule and trace modules *)
- Execs :: "('a,'s)ioa => ('a,'s)execution_module"
- Scheds :: "('a,'s)ioa => 'a schedule_module"
- Traces :: "('a,'s)ioa => 'a trace_module"
-
-
-defs
+type_synonym ('a, 's) pairs = "('a * 's) Seq"
+type_synonym ('a, 's) execution = "'s * ('a, 's) pairs"
+type_synonym 'a trace = "'a Seq"
+type_synonym ('a, 's) execution_module = "('a, 's) execution set * 'a signature"
+type_synonym 'a schedule_module = "'a trace set * 'a signature"
+type_synonym 'a trace_module = "'a trace set * 'a signature"
(* ------------------- Executions ------------------------------ *)
-
-is_exec_frag_def:
- "is_exec_frag A ex == ((is_exec_fragC A$(snd ex)) (fst ex) ~= FF)"
-
-
-is_exec_fragC_def:
- "is_exec_fragC A ==(fix$(LAM h ex. (%s. case ex of
+definition is_exec_fragC :: "('a, 's) ioa \<Rightarrow> ('a, 's) pairs \<rightarrow> 's \<Rightarrow> tr"
+where
+ "is_exec_fragC A = (fix $ (LAM h ex. (%s. case ex of
nil => TT
| x##xs => (flift1
(%p. Def ((s,p):trans_of A) andalso (h$xs) (snd p))
$x)
)))"
-
+definition is_exec_frag :: "[('a,'s)ioa, ('a,'s)execution] \<Rightarrow> bool"
+ where "is_exec_frag A ex = ((is_exec_fragC A $ (snd ex)) (fst ex) ~= FF)"
-executions_def:
- "executions ioa == {e. ((fst e) : starts_of(ioa)) &
- is_exec_frag ioa e}"
+definition executions :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution set"
+ where "executions ioa = {e. ((fst e) \<in> starts_of(ioa)) \<and> is_exec_frag ioa e}"
(* ------------------- Schedules ------------------------------ *)
-
-filter_act_def:
- "filter_act == Map fst"
+definition filter_act :: "('a, 's) pairs \<rightarrow> 'a trace"
+ where "filter_act = Map fst"
-has_schedule_def:
- "has_schedule ioa sch ==
- (? ex:executions ioa. sch = filter_act$(snd ex))"
+definition has_schedule :: "[('a, 's) ioa, 'a trace] \<Rightarrow> bool"
+ where "has_schedule ioa sch \<longleftrightarrow> (\<exists>ex \<in> executions ioa. sch = filter_act $ (snd ex))"
-schedules_def:
- "schedules ioa == {sch. has_schedule ioa sch}"
+definition schedules :: "('a, 's) ioa \<Rightarrow> 'a trace set"
+ where "schedules ioa = {sch. has_schedule ioa sch}"
(* ------------------- Traces ------------------------------ *)
-has_trace_def:
- "has_trace ioa tr ==
- (? sch:schedules ioa. tr = Filter (%a. a:ext(ioa))$sch)"
+definition has_trace :: "[('a, 's) ioa, 'a trace] \<Rightarrow> bool"
+ where "has_trace ioa tr = (\<exists>sch \<in> schedules ioa. tr = Filter (\<lambda>a. a \<in> ext ioa) $ sch)"
-traces_def:
- "traces ioa == {tr. has_trace ioa tr}"
-
+definition traces :: "('a, 's) ioa \<Rightarrow> 'a trace set"
+ where "traces ioa \<equiv> {tr. has_trace ioa tr}"
-mk_trace_def:
- "mk_trace ioa == LAM tr.
- Filter (%a. a:ext(ioa))$(filter_act$tr)"
+definition mk_trace :: "('a, 's) ioa \<Rightarrow> ('a, 's) pairs \<rightarrow> 'a trace"
+ where "mk_trace ioa = (LAM tr. Filter (\<lambda>a. a \<in> ext ioa) $ (filter_act $ tr))"
(* ------------------- Fair Traces ------------------------------ *)
-laststate_def:
- "laststate ex == case Last$(snd ex) of
- UU => fst ex
- | Def at => snd at"
+definition laststate :: "('a, 's) execution \<Rightarrow> 's"
+where
+ "laststate ex = (case Last $ (snd ex) of
+ UU => fst ex
+ | Def at => snd at)"
-inf_often_def:
- "inf_often P s == Infinite (Filter P$s)"
+(* A predicate holds infinitely (finitely) often in a sequence *)
+
+definition inf_often :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> bool"
+ where "inf_often P s \<longleftrightarrow> Infinite (Filter P $ s)"
(* filtering P yields a finite or partial sequence *)
-fin_often_def:
- "fin_often P s == ~inf_often P s"
+definition fin_often :: "('a \<Rightarrow> bool) \<Rightarrow> 'a Seq \<Rightarrow> bool"
+ where "fin_often P s \<longleftrightarrow> \<not> inf_often P s"
+
+
+(* fairness of executions *)
(* Note that partial execs cannot be wfair as the inf_often predicate in the
else branch prohibits it. However they can be sfair in the case when all W
are only finitely often enabled: Is this the right model?
See LiveIOA for solution conforming with the literature and superseding this one *)
-wfair_ex_def:
- "wfair_ex A ex == ! W : wfair_of A.
- if Finite (snd ex)
- then ~Enabled A W (laststate ex)
- else is_wfair A W ex"
+definition is_wfair :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) execution \<Rightarrow> bool"
+where
+ "is_wfair A W ex \<longleftrightarrow>
+ (inf_often (\<lambda>x. fst x \<in> W) (snd ex) \<or> inf_often (\<lambda>x. \<not> Enabled A W (snd x)) (snd ex))"
+definition wfair_ex :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution \<Rightarrow> bool"
+where
+ "wfair_ex A ex \<longleftrightarrow> (\<forall>W \<in> wfair_of A.
+ if Finite (snd ex)
+ then \<not> Enabled A W (laststate ex)
+ else is_wfair A W ex)"
-is_wfair_def:
- "is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex)
- | inf_often (%x. ~ Enabled A W (snd x)) (snd ex))"
-
-sfair_ex_def:
- "sfair_ex A ex == ! W : sfair_of A.
+definition is_sfair :: "('a, 's) ioa \<Rightarrow> 'a set \<Rightarrow> ('a, 's) execution \<Rightarrow> bool"
+where
+ "is_sfair A W ex \<longleftrightarrow>
+ (inf_often (\<lambda>x. fst x:W) (snd ex) \<or> fin_often (\<lambda>x. Enabled A W (snd x)) (snd ex))"
+definition sfair_ex :: "('a, 's)ioa \<Rightarrow> ('a, 's) execution \<Rightarrow> bool"
+where
+ "sfair_ex A ex \<longleftrightarrow> (\<forall>W \<in> sfair_of A.
if Finite (snd ex)
then ~Enabled A W (laststate ex)
- else is_sfair A W ex"
+ else is_sfair A W ex)"
-is_sfair_def:
- "is_sfair A W ex == (inf_often (%x. fst x:W) (snd ex)
- | fin_often (%x. Enabled A W (snd x)) (snd ex))"
+definition fair_ex :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution \<Rightarrow> bool"
+ where "fair_ex A ex \<longleftrightarrow> wfair_ex A ex \<and> sfair_ex A ex"
+
-fair_ex_def:
- "fair_ex A ex == wfair_ex A ex & sfair_ex A ex"
+(* fair behavior sets *)
-fairexecutions_def:
- "fairexecutions A == {ex. ex:executions A & fair_ex A ex}"
+definition fairexecutions :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution set"
+ where "fairexecutions A = {ex. ex \<in> executions A \<and> fair_ex A ex}"
-fairtraces_def:
- "fairtraces A == {mk_trace A$(snd ex) | ex. ex:fairexecutions A}"
+definition fairtraces :: "('a, 's) ioa \<Rightarrow> 'a trace set"
+ where "fairtraces A = {mk_trace A $ (snd ex) | ex. ex \<in> fairexecutions A}"
(* ------------------- Implementation ------------------------------ *)
-ioa_implements_def:
- "ioa1 =<| ioa2 ==
- (((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) &
- (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) &
- traces(ioa1) <= traces(ioa2))"
+(* Notions of implementation *)
-fair_implements_def:
- "fair_implements C A == inp(C) = inp(A) & out(C)=out(A) &
- fairtraces(C) <= fairtraces(A)"
+definition ioa_implements :: "[('a, 's1) ioa, ('a, 's2) ioa] \<Rightarrow> bool" (infixr "=<|" 12)
+where
+ "(ioa1 =<| ioa2) \<longleftrightarrow>
+ (((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) \<and>
+ (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) \<and>
+ traces(ioa1) \<subseteq> traces(ioa2))"
+
+definition fair_implements :: "('a, 's1) ioa \<Rightarrow> ('a, 's2) ioa \<Rightarrow> bool"
+where
+ "fair_implements C A \<longleftrightarrow> inp C = inp A \<and> out C = out A \<and> fairtraces C \<subseteq> fairtraces A"
+
(* ------------------- Modules ------------------------------ *)
-Execs_def:
- "Execs A == (executions A, asig_of A)"
+(* Execution, schedule and trace modules *)
+
+definition Execs :: "('a, 's) ioa \<Rightarrow> ('a, 's) execution_module"
+ where "Execs A = (executions A, asig_of A)"
-Scheds_def:
- "Scheds A == (schedules A, asig_of A)"
+definition Scheds :: "('a, 's) ioa \<Rightarrow> 'a schedule_module"
+ where "Scheds A = (schedules A, asig_of A)"
-Traces_def:
- "Traces A == (traces A,asig_of A)"
+definition Traces :: "('a, 's) ioa \<Rightarrow> 'a trace_module"
+ where "Traces A = (traces A, asig_of A)"
lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
@@ -217,16 +165,13 @@
lemma filter_act_UU: "filter_act$UU = UU"
-apply (simp add: filter_act_def)
-done
+ by (simp add: filter_act_def)
lemma filter_act_nil: "filter_act$nil = nil"
-apply (simp add: filter_act_def)
-done
+ by (simp add: filter_act_def)
lemma filter_act_cons: "filter_act$(x\<leadsto>xs) = (fst x) \<leadsto> filter_act$xs"
-apply (simp add: filter_act_def)
-done
+ by (simp add: filter_act_def)
declare filter_act_UU [simp] filter_act_nil [simp] filter_act_cons [simp]
@@ -236,20 +181,17 @@
(* ---------------------------------------------------------------- *)
lemma mk_trace_UU: "mk_trace A$UU=UU"
-apply (simp add: mk_trace_def)
-done
+ by (simp add: mk_trace_def)
lemma mk_trace_nil: "mk_trace A$nil=nil"
-apply (simp add: mk_trace_def)
-done
+ by (simp add: mk_trace_def)
-lemma mk_trace_cons: "mk_trace A$(at \<leadsto> xs) =
- (if ((fst at):ext A)
- then (fst at) \<leadsto> (mk_trace A$xs)
+lemma mk_trace_cons: "mk_trace A$(at \<leadsto> xs) =
+ (if ((fst at):ext A)
+ then (fst at) \<leadsto> (mk_trace A$xs)
else mk_trace A$xs)"
-apply (simp add: mk_trace_def)
-done
+ by (simp add: mk_trace_def)
declare mk_trace_UU [simp] mk_trace_nil [simp] mk_trace_cons [simp]
@@ -258,37 +200,37 @@
(* ---------------------------------------------------------------- *)
-lemma is_exec_fragC_unfold: "is_exec_fragC A = (LAM ex. (%s. case ex of
- nil => TT
- | x##xs => (flift1
- (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A$xs) (snd p))
- $x)
+lemma is_exec_fragC_unfold: "is_exec_fragC A = (LAM ex. (%s. case ex of
+ nil => TT
+ | x##xs => (flift1
+ (%p. Def ((s,p):trans_of A) andalso (is_exec_fragC A$xs) (snd p))
+ $x)
))"
-apply (rule trans)
-apply (rule fix_eq2)
-apply (rule is_exec_fragC_def)
-apply (rule beta_cfun)
-apply (simp add: flift1_def)
-done
+ apply (rule trans)
+ apply (rule fix_eq4)
+ apply (rule is_exec_fragC_def)
+ apply (rule beta_cfun)
+ apply (simp add: flift1_def)
+ done
lemma is_exec_fragC_UU: "(is_exec_fragC A$UU) s=UU"
-apply (subst is_exec_fragC_unfold)
-apply simp
-done
+ apply (subst is_exec_fragC_unfold)
+ apply simp
+ done
lemma is_exec_fragC_nil: "(is_exec_fragC A$nil) s = TT"
-apply (subst is_exec_fragC_unfold)
-apply simp
-done
+ apply (subst is_exec_fragC_unfold)
+ apply simp
+ done
-lemma is_exec_fragC_cons: "(is_exec_fragC A$(pr\<leadsto>xs)) s =
- (Def ((s,pr):trans_of A)
+lemma is_exec_fragC_cons: "(is_exec_fragC A$(pr\<leadsto>xs)) s =
+ (Def ((s,pr):trans_of A)
andalso (is_exec_fragC A$xs)(snd pr))"
-apply (rule trans)
-apply (subst is_exec_fragC_unfold)
-apply (simp add: Consq_def flift1_def)
-apply simp
-done
+ apply (rule trans)
+ apply (subst is_exec_fragC_unfold)
+ apply (simp add: Consq_def flift1_def)
+ apply simp
+ done
declare is_exec_fragC_UU [simp] is_exec_fragC_nil [simp] is_exec_fragC_cons [simp]
@@ -299,18 +241,15 @@
(* ---------------------------------------------------------------- *)
lemma is_exec_frag_UU: "is_exec_frag A (s, UU)"
-apply (simp add: is_exec_frag_def)
-done
+ by (simp add: is_exec_frag_def)
lemma is_exec_frag_nil: "is_exec_frag A (s, nil)"
-apply (simp add: is_exec_frag_def)
-done
+ by (simp add: is_exec_frag_def)
-lemma is_exec_frag_cons: "is_exec_frag A (s, (a,t)\<leadsto>ex) =
- (((s,a,t):trans_of A) &
+lemma is_exec_frag_cons: "is_exec_frag A (s, (a,t)\<leadsto>ex) =
+ (((s,a,t):trans_of A) &
is_exec_frag A (t, ex))"
-apply (simp add: is_exec_frag_def)
-done
+ by (simp add: is_exec_frag_def)
(* Delsimps [is_exec_fragC_UU,is_exec_fragC_nil,is_exec_fragC_cons]; *)
@@ -321,85 +260,83 @@
(* ---------------------------------------------------------------------------- *)
lemma laststate_UU: "laststate (s,UU) = s"
-apply (simp add: laststate_def)
-done
+ by (simp add: laststate_def)
lemma laststate_nil: "laststate (s,nil) = s"
-apply (simp add: laststate_def)
-done
+ by (simp add: laststate_def)
lemma laststate_cons: "!! ex. Finite ex ==> laststate (s,at\<leadsto>ex) = laststate (snd at,ex)"
-apply (simp (no_asm) add: laststate_def)
-apply (case_tac "ex=nil")
-apply (simp (no_asm_simp))
-apply (simp (no_asm_simp))
-apply (drule Finite_Last1 [THEN mp])
-apply assumption
-apply defined
-done
+ apply (simp (no_asm) add: laststate_def)
+ apply (case_tac "ex=nil")
+ apply (simp (no_asm_simp))
+ apply (simp (no_asm_simp))
+ apply (drule Finite_Last1 [THEN mp])
+ apply assumption
+ apply defined
+ done
declare laststate_UU [simp] laststate_nil [simp] laststate_cons [simp]
lemma exists_laststate: "!!ex. Finite ex ==> (! s. ? u. laststate (s,ex)=u)"
-apply (tactic "Seq_Finite_induct_tac @{context} 1")
-done
+ apply (tactic "Seq_Finite_induct_tac @{context} 1")
+ done
subsection "has_trace, mk_trace"
-(* alternative definition of has_trace tailored for the refinement proof, as it does not
+(* alternative definition of has_trace tailored for the refinement proof, as it does not
take the detour of schedules *)
-lemma has_trace_def2:
-"has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))"
-apply (unfold executions_def mk_trace_def has_trace_def schedules_def has_schedule_def)
-apply auto
-done
+lemma has_trace_def2:
+ "has_trace A b = (? ex:executions A. b = mk_trace A$(snd ex))"
+ apply (unfold executions_def mk_trace_def has_trace_def schedules_def has_schedule_def [abs_def])
+ apply auto
+ done
subsection "signatures and executions, schedules"
-(* All executions of A have only actions of A. This is only true because of the
+(* All executions of A have only actions of A. This is only true because of the
predicate state_trans (part of the predicate IOA): We have no dependent types.
For executions of parallel automata this assumption is not needed, as in par_def
this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *)
-lemma execfrag_in_sig:
- "!! A. is_trans_of A ==>
+lemma execfrag_in_sig:
+ "!! A. is_trans_of A ==>
! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)"
-apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def},
- @{thm Forall_def}, @{thm sforall_def}] 1\<close>)
-(* main case *)
-apply (auto simp add: is_trans_of_def)
-done
+ apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def},
+ @{thm Forall_def}, @{thm sforall_def}] 1\<close>)
+ (* main case *)
+ apply (auto simp add: is_trans_of_def)
+ done
-lemma exec_in_sig:
- "!! A.[| is_trans_of A; x:executions A |] ==>
+lemma exec_in_sig:
+ "!! A.[| is_trans_of A; x:executions A |] ==>
Forall (%a. a:act A) (filter_act$(snd x))"
-apply (simp add: executions_def)
-apply (tactic \<open>pair_tac @{context} "x" 1\<close>)
-apply (rule execfrag_in_sig [THEN spec, THEN mp])
-apply auto
-done
+ apply (simp add: executions_def)
+ apply (tactic \<open>pair_tac @{context} "x" 1\<close>)
+ apply (rule execfrag_in_sig [THEN spec, THEN mp])
+ apply auto
+ done
-lemma scheds_in_sig:
- "!! A.[| is_trans_of A; x:schedules A |] ==>
+lemma scheds_in_sig:
+ "!! A.[| is_trans_of A; x:schedules A |] ==>
Forall (%a. a:act A) x"
-apply (unfold schedules_def has_schedule_def)
-apply (fast intro!: exec_in_sig)
-done
+ apply (unfold schedules_def has_schedule_def [abs_def])
+ apply (fast intro!: exec_in_sig)
+ done
subsection "executions are prefix closed"
(* only admissible in y, not if done in x !! *)
lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x --> is_exec_frag A (s,y)"
-apply (tactic \<open>pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1\<close>)
-apply (intro strip)
-apply (tactic \<open>Seq_case_simp_tac @{context} "x" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-apply auto
-done
+ apply (tactic \<open>pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1\<close>)
+ apply (intro strip)
+ apply (tactic \<open>Seq_case_simp_tac @{context} "x" 1\<close>)
+ apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+ apply auto
+ done
lemmas exec_prefixclosed =
conjI [THEN execfrag_prefixclosed [THEN spec, THEN spec, THEN mp]]
@@ -409,11 +346,11 @@
lemma exec_prefix2closed [rule_format]:
"! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)"
-apply (tactic \<open>pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1\<close>)
-apply (intro strip)
-apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
-apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
-apply auto
-done
+ apply (tactic \<open>pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1\<close>)
+ apply (intro strip)
+ apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+ apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+ apply auto
+ done
end