# HG changeset patch # User mueller # Date 862392015 -7200 # Node ID 981258186b712c0a3b8e40d5e32322e5899401bd # Parent cadbaef4f4a51f8b83af174334c32f1c8ed4a380 New meta theory for IOA based on HOLCF. diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/README.html --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/README.html Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,38 @@ +HOLCF/ReadMe + +

IOA: A formalization of I/O automata in HOLCF

+ +Author: Olaf Mueller
+Copyright 1997 Technische Universität München

+ +Version: 1.0
+Date: 1.05.97

+ +The distribution contains + +

+ + + + + diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/ROOT.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/ROOT.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,18 @@ +(* Title: HOL/IOA/meta_theory/ROOT.ML + ID: $Id$ + Author: Olaf Mueller + Copyright 1997 TU Muenchen + +This is the ROOT file for the formalization of a semantic model of I/O-Automata. + +See the README.html file for details. + +Should be executed in the subdirectory HOLCF/IOA/meta_theory. +*) + + +goals_limit:=1; + +loadpath := ["meta_theory"]; + +use_thy"IOA"; diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/Asig.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/Asig.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,38 @@ +(* Title: HOL/IOA/meta_theory/Asig.ML + ID: $Id$ + Author: Olaf Mueller, Tobias Nipkow & Konrad Slind + Copyright 1994,1996 TU Muenchen + +Action signatures +*) + +open Asig; + +val asig_projections = [asig_inputs_def, asig_outputs_def, asig_internals_def]; + +goal thy "!!a.[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"; +by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1); +qed"int_and_ext_is_act"; + +goal thy "!!a.[|a:externals(S)|] ==> a:actions(S)"; +by (asm_full_simp_tac (!simpset addsimps [externals_def,actions_def]) 1); +qed"ext_is_act"; + +goal thy "!!a.[|a:internals S|] ==> a:actions S"; +by (asm_full_simp_tac (!simpset addsimps [asig_internals_def,actions_def]) 1); +qed"int_is_act"; + +goal thy "(x: actions S & x : externals S) = (x: externals S)"; +by (fast_tac (!claset addSIs [ext_is_act]) 1 ); +qed"ext_and_act"; + +goal thy "!!S. [|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)"; +by (asm_full_simp_tac (!simpset addsimps [actions_def,is_asig_def,externals_def]) 1); +by (best_tac (set_cs addEs [equalityCE]) 1); +qed"not_ext_is_int"; + +goalw thy [externals_def,actions_def,is_asig_def] + "!! x. [| is_asig (S); x:internals S |] ==> x~:externals S"; +by (Asm_full_simp_tac 1); +by (best_tac (set_cs addEs [equalityCE]) 1); +qed"int_is_not_ext"; \ No newline at end of file diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/Asig.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/Asig.thy Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,45 @@ +(* Title: HOL/IOA/meta_theory/Asig.thy + ID: $Id$ + Author: Tobias Nipkow & Konrad Slind + Copyright 1994 TU Muenchen + +Action signatures +*) + +Asig = Arith + + +types + +'a signature = "('a set * 'a set * 'a set)" + +consts + actions,inputs,outputs,internals,externals + ::"'action signature => 'action set" + is_asig ::"'action signature => bool" + mk_ext_asig ::"'action signature => 'action signature" + + +defs + +asig_inputs_def "inputs == fst" +asig_outputs_def "outputs == (fst o snd)" +asig_internals_def "internals == (snd o snd)" + +actions_def + "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" + +externals_def + "externals(asig) == (inputs(asig) Un outputs(asig))" + +is_asig_def + "is_asig(triple) == + ((inputs(triple) Int outputs(triple) = {}) & + (outputs(triple) Int internals(triple) = {}) & + (inputs(triple) Int internals(triple) = {}))" + + +mk_ext_asig_def + "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})" + + +end diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/Automata.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,283 @@ +(* Title: HOLCF/IOA/meta_theory/Automata.ML + ID: $$ + Author: Olaf Mueller, Tobias Nipkow, Konrad Slind + Copyright 1994, 1996 TU Muenchen + +The I/O automata of Lynch and Tuttle. +*) + +(* Has been removed from HOL-simpset, who knows why? *) +Addsimps [Let_def]; + +open reachable; + +val ioa_projections = [asig_of_def, starts_of_def, trans_of_def]; + +(* ----------------------------------------------------------------------------------- *) + +section "asig_of, starts_of, trans_of"; + + +goal thy +"asig_of((x,y,z)) = x & starts_of((x,y,z)) = y & trans_of((x,y,z)) = z"; + by (simp_tac (!simpset addsimps ioa_projections) 1); +qed "ioa_triple_proj"; + +goalw thy [ioa_def,state_trans_def,actions_def, is_asig_def] + "!!A. [| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:act A"; + by (REPEAT(etac conjE 1)); + by (EVERY1[etac allE, etac impE, atac]); + by (Asm_full_simp_tac 1); +qed "trans_in_actions"; + +goal thy +"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"; + by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1); +qed "starts_of_par"; + + +(* ----------------------------------------------------------------------------------- *) + +section "actions and par"; + + +goal thy +"actions(asig_comp a b) = actions(a) Un actions(b)"; + by(simp_tac (!simpset addsimps + ([actions_def,asig_comp_def]@asig_projections)) 1); + by (fast_tac (set_cs addSIs [equalityI]) 1); +qed "actions_asig_comp"; + + +goal thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)"; + by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1); +qed "asig_of_par"; + + +goal thy "ext (A1||A2) = \ +\ (ext A1) Un (ext A2)"; +by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_of_par,asig_comp_def, + asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1); +by (rtac set_ext 1); +by (fast_tac set_cs 1); +qed"externals_of_par"; + +goal thy "act (A1||A2) = \ +\ (act A1) Un (act A2)"; +by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def, + asig_inputs_def,asig_outputs_def,asig_internals_def,Un_def,set_diff_def]) 1); +by (rtac set_ext 1); +by (fast_tac set_cs 1); +qed"actions_of_par"; + + +goal thy "inp (A1||A2) =\ +\ ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))"; +by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def, + asig_inputs_def,asig_outputs_def,Un_def,set_diff_def]) 1); +qed"inputs_of_par"; + +goal thy "out (A1||A2) =\ +\ (out A1) Un (out A2)"; +by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def, + asig_outputs_def,Un_def,set_diff_def]) 1); +qed"outputs_of_par"; + + +(* ---------------------------------------------------------------------------------- *) + +section "actions and compatibility"; + +goal thy"compat_ioas A B = compat_ioas B A"; +by (asm_full_simp_tac (!simpset addsimps [compat_ioas_def,compat_asigs_def,Int_commute]) 1); +auto(); +qed"compat_commute"; + +goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def] + "!! a. [| compat_ioas A1 A2; a:ext A1|] ==> a~:int A2"; +by (Asm_full_simp_tac 1); +by (best_tac (set_cs addEs [equalityCE]) 1); +qed"ext1_is_not_int2"; + +(* just commuting the previous one: better commute compat_ioas *) +goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def] + "!! a. [| compat_ioas A2 A1 ; a:ext A1|] ==> a~:int A2"; +by (Asm_full_simp_tac 1); +by (best_tac (set_cs addEs [equalityCE]) 1); +qed"ext2_is_not_int1"; + +bind_thm("ext1_ext2_is_not_act2",ext1_is_not_int2 RS int_and_ext_is_act); +bind_thm("ext1_ext2_is_not_act1",ext2_is_not_int1 RS int_and_ext_is_act); + +goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def] + "!! x. [| compat_ioas A B; x:int A |] ==> x~:ext B"; +by (Asm_full_simp_tac 1); +by (best_tac (set_cs addEs [equalityCE]) 1); +qed"intA_is_not_extB"; + +goalw thy [externals_def,actions_def,compat_ioas_def,compat_asigs_def,is_asig_def,asig_of_def] +"!! a. [| compat_ioas A B; a:int A |] ==> a ~: act B"; +by (Asm_full_simp_tac 1); +by (best_tac (set_cs addEs [equalityCE]) 1); +qed"intA_is_not_actB"; + + +(* ---------------------------------------------------------------------------------- *) + +section "invariants"; + +val [p1,p2] = goalw thy [invariant_def] + "[| !!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"; +by (rtac allI 1); +by (rtac impI 1); +by (res_inst_tac [("za","s")] reachable.induct 1); +by (atac 1); +by (etac p1 1); +by (eres_inst_tac [("s1","sa")] (p2 RS mp) 1); +by (REPEAT (atac 1)); +qed"invariantI"; + + +val [p1,p2] = goal thy + "[| !!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"; + by (fast_tac (HOL_cs addSIs [invariantI] addSDs [p1,p2]) 1); +qed "invariantI1"; + +val [p1,p2] = goalw thy [invariant_def] +"[| invariant A P; reachable A s |] ==> P(s)"; + br(p2 RS (p1 RS spec RS mp))1; +qed "invariantE"; + +(* ---------------------------------------------------------------------------------- *) + +section "restrict"; + + +goal thy "starts_of(restrict ioa acts) = starts_of(ioa) & \ +\ trans_of(restrict ioa acts) = trans_of(ioa)"; +by(simp_tac (!simpset addsimps ([restrict_def]@ioa_projections)) 1); +qed "cancel_restrict_a"; + +goal thy "reachable (restrict ioa acts) s = reachable ioa s"; +by (rtac iffI 1); +be reachable.induct 1; +by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a,reachable_0]) 1); +by (etac reachable_n 1); +by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1); +(* <-- *) +be reachable.induct 1; +by (rtac reachable_0 1); +by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1); +by (etac reachable_n 1); +by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1); +qed "cancel_restrict_b"; + +goal thy "starts_of(restrict ioa acts) = starts_of(ioa) & \ +\ trans_of(restrict ioa acts) = trans_of(ioa) & \ +\ reachable (restrict ioa acts) s = reachable ioa s"; +by (simp_tac (!simpset addsimps [cancel_restrict_a,cancel_restrict_b]) 1); +qed"cancel_restrict"; + +(* ---------------------------------------------------------------------------------- *) + +section "rename"; + + + +goal thy "!!f. s -a--(rename C f)-> t ==> (? x. Some(x) = f(a) & s -x--C-> t)"; +by (asm_full_simp_tac (!simpset addsimps [Let_def,rename_def,trans_of_def]) 1); +qed"trans_rename"; + + +goal thy "!!s.[| reachable (rename C g) s |] ==> reachable C s"; +be reachable.induct 1; +br reachable_0 1; +by(asm_full_simp_tac (!simpset addsimps [rename_def]@ioa_projections) 1); +bd trans_rename 1; +be exE 1; +be conjE 1; +be reachable_n 1; +ba 1; +qed"reachable_rename"; + + + +(* ---------------------------------------------------------------------------------- *) + +section "trans_of(A||B)"; + + +goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act A|] \ +\ ==> (fst s,a,fst t):trans_of A"; +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1); +qed"trans_A_proj"; + +goal thy "!!A.[|(s,a,t):trans_of (A||B); a:act B|] \ +\ ==> (snd s,a,snd t):trans_of B"; +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1); +qed"trans_B_proj"; + +goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act A|]\ +\ ==> fst s = fst t"; +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1); +qed"trans_A_proj2"; + +goal thy "!!A.[|(s,a,t):trans_of (A||B); a~:act B|]\ +\ ==> snd s = snd t"; +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1); +qed"trans_B_proj2"; + +goal thy "!!A.(s,a,t):trans_of (A||B) \ +\ ==> a :act A | a :act B"; +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1); +qed"trans_AB_proj"; + +goal thy "!!A. [|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)"; +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1); +qed"trans_AB"; + +goal thy "!!A. [|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)"; +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1); +qed"trans_A_notB"; + +goal thy "!!A. [|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)"; +by (asm_full_simp_tac (!simpset addsimps [Let_def,par_def,trans_of_def]) 1); +qed"trans_notA_B"; + +val trans_of_defs1 = [trans_AB,trans_A_notB,trans_notA_B]; +val trans_of_defs2 = [trans_A_proj,trans_B_proj,trans_A_proj2, + trans_B_proj2,trans_AB_proj]; + + +goal thy +"(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)))))"; + + by(simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@ + ioa_projections) + setloop (split_tac [expand_if])) 1); +qed "trans_of_par4"; + + + diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/Automata.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/Automata.thy Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,162 @@ +(* Title: HOLCF/IOA/meta_theory/Automata.thy + ID: + Author: Olaf M"uller, Konrad Slind, Tobias Nipkow + Copyright 1995, 1996 TU Muenchen + +The I/O automata of Lynch and Tuttle in HOLCF. +*) + + +Automata = Option + Asig + + +default term + +types + ('a,'s)transition = "'s * 'a * 's" + ('a,'s)ioa = "'a signature * 's set * ('a,'s)transition set" + +consts + + (* IO automata *) + state_trans::"['a signature, ('a,'s)transition set] => bool" + asig_of ::"('a,'s)ioa => 'a signature" + starts_of ::"('a,'s)ioa => 's set" + trans_of ::"('a,'s)ioa => ('a,'s)transition set" + IOA ::"('a,'s)ioa => bool" + + (* reachability and invariants *) + reachable :: "('a,'s)ioa => 's set" + invariant :: "[('a,'s)ioa, 's=>bool] => bool" + + (* binary composition of action signatures and automata *) + compat_asigs ::"['a signature, 'a signature] => bool" + asig_comp ::"['a signature, 'a signature] => 'a signature" + compat_ioas ::"[('a,'s)ioa, ('a,'t)ioa] => bool" + "||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr 10) + + (* hiding *) + restrict_asig :: "['a signature, 'a set] => 'a signature" + restrict :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa" + + (* renaming *) + rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa" + + +syntax + + "_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool" ("_ -_--_-> _" [81,81,81,81] 100) + "reachable" :: "[('a,'s)ioa, 's] => bool" + "act" :: "('a,'s)ioa => 'a set" + "ext" :: "('a,'s)ioa => 'a set" + "int" :: "('a,'s)ioa => 'a set" + "inp" :: "('a,'s)ioa => 'a set" + "out" :: "('a,'s)ioa => 'a set" + + +syntax (symbols) + + "_trans_of" :: "'s => 'a => ('a,'s)ioa => 's => bool" + ("_ \\_\\_\\\\ _" [81,81,81,81] 100) + "op ||" ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa" (infixr "\\" 10) + + +inductive "reachable C" + intrs + reachable_0 "s:(starts_of C) ==> s : reachable C" + reachable_n "[|s:reachable C; (s,a,t):trans_of C|] ==> t:reachable C" + + +translations + "s -a--A-> t" == "(s,a,t):trans_of A" + "reachable A s" == "s:reachable A" + "act A" == "actions (asig_of A)" + "ext A" == "externals (asig_of A)" + "int A" == "internals (asig_of A)" + "inp A" == "inputs (asig_of A)" + "out A" == "outputs (asig_of A)" + + +defs + +(* --------------------------------- IOA ---------------------------------*) + +state_trans_def + "state_trans asig R == + (!triple. triple:R --> fst(snd(triple)):actions(asig)) & + (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))" + + +asig_of_def "asig_of == fst" +starts_of_def "starts_of == (fst o snd)" +trans_of_def "trans_of == (snd o snd)" + +ioa_def + "IOA(ioa) == (is_asig(asig_of(ioa)) & + (~ starts_of(ioa) = {}) & + state_trans (asig_of ioa) (trans_of ioa))" + + +invariant_def "invariant A P == (!s. reachable A s --> P(s))" + + +(* ------------------------- parallel composition --------------------------*) + +compat_asigs_def + "compat_asigs a1 a2 == + (((outputs(a1) Int outputs(a2)) = {}) & + ((internals(a1) Int actions(a2)) = {}) & + ((internals(a2) Int actions(a1)) = {}))" + + +compat_ioas_def + "compat_ioas ioa1 ioa2 == compat_asigs (asig_of(ioa1)) (asig_of(ioa2))" + + +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))))" + + +par_def + "(ioa1 || ioa2) == + (asig_comp (asig_of ioa1) (asig_of ioa2), + {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)}, + {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) + in (a:act ioa1 | a:act ioa2) & + (if a:act ioa1 then + (fst(s),a,fst(t)):trans_of(ioa1) + else fst(t) = fst(s)) + & + (if a:act ioa2 then + (snd(s),a,snd(t)):trans_of(ioa2) + else snd(t) = snd(s))})" + +(* ------------------------ hiding -------------------------------------------- *) + +restrict_asig_def + "restrict_asig asig actns == + (inputs(asig) Int actns, outputs(asig) Int actns, + internals(asig) Un (externals(asig) - actns))" + + +restrict_def + "restrict ioa actns == + (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))" + +(* ------------------------- renaming ------------------------------------------- *) + +rename_def +"rename ioa ren == + (({b. ? x. Some(x)= ren(b) & x : inp ioa}, + {b. ? x. Some(x)= ren(b) & x : out ioa}, + {b. ? x. Some(x)= ren(b) & x : int ioa}), + 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)})" + + +end + diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/CompoExecs.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,262 @@ +(* Title: HOLCF/IOA/meta_theory/CompoExecs.ML + ID: + Author: Olaf M"uller + Copyright 1996 TU Muenchen + +Compositionality on Execution level. +*) + +Delsimps (ex_simps @ all_simps); +Delsimps [split_paired_All]; + +(* ----------------------------------------------------------------------------------- *) + + +section "recursive equations of operators"; + + +(* ---------------------------------------------------------------- *) +(* ProjA2 *) +(* ---------------------------------------------------------------- *) + + +goal thy "ProjA2`UU = UU"; +by (simp_tac (!simpset addsimps [ProjA2_def]) 1); +qed"ProjA2_UU"; + +goal thy "ProjA2`nil = nil"; +by (simp_tac (!simpset addsimps [ProjA2_def]) 1); +qed"ProjA2_nil"; + +goal thy "ProjA2`((a,t)>>xs) = (a,fst t) >> ProjA2`xs"; +by (simp_tac (!simpset addsimps [ProjA2_def]) 1); +qed"ProjA2_cons"; + + +(* ---------------------------------------------------------------- *) +(* ProjB2 *) +(* ---------------------------------------------------------------- *) + + +goal thy "ProjB2`UU = UU"; +by (simp_tac (!simpset addsimps [ProjB2_def]) 1); +qed"ProjB2_UU"; + +goal thy "ProjB2`nil = nil"; +by (simp_tac (!simpset addsimps [ProjB2_def]) 1); +qed"ProjB2_nil"; + +goal thy "ProjB2`((a,t)>>xs) = (a,snd t) >> ProjB2`xs"; +by (simp_tac (!simpset addsimps [ProjB2_def]) 1); +qed"ProjB2_cons"; + + + +(* ---------------------------------------------------------------- *) +(* Filter_ex2 *) +(* ---------------------------------------------------------------- *) + + +goal thy "Filter_ex2 A`UU=UU"; +by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1); +qed"Filter_ex2_UU"; + +goal thy "Filter_ex2 A`nil=nil"; +by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1); +qed"Filter_ex2_nil"; + +goal thy "Filter_ex2 A`(at >> xs) = \ +\ (if (fst at:act A) \ +\ then at >> (Filter_ex2 A`xs) \ +\ else Filter_ex2 A`xs)"; + +by (asm_full_simp_tac (!simpset addsimps [Filter_ex2_def]) 1); +qed"Filter_ex2_cons"; + + +(* ---------------------------------------------------------------- *) +(* stutter2 *) +(* ---------------------------------------------------------------- *) + + +goal thy "stutter2 A = (LAM ex. (%s. case ex of \ +\ nil => TT \ +\ | x##xs => (flift1 \ +\ (%p.(If Def ((fst p)~:act A) \ +\ then Def (s=(snd p)) \ +\ else TT fi) \ +\ andalso (stutter2 A`xs) (snd p)) \ +\ `x) \ +\ ))"; +by (rtac trans 1); +br fix_eq2 1; +br stutter2_def 1; +br beta_cfun 1; +by (simp_tac (!simpset addsimps [flift1_def]) 1); +qed"stutter2_unfold"; + +goal thy "(stutter2 A`UU) s=UU"; +by (stac stutter2_unfold 1); +by (Simp_tac 1); +qed"stutter2_UU"; + +goal thy "(stutter2 A`nil) s = TT"; +by (stac stutter2_unfold 1); +by (Simp_tac 1); +qed"stutter2_nil"; + +goal thy "(stutter2 A`(at>>xs)) s = \ +\ ((if (fst at)~:act A then Def (s=snd at) else TT) \ +\ andalso (stutter2 A`xs) (snd at))"; +br trans 1; +by (stac stutter2_unfold 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def,If_and_if]) 1); +by (Simp_tac 1); +qed"stutter2_cons"; + + +Addsimps [stutter2_UU,stutter2_nil,stutter2_cons]; + + +(* ---------------------------------------------------------------- *) +(* stutter *) +(* ---------------------------------------------------------------- *) + +goal thy "stutter A (s, UU)"; +by (simp_tac (!simpset addsimps [stutter_def]) 1); +qed"stutter_UU"; + +goal thy "stutter A (s, nil)"; +by (simp_tac (!simpset addsimps [stutter_def]) 1); +qed"stutter_nil"; + +goal thy "stutter A (s, (a,t)>>ex) = \ +\ ((a~:act A --> (s=t)) & stutter A (t,ex))"; +by (simp_tac (!simpset addsimps [stutter_def] + setloop (split_tac [expand_if]) ) 1); +qed"stutter_cons"; + +(* ----------------------------------------------------------------------------------- *) + +Delsimps [stutter2_UU,stutter2_nil,stutter2_cons]; + +val compoex_simps = [ProjA2_UU,ProjA2_nil,ProjA2_cons, + ProjB2_UU,ProjB2_nil,ProjB2_cons, + Filter_ex2_UU,Filter_ex2_nil,Filter_ex2_cons, + stutter_UU,stutter_nil,stutter_cons]; + +Addsimps compoex_simps; + + + +(* ------------------------------------------------------------------ *) +(* The following lemmata aim for *) +(* COMPOSITIONALITY on EXECUTION Level *) +(* ------------------------------------------------------------------ *) + + +(* --------------------------------------------------------------------- *) +(* Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B *) +(* --------------------------------------------------------------------- *) + +goal thy "!s. is_execution_fragment (A||B) (s,xs) \ +\ --> is_execution_fragment A (fst s, Filter_ex2 A`(ProjA2`xs)) &\ +\ is_execution_fragment B (snd s, Filter_ex2 B`(ProjB2`xs))"; + +by (pair_induct_tac "xs" [is_execution_fragment_def] 1); +(* main case *) +ren "ss a t" 1; +by (safe_tac set_cs); +by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 + setloop (split_tac [expand_if])) 1)); +qed"lemma_1_1a"; + + +(* --------------------------------------------------------------------- *) +(* Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections *) +(* --------------------------------------------------------------------- *) + +goal thy "!s. is_execution_fragment (A||B) (s,xs) \ +\ --> stutter A (fst s,ProjA2`xs) &\ +\ stutter B (snd s,ProjB2`xs)"; + +by (pair_induct_tac "xs" [stutter_def,is_execution_fragment_def] 1); +(* main case *) +by (safe_tac set_cs); +by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 + setloop (split_tac [expand_if])) 1)); +qed"lemma_1_1b"; + + +(* --------------------------------------------------------------------- *) +(* Lemma_1_1c : Executions of A||B have only A- or B-actions *) +(* --------------------------------------------------------------------- *) + +goal thy "!s. (is_execution_fragment (A||B) (s,xs) \ +\ --> Forall (%x.fst x:act (A||B)) xs)"; + +by (pair_induct_tac "xs" [Forall_def,sforall_def,is_execution_fragment_def] 1); +(* main case *) +by (safe_tac set_cs); +by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @ + [actions_asig_comp,asig_of_par]) 1)); +qed"lemma_1_1c"; + + +(* ----------------------------------------------------------------------- *) +(* Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B) *) +(* ----------------------------------------------------------------------- *) + +goal thy +"!s. is_execution_fragment A (fst s,Filter_ex2 A`(ProjA2`xs)) &\ +\ is_execution_fragment B (snd s,Filter_ex2 B`(ProjB2`xs)) &\ +\ stutter A (fst s,(ProjA2`xs)) & \ +\ stutter B (snd s,(ProjB2`xs)) & \ +\ Forall (%x.fst x:act (A||B)) xs \ +\ --> is_execution_fragment (A||B) (s,xs)"; + +by (pair_induct_tac "xs" [Forall_def,sforall_def, + is_execution_fragment_def, stutter_def] 1); +(* main case *) +by (rtac allI 1); +ren "ss a t s" 1; +by (asm_full_simp_tac (!simpset addsimps trans_of_defs1 @ [actions_asig_comp,asig_of_par] + setloop (split_tac [expand_if])) 1); +by (safe_tac set_cs); +(* problem with asm_full_simp_tac: (fst s) = (fst t) is too high in assumption order ! *) +by (rotate_tac ~4 1); +by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); +by (rotate_tac ~4 1); +by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1); +qed"lemma_1_2"; + + +(* ------------------------------------------------------------------ *) +(* COMPOSITIONALITY on EXECUTION Level *) +(* Main Theorem *) +(* ------------------------------------------------------------------ *) + + +goal thy +"ex:executions(A||B) =\ +\(Filter_ex A (ProjA ex) : executions A &\ +\ Filter_ex B (ProjB ex) : executions B &\ +\ stutter A (ProjA ex) & stutter B (ProjB ex) &\ +\ Forall (%x.fst x:act (A||B)) (snd ex))"; + +by (simp_tac (!simpset addsimps [executions_def,ProjB_def, + Filter_ex_def,ProjA_def,starts_of_par]) 1); +by (pair_tac "ex" 1); +by (rtac iffI 1); +(* ==> *) +by (REPEAT (etac conjE 1)); +by (asm_full_simp_tac (!simpset addsimps [lemma_1_1a RS spec RS mp, + lemma_1_1b RS spec RS mp,lemma_1_1c RS spec RS mp]) 1); +(* <== *) +by (REPEAT (etac conjE 1)); +by (asm_full_simp_tac (!simpset addsimps [lemma_1_2 RS spec RS mp]) 1); +qed"compositionality_ex"; + + + + diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/CompoExecs.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,65 @@ +(* Title: HOLCF/IOA/meta_theory/CompoExecs.thy + ID: + Author: Olaf M"uller + Copyright 1996 TU Muenchen + +Compositionality on Execution level. +*) + +CompoExecs = Traces + + + +consts + + ProjA ::"('a,'s * 't)execution => ('a,'s)execution" + ProjA2 ::"('a,'s * 't)pairs -> ('a,'s)pairs" + ProjB ::"('a,'s * 't)execution => ('a,'t)execution" + ProjB2 ::"('a,'s * 't)pairs -> ('a,'t)pairs" + Filter_ex ::"('a,'s)ioa => ('a,'s)execution => ('a,'s)execution" + Filter_ex2 ::"('a,'s)ioa => ('a,'s)pairs -> ('a,'s)pairs" + stutter ::"('a,'s)ioa => ('a,'s)execution => bool" + stutter2 ::"('a,'s)ioa => ('a,'s)pairs -> ('s => tr)" + + +defs + + +ProjA_def + "ProjA ex == (fst (fst ex), ProjA2`(snd ex))" + +ProjB_def + "ProjB ex == (snd (fst ex), ProjB2`(snd ex))" + + +ProjA2_def + "ProjA2 == Map (%x.(fst x,fst(snd x)))" + +ProjB2_def + "ProjB2 == Map (%x.(fst x,snd(snd x)))" + + +Filter_ex_def + "Filter_ex A ex == (fst ex,Filter_ex2 A`(snd ex))" + + +Filter_ex2_def + "Filter_ex2 A == Filter (%x.fst x:act A)" + +stutter_def + "stutter A ex == ((stutter2 A`(snd ex)) (fst ex) ~= FF)" + +stutter2_def + "stutter2 A ==(fix`(LAM h ex. (%s. case ex of + nil => TT + | x##xs => (flift1 + (%p.(If Def ((fst p)~:act A) + then Def (s=(snd p)) + else TT fi) + andalso (h`xs) (snd p)) + `x) + )))" + + + + +end \ No newline at end of file diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/CompoScheds.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,503 @@ +(* Title: HOLCF/IOA/meta_theory/CompoScheds.ML + ID: + Author: Olaf M"uller + Copyright 1996 TU Muenchen + +Compositionality on Schedule level. +*) + + + +Addsimps [surjective_pairing RS sym]; + + + +(* ------------------------------------------------------------------------------- *) + +section "mkex rewrite rules"; + +(* ---------------------------------------------------------------- *) +(* mkex2 *) +(* ---------------------------------------------------------------- *) + + +bind_thm ("mkex2_unfold", fix_prover2 thy mkex2_def +"mkex2 A B = (LAM sch exA exB. (%s t. case sch of \ +\ nil => nil \ +\ | x##xs => \ +\ (case x of \ +\ Undef => UU \ +\ | Def y => \ +\ (if y:act A then \ +\ (if y:act B then \ +\ (case HD`exA of \ +\ Undef => UU \ +\ | Def a => (case HD`exB of \ +\ Undef => UU \ +\ | Def b => \ +\ (y,(snd a,snd b))>> \ +\ (mkex2 A B`xs`(TL`exA)`(TL`exB)) (snd a) (snd b))) \ +\ else \ +\ (case HD`exA of \ +\ Undef => UU \ +\ | Def a => \ +\ (y,(snd a,t))>>(mkex2 A B`xs`(TL`exA)`exB) (snd a) t) \ +\ ) \ +\ else \ +\ (if y:act B then \ +\ (case HD`exB of \ +\ Undef => UU \ +\ | Def b => \ +\ (y,(s,snd b))>>(mkex2 A B`xs`exA`(TL`exB)) s (snd b)) \ +\ else \ +\ UU \ +\ ) \ +\ ) \ +\ )))"); + + +goal thy "(mkex2 A B`UU`exA`exB) s t = UU"; +by (stac mkex2_unfold 1); +by (Simp_tac 1); +qed"mkex2_UU"; + +goal thy "(mkex2 A B`nil`exA`exB) s t= nil"; +by (stac mkex2_unfold 1); +by (Simp_tac 1); +qed"mkex2_nil"; + +goal thy "!!x.[| x:act A; x~:act B; HD`exA=Def a|] \ +\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \ +\ (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t"; +br trans 1; +by (stac mkex2_unfold 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1); +qed"mkex2_cons_1"; + +goal thy "!!x.[| x~:act A; x:act B; HD`exB=Def b|] \ +\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \ +\ (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)"; +br trans 1; +by (stac mkex2_unfold 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1); +qed"mkex2_cons_2"; + +goal thy "!!x.[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \ +\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \ +\ (x,snd a,snd b) >> \ +\ (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)"; +br trans 1; +by (stac mkex2_unfold 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1); +qed"mkex2_cons_3"; + +Addsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3]; + + +(* ---------------------------------------------------------------- *) +(* mkex *) +(* ---------------------------------------------------------------- *) + +goal thy "mkex A B UU (s,exA) (t,exB) = ((s,t),UU)"; +by (simp_tac (!simpset addsimps [mkex_def]) 1); +qed"mkex_UU"; + +goal thy "mkex A B nil (s,exA) (t,exB) = ((s,t),nil)"; +by (simp_tac (!simpset addsimps [mkex_def]) 1); +qed"mkex_nil"; + +goal thy "!!x.[| x:act A; x~:act B |] \ +\ ==> mkex A B (x>>sch) (s,a>>exA) (t,exB) = \ +\ ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))"; +by (simp_tac (!simpset addsimps [mkex_def] + setloop (split_tac [expand_if]) ) 1); +by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1); +auto(); +qed"mkex_cons_1"; + +goal thy "!!x.[| x~:act A; x:act B |] \ +\ ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) = \ +\ ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))"; +by (simp_tac (!simpset addsimps [mkex_def] + setloop (split_tac [expand_if]) ) 1); +by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1); +auto(); +qed"mkex_cons_2"; + +goal thy "!!x.[| x:act A; x:act B |] \ +\ ==> mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = \ +\ ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))"; +by (simp_tac (!simpset addsimps [mkex_def] + setloop (split_tac [expand_if]) ) 1); +by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1); +auto(); +qed"mkex_cons_3"; + +Delsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3]; + +val composch_simps = [mkex_UU,mkex_nil, + mkex_cons_1,mkex_cons_2,mkex_cons_3]; + +Addsimps composch_simps; + + + +(* ------------------------------------------------------------------ *) +(* The following lemmata aim for *) +(* COMPOSITIONALITY on SCHEDULE Level *) +(* ------------------------------------------------------------------ *) + +(* ---------------------------------------------------------------------- *) + section "Lemmas for ==>"; +(* ----------------------------------------------------------------------*) + +(* --------------------------------------------------------------------- *) +(* Lemma_2_1 : tfilter(ex) and filter_act are commutative *) +(* --------------------------------------------------------------------- *) + +goalw thy [filter_act_def,Filter_ex2_def] + "filter_act`(Filter_ex2 A`xs)=\ +\ Filter (%a.a:act A)`(filter_act`xs)"; + +by (simp_tac (!simpset addsimps [MapFilter,o_def]) 1); +qed"lemma_2_1a"; + + +(* --------------------------------------------------------------------- *) +(* Lemma_2_2 : State-projections do not affect filter_act *) +(* --------------------------------------------------------------------- *) + +goal thy + "filter_act`(ProjA2`xs) =filter_act`xs &\ +\ filter_act`(ProjB2`xs) =filter_act`xs"; + +by (pair_induct_tac "xs" [] 1); +qed"lemma_2_1b"; + + +(* --------------------------------------------------------------------- *) +(* Schedules of A||B have only A- or B-actions *) +(* --------------------------------------------------------------------- *) + +(* FIX: very similar to lemma_1_1c, but it is not checking if every action element of + an ex is in A or B, but after projecting it onto the action schedule. Of course, this + is the same proposition, but we cannot change this one, when then rather lemma_1_1c *) + +goal thy "!s. is_execution_fragment (A||B) (s,xs) \ +\ --> Forall (%x.x:act (A||B)) (filter_act`xs)"; + +by (pair_induct_tac "xs" [is_execution_fragment_def,Forall_def,sforall_def] 1); +(* main case *) +by (safe_tac set_cs); +by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @ + [actions_asig_comp,asig_of_par]) 1)); +qed"sch_actions_in_AorB"; + + +(* --------------------------------------------------------------------------*) + section "Lemmas for <=="; +(* ---------------------------------------------------------------------------*) + +(*--------------------------------------------------------------------------- + Filtering actions out of mkex(sch,exA,exB) yields the oracle sch + structural induction + --------------------------------------------------------------------------- *) + +goal thy "! exA exB s t. \ +\ Forall (%x.x:act (A||B)) sch & \ +\ Filter (%a.a:act A)`sch << filter_act`exA &\ +\ Filter (%a.a:act B)`sch << filter_act`exB \ +\ --> filter_act`(snd (mkex A B sch (s,exA) (t,exB))) = sch"; + +by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1); + +(* main case *) +(* splitting into 4 cases according to a:A, a:B *) +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1); +by (safe_tac set_cs); + +(* Case y:A, y:B *) +by (Seq_case_simp_tac "exA" 1); +(* Case exA=UU, Case exA=nil*) +(* These UU and nil cases are the only places where the assumption filter A sch< to generate a contradiction using ~a>>ss<< UU(nil), using theorems + Cons_not_less_UU and Cons_not_less_nil *) +by (Seq_case_simp_tac "exB" 1); +(* Case exA=a>>x, exB=b>>y *) +(* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case, + as otherwise mkex_cons_3 would not be rewritten without use of rotate_tac: then tactic + would not be generally applicable *) +by (Asm_full_simp_tac 1); + +(* Case y:A, y~:B *) +by (Seq_case_simp_tac "exB" 1); +by (Asm_full_simp_tac 1); + +(* Case y~:A, y:B *) +by (Seq_case_simp_tac "exA" 1); +by (Asm_full_simp_tac 1); + +(* Case y~:A, y~:B *) +by (asm_full_simp_tac (!simpset addsimps [asig_of_par,actions_asig_comp]) 1); +qed"Mapfst_mkex_is_sch"; + + +(* generalizing the proof above to a tactic *) + +fun mkex_induct_tac sch exA exB = + EVERY1[Seq_induct_tac sch [Filter_def,Forall_def,sforall_def,mkex_def,stutter_def], + asm_full_simp_tac (!simpset setloop split_tac [expand_if]), + SELECT_GOAL (safe_tac set_cs), + Seq_case_simp_tac exA, + Seq_case_simp_tac exB, + Asm_full_simp_tac, + Seq_case_simp_tac exB, + Asm_full_simp_tac, + Seq_case_simp_tac exA, + Asm_full_simp_tac, + asm_full_simp_tac (!simpset addsimps [asig_of_par,actions_asig_comp]) + ]; + + + +(*--------------------------------------------------------------------------- + Projection of mkex(sch,exA,exB) onto A stutters on A + structural induction + --------------------------------------------------------------------------- *) + + +goal thy "! exA exB s t. \ +\ Forall (%x.x:act (A||B)) sch & \ +\ Filter (%a.a:act A)`sch << filter_act`exA &\ +\ Filter (%a.a:act B)`sch << filter_act`exB \ +\ --> stutter A (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))"; + +by (mkex_induct_tac "sch" "exA" "exB"); + +qed"stutterA_mkex"; + + +goal thy "!! sch.[| \ +\ Forall (%x.x:act (A||B)) sch ; \ +\ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\ +\ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \ +\ ==> stutter A (ProjA (mkex A B sch exA exB))"; + +by (cut_facts_tac [stutterA_mkex] 1); +by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjA_def,mkex_def]) 1); +by (REPEAT (etac allE 1)); +bd mp 1; +ba 2; +by (Asm_full_simp_tac 1); +qed"stutter_mkex_on_A"; + + +(*--------------------------------------------------------------------------- + Projection of mkex(sch,exA,exB) onto B stutters on B + structural induction + --------------------------------------------------------------------------- *) + +goal thy "! exA exB s t. \ +\ Forall (%x.x:act (A||B)) sch & \ +\ Filter (%a.a:act A)`sch << filter_act`exA &\ +\ Filter (%a.a:act B)`sch << filter_act`exB \ +\ --> stutter B (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))"; + +by (mkex_induct_tac "sch" "exA" "exB"); + +qed"stutterB_mkex"; + + +goal thy "!! sch.[| \ +\ Forall (%x.x:act (A||B)) sch ; \ +\ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\ +\ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \ +\ ==> stutter B (ProjB (mkex A B sch exA exB))"; + +by (cut_facts_tac [stutterB_mkex] 1); +by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjB_def,mkex_def]) 1); +by (REPEAT (etac allE 1)); +bd mp 1; +ba 2; +by (Asm_full_simp_tac 1); +qed"stutter_mkex_on_B"; + + +(*--------------------------------------------------------------------------- + Filter of mkex(sch,exA,exB) to A after projection onto A is exA + -- using zip`(proj1`exA)`(proj2`exA) instead of exA -- + -- because of admissibility problems -- + structural induction + --------------------------------------------------------------------------- *) + +goal thy "! exA exB s t. \ +\ Forall (%x.x:act (A||B)) sch & \ +\ Filter (%a.a:act A)`sch << filter_act`exA &\ +\ Filter (%a.a:act B)`sch << filter_act`exB \ +\ --> Filter_ex2 A`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) = \ +\ Zip`(Filter (%a.a:act A)`sch)`(Map snd`exA)"; + +by (mkex_induct_tac "sch" "exA" "exB"); + +qed"filter_mkex_is_exA_tmp"; + +(*--------------------------------------------------------------------------- + zip`(proj1`y)`(proj2`y) = y (using the lift operations) + lemma for admissibility problems + --------------------------------------------------------------------------- *) + +goal thy "Zip`(Map fst`y)`(Map snd`y) = y"; +by (Seq_induct_tac "y" [] 1); +qed"Zip_Map_fst_snd"; + + +(*--------------------------------------------------------------------------- + filter A`sch = proj1`ex --> zip`(filter A`sch)`(proj2`ex) = ex + lemma for eliminating non admissible equations in assumptions + --------------------------------------------------------------------------- *) + +goal thy "!! sch ex. \ +\ Filter (%a.a:act AB)`sch = filter_act`ex \ +\ ==> ex = Zip`(Filter (%a.a:act AB)`sch)`(Map snd`ex)"; +by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 1); +by (rtac (Zip_Map_fst_snd RS sym) 1); +qed"trick_against_eq_in_ass"; + +(*--------------------------------------------------------------------------- + Filter of mkex(sch,exA,exB) to A after projection onto A is exA + using the above trick + --------------------------------------------------------------------------- *) + + +goal thy "!!sch exA exB.\ +\ [| Forall (%a.a:act (A||B)) sch ; \ +\ Filter (%a.a:act A)`sch = filter_act`(snd exA) ;\ +\ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\ +\ ==> Filter_ex A (ProjA (mkex A B sch exA exB)) = exA"; +by (asm_full_simp_tac (!simpset addsimps [ProjA_def,Filter_ex_def]) 1); +by (pair_tac "exA" 1); +by (pair_tac "exB" 1); +br conjI 1; +by (simp_tac (!simpset addsimps [mkex_def]) 1); +by (stac trick_against_eq_in_ass 1); +back(); +ba 1; +by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exA_tmp]) 1); +qed"filter_mkex_is_exA"; + + +(*--------------------------------------------------------------------------- + Filter of mkex(sch,exA,exB) to B after projection onto B is exB + -- using zip`(proj1`exB)`(proj2`exB) instead of exB -- + -- because of admissibility problems -- + structural induction + --------------------------------------------------------------------------- *) + + +goal thy "! exA exB s t. \ +\ Forall (%x.x:act (A||B)) sch & \ +\ Filter (%a.a:act A)`sch << filter_act`exA &\ +\ Filter (%a.a:act B)`sch << filter_act`exB \ +\ --> Filter_ex2 B`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) = \ +\ Zip`(Filter (%a.a:act B)`sch)`(Map snd`exB)"; + +(* notice necessary change of arguments exA and exB *) +by (mkex_induct_tac "sch" "exB" "exA"); + +qed"filter_mkex_is_exB_tmp"; + + +(*--------------------------------------------------------------------------- + Filter of mkex(sch,exA,exB) to A after projection onto B is exB + using the above trick + --------------------------------------------------------------------------- *) + + +goal thy "!!sch exA exB.\ +\ [| Forall (%a.a:act (A||B)) sch ; \ +\ Filter (%a.a:act A)`sch = filter_act`(snd exA) ;\ +\ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\ +\ ==> Filter_ex B (ProjB (mkex A B sch exA exB)) = exB"; +by (asm_full_simp_tac (!simpset addsimps [ProjB_def,Filter_ex_def]) 1); +by (pair_tac "exA" 1); +by (pair_tac "exB" 1); +br conjI 1; +by (simp_tac (!simpset addsimps [mkex_def]) 1); +by (stac trick_against_eq_in_ass 1); +back(); +ba 1; +by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exB_tmp]) 1); +qed"filter_mkex_is_exB"; + +(* --------------------------------------------------------------------- *) +(* mkex has only A- or B-actions *) +(* --------------------------------------------------------------------- *) + + +goal thy "!s t exA exB. \ +\ Forall (%x. x : act (A || B)) sch &\ +\ Filter (%a.a:act A)`sch << filter_act`exA &\ +\ Filter (%a.a:act B)`sch << filter_act`exB \ +\ --> Forall (%x.fst x : act (A ||B)) \ +\ (snd (mkex A B sch (s,exA) (t,exB)))"; + +by (mkex_induct_tac "sch" "exA" "exB"); + +qed"mkex_actions_in_AorB"; + + +(* ------------------------------------------------------------------ *) +(* COMPOSITIONALITY on SCHEDULE Level *) +(* Main Theorem *) +(* ------------------------------------------------------------------ *) + +goal thy +"sch : schedules (A||B) = \ +\ (Filter (%a.a:act A)`sch : schedules A &\ +\ Filter (%a.a:act B)`sch : schedules B &\ +\ Forall (%x. x:act (A||B)) sch)"; + +by (simp_tac (!simpset addsimps [schedules_def, has_schedule_def]) 1); +by (safe_tac set_cs); +(* ==> *) +by (res_inst_tac [("x","Filter_ex A (ProjA ex)")] bexI 1); +by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2); +by (simp_tac (!simpset addsimps [Filter_ex_def,ProjA_def, + lemma_2_1a,lemma_2_1b]) 1); +by (res_inst_tac [("x","Filter_ex B (ProjB ex)")] bexI 1); +by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2); +by (simp_tac (!simpset addsimps [Filter_ex_def,ProjB_def, + lemma_2_1a,lemma_2_1b]) 1); +by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1); +by (pair_tac "ex" 1); +be conjE 1; +by (asm_full_simp_tac (!simpset addsimps [sch_actions_in_AorB]) 1); + +(* <== *) + +(* mkex is exactly the construction of exA||B out of exA, exB, and the oracle sch, + we need here *) +ren "exA exB" 1; +by (res_inst_tac [("x","mkex A B sch exA exB")] bexI 1); +(* mkex actions are just the oracle *) +by (pair_tac "exA" 1); +by (pair_tac "exB" 1); +by (asm_full_simp_tac (!simpset addsimps [Mapfst_mkex_is_sch]) 1); + +(* mkex is an execution -- use compositionality on ex-level *) +by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 1); +by (asm_full_simp_tac (!simpset addsimps + [stutter_mkex_on_A, stutter_mkex_on_B, + filter_mkex_is_exB,filter_mkex_is_exA]) 1); +by (pair_tac "exA" 1); +by (pair_tac "exB" 1); +by (asm_full_simp_tac (!simpset addsimps [mkex_actions_in_AorB]) 1); +qed"compositionality_sch"; + + + +Delsimps compoex_simps; +Delsimps composch_simps; \ No newline at end of file diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/CompoScheds.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,63 @@ +(* Title: HOLCF/IOA/meta_theory/CompoScheds.thy + ID: + Author: Olaf M"uller + Copyright 1996 TU Muenchen + +Compositionality on Schedule level. +*) + +CompoScheds = CompoExecs + + + + +consts + + mkex ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq => + ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution" + mkex2 ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> + ('a,'s)pairs -> ('a,'t)pairs -> + ('s => 't => ('a,'s*'t)pairs)" + + +defs + +mkex_def + "mkex A B sch exA exB == + ((fst exA,fst exB), + (mkex2 A B`sch`(snd exA)`(snd exB)) (fst exA) (fst exB))" + +mkex2_def + "mkex2 A B == (fix`(LAM h sch exA exB. (%s t. case sch of + nil => nil + | x##xs => + (case x of + Undef => UU + | Def y => + (if y:act A then + (if y:act B then + (case HD`exA of + Undef => UU + | Def a => (case HD`exB of + Undef => UU + | Def b => + (y,(snd a,snd b))>> + (h`xs`(TL`exA)`(TL`exB)) (snd a) (snd b))) + else + (case HD`exA of + Undef => UU + | Def a => + (y,(snd a,t))>>(h`xs`(TL`exA)`exB) (snd a) t) + ) + else + (if y:act B then + (case HD`exB of + Undef => UU + | Def b => + (y,(s,snd b))>>(h`xs`exA`(TL`exB)) s (snd b)) + else + UU + ) + ) + ))))" + +end \ No newline at end of file diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/CompoTraces.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,734 @@ +(* Title: HOLCF/IOA/meta_theory/CompoTraces.ML + ID: + Author: Olaf M"uller + Copyright 1996 TU Muenchen + +Compositionality on Trace level. +*) + +(* FIX:Proof and add in Sequence.ML *) +Addsimps [Finite_Conc]; + + +(* +Addsimps [forall_cons]; + +Addsimps [(* LastActExtsmall1, LastActExtsmall2, looping !! *) ext_and_act]; +*) + +fun thin_tac' j = + rotate_tac (j - 1) THEN' + etac thin_rl THEN' + rotate_tac (~ (j - 1)); + + + +(* ---------------------------------------------------------------- *) + section "mksch rewrite rules"; +(* ---------------------------------------------------------------- *) + + + + +bind_thm ("mksch_unfold", fix_prover2 thy mksch_def +"mksch A B = (LAM tr schA schB. case tr of \ +\ nil => nil\ +\ | x##xs => \ +\ (case x of \ +\ Undef => 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 \ +\ ) \ +\ ) \ +\ ))"); + + +goal thy "mksch A B`UU`schA`schB = UU"; +by (stac mksch_unfold 1); +by (Simp_tac 1); +qed"mksch_UU"; + +goal thy "mksch A B`nil`schA`schB = nil"; +by (stac mksch_unfold 1); +by (Simp_tac 1); +qed"mksch_nil"; + +goal thy "!!x.[|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))"; +br trans 1; +by (stac mksch_unfold 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1); +by (simp_tac (!simpset addsimps [Cons_def]) 1); +qed"mksch_cons1"; + +goal thy "!!x.[|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)) \ +\ ))"; +br trans 1; +by (stac mksch_unfold 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1); +by (simp_tac (!simpset addsimps [Cons_def]) 1); +qed"mksch_cons2"; + +goal thy "!!x.[|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)))) \ +\ )"; +br trans 1; +by (stac mksch_unfold 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1); +by (simp_tac (!simpset addsimps [Cons_def]) 1); +qed"mksch_cons3"; + +val compotr_simps =[mksch_UU,mksch_nil, mksch_cons1,mksch_cons2,mksch_cons3]; + +Addsimps compotr_simps; + + +(* ------------------------------------------------------------------ *) +(* The following lemmata aim for *) +(* COMPOSITIONALITY on TRACE Level *) +(* ------------------------------------------------------------------ *) + + +(* ---------------------------------------------------------------------------- *) +(* Specifics for "==>" *) +(* ---------------------------------------------------------------------------- *) + +(* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of + the compatibility of IOA, in particular out of the condition that internals are + really hidden. *) + +goal thy "(eB & ~eA --> ~A) --> \ +\ (A & (eA | eB)) = (eA & A)"; +by (Fast_tac 1); +qed"compatibility_consequence1"; + + +(* very similar to above, only the commutativity of | is used to make a slight change *) + +goal thy "(eB & ~eA --> ~A) --> \ +\ (A & (eB | eA)) = (eA & A)"; +by (Fast_tac 1); +qed"compatibility_consequence2"; + + +goal thy "!!x. [| x = nil; y = z|] ==> (x @@ y) = z"; +auto(); +qed"nil_and_tconc"; + +(* FIX: should be easy to get out of lemma before *) +goal thy "!!x. [| x = nil; f`y = f`z|] ==> f`(x @@ y) = f`z"; +auto(); +qed"nil_and_tconc_f"; + +(* FIX: should be something like subst: or better improve simp_tac so that these lemmat are + superfluid *) +goal thy "!!x. [| x1 = x2; f`(x2 @@ y) = f`z|] ==> f`(x1 @@ y) = f`z"; +auto(); +qed"tconcf"; + + + +(* + + +(* -------------------------------------------------------------------------------- *) + + +goal thy "!!A B. compat_ioas A B ==> \ +\ ! schA schB. Forall (%x. x:act (A||B)) tr \ +\ --> Forall (%x. x:act (A||B)) (mksch A B`tr`schA`schB)"; +by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); +by (safe_tac set_cs); +by (asm_full_simp_tac (!simpset addsimps [actions_of_par]) 1); +by (case_tac "a:act A" 1); +by (case_tac "a:act B" 1); +(* a:A, a:B *) +by (Asm_full_simp_tac 1); +br (Forall_Conc_impl RS mp) 1; +by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1); +br (Forall_Conc_impl RS mp) 1; +by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1); +(* a:A,a~:B *) +by (Asm_full_simp_tac 1); +br (Forall_Conc_impl RS mp) 1; +by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1); +by (case_tac "a:act B" 1); +(* a~:A, a:B *) +by (Asm_full_simp_tac 1); +br (Forall_Conc_impl RS mp) 1; +by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1); +(* a~:A,a~:B *) +auto(); +qed"ForallAorB_mksch"; + + +goal thy "!!A B. compat_ioas A B ==> \ +\ ! 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))"; + +by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); +by (safe_tac set_cs); +br (Forall_Conc_impl RS mp) 1; +by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1); +qed"ForallBnA_mksch"; + +goal thy "!!A B. compat_ioas B A ==> \ +\ ! 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))"; + +by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); +by (safe_tac set_cs); +by (Asm_full_simp_tac 1); +br (Forall_Conc_impl RS mp) 1; +by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1); +qed"ForallAnB_mksch"; + + +(* ------------------------------------------------------------------------------------ *) + +(* +goal thy "!! tr. Finite tr ==> \ +\ ! x 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)"; + +be Seq_Finite_ind 1; +by (Asm_full_simp_tac 1); +(* main case *) +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1); +by (safe_tac set_cs); +by (Asm_full_simp_tac 1); + + + +qed"FiniteL_mksch"; + +goal thy " !!bs. Finite bs ==> \ +\ 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)"; +be Seq_Finite_ind 1; +by (rtac impI 1); +by (res_inst_tac [("x","nil")] exI 1); +by (res_inst_tac [("x","y")] exI 1); +by (Asm_full_simp_tac 1); +(* main case *) +by (rtac impI 1); +by (Asm_full_simp_tac 1); +by (REPEAT (etac conjE 1)); + + + + + +qed"reduce_mksch"; + +*) + + +(* Lemma for substitution of looping assumption in another specific assumption *) +val [p1,p2] = goal thy "[| f << (g x) ; x=(h x) |] ==> f << g (h x)"; +by (cut_facts_tac [p1] 1); +be (p2 RS subst) 1; +qed"subst_lemma1"; + + + + + +(*--------------------------------------------------------------------------- + Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr + structural induction + --------------------------------------------------------------------------- *) + +goal thy "! schA schB. compat_ioas A B & compat_ioas B A &\ +\ is_asig(asig_of A) & is_asig(asig_of B) &\ +\ 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"; + +by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); + +(* main case *) +(* splitting into 4 cases according to a:A, a:B *) +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1); +by (safe_tac set_cs); + +(* Case a:A, a:B *) +by (forward_tac [divide_Seq] 1); +by (forward_tac [divide_Seq] 1); +back(); +by (REPEAT (etac conjE 1)); +(* filtering internals of A is nil *) +br nil_and_tconc 1; +br FilterPTakewhileQnil 1; +by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1); +by (asm_full_simp_tac (!simpset addsimps [externals_of_par, + intA_is_not_extB,int_is_not_ext]) 1); +(* end*) +(* filtering internals of B is nil *) +(* FIX: should be done by simp_tac and claset combined until end*) +br nil_and_tconc 1; +br FilterPTakewhileQnil 1; +by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1); +by (asm_full_simp_tac (!simpset addsimps [externals_of_par, + intA_is_not_extB,int_is_not_ext]) 1); +(* end*) +(* conclusion of IH ok, but assumptions of IH have to be transformed *) +by (dres_inst_tac [("x","schA")] subst_lemma1 1); +ba 1; +by (dres_inst_tac [("x","schB")] subst_lemma1 1); +ba 1; +by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 1); + +(* Case a:B, a~:A *) + +by (forward_tac [divide_Seq] 1); +by (REPEAT (etac conjE 1)); +(* filtering internals of A is nil *) +(* FIX: should be done by simp_tac and claset combined until end*) +br nil_and_tconc 1; +br FilterPTakewhileQnil 1; +by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1); +by (asm_full_simp_tac (!simpset addsimps [externals_of_par, + intA_is_not_extB,int_is_not_ext]) 1); +(* end*) +by (dres_inst_tac [("x","schB")] subst_lemma1 1); +back(); +ba 1; +by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 1); + +(* Case a:A, a~:B *) + +by (forward_tac [divide_Seq] 1); +by (REPEAT (etac conjE 1)); +(* filtering internals of A is nil *) +(* FIX: should be done by simp_tac and claset combined until end*) +br nil_and_tconc 1; +br FilterPTakewhileQnil 1; +by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1); +by (asm_full_simp_tac (!simpset addsimps [externals_of_par, + intA_is_not_extB,int_is_not_ext]) 1); +(* end*) +by (dres_inst_tac [("x","schA")] subst_lemma1 1); +ba 1; +by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 1); + +(* Case a~:A, a~:B *) + +by (fast_tac (!claset addSIs [ext_is_act] + addss (!simpset addsimps [externals_of_par]) ) 1); +qed"filterA_mksch_is_tr"; + + + + +goal thy "!!x y. [|x=UU; y=UU|] ==> x=y"; +auto(); +qed"both_UU"; + +goal thy "!!x y. [|x=nil; y=nil|] ==> x=y"; +auto(); +qed"both_nil"; + + +(* FIX: does it exist already? *) +(* To eliminate representation a##xs, if only ~=UU & ~=nil is needed *) +goal thy "!!tr. [|tr=a##xs; a~=UU |] ==> tr~=UU & tr~=nil"; + by (Asm_full_simp_tac 1); +qed"yields_not_UU_or_nil"; + + + + + +(*--------------------------------------------------------------------------- + Filter of mksch(tr,schA,schB) to A is schA + take lemma + --------------------------------------------------------------------------- *) + +goal thy "compat_ioas A B & compat_ioas B A &\ +\ Forall (%x.x:ext (A||B)) tr & \ +\ 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 schA & LastActExtsch schB \ +\ --> Filter (%a.a:act A)`(mksch A B`tr`schA`schB) = schA"; + + +by (res_inst_tac [("Q","%x. x:act B & x~:act A")] take_lemma_less_induct 1); + + +(*--------------------------------------------------------------------------- + Filter of mksch(tr,schA,schB) to A is schA + take lemma + --------------------------------------------------------------------------- *) + +goal thy "! schA schB tr. compat_ioas A B & compat_ioas B A &\ +\ forall (plift (%x.x:externals(asig_of (A||B)))) tr & \ +\ tfilter`(plift (%a.a:externals(asig_of A)))`schA = tfilter`(plift (%a.a:actions(asig_of A)))`tr &\ +\ tfilter`(plift (%a.a:externals(asig_of B)))`schB = tfilter`(plift (%a.a:actions(asig_of B)))`tr &\ +\ LastActExtsch schA & LastActExtsch schB \ +\ --> trace_take n`(tfilter`(plift (%a.a:actions(asig_of A)))`(mksch A B`tr`schA`schB)) = trace_take n`schA"; + +by (res_inst_tac[("n","n")] less_induct 1); +by (REPEAT(rtac allI 1)); +br impI 1; +by (REPEAT (etac conjE 1)); +by (res_inst_tac [("x","tr")] trace.cases 1); + +(* tr = UU *) +by (rotate_tac ~1 1); +by (Asm_full_simp_tac 1); +by (dtac LastActExtimplUU 1); +ba 1; +by (Asm_simp_tac 1); + +(* tr = nil *) +by (rotate_tac ~1 1); +by (Asm_full_simp_tac 1); +by (dtac LastActExtimplnil 1); +ba 1; +by (Asm_simp_tac 1); + +(* tr = t##ts *) + +(* just to delete tr=a##xs, as we do not make induction on a but on an element in + xs we find later *) +by (dtac yields_not_UU_or_nil 1); +ba 1; +by (REPEAT (etac conjE 1)); + +(* FIX: or use equality "hd(f ~P x)=UU = fa P x" to make distinction on that *) +by (case_tac "forall (plift (%x.x:actions(asig_of B) & x~:actions(asig_of A))) tr" 1); +(* This case holds for whole streams, not only for takes *) +br (trace_take_lemma RS iffD2 RS spec) 1; + +by (case_tac "tr : tfinite" 1); + +(* FIX: Check if new trace lemmata with ==> instead of --> allow for simplifiaction instead + of ares_tac in the following *) +br both_nil 1; +(* mksch = nil *) +by (REPEAT (ares_tac [forallQfilterPnil,forallBnA_mksch,finiteL_mksch] 1)); +by (Fast_tac 1); +(* schA = nil *) +by (eres_inst_tac [("A","A")] LastActExtimplnil 1); +by (Asm_simp_tac 1); +br forallQfilterPnil 1; +ba 1; +back(); +ba 1; +by (Fast_tac 1); + +(* case tr~:tfinite *) + +br both_UU 1; +(* mksch = UU *) +by (REPEAT (ares_tac [forallQfilterPUU,(finiteR_mksch RS mp COMP rev_contrapos), + forallBnA_mksch] 1)); +by (Fast_tac 1); +(* schA = UU *) +by (eres_inst_tac [("A","A")] LastActExtimplUU 1); +by (Asm_simp_tac 1); +br forallQfilterPUU 1; +by (REPEAT (atac 1)); +back(); +by (Fast_tac 1); + +(* case" ~ forall (plift (%x.x:actions(asig_of B) & x~:actions(asig_of A))) tr" *) + +by (dtac divide_trace3 1); +by (REPEAT (atac 1)); +by (REPEAT (etac exE 1)); +by (REPEAT (etac conjE 1)); + +(* rewrite assuption for tr *) +by (hyp_subst_tac 1); +(* bring in lemma reduce_mksch *) +by (forw_inst_tac [("y","schB"),("x","schA")] reduce_mksch 1); +ba 1; +by (asm_simp_tac HOL_min_ss 1); +by (REPEAT (etac exE 1)); +by (REPEAT (etac conjE 1)); + +(* use reduce_mksch to rewrite conclusion *) +by (hyp_subst_tac 1); +by (Asm_full_simp_tac 1); + +(* eliminate the B-only prefix *) +(* FIX: Cannot be done by + by (asm_full_simp_tac (HOL_min_ss addsimps [forallQfilterPnil]) 1); + as P&Q --> Q is looping. Perhaps forall (and other) operations not on predicates but on + sets because of this reason ?????? *) +br nil_and_tconc_f 1; +be forallQfilterPnil 1; +ba 1; +by (Fast_tac 1); + +(* Now real recursive step follows (in Def x) *) + +by (case_tac "x:actions(asig_of A)" 1); +by (case_tac "x~:actions(asig_of B)" 1); +by (rotate_tac ~2 1); +by (asm_full_simp_tac (!simpset addsimps [filter_rep]) 1); + +(* same problem as above for the B-onlu prefix *) +(* FIX: eliminate generated subgoal immeadiately ! (as in case below x:A & x: B *) +by (subgoal_tac "tfilter`(plift (%a. a : actions (asig_of A) & a : externals (asig_of B)))`y1=nil" 1); +by (rotate_tac ~1 1); +by (Asm_full_simp_tac 1); +(* eliminate introduced subgoal 2 *) +be forallQfilterPnil 2; +ba 2; +by (Fast_tac 2); + +(* f A (tw iA) = tw iA *) +by (simp_tac (HOL_min_ss addsimps [filterPtakewhileQ,int_is_act]) 1); + +by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace] 1); +(* subst divide_trace in conlcusion, but only at the righest occurence *) +by (res_inst_tac [("t","schA")] ssubst 1); +back(); +back(); +back(); +ba 1; +by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite] 1); + +by (REPEAT (etac conjE 1)); +(* reduce trace_takes from n to strictly smaller k *) +by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext]) 1); +br take_reduction 1; +ba 1; +(* now conclusion fulfills induction hypothesis, but assumptions are not ready *) +by (rotate_tac ~10 1); +(* assumption forall and schB *) +by (asm_full_simp_tac (!simpset addsimps [tconc_cong,forall_cons,forall_tconc,ext_and_act]) 1); +(* assumption schA *) +by (dres_inst_tac [("x","schA"), + ("g","tfilter`(plift (%a. a : actions (asig_of A)))`rs")] lemma22 1); +ba 1; +by (asm_full_simp_tac (!simpset addsimps [tfiltertconc,not_int_is_ext,tfilterPtakewhileQ]) 1); +by (REPEAT (etac conjE 1)); +(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *) +by (dres_inst_tac [("sch","schA"),("P","plift (%a. a : internals (asig_of A))")] LastActExtsmall1 1); +by (dres_inst_tac [("sch1.0","y1")] LastActExtsmall2 1); +ba 1; +by (Asm_full_simp_tac 1); + +(* case x:actions(asig_of A) & x: actions(asig_of B) *) +by (rotate_tac ~2 1); +by (asm_full_simp_tac (!simpset addsimps [filter_rep]) 1); +by (subgoal_tac "tfilter`(plift (%a. a : actions (asig_of A) & a : externals (asig_of B)))`y1=nil" 1); +by (rotate_tac ~1 1); +by (Asm_full_simp_tac 1); +by (thin_tac' 1 1); +(* eliminate introduced subgoal 2 *) +be forallQfilterPnil 2; +ba 2; +by (Fast_tac 2); + +(* f A (tw iA) = tw iA *) +by (simp_tac (HOL_min_ss addsimps [filterPtakewhileQ,int_is_act]) 1); + +by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace] 1); +(* subst divide_trace in conlcusion, but only at the righest occurence *) +by (res_inst_tac [("t","schA")] ssubst 1); +back(); +back(); +back(); +ba 1; +by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite] 1); +by (REPEAT (etac conjE 1)); +(* tidy up *) +by (thin_tac' 12 1); +by (thin_tac' 12 1); +by (thin_tac' 14 1); +by (thin_tac' 14 1); +by (rotate_tac ~8 1); +(* rewrite assumption forall and schB *) +by (asm_full_simp_tac (!simpset addsimps [tconc_cong,forall_cons,forall_tconc,ext_and_act]) 1); +(* divide_trace for schB2 *) +by (forw_inst_tac [("y","y2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_trace) 1); +by (forw_inst_tac [("y","y2")](sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite) 1); +by (REPEAT (etac conjE 1)); +by (rotate_tac ~6 1); +(* assumption schA *) +by (dres_inst_tac [("x","schA"), + ("g","tfilter`(plift (%a. a : actions (asig_of A)))`rs")] lemma22 1); +ba 1; +by (asm_full_simp_tac (!simpset addsimps [tfiltertconc,not_int_is_ext,tfilterPtakewhileQ]) 1); +by (REPEAT (etac conjE 1)); +(* f A (tw iB schB2) = nil *) + +(* good luck: intAisnotextB is not looping *) +by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext,tfilterPtakewhileQ,intAisnotextB]) 1); +(* reduce trace_takes from n to strictly smaller k *) +by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext]) 1); +br take_reduction 1; +ba 1; +(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *) +(* assumption schB *) +by (dres_inst_tac [("x","y2"), + ("g","tfilter`(plift (%a. a : actions (asig_of B)))`rs")] lemma22 1); +ba 1; +(* FIX: hey wonder: why does loopin rule for y2 here rewrites !!!!!!!!!!!!!!!!!!!!!!!!*) +by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext,tfilterPtakewhileQ,intAisnotextB]) 1); +by (REPEAT (etac conjE 1)); +(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping *) +by (dres_inst_tac [("sch","schA"),("P","plift (%a. a : internals (asig_of A))")] LastActExtsmall1 1); +by (dres_inst_tac [("sch1.0","y1")] LastActExtsmall2 1); +ba 1; +by (dres_inst_tac [("sch","y2"),("P","plift (%a. a : internals (asig_of B))")] LastActExtsmall1 1); +by (Asm_full_simp_tac 1); + +(* case x~:A & x:B *) +(* cannot occur, as just this case has been scheduled out before as the B-only prefix *) +by (case_tac "x:actions(asig_of B)" 1); +by (Fast_tac 1); + +(* case x~:A & x~:B *) +(* cannot occur because of assumption: forall (a:ext A | a:ext B) *) +by (rotate_tac ~8 1); +(* reduce forall assumption from tr to (Def x ## rs) *) +by (asm_full_simp_tac (!simpset addsimps [forall_cons,forall_tconc]) 1); +by (REPEAT (etac conjE 1)); +by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1); +by (fast_tac (!claset addSIs [ext_is_act]) 1); + +qed"filterAmksch_is_schA"; + + +goal thy "!! tr. [|compat_ioas A B ; compat_ioas B A ;\ +\ forall (plift (%x.x:externals(asig_of (A||B)))) tr ; \ +\ tfilter`(plift (%a.a:externals(asig_of A)))`schA = tfilter`(plift (%a.a:actions(asig_of A)))`tr ;\ +\ tfilter`(plift (%a.a:externals(asig_of B)))`schB = tfilter`(plift (%a.a:actions(asig_of B)))`tr ;\ +\ LastActExtsch schA ; LastActExtsch schB |] \ +\ ==> tfilter`(plift (%a.a:actions(asig_of A)))`(mksch A B`tr`schA`schB) = schA"; + +br trace.take_lemma 1; +by (asm_simp_tac (!simpset addsimps [filterAmksch_is_schA]) 1); +qed"filterAmkschschA"; + + + +(* ------------------------------------------------------------------ *) +(* COMPOSITIONALITY on TRACE Level *) +(* Main Theorem *) +(* ------------------------------------------------------------------ *) + +goal thy +"!! A B. [| compat_ioas A B; compat_ioas B A; \ +\ is_asig(asig_of A); is_asig(asig_of B)|] \ +\ ==> traces(A||B) = \ +\ { tr.(Filter (%a.a:act A)`tr : traces A &\ +\ Filter (%a.a:act B)`tr : traces B &\ +\ Forall (%x. x:ext(A||B)) tr) }"; + +by (simp_tac (!simpset addsimps [traces_def,has_trace_def]) 1); +br set_ext 1; +by (safe_tac set_cs); + +(* ==> *) +(* There is a schedule of A *) +by (res_inst_tac [("x","Filter (%a.a:act A)`sch")] bexI 1); +by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2); +by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence1, + externals_of_par,ext1_ext2_is_not_act1]) 1); +(* There is a schedule of B *) +by (res_inst_tac [("x","Filter (%a.a:act B)`sch")] bexI 1); +by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 2); +by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence2, + externals_of_par,ext1_ext2_is_not_act2]) 1); +(* Traces of A||B have only external actions from A or B *) +br ForallPFilterP 1; + +(* <== *) + +(* replace schA and schB by cutsch(schA) and cutsch(schB) *) +by (dtac exists_LastActExtsch 1); +ba 1; +by (dtac exists_LastActExtsch 1); +ba 1; +by (REPEAT (etac exE 1)); +by (REPEAT (etac conjE 1)); + +(* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr, + we need here *) +by (res_inst_tac [("x","mksch A B`tr`schb`schc")] bexI 1); + +(* External actions of mksch are just the oracle *) +by (asm_full_simp_tac (!simpset addsimps [filterA_mksch_is_tr]) 1); + +(* mksch is a schedule -- use compositionality on sch-level *) +by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 1); + + das hier loopt: ForallPForallQ, ext_is_act,ForallAorB_mksch]) 1); + + + + + + +*) + + + +(* ------------------------------------------------------------------------------- + Other useful things + -------------------------------------------------------------------------------- *) + + +(* Lemmata not needed yet +goal Trace.thy "!!x. nil< nil=x"; +by (res_inst_tac [("x","x")] trace.cases 1); +by (hyp_subst_tac 1); +by (etac antisym_less 1); +by (Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); +by (hyp_subst_tac 1); +by (Asm_full_simp_tac 1); +qed"nil_less_is_nil"; + + +*) + + + + diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/CompoTraces.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,91 @@ +(* Title: HOLCF/IOA/meta_theory/CompoTraces.thy + ID: + Author: Olaf M"uller + Copyright 1996 TU Muenchen + +Compositionality on Trace level. +*) + +CompoTraces = CompoScheds + ShortExecutions + + + +consts + + mksch ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq" + + +defs + +mksch_def + "mksch A B == (fix`(LAM h tr schA schB. case tr of + nil => nil + | x##xs => + (case x of + Undef => 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>>(h`xs + `(TL`(Dropwhile (%a.a:int A)`schA)) + `(TL`(Dropwhile (%a.a:int B)`schB)) + ))) + else + ((Takewhile (%a.a:int A)`schA) + @@ (y>>(h`xs + `(TL`(Dropwhile (%a.a:int A)`schA)) + `schB))) + ) + else + (if y:act B then + ((Takewhile (%a.a:int B)`schB) + @@ (y>>(h`xs + `schA + `(TL`(Dropwhile (%a.a:int B)`schB)) + ))) + else + UU + ) + ) + )))" + + +rules + +(* FIX: x:actions S is further assumption, see Asig.ML: how to fulfill this in proofs ? *) +not_ext_is_int_FIX + "[|is_asig S|] ==> (x~:externals S) = (x: internals S)" + +(* FIX: should be more general , something like subst *) +lemma12 +"[| f << (g x) ; (x= (h x)) |] ==> f << g (h x)" + +(* FIX: as above, should be done more intelligent *) +lemma22 +"[| (f x) = y >> g ; x = h x |] ==> (f (h x)) = y >> g" + +Finite_Conc + "Finite (x @@ y) = (Finite x & Finite y)" + +finiteR_mksch + "Finite (mksch A B`tr`x`y) --> Finite tr" + +finiteL_mksch + "[| Finite tr; + Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr; + Filter (%a. a:ext B)`y = Filter (%a. a:actB)`tr; + Forall (%x. x:ext (A||B)) tr |] + ==> Finite (mksch A B`tr`x`y)" + +reduce_mksch + "[| Finite bs; 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" + +end + + diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/Compositionality.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,23 @@ +(* Title: HOLCF/IOA/meta_theory/Compositionality.ML + ID: + Author: Olaf M"uller + Copyright 1997 TU Muenchen + +Compositionality of I/O automata +*) + + +goal thy "!! A1 A2 B1 B2. \ +\ [| is_asig (asig_of A1); is_asig (asig_of A2); \ +\ is_asig (asig_of B1); is_asig (asig_of B2); \ +\ compat_ioas A1 B1; compat_ioas B1 A1; compat_ioas A2 B2; compat_ioas B2 A2; \ +\ A1 =<| A2; \ +\ B1 =<| B2 |] \ +\ ==> (A1 || B1) =<| (A2 || B2)"; +by (asm_full_simp_tac (!simpset addsimps [ioa_implements_def, + inputs_of_par,outputs_of_par]) 1); + + +by (safe_tac set_cs); +by (asm_full_simp_tac (!simpset addsimps [compotraces]) 1); + diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/Compositionality.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,21 @@ +(* Title: HOLCF/IOA/meta_theory/Compositionality.thy + ID: + Author: Olaf M"uller + Copyright 1997 TU Muenchen + +Compositionality of I/O automata +*) + +Compositionality = CompoTraces + + +rules + +compotraces +"[| compat_ioas A B; compat_ioas B A; + is_asig(asig_of A); is_asig(asig_of B)|] + ==> traces(A||B) = + {tr. (Filter (%a.a:act A)`tr : traces A & + Filter (%a.a:act B)`tr : traces B & + Forall (%x. x:ext(A||B)) tr)}" + +end \ No newline at end of file diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/IOA.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/IOA.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,7 @@ +(* Title: HOLCF/IOA/meta_theory/IOA.thy + ID: + Author: Olaf Mueller + Copyright 1996,1997 TU Muenchen + +The theory of I/O automata in HOLCF. +*) \ No newline at end of file diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/IOA.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/IOA.thy Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,13 @@ +(* Title: HOLCF/IOA/meta_theory/IOA.thy + ID: + Author: Olaf Mueller + Copyright 1996,1997 TU Muenchen + +The theory of I/O automata in HOLCF. +*) + + + +IOA = RefCorrectness + Compositionality + + diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/RefCorrectness.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,292 @@ +(* Title: HOLCF/IOA/meta_theory/RefCorrectness.ML + ID: $$ + Author: Olaf Mueller + Copyright 1996 TU Muenchen + +Correctness of Refinement Mappings in HOLCF/IOA +*) + + + +(* -------------------------------------------------------------------------------- *) + +section "corresp_ex"; + + +(* ---------------------------------------------------------------- *) +(* corresp_ex2 *) +(* ---------------------------------------------------------------- *) + + +goal thy "corresp_ex2 A f = (LAM ex. (%s. case ex of \ +\ nil => nil \ +\ | x##xs => (flift1 (%pr. (snd(@cex. move A cex s (fst pr) (f (snd pr)))) \ +\ @@ ((corresp_ex2 A f `xs) (f (snd pr)))) \ +\ `x) ))"; +by (rtac trans 1); +br fix_eq2 1; +br corresp_ex2_def 1; +br beta_cfun 1; +by (simp_tac (!simpset addsimps [flift1_def]) 1); +qed"corresp_ex2_unfold"; + +goal thy "(corresp_ex2 A f`UU) s=UU"; +by (stac corresp_ex2_unfold 1); +by (Simp_tac 1); +qed"corresp_ex2_UU"; + +goal thy "(corresp_ex2 A f`nil) s = nil"; +by (stac corresp_ex2_unfold 1); +by (Simp_tac 1); +qed"corresp_ex2_nil"; + +goal thy "(corresp_ex2 A f`(at>>xs)) s = \ +\ (snd(@cex. move A cex s (fst at) (f (snd at)))) \ +\ @@ ((corresp_ex2 A f`xs) (f (snd at)))"; +br trans 1; +by (stac corresp_ex2_unfold 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1); +by (Simp_tac 1); +qed"corresp_ex2_cons"; + + +Addsimps [corresp_ex2_UU,corresp_ex2_nil,corresp_ex2_cons]; + + + +(* ------------------------------------------------------------------ *) +(* The following lemmata describe the definition *) +(* of move in more detail *) +(* ------------------------------------------------------------------ *) + +section"properties of move"; + +goalw thy [is_ref_map_def] + "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\ +\ move A (@x. move A x (f s) a (f t)) (f s) a (f t)"; + +by (subgoal_tac "? ex.move A ex (f s) a (f t)" 1); +by (Asm_full_simp_tac 2); +by (etac exE 1); +by (rtac selectI 1); +by (assume_tac 1); +qed"move_is_move"; + +goal thy + "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\ +\ is_execution_fragment A (@x. move A x (f s) a (f t))"; +by (cut_inst_tac [] move_is_move 1); +by (REPEAT (assume_tac 1)); +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1); +qed"move_subprop1"; + +goal thy + "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\ +\ Finite (snd (@x. move A x (f s) a (f t)))"; +by (cut_inst_tac [] move_is_move 1); +by (REPEAT (assume_tac 1)); +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1); +qed"move_subprop2"; + +goal thy + "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\ +\ fst (@x. move A x (f s) a (f t)) = (f s)"; +by (cut_inst_tac [] move_is_move 1); +by (REPEAT (assume_tac 1)); +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1); +qed"move_subprop3"; + +goal thy + "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\ +\ laststate (@x. move A x (f s) a (f t)) = (f t)"; +by (cut_inst_tac [] move_is_move 1); +by (REPEAT (assume_tac 1)); +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1); +qed"move_subprop4"; + +goal thy + "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\ +\ mk_trace A`(snd(@x. move A x (f s) a (f t))) = \ +\ (if a:ext A then a>>nil else nil)"; + +by (cut_inst_tac [] move_is_move 1); +by (REPEAT (assume_tac 1)); +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1); +qed"move_subprop5"; + +goal thy + "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\ +\ (is_execution_fragment A (f s,(snd (@x. move A x (f s) a (f t)))))"; +by (cut_inst_tac [] move_subprop3 1); +by (REPEAT (assume_tac 1)); +by (cut_inst_tac [] move_subprop1 1); +by (REPEAT (assume_tac 1)); +by (res_inst_tac [("s","fst (@x. move A x (f s) a (f t))")] subst 1); +back(); +back(); +back(); +ba 1; +by (simp_tac (HOL_basic_ss addsimps [surjective_pairing RS sym]) 1); +qed"move_subprop_1and3"; + +goal thy + "!!f. [|is_ref_map f C A; reachable C s; (s,a,t):trans_of C|] ==>\ +\ (case Last`(snd (@x. move A x (f s) a (f t))) of \ +\ Undef => (f s) \ +\ | Def p => snd p) = (f t)"; +by (cut_inst_tac [] move_subprop3 1); +by (REPEAT (assume_tac 1)); +by (cut_inst_tac [] move_subprop4 1); +by (REPEAT (assume_tac 1)); +by (asm_full_simp_tac (!simpset addsimps [laststate_def]) 1); +qed"move_subprop_4and3"; + + + +(* ------------------------------------------------------------------ *) +(* The following lemmata contribute to *) +(* TRACE INCLUSION Part 1: Traces coincide *) +(* ------------------------------------------------------------------ *) + +section "Lemmata for <=="; + +(* --------------------------------------------------- *) +(* Lemma 1.1: Distribution of mk_trace and @@ *) +(* --------------------------------------------------- *) + + +goal thy "mk_trace C`(ex1 @@ ex2)= (mk_trace C`ex1) @@ (mk_trace C`ex2)"; +by (simp_tac (!simpset addsimps [mk_trace_def,filter_act_def, + FilterConc,MapConc]) 1); +qed"mk_traceConc"; + + + +(* ------------------------------------------------------ + Lemma 1 :Traces coincide + ------------------------------------------------------- *) + +goalw thy [corresp_ex_def] + "!!f.[|is_ref_map f C A; ext C = ext A|] ==> \ +\ !s. reachable C s & is_execution_fragment C (s,xs) --> \ +\ mk_trace C`xs = mk_trace A`(snd (corresp_ex A f (s,xs)))"; + +by (pair_induct_tac "xs" [is_execution_fragment_def] 1); +(* cons case *) +by (safe_tac set_cs); +by (asm_full_simp_tac (!simpset addsimps [mk_traceConc]) 1); +by (forward_tac [reachable.reachable_n] 1); +ba 1; +by (eres_inst_tac [("x","y")] allE 1); +by (Asm_full_simp_tac 1); +by (asm_full_simp_tac (!simpset addsimps [move_subprop5] + setloop split_tac [expand_if] ) 1); +qed"lemma_1"; + + +(* ------------------------------------------------------------------ *) +(* The following lemmata contribute to *) +(* TRACE INCLUSION Part 2: corresp_ex is execution *) +(* ------------------------------------------------------------------ *) + +section "Lemmata for ==>"; + +(* -------------------------------------------------- *) +(* Lemma 2.1 *) +(* -------------------------------------------------- *) + +goal thy +"Finite xs --> \ +\(!s .is_execution_fragment A (s,xs) & is_execution_fragment A (t,ys) & \ +\ t = laststate (s,xs) \ +\ --> is_execution_fragment A (s,xs @@ ys))"; + +br impI 1; +by (Seq_Finite_induct_tac 1); +(* base_case *) +by (fast_tac HOL_cs 1); +(* main case *) +by (safe_tac set_cs); +by (pair_tac "a" 1); +qed"lemma_2_1"; + + +(* ----------------------------------------------------------- *) +(* Lemma 2 : corresp_ex is execution *) +(* ----------------------------------------------------------- *) + + + +goalw thy [corresp_ex_def] + "!!f.[| is_ref_map f C A |] ==>\ +\ !s. reachable C s & is_execution_fragment C (s,xs) \ +\ --> is_execution_fragment A (corresp_ex A f (s,xs))"; + +by (Asm_full_simp_tac 1); +by (pair_induct_tac "xs" [is_execution_fragment_def] 1); +(* main case *) +by (safe_tac set_cs); +by (res_inst_tac [("t3","f y")] (lemma_2_1 RS mp RS spec RS mp) 1); + +(* Finite *) +be move_subprop2 1; +by (REPEAT (atac 1)); +by (rtac conjI 1); + +(* is_execution_fragment *) +be move_subprop_1and3 1; +by (REPEAT (atac 1)); +by (rtac conjI 1); + +(* Induction hypothesis *) +(* reachable_n looping, therefore apply it manually *) +by (eres_inst_tac [("x","y")] allE 1); +by (Asm_full_simp_tac 1); +by (forward_tac [reachable.reachable_n] 1); +ba 1; +by (Asm_full_simp_tac 1); +(* laststate *) +by (simp_tac (!simpset addsimps [laststate_def]) 1); +be (move_subprop_4and3 RS sym) 1; +by (REPEAT (atac 1)); +qed"lemma_2"; + + +(* -------------------------------------------------------------------------------- *) + +section "Main Theorem: T R A C E - I N C L U S I O N"; + +(* -------------------------------------------------------------------------------- *) + + +goalw thy [traces_def] + "!!f. [| IOA C; IOA A; ext C = ext A; is_ref_map f C A |] \ +\ ==> traces C <= traces A"; + + by (simp_tac(!simpset addsimps [has_trace_def2])1); + by (safe_tac set_cs); + + (* give execution of abstract automata *) + by (res_inst_tac[("x","corresp_ex A f ex")] bexI 1); + + (* Traces coincide, Lemma 1 *) + by (pair_tac "ex" 1); + by (etac (lemma_1 RS spec RS mp) 1); + by (REPEAT (atac 1)); + by (asm_full_simp_tac (!simpset addsimps [executions_def,reachable.reachable_0]) 1); + + (* corresp_ex is execution, Lemma 2 *) + by (pair_tac "ex" 1); + by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1); + (* start state *) + by (rtac conjI 1); + by (asm_full_simp_tac (!simpset addsimps [is_ref_map_def,corresp_ex_def]) 1); + (* is-execution-fragment *) + by (etac (lemma_2 RS spec RS mp) 1); + by (asm_full_simp_tac (!simpset addsimps [reachable.reachable_0]) 1); +qed"trace_inclusion"; + + + + + diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/RefCorrectness.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,35 @@ +(* Title: HOLCF/IOA/meta_theory/RefCorrectness.thy + ID: $$ + Author: Olaf Mueller + Copyright 1996 TU Muenchen + +Correctness of Refinement Mappings in HOLCF/IOA +*) + + +RefCorrectness = RefMappings + + +consts + + corresp_ex ::"('a,'s2)ioa => ('s1 => 's2) => + ('a,'s1)execution => ('a,'s2)execution" + corresp_ex2 ::"('a,'s2)ioa => ('s1 => 's2) => ('a,'s1)pairs + -> ('s2 => ('a,'s2)pairs)" + + +defs + +corresp_ex_def + "corresp_ex A f ex == (f (fst ex),(corresp_ex2 A f`(snd ex)) (f (fst ex)))" + + +corresp_ex2_def + "corresp_ex2 A f == (fix`(LAM h ex. (%s. case ex of + nil => nil + | x##xs => (flift1 (%pr. (snd(@cex. move A cex s (fst pr) (f (snd pr)))) + @@ ((h`xs) (f (snd pr)))) + `x) )))" + + + +end \ No newline at end of file diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/RefMappings.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,132 @@ +(* Title: HOLCF/IOA/meta_theory/RefMappings.ML + ID: $$ + Author: Olaf Mueller + Copyright 1996 TU Muenchen + +Refinement Mappings in HOLCF/IOA +*) + + + +goal thy "laststate (s,UU) = s"; +by (simp_tac (!simpset addsimps [laststate_def]) 1); +qed"laststate_UU"; + +goal thy "laststate (s,nil) = s"; +by (simp_tac (!simpset addsimps [laststate_def]) 1); +qed"laststate_nil"; + +goal thy "!! ex. Finite ex ==> laststate (s,at>>ex) = laststate (snd at,ex)"; +by (simp_tac (!simpset addsimps [laststate_def]) 1); +by (case_tac "ex=nil" 1); +by (Asm_simp_tac 1); +by (Asm_simp_tac 1); +bd (Finite_Last1 RS mp) 1; +ba 1; +by (def_tac 1); +qed"laststate_cons"; + +Addsimps [laststate_UU,laststate_nil,laststate_cons]; + +(* ---------------------------------------------------------------------------- *) + +section "transitions and moves"; + + +goal thy"!!f. s -a--A-> t ==> ? ex. move A ex s a t"; + +by (res_inst_tac [("x","(s,(a,t)>>nil)")] exI 1); +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1); +qed"transition_is_ex"; + + +goal thy"!!f. (~a:ext A) & s=t ==> ? ex. move A ex s a t"; + +by (res_inst_tac [("x","(s,nil)")] exI 1); +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1); +qed"nothing_is_ex"; + + +goal thy"!!f. (s -a--A-> s') & (s' -a'--A-> s'') & (~a':ext A) \ +\ ==> ? ex. move A ex s a s''"; + +by (res_inst_tac [("x","(s,(a,s')>>(a',s'')>>nil)")] exI 1); +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1); +qed"ei_transitions_are_ex"; + + +goal thy +"!!f. (s1 -a1--A-> s2) & (s2 -a2--A-> s3) & (s3 -a3--A-> s4) &\ +\ (~a2:ext A) & (~a3:ext A) ==> \ +\ ? ex. move A ex s1 a1 s4"; + +by (res_inst_tac [("x","(s1,(a1,s2)>>(a2,s3)>>(a3,s4)>>nil)")] exI 1); +by (asm_full_simp_tac (!simpset addsimps [move_def]) 1); +qed"eii_transitions_are_ex"; + + +(* ---------------------------------------------------------------------------- *) + +section "weak_ref_map and ref_map"; + + +goalw thy [is_weak_ref_map_def,is_ref_map_def] + "!!f. [| ext C = ext A; \ +\ is_weak_ref_map f C A |] ==> is_ref_map f C A"; +by (safe_tac set_cs); +by (case_tac "a:ext A" 1); +by (rtac transition_is_ex 1); +by (Asm_simp_tac 1); +by (rtac nothing_is_ex 1); +by (Asm_simp_tac 1); +qed"weak_ref_map2ref_map"; + + +val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R"; + by(fast_tac (!claset addDs prems) 1); +qed "imp_conj_lemma"; + +goal thy "!!f.[| is_weak_ref_map f C A |]\ +\ ==> (is_weak_ref_map f (rename C g) (rename A g))"; +by (asm_full_simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1); +by (rtac conjI 1); +(* 1: start states *) +by (asm_full_simp_tac (!simpset addsimps [rename_def,starts_of_def]) 1); +(* 2: reachable transitions *) +by (REPEAT (rtac allI 1)); +by (rtac imp_conj_lemma 1); +by (simp_tac (!simpset addsimps [rename_def]) 1); +by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def, +asig_outputs_def,asig_of_def,trans_of_def]) 1); +by (safe_tac (!claset)); +by (rtac (expand_if RS ssubst) 1); + by (rtac conjI 1); + by (rtac impI 1); + by (etac disjE 1); + by (etac exE 1); +by (etac conjE 1); +(* x is input *) + by (dtac sym 1); + by (dtac sym 1); +by (Asm_full_simp_tac 1); +by (REPEAT (hyp_subst_tac 1)); +by (forward_tac [reachable_rename] 1); +by (Asm_full_simp_tac 1); +(* x is output *) + by (etac exE 1); +by (etac conjE 1); + by (dtac sym 1); + by (dtac sym 1); +by (Asm_full_simp_tac 1); +by (REPEAT (hyp_subst_tac 1)); +by (forward_tac [reachable_rename] 1); +by (Asm_full_simp_tac 1); +(* x is internal *) +by (simp_tac (!simpset addcongs [conj_cong]) 1); +by (rtac impI 1); +by (etac conjE 1); +by (forward_tac [reachable_rename] 1); +by (Auto_tac()); +qed"rename_through_pmap"; + + diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/RefMappings.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,50 @@ +(* Title: HOLCF/IOA/meta_theory/RefMappings.thy + ID: $$ + Author: Olaf Mueller + Copyright 1996 TU Muenchen + +Refinement Mappings in HOLCF/IOA +*) + +RefMappings = Traces + + +default term + +consts + laststate ::"('a,'s)execution => 's" + move ::"[('a,'s)ioa,('a,'s)execution,'s,'a,'s] => bool" + is_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" + is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" + +defs + +laststate_def + "laststate ex == case Last`(snd ex) of + Undef => fst ex + | Def at => snd at" + +(* FIX: see paper, move should be defined on pairs, not on execs, then fst ex=s can + be omitted *) +move_def + "move ioa ex s a t == + (is_execution_fragment ioa ex & Finite (snd ex) & + fst ex=s & laststate ex=t & + mk_trace ioa`(snd ex) = (if a:ext(ioa) then a>>nil else nil))" + +is_ref_map_def + "is_ref_map f C A == + (!s:starts_of(C). f(s):starts_of(A)) & + (!s t a. reachable C s & + s -a--C-> t + --> (? ex. move A ex (f s) a (f t)))" + +is_weak_ref_map_def + "is_weak_ref_map f C A == + (!s:starts_of(C). f(s):starts_of(A)) & + (!s t a. reachable C s & + s -a--C-> t + --> (if a:ext(C) + then (f s) -a--A-> (f t) + else (f s)=(f t)))" + +end diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/Seq.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/Seq.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,510 @@ +(* Title: HOLCF/IOA/meta_theory/Seq.ML + ID: + Author: Olaf M"uller + Copyright 1996 TU Muenchen + +*) + +Addsimps (sfinite.intrs @ seq.rews); + + +(* Instead of adding UU_neq_nil every equation UU~=x could be changed to x~=UU *) +goal thy "UU ~=nil"; +by (res_inst_tac [("s1","UU"),("t1","nil")] (sym RS rev_contrapos) 1); +by (REPEAT (Simp_tac 1)); +qed"UU_neq_nil"; + +Addsimps [UU_neq_nil]; + +(* ------------------------------------------------------------------------------------- *) + + +(* ---------------------------------------------------- *) + section "recursive equations of operators"; +(* ---------------------------------------------------- *) + + +(* ----------------------------------------------------------- *) +(* smap *) +(* ----------------------------------------------------------- *) + +bind_thm ("smap_unfold", fix_prover2 thy smap_def + "smap = (LAM f tr. case tr of \ + \ nil => nil \ + \ | x##xs => f`x ## smap`f`xs)"); + +goal thy "smap`f`nil=nil"; +by (stac smap_unfold 1); +by (Simp_tac 1); +qed"smap_nil"; + +goal thy "smap`f`UU=UU"; +by (stac smap_unfold 1); +by (Simp_tac 1); +qed"smap_UU"; + +goal thy +"!!x.[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs"; +br trans 1; +by (stac smap_unfold 1); +by (Asm_full_simp_tac 1); +br refl 1; +qed"smap_cons"; + +(* ----------------------------------------------------------- *) +(* sfilter *) +(* ----------------------------------------------------------- *) + +bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def + "sfilter = (LAM P tr. case tr of \ + \ nil => nil \ + \ | x##xs => If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)"); + +goal thy "sfilter`P`nil=nil"; +by (stac sfilter_unfold 1); +by (Simp_tac 1); +qed"sfilter_nil"; + +goal thy "sfilter`P`UU=UU"; +by (stac sfilter_unfold 1); +by (Simp_tac 1); +qed"sfilter_UU"; + +goal thy +"!!x.x~=UU ==> sfilter`P`(x##xs)= \ +\ (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)"; +br trans 1; +by (stac sfilter_unfold 1); +by (Asm_full_simp_tac 1); +br refl 1; +qed"sfilter_cons"; + +(* ----------------------------------------------------------- *) +(* sforall2 *) +(* ----------------------------------------------------------- *) + +bind_thm ("sforall2_unfold", fix_prover2 thy sforall2_def + "sforall2 = (LAM P tr. case tr of \ + \ nil => TT \ + \ | x##xs => (P`x andalso sforall2`P`xs))"); + +goal thy "sforall2`P`nil=TT"; +by (stac sforall2_unfold 1); +by (Simp_tac 1); +qed"sforall2_nil"; + +goal thy "sforall2`P`UU=UU"; +by (stac sforall2_unfold 1); +by (Simp_tac 1); +qed"sforall2_UU"; + +goal thy +"!!x.x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)"; +br trans 1; +by (stac sforall2_unfold 1); +by (Asm_full_simp_tac 1); +br refl 1; +qed"sforall2_cons"; + + +(* ----------------------------------------------------------- *) +(* stakewhile *) +(* ----------------------------------------------------------- *) + + +bind_thm ("stakewhile_unfold", fix_prover2 thy stakewhile_def + "stakewhile = (LAM P tr. case tr of \ + \ nil => nil \ + \ | x##xs => (If P`x then x##(stakewhile`P`xs) else nil fi))"); + +goal thy "stakewhile`P`nil=nil"; +by (stac stakewhile_unfold 1); +by (Simp_tac 1); +qed"stakewhile_nil"; + +goal thy "stakewhile`P`UU=UU"; +by (stac stakewhile_unfold 1); +by (Simp_tac 1); +qed"stakewhile_UU"; + +goal thy +"!!x.x~=UU ==> stakewhile`P`(x##xs) = \ +\ (If P`x then x##(stakewhile`P`xs) else nil fi)"; +br trans 1; +by (stac stakewhile_unfold 1); +by (Asm_full_simp_tac 1); +br refl 1; +qed"stakewhile_cons"; + +(* ----------------------------------------------------------- *) +(* sdropwhile *) +(* ----------------------------------------------------------- *) + + +bind_thm ("sdropwhile_unfold", fix_prover2 thy sdropwhile_def + "sdropwhile = (LAM P tr. case tr of \ + \ nil => nil \ + \ | x##xs => (If P`x then sdropwhile`P`xs else tr fi))"); + +goal thy "sdropwhile`P`nil=nil"; +by (stac sdropwhile_unfold 1); +by (Simp_tac 1); +qed"sdropwhile_nil"; + +goal thy "sdropwhile`P`UU=UU"; +by (stac sdropwhile_unfold 1); +by (Simp_tac 1); +qed"sdropwhile_UU"; + +goal thy +"!!x.x~=UU ==> sdropwhile`P`(x##xs) = \ +\ (If P`x then sdropwhile`P`xs else x##xs fi)"; +br trans 1; +by (stac sdropwhile_unfold 1); +by (Asm_full_simp_tac 1); +br refl 1; +qed"sdropwhile_cons"; + + +(* ----------------------------------------------------------- *) +(* slast *) +(* ----------------------------------------------------------- *) + + +bind_thm ("slast_unfold", fix_prover2 thy slast_def + "slast = (LAM tr. case tr of \ + \ nil => UU \ + \ | x##xs => (If is_nil`xs then x else slast`xs fi))"); + + +goal thy "slast`nil=UU"; +by (stac slast_unfold 1); +by (Simp_tac 1); +qed"slast_nil"; + +goal thy "slast`UU=UU"; +by (stac slast_unfold 1); +by (Simp_tac 1); +qed"slast_UU"; + +goal thy +"!!x.x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)"; +br trans 1; +by (stac slast_unfold 1); +by (Asm_full_simp_tac 1); +br refl 1; +qed"slast_cons"; + + +(* ----------------------------------------------------------- *) +(* sconc *) +(* ----------------------------------------------------------- *) + +bind_thm ("sconc_unfold", fix_prover2 thy sconc_def + "sconc = (LAM t1 t2. case t1 of \ + \ nil => t2 \ + \ | x##xs => x ## (xs @@ t2))"); + + +goal thy "nil @@ y = y"; +by (stac sconc_unfold 1); +by (Simp_tac 1); +qed"sconc_nil"; + +goal thy "UU @@ y=UU"; +by (stac sconc_unfold 1); +by (Simp_tac 1); +qed"sconc_UU"; + +goal thy "(x##xs) @@ y=x##(xs @@ y)"; +br trans 1; +by (stac sconc_unfold 1); +by (Asm_full_simp_tac 1); +by (case_tac "x=UU" 1); +by (REPEAT (Asm_full_simp_tac 1)); +qed"sconc_cons"; + +Addsimps [sconc_nil, sconc_UU,sconc_cons]; + + +(* ----------------------------------------------------------- *) +(* sflat *) +(* ----------------------------------------------------------- *) + +bind_thm ("sflat_unfold", fix_prover2 thy sflat_def + "sflat = (LAM tr. case tr of \ + \ nil => nil \ + \ | x##xs => x @@ sflat`xs)"); + +goal thy "sflat`nil=nil"; +by (stac sflat_unfold 1); +by (Simp_tac 1); +qed"sflat_nil"; + +goal thy "sflat`UU=UU"; +by (stac sflat_unfold 1); +by (Simp_tac 1); +qed"sflat_UU"; + +goal thy "sflat`(x##xs)= x@@(sflat`xs)"; +br trans 1; +by (stac sflat_unfold 1); +by (Asm_full_simp_tac 1); +by (case_tac "x=UU" 1); +by (REPEAT (Asm_full_simp_tac 1)); +qed"sflat_cons"; + + + + +(* ----------------------------------------------------------- *) +(* szip *) +(* ----------------------------------------------------------- *) + +bind_thm ("szip_unfold", fix_prover2 thy szip_def + "szip = (LAM t1 t2. case t1 of \ +\ nil => nil \ +\ | x##xs => (case t2 of \ +\ nil => UU \ +\ | y##ys => ##(szip`xs`ys)))"); + +goal thy "szip`nil`y=nil"; +by (stac szip_unfold 1); +by (Simp_tac 1); +qed"szip_nil"; + +goal thy "szip`UU`y=UU"; +by (stac szip_unfold 1); +by (Simp_tac 1); +qed"szip_UU1"; + +goal thy "!!x. x~=nil ==> szip`x`UU=UU"; +by (stac szip_unfold 1); +by (Asm_full_simp_tac 1); +by (res_inst_tac [("x","x")] seq.cases 1); +by (REPEAT (Asm_full_simp_tac 1)); +qed"szip_UU2"; + +goal thy "!!x.x~=UU ==> szip`(x##xs)`nil=UU"; +br trans 1; +by (stac szip_unfold 1); +by (REPEAT (Asm_full_simp_tac 1)); +qed"szip_cons_nil"; + +goal thy "!!x.[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = ##szip`xs`ys"; +br trans 1; +by (stac szip_unfold 1); +by (REPEAT (Asm_full_simp_tac 1)); +qed"szip_cons"; + + +Addsimps [sfilter_UU,sfilter_nil,sfilter_cons, + smap_UU,smap_nil,smap_cons, + sforall2_UU,sforall2_nil,sforall2_cons, + slast_UU,slast_nil,slast_cons, + stakewhile_UU, stakewhile_nil, stakewhile_cons, + sdropwhile_UU, sdropwhile_nil, sdropwhile_cons, + sflat_UU,sflat_nil,sflat_cons, + szip_UU1,szip_UU2,szip_nil,szip_cons_nil,szip_cons]; + + + +(* ------------------------------------------------------------------------------------- *) + +section "scons"; + +goal thy + "!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)"; +by (rtac iffI 1); +by (etac (hd seq.injects) 1); +auto(); +qed"scons_inject_eq"; + + +(* ------------------------------------------------------------------------------------- *) + +section "sfilter, sforall, sconc"; + + +goal thy "(if b then tr1 else tr2) @@ tr \ + \= (if b then tr1 @@ tr else tr2 @@ tr)"; +by (res_inst_tac [("P","b"),("Q","b")] impCE 1); +by (fast_tac HOL_cs 1); +by (REPEAT (Asm_full_simp_tac 1)); +qed"if_and_sconc"; + +Addsimps [if_and_sconc]; + + +goal thy "sfilter`P`(x @@ y) = (sfilter`P`x @@ sfilter`P`y)"; + +by (res_inst_tac[("x","x")] seq.ind 1); +(* adm *) +by (Simp_tac 1); +(* base cases *) +by (Simp_tac 1); +by (Simp_tac 1); +(* main case *) +by (asm_full_simp_tac (!simpset setloop split_If_tac) 1); +qed"sfiltersconc"; + +goal thy "sforall P (stakewhile`P`x)"; +by (simp_tac (!simpset addsimps [sforall_def]) 1); +by (res_inst_tac[("x","x")] seq.ind 1); +(* adm *) +by (simp_tac (!simpset addsimps [adm_trick_1]) 1); +(* base cases *) +by (Simp_tac 1); +by (Simp_tac 1); +(* main case *) +by (asm_full_simp_tac (!simpset setloop split_If_tac) 1); +qed"sforallPstakewhileP"; + +goal thy "sforall P (sfilter`P`x)"; +by (simp_tac (!simpset addsimps [sforall_def]) 1); +by (res_inst_tac[("x","x")] seq.ind 1); +(* adm *) +(* FIX should be refined in _one_ tactic *) +by (simp_tac (!simpset addsimps [adm_trick_1]) 1); +(* base cases *) +by (Simp_tac 1); +by (Simp_tac 1); +(* main case *) +by (asm_full_simp_tac (!simpset setloop split_If_tac) 1); +qed"forallPsfilterP"; + + + +(* ------------------------------------------------------------------------------------- *) + +section "Finite"; + +(* ---------------------------------------------------- *) +(* Proofs of rewrite rules for Finite: *) +(* 1. Finite(nil), (by definition) *) +(* 2. ~Finite(UU), *) +(* 3. a~=UU==> Finite(a##x)=Finite(x) *) +(* ---------------------------------------------------- *) + +goal thy "Finite x --> x~=UU"; +br impI 1; +be sfinite.induct 1; + by (Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); +qed"Finite_UU_a"; + +goal thy "~(Finite UU)"; +by (cut_inst_tac [("x","UU")]Finite_UU_a 1); +by (fast_tac HOL_cs 1); +qed"Finite_UU"; + +goal thy "Finite x --> a~=UU --> x=a##xs --> Finite xs"; +by (strip_tac 1); +be sfinite.elim 1; +by (fast_tac (HOL_cs addss !simpset) 1); +by (fast_tac (HOL_cs addSDs seq.injects) 1); +qed"Finite_cons_a"; + +goal thy "!!x.a~=UU ==>(Finite (a##x)) = (Finite x)"; +by (rtac iffI 1); +by (rtac (Finite_cons_a RS mp RS mp RS mp) 1); +by (REPEAT (assume_tac 1)); +by (fast_tac HOL_cs 1); +by (Asm_full_simp_tac 1); +qed"Finite_cons"; + +Addsimps [Finite_UU]; + + +(* ------------------------------------------------------------------------------------- *) + +section "induction"; + + +(*-------------------------------- *) +(* Extensions to Induction Theorems *) +(*-------------------------------- *) + + +qed_goalw "seq_finite_ind_lemma" thy [seq.finite_def] +"(!!n.P(seq_take n`s)) ==> seq_finite(s) -->P(s)" + (fn prems => + [ + (strip_tac 1), + (etac exE 1), + (etac subst 1), + (resolve_tac prems 1) + ]); + + +goal thy +"!!P.[|P(UU);P(nil);\ +\ !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)\ +\ |] ==> seq_finite(s) --> P(s)"; +by (rtac seq_finite_ind_lemma 1); +be seq.finite_ind 1; + ba 1; +by (Asm_full_simp_tac 1); +qed"seq_finite_ind"; + + + + +(* +(* ----------------------------------------------------------------- + Fr"uhere Herleitung des endlichen Induktionsprinzips + aus dem seq_finite Induktionsprinzip. + Problem bei admissibility von Finite-->seq_finite! + Deshalb Finite jetzt induktiv und nicht mehr rekursiv definiert! + ------------------------------------------------------------------ *) + +goal thy "seq_finite nil"; +by (simp_tac (!simpset addsimps [seq.sfinite_def]) 1); +by (res_inst_tac [("x","Suc 0")] exI 1); +by (simp_tac (!simpset addsimps seq.rews) 1); +qed"seq_finite_nil"; + +goal thy "seq_finite UU"; +by (simp_tac (!simpset addsimps [seq.sfinite_def]) 1); +qed"seq_finite_UU"; + +Addsimps[seq_finite_nil,seq_finite_UU]; + +goal HOL.thy "(B-->A) --> (A--> (B-->C))--> (B--> C)"; +by (fast_tac HOL_cs 1); +qed"logic_lemma"; + + +goal thy "!!P.[| P nil; \ +\ !!a t. [|a~=UU;Finite t; P t|] ==> P (a##t)|]\ +\ ==> Finite x --> P x"; + +by (rtac (logic_lemma RS mp RS mp) 1); +by (rtac trf_impl_tf 1); +by (rtac seq_finite_ind 1); +by (simp_tac (!simpset addsimps [Finite_def]) 1); +by (simp_tac (!simpset addsimps [Finite_def]) 1); +by (asm_full_simp_tac (!simpset addsimps [Finite_def]) 1); +qed"Finite_ind"; + + +goal thy "Finite tr --> seq_finite tr"; +by (rtac seq.ind 1); +(* adm *) +(* hier grosses Problem !!!!!!!!!!!!!!! *) + +by (simp_tac (!simpset addsimps [Finite_def]) 2); +by (simp_tac (!simpset addsimps [Finite_def]) 2); + +(* main case *) +by (asm_full_simp_tac (!simpset addsimps [Finite_def,seq.sfinite_def]) 2); +by (rtac impI 2); +by (rotate_tac 2 2); +by (Asm_full_simp_tac 2); +by (etac exE 2); +by (res_inst_tac [("x","Suc n")] exI 2); +by (asm_full_simp_tac (!simpset addsimps seq.rews) 2); +qed"tf_is_trf"; + +*) + diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/Seq.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/Seq.thy Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,124 @@ +(* Title: HOLCF/IOA/meta_theory/Seq.thy + ID: + Author: Olaf M"uller + Copyright 1996 TU Muenchen + +Partial, Finite and Infinite Sequences (lazy lists), modeled as domain. +*) + + +Seq = HOLCF + + +domain 'a seq = nil | "##" (HD::'a) (lazy TL::'a seq) (cinfixr 65) + + +consts + sfilter :: "('a -> tr) -> 'a seq -> 'a seq" + smap :: "('a -> 'b) -> 'a seq -> 'b seq" + sforall :: "('a -> tr) => 'a seq => bool" + sforall2 :: "('a -> tr) -> 'a seq -> tr" + slast :: "'a seq -> 'a" + sconc :: "'a seq -> 'a seq -> 'a seq" + sdropwhile, + stakewhile ::"('a -> tr) -> 'a seq -> 'a seq" + szip ::"'a seq -> 'b seq -> ('a*'b) seq" + sflat :: "('a seq) seq -> 'a seq" + + sfinite :: "'a seq set" + Partial ::"'a seq => bool" + Infinite ::"'a seq => bool" + + nproj :: "nat => 'a seq => 'a" + +syntax + "@@" :: "'a seq => 'a seq => 'a seq" (infixr 65) + "Finite" :: "'a seq => bool" + +translations + "xs @@ ys" == "sconc`xs`ys" + "Finite x" == "x:sfinite" + "~(Finite x)" =="x~:sfinite" + +defs + + + +(* f not possible at lhs, as "pattern matching" only for % x arguments, + f cannot be written at rhs in front, as fix_eq3 does not apply later *) +smap_def + "smap == (fix`(LAM h f tr. case tr of + nil => nil + | x##xs => f`x ## h`f`xs))" + +sfilter_def + "sfilter == (fix`(LAM h P t. case t of + nil => nil + | x##xs => If P`x + then x##(h`P`xs) + else h`P`xs + fi))" +sforall_def + "sforall P t == (sforall2`P`t ~=FF)" + + +sforall2_def + "sforall2 == (fix`(LAM h P t. case t of + nil => TT + | x##xs => P`x andalso h`P`xs))" + +sconc_def + "sconc == (fix`(LAM h t1 t2. case t1 of + nil => t2 + | x##xs => x##(h`xs`t2)))" + +slast_def + "slast == (fix`(LAM h t. case t of + nil => UU + | x##xs => (If is_nil`xs + then x + else h`xs fi)))" + +stakewhile_def + "stakewhile == (fix`(LAM h P t. case t of + nil => nil + | x##xs => If P`x + then x##(h`P`xs) + else nil + fi))" +sdropwhile_def + "sdropwhile == (fix`(LAM h P t. case t of + nil => nil + | x##xs => If P`x + then h`P`xs + else t + fi))" +sflat_def + "sflat == (fix`(LAM h t. case t of + nil => nil + | x##xs => x @@ (h`xs)))" + +szip_def + "szip == (fix`(LAM h t1 t2. case t1 of + nil => nil + | x##xs => (case t2 of + nil => UU + | y##ys => ##(h`xs`ys))))" + + +proj_def + "nproj == (%n tr.HD`(iterate n TL tr))" + +Partial_def + "Partial x == (seq_finite x) & ~(Finite x)" + +Infinite_def + "Infinite x == ~(seq_finite x)" + + +inductive "sfinite" + intrs + sfinite_0 "nil:sfinite" + sfinite_n "[|tr:sfinite;a~=UU|] ==> (a##tr) : sfinite" + + +end diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/Sequence.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,851 @@ +(* Title: HOLCF/IOA/meta_theory/Sequence.ML + ID: + Author: Olaf M"uller + Copyright 1996 TU Muenchen + +Theorems about Sequences over flat domains with lifted elements + +*) + + +Addsimps [andalso_and,andalso_or]; + +(* ----------------------------------------------------------------------------------- *) + +section "recursive equations of operators"; + +(* ---------------------------------------------------------------- *) +(* Map *) +(* ---------------------------------------------------------------- *) + +goal thy "Map f`UU =UU"; +by (simp_tac (!simpset addsimps [Map_def]) 1); +qed"Map_UU"; + +goal thy "Map f`nil =nil"; +by (simp_tac (!simpset addsimps [Map_def]) 1); +qed"Map_nil"; + +goal thy "Map f`(x>>xs)=(f x) >> Map f`xs"; +by (simp_tac (!simpset addsimps [Map_def, Cons_def,flift2_def]) 1); +qed"Map_cons"; + +(* ---------------------------------------------------------------- *) +(* Filter *) +(* ---------------------------------------------------------------- *) + +goal thy "Filter P`UU =UU"; +by (simp_tac (!simpset addsimps [Filter_def]) 1); +qed"Filter_UU"; + +goal thy "Filter P`nil =nil"; +by (simp_tac (!simpset addsimps [Filter_def]) 1); +qed"Filter_nil"; + +goal thy "Filter P`(x>>xs)= (if P x then x>>(Filter P`xs) else Filter P`xs)"; +by (simp_tac (!simpset addsimps [Filter_def, Cons_def,flift2_def,If_and_if]) 1); +qed"Filter_cons"; + +(* ---------------------------------------------------------------- *) +(* Forall *) +(* ---------------------------------------------------------------- *) + +goal thy "Forall P UU"; +by (simp_tac (!simpset addsimps [Forall_def,sforall_def]) 1); +qed"Forall_UU"; + +goal thy "Forall P nil"; +by (simp_tac (!simpset addsimps [Forall_def,sforall_def]) 1); +qed"Forall_nil"; + +goal thy "Forall P (x>>xs)= (P x & Forall P xs)"; +by (simp_tac (!simpset addsimps [Forall_def, sforall_def, + Cons_def,flift2_def]) 1); +qed"Forall_cons"; + +(* ---------------------------------------------------------------- *) +(* Conc *) +(* ---------------------------------------------------------------- *) + +goal thy "UU @@ y =UU"; +by (Simp_tac 1); +qed"Conc_UU"; + +goal thy "nil @@ y =y"; +by (Simp_tac 1); +qed"Conc_nil"; + +goal thy "(x>>xs) @@ y = x>>(xs @@y)"; +by (simp_tac (!simpset addsimps [Cons_def]) 1); +qed"Conc_cons"; + +(* ---------------------------------------------------------------- *) +(* Takewhile *) +(* ---------------------------------------------------------------- *) + +goal thy "Takewhile P`UU =UU"; +by (simp_tac (!simpset addsimps [Takewhile_def]) 1); +qed"Takewhile_UU"; + +goal thy "Takewhile P`nil =nil"; +by (simp_tac (!simpset addsimps [Takewhile_def]) 1); +qed"Takewhile_nil"; + +goal thy "Takewhile P`(x>>xs)= (if P x then x>>(Takewhile P`xs) else nil)"; +by (simp_tac (!simpset addsimps [Takewhile_def, Cons_def,flift2_def,If_and_if]) 1); +qed"Takewhile_cons"; + +(* ---------------------------------------------------------------- *) +(* Dropwhile *) +(* ---------------------------------------------------------------- *) + +goal thy "Dropwhile P`UU =UU"; +by (simp_tac (!simpset addsimps [Dropwhile_def]) 1); +qed"Dropwhile_UU"; + +goal thy "Dropwhile P`nil =nil"; +by (simp_tac (!simpset addsimps [Dropwhile_def]) 1); +qed"Dropwhile_nil"; + +goal thy "Dropwhile P`(x>>xs)= (if P x then Dropwhile P`xs else x>>xs)"; +by (simp_tac (!simpset addsimps [Dropwhile_def, Cons_def,flift2_def,If_and_if]) 1); +qed"Dropwhile_cons"; + +(* ---------------------------------------------------------------- *) +(* Last *) +(* ---------------------------------------------------------------- *) + + +goal thy "Last`UU =UU"; +by (simp_tac (!simpset addsimps [Last_def]) 1); +qed"Last_UU"; + +goal thy "Last`nil =UU"; +by (simp_tac (!simpset addsimps [Last_def]) 1); +qed"Last_nil"; + +goal thy "Last`(x>>xs)= (if xs=nil then Def x else Last`xs)"; +by (simp_tac (!simpset addsimps [Last_def, Cons_def]) 1); +by (res_inst_tac [("x","xs")] seq.cases 1); +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1); +by (REPEAT (Asm_simp_tac 1)); +qed"Last_cons"; + + +(* ---------------------------------------------------------------- *) +(* Flat *) +(* ---------------------------------------------------------------- *) + +goal thy "Flat`UU =UU"; +by (simp_tac (!simpset addsimps [Flat_def]) 1); +qed"Flat_UU"; + +goal thy "Flat`nil =nil"; +by (simp_tac (!simpset addsimps [Flat_def]) 1); +qed"Flat_nil"; + +goal thy "Flat`(x##xs)= x @@ (Flat`xs)"; +by (simp_tac (!simpset addsimps [Flat_def, Cons_def]) 1); +qed"Flat_cons"; + + +(* ---------------------------------------------------------------- *) +(* Zip *) +(* ---------------------------------------------------------------- *) + +goal thy "Zip = (LAM t1 t2. case t1 of \ +\ nil => nil \ +\ | x##xs => (case t2 of \ +\ nil => UU \ +\ | y##ys => (case x of \ +\ Undef => UU \ +\ | Def a => (case y of \ +\ Undef => UU \ +\ | Def b => Def (a,b)##(Zip`xs`ys)))))"; +by (rtac trans 1); +br fix_eq2 1; +br Zip_def 1; +br beta_cfun 1; +by (Simp_tac 1); +qed"Zip_unfold"; + +goal thy "Zip`UU`y =UU"; +by (stac Zip_unfold 1); +by (Simp_tac 1); +qed"Zip_UU1"; + +goal thy "!! x. x~=nil ==> Zip`x`UU =UU"; +by (stac Zip_unfold 1); +by (Simp_tac 1); +by (res_inst_tac [("x","x")] seq.cases 1); +by (REPEAT (Asm_full_simp_tac 1)); +qed"Zip_UU2"; + +goal thy "Zip`nil`y =nil"; +by (stac Zip_unfold 1); +by (Simp_tac 1); +qed"Zip_nil"; + +goal thy "Zip`(x>>xs)`nil= UU"; +by (stac Zip_unfold 1); +by (simp_tac (!simpset addsimps [Cons_def]) 1); +qed"Zip_cons_nil"; + +goal thy "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys"; +br trans 1; +by (stac Zip_unfold 1); +by (Simp_tac 1); +(* FIX: Why Simp_tac 2 times. Does continuity in simpflication make job sometimes not + completely ready ? *) +by (simp_tac (!simpset addsimps [Cons_def]) 1); +qed"Zip_cons"; + + +Delsimps [sfilter_UU,sfilter_nil,sfilter_cons, + smap_UU,smap_nil,smap_cons, + sforall2_UU,sforall2_nil,sforall2_cons, + slast_UU,slast_nil,slast_cons, + stakewhile_UU, stakewhile_nil, stakewhile_cons, + sdropwhile_UU, sdropwhile_nil, sdropwhile_cons, + sflat_UU,sflat_nil,sflat_cons, + szip_UU1,szip_UU2,szip_nil,szip_cons_nil,szip_cons]; + + +Addsimps [Filter_UU,Filter_nil,Filter_cons, + Map_UU,Map_nil,Map_cons, + Forall_UU,Forall_nil,Forall_cons, + Last_UU,Last_nil,Last_cons, + Conc_UU,Conc_nil,Conc_cons, + Takewhile_UU, Takewhile_nil, Takewhile_cons, + Dropwhile_UU, Dropwhile_nil, Dropwhile_cons, + Zip_UU1,Zip_UU2,Zip_nil,Zip_cons_nil,Zip_cons]; + + +(* + +Can Filter with HOL predicate directly be defined as fixpoint ? + +goal thy "Filter2 P = (LAM tr. case tr of \ + \ nil => nil \ + \ | x##xs => (case x of Undef => UU | Def y => \ +\ (if P y then y>>(Filter2 P`xs) else Filter2 P`xs)))"; +by (rtac trans 1); +br fix_eq2 1; +br Filter2_def 1; +br beta_cfun 1; +by (Simp_tac 1); + +is also possible, if then else has to be proven continuous and it would be nice if a case for +Seq would be available. + +*) + + +(* ------------------------------------------------------------------------------------- *) + + +section "Cons"; + +goal thy "a>>s = (Def a)##s"; +by (simp_tac (!simpset addsimps [Cons_def]) 1); +qed"Cons_def2"; + +goal thy "x = UU | x = nil | (? a s. x = a >> s)"; +by (simp_tac (!simpset addsimps [Cons_def2]) 1); +by (cut_facts_tac [seq.exhaust] 1); +by (fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1]) 1); +qed"Seq_exhaust"; + + +goal thy "!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s ==> P |] ==> P"; +by (cut_inst_tac [("x","x")] Seq_exhaust 1); +be disjE 1; +by (Asm_full_simp_tac 1); +be disjE 1; +by (Asm_full_simp_tac 1); +by (REPEAT (etac exE 1)); +by (Asm_full_simp_tac 1); +qed"Seq_cases"; + +fun Seq_case_tac s i = res_inst_tac [("x",s)] Seq_cases i + THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2); + +(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *) +fun Seq_case_simp_tac s i = Seq_case_tac s i THEN Asm_simp_tac (i+2) + THEN Asm_full_simp_tac (i+1) + THEN Asm_full_simp_tac i; + +goal thy "a>>s ~= UU"; +by (stac Cons_def2 1); +by (resolve_tac seq.con_rews 1); +br Def_not_UU 1; +qed"Cons_not_UU"; + +goal thy "~(a>>x) << UU"; +by (rtac notI 1); +by (dtac antisym_less 1); +by (Simp_tac 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_not_UU]) 1); +qed"Cons_not_less_UU"; + +goal thy "~a>>s << nil"; +by (stac Cons_def2 1); +by (resolve_tac seq.rews 1); +br Def_not_UU 1; +qed"Cons_not_less_nil"; + +goal thy "a>>s ~= nil"; +by (stac Cons_def2 1); +by (resolve_tac seq.rews 1); +qed"Cons_not_nil"; + +goal thy "(a>>s = b>>t) = (a = b & s = t)"; +by (simp_tac (HOL_ss addsimps [Cons_def2]) 1); +by (stac (hd lift.inject RS sym) 1); +back(); back(); +by (rtac scons_inject_eq 1); +by (REPEAT(rtac Def_not_UU 1)); +qed"Cons_inject_eq"; + +goal thy "(a>>s<>t) = (a = b & s<>x) = a>> (seq_take n`x)"; +by (simp_tac (!simpset addsimps [Cons_def]) 1); +qed"seq_take_Cons"; + +Addsimps [Cons_inject_eq,Cons_inject_less_eq,seq_take_Cons, + Cons_not_UU,Cons_not_less_UU,Cons_not_less_nil,Cons_not_nil]; + + +(* ----------------------------------------------------------------------------------- *) + +section "induction"; + +goal thy "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x"; +be seq.ind 1; +by (REPEAT (atac 1)); +by (def_tac 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1); +qed"Seq_induct"; + +goal thy "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |] \ +\ ==> seq_finite x --> P x"; +be seq_finite_ind 1; +by (REPEAT (atac 1)); +by (def_tac 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1); +qed"Seq_FinitePartial_ind"; + +goal thy "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x"; +be sfinite.induct 1; +ba 1; +by (def_tac 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1); +qed"Seq_Finite_ind"; + + +(* rws are definitions to be unfolded for admissibility check *) +fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i + THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1)))) + THEN simp_tac (!simpset addsimps rws) i; + +fun Seq_Finite_induct_tac i = etac Seq_Finite_ind i + THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i))); + +fun pair_tac s = res_inst_tac [("p",s)] PairE + THEN' hyp_subst_tac THEN' Asm_full_simp_tac; + +(* induction on a sequence of pairs with pairsplitting and simplification *) +fun pair_induct_tac s rws i = + res_inst_tac [("x",s)] Seq_induct i + THEN pair_tac "a" (i+3) + THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1)))) + THEN simp_tac (!simpset addsimps rws) i; + + + +(* ------------------------------------------------------------------------------------ *) + +section "HD,TL"; + +goal thy "HD`(x>>y) = Def x"; +by (simp_tac (!simpset addsimps [Cons_def]) 1); +qed"HD_Cons"; + +goal thy "TL`(x>>y) = y"; +by (simp_tac (!simpset addsimps [Cons_def]) 1); +qed"TL_Cons"; + +Addsimps [HD_Cons,TL_Cons]; + +(* ------------------------------------------------------------------------------------ *) + +section "Finite, Partial, Infinite"; + +goal thy "Finite (a>>xs) = Finite xs"; +by (simp_tac (!simpset addsimps [Cons_def2,Finite_cons]) 1); +qed"Finite_Cons"; + +Addsimps [Finite_Cons]; + +(* ------------------------------------------------------------------------------------ *) + +section "Conc"; + +goal thy "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)"; +by (Seq_Finite_induct_tac 1); +qed"Conc_cong"; + +(* ------------------------------------------------------------------------------------ *) + +section "Last"; + +goal thy "!! s.Finite s ==> s~=nil --> Last`s~=UU"; +by (Seq_Finite_induct_tac 1); +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1); +qed"Finite_Last1"; + +goal thy "!! s. Finite s ==> Last`s=UU --> s=nil"; +by (Seq_Finite_induct_tac 1); +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1); +by (fast_tac HOL_cs 1); +qed"Finite_Last2"; + + +(* ------------------------------------------------------------------------------------ *) + + +section "Filter, Conc"; + + +goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s"; +by (Seq_induct_tac "s" [Filter_def] 1); +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1); +qed"FilterPQ"; + +goal thy "Filter P`(x @@ y) = (Filter P`x @@ Filter P`y)"; +by (simp_tac (!simpset addsimps [Filter_def,sfiltersconc]) 1); +qed"FilterConc"; + +(* ------------------------------------------------------------------------------------ *) + +section "Map"; + +goal thy "Map f`(Map g`s) = Map (f o g)`s"; +by (Seq_induct_tac "s" [] 1); +qed"MapMap"; + +goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)"; +by (Seq_induct_tac "x" [] 1); +qed"MapConc"; + +goal thy "Filter P`(Map f`x) = Map f`(Filter (P o f)`x)"; +by (Seq_induct_tac "x" [] 1); +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1); +qed"MapFilter"; + + +(* ------------------------------------------------------------------------------------ *) + +section "Forall, Conc"; + + +goal thy "Forall P ys & (! x. P x --> Q x) \ +\ --> Forall Q ys"; +by (Seq_induct_tac "ys" [Forall_def,sforall_def] 1); +qed"ForallPForallQ1"; + +bind_thm ("ForallPForallQ",impI RSN (2,allI RSN (2,conjI RS (ForallPForallQ1 RS mp)))); + +goal thy "(Forall P x & Forall P y) --> Forall P (x @@ y)"; +by (Seq_induct_tac "x" [Forall_def,sforall_def] 1); +qed"Forall_Conc_impl"; + +goal thy "!! x. Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)"; +by (Seq_Finite_induct_tac 1); +qed"Forall_Conc"; + + +(* ------------------------------------------------------------------------------------- *) + +section "Forall, Filter"; + + +goal thy "Forall P (Filter P`x)"; +by (simp_tac (!simpset addsimps [Filter_def,Forall_def,forallPsfilterP]) 1); +qed"ForallPFilterP"; + +(* FIX: holds also in other direction, then equal to forallPfilterP *) +goal thy "Forall P x --> Filter P`x = x"; +by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1); +qed"ForallPFilterPid1"; + +val ForallPFilterPid = standard (ForallPFilterPid1 RS mp); + + +(* holds also in <-- direction. FIX: prove that also *) + +goal thy "!! P. Finite ys & Forall (%x. ~P x) ys \ +\ --> Filter P`ys = nil "; +by (res_inst_tac[("x","ys")] Seq_induct 1); +(* adm *) +(* FIX: cont tfinite behandeln *) +br adm_all 1; +(* base cases *) +by (Simp_tac 1); +by (Simp_tac 1); +(* main case *) +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1); +qed"ForallnPFilterPnil1"; + +val ForallnPFilterPnil = standard (conjI RS (ForallnPFilterPnil1 RS mp)); + + +(* FIX: holds also in <== direction *) +goal thy "!! P. ~Finite ys & Forall (%x. ~P x) ys \ +\ --> Filter P`ys = UU "; +by (res_inst_tac[("x","ys")] Seq_induct 1); +(* adm *) +(* FIX: cont ~tfinite behandeln *) +br adm_all 1; +(* base cases *) +by (Simp_tac 1); +by (Simp_tac 1); +(* main case *) +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1); +qed"ForallnPFilterPUU1"; + +val ForallnPFilterPUU = standard (conjI RS (ForallnPFilterPUU1 RS mp)); + + +goal thy "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \ +\ ==> Filter P`ys = nil"; +be ForallnPFilterPnil 1; +be ForallPForallQ 1; +auto(); +qed"ForallQFilterPnil"; + +goal thy "!! Q P. [| ~Finite ys; Forall Q ys; !!x. Q x ==> ~P x|] \ +\ ==> Filter P`ys = UU "; +be ForallnPFilterPUU 1; +be ForallPForallQ 1; +auto(); +qed"ForallQFilterPUU"; + + + +(* ------------------------------------------------------------------------------------- *) + +section "Takewhile, Forall, Filter"; + + +goal thy "Forall P (Takewhile P`x)"; +by (simp_tac (!simpset addsimps [Forall_def,Takewhile_def,sforallPstakewhileP]) 1); +qed"ForallPTakewhileP"; + + +goal thy"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)"; +br ForallPForallQ 1; +br ForallPTakewhileP 1; +auto(); +qed"ForallPTakewhileQ"; + + +goal thy "!! Q P.[| Finite (Takewhile Q`ys); !!x. Q x ==> ~P x |] \ +\ ==> Filter P`(Takewhile Q`ys) = nil"; +be ForallnPFilterPnil 1; +br ForallPForallQ 1; +br ForallPTakewhileP 1; +auto(); +qed"FilterPTakewhileQnil"; + +goal thy "!! Q P. [| !!x. Q x ==> P x |] ==> \ +\ Filter P`(Takewhile Q`ys) = (Takewhile Q`ys)"; +br ForallPFilterPid 1; +br ForallPForallQ 1; +br ForallPTakewhileP 1; +auto(); +qed"FilterPTakewhileQid"; + +Addsimps [ForallPTakewhileP,ForallPTakewhileQ, + FilterPTakewhileQnil,FilterPTakewhileQid]; + + + +(* ----------------------------------------------------------------------------------- *) + + +(* +section "admissibility"; + +goal thy "adm(%x.~Finite x)"; +br admI 1; +bd spec 1; +be contrapos 1; + +*) + +(* ----------------------------------------------------------------------------------- *) + +section "coinductive characterizations of Filter"; + + +goal thy "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 *) +by (Seq_induct_tac "y" [] 1); +br adm_all 1; +by (Asm_full_simp_tac 1); +by (case_tac "P a" 1); +by (Asm_full_simp_tac 1); +br impI 1; +by (hyp_subst_tac 1); +by (Asm_full_simp_tac 1); +(* ~ P a *) +by (Asm_full_simp_tac 1); +br impI 1; +by (rotate_tac ~1 1); +by (Asm_full_simp_tac 1); +by (REPEAT (etac conjE 1)); +ba 1; +qed"divide_Seq_lemma"; + +goal thy "!! x. (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"; +br (divide_Seq_lemma RS mp) 1; +by (dres_inst_tac [("fo","HD"),("xa","x>>xs")] monofun_cfun_arg 1); +by (Asm_full_simp_tac 1); +qed"divide_Seq"; + + +goal thy "~Forall P y --> (? x. HD`(Filter (%a. ~P a)`y) = Def x)"; +(* FIX: pay attention: is only admissible with chain-finite package to be added to + adm test *) +by (Seq_induct_tac "y" [] 1); +br adm_all 1; +by (case_tac "P a" 1); +by (Asm_full_simp_tac 1); +by (Asm_full_simp_tac 1); +qed"nForall_HDFilter"; + + +goal thy "!!y. ~Forall P y \ +\ ==> ? x. y= (Takewhile P`y @@ (x >> TL`(Dropwhile P`y))) & \ +\ Finite (Takewhile P`y) & (~ P x)"; +bd (nForall_HDFilter RS mp) 1; +by (safe_tac set_cs); +by (res_inst_tac [("x","x")] exI 1); +by (cut_inst_tac [("P1","%x. ~ P x")] (divide_Seq_lemma RS mp) 1); +auto(); +qed"divide_Seq2"; + + +goal thy "!! y. ~Forall P y \ +\ ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)"; +by (cut_inst_tac [] divide_Seq2 1); +auto(); +qed"divide_Seq3"; + +Addsimps [FilterPQ,FilterConc,Conc_cong,Forall_Conc]; + + +(* ------------------------------------------------------------------------------------- *) + + +section "take_lemma"; + +goal thy "(!n. seq_take n`x = seq_take n`x') = (x = x')"; +by (rtac iffI 1); +br seq.take_lemma 1; +auto(); +qed"seq_take_lemma"; + +(* + +goal thy "Finite x & (! k. k < n --> seq_take k`y1 = seq_take k`y2) \ +\ --> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2))"; +br less_induct 1; + + +goal thy "!!x. Finite x ==> \ +\ ((! k. k < n --> seq_take k`y1 = seq_take k`y2) \ +\ --> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2)))"; +by (Seq_Finite_induct_tac 1); +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1); + + +qed"take_reduction"; +*) + +goal thy "!! 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)"; +by (case_tac "Forall Q x" 1); +by (auto_tac (!claset addSDs [divide_Seq3],!simpset)); +qed"take_lemma_principle1"; + +goal thy "!! 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)|] \ +\ ==> ! n. seq_take n`(f (s1 @@ y>>s2)) \ +\ = seq_take n`(g (s1 @@ y>>s2)) |] \ +\ ==> A x --> (f x)=(g x)"; +by (case_tac "Forall Q x" 1); +by (auto_tac (!claset addSDs [divide_Seq3],!simpset)); +br seq.take_lemma 1; +auto(); +qed"take_lemma_principle2"; + + +(* Note: in the following proofs the ordering of proof steps is very + important, as otherwise either (Forall Q s1) would be in the IH as + assumption (then rule useless) or it is not possible to strengthen + the IH by doing a forall closure of the sequence t (then rule also useless). + This is also the reason why the induction rule (less_induct or nat_induct) has to + to be imbuilt into the rule, as induction has to be done early and the take lemma + has to be used in the trivial direction afterwards for the (Forall Q x) case. *) + +goal thy +"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \ +\ !! s1 s2 y n. [| ! t. A t --> seq_take n`(f t) = seq_take n`(g t);\ +\ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \ +\ ==> seq_take (Suc n)`(f (s1 @@ y>>s2)) \ +\ = seq_take (Suc n)`(g (s1 @@ y>>s2)) |] \ +\ ==> A x --> (f x)=(g x)"; +br impI 1; +br seq.take_lemma 1; +br mp 1; +ba 2; +by (res_inst_tac [("x","x")] spec 1); +br nat_induct 1; +by (Simp_tac 1); +br allI 1; +by (case_tac "Forall Q xa" 1); +by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec], + !simpset)) 1); +by (auto_tac (!claset addSDs [divide_Seq3],!simpset)); +qed"take_lemma_induct"; + + +goal thy +"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \ +\ !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m`(f t) = seq_take m`(g t);\ +\ Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |] \ +\ ==> seq_take n`(f (s1 @@ y>>s2)) \ +\ = seq_take n`(g (s1 @@ y>>s2)) |] \ +\ ==> A x --> (f x)=(g x)"; +br impI 1; +br seq.take_lemma 1; +br mp 1; +ba 2; +by (res_inst_tac [("x","x")] spec 1); +br less_induct 1; +br allI 1; +by (case_tac "Forall Q xa" 1); +by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec], + !simpset)) 1); +by (auto_tac (!claset addSDs [divide_Seq3],!simpset)); +qed"take_lemma_less_induct"; + +goal thy +"!! Q. [| A UU ==> (f UU) = (g UU) ; \ +\ A nil ==> (f nil) = (g nil) ; \ +\ !! s y n. [| ! t. A t --> seq_take n`(f t) = seq_take n`(g t);\ +\ A (y>>s) |] \ +\ ==> seq_take (Suc n)`(f (y>>s)) \ +\ = seq_take (Suc n)`(g (y>>s)) |] \ +\ ==> A x --> (f x)=(g x)"; +br impI 1; +br seq.take_lemma 1; +br mp 1; +ba 2; +by (res_inst_tac [("x","x")] spec 1); +br nat_induct 1; +by (Simp_tac 1); +br allI 1; +by (Seq_case_simp_tac "xa" 1); +qed"take_lemma_in_eq_out"; + + +(* ------------------------------------------------------------------------------------ *) + +section "alternative take_lemma proofs"; + + +(* --------------------------------------------------------------- *) +(* Alternative Proof of FilterPQ *) +(* --------------------------------------------------------------- *) + +Delsimps [FilterPQ]; + + +(* In general: How to do this case without the same adm problems + as for the entire proof ? *) +goal thy "Forall (%x.~(P x & Q x)) s \ +\ --> Filter P`(Filter Q`s) =\ +\ Filter (%x. P x & Q x)`s"; + +by (Seq_induct_tac "s" [Forall_def,sforall_def] 1); +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1); +qed"Filter_lemma1"; + +goal thy "!! s. Finite s ==> \ +\ (Forall (%x. (~P x) | (~ Q x)) s \ +\ --> Filter P`(Filter Q`s) = nil)"; +by (Seq_Finite_induct_tac 1); +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1); +qed"Filter_lemma2"; + +goal thy "!! s. Finite s ==> \ +\ Forall (%x. (~P x) | (~ Q x)) s \ +\ --> Filter (%x.P x & Q x)`s = nil"; +by (Seq_Finite_induct_tac 1); +by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1); +qed"Filter_lemma3"; + + +goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s"; +by (res_inst_tac [("A1","%x.True") + ,("Q1","%x.~(P x & Q x)")] + (take_lemma_induct RS mp) 1); +(* FIX: rule always needs a back: eliminate *) +back(); +(* FIX: better support for A = %.True *) +by (Fast_tac 3); +by (asm_full_simp_tac (!simpset addsimps [Filter_lemma1]) 1); +by (asm_full_simp_tac (!simpset addsimps [Filter_lemma2,Filter_lemma3] + setloop split_tac [expand_if]) 1); +qed"FilterPQ_takelemma"; + +Addsimps [FilterPQ]; + + +(* --------------------------------------------------------------- *) +(* Alternative Proof of MapConc *) +(* --------------------------------------------------------------- *) + +Delsimps [MapConc]; + +goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)"; +by (res_inst_tac [("A1","%x.True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1); +auto(); +qed"MapConc_takelemma"; + +Addsimps [MapConc]; + diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/Sequence.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,91 @@ +(* Title: HOLCF/IOA/meta_theory/Sequence.thy + ID: + Author: Olaf M"uller + Copyright 1996 TU Muenchen + +Sequences over flat domains with lifted elements + +*) + +Sequence = Seq + + +default term + +types 'a Seq = ('a::term lift)seq + +ops curried + + Cons ::"'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, + Takewhile ::"('a => bool) => 'a Seq -> 'a Seq" + Zip ::"'a Seq -> 'b Seq -> ('a * 'b) Seq" + Flat ::"('a Seq) seq -> 'a Seq" + + Filter2 ::"('a => bool) => 'a Seq -> 'a Seq" + +syntax + + "@Cons" ::"'a => 'a Seq => 'a Seq" ("(_>>_)" [66,65] 65) + +syntax (symbols) + + "@Cons" ::"'a => 'a Seq => 'a Seq" ("(_\\_)" [66,65] 65) + + +translations + + "a>>s" == "Cons a`s" + +defs + + +Cons_def "Cons a == LAM s. Def a ## s" + +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" + +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 + nil => nil + | x##xs => (case t2 of + nil => UU + | y##ys => (case x of + Undef => UU + | Def a => (case y of + Undef => 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 Undef => UU | Def y => (if P y + then x##(h`xs) + else h`xs))))" + +rules + + +(* for test purposes should be deleted FIX !! *) +adm_all "adm f" + + +take_reduction + "[| Finite x; !! k. k < n ==> seq_take k`y1 = seq_take k`y2 |] + ==> seq_take n`(x @@ (t>>y1)) = seq_take n`(x @@ (t>>y2))" + + +end \ No newline at end of file diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/ShortExecutions.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,11 @@ +(* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy + ID: + Author: Olaf M"uller + Copyright 1997 TU Muenchen + +Some properties about cut(ex), defined as follows: + +For every execution ex there is another shorter execution cut(ex) +that has the same trace as ex, but its schedule ends with an external action. + +*) \ No newline at end of file diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/ShortExecutions.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,54 @@ +(* Title: HOLCF/IOA/meta_theory/ShortExecutions.thy + ID: + Author: Olaf M"uller + Copyright 1997 TU Muenchen + +Some properties about cut(ex), defined as follows: + +For every execution ex there is another shorter execution cut(ex) +that has the same trace as ex, but its schedule ends with an external action. + +*) + + +ShortExecutions = Traces + + +consts + + LastActExtsch ::"'a Seq => bool" + cutsch ::"'a Seq => 'a Seq" + + +defs + +LastActExtsch_def + "LastActExtsch sch == (cutsch sch = sch)" + + +rules + +exists_LastActExtsch + "[|sch : schedules A ; tr = Filter (%a.a:ext A)`sch|] + ==> ? sch. sch : schedules A & + tr = Filter (%a.a:ext A)`sch & + LastActExtsch sch" + +(* FIX: 1. LastActExtsch should have argument A also? + 2. use equality: (I) f P x =UU <-> (II) (fa ~P x) & ~finite(x) to prove it for (II) instead *) +LastActExtimplUU + "[|LastActExtsch sch; Filter (%x.x:ext A)`sch = UU |] + ==> sch=UU" + +(* FIX: see above *) +LastActExtimplnil + "[|LastActExtsch sch; Filter (%x.x:ext A)`sch = nil |] + ==> sch=nil" + +LastActExtsmall1 + "LastActExtsch sch ==> LastActExtsch (TL`(Dropwhile P`sch))" + +LastActExtsmall2 + "[| Finite sch1; LastActExtsch (sch1 @@ sch2) |] ==> LastActExtsch (sch2)" + +end + diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/Traces.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/Traces.ML Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,152 @@ +(* Title: HOLCF/IOA/meta_theory/Traces.ML + ID: + Author: Olaf M"uller + Copyright 1996 TU Muenchen + +Theorems about Executions and Traces of I/O automata in HOLCF. +*) + + + +val exec_rws = [executions_def,is_execution_fragment_def]; + + + +(* ----------------------------------------------------------------------------------- *) + +section "recursive equations of operators"; + + +(* ---------------------------------------------------------------- *) +(* filter_act *) +(* ---------------------------------------------------------------- *) + + +goal thy "filter_act`UU = UU"; +by (simp_tac (!simpset addsimps [filter_act_def]) 1); +qed"filter_act_UU"; + +goal thy "filter_act`nil = nil"; +by (simp_tac (!simpset addsimps [filter_act_def]) 1); +qed"filter_act_nil"; + +goal thy "filter_act`(x>>xs) = (fst x) >> filter_act`xs"; +by (simp_tac (!simpset addsimps [filter_act_def]) 1); +qed"filter_act_cons"; + +Addsimps [filter_act_UU,filter_act_nil,filter_act_cons]; + + +(* ---------------------------------------------------------------- *) +(* mk_trace *) +(* ---------------------------------------------------------------- *) + +goal thy "mk_trace A`UU=UU"; +by (simp_tac (!simpset addsimps [mk_trace_def]) 1); +qed"mk_trace_UU"; + +goal thy "mk_trace A`nil=nil"; +by (simp_tac (!simpset addsimps [mk_trace_def]) 1); +qed"mk_trace_nil"; + +goal thy "mk_trace A`(at >> xs) = \ +\ (if ((fst at):ext A) \ +\ then (fst at) >> (mk_trace A`xs) \ +\ else mk_trace A`xs)"; + +by (asm_full_simp_tac (!simpset addsimps [mk_trace_def]) 1); +qed"mk_trace_cons"; + +Addsimps [mk_trace_UU,mk_trace_nil,mk_trace_cons]; + +(* ---------------------------------------------------------------- *) +(* is_ex_fr *) +(* ---------------------------------------------------------------- *) + + +goal thy "is_ex_fr A = (LAM ex. (%s. case ex of \ +\ nil => TT \ +\ | x##xs => (flift1 \ +\ (%p.Def ((s,p):trans_of A) andalso (is_ex_fr A`xs) (snd p)) \ +\ `x) \ +\ ))"; +by (rtac trans 1); +br fix_eq2 1; +br is_ex_fr_def 1; +br beta_cfun 1; +by (simp_tac (!simpset addsimps [flift1_def]) 1); +qed"is_ex_fr_unfold"; + +goal thy "(is_ex_fr A`UU) s=UU"; +by (stac is_ex_fr_unfold 1); +by (Simp_tac 1); +qed"is_ex_fr_UU"; + +goal thy "(is_ex_fr A`nil) s = TT"; +by (stac is_ex_fr_unfold 1); +by (Simp_tac 1); +qed"is_ex_fr_nil"; + +goal thy "(is_ex_fr A`(pr>>xs)) s = \ +\ (Def ((s,pr):trans_of A) \ +\ andalso (is_ex_fr A`xs)(snd pr))"; +br trans 1; +by (stac is_ex_fr_unfold 1); +by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1); +by (Simp_tac 1); +qed"is_ex_fr_cons"; + + +Addsimps [is_ex_fr_UU,is_ex_fr_nil,is_ex_fr_cons]; + + +(* ---------------------------------------------------------------- *) +(* is_execution_fragment *) +(* ---------------------------------------------------------------- *) + +goal thy "is_execution_fragment A (s, UU)"; +by (simp_tac (!simpset addsimps [is_execution_fragment_def]) 1); +qed"is_execution_fragment_UU"; + +goal thy "is_execution_fragment A (s, nil)"; +by (simp_tac (!simpset addsimps [is_execution_fragment_def]) 1); +qed"is_execution_fragment_nil"; + +goal thy "is_execution_fragment A (s, (a,t)>>ex) = \ +\ (((s,a,t):trans_of A) & \ +\ is_execution_fragment A (t, ex))"; +by (simp_tac (!simpset addsimps [is_execution_fragment_def]) 1); +qed"is_execution_fragment_cons"; + + +(* Delsimps [is_ex_fr_UU,is_ex_fr_nil,is_ex_fr_cons]; *) +Addsimps [is_execution_fragment_UU,is_execution_fragment_nil, is_execution_fragment_cons]; + + +(* -------------------------------------------------------------------------------- *) + +section "has_trace, mk_trace"; + +(* alternative definition of has_trace tailored for the refinement proof, as it does not + take the detour of schedules *) + +goalw thy [executions_def,mk_trace_def,has_trace_def,schedules_def,has_schedule_def] +"has_trace A b = (? ex:executions A. b = mk_trace A`(snd ex))"; + +by (safe_tac set_cs); +(* 1 *) +by (res_inst_tac[("x","ex")] bexI 1); +by (stac beta_cfun 1); +by (cont_tacR 1); +by (Simp_tac 1); +by (Asm_simp_tac 1); +(* 2 *) +by (res_inst_tac[("x","filter_act`(snd ex)")] bexI 1); +by (stac beta_cfun 1); +by (cont_tacR 1); +by (Simp_tac 1); +by (safe_tac set_cs); +by (res_inst_tac[("x","ex")] bexI 1); +by (REPEAT (Asm_simp_tac 1)); +qed"has_trace_def2"; + diff -r cadbaef4f4a5 -r 981258186b71 src/HOLCF/IOA/meta_theory/Traces.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOLCF/IOA/meta_theory/Traces.thy Wed Apr 30 11:20:15 1997 +0200 @@ -0,0 +1,107 @@ +(* Title: HOLCF/IOA/meta_theory/Traces.thy + ID: + Author: Olaf M"uller + Copyright 1996 TU Muenchen + +Executions and Traces of I/O automata in HOLCF. +*) + + +Traces = Automata + Sequence + + +default term + +types + ('a,'s)pairs = "('a * 's) Seq" + ('a,'s)execution = "'s * ('a,'s)pairs" + 'a trace = "'a Seq" + +consts + + (* Executions *) + is_ex_fr ::"('a,'s)ioa => ('a,'s)pairs -> ('s => tr)" + is_execution_fragment, + 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, + has_trace :: "[('a,'s)ioa, 'a trace] => bool" + schedules, + traces :: "('a,'s)ioa => 'a trace set" + + mk_trace :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace" + + (* Notion of implementation *) + "=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr 12) + +(* +(* FIX: introduce good symbol *) +syntax (symbols) + + "op <<|" ::"[('a,'s1)ioa, ('a,'s2)ioa] => bool" (infixr "\\" 10) +*) + + +defs + + +(* ------------------- Executions ------------------------------ *) + + +is_execution_fragment_def + "is_execution_fragment A ex == ((is_ex_fr A`(snd ex)) (fst ex) ~= FF)" + +is_ex_fr_def + "is_ex_fr 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) + )))" + +executions_def + "executions ioa == {e. ((fst e) : starts_of(ioa)) & + is_execution_fragment ioa e}" + + +(* ------------------- Schedules ------------------------------ *) + + +filter_act_def + "filter_act == Map fst" + +has_schedule_def + "has_schedule ioa sch == + (? ex:executions ioa. sch = filter_act`(snd ex))" + +schedules_def + "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)" + +traces_def + "traces ioa == {tr. has_trace ioa tr}" + + +mk_trace_def + "mk_trace ioa == LAM tr. + Filter (%a.a:ext(ioa))`(filter_act`tr)" + + +(* ------------------- 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))" + + +end \ No newline at end of file