# HG changeset patch # User wenzelm # Date 1169298567 -3600 # Node ID 539a63b98f76972ac4549118f76445db730a3e52 # Parent b9cbcd8be40ff1729c85755e9442b158a0cdd2e4 tuned ML setup; diff -r b9cbcd8be40f -r 539a63b98f76 src/FOL/FOL.thy --- a/src/FOL/FOL.thy Sat Jan 20 14:09:23 2007 +0100 +++ b/src/FOL/FOL.thy Sat Jan 20 14:09:27 2007 +0100 @@ -55,13 +55,8 @@ (*For disjunctive case analysis*) ML {* - local - val excluded_middle = thm "excluded_middle" - val disjE = thm "disjE" - in - fun excluded_middle_tac sP = - res_inst_tac [("Q",sP)] (excluded_middle RS disjE) - end + fun excluded_middle_tac sP = + res_inst_tac [("Q",sP)] (@{thm excluded_middle} RS @{thm disjE}) *} lemma case_split_thm: @@ -77,11 +72,7 @@ (*HOL's more natural case analysis tactic*) ML {* - local - val case_split_thm = thm "case_split_thm" - in - fun case_tac a = res_inst_tac [("P",a)] case_split_thm - end + fun case_tac a = res_inst_tac [("P",a)] @{thm case_split_thm} *} @@ -278,10 +269,10 @@ ML {* structure InductMethod = InductMethodFun (struct - val cases_default = thm "case_split"; - val atomize = thms "induct_atomize"; - val rulify = thms "induct_rulify"; - val rulify_fallback = thms "induct_rulify_fallback"; + val cases_default = @{thm case_split} + val atomize = @{thms induct_atomize} + val rulify = @{thms induct_rulify} + val rulify_fallback = @{thms induct_rulify_fallback} end); *} diff -r b9cbcd8be40f -r 539a63b98f76 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Sat Jan 20 14:09:23 2007 +0100 +++ b/src/FOL/IFOL.thy Sat Jan 20 14:09:27 2007 +0100 @@ -231,13 +231,8 @@ (*Finds P-->Q and P in the assumptions, replaces implication by Q *) ML {* - local - val notE = thm "notE" - val impE = thm "impE" - in - fun mp_tac i = eresolve_tac [notE,impE] i THEN assume_tac i - fun eq_mp_tac i = eresolve_tac [notE,impE] i THEN eq_assume_tac i - end + fun mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN assume_tac i + fun eq_mp_tac i = eresolve_tac [@{thm notE}, @{thm impE}] i THEN eq_assume_tac i *} @@ -337,14 +332,9 @@ (*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) ML {* - local - val iffE = thm "iffE" - val mp = thm "mp" - in - fun iff_tac prems i = - resolve_tac (prems RL [iffE]) i THEN - REPEAT1 (eresolve_tac [asm_rl, mp] i) - end + fun iff_tac prems i = + resolve_tac (prems RL @{thms iffE}) i THEN + REPEAT1 (eresolve_tac [@{thm asm_rl}, @{thm mp}] i) *} lemma conj_cong: @@ -525,7 +515,7 @@ bind_thms ("pred_congs", List.concat (map (fn c => map (fn th => read_instantiate [("P",c)] th) - [thm "pred1_cong", thm "pred2_cong", thm "pred3_cong"]) + [@{thm pred1_cong}, @{thm pred2_cong}, @{thm pred3_cong}]) (explode"PQRS"))) *} @@ -614,9 +604,9 @@ ML {* structure ProjectRule = ProjectRuleFun (struct - val conjunct1 = thm "conjunct1"; - val conjunct2 = thm "conjunct2"; - val mp = thm "mp"; + val conjunct1 = @{thm conjunct1} + val conjunct2 = @{thm conjunct2} + val mp = @{thm mp} end) *} @@ -791,41 +781,41 @@ subsection {* ML bindings *} ML {* -val refl = thm "refl" -val trans = thm "trans" -val sym = thm "sym" -val subst = thm "subst" -val ssubst = thm "ssubst" -val conjI = thm "conjI" -val conjE = thm "conjE" -val conjunct1 = thm "conjunct1" -val conjunct2 = thm "conjunct2" -val disjI1 = thm "disjI1" -val disjI2 = thm "disjI2" -val disjE = thm "disjE" -val impI = thm "impI" -val impE = thm "impE" -val mp = thm "mp" -val rev_mp = thm "rev_mp" -val TrueI = thm "TrueI" -val FalseE = thm "FalseE" -val iff_refl = thm "iff_refl" -val iff_trans = thm "iff_trans" -val iffI = thm "iffI" -val iffE = thm "iffE" -val iffD1 = thm "iffD1" -val iffD2 = thm "iffD2" -val notI = thm "notI" -val notE = thm "notE" -val allI = thm "allI" -val allE = thm "allE" -val spec = thm "spec" -val exI = thm "exI" -val exE = thm "exE" -val eq_reflection = thm "eq_reflection" -val iff_reflection = thm "iff_reflection" -val meta_eq_to_obj_eq = thm "meta_eq_to_obj_eq" -val meta_eq_to_iff = thm "meta_eq_to_iff" +val refl = @{thm refl} +val trans = @{thm trans} +val sym = @{thm sym} +val subst = @{thm subst} +val ssubst = @{thm ssubst} +val conjI = @{thm conjI} +val conjE = @{thm conjE} +val conjunct1 = @{thm conjunct1} +val conjunct2 = @{thm conjunct2} +val disjI1 = @{thm disjI1} +val disjI2 = @{thm disjI2} +val disjE = @{thm disjE} +val impI = @{thm impI} +val impE = @{thm impE} +val mp = @{thm mp} +val rev_mp = @{thm rev_mp} +val TrueI = @{thm TrueI} +val FalseE = @{thm FalseE} +val iff_refl = @{thm iff_refl} +val iff_trans = @{thm iff_trans} +val iffI = @{thm iffI} +val iffE = @{thm iffE} +val iffD1 = @{thm iffD1} +val iffD2 = @{thm iffD2} +val notI = @{thm notI} +val notE = @{thm notE} +val allI = @{thm allI} +val allE = @{thm allE} +val spec = @{thm spec} +val exI = @{thm exI} +val exE = @{thm exE} +val eq_reflection = @{thm eq_reflection} +val iff_reflection = @{thm iff_reflection} +val meta_eq_to_obj_eq = @{thm meta_eq_to_obj_eq} +val meta_eq_to_iff = @{thm meta_eq_to_iff} *} end diff -r b9cbcd8be40f -r 539a63b98f76 src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Sat Jan 20 14:09:23 2007 +0100 +++ b/src/HOL/Lattices.thy Sat Jan 20 14:09:27 2007 +0100 @@ -280,26 +280,26 @@ text {* ML legacy bindings *} ML {* -val Least_def = thm "Least_def"; -val Least_equality = thm "Least_equality"; -val min_def = thm "min_def"; -val min_of_mono = thm "min_of_mono"; -val max_def = thm "max_def"; -val max_of_mono = thm "max_of_mono"; -val min_leastL = thm "min_leastL"; -val max_leastL = thm "max_leastL"; -val min_leastR = thm "min_leastR"; -val max_leastR = thm "max_leastR"; -val le_max_iff_disj = thm "le_max_iff_disj"; -val le_maxI1 = thm "le_maxI1"; -val le_maxI2 = thm "le_maxI2"; -val less_max_iff_disj = thm "less_max_iff_disj"; -val max_less_iff_conj = thm "max_less_iff_conj"; -val min_less_iff_conj = thm "min_less_iff_conj"; -val min_le_iff_disj = thm "min_le_iff_disj"; -val min_less_iff_disj = thm "min_less_iff_disj"; -val split_min = thm "split_min"; -val split_max = thm "split_max"; +val Least_def = @{thm Least_def} +val Least_equality = @{thm Least_equality} +val min_def = @{thm min_def} +val min_of_mono = @{thm min_of_mono} +val max_def = @{thm max_def} +val max_of_mono = @{thm max_of_mono} +val min_leastL = @{thm min_leastL} +val max_leastL = @{thm max_leastL} +val min_leastR = @{thm min_leastR} +val max_leastR = @{thm max_leastR} +val le_max_iff_disj = @{thm le_max_iff_disj} +val le_maxI1 = @{thm le_maxI1} +val le_maxI2 = @{thm le_maxI2} +val less_max_iff_disj = @{thm less_max_iff_disj} +val max_less_iff_conj = @{thm max_less_iff_conj} +val min_less_iff_conj = @{thm min_less_iff_conj} +val min_le_iff_disj = @{thm min_le_iff_disj} +val min_less_iff_disj = @{thm min_less_iff_disj} +val split_min = @{thm split_min} +val split_max = @{thm split_max} *} end diff -r b9cbcd8be40f -r 539a63b98f76 src/HOL/Set.thy --- a/src/HOL/Set.thy Sat Jan 20 14:09:23 2007 +0100 +++ b/src/HOL/Set.thy Sat Jan 20 14:09:27 2007 +0100 @@ -391,7 +391,8 @@ lemma ballE [elim]: "ALL x:A. P x ==> (P x ==> Q) ==> (x ~: A ==> Q) ==> Q" by (unfold Ball_def) blast -ML {* bind_thm("rev_ballE",permute_prems 1 1 (thm "ballE")) *} + +ML {* bind_thm ("rev_ballE", permute_prems 1 1 @{thm ballE}) *} text {* \medskip This tactic takes assumptions @{prop "ALL x:A. P x"} and @@ -399,8 +400,7 @@ *} ML {* - local val ballE = thm "ballE" - in fun ball_tac i = etac ballE i THEN contr_tac (i + 1) end; + fun ball_tac i = etac @{thm ballE} i THEN contr_tac (i + 1) *} text {* @@ -408,7 +408,7 @@ *} ML_setup {* - change_claset (fn cs => cs addbefore ("bspec", datac (thm "bspec") 1)); + change_claset (fn cs => cs addbefore ("bspec", datac @{thm bspec} 1)) *} lemma bexI [intro]: "P x ==> x:A ==> EX x:A. P x" @@ -454,11 +454,11 @@ ML_setup {* local - val unfold_bex_tac = unfold_tac [thm "Bex_def"]; + val unfold_bex_tac = unfold_tac @{thms "Bex_def"}; fun prove_bex_tac ss = unfold_bex_tac ss THEN Quantifier1.prove_one_point_ex_tac; val rearrange_bex = Quantifier1.rearrange_bex prove_bex_tac; - val unfold_ball_tac = unfold_tac [thm "Ball_def"]; + val unfold_ball_tac = unfold_tac @{thms "Ball_def"}; fun prove_ball_tac ss = unfold_ball_tac ss THEN Quantifier1.prove_one_point_all_tac; val rearrange_ball = Quantifier1.rearrange_ball prove_ball_tac; in @@ -524,8 +524,7 @@ *} ML {* - local val rev_subsetD = thm "rev_subsetD" - in fun impOfSubs th = th RSN (2, rev_subsetD) end; + fun impOfSubs th = th RSN (2, @{thm rev_subsetD}) *} lemma subsetCE [elim]: "A \ B ==> (c \ A ==> P) ==> (c \ B ==> P) ==> P" @@ -538,8 +537,7 @@ *} ML {* - local val subsetCE = thm "subsetCE" - in fun set_mp_tac i = etac subsetCE i THEN mp_tac i end; + fun set_mp_tac i = etac @{thm subsetCE} i THEN mp_tac i *} lemma contra_subsetD: "A \ B ==> c \ B ==> c \ A" @@ -990,7 +988,7 @@ *) ML_setup {* - val mksimps_pairs = [("Ball", [thm "bspec"])] @ mksimps_pairs; + val mksimps_pairs = [("Ball", @{thms bspec})] @ mksimps_pairs; change_simpset (fn ss => ss setmksimps (mksimps mksimps_pairs)); *} @@ -2121,61 +2119,61 @@ subsection {* Basic ML bindings *} ML {* -val Ball_def = thm "Ball_def"; -val Bex_def = thm "Bex_def"; -val CollectD = thm "CollectD"; -val CollectE = thm "CollectE"; -val CollectI = thm "CollectI"; -val Collect_conj_eq = thm "Collect_conj_eq"; -val Collect_mem_eq = thm "Collect_mem_eq"; -val IntD1 = thm "IntD1"; -val IntD2 = thm "IntD2"; -val IntE = thm "IntE"; -val IntI = thm "IntI"; -val Int_Collect = thm "Int_Collect"; -val UNIV_I = thm "UNIV_I"; -val UNIV_witness = thm "UNIV_witness"; -val UnE = thm "UnE"; -val UnI1 = thm "UnI1"; -val UnI2 = thm "UnI2"; -val ballE = thm "ballE"; -val ballI = thm "ballI"; -val bexCI = thm "bexCI"; -val bexE = thm "bexE"; -val bexI = thm "bexI"; -val bex_triv = thm "bex_triv"; -val bspec = thm "bspec"; -val contra_subsetD = thm "contra_subsetD"; -val distinct_lemma = thm "distinct_lemma"; -val eq_to_mono = thm "eq_to_mono"; -val eq_to_mono2 = thm "eq_to_mono2"; -val equalityCE = thm "equalityCE"; -val equalityD1 = thm "equalityD1"; -val equalityD2 = thm "equalityD2"; -val equalityE = thm "equalityE"; -val equalityI = thm "equalityI"; -val imageE = thm "imageE"; -val imageI = thm "imageI"; -val image_Un = thm "image_Un"; -val image_insert = thm "image_insert"; -val insert_commute = thm "insert_commute"; -val insert_iff = thm "insert_iff"; -val mem_Collect_eq = thm "mem_Collect_eq"; -val rangeE = thm "rangeE"; -val rangeI = thm "rangeI"; -val range_eqI = thm "range_eqI"; -val subsetCE = thm "subsetCE"; -val subsetD = thm "subsetD"; -val subsetI = thm "subsetI"; -val subset_refl = thm "subset_refl"; -val subset_trans = thm "subset_trans"; -val vimageD = thm "vimageD"; -val vimageE = thm "vimageE"; -val vimageI = thm "vimageI"; -val vimageI2 = thm "vimageI2"; -val vimage_Collect = thm "vimage_Collect"; -val vimage_Int = thm "vimage_Int"; -val vimage_Un = thm "vimage_Un"; +val Ball_def = @{thm Ball_def} +val Bex_def = @{thm Bex_def} +val CollectD = @{thm CollectD} +val CollectE = @{thm CollectE} +val CollectI = @{thm CollectI} +val Collect_conj_eq = @{thm Collect_conj_eq} +val Collect_mem_eq = @{thm Collect_mem_eq} +val IntD1 = @{thm IntD1} +val IntD2 = @{thm IntD2} +val IntE = @{thm IntE} +val IntI = @{thm IntI} +val Int_Collect = @{thm Int_Collect} +val UNIV_I = @{thm UNIV_I} +val UNIV_witness = @{thm UNIV_witness} +val UnE = @{thm UnE} +val UnI1 = @{thm UnI1} +val UnI2 = @{thm UnI2} +val ballE = @{thm ballE} +val ballI = @{thm ballI} +val bexCI = @{thm bexCI} +val bexE = @{thm bexE} +val bexI = @{thm bexI} +val bex_triv = @{thm bex_triv} +val bspec = @{thm bspec} +val contra_subsetD = @{thm contra_subsetD} +val distinct_lemma = @{thm distinct_lemma} +val eq_to_mono = @{thm eq_to_mono} +val eq_to_mono2 = @{thm eq_to_mono2} +val equalityCE = @{thm equalityCE} +val equalityD1 = @{thm equalityD1} +val equalityD2 = @{thm equalityD2} +val equalityE = @{thm equalityE} +val equalityI = @{thm equalityI} +val imageE = @{thm imageE} +val imageI = @{thm imageI} +val image_Un = @{thm image_Un} +val image_insert = @{thm image_insert} +val insert_commute = @{thm insert_commute} +val insert_iff = @{thm insert_iff} +val mem_Collect_eq = @{thm mem_Collect_eq} +val rangeE = @{thm rangeE} +val rangeI = @{thm rangeI} +val range_eqI = @{thm range_eqI} +val subsetCE = @{thm subsetCE} +val subsetD = @{thm subsetD} +val subsetI = @{thm subsetI} +val subset_refl = @{thm subset_refl} +val subset_trans = @{thm subset_trans} +val vimageD = @{thm vimageD} +val vimageE = @{thm vimageE} +val vimageI = @{thm vimageI} +val vimageI2 = @{thm vimageI2} +val vimage_Collect = @{thm vimage_Collect} +val vimage_Int = @{thm vimage_Int} +val vimage_Un = @{thm vimage_Un} *} end