moved conversions to structure Conv;
authorwenzelm
Thu May 10 00:39:45 2007 +0200 (2007-05-10 ago)
changeset 22900f8a7c10e1bd0
parent 22899 5ea718c68123
child 22901 481cd919c47f
moved conversions to structure Conv;
src/HOL/Code_Generator.thy
src/HOL/Library/EfficientNat.thy
src/HOL/Tools/sat_funcs.ML
src/HOL/arith_data.ML
src/Provers/induct_method.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/element.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Tools/codegen_func.ML
     1.1 --- a/src/HOL/Code_Generator.thy	Wed May 09 23:28:18 2007 +0200
     1.2 +++ b/src/HOL/Code_Generator.thy	Thu May 10 00:39:45 2007 +0200
     1.3 @@ -73,8 +73,8 @@
     1.4  method_setup evaluation = {*
     1.5  let
     1.6  
     1.7 -fun evaluation_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
     1.8 -  (Drule.goals_conv (equal i) Codegen.evaluation_conv));
     1.9 +fun evaluation_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
    1.10 +  (Conv.goals_conv (equal i) Codegen.evaluation_conv));
    1.11  
    1.12  in Method.no_args (Method.SIMPLE_METHOD' (evaluation_tac THEN' rtac TrueI)) end
    1.13  *} "solve goal by evaluation"
    1.14 @@ -201,8 +201,8 @@
    1.15  
    1.16  method_setup normalization = {*
    1.17  let
    1.18 -  fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
    1.19 -    (Drule.goals_conv (equal i) (HOLogic.Trueprop_conv
    1.20 +  fun normalization_tac i = Tactical.PRIMITIVE (Conv.fconv_rule
    1.21 +    (Conv.goals_conv (equal i) (HOLogic.Trueprop_conv
    1.22        NBE.normalization_conv)));
    1.23  in
    1.24    Method.no_args (Method.SIMPLE_METHOD' (normalization_tac THEN' resolve_tac [TrueI, refl]))
     2.1 --- a/src/HOL/Library/EfficientNat.thy	Wed May 09 23:28:18 2007 +0200
     2.2 +++ b/src/HOL/Library/EfficientNat.thy	Thu May 10 00:39:45 2007 +0200
     2.3 @@ -290,7 +290,7 @@
     2.4        let
     2.5          val th' =
     2.6            Thm.implies_elim
     2.7 -           (Drule.fconv_rule (Thm.beta_conversion true)
     2.8 +           (Conv.fconv_rule (Thm.beta_conversion true)
     2.9               (Drule.instantiate'
    2.10                 [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
    2.11                   SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
    2.12 @@ -338,7 +338,7 @@
    2.13          let
    2.14            val cert = cterm_of (Thm.theory_of_thm th);
    2.15            val th'' = ObjectLogic.rulify (Thm.implies_elim
    2.16 -            (Drule.fconv_rule (Thm.beta_conversion true)
    2.17 +            (Conv.fconv_rule (Thm.beta_conversion true)
    2.18                (Drule.instantiate' []
    2.19                  [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
    2.20                     abstract_over (Sucv,
     3.1 --- a/src/HOL/Tools/sat_funcs.ML	Wed May 09 23:28:18 2007 +0200
     3.2 +++ b/src/HOL/Tools/sat_funcs.ML	Thu May 10 00:39:45 2007 +0200
     3.3 @@ -434,7 +434,7 @@
     3.4  
     3.5  fun pre_cnf_tac i =
     3.6  	rtac ccontr i THEN ObjectLogic.atomize_tac i THEN
     3.7 -		PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (Drule.beta_eta_conversion)));
     3.8 +		PRIMITIVE (Conv.fconv_rule (Conv.goals_conv (equal i) (Drule.beta_eta_conversion)));
     3.9  
    3.10  (* ------------------------------------------------------------------------- *)
    3.11  (* cnfsat_tac: checks if the empty clause "False" occurs among the premises; *)
     4.1 --- a/src/HOL/arith_data.ML	Wed May 09 23:28:18 2007 +0200
     4.2 +++ b/src/HOL/arith_data.ML	Thu May 10 00:39:45 2007 +0200
     4.3 @@ -896,8 +896,8 @@
     4.4          (TRY o REPEAT_ALL_NEW (split_once_tac split_thms))
     4.5            THEN_ALL_NEW
     4.6              ((fn j => PRIMITIVE
     4.7 -                        (Drule.fconv_rule
     4.8 -                          (Drule.goals_conv (equal j) (Drule.beta_eta_conversion))))
     4.9 +                        (Conv.fconv_rule
    4.10 +                          (Conv.goals_conv (equal j) (Drule.beta_eta_conversion))))
    4.11                THEN'
    4.12              (TRY o (etac notE THEN' eq_assume_tac)))
    4.13        ) i
     5.1 --- a/src/Provers/induct_method.ML	Wed May 09 23:28:18 2007 +0200
     5.2 +++ b/src/Provers/induct_method.ML	Thu May 10 00:39:45 2007 +0200
     5.3 @@ -195,7 +195,7 @@
     5.4  
     5.5  fun internalize k th =
     5.6    th |> Thm.permute_prems 0 k
     5.7 -  |> Drule.fconv_rule (Drule.concl_conv (Thm.nprems_of th - k) atomize_cterm);
     5.8 +  |> Conv.fconv_rule (Conv.concl_conv (Thm.nprems_of th - k) atomize_cterm);
     5.9  
    5.10  
    5.11  (* guess rule instantiation -- cannot handle pending goal parameters *)
    5.12 @@ -310,9 +310,9 @@
    5.13      | NONE => all_tac)
    5.14    end);
    5.15  
    5.16 -fun miniscope_tac p i = PRIMITIVE (Drule.fconv_rule
    5.17 -  (Drule.goals_conv (Library.equal i)
    5.18 -    (Drule.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]))));
    5.19 +fun miniscope_tac p i = PRIMITIVE (Conv.fconv_rule
    5.20 +  (Conv.goals_conv (Library.equal i)
    5.21 +    (Conv.forall_conv p (MetaSimplifier.rewrite true [Thm.symmetric Drule.norm_hhf_eq]))));
    5.22  
    5.23  in
    5.24  
     6.1 --- a/src/Pure/Isar/attrib.ML	Wed May 09 23:28:18 2007 +0200
     6.2 +++ b/src/Pure/Isar/attrib.ML	Thu May 10 00:39:45 2007 +0200
     6.3 @@ -252,7 +252,8 @@
     6.4    let val ((_, [th']), _) = Variable.import_thms true [th] (Context.proof_of ctxt)
     6.5    in th' end)) x;
     6.6  
     6.7 -fun eta_long x = no_args (Thm.rule_attribute (K (Drule.fconv_rule Drule.eta_long_conversion))) x;
     6.8 +fun eta_long x =
     6.9 +  no_args (Thm.rule_attribute (K (Conv.fconv_rule Drule.eta_long_conversion))) x;
    6.10  
    6.11  
    6.12  (* internal attribute *)
     7.1 --- a/src/Pure/Isar/element.ML	Wed May 09 23:28:18 2007 +0200
     7.2 +++ b/src/Pure/Isar/element.ML	Thu May 10 00:39:45 2007 +0200
     7.3 @@ -456,7 +456,7 @@
     7.4        else th |> hyps_rule
     7.5         (instantiate_tfrees thy substT #>
     7.6          instantiate_frees thy subst #>
     7.7 -        Drule.fconv_rule (Thm.beta_conversion true))
     7.8 +        Conv.fconv_rule (Thm.beta_conversion true))
     7.9      end;
    7.10  
    7.11  fun inst_morphism thy envs =
     8.1 --- a/src/Pure/Isar/local_defs.ML	Wed May 09 23:28:18 2007 +0200
     8.2 +++ b/src/Pure/Isar/local_defs.ML	Thu May 10 00:39:45 2007 +0200
     8.3 @@ -171,10 +171,10 @@
     8.4    MetaSimplifier.rewrite_cterm (false, false, false) (K (K NONE))
     8.5      (equals_ss addsimps (Rules.get (Context.Proof ctxt)));
     8.6  
     8.7 -val meta_rewrite_rule = Drule.fconv_rule o meta_rewrite;
     8.8 +val meta_rewrite_rule = Conv.fconv_rule o meta_rewrite;
     8.9  
    8.10  fun meta_rewrite_tac ctxt i =
    8.11 -  PRIMITIVE (Drule.fconv_rule (Drule.goals_conv (equal i) (meta_rewrite ctxt)));
    8.12 +  PRIMITIVE (Conv.fconv_rule (Conv.goals_conv (equal i) (meta_rewrite ctxt)));
    8.13  
    8.14  
    8.15  (* rewriting with object-level rules *)
     9.1 --- a/src/Pure/Isar/object_logic.ML	Wed May 09 23:28:18 2007 +0200
     9.2 +++ b/src/Pure/Isar/object_logic.ML	Thu May 10 00:39:45 2007 +0200
     9.3 @@ -141,10 +141,10 @@
     9.4  
     9.5  (* atomize *)
     9.6  
     9.7 -fun rewrite_prems_tac rews i = PRIMITIVE (Drule.fconv_rule
     9.8 -  (Drule.goals_conv (Library.equal i)
     9.9 -    (Drule.forall_conv ~1
    9.10 -      (Drule.goals_conv (K true) (MetaSimplifier.rewrite true rews)))));
    9.11 +fun rewrite_prems_tac rews i = PRIMITIVE (Conv.fconv_rule
    9.12 +  (Conv.goals_conv (Library.equal i)
    9.13 +    (Conv.forall_conv ~1
    9.14 +      (Conv.goals_conv (K true) (MetaSimplifier.rewrite true rews)))));
    9.15  
    9.16  fun atomize_term thy =
    9.17    drop_judgment thy o MetaSimplifier.rewrite_term thy (get_atomize thy) [];
    10.1 --- a/src/Pure/Isar/rule_cases.ML	Wed May 09 23:28:18 2007 +0200
    10.2 +++ b/src/Pure/Isar/rule_cases.ML	Thu May 10 00:39:45 2007 +0200
    10.3 @@ -189,14 +189,14 @@
    10.4  
    10.5  fun unfold_prems n defs th =
    10.6    if null defs then th
    10.7 -  else Drule.fconv_rule (Drule.goals_conv (fn i => i <= n) (MetaSimplifier.rewrite true defs)) th;
    10.8 +  else Conv.fconv_rule (Conv.goals_conv (fn i => i <= n) (MetaSimplifier.rewrite true defs)) th;
    10.9  
   10.10  fun unfold_prems_concls defs th =
   10.11    if null defs orelse not (can Logic.dest_conjunction (Thm.concl_of th)) then th
   10.12    else
   10.13 -    Drule.fconv_rule
   10.14 -      (Drule.concl_conv ~1 (Conjunction.conv ~1
   10.15 -        (K (Drule.prems_conv ~1 (K (MetaSimplifier.rewrite true defs)))))) th;
   10.16 +    Conv.fconv_rule
   10.17 +      (Conv.concl_conv ~1 (Conjunction.conv ~1
   10.18 +        (K (Conv.prems_conv ~1 (K (MetaSimplifier.rewrite true defs)))))) th;
   10.19  
   10.20  in
   10.21  
    11.1 --- a/src/Pure/Tools/codegen_func.ML	Wed May 09 23:28:18 2007 +0200
    11.2 +++ b/src/Pure/Tools/codegen_func.ML	Thu May 10 00:39:45 2007 +0200
    11.3 @@ -109,7 +109,7 @@
    11.4      val _ = map (check 0) args;
    11.5    in thm end;
    11.6  
    11.7 -val mk_func = assert_func o Drule.fconv_rule Drule.beta_eta_conversion o mk_rew;
    11.8 +val mk_func = assert_func o Conv.fconv_rule Drule.beta_eta_conversion o mk_rew;
    11.9  
   11.10  fun head_func thm =
   11.11    let
   11.12 @@ -183,7 +183,7 @@
   11.13    in
   11.14      thms
   11.15      |> map (expand_eta k)
   11.16 -    |> map (Drule.fconv_rule Drule.beta_eta_conversion)
   11.17 +    |> map (Conv.fconv_rule Drule.beta_eta_conversion)
   11.18    end;
   11.19  
   11.20  fun canonical_tvars purify_tvar thm =