added select_equality to the implicit claset
authoroheimb
Thu Jan 08 18:09:07 1998 +0100 (1998-01-08)
changeset 4535f24cebc299e4
parent 4534 6932c3ae3912
child 4536 74f7c556fd90
added select_equality to the implicit claset
src/HOL/Induct/LFilter.ML
src/HOL/NatDef.ML
src/HOL/Sexp.ML
src/HOL/Sum.ML
src/HOL/Univ.ML
src/HOL/cladata.ML
src/HOLCF/Sprod0.ML
src/HOLCF/Ssum0.ML
src/HOLCF/Ssum1.ML
     1.1 --- a/src/HOL/Induct/LFilter.ML	Thu Jan 08 18:08:43 1998 +0100
     1.2 +++ b/src/HOL/Induct/LFilter.ML	Thu Jan 08 18:09:07 1998 +0100
     1.3 @@ -69,12 +69,12 @@
     1.4  (*** find: basic equations ***)
     1.5  
     1.6  goalw thy [find_def] "find p LNil = LNil";
     1.7 -by (blast_tac (claset() addIs [select_equality]) 1);
     1.8 +by (Blast_tac 1);
     1.9  qed "find_LNil";
    1.10  Addsimps [find_LNil];
    1.11  
    1.12  goalw thy [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
    1.13 -by (blast_tac (claset() addIs [select_equality] addDs [findRel_functional]) 1);
    1.14 +by (blast_tac (claset() addDs [findRel_functional]) 1);
    1.15  qed "findRel_imp_find";
    1.16  Addsimps [findRel_imp_find];
    1.17  
    1.18 @@ -84,7 +84,7 @@
    1.19  Addsimps [find_LCons_found];
    1.20  
    1.21  goalw thy [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
    1.22 -by (blast_tac (claset() addIs [select_equality]) 1);
    1.23 +by (Blast_tac 1);
    1.24  qed "diverge_find_LNil";
    1.25  Addsimps [diverge_find_LNil];
    1.26  
     2.1 --- a/src/HOL/NatDef.ML	Thu Jan 08 18:08:43 1998 +0100
     2.2 +++ b/src/HOL/NatDef.ML	Thu Jan 08 18:09:07 1998 +0100
     2.3 @@ -135,11 +135,11 @@
     2.4  (*** nat_case -- the selection operator for nat ***)
     2.5  
     2.6  goalw thy [nat_case_def] "nat_case a f 0 = a";
     2.7 -by (blast_tac (claset() addIs [select_equality]) 1);
     2.8 +by (Blast_tac 1);
     2.9  qed "nat_case_0";
    2.10  
    2.11  goalw thy [nat_case_def] "nat_case a f (Suc k) = f(k)";
    2.12 -by (blast_tac (claset() addIs [select_equality]) 1);
    2.13 +by (Blast_tac 1);
    2.14  qed "nat_case_Suc";
    2.15  
    2.16  goalw thy [wf_def, pred_nat_def] "wf(pred_nat)";
     3.1 --- a/src/HOL/Sexp.ML	Thu Jan 08 18:08:43 1998 +0100
     3.2 +++ b/src/HOL/Sexp.ML	Thu Jan 08 18:09:07 1998 +0100
     3.3 @@ -11,15 +11,15 @@
     3.4  (** sexp_case **)
     3.5  
     3.6  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Leaf a) = c(a)";
     3.7 -by (blast_tac (claset() addSIs [select_equality]) 1);
     3.8 +by (Blast_tac 1);
     3.9  qed "sexp_case_Leaf";
    3.10  
    3.11  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (Numb k) = d(k)";
    3.12 -by (blast_tac (claset() addSIs [select_equality]) 1);
    3.13 +by (Blast_tac 1);
    3.14  qed "sexp_case_Numb";
    3.15  
    3.16  goalw Sexp.thy [sexp_case_def] "sexp_case c d e (M$N) = e M N";
    3.17 -by (blast_tac (claset() addSIs [select_equality]) 1);
    3.18 +by (Blast_tac 1);
    3.19  qed "sexp_case_Scons";
    3.20  
    3.21  Addsimps [sexp_case_Leaf, sexp_case_Numb, sexp_case_Scons];
     4.1 --- a/src/HOL/Sum.ML	Thu Jan 08 18:08:43 1998 +0100
     4.2 +++ b/src/HOL/Sum.ML	Thu Jan 08 18:09:07 1998 +0100
     4.3 @@ -119,11 +119,11 @@
     4.4  (** sum_case -- the selection operator for sums **)
     4.5  
     4.6  goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
     4.7 -by (blast_tac (claset() addIs [select_equality]) 1);
     4.8 +by (Blast_tac 1);
     4.9  qed "sum_case_Inl";
    4.10  
    4.11  goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
    4.12 -by (blast_tac (claset() addIs [select_equality]) 1);
    4.13 +by (Blast_tac 1);
    4.14  qed "sum_case_Inr";
    4.15  
    4.16  Addsimps [sum_case_Inl, sum_case_Inr];
     5.1 --- a/src/HOL/Univ.ML	Thu Jan 08 18:08:43 1998 +0100
     5.2 +++ b/src/HOL/Univ.ML	Thu Jan 08 18:09:07 1998 +0100
     5.3 @@ -432,15 +432,15 @@
     5.4  (*** Split and Case ***)
     5.5  
     5.6  goalw Univ.thy [Split_def] "Split c (M$N) = c M N";
     5.7 -by (blast_tac (claset() addIs [select_equality]) 1);
     5.8 +by (Blast_tac  1);
     5.9  qed "Split";
    5.10  
    5.11  goalw Univ.thy [Case_def] "Case c d (In0 M) = c(M)";
    5.12 -by (blast_tac (claset() addIs [select_equality]) 1);
    5.13 +by (Blast_tac 1);
    5.14  qed "Case_In0";
    5.15  
    5.16  goalw Univ.thy [Case_def] "Case c d (In1 N) = d(N)";
    5.17 -by (blast_tac (claset() addIs [select_equality]) 1);
    5.18 +by (Blast_tac 1);
    5.19  qed "Case_In1";
    5.20  
    5.21  Addsimps [Split, Case_In0, Case_In1];
     6.1 --- a/src/HOL/cladata.ML	Thu Jan 08 18:08:43 1998 +0100
     6.2 +++ b/src/HOL/cladata.ML	Thu Jan 08 18:09:07 1998 +0100
     6.3 @@ -47,7 +47,7 @@
     6.4                         addSEs [conjE,disjE,impCE,FalseE,iffCE];
     6.5  
     6.6  (*Quantifier rules*)
     6.7 -val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI] 
     6.8 +val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, select_equality] 
     6.9                       addSEs [exE] addEs [allE];
    6.10  
    6.11  claset_ref() := HOL_cs;
     7.1 --- a/src/HOLCF/Sprod0.ML	Thu Jan 08 18:08:43 1998 +0100
     7.2 +++ b/src/HOLCF/Sprod0.ML	Thu Jan 08 18:09:07 1998 +0100
     7.3 @@ -207,7 +207,7 @@
     7.4  (fn prems =>
     7.5          [
     7.6          (cut_facts_tac prems 1),
     7.7 -        (rtac  select_equality 1),
     7.8 +        (rtac select_equality 1),
     7.9          (rtac conjI 1),
    7.10          (fast_tac HOL_cs  1),
    7.11          (strip_tac 1),
    7.12 @@ -242,7 +242,7 @@
    7.13  (fn prems =>
    7.14          [
    7.15          (cut_facts_tac prems 1),
    7.16 -        (rtac  select_equality 1),
    7.17 +        (rtac select_equality 1),
    7.18          (rtac conjI 1),
    7.19          (fast_tac HOL_cs  1),
    7.20          (strip_tac 1),
    7.21 @@ -275,7 +275,7 @@
    7.22  (fn prems =>
    7.23          [
    7.24          (cut_facts_tac prems 1),
    7.25 -        (rtac  select_equality 1),
    7.26 +        (rtac select_equality 1),
    7.27          (rtac conjI 1),
    7.28          (strip_tac 1),
    7.29          (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
    7.30 @@ -295,7 +295,7 @@
    7.31  (fn prems =>
    7.32          [
    7.33          (cut_facts_tac prems 1),
    7.34 -        (rtac  select_equality 1),
    7.35 +        (rtac select_equality 1),
    7.36          (rtac conjI 1),
    7.37          (strip_tac 1),
    7.38          (res_inst_tac [("P","Ispair x y = Ispair UU UU")] notE 1),
     8.1 --- a/src/HOLCF/Ssum0.ML	Thu Jan 08 18:08:43 1998 +0100
     8.2 +++ b/src/HOLCF/Ssum0.ML	Thu Jan 08 18:09:07 1998 +0100
     8.3 @@ -310,7 +310,7 @@
     8.4          "Iwhen f g (Isinl UU) = UU"
     8.5   (fn prems =>
     8.6          [
     8.7 -        (rtac  select_equality 1),
     8.8 +        (rtac select_equality 1),
     8.9          (rtac conjI 1),
    8.10          (fast_tac HOL_cs  1),
    8.11          (rtac conjI 1),
    8.12 @@ -336,7 +336,7 @@
    8.13   (fn prems =>
    8.14          [
    8.15          (cut_facts_tac prems 1),
    8.16 -        (rtac  select_equality 1),
    8.17 +        (rtac select_equality 1),
    8.18          (fast_tac HOL_cs  2),
    8.19          (rtac conjI 1),
    8.20          (strip_tac 1),
    8.21 @@ -362,7 +362,7 @@
    8.22   (fn prems =>
    8.23          [
    8.24          (cut_facts_tac prems 1),
    8.25 -        (rtac  select_equality 1),
    8.26 +        (rtac select_equality 1),
    8.27          (fast_tac HOL_cs  2),
    8.28          (rtac conjI 1),
    8.29          (strip_tac 1),
     9.1 --- a/src/HOLCF/Ssum1.ML	Thu Jan 08 18:08:43 1998 +0100
     9.2 +++ b/src/HOLCF/Ssum1.ML	Thu Jan 08 18:09:07 1998 +0100
     9.3 @@ -45,7 +45,7 @@
     9.4   (fn prems =>
     9.5          [
     9.6          (cut_facts_tac prems 1),
     9.7 -        (rtac  select_equality 1),
     9.8 +        (rtac select_equality 1),
     9.9          (dtac conjunct1 2),
    9.10          (dtac spec 2),
    9.11          (dtac spec 2),
    9.12 @@ -86,7 +86,7 @@
    9.13   (fn prems =>
    9.14          [
    9.15          (cut_facts_tac prems 1),
    9.16 -        (rtac  select_equality 1),
    9.17 +        (rtac select_equality 1),
    9.18          (dtac conjunct2 2),
    9.19          (dtac conjunct1 2),
    9.20          (dtac spec 2),
    9.21 @@ -128,7 +128,7 @@
    9.22   (fn prems =>
    9.23          [
    9.24          (cut_facts_tac prems 1),
    9.25 -        (rtac  select_equality 1),
    9.26 +        (rtac select_equality 1),
    9.27          (rtac conjI 1),
    9.28          (strip_tac 1),
    9.29          (etac conjE 1),
    9.30 @@ -170,7 +170,7 @@
    9.31   (fn prems =>
    9.32          [
    9.33          (cut_facts_tac prems 1),
    9.34 -        (rtac  select_equality 1),
    9.35 +        (rtac select_equality 1),
    9.36          (dtac conjunct2 2),
    9.37          (dtac conjunct2 2),
    9.38          (dtac conjunct2 2),