# HG changeset patch # User wenzelm # Date 1451516862 -3600 # Node ID 68db98c2cd9782d290b81d22ca181f01cd0cf267 # Parent 8c6226d88ced36a833bd9dca71ccd5484168536c modernized defs; tuned proofs; tuned whitespace; diff -r 8c6226d88ced -r 68db98c2cd97 src/HOL/HOLCF/IOA/meta_theory/Automata.thy --- 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 "\" 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 \ 'a signature" + where "asig_of = fst" + +definition starts_of :: "('a, 's) ioa \ 's set" + where "starts_of = (fst \ snd)" + +definition trans_of :: "('a, 's) ioa \ ('a, 's) transition set" + where "trans_of = (fst \ snd \ snd)" + +abbreviation trans_of_syn ("_ \_\_\ _" [81, 81, 81, 81] 100) + where "s \a\A\ t \ (s, a, t) \ trans_of A" + +definition wfair_of :: "('a, 's) ioa \ 'a set set" + where "wfair_of = (fst \ snd \ snd \ snd)" -abbreviation - trans_of_syn ("_ \_\_\ _" [81,81,81,81] 100) where - "s \a\A\ t == (s,a,t):trans_of A" +definition sfair_of :: "('a, 's) ioa \ 'a set set" + where "sfair_of = (snd \ snd \ snd \ snd)" + +definition is_asig_of :: "('a, 's) ioa \ bool" + where "is_asig_of A = is_asig (asig_of A)" + +definition is_starts_of :: "('a, 's) ioa \ bool" + where "is_starts_of A \ starts_of A \ {}" + +definition is_trans_of :: "('a, 's) ioa \ bool" + where "is_trans_of A \ + (\triple. triple \ trans_of A \ fst (snd triple) \ actions (asig_of A))" + +definition input_enabled :: "('a, 's) ioa \ bool" + where "input_enabled A \ + (\a. a \ inputs (asig_of A) \ (\s1. \s2. (s1, a, s2) \ trans_of A))" + +definition IOA :: "('a, 's) ioa \ bool" + where "IOA A \ + is_asig_of A \ + is_starts_of A \ + is_trans_of A \ + 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 \ '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" -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 \ bool] \ bool" + where "invariant A P \ (\s. reachable A s \ 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] \ bool" +where + "compatible A B \ + (((out A \ out B) = {}) \ + ((int A \ act B) = {}) \ + ((int B \ 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] \ 'a signature" +where + "asig_comp a1 a2 = + (((inputs(a1) \ inputs(a2)) - (outputs(a1) \ outputs(a2)), + (outputs(a1) \ outputs(a2)), + (internals(a1) \ internals(a2))))" -par_def: - "(A \ B) == +definition par :: "[('a, 's) ioa, ('a, 't) ioa] \ ('a, 's * 't) ioa" (infixr "\" 10) +where + "(A \ B) = (asig_comp (asig_of A) (asig_of B), - {pr. fst(pr):starts_of(A) & snd(pr):starts_of(B)}, + {pr. fst(pr) \ starts_of(A) \ snd(pr) \ 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 \ 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) + (if a \ act B then + (snd(s), a, snd(t)) \ 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 \ wfair_of B, + sfair_of A \ sfair_of B)" (* ------------------------ hiding -------------------------------------------- *) -restrict_asig_def: - "restrict_asig asig actns == +(* hiding and restricting *) + +definition restrict_asig :: "['a signature, 'a set] \ '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] \ ('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] \ 'a signature" +where + "hide_asig asig actns = (inputs(asig) - actns, outputs(asig) - actns, - internals(asig) Un actns)" + internals(asig) \ actns)" -hide_def: - "hide A actns == +definition hide :: "[('a, 's) ioa, 'a set] \ ('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 \ ('c \ 'a option) \ 'c set" + where "rename_set A ren = {b. \x. Some x = ren b \ x \ 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 \ ('c \ 'a option) \ ('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 + \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})" + (* ------------------------- 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 \ 'a \ 's \ bool" + where "enabled A a s \ (\t. s \a\A\ t)" + +definition Enabled :: "('a, 's) ioa \ 'a set \ 's \ bool" + where "Enabled A W s \ (\w \ 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 \a\A\ t - --> Enabled A W t" +(* action set keeps enabled until probably disabled by itself *) -enabled_def: - "enabled A a s == ? t. s \a\A\ t" +definition en_persistent :: "('a, 's) ioa \ 'a set \ bool" +where + "en_persistent A W \ + (\s a t. Enabled A W s \ a \ W \ s \a\A\ t \ 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 \ 'a \ 's \ bool" + where "was_enabled A a t \ (\s. s \a\A\ t)" + +definition set_was_enabled :: "('a, 's) ioa \ 'a set \ 's \ bool" + where "set_was_enabled A W t \ (\w \ 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 \a\A\ t - --> Enabled A W t" -was_enabled_def: - "was_enabled A a t == ? s. s \a\A\ t" +definition fairIOA :: "('a, 's) ioa \ bool" + where "fairIOA A \ (\S \ wfair_of A. S \ local A) \ (\S \ sfair_of A. S \ 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 \ bool" +where + "input_resistant A \ + (\W \ sfair_of A. \s a t. + reachable A s \ reachable A t \ a \ inp A \ + Enabled A W s \ s \a\A\ t \ 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 \ 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 \ 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 \ 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 \ 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 \ B) = asig_comp (asig_of A) (asig_of B)" + by (simp add: par_def ioa_projections) + + +lemma externals_of_par: "ext (A1\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 \ B) = asig_comp (asig_of A) (asig_of B)" - apply (simp add: par_def ioa_projections) +lemma actions_of_par: "act (A1\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\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\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\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\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\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\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\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\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\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\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\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 \a\(rename C f)\ t ==> (? x. Some(x) = f(a) & s \x\C\ 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\B)" - -lemma trans_A_proj: "[|(s,a,t):trans_of (A\B); a:act A|] +lemma trans_A_proj: "[|(s,a,t):trans_of (A\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\B); a:act B|] +lemma trans_B_proj: "[|(s,a,t):trans_of (A\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\B); a~:act A|] +lemma trans_A_proj2: "[|(s,a,t):trans_of (A\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\B); a~:act B|] +lemma trans_B_proj2: "[|(s,a,t):trans_of (A\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\B) +lemma trans_AB_proj: "(s,a,t):trans_of (A\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\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\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\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 \ B \ C \ 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 \ B \ C \ 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 \def *) lemma is_trans_of_par: "is_trans_of (A\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\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\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\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\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\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] diff -r 8c6226d88ced -r 68db98c2cd97 src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy --- 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 \ - -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 \ method_setup mkex_induct = \ @@ -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\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) diff -r 8c6226d88ced -r 68db98c2cd97 src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy --- 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 \Compositionality on Trace level\ 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\(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\(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) \ Finite tr" +axiomatization +where + finiteR_mksch: + "Finite (mksch A B$tr$x$y) \ Finite tr" lemma finiteR_mksch': "\ Finite tr \ \ 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\(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\(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\(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\(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\(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\(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\tr)$schA$schB = - (Takewhile (%a. a:int A)$schA) - @@ (x\(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA)) +lemma mksch_cons1: "[|x:act A;x~:act B|] + ==> mksch A B$(x\tr)$schA$schB = + (Takewhile (%a. a:int A)$schA) + @@ (x\(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\tr)$schA$schB = - (Takewhile (%a. a:int B)$schB) - @@ (x\(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\tr)$schA$schB = + (Takewhile (%a. a:int B)$schB) + @@ (x\(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\tr)$schA$schB = - (Takewhile (%a. a:int A)$schA) - @@ ((Takewhile (%a. a:int B)$schB) - @@ (x\(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\tr)$schA$schB = + (Takewhile (%a. a:int A)$schA) + @@ ((Takewhile (%a. a:int B)$schB) + @@ (x\(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\B)) tr + "!!A B. compatible A B ==> + ! schA schB. Forall (%x. x:act (A\B)) tr --> Forall (%x. x:act (A\B)) (mksch A B$tr$schA$schB)" apply (tactic \Seq_induct_tac @{context} "tr" [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\) @@ -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 \Seq_induct_tac @{context} "tr" [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\) @@ -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 \Seq_induct_tac @{context} "tr" [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\) @@ -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\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\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\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\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\B))$(mksch A B$tr$schA$schB) = tr" apply (tactic \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\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\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\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\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\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\B)) = + (Filter (%a. a:act A)$tr : traces A & + Filter (%a. a:act B)$tr : traces B & Forall (%x. x:ext(A\B)) tr)" apply (simp (no_asm) add: traces_def has_trace_def) @@ -957,10 +950,10 @@ subsection \COMPOSITIONALITY on TRACE Level -- for Modules\ -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\B) = par_traces (Traces A) (Traces B)" apply (unfold Traces_def par_traces_def) diff -r 8c6226d88ced -r 68db98c2cd97 src/HOL/HOLCF/IOA/meta_theory/Pred.thy --- 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" ("_ \ _" [100,9] 8) -valid ::"'a predicate => bool" (* ("|-") *) +type_synonym 'a predicate = "'a \ bool" -NOT ::"'a predicate => 'a predicate" ("\<^bold>\ _" [40] 40) -AND ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<^bold>\" 35) -OR ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<^bold>\" 30) -IMPLIES ::"'a predicate => 'a predicate => 'a predicate" (infixr "\<^bold>\" 25) +definition satisfies :: "'a \ 'a predicate \ bool" ("_ \ _" [100,9] 8) + where "(s \ P) \ P s" - -defs +definition valid :: "'a predicate \ bool" (* ("|-") *) + where "valid P \ (\s. (s \ P))" -satisfies_def: - "s \ P == P s" +definition NOT :: "'a predicate \ 'a predicate" ("\<^bold>\ _" [40] 40) + where "NOT P s \ ~ (P s)" -valid_def: - "valid P == (! s. (s \ P))" - -NOT_def: - "NOT P s == ~ (P s)" +definition AND :: "'a predicate \ 'a predicate \ 'a predicate" (infixr "\<^bold>\" 35) + where "(P \<^bold>\ Q) s \ P s \ Q s" -AND_def: - "(P \<^bold>\ Q) s == (P s) & (Q s)" +definition OR :: "'a predicate \ 'a predicate \ 'a predicate" (infixr "\<^bold>\" 30) + where "(P \<^bold>\ Q) s \ P s \ Q s" -OR_def: - "(P \<^bold>\ Q) s == (P s) | (Q s)" - -IMPLIES_def: - "(P \<^bold>\ Q) s == (P s) --> (Q s)" +definition IMPLIES :: "'a predicate \ 'a predicate \ 'a predicate" (infixr "\<^bold>\" 25) + where "(P \<^bold>\ Q) s \ P s \ Q s" end diff -r 8c6226d88ced -r 68db98c2cd97 src/HOL/HOLCF/IOA/meta_theory/Sequence.thy --- 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 \ 'a Seq \ 'a Seq" + where "Consq a = (LAM s. Def a ## s)" + +definition Filter :: "('a \ bool) \ 'a Seq \ '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 \ 'b) \ 'a Seq \ 'b Seq" + where "Map f = smap $ (flift2 f)" - Filter2 ::"('a => bool) => 'a Seq -> 'a Seq" - -abbreviation - Consq_syn ("(_/\_)" [66,65] 65) where - "a\s == Consq a$s" - +definition Forall :: "('a \ bool) \ 'a Seq \ bool" + where "Forall P = sforall (flift2 P)" -(* list Enumeration *) -syntax - "_totlist" :: "args => 'a Seq" ("[(_)!]") - "_partlist" :: "args => 'a Seq" ("[(_)?]") -translations - "[x, xs!]" == "x\[xs!]" - "[x!]" == "x\nil" - "[x, xs?]" == "x\[xs?]" - "[x?]" == "x\CONST bottom" +definition Last :: "'a Seq \ 'a lift" + where "Last = slast" -defs - -Consq_def: "Consq a == LAM s. Def a ## s" +definition Dropwhile :: "('a \ bool) \ 'a Seq \ '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 \ bool) \ 'a Seq \ '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 \ 'b Seq \ ('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 \ 'a Seq" + where "Flat = sflat" + +definition Filter2 :: "('a \ bool) \ 'a Seq \ 'a Seq" +where + "Filter2 P = (fix $ (LAM h t. case t of + nil \ nil + | x##xs \ (case x of UU \ UU | Def y \ (if P y then x##(h$xs) else h$xs))))" +abbreviation Consq_syn ("(_/\_)" [66,65] 65) + where "a\s \ Consq a $ s" + + +text \List enumeration\ +syntax + "_totlist" :: "args => 'a Seq" ("[(_)!]") + "_partlist" :: "args => 'a Seq" ("[(_)?]") +translations + "[x, xs!]" == "x\[xs!]" + "[x!]" == "x\nil" + "[x, xs?]" == "x\[xs?]" + "[x?]" == "x\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\xs)=(f x) \ Map f$xs" -by (simp add: Map_def Consq_def flift2_def) + by (simp add: Map_def Consq_def flift2_def) subsubsection \Filter\ 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\xs)= (if P x then x\(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 \Forall\ 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\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 \Conc\ lemma Conc_cons: "(x\xs) @@ y = x\(xs @@y)" -by (simp add: Consq_def) + by (simp add: Consq_def) subsubsection \Takewhile\ 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\xs)= (if P x then x\(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 \DropWhile\ 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\xs)= (if P x then Dropwhile P$xs else x\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 \Last\ 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\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 \Flat\ 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 \Zip\ 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\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\xs)$(y\ys)= (x,y) \ 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\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 \ 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 \ 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 \ 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\s ~= UU" -apply (subst Consq_def2) -apply simp -done + apply (subst Consq_def2) + apply simp + done lemma Cons_not_less_UU: "~(a\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\s << nil" -apply (simp add: Consq_def2) -done + by (simp add: Consq_def2) lemma Cons_not_nil: "a\s ~= nil" -apply (simp add: Consq_def2) -done + by (simp add: Consq_def2) lemma Cons_not_nil2: "nil ~= a\s" -apply (simp add: Consq_def2) -done + by (simp add: Consq_def2) lemma Cons_inject_eq: "(a\s = b\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\s<t) = (a = b & s<x) = a\ (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\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\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\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\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\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\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\y) = Def x" -apply (simp add: Consq_def) -done + by (simp add: Consq_def) lemma TL_Cons [simp]: "TL$(x\y) = y" -apply (simp add: Consq_def) -done + by (simp add: Consq_def) (* ------------------------------------------------------------------------------------ *) subsection "Finite, Partial, Infinite" lemma Finite_Cons [simp]: "Finite (a\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< 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 \ 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\xs) << Filter P$y +lemma divide_Seq: "(x\xs) << Filter P$y ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x \ 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\xs" in monofun_cfun_arg) -apply simp -done + apply (rule divide_Seq_lemma [THEN mp]) + apply (drule_tac f="HD" and x="x\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 \ 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\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) + "\n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2) --> seq_take n$(x @@ (t\y1)) = seq_take n$(x @@ (t\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 seq_take k$y1 = seq_take k$y2|] - ==> seq_take n$(x @@ (s\y1)) = seq_take n$(y @@ (t\y2))" -apply (auto intro!: take_reduction1 [rule_format]) -done + "!! n.[| x=y; s=t; !! k. k seq_take k$y1 = seq_take k$y2|] + ==> seq_take n$(x @@ (s\y1)) = seq_take n$(y @@ (t\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) + "\n. ((! k. k < n --> seq_take k$y1 << seq_take k$y2) --> seq_take n$(x @@ (t\y1)) << seq_take n$(x @@ (t\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 seq_take k$y1 << seq_take k$y2|] - ==> seq_take n$(x @@ (s\y1)) << seq_take n$(y @@ (t\y2))" -apply (auto intro!: take_reduction_less1 [rule_format]) -done + "\n.[| x=y; s=t;!! k. k seq_take k$y1 << seq_take k$y2|] + ==> seq_take n$(x @@ (s\y1)) << seq_take n$(y @@ (t\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< (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\s2)|] ==> (f (s1 @@ y\s2)) = (g (s1 @@ y\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\s2)) = seq_take n$(g (s1 @@ y\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\s2)) = seq_take (Suc n)$(g (s1 @@ y\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\s2)) = seq_take n$(g (s1 @@ y\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\s)) = seq_take (Suc n)$(g (y\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 \ @@ -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; - \ end diff -r 8c6226d88ced -r 68db98c2cd97 src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy --- 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) diff -r 8c6226d88ced -r 68db98c2cd97 src/HOL/HOLCF/IOA/meta_theory/TL.thy --- 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 \ bool" + where "validT P \ (\s. s \ UU \ s \ nil \ (s \ P))" -Init :: "'a predicate => 'a temporal" ("\_\" [0] 1000) +definition unlift :: "'a lift \ 'a" + where "unlift x = (case x of Def y \ y)" -Box :: "'a temporal => 'a temporal" ("\(_)" [80] 80) -Diamond :: "'a temporal => 'a temporal" ("\(_)" [80] 80) -Next :: "'a temporal => 'a temporal" -Leadsto :: "'a temporal => 'a temporal => 'a temporal" (infixr "\" 22) +definition Init :: "'a predicate \ 'a temporal" ("\_\" [0] 1000) + where "Init P s = P (unlift (HD $ s))" + \ \this means that for \nil\ and \UU\ the effect is unpredictable\ -defs - -unlift_def: - "unlift x == (case x of Def y => y)" +definition Next :: "'a temporal \ 'a temporal" + where "(Next P) s \ (if TL $ s = UU \ 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 \ 'a Seq \ bool" + where "suffix s2 s \ (\s1. Finite s1 \ 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 \ 'a Seq \ bool" + where "tsuffix s2 s \ s2 \ nil \ s2 \ UU \ suffix s2 s" -Box_def: - "(\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 \ 'a temporal" ("\(_)" [80] 80) + where "(\P) s \ (\s2. tsuffix s2 s \ P s2)" -Diamond_def: - "\P == \<^bold>\ (\(\<^bold>\ P))" +definition Diamond :: "'a temporal \ 'a temporal" ("\(_)" [80] 80) + where "\P = (\<^bold>\ (\(\<^bold>\ P)))" -Leadsto_def: - "P \ Q == (\(P \<^bold>\ (\Q)))" - -validT_def: - "validT P == ! s. s~=UU & s~=nil --> (s \ P)" +definition Leadsto :: "'a temporal \ 'a temporal \ 'a temporal" (infixr "\" 22) + where "(P \ Q) = (\(P \<^bold>\ (\Q)))" lemma simple: "\\(\<^bold>\ P) = (\<^bold>\ \\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 \ \F \<^bold>\ (F \<^bold>\ (Next (\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 \ \<^bold>\ (Next F) \<^bold>\ (Next (\<^bold>\ F))" apply (unfold Next_def satisfies_def NOT_def IMPLIES_def) apply simp done -lemma LTL2b: +lemma LTL2b: "s \ (Next (\<^bold>\ F)) \<^bold>\ (\<^bold>\ (Next F))" apply (unfold Next_def satisfies_def NOT_def IMPLIES_def) apply simp done -lemma LTL3: +lemma LTL3: "ex \ (Next (F \<^bold>\ G)) \<^bold>\ (Next F) \<^bold>\ (Next G)" apply (unfold Next_def satisfies_def NOT_def IMPLIES_def) apply simp diff -r 8c6226d88ced -r 68db98c2cd97 src/HOL/HOLCF/IOA/meta_theory/TLS.thy --- 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 "\" 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 \ 'a Seq" + where "mkfin s = (if Partial s then SOME t. Finite t \ s = t @@ UU else s)" -defs +definition option_lift :: "('a \ 'b) \ 'b \ 'a option \ 'b" + where "option_lift f s y = (case y of None \ s | Some x \ 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 \ bool) \ 'a option \ 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 \ P == ((ex2seq ex) \ P)" - -xt1_def: - "xt1 P tr == P (fst tr)" +definition xt1 :: "'s predicate \ ('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 \ ('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 \ ('s \ ('a option, 's) transition Seq)" +where + "ex2seqC = (fix$(LAM h ex. (%s. case ex of nil => (s,None,s)\nil | x##xs => (flift1 (%pr. (s,Some (fst pr), snd pr)\ (h$xs) (snd pr)) $x) )))" -validTE_def: - "validTE P == ! ex. (ex \ P)" +definition ex2seq :: "('a, 's) execution \ ('a option, 's) transition Seq" + where "ex2seq ex = (ex2seqC $ (mkfin (snd ex))) (fst ex)" + +definition temp_sat :: "('a, 's) execution \ ('a, 's) ioa_temp \ bool" (infixr "\" 22) + where "(ex \ P) \ ((ex2seq ex) \ P)" -validIOA_def: - "validIOA A P == ! ex : executions A . (ex \ P)" +definition validTE :: "('a, 's) ioa_temp \ bool" + where "validTE P \ (\ex. (ex \ P))" + +definition validIOA :: "('a, 's) ioa \ ('a, 's) ioa_temp \ bool" + where "validIOA A P \ (\ex \ executions A. (ex \ P))" -axiomatization where +axiomatization +where mkfin_UU: "mkfin UU = nil" and @@ -97,36 +75,35 @@ subsection \ex2seqC\ -lemma ex2seqC_unfold: "ex2seqC = (LAM ex. (%s. case ex of - nil => (s,None,s)\nil - | x##xs => (flift1 (%pr. - (s,Some (fst pr), snd pr)\ (ex2seqC$xs) (snd pr)) - $x) +lemma ex2seqC_unfold: "ex2seqC = (LAM ex. (%s. case ex of + nil => (s,None,s)\nil + | x##xs => (flift1 (%pr. + (s,Some (fst pr), snd pr)\ (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)\nil" -apply (subst ex2seqC_unfold) -apply simp -done + apply (subst ex2seqC_unfold) + apply simp + done -lemma ex2seqC_cons: "(ex2seqC $((a,t)\xs)) s = - (s,Some a,t)\ ((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)\xs)) s = (s,Some a,t)\ ((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)\nil" -apply (simp add: ex2seq_def) -done + by (simp add: ex2seq_def) lemma ex2seq_nil: "ex2seq (s, nil) = (s,None,s)\nil" -apply (simp add: ex2seq_def) -done + by (simp add: ex2seq_def) lemma ex2seq_cons: "ex2seq (s, (a,t)\ex) = (s,Some a,t) \ 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 \pair_tac @{context} "exec" 1\) -apply (tactic \Seq_case_simp_tac @{context} "x2" 1\) -apply (tactic \pair_tac @{context} "a" 1\) -done + apply (tactic \pair_tac @{context} "exec" 1\) + apply (tactic \Seq_case_simp_tac @{context} "x2" 1\) + apply (tactic \pair_tac @{context} "a" 1\) + done subsection \Interface TL -- TLS\ -(* 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 \a\A\ t --> (Q t) |] - ==> ex \ (Init (%(s,a,t). P s) \<^bold>\ Init (%(s,a,t). s \a\A\ t) +lemma TL_TLS: + "[| ! s a t. (P s) & s \a\A\ t --> (Q t) |] + ==> ex \ (Init (%(s,a,t). P s) \<^bold>\ Init (%(s,a,t). s \a\A\ t) \<^bold>\ (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 \pair_tac @{context} "ex" 1\) -apply (tactic \Seq_case_simp_tac @{context} "x2" 1\) -apply (tactic \pair_tac @{context} "a" 1\) -apply (tactic \Seq_case_simp_tac @{context} "s" 1\) -apply (tactic \pair_tac @{context} "a" 1\) -(* TL = nil *) -apply (rule conjI) -apply (tactic \pair_tac @{context} "ex" 1\) -apply (tactic \Seq_case_tac @{context} "x2" 1\) -apply (simp add: unlift_def) -apply fast -apply (simp add: unlift_def) -apply fast -apply (simp add: unlift_def) -apply (tactic \pair_tac @{context} "a" 1\) -apply (tactic \Seq_case_simp_tac @{context} "s" 1\) -apply (tactic \pair_tac @{context} "a" 1\) -(* TL =cons *) -apply (simp add: unlift_def) + apply clarify + apply (simp split add: split_if) + (* TL = UU *) + apply (rule conjI) + apply (tactic \pair_tac @{context} "ex" 1\) + apply (tactic \Seq_case_simp_tac @{context} "x2" 1\) + apply (tactic \pair_tac @{context} "a" 1\) + apply (tactic \Seq_case_simp_tac @{context} "s" 1\) + apply (tactic \pair_tac @{context} "a" 1\) + (* TL = nil *) + apply (rule conjI) + apply (tactic \pair_tac @{context} "ex" 1\) + apply (tactic \Seq_case_tac @{context} "x2" 1\) + apply (simp add: unlift_def) + apply fast + apply (simp add: unlift_def) + apply fast + apply (simp add: unlift_def) + apply (tactic \pair_tac @{context} "a" 1\) + apply (tactic \Seq_case_simp_tac @{context} "s" 1\) + apply (tactic \pair_tac @{context} "a" 1\) + (* TL =cons *) + apply (simp add: unlift_def) -apply (tactic \pair_tac @{context} "ex" 1\) -apply (tactic \Seq_case_simp_tac @{context} "x2" 1\) -apply (tactic \pair_tac @{context} "a" 1\) -apply (tactic \Seq_case_simp_tac @{context} "s" 1\) -apply (tactic \pair_tac @{context} "a" 1\) -done + apply (tactic \pair_tac @{context} "ex" 1\) + apply (tactic \Seq_case_simp_tac @{context} "x2" 1\) + apply (tactic \pair_tac @{context} "a" 1\) + apply (tactic \Seq_case_simp_tac @{context} "s" 1\) + apply (tactic \pair_tac @{context} "a" 1\) + done end diff -r 8c6226d88ced -r 68db98c2cd97 src/HOL/HOLCF/IOA/meta_theory/Traces.thy --- 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 \ ('a, 's) pairs \ 's \ 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] \ 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 \ ('a, 's) execution set" + where "executions ioa = {e. ((fst e) \ starts_of(ioa)) \ is_exec_frag ioa e}" (* ------------------- Schedules ------------------------------ *) - -filter_act_def: - "filter_act == Map fst" +definition filter_act :: "('a, 's) pairs \ '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] \ bool" + where "has_schedule ioa sch \ (\ex \ executions ioa. sch = filter_act $ (snd ex))" -schedules_def: - "schedules ioa == {sch. has_schedule ioa sch}" +definition schedules :: "('a, 's) ioa \ '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] \ bool" + where "has_trace ioa tr = (\sch \ schedules ioa. tr = Filter (\a. a \ ext ioa) $ sch)" -traces_def: - "traces ioa == {tr. has_trace ioa tr}" - +definition traces :: "('a, 's) ioa \ 'a trace set" + where "traces ioa \ {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 \ ('a, 's) pairs \ 'a trace" + where "mk_trace ioa = (LAM tr. Filter (\a. a \ 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 \ '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 \ bool) \ 'a Seq \ bool" + where "inf_often P s \ 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 \ bool) \ 'a Seq \ bool" + where "fin_often P s \ \ 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 \ 'a set \ ('a, 's) execution \ bool" +where + "is_wfair A W ex \ + (inf_often (\x. fst x \ W) (snd ex) \ inf_often (\x. \ Enabled A W (snd x)) (snd ex))" +definition wfair_ex :: "('a, 's) ioa \ ('a, 's) execution \ bool" +where + "wfair_ex A ex \ (\W \ wfair_of A. + if Finite (snd ex) + then \ 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 \ 'a set \ ('a, 's) execution \ bool" +where + "is_sfair A W ex \ + (inf_often (\x. fst x:W) (snd ex) \ fin_often (\x. Enabled A W (snd x)) (snd ex))" +definition sfair_ex :: "('a, 's)ioa \ ('a, 's) execution \ bool" +where + "sfair_ex A ex \ (\W \ 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 \ ('a, 's) execution \ bool" + where "fair_ex A ex \ wfair_ex A ex \ 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 \ ('a, 's) execution set" + where "fairexecutions A = {ex. ex \ executions A \ fair_ex A ex}" -fairtraces_def: - "fairtraces A == {mk_trace A$(snd ex) | ex. ex:fairexecutions A}" +definition fairtraces :: "('a, 's) ioa \ 'a trace set" + where "fairtraces A = {mk_trace A $ (snd ex) | ex. ex \ 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] \ bool" (infixr "=<|" 12) +where + "(ioa1 =<| ioa2) \ + (((inputs(asig_of(ioa1)) = inputs(asig_of(ioa2))) \ + (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) \ + traces(ioa1) \ traces(ioa2))" + +definition fair_implements :: "('a, 's1) ioa \ ('a, 's2) ioa \ bool" +where + "fair_implements C A \ inp C = inp A \ out C = out A \ fairtraces C \ fairtraces A" + (* ------------------- Modules ------------------------------ *) -Execs_def: - "Execs A == (executions A, asig_of A)" +(* Execution, schedule and trace modules *) + +definition Execs :: "('a, 's) ioa \ ('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 \ '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 \ '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\xs) = (fst x) \ 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 \ xs) = - (if ((fst at):ext A) - then (fst at) \ (mk_trace A$xs) +lemma mk_trace_cons: "mk_trace A$(at \ xs) = + (if ((fst at):ext A) + then (fst at) \ (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\xs)) s = - (Def ((s,pr):trans_of A) +lemma is_exec_fragC_cons: "(is_exec_fragC A$(pr\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)\ex) = - (((s,a,t):trans_of A) & +lemma is_exec_frag_cons: "is_exec_frag A (s, (a,t)\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\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 \pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, - @{thm Forall_def}, @{thm sforall_def}] 1\) -(* main case *) -apply (auto simp add: is_trans_of_def) -done + apply (tactic \pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, + @{thm Forall_def}, @{thm sforall_def}] 1\) + (* 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 \pair_tac @{context} "x" 1\) -apply (rule execfrag_in_sig [THEN spec, THEN mp]) -apply auto -done + apply (simp add: executions_def) + apply (tactic \pair_tac @{context} "x" 1\) + 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< is_exec_frag A (s,y)" -apply (tactic \pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1\) -apply (intro strip) -apply (tactic \Seq_case_simp_tac @{context} "x" 1\) -apply (tactic \pair_tac @{context} "a" 1\) -apply auto -done + apply (tactic \pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1\) + apply (intro strip) + apply (tactic \Seq_case_simp_tac @{context} "x" 1\) + apply (tactic \pair_tac @{context} "a" 1\) + 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 \pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1\) -apply (intro strip) -apply (tactic \Seq_case_simp_tac @{context} "s" 1\) -apply (tactic \pair_tac @{context} "a" 1\) -apply auto -done + apply (tactic \pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1\) + apply (intro strip) + apply (tactic \Seq_case_simp_tac @{context} "s" 1\) + apply (tactic \pair_tac @{context} "a" 1\) + apply auto + done end