# HG changeset patch # User paulson # Date 907259298 -7200 # Node ID b29d18d8c4d23fb8d0bddf4676f80c4297e5e8da # Parent d283d61205481f3bcc94d0e9c6a20b2d54831d0a abstype of programs diff -r d283d6120548 -r b29d18d8c4d2 src/HOL/UNITY/Handshake.thy --- a/src/HOL/UNITY/Handshake.thy Thu Oct 01 18:27:55 1998 +0200 +++ b/src/HOL/UNITY/Handshake.thy Thu Oct 01 18:28:18 1998 +0200 @@ -21,16 +21,14 @@ "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}" prgF :: "state program" - "prgF == (|Init = {s. NF s = 0 & BB s}, - Acts0 = {cmdF}|)" + "prgF == mk_program ({s. NF s = 0 & BB s}, {cmdF})" (*G's program*) cmdG :: "(state*state) set" "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}" prgG :: "state program" - "prgG == (|Init = {s. NG s = 0 & BB s}, - Acts0 = {cmdG}|)" + "prgG == mk_program ({s. NG s = 0 & BB s}, {cmdG})" (*the joint invariant*) invFG :: "state set" diff -r d283d6120548 -r b29d18d8c4d2 src/HOL/UNITY/LessThan.ML --- a/src/HOL/UNITY/LessThan.ML Thu Oct 01 18:27:55 1998 +0200 +++ b/src/HOL/UNITY/LessThan.ML Thu Oct 01 18:28:18 1998 +0200 @@ -87,7 +87,7 @@ Goalw [atLeast_def] "atLeast (Suc k) = atLeast k - {k}"; by (simp_tac (simpset() addsimps [Suc_le_eq]) 1); -by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1); +by (simp_tac (simpset() addsimps [order_le_less]) 1); by (Blast_tac 1); qed "atLeast_Suc"; @@ -119,7 +119,7 @@ Addsimps [atMost_0]; Goalw [atMost_def] "atMost (Suc k) = insert (Suc k) (atMost k)"; -by (simp_tac (simpset() addsimps [less_Suc_eq, le_eq_less_or_eq]) 1); +by (simp_tac (simpset() addsimps [less_Suc_eq, order_le_less]) 1); by (Blast_tac 1); qed "atMost_Suc"; diff -r d283d6120548 -r b29d18d8c4d2 src/HOL/UNITY/Lift.ML --- a/src/HOL/UNITY/Lift.ML Thu Oct 01 18:27:55 1998 +0200 +++ b/src/HOL/UNITY/Lift.ML Thu Oct 01 18:28:18 1998 +0200 @@ -6,27 +6,6 @@ The Lift-Control Example *) - -Addsimps [integ_of_Pls RS sym]; -(*AND ALSO int 1 = #1 ??*) - - -(**INTDEF.ML**) -Goal "(int m) + (int n + z) = int (m + n) + z"; -by (simp_tac (simpset() addsimps [zadd_int, zadd_assoc RS sym]) 1); -qed "zadd_int_left"; - - -(**INT.ML**) - - -(**BIN.ML**) - - Goal "#0 <= int m"; - by (simp_tac (simpset_of Bin.thy addsimps [integ_of_Pls]) 1); - qed "zero_zle_int"; - AddIffs [zero_zle_int]; - Goal "~ z < w ==> (z < w + #1) = (z = w)"; by (asm_simp_tac (simpset() addsimps [zless_add1_eq, integ_le_less]) 1); qed "not_zless_zless1_eq"; @@ -49,16 +28,16 @@ (** Rules to move "metric n s" out of the assumptions, for case splitting **) val mov_metric1 = read_instantiate_sg (sign_of thy) - [("P", "?x < metric ?n ?s")] rev_mp; + [("P", "?x < metric ?n ?s")] rev_mp; val mov_metric2 = read_instantiate_sg (sign_of thy) - [("P", "?x = metric ?n ?s")] rev_mp; + [("P", "?x = metric ?n ?s")] rev_mp; val mov_metric3 = read_instantiate_sg (sign_of thy) - [("P", "~ (?x < metric ?n ?s)")] rev_mp; + [("P", "~ (?x < metric ?n ?s)")] rev_mp; val mov_metric4 = read_instantiate_sg (sign_of thy) - [("P", "(?x <= metric ?n ?s)")] rev_mp; + [("P", "(?x <= metric ?n ?s)")] rev_mp; (*The order in which they are applied seems to be critical...*) val mov_metrics = [mov_metric2, mov_metric3, mov_metric1, mov_metric4]; @@ -267,7 +246,7 @@ (** LEVEL 6 **) by (ALLGOALS (asm_simp_tac (simpset() addsimps [zle_def] @ metric_simps @ zcompare_rls))); -by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac))); +by (ALLGOALS (asm_simp_tac (simpset() addsimps int_0::zadd_ac))); qed "E_thm12b"; (*lift_4*) @@ -308,7 +287,8 @@ by Auto_tac; by (REPEAT_FIRST (eresolve_tac mov_metrics)); by (ALLGOALS - (asm_simp_tac (simpset() addsimps [zle_def]@metric_simps @ zcompare_rls))); + (asm_simp_tac (simpset() addsimps [int_0, zle_def] @ + metric_simps @ zcompare_rls))); (** LEVEL 5 **) by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1); by (etac exE 1); diff -r d283d6120548 -r b29d18d8c4d2 src/HOL/UNITY/Lift.thy --- a/src/HOL/UNITY/Lift.thy Thu Oct 01 18:27:55 1998 +0200 +++ b/src/HOL/UNITY/Lift.thy Thu Oct 01 18:28:18 1998 +0200 @@ -116,10 +116,10 @@ Lprg :: state program (*for the moment, we OMIT button_press*) - "Lprg == (|Init = {s. floor s = Min & ~ up s & move s & stop s & + "Lprg == mk_program ({s. floor s = Min & ~ up s & move s & stop s & ~ open s & req s = {}}, - Acts0 = {request_act, open_act, close_act, - req_up, req_down, move_up, move_down}|)" + {request_act, open_act, close_act, + req_up, req_down, move_up, move_down})" (** Invariants **) diff -r d283d6120548 -r b29d18d8c4d2 src/HOL/UNITY/Mutex.ML --- a/src/HOL/UNITY/Mutex.ML Thu Oct 01 18:27:55 1998 +0200 +++ b/src/HOL/UNITY/Mutex.ML Thu Oct 01 18:28:18 1998 +0200 @@ -37,7 +37,7 @@ (*The safety property: mutual exclusion*) -Goal "(reachable Mprg) Int {s. MM s = 3 & NN s = 3} = {}"; +Goal "(reachable Mprg) Int {s. MM s = #3 & NN s = #3} = {}"; by (cut_facts_tac [invariantUV RS Invariant_includes_reachable] 1); by Auto_tac; qed "mutual_exclusion"; @@ -47,8 +47,15 @@ Goal "Invariant Mprg bad_invariantU"; by (rtac InvariantI 1); by (constrains_tac 2); -by (auto_tac (claset() addSEs [le_SucE], simpset())); -by (Asm_full_simp_tac 1); +by (Force_tac 1); +(*Needs a decision procedure to simplify the resulting state*) +by (auto_tac (claset(), + simpset_of Int.thy addsimps + [zadd_int, integ_of_Pls, integ_of_Min, + integ_of_BIT, le_int_Suc_eq])); +by (dtac zle_trans 1 THEN assume_tac 1); +by (full_simp_tac (simpset_of Int.thy) 1); +by (asm_full_simp_tac (simpset() addsimps int_simps) 1); (*Resulting state: n=1, p=false, m=4, u=false. Execution of cmd1V (the command of process v guarded by n=1) sets p:=true, violating the invariant!*) @@ -56,43 +63,53 @@ getgoal 1; +Goal "(#1 <= m & m <= #3) = (m = #1 | m = #2 | m = #3)"; +by (auto_tac (claset(), + simpset_of Int.thy addsimps + [zle_iff_zadd, zadd_int, integ_of_Pls, integ_of_Min, + integ_of_BIT])); +by (exhaust_tac "na" 1); +by (exhaust_tac "nat" 2); +by (exhaust_tac "n" 3); +auto(); +qed "eq_123"; + + (*** Progress for U ***) -Goalw [Unless_def] "Unless Mprg {s. MM s=2} {s. MM s=3}"; +Goalw [Unless_def] "Unless Mprg {s. MM s=#2} {s. MM s=#3}"; by (constrains_tac 1); qed "U_F0"; -Goal "LeadsTo Mprg {s. MM s=1} {s. PP s = VV s & MM s = 2}"; +Goal "LeadsTo Mprg {s. MM s=#1} {s. PP s = VV s & MM s = #2}"; by (ensures_tac "cmd1U" 1); qed "U_F1"; -Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}"; +Goal "LeadsTo Mprg {s. ~ PP s & MM s = #2} {s. MM s = #3}"; by (cut_facts_tac [invariantU] 1); by (ensures_tac "cmd2U" 1); qed "U_F2"; -Goal "LeadsTo Mprg {s. MM s = 3} {s. PP s}"; -by (res_inst_tac [("B", "{s. MM s = 4}")] LeadsTo_Trans 1); +Goal "LeadsTo Mprg {s. MM s = #3} {s. PP s}"; +by (res_inst_tac [("B", "{s. MM s = #4}")] LeadsTo_Trans 1); by (ensures_tac "cmd4U" 2); by (ensures_tac "cmd3U" 1); qed "U_F3"; -Goal "LeadsTo Mprg {s. MM s = 2} {s. PP s}"; +Goal "LeadsTo Mprg {s. MM s = #2} {s. PP s}"; by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] MRS LeadsTo_Diff) 1); by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1); by (auto_tac (claset() addSEs [less_SucE], simpset())); val U_lemma2 = result(); -Goal "LeadsTo Mprg {s. MM s = 1} {s. PP s}"; +Goal "LeadsTo Mprg {s. MM s = #1} {s. PP s}"; by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1); by (Blast_tac 1); val U_lemma1 = result(); -Goal "LeadsTo Mprg {s. 1 <= MM s & MM s <= 3} {s. PP s}"; -by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] - addcongs [rev_conj_cong]) 1); -by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib, +Goal "LeadsTo Mprg {s. #1 <= MM s & MM s <= #3} {s. PP s}"; +by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib, U_lemma1, U_lemma2, U_F3] ) 1); val U_lemma123 = result(); @@ -106,41 +123,39 @@ (*** Progress for V ***) -Goalw [Unless_def] "Unless Mprg {s. NN s=2} {s. NN s=3}"; +Goalw [Unless_def] "Unless Mprg {s. NN s=#2} {s. NN s=#3}"; by (constrains_tac 1); qed "V_F0"; -Goal "LeadsTo Mprg {s. NN s=1} {s. PP s = (~ UU s) & NN s = 2}"; +Goal "LeadsTo Mprg {s. NN s=#1} {s. PP s = (~ UU s) & NN s = #2}"; by (ensures_tac "cmd1V" 1); qed "V_F1"; -Goal "LeadsTo Mprg {s. PP s & NN s = 2} {s. NN s = 3}"; +Goal "LeadsTo Mprg {s. PP s & NN s = #2} {s. NN s = #3}"; by (cut_facts_tac [invariantV] 1); by (ensures_tac "cmd2V" 1); qed "V_F2"; -Goal "LeadsTo Mprg {s. NN s = 3} {s. ~ PP s}"; -by (res_inst_tac [("B", "{s. NN s = 4}")] LeadsTo_Trans 1); +Goal "LeadsTo Mprg {s. NN s = #3} {s. ~ PP s}"; +by (res_inst_tac [("B", "{s. NN s = #4}")] LeadsTo_Trans 1); by (ensures_tac "cmd4V" 2); by (ensures_tac "cmd3V" 1); qed "V_F3"; -Goal "LeadsTo Mprg {s. NN s = 2} {s. ~ PP s}"; +Goal "LeadsTo Mprg {s. NN s = #2} {s. ~ PP s}"; by (rtac ([LeadsTo_weaken_L, Int_lower2 RS subset_imp_LeadsTo] MRS LeadsTo_Diff) 1); by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1); by (auto_tac (claset() addSEs [less_SucE], simpset())); val V_lemma2 = result(); -Goal "LeadsTo Mprg {s. NN s = 1} {s. ~ PP s}"; +Goal "LeadsTo Mprg {s. NN s = #1} {s. ~ PP s}"; by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1); by (Blast_tac 1); val V_lemma1 = result(); -Goal "LeadsTo Mprg {s. 1 <= NN s & NN s <= 3} {s. ~ PP s}"; -by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] - addcongs [rev_conj_cong]) 1); -by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib, +Goal "LeadsTo Mprg {s. #1 <= NN s & NN s <= #3} {s. ~ PP s}"; +by (simp_tac (simpset() addsimps [eq_123, Collect_disj_eq, LeadsTo_Un_distrib, V_lemma1, V_lemma2, V_F3] ) 1); val V_lemma123 = result(); @@ -155,7 +170,7 @@ (** Absence of starvation **) (*Misra's F6*) -Goal "LeadsTo Mprg {s. MM s = 1} {s. MM s = 3}"; +Goal "LeadsTo Mprg {s. MM s = #1} {s. MM s = #3}"; by (rtac LeadsTo_Un_duplicate 1); by (rtac LeadsTo_cancel2 1); by (rtac U_F2 2); @@ -169,7 +184,7 @@ (*The same for V*) -Goal "LeadsTo Mprg {s. NN s = 1} {s. NN s = 3}"; +Goal "LeadsTo Mprg {s. NN s = #1} {s. NN s = #3}"; by (rtac LeadsTo_Un_duplicate 1); by (rtac LeadsTo_cancel2 1); by (rtac V_F2 2); diff -r d283d6120548 -r b29d18d8c4d2 src/HOL/UNITY/Mutex.thy --- a/src/HOL/UNITY/Mutex.thy Thu Oct 01 18:27:55 1998 +0200 +++ b/src/HOL/UNITY/Mutex.thy Thu Oct 01 18:28:18 1998 +0200 @@ -8,20 +8,10 @@ Mutex = SubstAx + -(*WE NEED A GENERAL TREATMENT OF NUMBERS!!*) -syntax - "3" :: nat ("3") - "4" :: nat ("4") - -translations - "3" == "Suc 2" - "4" == "Suc 3" - - record state = PP :: bool - MM :: nat - NN :: nat + MM :: int + NN :: int UU :: bool VV :: bool @@ -30,57 +20,57 @@ (** The program for process U **) cmd0U :: "(state*state) set" - "cmd0U == {(s,s'). s' = s (|UU:=True, MM:=1|) & MM s = 0}" + "cmd0U == {(s,s'). s' = s (|UU:=True, MM:=#1|) & MM s = #0}" cmd1U :: "(state*state) set" - "cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=2|) & MM s = 1}" + "cmd1U == {(s,s'). s' = s (|PP:= VV s, MM:=#2|) & MM s = #1}" cmd2U :: "(state*state) set" - "cmd2U == {(s,s'). s' = s (|MM:=3|) & ~ PP s & MM s = 2}" + "cmd2U == {(s,s'). s' = s (|MM:=#3|) & ~ PP s & MM s = #2}" cmd3U :: "(state*state) set" - "cmd3U == {(s,s'). s' = s (|UU:=False, MM:=4|) & MM s = 3}" + "cmd3U == {(s,s'). s' = s (|UU:=False, MM:=#4|) & MM s = #3}" cmd4U :: "(state*state) set" - "cmd4U == {(s,s'). s' = s (|PP:=True, MM:=0|) & MM s = 4}" + "cmd4U == {(s,s'). s' = s (|PP:=True, MM:=#0|) & MM s = #4}" (** The program for process V **) cmd0V :: "(state*state) set" - "cmd0V == {(s,s'). s' = s (|VV:=True, NN:=1|) & NN s = 0}" + "cmd0V == {(s,s'). s' = s (|VV:=True, NN:=#1|) & NN s = #0}" cmd1V :: "(state*state) set" - "cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=2|) & NN s = 1}" + "cmd1V == {(s,s'). s' = s (|PP:= ~ UU s, NN:=#2|) & NN s = #1}" cmd2V :: "(state*state) set" - "cmd2V == {(s,s'). s' = s (|NN:=3|) & PP s & NN s = 2}" + "cmd2V == {(s,s'). s' = s (|NN:=#3|) & PP s & NN s = #2}" cmd3V :: "(state*state) set" - "cmd3V == {(s,s'). s' = s (|VV:=False, NN:=4|) & NN s = 3}" + "cmd3V == {(s,s'). s' = s (|VV:=False, NN:=#4|) & NN s = #3}" cmd4V :: "(state*state) set" - "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=0|) & NN s = 4}" + "cmd4V == {(s,s'). s' = s (|PP:=False, NN:=#0|) & NN s = #4}" Mprg :: state program - "Mprg == (|Init = {s. ~ UU s & ~ VV s & MM s = 0 & NN s = 0}, - Acts0 = {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, - cmd0V, cmd1V, cmd2V, cmd3V, cmd4V}|)" + "Mprg == mk_program ({s. ~ UU s & ~ VV s & MM s = #0 & NN s = #0}, + {cmd0U, cmd1U, cmd2U, cmd3U, cmd4U, + cmd0V, cmd1V, cmd2V, cmd3V, cmd4V})" (** The correct invariants **) invariantU :: "state set" - "invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) & - (MM s = 3 --> ~ PP s)}" + "invariantU == {s. (UU s = (#1 <= MM s & MM s <= #3)) & + (MM s = #3 --> ~ PP s)}" invariantV :: "state set" - "invariantV == {s. (VV s = (1 <= NN s & NN s <= 3)) & - (NN s = 3 --> PP s)}" + "invariantV == {s. (VV s = (#1 <= NN s & NN s <= #3)) & + (NN s = #3 --> PP s)}" (** The faulty invariant (for U alone) **) bad_invariantU :: "state set" - "bad_invariantU == {s. (UU s = (1 <= MM s & MM s <= 3)) & - (3 <= MM s & MM s <= 4 --> ~ PP s)}" + "bad_invariantU == {s. (UU s = (#1 <= MM s & MM s <= #3)) & + (#3 <= MM s & MM s <= #4 --> ~ PP s)}" end diff -r d283d6120548 -r b29d18d8c4d2 src/HOL/UNITY/NSP_Bad.thy --- a/src/HOL/UNITY/NSP_Bad.thy Thu Oct 01 18:27:55 1998 +0200 +++ b/src/HOL/UNITY/NSP_Bad.thy Thu Oct 01 18:28:18 1998 +0200 @@ -54,7 +54,6 @@ constdefs Nprg :: state program (*Initial trace is empty*) - "Nprg == (|Init = {[]}, - Acts0 = {Fake, NS1, NS2, NS3}|)" + "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3})" end diff -r d283d6120548 -r b29d18d8c4d2 src/HOL/UNITY/Reach.thy --- a/src/HOL/UNITY/Reach.thy Thu Oct 01 18:27:55 1998 +0200 +++ b/src/HOL/UNITY/Reach.thy Thu Oct 01 18:28:18 1998 +0200 @@ -24,8 +24,7 @@ "asgt u v == {(s,s'). s' = s(v:= s u | s v)}" Rprg :: state program - "Rprg == (|Init = {%v. v=init}, - Acts0 = (UN (u,v): edges. {asgt u v})|)" + "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v})" reach_invariant :: state set "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}" diff -r d283d6120548 -r b29d18d8c4d2 src/HOL/UNITY/Token.ML --- a/src/HOL/UNITY/Token.ML Thu Oct 01 18:27:55 1998 +0200 +++ b/src/HOL/UNITY/Token.ML Thu Oct 01 18:28:18 1998 +0200 @@ -54,7 +54,7 @@ by (auto_tac (claset(), simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq])); by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1); -by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, Suc_leI, +by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, Suc_leI, less_imp_le, diff_add_assoc]) 2); by (full_simp_tac (simpset() addsimps [nat_neq_iff]) 1); by (asm_full_simp_tac (simpset() addsimps [less_Suc_eq, mod_Suc]) 1); diff -r d283d6120548 -r b29d18d8c4d2 src/HOL/UNITY/Traces.ML --- a/src/HOL/UNITY/Traces.ML Thu Oct 01 18:27:55 1998 +0200 +++ b/src/HOL/UNITY/Traces.ML Thu Oct 01 18:28:18 1998 +0200 @@ -9,40 +9,44 @@ *) + +(*** The abstract type of programs ***) + +val rep_ss = simpset() addsimps + [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, + Rep_Program_inverse, Abs_Program_inverse]; + + Goal "id: Acts prg"; -by (simp_tac (simpset() addsimps [Acts_def]) 1); +by (cut_inst_tac [("x", "prg")] Rep_Program 1); +by (auto_tac (claset(), rep_ss)); qed "id_in_Acts"; AddIffs [id_in_Acts]; - -Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}"; -by Safe_tac; -by (etac traces.induct 2); -by (etac reachable.induct 1); -by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs)))); -qed "reachable_equiv_traces"; +Goal "Init (mk_program (init,acts)) = init"; +by (auto_tac (claset(), rep_ss)); +qed "Init_eq"; -Goal "acts <= Acts prg ==> stable acts (reachable prg)"; -by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1); -qed "stable_reachable"; - -Goalw [Acts_def] - "(act : Acts(|Init=init, Acts0=acts|)) = (act=id | act : acts)"; -by Auto_tac; +Goal "Acts (mk_program (init,acts)) = insert id acts"; +by (auto_tac (claset(), rep_ss)); qed "Acts_eq"; -Goal "(s : Init(|Init=init, Acts0=acts|)) = (s:init)"; -by Auto_tac; -qed "Init_eq"; +Addsimps [Acts_eq, Init_eq]; + -AddIffs [Acts_eq, Init_eq]; +Goal "[| Init prg = Init prg'; Acts prg = Acts prg' |] ==> prg = prg'"; +by (cut_inst_tac [("p", "Rep_Program prg")] surjective_pairing 1); +by (auto_tac (claset(), rep_ss)); +by (dres_inst_tac [("f", "Abs_Program")] arg_cong 1); +by (full_simp_tac (rep_ss addsimps [surjective_pairing RS sym]) 1); +qed "program_equalityI"; (*** These three rules allow "lazy" definition expansion ***) val [rew] = goal thy - "[| prg == (|Init=init, Acts0=acts|) |] \ + "[| prg == mk_program (init,acts) |] \ \ ==> Init prg = init & Acts prg = insert id acts"; by (rewtac rew); by Auto_tac; @@ -64,3 +68,16 @@ fun simp_of_set def = def RS def_set_simp; + +(*** traces and reachable ***) + +Goal "reachable prg = {s. EX evs. (s,evs): traces (Init prg) (Acts prg)}"; +by Safe_tac; +by (etac traces.induct 2); +by (etac reachable.induct 1); +by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs)))); +qed "reachable_equiv_traces"; + +Goal "acts <= Acts prg ==> stable acts (reachable prg)"; +by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1); +qed "stable_reachable"; diff -r d283d6120548 -r b29d18d8c4d2 src/HOL/UNITY/Traces.thy --- a/src/HOL/UNITY/Traces.thy Thu Oct 01 18:27:55 1998 +0200 +++ b/src/HOL/UNITY/Traces.thy Thu Oct 01 18:28:18 1998 +0200 @@ -24,14 +24,18 @@ ==> (s', s#evs) : traces Init Acts" -record 'a program = - Init :: 'a set - Acts0 :: "('a * 'a)set set" - +typedef (Program) + 'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). id:acts}" constdefs + mk_program :: "('a set * ('a * 'a)set set) => 'a program" + "mk_program == %(init, acts). Abs_Program (init, insert id acts)" + + Init :: "'a program => 'a set" + "Init prg == fst (Rep_Program prg)" + Acts :: "'a program => ('a * 'a)set set" - "Acts prg == insert id (Acts0 prg)" + "Acts prg == snd (Rep_Program prg)" consts reachable :: "'a program => 'a set" diff -r d283d6120548 -r b29d18d8c4d2 src/HOL/UNITY/Union.ML --- a/src/HOL/UNITY/Union.ML Thu Oct 01 18:27:55 1998 +0200 +++ b/src/HOL/UNITY/Union.ML Thu Oct 01 18:28:18 1998 +0200 @@ -14,8 +14,7 @@ qed "Init_Join"; Goal "Acts (Join prgF prgG) = Acts prgF Un Acts prgG"; -by (auto_tac (claset(), - simpset() addsimps [Acts_def, Join_def])); +by (auto_tac (claset(), simpset() addsimps [Join_def])); qed "Acts_Join"; Goal "Init (JN i:I. prg i) = (INT i:I. Init (prg i))"; @@ -23,14 +22,14 @@ qed "Init_JN"; Goal "Acts (JN i:I. prg i) = insert id (UN i:I. Acts (prg i))"; -by (auto_tac (claset(), - simpset() addsimps [Acts_def, JOIN_def])); +by (auto_tac (claset(), simpset() addsimps [JOIN_def])); qed "Acts_JN"; Addsimps [Init_Join, Init_JN]; Goal "(JN x:insert a A. B x) = Join (B a) (JN x:A. B x)"; -by (simp_tac (simpset() addsimps [Acts_def, JOIN_def, Join_def]) 1); +br program_equalityI 1; +by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def]))); qed "JN_insert"; Addsimps[JN_insert]; @@ -42,41 +41,18 @@ qed "Join_commute"; Goal "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)"; -by (simp_tac (simpset() addsimps Un_ac@[Join_def, Acts_def, Int_assoc]) 1); +by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1); qed "Join_assoc"; - - -(* -val field_defs = thms"program.field_defs"; -val dest_defs = thms"program.dest_defs"; -val dest_convs = thms"program.dest_convs"; - -val update_defs = thms"program.update_defs"; -val make_defs = thms"program.make_defs"; -val update_convs = thms"program.update_convs"; -val simps = thms"program.simps"; -*) - - - - - -(**NOT PROVABLE because no "surjective pairing" for records + Goalw [Join_def, SKIP_def] "Join prgF SKIP = prgF"; -by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1); +br program_equalityI 1; +by (ALLGOALS (simp_tac (simpset() addsimps [insert_absorb]))); qed "Join_SKIP"; - In order to prove Join_SKIP, we possibly need - "Acts0 = ... - {id}" in JOIN_def and Join_def. But then Join_absorb only - holds if id ~: Acts0(prg). Or else we need to change 'a program to - an abstract type! Then equality could be made to ignore Acts0. - -NOT PROVABLE because no "surjective pairing" for records Goalw [Join_def] "Join prgF prgF = prgF"; +br program_equalityI 1; by Auto_tac; qed "Join_absorb"; -*) - Goal "(JN G:{}. G) = SKIP"; @@ -93,7 +69,8 @@ "I ~= {} ==> \ \ constrains (Acts (JN i:I. prg i)) A B = \ \ (ALL i:I. constrains (Acts (prg i)) A B)"; -by Auto_tac; +by (Simp_tac 1); +by (Blast_tac 1); qed "constrains_JN"; (**FAILS, I think; see 5.4.1, Substitution Axiom. @@ -108,7 +85,7 @@ \ (constrains (Acts prgF) A B & constrains (Acts prgG) A B)"; by (auto_tac (claset(), - simpset() addsimps [constrains_def, Join_def, Acts_def, ball_Un])); + simpset() addsimps [constrains_def, Join_def, ball_Un])); qed "constrains_Join"; Goal "[| constrains (Acts prgF) A A'; constrains (Acts prgG) B B' |] \ @@ -143,7 +120,7 @@ Goal "transient (Acts (Join prgF prgG)) A = \ \ (transient (Acts prgF) A | transient (Acts prgG) A)"; by (auto_tac (claset(), - simpset() addsimps [bex_Un, Acts_def, transient_def, + simpset() addsimps [bex_Un, transient_def, Join_def])); qed "transient_Join"; diff -r d283d6120548 -r b29d18d8c4d2 src/HOL/UNITY/Union.thy --- a/src/HOL/UNITY/Union.thy Thu Oct 01 18:27:55 1998 +0200 +++ b/src/HOL/UNITY/Union.thy Thu Oct 01 18:28:18 1998 +0200 @@ -12,15 +12,15 @@ constdefs JOIN :: ['a set, 'a => 'b program] => 'b program - "JOIN I prg == (|Init = INT i:I. Init (prg i), - Acts0 = UN i:I. Acts (prg i)|)" + "JOIN I prg == mk_program (INT i:I. Init (prg i), + UN i:I. Acts (prg i))" Join :: ['a program, 'a program] => 'a program - "Join prgF prgG == (|Init = Init prgF Int Init prgG, - Acts0 = Acts prgF Un Acts prgG|)" + "Join prgF prgG == mk_program (Init prgF Int Init prgG, + Acts prgF Un Acts prgG)" SKIP :: 'a program - "SKIP == (|Init = UNIV, Acts0 = {}|)" + "SKIP == mk_program (UNIV, {})" syntax "@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3JN _:_./ _)" 10)