simplified ML code for setsubgoaler;
authorwenzelm
Fri Apr 16 13:52:43 2004 +0200 (2004-04-16)
changeset 14590276ef51cedbf
parent 14589 feae7b5fd425
child 14591 7be4d5dadf15
simplified ML code for setsubgoaler;
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/HOL.thy
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Fri Apr 16 13:51:04 2004 +0200
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Fri Apr 16 13:52:43 2004 +0200
     1.3 @@ -291,8 +291,7 @@
     1.4     like \<Otimes>\<index> i\<in>A. f i, probably needs hand-coded translation *)
     1.5  
     1.6  ML_setup {* 
     1.7 -  Context.>> (fn thy => (simpset_ref_of thy :=
     1.8 -    simpset_of thy setsubgoaler asm_full_simp_tac; thy))
     1.9 +  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    1.10  *}
    1.11  
    1.12  lemma (in comm_monoid) finprod_empty [simp]: 
    1.13 @@ -300,8 +299,7 @@
    1.14    by (simp add: finprod_def)
    1.15  
    1.16  ML_setup {* 
    1.17 -  Context.>> (fn thy => (simpset_ref_of thy :=
    1.18 -    simpset_of thy setsubgoaler asm_simp_tac; thy))
    1.19 +  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
    1.20  *}
    1.21  
    1.22  declare funcsetI [intro]
     2.1 --- a/src/HOL/Algebra/UnivPoly.thy	Fri Apr 16 13:51:04 2004 +0200
     2.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Apr 16 13:52:43 2004 +0200
     2.3 @@ -295,8 +295,8 @@
     2.4    by (rule up_eqI, simp add: a_comm R, simp_all add: R)
     2.5  
     2.6  ML_setup {*
     2.7 -Context.>> (fn thy => (simpset_ref_of thy :=
     2.8 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
     2.9 +  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    2.10 +*}
    2.11  
    2.12  lemma (in UP_cring) UP_m_assoc:
    2.13    assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
    2.14 @@ -328,8 +328,8 @@
    2.15  qed (simp_all add: R)
    2.16  
    2.17  ML_setup {*
    2.18 -Context.>> (fn thy => (simpset_ref_of thy :=
    2.19 -  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
    2.20 +  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
    2.21 +*}
    2.22  
    2.23  lemma (in UP_cring) UP_l_one [simp]:
    2.24    assumes R: "p \<in> carrier P"
    2.25 @@ -618,8 +618,8 @@
    2.26    by (simp add: UP_def P_def)
    2.27  
    2.28  ML_setup {*
    2.29 -Context.>> (fn thy => (simpset_ref_of thy :=
    2.30 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
    2.31 +  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    2.32 +*}
    2.33  
    2.34  lemma (in UP_cring) monom_mult_is_smult:
    2.35    assumes R: "a \<in> carrier R" "p \<in> carrier P"
    2.36 @@ -639,8 +639,8 @@
    2.37  qed (simp_all add: R)
    2.38  
    2.39  ML_setup {*
    2.40 -Context.>> (fn thy => (simpset_ref_of thy :=
    2.41 -  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
    2.42 +  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
    2.43 +*}
    2.44  
    2.45  lemma (in UP_cring) monom_add [simp]:
    2.46    "[| a \<in> carrier R; b \<in> carrier R |] ==>
    2.47 @@ -648,8 +648,8 @@
    2.48    by (rule up_eqI) simp_all
    2.49  
    2.50  ML_setup {*
    2.51 -Context.>> (fn thy => (simpset_ref_of thy :=
    2.52 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
    2.53 +  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    2.54 +*}
    2.55  
    2.56  lemma (in UP_cring) monom_one_Suc:
    2.57    "monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1"
    2.58 @@ -725,8 +725,8 @@
    2.59  qed (simp_all)
    2.60  
    2.61  ML_setup {*
    2.62 -Context.>> (fn thy => (simpset_ref_of thy :=
    2.63 -  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
    2.64 +  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
    2.65 +*}
    2.66  
    2.67  lemma (in UP_cring) monom_mult_smult:
    2.68    "[| a \<in> carrier R; b \<in> carrier R |] ==> monom P (a \<otimes> b) n = a \<odot>\<^sub>2 monom P b n"
    2.69 @@ -977,8 +977,8 @@
    2.70  qed (simp add: R)
    2.71  
    2.72  ML_setup {*
    2.73 -Context.>> (fn thy => (simpset_ref_of thy :=
    2.74 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
    2.75 +  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    2.76 +*}
    2.77  
    2.78  lemma (in UP_domain) deg_mult [simp]:
    2.79    "[| p ~= \<zero>\<^sub>2; q ~= \<zero>\<^sub>2; p \<in> carrier P; q \<in> carrier P |] ==>
    2.80 @@ -1017,8 +1017,8 @@
    2.81    using fin by induct (auto simp: Pi_def)
    2.82  
    2.83  ML_setup {*
    2.84 -Context.>> (fn thy => (simpset_ref_of thy :=
    2.85 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
    2.86 +  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    2.87 +*}
    2.88  
    2.89  lemma (in UP_cring) up_repr:
    2.90    assumes R: "p \<in> carrier P"
    2.91 @@ -1073,8 +1073,8 @@
    2.92  qed
    2.93  
    2.94  ML_setup {*
    2.95 -Context.>> (fn thy => (simpset_ref_of thy :=
    2.96 -  simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
    2.97 +  simpset_ref() := simpset() setsubgoaler asm_simp_tac;
    2.98 +*}
    2.99  
   2.100  subsection {* Polynomials over an integral domain form an integral domain *}
   2.101  
   2.102 @@ -1153,8 +1153,8 @@
   2.103  subsection {* Evaluation Homomorphism and Universal Property*}
   2.104  
   2.105  ML_setup {*
   2.106 -Context.>> (fn thy => (simpset_ref_of thy :=
   2.107 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
   2.108 +  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
   2.109 +*}
   2.110  
   2.111  (* alternative congruence rule (possibly more efficient)
   2.112  lemma (in abelian_monoid) finsum_cong2:
   2.113 @@ -1493,7 +1493,6 @@
   2.114      by (auto intro: ring_hom_cringI UP_cring S.cring Phi)
   2.115    have Psi_hom: "ring_hom_cring P S Psi"
   2.116      by (auto intro: ring_hom_cringI UP_cring S.cring Psi)
   2.117 -thm monom_mult
   2.118    have "Phi p = Phi (finsum P
   2.119      (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
   2.120      by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult)
   2.121 @@ -1568,4 +1567,4 @@
   2.122  -- {* Calculates @{term "x = 500"} *}
   2.123  
   2.124  
   2.125 -end
   2.126 \ No newline at end of file
   2.127 +end
     3.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Apr 16 13:51:04 2004 +0200
     3.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Apr 16 13:52:43 2004 +0200
     3.3 @@ -36,11 +36,11 @@
     3.4     This makes setsum_cong more convenient to use, because assumptions
     3.5     like i:{m..n} get simplified (to m <= i & i <= n). *)
     3.6  
     3.7 -ML_setup {* 
     3.8 +declare setsum_cong [cong]
     3.9  
    3.10 -Addcongs [thm "setsum_cong"];
    3.11 -Context.>> (fn thy => (simpset_ref_of thy :=
    3.12 -  simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
    3.13 +ML_setup {* 
    3.14 +  simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
    3.15 +*}
    3.16  
    3.17  section {* Definition of type up *}
    3.18  
    3.19 @@ -776,4 +776,4 @@
    3.20    "(a::'a::domain) *s p = 0 ==> a = 0 | p = 0"
    3.21  by (simp add: monom_mult_is_smult [THEN sym] integral_iff monom_inj_zero)
    3.22  
    3.23 -end
    3.24 \ No newline at end of file
    3.25 +end
     4.1 --- a/src/HOL/HOL.thy	Fri Apr 16 13:51:04 2004 +0200
     4.2 +++ b/src/HOL/HOL.thy	Fri Apr 16 13:52:43 2004 +0200
     4.3 @@ -1022,15 +1022,13 @@
     4.4  
     4.5    end);  (* struct *)
     4.6  
     4.7 -Context.>> (fn thy => (simpset_ref_of thy :=
     4.8 -  simpset_of thy
     4.9 +simpset_ref() := simpset ()
    4.10      addSolver (mk_solver "Trans_linear" (fn _ => Trans_Tac.linear_tac))
    4.11      addSolver (mk_solver "Trans_partial" (fn _ => Trans_Tac.partial_tac));
    4.12    (* Adding the transitivity reasoners also as safe solvers showed a slight
    4.13       speed up, but the reasoning strength appears to be not higher (at least
    4.14       no breaking of additional proofs in the entire HOL distribution, as
    4.15       of 5 March 2004, was observed). *)
    4.16 -  thy))
    4.17  *}
    4.18  
    4.19  (* Optional methods