src/HOL/IOA/Solve.ML
changeset 6916 4957978b6f9e
parent 5184 9b8547a9496a
child 7499 23e090051cb8
     1.1 --- a/src/HOL/IOA/Solve.ML	Thu Jul 08 13:38:41 1999 +0200
     1.2 +++ b/src/HOL/IOA/Solve.ML	Thu Jul 08 13:42:31 1999 +0200
     1.3 @@ -73,13 +73,13 @@
     1.4  \                (fst ex),                                                \
     1.5  \    %i. fst (snd ex i))")]  bexI 1);
     1.6  (* fst(s) is in projected execution *)
     1.7 - by (Simp_tac 1);
     1.8 - by (fast_tac (claset() delSWrapper"split_all_tac")1);
     1.9 + by (Force_tac 1);
    1.10  (* projected execution is indeed an execution *)
    1.11  by (asm_full_simp_tac
    1.12 -      (simpset() addsimps [executions_def,is_execution_fragment_def,
    1.13 -                          par_def,starts_of_def,trans_of_def,filter_oseq_def]
    1.14 -                addsplits [option.split]) 1);
    1.15 +      (simpset() delcongs [if_weak_cong]
    1.16 +		 addsimps [executions_def,is_execution_fragment_def,
    1.17 +			   par_def,starts_of_def,trans_of_def,filter_oseq_def]
    1.18 +                 addsplits [option.split]) 1);
    1.19  qed"comp1_reachable";
    1.20  
    1.21  
    1.22 @@ -93,23 +93,25 @@
    1.23  \                (fst ex),                                                \
    1.24  \    %i. snd (snd ex i))")]  bexI 1);
    1.25  (* fst(s) is in projected execution *)
    1.26 - by (Simp_tac 1);
    1.27 - by (fast_tac (claset() delSWrapper"split_all_tac")1);
    1.28 + by (Force_tac 1);
    1.29  (* projected execution is indeed an execution *)
    1.30  by (asm_full_simp_tac
    1.31 -      (simpset() addsimps [executions_def,is_execution_fragment_def,
    1.32 -                          par_def,starts_of_def,trans_of_def,filter_oseq_def]
    1.33 -                addsplits [option.split]) 1);
    1.34 +      (simpset() delcongs [if_weak_cong]
    1.35 +		 addsimps [executions_def,is_execution_fragment_def,
    1.36 +			   par_def,starts_of_def,trans_of_def,filter_oseq_def]
    1.37 +                 addsplits [option.split]) 1);
    1.38  qed"comp2_reachable";
    1.39  
    1.40 -Delsplits [split_if];
    1.41 +Delsplits [split_if]; Delcongs [if_weak_cong];
    1.42  
    1.43 -(* Composition of possibility-mappings *)
    1.44 -Goalw [is_weak_pmap_def] "[| is_weak_pmap f C1 A1 & \
    1.45 -\               externals(asig_of(A1))=externals(asig_of(C1)) &\
    1.46 -\               is_weak_pmap g C2 A2 &  \
    1.47 -\               externals(asig_of(A2))=externals(asig_of(C2)) & \
    1.48 -\               compat_ioas C1 C2 & compat_ioas A1 A2  |]     \
    1.49 +(* THIS THEOREM IS NEVER USED (lcp)
    1.50 +   Composition of possibility-mappings *)
    1.51 +Goalw [is_weak_pmap_def]
    1.52 +     "[| is_weak_pmap f C1 A1; \
    1.53 +\        externals(asig_of(A1))=externals(asig_of(C1));\
    1.54 +\        is_weak_pmap g C2 A2;  \
    1.55 +\        externals(asig_of(A2))=externals(asig_of(C2)); \
    1.56 +\        compat_ioas C1 C2; compat_ioas A1 A2  |]     \
    1.57  \  ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)";
    1.58   by (rtac conjI 1);
    1.59  (* start_states *)
    1.60 @@ -117,7 +119,6 @@
    1.61  (* transitions *)
    1.62  by (REPEAT (rtac allI 1));
    1.63  by (rtac imp_conj_lemma 1);
    1.64 -by (REPEAT(etac conjE 1));
    1.65  by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1);
    1.66  by (simp_tac (simpset() addsimps [par_def]) 1);
    1.67  by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
    1.68 @@ -144,8 +145,8 @@
    1.69  by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
    1.70                   addsplits [split_if]) 1);
    1.71  by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
    1.72 -        asm_full_simp_tac(simpset() addsimps[comp1_reachable,
    1.73 -                                      comp2_reachable])1));
    1.74 +	   asm_full_simp_tac(simpset() addsimps[comp1_reachable,
    1.75 +						comp2_reachable])1));
    1.76  qed"fxg_is_weak_pmap_of_product_IOA";
    1.77  
    1.78  
    1.79 @@ -210,3 +211,4 @@
    1.80  qed"rename_through_pmap";
    1.81  
    1.82  Addsplits [split_if];
    1.83 +Addcongs  [if_weak_cong];