--- a/src/HOL/Boogie/Tools/boogie_tactics.ML Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML Sat May 15 17:59:06 2010 +0200
@@ -25,8 +25,8 @@
val label_eqs = [assert_at_def, block_at_def]
fun unfold_labels_tac ctxt =
- let val unfold = More_Conv.rewrs_conv label_eqs
- in CONVERSION (More_Conv.top_sweep_conv (K unfold) ctxt) end
+ let val unfold = Conv.rewrs_conv label_eqs
+ in CONVERSION (Conv.top_sweep_conv (K unfold) ctxt) end
fun boogie_tac ctxt rules =
unfold_labels_tac ctxt
--- a/src/HOL/HOL.thy Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/HOL.thy Sat May 15 17:59:06 2010 +0200
@@ -29,7 +29,6 @@
"~~/src/Tools/induct.ML"
("~~/src/Tools/induct_tacs.ML")
("Tools/recfun_codegen.ML")
- "~~/src/Tools/more_conv.ML"
begin
setup {* Intuitionistic.method_setup @{binding iprover} *}
--- a/src/HOL/IsaMakefile Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/IsaMakefile Sat May 15 17:59:06 2010 +0200
@@ -128,7 +128,6 @@
$(SRC)/Tools/induct.ML \
$(SRC)/Tools/induct_tacs.ML \
$(SRC)/Tools/intuitionistic.ML \
- $(SRC)/Tools/more_conv.ML \
$(SRC)/Tools/nbe.ML \
$(SRC)/Tools/project_rule.ML \
$(SRC)/Tools/quickcheck.ML \
--- a/src/HOL/Library/normarith.ML Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Library/normarith.ML Sat May 15 17:59:06 2010 +0200
@@ -182,7 +182,6 @@
fun botc1 conv ct =
((sub_conv (botc1 conv)) then_conv (conv else_conv all_conv)) ct;
- fun rewrs_conv eqs ct = first_conv (map rewr_conv eqs) ct;
val apply_pth1 = rewr_conv @{thm pth_1};
val apply_pth2 = rewr_conv @{thm pth_2};
val apply_pth3 = rewr_conv @{thm pth_3};
@@ -333,9 +332,9 @@
in fst (RealArith.real_linear_prover translator
(map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
zerodests,
- map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
+ map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
arg_conv (arg_conv real_poly_conv))) ges',
- map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
+ map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
arg_conv (arg_conv real_poly_conv))) gts))
end
in val real_vector_combo_prover = real_vector_combo_prover
--- a/src/HOL/Tools/Function/function_core.ML Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Sat May 15 17:59:06 2010 +0200
@@ -617,7 +617,7 @@
local open Conv in
val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
val sih =
- fconv_rule (More_Conv.binder_conv
+ fconv_rule (Conv.binder_conv
(K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
end
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sat May 15 17:59:06 2010 +0200
@@ -490,7 +490,7 @@
end
| _ => Conv.all_conv ctrm
-fun lambda_prs_conv ctxt = More_Conv.top_conv lambda_prs_simple_conv ctxt
+fun lambda_prs_conv ctxt = Conv.top_conv lambda_prs_simple_conv ctxt
fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
--- a/src/HOL/Tools/SMT/smt_normalize.ML Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_normalize.ML Sat May 15 17:59:06 2010 +0200
@@ -47,11 +47,11 @@
"distinct [x, y] == (x ~= y)"
by simp_all}
fun distinct_conv _ =
- if_true_conv is_trivial_distinct (More_Conv.rewrs_conv thms)
+ if_true_conv is_trivial_distinct (Conv.rewrs_conv thms)
in
fun trivial_distinct ctxt =
map ((Term.exists_subterm is_trivial_distinct o Thm.prop_of) ??
- Conv.fconv_rule (More_Conv.top_conv distinct_conv ctxt))
+ Conv.fconv_rule (Conv.top_conv distinct_conv ctxt))
end
@@ -67,11 +67,11 @@
"(case P of True => x | False => y) == (if P then x else y)"
"(case P of False => y | True => x) == (if P then x else y)"
by (rule eq_reflection, simp)+}
- val unfold_conv = if_true_conv is_bool_case (More_Conv.rewrs_conv thms)
+ val unfold_conv = if_true_conv is_bool_case (Conv.rewrs_conv thms)
in
fun rewrite_bool_cases ctxt =
map ((Term.exists_subterm is_bool_case o Thm.prop_of) ??
- Conv.fconv_rule (More_Conv.top_conv (K unfold_conv) ctxt))
+ Conv.fconv_rule (Conv.top_conv (K unfold_conv) ctxt))
end
@@ -107,7 +107,7 @@
in
fun normalize_numerals ctxt =
map ((Term.exists_subterm (is_strange_number ctxt) o Thm.prop_of) ??
- Conv.fconv_rule (More_Conv.top_sweep_conv pos_conv ctxt))
+ Conv.fconv_rule (Conv.top_sweep_conv pos_conv ctxt))
end
@@ -193,7 +193,7 @@
local
val eta_conv = eta_expand_conv
- fun keep_conv ctxt = More_Conv.binder_conv norm_conv ctxt
+ fun keep_conv ctxt = Conv.binder_conv (norm_conv o snd) ctxt
and eta_binder_conv ctxt = Conv.arg_conv (eta_conv norm_conv ctxt)
and keep_let_conv ctxt = Conv.combination_conv
(Conv.arg_conv (norm_conv ctxt)) (Conv.abs_conv (norm_conv o snd) ctxt)
@@ -267,7 +267,7 @@
Conv.binop_conv (atomize_conv ctxt) then_conv
Conv.rewr_conv @{thm atomize_eq}
| Const (@{const_name all}, _) $ Abs _ =>
- More_Conv.binder_conv atomize_conv ctxt then_conv
+ Conv.binder_conv (atomize_conv o snd) ctxt then_conv
Conv.rewr_conv @{thm atomize_all}
| _ => Conv.all_conv) ct
--- a/src/HOL/Tools/SMT/smtlib_interface.ML Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML Sat May 15 17:59:06 2010 +0200
@@ -81,7 +81,7 @@
fun unfold_abs_min_max_defs ctxt thm =
if exists_abs_min_max (Thm.prop_of thm)
- then Conv.fconv_rule (More_Conv.top_conv unfold_def_conv ctxt) thm
+ then Conv.fconv_rule (Conv.top_conv unfold_def_conv ctxt) thm
else thm
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML Sat May 15 17:59:06 2010 +0200
@@ -540,7 +540,7 @@
fun elim_unused_conv ctxt =
Conv.params_conv ~1 (K (Conv.arg_conv (Conv.arg1_conv
- (More_Conv.rewrs_conv [elim_all, elim_ex])))) ctxt
+ (Conv.rewrs_conv [elim_all, elim_ex])))) ctxt
fun elim_unused_tac ctxt =
REPEAT_ALL_NEW (
--- a/src/HOL/Tools/SMT/z3_proof_tools.ML Sat May 15 15:31:33 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_tools.ML Sat May 15 17:59:06 2010 +0200
@@ -96,7 +96,7 @@
fun unfold_eqs _ [] = Conv.all_conv
| unfold_eqs ctxt eqs =
- More_Conv.top_sweep_conv (K (More_Conv.rewrs_conv eqs)) ctxt
+ Conv.top_sweep_conv (K (Conv.rewrs_conv eqs)) ctxt
fun match_instantiate f ct thm =
Thm.instantiate (Thm.match (f (Thm.cprop_of thm), ct)) thm
@@ -256,7 +256,7 @@
val set5 = @{lemma "x ~: set (y # ys) == x ~= y & x ~: set ys" by simp}
fun set_conv ct =
- (More_Conv.rewrs_conv [set1, set2, set3, set4] else_conv
+ (Conv.rewrs_conv [set1, set2, set3, set4] else_conv
(Conv.rewr_conv set5 then_conv Conv.arg_conv set_conv)) ct
val dist1 = @{lemma "distinct [] == ~False" by simp}
@@ -267,7 +267,7 @@
fun binop_conv cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
in
fun unfold_distinct_conv ct =
- (More_Conv.rewrs_conv [dist1, dist2] else_conv
+ (Conv.rewrs_conv [dist1, dist2] else_conv
(Conv.rewr_conv dist3 then_conv binop_conv set_conv unfold_distinct_conv)) ct
end
--- a/src/Pure/conv.ML Sat May 15 15:31:33 2010 +0200
+++ b/src/Pure/conv.ML Sat May 15 17:59:06 2010 +0200
@@ -1,5 +1,6 @@
(* Title: Pure/conv.ML
Author: Amine Chaieb, TU Muenchen
+ Author: Sascha Boehme, TU Muenchen
Author: Makarius
Conversions: primitive equality reasoning.
@@ -32,10 +33,16 @@
val arg1_conv: conv -> conv
val fun2_conv: conv -> conv
val binop_conv: conv -> conv
+ val binder_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
val forall_conv: (cterm * Proof.context -> conv) -> Proof.context -> conv
val implies_conv: conv -> conv -> conv
val implies_concl_conv: conv -> conv
val rewr_conv: thm -> conv
+ val rewrs_conv: thm list -> conv
+ val sub_conv: (Proof.context -> conv) -> Proof.context -> conv
+ val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv
+ val top_conv: (Proof.context -> conv) -> Proof.context -> conv
+ val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
val params_conv: int -> (Proof.context -> conv) -> Proof.context -> conv
val prems_conv: int -> conv -> conv
val concl_conv: int -> conv -> conv
@@ -105,6 +112,29 @@
fun binop_conv cv = combination_conv (arg_conv cv) cv;
+fun binder_conv cv ctxt = arg_conv (abs_conv cv ctxt);
+
+
+(* subterm structure *)
+
+(*cf. SUB_CONV in HOL*)
+fun sub_conv conv ctxt =
+ comb_conv (conv ctxt) else_conv
+ abs_conv (conv o snd) ctxt else_conv
+ all_conv;
+
+(*cf. BOTTOM_CONV in HOL*)
+fun bottom_conv conv ctxt ct =
+ (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct;
+
+(*cf. TOP_CONV in HOL*)
+fun top_conv conv ctxt ct =
+ (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct;
+
+(*cf. TOP_SWEEP_CONV in HOL*)
+fun top_sweep_conv conv ctxt ct =
+ (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct;
+
(* primitive logic *)
@@ -136,6 +166,8 @@
handle Pattern.MATCH => raise CTERM ("rewr_conv", [lhs, ct])
end;
+fun rewrs_conv rules = first_conv (map rewr_conv rules);
+
(* conversions on HHF rules *)
--- a/src/Tools/more_conv.ML Sat May 15 15:31:33 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,43 +0,0 @@
-(* Title: Tools/more_conv.ML
- Author: Sascha Boehme, TU Muenchen
-
-Further conversions and conversionals.
-*)
-
-signature MORE_CONV =
-sig
- val rewrs_conv: thm list -> conv
-
- val sub_conv: (Proof.context -> conv) -> Proof.context -> conv
- val bottom_conv: (Proof.context -> conv) -> Proof.context -> conv
- val top_conv: (Proof.context -> conv) -> Proof.context -> conv
- val top_sweep_conv: (Proof.context -> conv) -> Proof.context -> conv
-
- val binder_conv: (Proof.context -> conv) -> Proof.context -> conv
-end
-
-structure More_Conv : MORE_CONV =
-struct
-
-fun rewrs_conv eqs = Conv.first_conv (map Conv.rewr_conv eqs)
-
-
-fun sub_conv conv ctxt =
- Conv.comb_conv (conv ctxt) else_conv
- Conv.abs_conv (fn (_, cx) => conv cx) ctxt else_conv
- Conv.all_conv
-
-fun bottom_conv conv ctxt ct =
- (sub_conv (bottom_conv conv) ctxt then_conv conv ctxt) ct
-
-fun top_conv conv ctxt ct =
- (conv ctxt then_conv sub_conv (top_conv conv) ctxt) ct
-
-fun top_sweep_conv conv ctxt ct =
- (conv ctxt else_conv sub_conv (top_sweep_conv conv) ctxt) ct
-
-
-fun binder_conv cv ctxt =
- Conv.arg_conv (Conv.abs_conv (fn (_, cx) => cv cx) ctxt)
-
-end