# HG changeset patch # User paulson # Date 936177362 -7200 # Node ID c318acb8825135dd58d683fc8d52c96705b25e9a # Parent e53d5f0c7c94838e31fe3b87541de306bd3a1f04 tidied some proofs diff -r e53d5f0c7c94 -r c318acb88251 src/HOL/UNITY/Channel.ML --- a/src/HOL/UNITY/Channel.ML Wed Sep 01 11:15:35 1999 +0200 +++ b/src/HOL/UNITY/Channel.ML Wed Sep 01 11:16:02 1999 +0200 @@ -20,8 +20,7 @@ Addsimps [minSet_empty]; Goalw [minSet_def] "x:A ==> minSet A = Some (LEAST x. x: A)"; -by (ALLGOALS Asm_simp_tac); -by (Blast_tac 1); +by Auto_tac; qed_spec_mp "minSet_nonempty"; Goal "F : (minSet -`` {Some x}) leadsTo (minSet -`` (Some``greaterThan x))"; @@ -53,6 +52,6 @@ by (rtac (lemma RS leadsTo_weaken_R) 1); by (Clarify_tac 1); by (forward_tac [minSet_nonempty] 1); -by (asm_full_simp_tac (simpset() addsimps [Suc_le_eq]) 1); -by (blast_tac (claset() addDs [Suc_le_lessD, not_less_Least]) 1); +by (auto_tac (claset() addDs [Suc_le_lessD, not_less_Least], + simpset())); qed "Channel_progress"; diff -r e53d5f0c7c94 -r c318acb88251 src/HOL/UNITY/Constrains.ML --- a/src/HOL/UNITY/Constrains.ML Wed Sep 01 11:15:35 1999 +0200 +++ b/src/HOL/UNITY/Constrains.ML Wed Sep 01 11:16:02 1999 +0200 @@ -43,7 +43,8 @@ (*** Co ***) -overload_1st_set "Constrains.op Co"; +(*Needed because its operands are sets*) +overload_1st_set "Constrains.Constrains"; (*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*) bind_thm ("constrains_reachable_Int", @@ -341,11 +342,18 @@ (*proves "co" properties when the program is specified*) fun constrains_tac i = SELECT_GOAL - (EVERY [simp_tac (simpset() addsimps !program_defs_ref) 1, - REPEAT (resolve_tac [StableI, stableI, + (EVERY [REPEAT (Always_Int_tac 1), + REPEAT (etac Always_ConstrainsI 1 + ORELSE + resolve_tac [StableI, stableI, constrains_imp_Constrains] 1), rtac constrainsI 1, - Full_simp_tac 1, + full_simp_tac (simpset() addsimps !program_defs_ref) 1, REPEAT (FIRSTGOAL (etac disjE)), ALLGOALS Clarify_tac, ALLGOALS Asm_full_simp_tac]) i; + + +(*For proving invariants*) +fun always_tac i = + rtac AlwaysI i THEN Force_tac i THEN constrains_tac i; diff -r e53d5f0c7c94 -r c318acb88251 src/HOL/UNITY/Handshake.ML --- a/src/HOL/UNITY/Handshake.ML Wed Sep 01 11:15:35 1999 +0200 +++ b/src/HOL/UNITY/Handshake.ML Wed Sep 01 11:16:02 1999 +0200 @@ -30,14 +30,12 @@ by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); by (ensures_tac "cmdG" 2); by (constrains_tac 1); -by Auto_tac; qed "lemma2_1"; Goal "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo {s. k < NF s}"; by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1); by (constrains_tac 2); by (ensures_tac "cmdF" 1); -by Auto_tac; qed "lemma2_2"; @@ -45,11 +43,8 @@ by (rtac LeadsTo_weaken_R 1); by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")] GreaterThan_bounded_induct 1); -by (auto_tac (claset(), simpset() addsimps [vimage_def])); -(*The inductive step: (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*) -by (rtac LeadsTo_Diff 1); -by (rtac lemma2_2 2); -by (rtac LeadsTo_Trans 1); -by (rtac lemma2_2 2); -by (rtac lemma2_1 1); +(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*) +by (auto_tac (claset() addSIs [lemma2_1, lemma2_2] + addIs[LeadsTo_Trans, LeadsTo_Diff], + simpset() addsimps [vimage_def])); qed "progress"; diff -r e53d5f0c7c94 -r c318acb88251 src/HOL/UNITY/Lift.ML --- a/src/HOL/UNITY/Lift.ML Wed Sep 01 11:15:35 1999 +0200 +++ b/src/HOL/UNITY/Lift.ML Wed Sep 01 11:16:02 1999 +0200 @@ -47,14 +47,9 @@ req_up_def, req_down_def, move_up_def, move_down_def, button_press_def]); -val always_defs = [above_def, below_def, queueing_def, - goingup_def, goingdown_def, ready_def]; - -Addsimps (map simp_of_set always_defs); - - -val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un; -(* [| Lift: B LeadsTo C; Lift: A LeadsTo B |] ==> Lift: (A Un B) LeadsTo C *) +(*The ALWAYS properties*) +Addsimps (map simp_of_set [above_def, below_def, queueing_def, + goingup_def, goingdown_def, ready_def]); Addsimps [bounded_def, open_stop_def, open_move_def, stop_floor_def, @@ -64,47 +59,33 @@ Goal "Lift : Always open_stop"; -by (rtac AlwaysI 1); -by (Force_tac 1); -by (constrains_tac 1); +by (always_tac 1); qed "open_stop"; Goal "Lift : Always stop_floor"; -by (rtac AlwaysI 1); -by (Force_tac 1); -by (constrains_tac 1); +by (always_tac 1); qed "stop_floor"; (*This one needs open_stop, which was proved above*) Goal "Lift : Always open_move"; -by (rtac AlwaysI 1); -by (rtac (open_stop RS Always_ConstrainsI RS StableI) 2); -by (Force_tac 1); -by (constrains_tac 1); +by (cut_facts_tac [open_stop] 1); +by (always_tac 1); qed "open_move"; Goal "Lift : Always moving_up"; -by (rtac AlwaysI 1); -by (Force_tac 1); -by (constrains_tac 1); -by (auto_tac (claset(), +by (always_tac 1); +by (auto_tac (claset() addDs [zle_imp_zless_or_eq], simpset() addsimps [add1_zle_eq])); -by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1); qed "moving_up"; Goal "Lift : Always moving_down"; -by (rtac AlwaysI 1); -by (Force_tac 1); -by (constrains_tac 1); +by (always_tac 1); by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1); qed "moving_down"; Goal "Lift : Always bounded"; -by (rtac AlwaysI 1); -by (rtac (Always_Int_rule [moving_up, moving_down] RS - Always_ConstrainsI RS StableI) 2); -by (Force_tac 1); -by (constrains_tac 1); +by (cut_facts_tac [moving_up, moving_down] 1); +by (always_tac 1); by (ALLGOALS Clarify_tac); by (REPEAT_FIRST distinct_tac); by Auto_tac; @@ -170,8 +151,8 @@ Goal "Lift : (Req n Int closed - (atFloor n - queueing)) \ \ LeadsTo ((closed Int goingup Int Req n) Un \ \ (closed Int goingdown Int Req n))"; -by (rtac subset_imp_LeadsTo 1); -by (auto_tac (claset() addSEs [int_neqE], simpset())); +by (auto_tac (claset() addSIs [subset_imp_LeadsTo] addSEs [int_neqE], + simpset())); qed "E_thm05c"; (*lift_2*) @@ -198,15 +179,12 @@ by Safe_tac; (*this step consolidates two formulae to the goal metric n s' <= metric n s*) by (etac (linorder_leI RS order_antisym RS sym) 1); -by (REPEAT_FIRST (eresolve_tac mov_metrics)); -by (REPEAT_FIRST distinct_tac); +by (REPEAT_FIRST (eresolve_tac mov_metrics ORELSE' distinct_tac)); (** LEVEL 6 **) -by (ALLGOALS (asm_simp_tac (simpset() addsimps - [zle_def] @ metric_simps @ zcompare_rls))); +by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls))); qed "E_thm12a"; - (*lem_lift_4_3 *) Goal "#0 < N ==> \ \ Lift : (moving Int Req n Int {s. metric n s = N} Int \ @@ -217,8 +195,7 @@ by Safe_tac; (*this step consolidates two formulae to the goal metric n s' <= metric n s*) by (etac (linorder_leI RS order_antisym RS sym) 1); -by (REPEAT_FIRST (eresolve_tac mov_metrics)); -by (REPEAT_FIRST distinct_tac); +by (REPEAT_FIRST (eresolve_tac mov_metrics ORELSE' distinct_tac)); (** LEVEL 6 **) by (ALLGOALS (asm_simp_tac (simpset() addsimps metric_simps @ zcompare_rls))); qed "E_thm12b"; @@ -227,10 +204,9 @@ Goal "#0 Lift : (moving Int Req n Int {s. metric n s = N} Int \ \ {s. floor s ~: req s}) LeadsTo \ \ (moving Int Req n Int {s. metric n s < N})"; -by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); -by (etac E_thm12b 3); -by (etac E_thm12a 2); -by (Blast_tac 1); +by (rtac ([subset_imp_LeadsTo, [E_thm12a, E_thm12b] MRS LeadsTo_Un] + MRS LeadsTo_Trans) 1); +by Auto_tac; qed "lift_4"; @@ -278,11 +254,10 @@ (*lift_5*) Goal "#0 Lift : (closed Int Req n Int {s. metric n s = N}) LeadsTo \ \ (moving Int Req n Int {s. metric n s < N})"; -by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); -by (etac E_thm16b 3); -by (etac E_thm16a 2); +by (rtac ([subset_imp_LeadsTo, [E_thm16a, E_thm16b] MRS LeadsTo_Un] + MRS LeadsTo_Trans) 1); by (dtac E_thm16c 1); -by (Blast_tac 1); +by Auto_tac; qed "lift_5"; @@ -357,35 +332,33 @@ by (rtac (Always_nonneg RS integ_0_le_induct) 1); by (case_tac "#0 < z" 1); (*If z <= #0 then actually z = #0*) -by (fold_tac [zle_def]); -by (force_tac (claset() addIs [R_thm11, order_antisym], simpset()) 2); +by (force_tac (claset() addIs [R_thm11, order_antisym], + simpset() addsimps [linorder_not_less]) 2); by (rtac ([asm_rl, Un_upper1] MRS LeadsTo_weaken_R) 1); -by (rtac ([subset_imp_LeadsTo, LeadsTo_Un] MRS LeadsTo_Trans) 1); -by (rtac lift_3_Req 3); -by (rtac lift_4 2); +by (rtac ([subset_imp_LeadsTo, [lift_4, lift_3_Req] MRS LeadsTo_Un] + MRS LeadsTo_Trans) 1); by Auto_tac; qed "lift_3"; +val LeadsTo_Trans_Un' = rotate_prems 1 LeadsTo_Trans_Un; +(* [| Lift: B LeadsTo C; Lift: A LeadsTo B |] ==> Lift: (A Un B) LeadsTo C *) + Goal "Lift : (Req n) LeadsTo (opened Int atFloor n)"; by (rtac LeadsTo_Trans 1); -by (rtac (E_thm04 RS LeadsTo_Un) 2); -by (rtac LeadsTo_Un_post 2); +by (rtac ([E_thm04, LeadsTo_Un_post] MRS LeadsTo_Un) 2); by (rtac (E_thm01 RS LeadsTo_Trans_Un') 2); by (rtac (lift_3 RS LeadsTo_Trans_Un') 2); by (rtac (lift_2 RS LeadsTo_Trans_Un') 2); -by (rtac (E_thm03 RS LeadsTo_Trans_Un') 2); -by (rtac E_thm02 2); +by (rtac ([E_thm03,E_thm02] MRS LeadsTo_Trans_Un') 2); by (rtac (open_move RS Always_LeadsToI) 1); -by (rtac (open_stop RS Always_LeadsToI) 1); -by (rtac subset_imp_LeadsTo 1); +by (rtac ([open_stop, subset_imp_LeadsTo] MRS Always_LeadsToI) 1); by (Clarify_tac 1); (*The case split is not essential but makes Blast_tac much faster. - Must also be careful to prevent simplification from looping*) + Calling rotate_tac prevents simplification from looping*) by (case_tac "open x" 1); by (ALLGOALS (rotate_tac ~1)); -by (ALLGOALS Asm_full_simp_tac); -by (Blast_tac 1); +by Auto_tac; qed "lift_1"; Close_locale "floor"; diff -r e53d5f0c7c94 -r c318acb88251 src/HOL/UNITY/Mutex.ML --- a/src/HOL/UNITY/Mutex.ML Wed Sep 01 11:15:35 1999 +0200 +++ b/src/HOL/UNITY/Mutex.ML Wed Sep 01 11:16:02 1999 +0200 @@ -17,15 +17,11 @@ Goal "Mutex : Always IU"; -by (rtac AlwaysI 1); -by (constrains_tac 2); -by Auto_tac; +by (always_tac 1); qed "IU"; Goal "Mutex : Always IV"; -by (rtac AlwaysI 1); -by (constrains_tac 2); -by Auto_tac; +by (always_tac 1); qed "IV"; (*The safety property: mutual exclusion*) @@ -38,8 +34,7 @@ (*The bad invariant FAILS in V1*) Goal "Mutex : Always bad_IU"; -by (rtac AlwaysI 1); -by (constrains_tac 2); +by (always_tac 1); by Auto_tac; (*Resulting state: n=1, p=false, m=4, u=false. Execution of V1 (the command of process v guarded by n=1) sets p:=true, diff -r e53d5f0c7c94 -r c318acb88251 src/HOL/UNITY/Reach.ML --- a/src/HOL/UNITY/Reach.ML Wed Sep 01 11:15:35 1999 +0200 +++ b/src/HOL/UNITY/Reach.ML Wed Sep 01 11:16:02 1999 +0200 @@ -30,9 +30,7 @@ Addsimps [simp_of_set reach_invariant_def]; Goal "Rprg : Always reach_invariant"; -by (rtac AlwaysI 1); -by Auto_tac; (*for the initial state; proof of stability remains*) -by (constrains_tac 1); +by (always_tac 1); by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1); qed "reach_invariant"; diff -r e53d5f0c7c94 -r c318acb88251 src/HOL/UNITY/Token.ML --- a/src/HOL/UNITY/Token.ML Wed Sep 01 11:15:35 1999 +0200 +++ b/src/HOL/UNITY/Token.ML Wed Sep 01 11:16:02 1999 +0200 @@ -71,8 +71,7 @@ by (case_tac "i=j" 1); by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1); by (rtac (TR7 RS leadsTo_weaken_R) 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1); +by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq])); qed "TR7_nodeOrder"; @@ -80,8 +79,7 @@ Goal "[| i F : (HasTok i) leadsTo {s. (token s, i) : nodeOrder j}"; by (rtac (TR7 RS leadsTo_weaken_R) 1); -by (Clarify_tac 1); -by (asm_full_simp_tac (simpset() addsimps [HasTok_def, nodeOrder_eq]) 1); +by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_eq])); qed "TR7_aux"; Goal "({s. token s < N} Int token -`` {m}) = \ @@ -100,15 +98,13 @@ by (Blast_tac 2); by (Clarify_tac 1); by (rtac (TR7_aux RS leadsTo_weaken) 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [nodeOrder_def, HasTok_def]))); -by (ALLGOALS Blast_tac); +by (auto_tac (claset(), simpset() addsimps [HasTok_def, nodeOrder_def])); qed "leadsTo_j"; (*Misra's TR8: a hungry process eventually eats*) Goal "j F : ({s. token s < N} Int H j) leadsTo (E j)"; by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1); by (rtac TR6 2); -by (rtac leadsTo_weaken 1); -by (rtac ([leadsTo_j, TR3] MRS psp) 1); +by (rtac ([leadsTo_j, TR3] MRS psp RS leadsTo_weaken) 1); by (ALLGOALS Blast_tac); qed "token_progress"; diff -r e53d5f0c7c94 -r c318acb88251 src/HOL/UNITY/UNITY.ML --- a/src/HOL/UNITY/UNITY.ML Wed Sep 01 11:15:35 1999 +0200 +++ b/src/HOL/UNITY/UNITY.ML Wed Sep 01 11:16:02 1999 +0200 @@ -112,7 +112,9 @@ (*** co ***) -overload_1st_set "UNITY.op co"; +(*These operators are not overloaded, but their operands are sets, and + ultimately there's a risk of reaching equality, which IS overloaded*) +overload_1st_set "UNITY.constrains"; overload_1st_set "UNITY.stable"; overload_1st_set "UNITY.unless";