src/HOL/UNITY/SubstAx.ML
changeset 5313 1861a564d7e2
parent 5277 e4297d03e5d2
child 5340 d75c03cf77b5
     1.1 --- a/src/HOL/UNITY/SubstAx.ML	Thu Aug 13 17:44:50 1998 +0200
     1.2 +++ b/src/HOL/UNITY/SubstAx.ML	Thu Aug 13 18:06:40 1998 +0200
     1.3 @@ -7,32 +7,22 @@
     1.4  *)
     1.5  
     1.6  
     1.7 -(*constrains (Acts prg) B B'
     1.8 -  ==> constrains (Acts prg) (reachable prg Int B) (reachable prg Int B')*)
     1.9 -bind_thm ("constrains_reachable",
    1.10 -	  rewrite_rule [stable_def] stable_reachable RS constrains_Int);
    1.11 -
    1.12  
    1.13  (*** Specialized laws for handling invariants ***)
    1.14  
    1.15 -Goal "invariant prg INV ==> reachable prg Int INV = reachable prg";
    1.16 -bd invariant_includes_reachable 1;
    1.17 -by (Blast_tac 1);
    1.18 -qed "reachable_Int_INV";
    1.19 -
    1.20 -Goal "[| invariant prg INV;  LeadsTo prg (INV Int A) A' |]   \
    1.21 +Goal "[| Invariant prg INV;  LeadsTo prg (INV Int A) A' |]   \
    1.22  \     ==> LeadsTo prg A A'";
    1.23  by (asm_full_simp_tac
    1.24      (simpset() addsimps [LeadsTo_def, reachable_Int_INV,
    1.25  			 Int_assoc RS sym]) 1);
    1.26 -qed "invariant_LeadsToI";
    1.27 +qed "Invariant_LeadsToI";
    1.28  
    1.29 -Goal "[| invariant prg INV;  LeadsTo prg A A' |]   \
    1.30 +Goal "[| Invariant prg INV;  LeadsTo prg A A' |]   \
    1.31  \     ==> LeadsTo prg A (INV Int A')";
    1.32  by (asm_full_simp_tac
    1.33      (simpset() addsimps [LeadsTo_def, reachable_Int_INV,
    1.34  			 Int_assoc RS sym]) 1);
    1.35 -qed "invariant_LeadsToD";
    1.36 +qed "Invariant_LeadsToD";
    1.37  
    1.38  
    1.39  (*** Introduction rules: Basis, Trans, Union ***)
    1.40 @@ -42,9 +32,6 @@
    1.41  by (blast_tac (claset() addIs [psp_stable2, stable_reachable]) 1);
    1.42  qed "leadsTo_imp_LeadsTo";
    1.43  
    1.44 -(* ensures (Acts prg) A B ==> LeadsTo prg A B *)
    1.45 -bind_thm ("LeadsTo_Basis", leadsTo_Basis RS leadsTo_imp_LeadsTo);
    1.46 -
    1.47  Goal "[| LeadsTo prg A B;  LeadsTo prg B C |] ==> LeadsTo prg A C";
    1.48  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
    1.49  by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
    1.50 @@ -138,33 +125,37 @@
    1.51  qed "LeadsTo_weaken";
    1.52  
    1.53  
    1.54 -(** More rules using the premise "invariant prg" **)
    1.55 +(** More rules using the premise "Invariant prg" **)
    1.56  
    1.57 -Goal "[| invariant prg INV;      \
    1.58 -\        constrains (Acts prg) (INV Int (A-A')) (A Un A'); \
    1.59 +Goalw [LeadsTo_def, Constrains_def]
    1.60 +     "[| Constrains prg (A-A') (A Un A'); transient  (Acts prg) (A-A') |]   \
    1.61 +\     ==> LeadsTo prg A A'";
    1.62 +by (rtac (ensuresI RS leadsTo_Basis) 1);
    1.63 +by (blast_tac (claset() addIs [transient_strengthen]) 2);
    1.64 +by (blast_tac (claset() addIs [constrains_weaken]) 1);
    1.65 +qed "LeadsTo_Basis";
    1.66 +
    1.67 +Goal "[| Invariant prg INV;      \
    1.68 +\        Constrains prg (INV Int (A-A')) (A Un A'); \
    1.69  \        transient  (Acts prg) (INV Int (A-A')) |]   \
    1.70  \ ==> LeadsTo prg A A'";
    1.71 -br invariant_LeadsToI 1;
    1.72 -ba 1;
    1.73 -by (rtac (ensuresI RS LeadsTo_Basis) 1);
    1.74 -by (ALLGOALS 
    1.75 -    (full_simp_tac (simpset() addsimps [Int_Diff, Int_Un_distrib RS sym, 
    1.76 -					Diff_Int_distrib RS sym])));
    1.77 -be invariantE 1;
    1.78 -by (blast_tac (claset() addSDs [stable_constrains_Int]
    1.79 -			addIs [constrains_weaken]) 1);
    1.80 -qed "invariant_LeadsTo_Basis";
    1.81 +by (rtac Invariant_LeadsToI 1);
    1.82 +by (assume_tac 1);
    1.83 +by (rtac LeadsTo_Basis 1);
    1.84 +by (blast_tac (claset() addIs [transient_strengthen]) 2);
    1.85 +by (blast_tac (claset() addIs [Invariant_ConstrainsD RS Constrains_weaken]) 1);
    1.86 +qed "Invariant_LeadsTo_Basis";
    1.87  
    1.88 -Goal "[| invariant prg INV;      \
    1.89 +Goal "[| Invariant prg INV;      \
    1.90  \        LeadsTo prg A A'; id: Acts prg;   \
    1.91  \        INV Int B  <= A;  INV Int A' <= B' |] \
    1.92  \     ==> LeadsTo prg B B'";
    1.93 -br invariant_LeadsToI 1;
    1.94 -ba 1;
    1.95 -bd invariant_LeadsToD 1;
    1.96 -ba 1;
    1.97 +by (rtac Invariant_LeadsToI 1);
    1.98 +by (assume_tac 1);
    1.99 +by (dtac Invariant_LeadsToD 1);
   1.100 +by (assume_tac 1);
   1.101  by (blast_tac (claset()addIs [LeadsTo_weaken]) 1);
   1.102 -qed "invariant_LeadsTo_weaken";
   1.103 +qed "Invariant_LeadsTo_weaken";
   1.104  
   1.105  
   1.106  (*Set difference: maybe combine with leadsTo_weaken_L??
   1.107 @@ -250,43 +241,39 @@
   1.108  (** PSP: Progress-Safety-Progress **)
   1.109  
   1.110  (*Special case of PSP: Misra's "stable conjunction".  Doesn't need id:Acts. *)
   1.111 -Goal "[| LeadsTo prg A A'; stable (Acts prg) B |] \
   1.112 -\     ==> LeadsTo prg (A Int B) (A' Int B)";
   1.113 -by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Int_assoc RS sym, 
   1.114 -					   psp_stable]) 1);
   1.115 +Goal
   1.116 +  "[| LeadsTo prg A A';  Stable prg B |] ==> LeadsTo prg (A Int B) (A' Int B)";
   1.117 +by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
   1.118 +by (dtac psp_stable 1);
   1.119 +by (assume_tac 1);
   1.120 +by (asm_full_simp_tac (simpset() addsimps Int_ac) 1);
   1.121  qed "PSP_stable";
   1.122  
   1.123 -Goal "[| LeadsTo prg A A'; stable (Acts prg) B |] \
   1.124 +Goal "[| LeadsTo prg A A'; Stable prg B |] \
   1.125  \     ==> LeadsTo prg (B Int A) (B Int A')";
   1.126  by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
   1.127  qed "PSP_stable2";
   1.128  
   1.129 -
   1.130 -Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: Acts prg |] \
   1.131 +Goalw [LeadsTo_def, Constrains_def]
   1.132 +     "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
   1.133  \     ==> LeadsTo prg (A Int B) ((A' Int B) Un (B' - B))";
   1.134 -by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   1.135 -by (dtac psp 1);
   1.136 -by (etac constrains_reachable 1);
   1.137 -by (etac leadsTo_weaken 2);
   1.138 -by (ALLGOALS Blast_tac);
   1.139 +by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
   1.140  qed "PSP";
   1.141  
   1.142 -Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: Acts prg |] \
   1.143 +Goal "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
   1.144  \     ==> LeadsTo prg (B Int A) ((B Int A') Un (B' - B))";
   1.145  by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
   1.146  qed "PSP2";
   1.147  
   1.148 -Goalw [unless_def]
   1.149 -   "[| LeadsTo prg A A'; unless (Acts prg) B B'; id: Acts prg |] \
   1.150 +Goalw [Unless_def]
   1.151 +     "[| LeadsTo prg A A'; Unless prg B B'; id: Acts prg |] \
   1.152  \     ==> LeadsTo prg (A Int B) ((A' Int B) Un B')";
   1.153  by (dtac PSP 1);
   1.154  by (assume_tac 1);
   1.155 -by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
   1.156 -by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
   1.157 -by (etac LeadsTo_Diff 2);
   1.158 -by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 2);
   1.159 -by Auto_tac;
   1.160 -qed "PSP_unless";
   1.161 +by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken, 
   1.162 +			       subset_imp_LeadsTo]) 2);
   1.163 +by (assume_tac 1);
   1.164 +qed "PSP_Unless";
   1.165  
   1.166  
   1.167  (*** Induction rules ***)
   1.168 @@ -294,7 +281,7 @@
   1.169  (** Meta or object quantifier ????? **)
   1.170  Goal "[| wf r;     \
   1.171  \        ALL m. LeadsTo prg (A Int f-``{m})                     \
   1.172 -\                                 ((A Int f-``(r^-1 ^^ {m})) Un B);   \
   1.173 +\                           ((A Int f-``(r^-1 ^^ {m})) Un B);   \
   1.174  \        id: Acts prg |] \
   1.175  \     ==> LeadsTo prg A B";
   1.176  by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   1.177 @@ -353,49 +340,42 @@
   1.178  
   1.179  (*** Completion: Binary and General Finite versions ***)
   1.180  
   1.181 -Goal "[| LeadsTo prg A A';  stable (Acts prg) A';   \
   1.182 -\        LeadsTo prg B B';  stable (Acts prg) B';  id: Acts prg |] \
   1.183 +Goal "[| LeadsTo prg A A';  Stable prg A';   \
   1.184 +\        LeadsTo prg B B';  Stable prg B';  id: Acts prg |] \
   1.185  \     ==> LeadsTo prg (A Int B) (A' Int B')";
   1.186 -by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
   1.187 -by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken] 
   1.188 -                        addSIs [stable_Int, stable_reachable]) 1);
   1.189 +by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
   1.190 +by (blast_tac (claset() addIs [stable_completion, leadsTo_weaken]) 1);
   1.191  qed "Stable_completion";
   1.192  
   1.193  
   1.194 -Goal "[| finite I;  id: Acts prg |]                     \
   1.195 +Goal "[| finite I;  id: Acts prg |]      \
   1.196  \     ==> (ALL i:I. LeadsTo prg (A i) (A' i)) -->  \
   1.197 -\         (ALL i:I. stable (Acts prg) (A' i)) -->         \
   1.198 +\         (ALL i:I. Stable prg (A' i)) -->         \
   1.199  \         LeadsTo prg (INT i:I. A i) (INT i:I. A' i)";
   1.200  by (etac finite_induct 1);
   1.201  by (Asm_simp_tac 1);
   1.202 -by (asm_simp_tac 
   1.203 -    (simpset() addsimps [Stable_completion, stable_def, 
   1.204 -			 ball_constrains_INT]) 1);
   1.205 +by (asm_simp_tac (simpset() addsimps [Stable_completion, ball_Stable_INT]) 1);
   1.206  qed_spec_mp "Finite_stable_completion";
   1.207  
   1.208  
   1.209 -Goal "[| LeadsTo prg A (A' Un C);  constrains (Acts prg) A' (A' Un C); \
   1.210 -\        LeadsTo prg B (B' Un C);  constrains (Acts prg) B' (B' Un C); \
   1.211 +Goal "[| LeadsTo prg A (A' Un C);  Constrains prg A' (A' Un C); \
   1.212 +\        LeadsTo prg B (B' Un C);  Constrains prg B' (B' Un C); \
   1.213  \        id: Acts prg |] \
   1.214  \     ==> LeadsTo prg (A Int B) ((A' Int B') Un C)";
   1.215 -by (full_simp_tac (simpset() addsimps [LeadsTo_def, Int_Un_distrib]) 1);
   1.216 -by (dtac completion 1);
   1.217 -by (assume_tac 2);
   1.218 -by (ALLGOALS 
   1.219 -    (asm_simp_tac 
   1.220 -     (simpset() addsimps [constrains_reachable, Int_Un_distrib RS sym])));
   1.221 -by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
   1.222 +by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def,
   1.223 +				       Int_Un_distrib]) 1);
   1.224 +by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
   1.225  qed "Completion";
   1.226  
   1.227  
   1.228  Goal "[| finite I;  id: Acts prg |] \
   1.229  \     ==> (ALL i:I. LeadsTo prg (A i) (A' i Un C)) -->  \
   1.230 -\         (ALL i:I. constrains (Acts prg) (A' i) (A' i Un C)) --> \
   1.231 +\         (ALL i:I. Constrains prg (A' i) (A' i Un C)) --> \
   1.232  \         LeadsTo prg (INT i:I. A i) ((INT i:I. A' i) Un C)";
   1.233  by (etac finite_induct 1);
   1.234  by (ALLGOALS Asm_simp_tac);
   1.235  by (Clarify_tac 1);
   1.236 -by (dtac ball_constrains_INT 1);
   1.237 +by (dtac ball_Constrains_INT 1);
   1.238  by (asm_full_simp_tac (simpset() addsimps [Completion]) 1); 
   1.239  qed "Finite_completion";
   1.240  
   1.241 @@ -408,22 +388,22 @@
   1.242  (*proves "constrains" properties when the program is specified*)
   1.243  fun constrains_tac (main_def::cmd_defs) = 
   1.244     SELECT_GOAL
   1.245 -      (EVERY [TRY (rtac stableI 1),
   1.246 +      (EVERY [REPEAT (resolve_tac [StableI, stableI,
   1.247 +				   constrains_imp_Constrains] 1),
   1.248  	      rtac constrainsI 1,
   1.249  	      full_simp_tac (simpset() addsimps [main_def]) 1,
   1.250 -	      REPEAT_FIRST (eresolve_tac [disjE]),
   1.251 +	      REPEAT_FIRST (etac disjE ),
   1.252  	      rewrite_goals_tac cmd_defs,
   1.253  	      ALLGOALS (SELECT_GOAL Auto_tac)]);
   1.254  
   1.255  
   1.256 -(*proves "ensures" properties when the program is specified*)
   1.257 +(*proves "ensures/leadsTo" properties when the program is specified*)
   1.258  fun ensures_tac (main_def::cmd_defs) sact = 
   1.259      SELECT_GOAL
   1.260 -      (EVERY [REPEAT (invariant_Int_tac 1),
   1.261 -	      etac invariant_LeadsTo_Basis 1 
   1.262 +      (EVERY [REPEAT (Invariant_Int_tac 1),
   1.263 +	      etac Invariant_LeadsTo_Basis 1 
   1.264  	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   1.265 -		  REPEAT (ares_tac [leadsTo_imp_LeadsTo, leadsTo_Basis, 
   1.266 -				    ensuresI] 1),
   1.267 +		  REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1),
   1.268  	      res_inst_tac [("act", sact)] transient_mem 2,
   1.269  	      simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3,
   1.270  	      simp_tac (simpset() addsimps [main_def]) 2,