added the new elim rule psubsetE
authorpaulson
Thu Oct 03 10:34:51 2002 +0200 (2002-10-03)
changeset 1362417684cf64fda
parent 13623 c2b235e60f8b
child 13625 ca86e84ce200
added the new elim rule psubsetE
src/HOL/HoareParallel/Gar_Coll.thy
src/HOL/Real/PReal.ML
src/HOL/Set.thy
     1.1 --- a/src/HOL/HoareParallel/Gar_Coll.thy	Thu Oct 03 09:54:54 2002 +0200
     1.2 +++ b/src/HOL/HoareParallel/Gar_Coll.thy	Thu Oct 03 10:34:51 2002 +0200
     1.3 @@ -3,6 +3,8 @@
     1.4  
     1.5  theory Gar_Coll = Graph + OG_Syntax:
     1.6  
     1.7 +declare psubsetE [rule del]
     1.8 +
     1.9  text {* Declaration of variables: *}
    1.10  
    1.11  record gar_coll_state =
     2.1 --- a/src/HOL/Real/PReal.ML	Thu Oct 03 09:54:54 2002 +0200
     2.2 +++ b/src/HOL/Real/PReal.ML	Thu Oct 03 10:34:51 2002 +0200
     2.3 @@ -1167,14 +1167,7 @@
     2.4  \         ==> (ALL Y. (EX X: P. Y < X) = (Y < psup P))";              
     2.5  by (forward_tac [preal_sup RS Abs_preal_inverse] 1);
     2.6  by (Fast_tac 1);
     2.7 -by (auto_tac (claset() addSIs [psubsetI],simpset() addsimps [psup_def,preal_less_def]));
     2.8 -by (blast_tac (claset() addDs [psubset_def RS meta_eq_to_obj_eq RS iffD1]) 1);
     2.9 -by (rotate_tac 4 1);
    2.10 -by (asm_full_simp_tac (simpset() addsimps [psubset_def]) 1);
    2.11 -by (dtac bspec 1 THEN assume_tac 1);
    2.12 -by (REPEAT(etac conjE 1));
    2.13 -by (EVERY1[rtac contrapos_np, assume_tac]);
    2.14 -by (auto_tac (claset() addSDs [lemma_psubset_mem],simpset()));
    2.15 +by (auto_tac (claset(), simpset() addsimps [psup_def,preal_less_def]));
    2.16  by (cut_inst_tac [("r1.0","Xa"),("r2.0","Ya")] preal_linear 1);
    2.17  by (auto_tac (claset() addDs [psubsetD],simpset() addsimps [preal_less_def]));
    2.18  qed "preal_complete";
     3.1 --- a/src/HOL/Set.thy	Thu Oct 03 09:54:54 2002 +0200
     3.2 +++ b/src/HOL/Set.thy	Thu Oct 03 10:34:51 2002 +0200
     3.3 @@ -834,6 +834,10 @@
     3.4  lemma psubsetI [intro!]: "A \<subseteq> B ==> A \<noteq> B ==> A \<subset> B"
     3.5    by (unfold psubset_def) blast
     3.6  
     3.7 +lemma psubsetE [elim!]: 
     3.8 +    "[|A \<subset> B;  [|A \<subseteq> B; ~ (B\<subseteq>A)|] ==> R|] ==> R"
     3.9 +  by (unfold psubset_def) blast
    3.10 +
    3.11  lemma psubset_insert_iff:
    3.12    "(A \<subset> insert x B) = (if x \<in> B then A \<subset> B else if x \<in> A then A - {x} \<subset> B else A \<subseteq> B)"
    3.13    by (auto simp add: psubset_def subset_insert_iff)