--- a/src/HOL/HOL.thy Wed Aug 26 10:48:45 2009 +0200
+++ b/src/HOL/HOL.thy Wed Aug 26 11:40:28 2009 +0200
@@ -29,6 +29,7 @@
"~~/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 Wed Aug 26 10:48:45 2009 +0200
+++ b/src/HOL/IsaMakefile Wed Aug 26 11:40:28 2009 +0200
@@ -108,6 +108,7 @@
$(SRC)/Tools/random_word.ML \
$(SRC)/Tools/value.ML \
$(SRC)/Tools/Code_Generator.thy \
+ $(SRC)/Tools/more_conv.ML \
HOL.thy \
Tools/hologic.ML \
Tools/recfun_codegen.ML \
--- a/src/HOL/Library/normarith.ML Wed Aug 26 10:48:45 2009 +0200
+++ b/src/HOL/Library/normarith.ML Wed Aug 26 11:40:28 2009 +0200
@@ -15,7 +15,7 @@
structure NormArith : NORM_ARITH =
struct
- open Conv Thm Conv2;
+ open Conv Thm;
val bool_eq = op = : bool *bool -> bool
fun dest_ratconst t = case term_of t of
Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
@@ -322,6 +322,7 @@
val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE
else SOME(norm_cmul_rule v t))
(v ~~ nubs)
+ fun end_itlist f xs = split_last xs |> uncurry (fold_rev f)
in inequality_canon_rule ctxt (end_itlist norm_add_rule ths)
end
val ges' = map_filter (try compute_ineq) (fold_rev (append o consider) destfuns []) @
@@ -332,9 +333,9 @@
in RealArith.real_linear_prover translator
(map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
zerodests,
- map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv
+ map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
arg_conv (arg_conv real_poly_conv))) ges',
- map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv
+ map (fconv_rule (try_conv (More_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
@@ -353,6 +354,7 @@
val ntms = fold_rev find_normedterms (map (dest_arg o concl) (ges @ gts)) []
val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
+ fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns
--- a/src/HOL/Library/positivstellensatz.ML Wed Aug 26 10:48:45 2009 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Wed Aug 26 11:40:28 2009 +0200
@@ -81,82 +81,6 @@
structure Ctermfunc = FuncFun(type key = cterm val ord = (fn (s,t) => TermOrd.fast_term_ord(term_of s, term_of t)));
structure Ratfunc = FuncFun(type key = Rat.rat val ord = Rat.ord);
- (* Some conversions-related stuff which has been forbidden entrance into Pure/conv.ML*)
-structure Conv2 =
-struct
- open Conv
-fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
-fun is_comb t = case (term_of t) of _$_ => true | _ => false;
-fun is_abs t = case (term_of t) of Abs _ => true | _ => false;
-
-fun end_itlist f l =
- case l of
- [] => error "end_itlist"
- | [x] => x
- | (h::t) => f h (end_itlist f t);
-
- fun absc cv ct = case term_of ct of
- Abs (v,_, _) =>
- let val (x,t) = Thm.dest_abs (SOME v) ct
- in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t)
- end
- | _ => all_conv ct;
-
-fun cache_conv conv =
- let
- val tab = ref Termtab.empty
- fun cconv t =
- case Termtab.lookup (!tab) (term_of t) of
- SOME th => th
- | NONE => let val th = conv t
- in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end
- in cconv end;
-fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
- handle CTERM _ => false;
-
-local
- fun thenqc conv1 conv2 tm =
- case try conv1 tm of
- SOME th1 => (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2 | NONE => th1)
- | NONE => conv2 tm
-
- fun thencqc conv1 conv2 tm =
- let val th1 = conv1 tm
- in (case try conv2 (Thm.rhs_of th1) of SOME th2 => Thm.transitive th1 th2 | NONE => th1)
- end
- fun comb_qconv conv tm =
- let val (l,r) = Thm.dest_comb tm
- in (case try conv l of
- SOME th1 => (case try conv r of SOME th2 => Thm.combination th1 th2
- | NONE => Drule.fun_cong_rule th1 r)
- | NONE => Drule.arg_cong_rule l (conv r))
- end
- fun repeatqc conv tm = thencqc conv (repeatqc conv) tm
- fun sub_qconv conv tm = if is_abs tm then absc conv tm else comb_qconv conv tm
- fun once_depth_qconv conv tm =
- (conv else_conv (sub_qconv (once_depth_qconv conv))) tm
- fun depth_qconv conv tm =
- thenqc (sub_qconv (depth_qconv conv))
- (repeatqc conv) tm
- fun redepth_qconv conv tm =
- thenqc (sub_qconv (redepth_qconv conv))
- (thencqc conv (redepth_qconv conv)) tm
- fun top_depth_qconv conv tm =
- thenqc (repeatqc conv)
- (thencqc (sub_qconv (top_depth_qconv conv))
- (thencqc conv (top_depth_qconv conv))) tm
- fun top_sweep_qconv conv tm =
- thenqc (repeatqc conv)
- (sub_qconv (top_sweep_qconv conv)) tm
-in
-val (once_depth_conv, depth_conv, rdepth_conv, top_depth_conv, top_sweep_conv) =
- (fn c => try_conv (once_depth_qconv c),
- fn c => try_conv (depth_qconv c),
- fn c => try_conv (redepth_qconv c),
- fn c => try_conv (top_depth_qconv c),
- fn c => try_conv (top_sweep_qconv c));
-end;
-end;
(* Some useful derived rules *)
@@ -373,15 +297,6 @@
fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
fun is_comb t = case (term_of t) of _$_ => true | _ => false;
-fun cache_conv conv =
- let
- val tab = ref Termtab.empty
- fun cconv t =
- case Termtab.lookup (!tab) (term_of t) of
- SOME th => th
- | NONE => let val th = conv t
- in ((tab := Termtab.insert Thm.eq_thm (term_of t, th) (!tab)); th) end
- in cconv end;
fun is_binop ct ct' = ct aconvc (Thm.dest_fun (Thm.dest_fun ct'))
handle CTERM _ => false;
@@ -571,7 +486,7 @@
val nnf_norm_conv' =
nnf_conv then_conv
literals_conv [@{term "op &"}, @{term "op |"}] []
- (cache_conv
+ (More_Conv.cache_conv
(first_conv [real_lt_conv, real_le_conv,
real_eq_conv, real_not_lt_conv,
real_not_le_conv, real_not_eq_conv, all_conv]))
--- a/src/HOL/Tools/Function/fundef_core.ML Wed Aug 26 10:48:45 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_core.ML Wed Aug 26 11:40:28 2009 +0200
@@ -577,8 +577,6 @@
val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm accp_subset_induct}
-fun binder_conv cv ctxt = Conv.arg_conv (Conv.abs_conv (K cv) ctxt);
-
fun mk_partial_induct_rule thy globals R complete_thm clauses =
let
val Globals {domT, x, z, a, P, D, ...} = globals
@@ -614,7 +612,7 @@
val case_hyp_conv = K (case_hyp RS eq_reflection)
local open Conv in
val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
- val sih = fconv_rule (binder_conv (arg1_conv (arg_conv (arg_conv case_hyp_conv))) ctxt) aihyp
+ val sih = fconv_rule (More_Conv.binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
end
fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/more_conv.ML Wed Aug 26 11:40:28 2009 +0200
@@ -0,0 +1,61 @@
+(* Title: Tools/more_conv.ML
+ Author: Sascha Boehme
+
+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
+
+ val cache_conv: conv -> 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)
+
+
+fun cache_conv conv =
+ let
+ val tab = ref Termtab.empty
+ fun add_result t thm =
+ let val _ = change tab (Termtab.insert Thm.eq_thm (t, thm))
+ in thm end
+ fun cconv ct =
+ (case Termtab.lookup (!tab) (Thm.term_of ct) of
+ SOME thm => thm
+ | NONE => add_result (Thm.term_of ct) (conv ct))
+ in cconv end
+
+end