# HG changeset patch # User wenzelm # Date 1178750385 -7200 # Node ID f8a7c10e1bd03952688a6bde9fcda46edc2daaaa # Parent 5ea718c681233d5f1e3ac932f9490dd40555a643 moved conversions to structure Conv; diff -r 5ea718c68123 -r f8a7c10e1bd0 src/HOL/Code_Generator.thy --- a/src/HOL/Code_Generator.thy Wed May 09 23:28:18 2007 +0200 +++ b/src/HOL/Code_Generator.thy Thu May 10 00:39:45 2007 +0200 @@ -73,8 +73,8 @@ method_setup evaluation = {* let -fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule - (Drule.goals_conv (equal i) Codegen.evaluation_conv)); +fun evaluation_tac i = Tactical.PRIMITIVE (Conv.fconv_rule + (Conv.goals_conv (equal i) Codegen.evaluation_conv)); in Method.no_args (Method.SIMPLE_METHOD' (evaluation_tac THEN' rtac TrueI)) end *} "solve goal by evaluation" @@ -201,8 +201,8 @@ method_setup normalization = {* let - fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule - (Drule.goals_conv (equal i) (HOLogic.Trueprop_conv + fun normalization_tac i = Tactical.PRIMITIVE (Conv.fconv_rule + (Conv.goals_conv (equal i) (HOLogic.Trueprop_conv NBE.normalization_conv))); in Method.no_args (Method.SIMPLE_METHOD' (normalization_tac THEN' resolve_tac [TrueI, refl])) diff -r 5ea718c68123 -r f8a7c10e1bd0 src/HOL/Library/EfficientNat.thy --- a/src/HOL/Library/EfficientNat.thy Wed May 09 23:28:18 2007 +0200 +++ b/src/HOL/Library/EfficientNat.thy Thu May 10 00:39:45 2007 +0200 @@ -290,7 +290,7 @@ let val th' = Thm.implies_elim - (Drule.fconv_rule (Thm.beta_conversion true) + (Conv.fconv_rule (Thm.beta_conversion true) (Drule.instantiate' [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct), SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv'] @@ -338,7 +338,7 @@ let val cert = cterm_of (Thm.theory_of_thm th); val th'' = ObjectLogic.rulify (Thm.implies_elim - (Drule.fconv_rule (Thm.beta_conversion true) + (Conv.fconv_rule (Thm.beta_conversion true) (Drule.instantiate' [] [SOME (cert (lambda v (Abs ("x", HOLogic.natT, abstract_over (Sucv, diff -r 5ea718c68123 -r f8a7c10e1bd0 src/HOL/Tools/sat_funcs.ML --- a/src/HOL/Tools/sat_funcs.ML Wed May 09 23:28:18 2007 +0200 +++ b/src/HOL/Tools/sat_funcs.ML Thu May 10 00:39:45 2007 +0200 @@ -434,7 +434,7 @@ fun pre_cnf_tac i = rtac ccontr i THEN ObjectLogic.atomize_tac i THEN - PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (Drule.beta_eta_conversion))); + PRIMITIVE (Conv.fconv_rule (Conv.goals_conv (equal i) (Drule.beta_eta_conversion))); (* ------------------------------------------------------------------------- *) (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *) diff -r 5ea718c68123 -r f8a7c10e1bd0 src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Wed May 09 23:28:18 2007 +0200 +++ b/src/HOL/arith_data.ML Thu May 10 00:39:45 2007 +0200 @@ -896,8 +896,8 @@ (TRY o REPEAT_ALL_NEW (split_once_tac split_thms)) THEN_ALL_NEW ((fn j => PRIMITIVE - (Drule.fconv_rule - (Drule.goals_conv (equal j) (Drule.beta_eta_conversion)))) + (Conv.fconv_rule + (Conv.goals_conv (equal j) (Drule.beta_eta_conversion)))) THEN' (TRY o (etac notE THEN' eq_assume_tac))) ) i diff -r 5ea718c68123 -r f8a7c10e1bd0 src/Provers/induct_method.ML --- a/src/Provers/induct_method.ML Wed May 09 23:28:18 2007 +0200 +++ b/src/Provers/induct_method.ML Thu May 10 00:39:45 2007 +0200 @@ -195,7 +195,7 @@ fun internalize k th = th |> Thm.permute_prems 0 k - |> Drule.fconv_rule (Drule.concl_conv (Thm.nprems_of th - k) atomize_cterm); + |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm); (* guess rule instantiation -- cannot handle pending goal parameters *) @@ -310,9 +310,9 @@ | NONE => all_tac) end); -fun miniscope_tac p i = PRIMITIVE (Drule.fconv_rule - (Drule.goals_conv (Library.equal i) - (Drule.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq])))); +fun miniscope_tac p i = PRIMITIVE (Conv.fconv_rule + (Conv.goals_conv (Library.equal i) + (Conv.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq])))); in diff -r 5ea718c68123 -r f8a7c10e1bd0 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Wed May 09 23:28:18 2007 +0200 +++ b/src/Pure/Isar/attrib.ML Thu May 10 00:39:45 2007 +0200 @@ -252,7 +252,8 @@ let val ((_, [th']), _) = Variable.import_thms true [th] (Context.proof_of ctxt) in th' end)) x; -fun eta_long x = no_args (Thm.rule_attribute (K (Drule.fconv_rule Drule.eta_long_conversion))) x; +fun eta_long x = + no_args (Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion))) x; (* internal attribute *) diff -r 5ea718c68123 -r f8a7c10e1bd0 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Wed May 09 23:28:18 2007 +0200 +++ b/src/Pure/Isar/element.ML Thu May 10 00:39:45 2007 +0200 @@ -456,7 +456,7 @@ else th |> hyps_rule (instantiate_tfrees thy substT #> instantiate_frees thy subst #> - Drule.fconv_rule (Thm.beta_conversion true)) + Conv.fconv_rule (Thm.beta_conversion true)) end; fun inst_morphism thy envs = diff -r 5ea718c68123 -r f8a7c10e1bd0 src/Pure/Isar/local_defs.ML --- a/src/Pure/Isar/local_defs.ML Wed May 09 23:28:18 2007 +0200 +++ b/src/Pure/Isar/local_defs.ML Thu May 10 00:39:45 2007 +0200 @@ -171,10 +171,10 @@ MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE)) (equals_ss addsimps (Rules.get (Context.Proof ctxt))); -val meta_rewrite_rule = Drule.fconv_rule o meta_rewrite; +val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite; fun meta_rewrite_tac ctxt i = - PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (meta_rewrite ctxt))); + PRIMITIVE (Conv.fconv_rule (Conv.goals_conv (equal i) (meta_rewrite ctxt))); (* rewriting with object-level rules *) diff -r 5ea718c68123 -r f8a7c10e1bd0 src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Wed May 09 23:28:18 2007 +0200 +++ b/src/Pure/Isar/object_logic.ML Thu May 10 00:39:45 2007 +0200 @@ -141,10 +141,10 @@ (* atomize *) -fun rewrite_prems_tac rews i = PRIMITIVE (Drule.fconv_rule - (Drule.goals_conv (Library.equal i) - (Drule.forall_conv ~1 - (Drule.goals_conv (K true) (MetaSimplifier.rewrite true rews))))); +fun rewrite_prems_tac rews i = PRIMITIVE (Conv.fconv_rule + (Conv.goals_conv (Library.equal i) + (Conv.forall_conv ~1 + (Conv.goals_conv (K true) (MetaSimplifier.rewrite true rews))))); fun atomize_term thy = drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) []; diff -r 5ea718c68123 -r f8a7c10e1bd0 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Wed May 09 23:28:18 2007 +0200 +++ b/src/Pure/Isar/rule_cases.ML Thu May 10 00:39:45 2007 +0200 @@ -189,14 +189,14 @@ fun unfold_prems n defs th = if null defs then th - else Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (MetaSimplifier.rewrite true defs)) th; + else Conv.fconv_rule (Conv.goals_conv (fn i => i <= n) (MetaSimplifier.rewrite true defs)) th; fun unfold_prems_concls defs th = if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th else - Drule.fconv_rule - (Drule.concl_conv ~1 (Conjunction.conv ~1 - (K (Drule.prems_conv ~1 (K (MetaSimplifier.rewrite true defs)))))) th; + Conv.fconv_rule + (Conv.concl_conv ~1 (Conjunction.conv ~1 + (K (Conv.prems_conv ~1 (K (MetaSimplifier.rewrite true defs)))))) th; in diff -r 5ea718c68123 -r f8a7c10e1bd0 src/Pure/Tools/codegen_func.ML --- a/src/Pure/Tools/codegen_func.ML Wed May 09 23:28:18 2007 +0200 +++ b/src/Pure/Tools/codegen_func.ML Thu May 10 00:39:45 2007 +0200 @@ -109,7 +109,7 @@ val _ = map (check 0) args; in thm end; -val mk_func = assert_func o Drule.fconv_rule Drule.beta_eta_conversion o mk_rew; +val mk_func = assert_func o Conv.fconv_rule Drule.beta_eta_conversion o mk_rew; fun head_func thm = let @@ -183,7 +183,7 @@ in thms |> map (expand_eta k) - |> map (Drule.fconv_rule Drule.beta_eta_conversion) + |> map (Conv.fconv_rule Drule.beta_eta_conversion) end; fun canonical_tvars purify_tvar thm =