incorporated further conversions and conversionals, after some minor tuning;
authorwenzelm
Sat May 15 17:59:06 2010 +0200 (2010-05-15)
changeset 36936c52d1c130898
parent 36935 a3715d7ff337
child 36937 a30e50d4aeeb
incorporated further conversions and conversionals, after some minor tuning;
src/HOL/Boogie/Tools/boogie_tactics.ML
src/HOL/HOL.thy
src/HOL/IsaMakefile
src/HOL/Library/normarith.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smtlib_interface.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Tools/SMT/z3_proof_tools.ML
src/Pure/conv.ML
src/Tools/more_conv.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Sat May 15 15:31:33 2010 +0200
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Sat May 15 17:59:06 2010 +0200
     1.3 @@ -25,8 +25,8 @@
     1.4  val label_eqs = [assert_at_def, block_at_def]
     1.5  
     1.6  fun unfold_labels_tac ctxt =
     1.7 -  let val unfold = More_Conv.rewrs_conv label_eqs
     1.8 -  in CONVERSION (More_Conv.top_sweep_conv (K unfold) ctxt) end
     1.9 +  let val unfold = Conv.rewrs_conv label_eqs
    1.10 +  in CONVERSION (Conv.top_sweep_conv (K unfold) ctxt) end
    1.11  
    1.12  fun boogie_tac ctxt rules =
    1.13    unfold_labels_tac ctxt
     2.1 --- a/src/HOL/HOL.thy	Sat May 15 15:31:33 2010 +0200
     2.2 +++ b/src/HOL/HOL.thy	Sat May 15 17:59:06 2010 +0200
     2.3 @@ -29,7 +29,6 @@
     2.4    "~~/src/Tools/induct.ML"
     2.5    ("~~/src/Tools/induct_tacs.ML")
     2.6    ("Tools/recfun_codegen.ML")
     2.7 -  "~~/src/Tools/more_conv.ML"
     2.8  begin
     2.9  
    2.10  setup {* Intuitionistic.method_setup @{binding iprover} *}
     3.1 --- a/src/HOL/IsaMakefile	Sat May 15 15:31:33 2010 +0200
     3.2 +++ b/src/HOL/IsaMakefile	Sat May 15 17:59:06 2010 +0200
     3.3 @@ -128,7 +128,6 @@
     3.4    $(SRC)/Tools/induct.ML \
     3.5    $(SRC)/Tools/induct_tacs.ML \
     3.6    $(SRC)/Tools/intuitionistic.ML \
     3.7 -  $(SRC)/Tools/more_conv.ML \
     3.8    $(SRC)/Tools/nbe.ML \
     3.9    $(SRC)/Tools/project_rule.ML \
    3.10    $(SRC)/Tools/quickcheck.ML \
     4.1 --- a/src/HOL/Library/normarith.ML	Sat May 15 15:31:33 2010 +0200
     4.2 +++ b/src/HOL/Library/normarith.ML	Sat May 15 17:59:06 2010 +0200
     4.3 @@ -182,7 +182,6 @@
     4.4  fun botc1 conv ct = 
     4.5    ((sub_conv (botc1 conv)) then_conv (conv else_conv all_conv)) ct;
     4.6  
     4.7 - fun rewrs_conv eqs ct = first_conv (map rewr_conv eqs) ct;
     4.8   val apply_pth1 = rewr_conv @{thm pth_1};
     4.9   val apply_pth2 = rewr_conv @{thm pth_2};
    4.10   val apply_pth3 = rewr_conv @{thm pth_3};
    4.11 @@ -333,9 +332,9 @@
    4.12    in fst (RealArith.real_linear_prover translator
    4.13          (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
    4.14              zerodests,
    4.15 -        map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
    4.16 +        map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
    4.17                         arg_conv (arg_conv real_poly_conv))) ges',
    4.18 -        map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv 
    4.19 +        map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv 
    4.20                         arg_conv (arg_conv real_poly_conv))) gts))
    4.21    end
    4.22  in val real_vector_combo_prover = real_vector_combo_prover
     5.1 --- a/src/HOL/Tools/Function/function_core.ML	Sat May 15 15:31:33 2010 +0200
     5.2 +++ b/src/HOL/Tools/Function/function_core.ML	Sat May 15 17:59:06 2010 +0200
     5.3 @@ -617,7 +617,7 @@
     5.4          local open Conv in
     5.5            val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
     5.6            val sih =
     5.7 -            fconv_rule (More_Conv.binder_conv
     5.8 +            fconv_rule (Conv.binder_conv
     5.9                (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
    5.10          end
    5.11  
     6.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat May 15 15:31:33 2010 +0200
     6.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat May 15 17:59:06 2010 +0200
     6.3 @@ -490,7 +490,7 @@
     6.4        end
     6.5    | _ => Conv.all_conv ctrm
     6.6  
     6.7 -fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt
     6.8 +fun lambda_prs_conv ctxt = Conv.top_conv lambda_prs_simple_conv ctxt
     6.9  fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
    6.10  
    6.11  
     7.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Sat May 15 15:31:33 2010 +0200
     7.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Sat May 15 17:59:06 2010 +0200
     7.3 @@ -47,11 +47,11 @@
     7.4      "distinct [x, y] == (x ~= y)"
     7.5      by simp_all}
     7.6    fun distinct_conv _ =
     7.7 -    if_true_conv is_trivial_distinct (More_Conv.rewrs_conv thms)
     7.8 +    if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
     7.9  in
    7.10  fun trivial_distinct ctxt =
    7.11    map ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
    7.12 -    Conv.fconv_rule (More_Conv.top_conv distinct_conv ctxt))
    7.13 +    Conv.fconv_rule (Conv.top_conv distinct_conv ctxt))
    7.14  end
    7.15  
    7.16  
    7.17 @@ -67,11 +67,11 @@
    7.18      "(case P of True => x | False => y) == (if P then x else y)"
    7.19      "(case P of False => y | True => x) == (if P then x else y)"
    7.20      by (rule eq_reflection, simp)+}
    7.21 -  val unfold_conv = if_true_conv is_bool_case (More_Conv.rewrs_conv thms)
    7.22 +  val unfold_conv = if_true_conv is_bool_case (Conv.rewrs_conv thms)
    7.23  in
    7.24  fun rewrite_bool_cases ctxt =
    7.25    map ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
    7.26 -    Conv.fconv_rule (More_Conv.top_conv (K unfold_conv) ctxt))
    7.27 +    Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt))
    7.28  end
    7.29  
    7.30  
    7.31 @@ -107,7 +107,7 @@
    7.32  in
    7.33  fun normalize_numerals ctxt =
    7.34    map ((Term.exists_subterm (is_strange_number ctxt) o Thm.prop_of) ??
    7.35 -    Conv.fconv_rule (More_Conv.top_sweep_conv pos_conv ctxt))
    7.36 +    Conv.fconv_rule (Conv.top_sweep_conv pos_conv ctxt))
    7.37  end
    7.38  
    7.39  
    7.40 @@ -193,7 +193,7 @@
    7.41  local
    7.42    val eta_conv = eta_expand_conv
    7.43  
    7.44 -  fun keep_conv ctxt = More_Conv.binder_conv norm_conv ctxt
    7.45 +  fun keep_conv ctxt = Conv.binder_conv (norm_conv o snd) ctxt
    7.46    and eta_binder_conv ctxt = Conv.arg_conv (eta_conv norm_conv ctxt)
    7.47    and keep_let_conv ctxt = Conv.combination_conv
    7.48      (Conv.arg_conv (norm_conv ctxt)) (Conv.abs_conv (norm_conv o snd) ctxt)
    7.49 @@ -267,7 +267,7 @@
    7.50        Conv.binop_conv (atomize_conv ctxt) then_conv
    7.51        Conv.rewr_conv @{thm atomize_eq}
    7.52    | Const (@{const_name all}, _) $ Abs _ =>
    7.53 -      More_Conv.binder_conv atomize_conv ctxt then_conv
    7.54 +      Conv.binder_conv (atomize_conv o snd) ctxt then_conv
    7.55        Conv.rewr_conv @{thm atomize_all}
    7.56    | _ => Conv.all_conv) ct
    7.57  
     8.1 --- a/src/HOL/Tools/SMT/smtlib_interface.ML	Sat May 15 15:31:33 2010 +0200
     8.2 +++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Sat May 15 17:59:06 2010 +0200
     8.3 @@ -81,7 +81,7 @@
     8.4  
     8.5  fun unfold_abs_min_max_defs ctxt thm =
     8.6    if exists_abs_min_max (Thm.prop_of thm)
     8.7 -  then Conv.fconv_rule (More_Conv.top_conv unfold_def_conv ctxt) thm
     8.8 +  then Conv.fconv_rule (Conv.top_conv unfold_def_conv ctxt) thm
     8.9    else thm
    8.10  
    8.11  
     9.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat May 15 15:31:33 2010 +0200
     9.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Sat May 15 17:59:06 2010 +0200
     9.3 @@ -540,7 +540,7 @@
     9.4  
     9.5    fun elim_unused_conv ctxt =
     9.6      Conv.params_conv ~1 (K (Conv.arg_conv (Conv.arg1_conv
     9.7 -      (More_Conv.rewrs_conv [elim_all, elim_ex])))) ctxt
     9.8 +      (Conv.rewrs_conv [elim_all, elim_ex])))) ctxt
     9.9  
    9.10    fun elim_unused_tac ctxt =
    9.11      REPEAT_ALL_NEW (
    10.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Sat May 15 15:31:33 2010 +0200
    10.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Sat May 15 17:59:06 2010 +0200
    10.3 @@ -96,7 +96,7 @@
    10.4  
    10.5  fun unfold_eqs _ [] = Conv.all_conv
    10.6    | unfold_eqs ctxt eqs =
    10.7 -      More_Conv.top_sweep_conv (K (More_Conv.rewrs_conv eqs)) ctxt
    10.8 +      Conv.top_sweep_conv (K (Conv.rewrs_conv eqs)) ctxt
    10.9  
   10.10  fun match_instantiate f ct thm =
   10.11    Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
   10.12 @@ -256,7 +256,7 @@
   10.13    val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
   10.14  
   10.15    fun set_conv ct =
   10.16 -    (More_Conv.rewrs_conv [set1, set2, set3, set4] else_conv
   10.17 +    (Conv.rewrs_conv [set1, set2, set3, set4] else_conv
   10.18      (Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
   10.19  
   10.20    val dist1 = @{lemma "distinct [] == ~False" by simp}
   10.21 @@ -267,7 +267,7 @@
   10.22    fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
   10.23  in
   10.24  fun unfold_distinct_conv ct =
   10.25 -  (More_Conv.rewrs_conv [dist1, dist2] else_conv
   10.26 +  (Conv.rewrs_conv [dist1, dist2] else_conv
   10.27    (Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
   10.28  end
   10.29  
    11.1 --- a/src/Pure/conv.ML	Sat May 15 15:31:33 2010 +0200
    11.2 +++ b/src/Pure/conv.ML	Sat May 15 17:59:06 2010 +0200
    11.3 @@ -1,5 +1,6 @@
    11.4  (*  Title:      Pure/conv.ML
    11.5      Author:     Amine Chaieb, TU Muenchen
    11.6 +    Author:     Sascha Boehme, TU Muenchen
    11.7      Author:     Makarius
    11.8  
    11.9  Conversions: primitive equality reasoning.
   11.10 @@ -32,10 +33,16 @@
   11.11    val arg1_conv: conv -> conv
   11.12    val fun2_conv: conv -> conv
   11.13    val binop_conv: conv -> conv
   11.14 +  val binder_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
   11.15    val forall_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
   11.16    val implies_conv: conv -> conv -> conv
   11.17    val implies_concl_conv: conv -> conv
   11.18    val rewr_conv: thm -> conv
   11.19 +  val rewrs_conv: thm list -> conv
   11.20 +  val sub_conv: (Proof.context -> conv) -> Proof.context -> conv
   11.21 +  val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv
   11.22 +  val top_conv: (Proof.context -> conv) -> Proof.context -> conv
   11.23 +  val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
   11.24    val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
   11.25    val prems_conv: int -> conv -> conv
   11.26    val concl_conv: int -> conv -> conv
   11.27 @@ -105,6 +112,29 @@
   11.28  
   11.29  fun binop_conv cv = combination_conv (arg_conv cv) cv;
   11.30  
   11.31 +fun binder_conv cv ctxt = arg_conv (abs_conv cv ctxt);
   11.32 +
   11.33 +
   11.34 +(* subterm structure *)
   11.35 +
   11.36 +(*cf. SUB_CONV in HOL*)
   11.37 +fun sub_conv conv ctxt =
   11.38 +  comb_conv (conv ctxt) else_conv
   11.39 +  abs_conv (conv o snd) ctxt else_conv
   11.40 +  all_conv;
   11.41 +
   11.42 +(*cf. BOTTOM_CONV in HOL*)
   11.43 +fun bottom_conv conv ctxt ct =
   11.44 +  (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct;
   11.45 +
   11.46 +(*cf. TOP_CONV in HOL*)
   11.47 +fun top_conv conv ctxt ct =
   11.48 +  (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct;
   11.49 +
   11.50 +(*cf. TOP_SWEEP_CONV in HOL*)
   11.51 +fun top_sweep_conv conv ctxt ct =
   11.52 +  (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct;
   11.53 +
   11.54  
   11.55  (* primitive logic *)
   11.56  
   11.57 @@ -136,6 +166,8 @@
   11.58        handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
   11.59    end;
   11.60  
   11.61 +fun rewrs_conv rules = first_conv (map rewr_conv rules);
   11.62 +
   11.63  
   11.64  (* conversions on HHF rules *)
   11.65  
    12.1 --- a/src/Tools/more_conv.ML	Sat May 15 15:31:33 2010 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,43 +0,0 @@
    12.4 -(*  Title:       Tools/more_conv.ML
    12.5 -    Author:      Sascha Boehme, TU Muenchen
    12.6 -
    12.7 -Further conversions and conversionals.
    12.8 -*)
    12.9 -
   12.10 -signature MORE_CONV =
   12.11 -sig
   12.12 -  val rewrs_conv: thm list -> conv
   12.13 -
   12.14 -  val sub_conv: (Proof.context -> conv) -> Proof.context -> conv
   12.15 -  val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv
   12.16 -  val top_conv: (Proof.context -> conv) -> Proof.context -> conv
   12.17 -  val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
   12.18 -
   12.19 -  val binder_conv: (Proof.context -> conv) -> Proof.context -> conv
   12.20 -end
   12.21 -
   12.22 -structure More_Conv : MORE_CONV =
   12.23 -struct
   12.24 -
   12.25 -fun rewrs_conv eqs = Conv.first_conv (map Conv.rewr_conv eqs)
   12.26 -
   12.27 -
   12.28 -fun sub_conv conv ctxt =
   12.29 -  Conv.comb_conv (conv ctxt) else_conv
   12.30 -  Conv.abs_conv (fn (_, cx) => conv cx) ctxt else_conv
   12.31 -  Conv.all_conv
   12.32 -
   12.33 -fun bottom_conv conv ctxt ct =
   12.34 -  (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct
   12.35 -
   12.36 -fun top_conv conv ctxt ct =
   12.37 -  (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct
   12.38 -
   12.39 -fun top_sweep_conv conv ctxt ct =
   12.40 -  (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct
   12.41 -
   12.42 -
   12.43 -fun binder_conv cv ctxt =
   12.44 -  Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt)
   12.45 -
   12.46 -end