tuned ML setup;
authorwenzelm
Sat Jan 20 14:09:27 2007 +0100 (2007-01-20)
changeset 22139539a63b98f76
parent 22138 b9cbcd8be40f
child 22140 0d49078c28bd
tuned ML setup;
src/FOL/FOL.thy
src/FOL/IFOL.thy
src/HOL/Lattices.thy
src/HOL/Set.thy
     1.1 --- a/src/FOL/FOL.thy	Sat Jan 20 14:09:23 2007 +0100
     1.2 +++ b/src/FOL/FOL.thy	Sat Jan 20 14:09:27 2007 +0100
     1.3 @@ -55,13 +55,8 @@
     1.4  
     1.5  (*For disjunctive case analysis*)
     1.6  ML {*
     1.7 -  local
     1.8 -    val excluded_middle = thm "excluded_middle"
     1.9 -    val disjE = thm "disjE"
    1.10 -  in
    1.11 -    fun excluded_middle_tac sP =
    1.12 -      res_inst_tac [("Q",sP)] (excluded_middle RS disjE)
    1.13 -  end
    1.14 +  fun excluded_middle_tac sP =
    1.15 +    res_inst_tac [("Q",sP)] (@{thm excluded_middle} RS @{thm disjE})
    1.16  *}
    1.17  
    1.18  lemma case_split_thm:
    1.19 @@ -77,11 +72,7 @@
    1.20  
    1.21  (*HOL's more natural case analysis tactic*)
    1.22  ML {*
    1.23 -  local
    1.24 -    val case_split_thm = thm "case_split_thm"
    1.25 -  in
    1.26 -    fun case_tac a = res_inst_tac [("P",a)] case_split_thm
    1.27 -  end
    1.28 +  fun case_tac a = res_inst_tac [("P",a)] @{thm case_split_thm}
    1.29  *}
    1.30  
    1.31  
    1.32 @@ -278,10 +269,10 @@
    1.33  ML {*
    1.34    structure InductMethod = InductMethodFun
    1.35    (struct
    1.36 -    val cases_default = thm "case_split";
    1.37 -    val atomize = thms "induct_atomize";
    1.38 -    val rulify = thms "induct_rulify";
    1.39 -    val rulify_fallback = thms "induct_rulify_fallback";
    1.40 +    val cases_default = @{thm case_split}
    1.41 +    val atomize = @{thms induct_atomize}
    1.42 +    val rulify = @{thms induct_rulify}
    1.43 +    val rulify_fallback = @{thms induct_rulify_fallback}
    1.44    end);
    1.45  *}
    1.46  
     2.1 --- a/src/FOL/IFOL.thy	Sat Jan 20 14:09:23 2007 +0100
     2.2 +++ b/src/FOL/IFOL.thy	Sat Jan 20 14:09:27 2007 +0100
     2.3 @@ -231,13 +231,8 @@
     2.4  
     2.5  (*Finds P-->Q and P in the assumptions, replaces implication by Q *)
     2.6  ML {*
     2.7 -  local
     2.8 -    val notE = thm "notE"
     2.9 -    val impE = thm "impE"
    2.10 -  in
    2.11 -    fun mp_tac i = eresolve_tac [notE,impE] i  THEN  assume_tac i
    2.12 -    fun eq_mp_tac i = eresolve_tac [notE,impE] i  THEN  eq_assume_tac i
    2.13 -  end
    2.14 +  fun mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  assume_tac i
    2.15 +  fun eq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i  THEN  eq_assume_tac i
    2.16  *}
    2.17  
    2.18  
    2.19 @@ -337,14 +332,9 @@
    2.20  
    2.21  (*Use iffE on a premise.  For conj_cong, imp_cong, all_cong, ex_cong*)
    2.22  ML {*
    2.23 -  local
    2.24 -    val iffE = thm "iffE"
    2.25 -    val mp = thm "mp"
    2.26 -  in
    2.27 -    fun iff_tac prems i =
    2.28 -      resolve_tac (prems RL [iffE]) i THEN
    2.29 -      REPEAT1 (eresolve_tac [asm_rl, mp] i)
    2.30 -  end
    2.31 +  fun iff_tac prems i =
    2.32 +    resolve_tac (prems RL @{thms iffE}) i THEN
    2.33 +    REPEAT1 (eresolve_tac [@{thm asm_rl}, @{thm mp}] i)
    2.34  *}
    2.35  
    2.36  lemma conj_cong:
    2.37 @@ -525,7 +515,7 @@
    2.38  bind_thms ("pred_congs",
    2.39    List.concat (map (fn c => 
    2.40                 map (fn th => read_instantiate [("P",c)] th)
    2.41 -                   [thm "pred1_cong", thm "pred2_cong", thm "pred3_cong"])
    2.42 +                   [@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}])
    2.43                 (explode"PQRS")))
    2.44  *}
    2.45  
    2.46 @@ -614,9 +604,9 @@
    2.47  ML {*
    2.48  structure ProjectRule = ProjectRuleFun
    2.49  (struct
    2.50 -  val conjunct1 = thm "conjunct1";
    2.51 -  val conjunct2 = thm "conjunct2";
    2.52 -  val mp = thm "mp";
    2.53 +  val conjunct1 = @{thm conjunct1}
    2.54 +  val conjunct2 = @{thm conjunct2}
    2.55 +  val mp = @{thm mp}
    2.56  end)
    2.57  *}
    2.58  
    2.59 @@ -791,41 +781,41 @@
    2.60  subsection {* ML bindings *}
    2.61  
    2.62  ML {*
    2.63 -val refl = thm "refl"
    2.64 -val trans = thm "trans"
    2.65 -val sym = thm "sym"
    2.66 -val subst = thm "subst"
    2.67 -val ssubst = thm "ssubst"
    2.68 -val conjI = thm "conjI"
    2.69 -val conjE = thm "conjE"
    2.70 -val conjunct1 = thm "conjunct1"
    2.71 -val conjunct2 = thm "conjunct2"
    2.72 -val disjI1 = thm "disjI1"
    2.73 -val disjI2 = thm "disjI2"
    2.74 -val disjE = thm "disjE"
    2.75 -val impI = thm "impI"
    2.76 -val impE = thm "impE"
    2.77 -val mp = thm "mp"
    2.78 -val rev_mp = thm "rev_mp"
    2.79 -val TrueI = thm "TrueI"
    2.80 -val FalseE = thm "FalseE"
    2.81 -val iff_refl = thm "iff_refl"
    2.82 -val iff_trans = thm "iff_trans"
    2.83 -val iffI = thm "iffI"
    2.84 -val iffE = thm "iffE"
    2.85 -val iffD1 = thm "iffD1"
    2.86 -val iffD2 = thm "iffD2"
    2.87 -val notI = thm "notI"
    2.88 -val notE = thm "notE"
    2.89 -val allI = thm "allI"
    2.90 -val allE = thm "allE"
    2.91 -val spec = thm "spec"
    2.92 -val exI = thm "exI"
    2.93 -val exE = thm "exE"
    2.94 -val eq_reflection = thm "eq_reflection"
    2.95 -val iff_reflection = thm "iff_reflection"
    2.96 -val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq"
    2.97 -val meta_eq_to_iff = thm "meta_eq_to_iff"
    2.98 +val refl = @{thm refl}
    2.99 +val trans = @{thm trans}
   2.100 +val sym = @{thm sym}
   2.101 +val subst = @{thm subst}
   2.102 +val ssubst = @{thm ssubst}
   2.103 +val conjI = @{thm conjI}
   2.104 +val conjE = @{thm conjE}
   2.105 +val conjunct1 = @{thm conjunct1}
   2.106 +val conjunct2 = @{thm conjunct2}
   2.107 +val disjI1 = @{thm disjI1}
   2.108 +val disjI2 = @{thm disjI2}
   2.109 +val disjE = @{thm disjE}
   2.110 +val impI = @{thm impI}
   2.111 +val impE = @{thm impE}
   2.112 +val mp = @{thm mp}
   2.113 +val rev_mp = @{thm rev_mp}
   2.114 +val TrueI = @{thm TrueI}
   2.115 +val FalseE = @{thm FalseE}
   2.116 +val iff_refl = @{thm iff_refl}
   2.117 +val iff_trans = @{thm iff_trans}
   2.118 +val iffI = @{thm iffI}
   2.119 +val iffE = @{thm iffE}
   2.120 +val iffD1 = @{thm iffD1}
   2.121 +val iffD2 = @{thm iffD2}
   2.122 +val notI = @{thm notI}
   2.123 +val notE = @{thm notE}
   2.124 +val allI = @{thm allI}
   2.125 +val allE = @{thm allE}
   2.126 +val spec = @{thm spec}
   2.127 +val exI = @{thm exI}
   2.128 +val exE = @{thm exE}
   2.129 +val eq_reflection = @{thm eq_reflection}
   2.130 +val iff_reflection = @{thm iff_reflection}
   2.131 +val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq}
   2.132 +val meta_eq_to_iff = @{thm meta_eq_to_iff}
   2.133  *}
   2.134  
   2.135  end
     3.1 --- a/src/HOL/Lattices.thy	Sat Jan 20 14:09:23 2007 +0100
     3.2 +++ b/src/HOL/Lattices.thy	Sat Jan 20 14:09:27 2007 +0100
     3.3 @@ -280,26 +280,26 @@
     3.4  text {* ML legacy bindings *}
     3.5  
     3.6  ML {*
     3.7 -val Least_def = thm "Least_def";
     3.8 -val Least_equality = thm "Least_equality";
     3.9 -val min_def = thm "min_def";
    3.10 -val min_of_mono = thm "min_of_mono";
    3.11 -val max_def = thm "max_def";
    3.12 -val max_of_mono = thm "max_of_mono";
    3.13 -val min_leastL = thm "min_leastL";
    3.14 -val max_leastL = thm "max_leastL";
    3.15 -val min_leastR = thm "min_leastR";
    3.16 -val max_leastR = thm "max_leastR";
    3.17 -val le_max_iff_disj = thm "le_max_iff_disj";
    3.18 -val le_maxI1 = thm "le_maxI1";
    3.19 -val le_maxI2 = thm "le_maxI2";
    3.20 -val less_max_iff_disj = thm "less_max_iff_disj";
    3.21 -val max_less_iff_conj = thm "max_less_iff_conj";
    3.22 -val min_less_iff_conj = thm "min_less_iff_conj";
    3.23 -val min_le_iff_disj = thm "min_le_iff_disj";
    3.24 -val min_less_iff_disj = thm "min_less_iff_disj";
    3.25 -val split_min = thm "split_min";
    3.26 -val split_max = thm "split_max";
    3.27 +val Least_def = @{thm Least_def}
    3.28 +val Least_equality = @{thm Least_equality}
    3.29 +val min_def = @{thm min_def}
    3.30 +val min_of_mono = @{thm min_of_mono}
    3.31 +val max_def = @{thm max_def}
    3.32 +val max_of_mono = @{thm max_of_mono}
    3.33 +val min_leastL = @{thm min_leastL}
    3.34 +val max_leastL = @{thm max_leastL}
    3.35 +val min_leastR = @{thm min_leastR}
    3.36 +val max_leastR = @{thm max_leastR}
    3.37 +val le_max_iff_disj = @{thm le_max_iff_disj}
    3.38 +val le_maxI1 = @{thm le_maxI1}
    3.39 +val le_maxI2 = @{thm le_maxI2}
    3.40 +val less_max_iff_disj = @{thm less_max_iff_disj}
    3.41 +val max_less_iff_conj = @{thm max_less_iff_conj}
    3.42 +val min_less_iff_conj = @{thm min_less_iff_conj}
    3.43 +val min_le_iff_disj = @{thm min_le_iff_disj}
    3.44 +val min_less_iff_disj = @{thm min_less_iff_disj}
    3.45 +val split_min = @{thm split_min}
    3.46 +val split_max = @{thm split_max}
    3.47  *}
    3.48  
    3.49  end
     4.1 --- a/src/HOL/Set.thy	Sat Jan 20 14:09:23 2007 +0100
     4.2 +++ b/src/HOL/Set.thy	Sat Jan 20 14:09:27 2007 +0100
     4.3 @@ -391,7 +391,8 @@
     4.4  
     4.5  lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q"
     4.6    by (unfold Ball_def) blast
     4.7 -ML {* bind_thm("rev_ballE",permute_prems 1 1 (thm "ballE")) *}
     4.8 +
     4.9 +ML {* bind_thm ("rev_ballE", permute_prems 1 1 @{thm ballE}) *}
    4.10  
    4.11  text {*
    4.12    \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and
    4.13 @@ -399,8 +400,7 @@
    4.14  *}
    4.15  
    4.16  ML {*
    4.17 -  local val ballE = thm "ballE"
    4.18 -  in fun ball_tac i = etac ballE i THEN contr_tac (i + 1) end;
    4.19 +  fun ball_tac i = etac @{thm ballE} i THEN contr_tac (i + 1)
    4.20  *}
    4.21  
    4.22  text {*
    4.23 @@ -408,7 +408,7 @@
    4.24  *}
    4.25  
    4.26  ML_setup {*
    4.27 -  change_claset (fn cs => cs addbefore ("bspec", datac (thm "bspec") 1));
    4.28 +  change_claset (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1))
    4.29  *}
    4.30  
    4.31  lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x"
    4.32 @@ -454,11 +454,11 @@
    4.33  
    4.34  ML_setup {*
    4.35    local
    4.36 -    val unfold_bex_tac = unfold_tac [thm "Bex_def"];
    4.37 +    val unfold_bex_tac = unfold_tac @{thms "Bex_def"};
    4.38      fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac;
    4.39      val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac;
    4.40  
    4.41 -    val unfold_ball_tac = unfold_tac [thm "Ball_def"];
    4.42 +    val unfold_ball_tac = unfold_tac @{thms "Ball_def"};
    4.43      fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac;
    4.44      val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac;
    4.45    in
    4.46 @@ -524,8 +524,7 @@
    4.47  *}
    4.48  
    4.49  ML {*
    4.50 -  local val rev_subsetD = thm "rev_subsetD"
    4.51 -  in fun impOfSubs th = th RSN (2, rev_subsetD) end;
    4.52 +  fun impOfSubs th = th RSN (2, @{thm rev_subsetD})
    4.53  *}
    4.54  
    4.55  lemma subsetCE [elim]: "A \<subseteq>  B ==> (c \<notin> A ==> P) ==> (c \<in> B ==> P) ==> P"
    4.56 @@ -538,8 +537,7 @@
    4.57  *}
    4.58  
    4.59  ML {*
    4.60 -  local val subsetCE = thm "subsetCE"
    4.61 -  in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end;
    4.62 +  fun set_mp_tac i = etac @{thm subsetCE} i THEN mp_tac i
    4.63  *}
    4.64  
    4.65  lemma contra_subsetD: "A \<subseteq> B ==> c \<notin> B ==> c \<notin> A"
    4.66 @@ -990,7 +988,7 @@
    4.67   *)
    4.68  
    4.69  ML_setup {*
    4.70 -  val mksimps_pairs = [("Ball", [thm "bspec"])] @ mksimps_pairs;
    4.71 +  val mksimps_pairs = [("Ball", @{thms bspec})] @ mksimps_pairs;
    4.72    change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs));
    4.73  *}
    4.74  
    4.75 @@ -2121,61 +2119,61 @@
    4.76  subsection {* Basic ML bindings *}
    4.77  
    4.78  ML {*
    4.79 -val Ball_def = thm "Ball_def";
    4.80 -val Bex_def = thm "Bex_def";
    4.81 -val CollectD = thm "CollectD";
    4.82 -val CollectE = thm "CollectE";
    4.83 -val CollectI = thm "CollectI";
    4.84 -val Collect_conj_eq = thm "Collect_conj_eq";
    4.85 -val Collect_mem_eq = thm "Collect_mem_eq";
    4.86 -val IntD1 = thm "IntD1";
    4.87 -val IntD2 = thm "IntD2";
    4.88 -val IntE = thm "IntE";
    4.89 -val IntI = thm "IntI";
    4.90 -val Int_Collect = thm "Int_Collect";
    4.91 -val UNIV_I = thm "UNIV_I";
    4.92 -val UNIV_witness = thm "UNIV_witness";
    4.93 -val UnE = thm "UnE";
    4.94 -val UnI1 = thm "UnI1";
    4.95 -val UnI2 = thm "UnI2";
    4.96 -val ballE = thm "ballE";
    4.97 -val ballI = thm "ballI";
    4.98 -val bexCI = thm "bexCI";
    4.99 -val bexE = thm "bexE";
   4.100 -val bexI = thm "bexI";
   4.101 -val bex_triv = thm "bex_triv";
   4.102 -val bspec = thm "bspec";
   4.103 -val contra_subsetD = thm "contra_subsetD";
   4.104 -val distinct_lemma = thm "distinct_lemma";
   4.105 -val eq_to_mono = thm "eq_to_mono";
   4.106 -val eq_to_mono2 = thm "eq_to_mono2";
   4.107 -val equalityCE = thm "equalityCE";
   4.108 -val equalityD1 = thm "equalityD1";
   4.109 -val equalityD2 = thm "equalityD2";
   4.110 -val equalityE = thm "equalityE";
   4.111 -val equalityI = thm "equalityI";
   4.112 -val imageE = thm "imageE";
   4.113 -val imageI = thm "imageI";
   4.114 -val image_Un = thm "image_Un";
   4.115 -val image_insert = thm "image_insert";
   4.116 -val insert_commute = thm "insert_commute";
   4.117 -val insert_iff = thm "insert_iff";
   4.118 -val mem_Collect_eq = thm "mem_Collect_eq";
   4.119 -val rangeE = thm "rangeE";
   4.120 -val rangeI = thm "rangeI";
   4.121 -val range_eqI = thm "range_eqI";
   4.122 -val subsetCE = thm "subsetCE";
   4.123 -val subsetD = thm "subsetD";
   4.124 -val subsetI = thm "subsetI";
   4.125 -val subset_refl = thm "subset_refl";
   4.126 -val subset_trans = thm "subset_trans";
   4.127 -val vimageD = thm "vimageD";
   4.128 -val vimageE = thm "vimageE";
   4.129 -val vimageI = thm "vimageI";
   4.130 -val vimageI2 = thm "vimageI2";
   4.131 -val vimage_Collect = thm "vimage_Collect";
   4.132 -val vimage_Int = thm "vimage_Int";
   4.133 -val vimage_Un = thm "vimage_Un";
   4.134 +val Ball_def = @{thm Ball_def}
   4.135 +val Bex_def = @{thm Bex_def}
   4.136 +val CollectD = @{thm CollectD}
   4.137 +val CollectE = @{thm CollectE}
   4.138 +val CollectI = @{thm CollectI}
   4.139 +val Collect_conj_eq = @{thm Collect_conj_eq}
   4.140 +val Collect_mem_eq = @{thm Collect_mem_eq}
   4.141 +val IntD1 = @{thm IntD1}
   4.142 +val IntD2 = @{thm IntD2}
   4.143 +val IntE = @{thm IntE}
   4.144 +val IntI = @{thm IntI}
   4.145 +val Int_Collect = @{thm Int_Collect}
   4.146 +val UNIV_I = @{thm UNIV_I}
   4.147 +val UNIV_witness = @{thm UNIV_witness}
   4.148 +val UnE = @{thm UnE}
   4.149 +val UnI1 = @{thm UnI1}
   4.150 +val UnI2 = @{thm UnI2}
   4.151 +val ballE = @{thm ballE}
   4.152 +val ballI = @{thm ballI}
   4.153 +val bexCI = @{thm bexCI}
   4.154 +val bexE = @{thm bexE}
   4.155 +val bexI = @{thm bexI}
   4.156 +val bex_triv = @{thm bex_triv}
   4.157 +val bspec = @{thm bspec}
   4.158 +val contra_subsetD = @{thm contra_subsetD}
   4.159 +val distinct_lemma = @{thm distinct_lemma}
   4.160 +val eq_to_mono = @{thm eq_to_mono}
   4.161 +val eq_to_mono2 = @{thm eq_to_mono2}
   4.162 +val equalityCE = @{thm equalityCE}
   4.163 +val equalityD1 = @{thm equalityD1}
   4.164 +val equalityD2 = @{thm equalityD2}
   4.165 +val equalityE = @{thm equalityE}
   4.166 +val equalityI = @{thm equalityI}
   4.167 +val imageE = @{thm imageE}
   4.168 +val imageI = @{thm imageI}
   4.169 +val image_Un = @{thm image_Un}
   4.170 +val image_insert = @{thm image_insert}
   4.171 +val insert_commute = @{thm insert_commute}
   4.172 +val insert_iff = @{thm insert_iff}
   4.173 +val mem_Collect_eq = @{thm mem_Collect_eq}
   4.174 +val rangeE = @{thm rangeE}
   4.175 +val rangeI = @{thm rangeI}
   4.176 +val range_eqI = @{thm range_eqI}
   4.177 +val subsetCE = @{thm subsetCE}
   4.178 +val subsetD = @{thm subsetD}
   4.179 +val subsetI = @{thm subsetI}
   4.180 +val subset_refl = @{thm subset_refl}
   4.181 +val subset_trans = @{thm subset_trans}
   4.182 +val vimageD = @{thm vimageD}
   4.183 +val vimageE = @{thm vimageE}
   4.184 +val vimageI = @{thm vimageI}
   4.185 +val vimageI2 = @{thm vimageI2}
   4.186 +val vimage_Collect = @{thm vimage_Collect}
   4.187 +val vimage_Int = @{thm vimage_Int}
   4.188 +val vimage_Un = @{thm vimage_Un}
   4.189  *}
   4.190  
   4.191  end