--- a/src/HOL/Decision_Procs/Approximation.thy Sat Feb 15 18:28:18 2014 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Sat Feb 15 18:48:43 2014 +0100
@@ -3242,7 +3242,6 @@
oracle approximation_oracle = {* fn (thy, t) =>
let
-
fun bad t = error ("Bad term: " ^ Syntax.string_of_term_global thy t);
fun term_of_bool true = @{term True}
@@ -3424,10 +3423,8 @@
end
end
- (* copied from Tools/induct.ML should probably in args.ML *)
val free = Args.context -- Args.term >> (fn (_, Free (n, _)) => n | (ctxt, t) =>
error ("Bad free variable: " ^ Syntax.string_of_term ctxt t));
-
*}
lemma intervalE: "a \<le> x \<and> x \<le> b \<Longrightarrow> \<lbrakk> x \<in> { a .. b } \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
@@ -3455,7 +3452,7 @@
THEN DETERM (Reification.tac ctxt form_equations NONE i)
THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
THEN gen_eval_tac (approximation_conv ctxt) ctxt i))
- *} "real number approximation"
+*} "real number approximation"
ML {*
fun calculated_subterms (@{const Trueprop} $ t) = calculated_subterms t
@@ -3473,7 +3470,9 @@
| dest_interpret t = raise TERM ("dest_interpret", [t])
- fun dest_float (@{const "Float"} $ m $ e) = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
+ fun dest_float (@{const "Float"} $ m $ e) =
+ (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
+
fun dest_ivl (Const (@{const_name "Some"}, _) $
(Const (@{const_name Pair}, _) $ u $ l)) = SOME (dest_float u, dest_float l)
| dest_ivl (Const (@{const_name "None"}, _)) = NONE
@@ -3516,7 +3515,8 @@
in (sgn * (digits + x * (Integer.pow e10 10)), ~e10)
end)
- fun mk_result prec (SOME (l, u)) = (let
+ fun mk_result prec (SOME (l, u)) =
+ (let
fun mk_float10 rnd x = (let val (m, e) = float2_float10 prec rnd x
in if e = 0 then HOLogic.mk_number @{typ real} m
else if e = 1 then @{term "divide :: real \<Rightarrow> real \<Rightarrow> real"} $
@@ -3529,7 +3529,8 @@
in @{term "atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set"} $ mk_float10 true l $ mk_float10 false u end)
| mk_result _ NONE = @{term "UNIV :: real set"}
- fun realify t = let
+ fun realify t =
+ let
val t = Logic.varify_global t
val m = map (fn (name, _) => (name, @{typ real})) (Term.add_tvars t [])
val t = Term.subst_TVars m t
@@ -3579,13 +3580,12 @@
|> dest_ivl
|> mk_result prec
- fun approx prec ctxt t = if type_of t = @{typ prop} then approx_form prec ctxt t
- else if type_of t = @{typ bool} then approx_form prec ctxt (@{const Trueprop} $ t)
- else approx_arith prec ctxt t
+ fun approx prec ctxt t =
+ if type_of t = @{typ prop} then approx_form prec ctxt t
+ else if type_of t = @{typ bool} then approx_form prec ctxt (@{const Trueprop} $ t)
+ else approx_arith prec ctxt t
*}
-setup {*
- Value.add_evaluator ("approximate", approx 30)
-*}
+setup {* Value.add_evaluator ("approximate", approx 30) *}
end
--- a/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Sat Feb 15 18:28:18 2014 +0100
+++ b/src/HOL/Decision_Procs/ferrante_rackoff_data.ML Sat Feb 15 18:48:43 2014 +0100
@@ -68,9 +68,7 @@
fun match ctxt tm =
let
- fun match_inst
- ({minf, pinf, nmi, npi, ld, qe, atoms},
- fns as {isolate_conv, whatis, simpset}) pat =
+ fun match_inst ({minf, pinf, nmi, npi, ld, qe, atoms}, fns) pat =
let
fun h instT =
let
--- a/src/HOL/Decision_Procs/langford.ML Sat Feb 15 18:28:18 2014 +0100
+++ b/src/HOL/Decision_Procs/langford.ML Sat Feb 15 18:48:43 2014 +0100
@@ -2,24 +2,24 @@
Author: Amine Chaieb, TU Muenchen
*)
-signature LANGFORD_QE =
+signature LANGFORD_QE =
sig
val dlo_tac : Proof.context -> int -> tactic
val dlo_conv : Proof.context -> cterm -> thm
end
-structure LangfordQE :LANGFORD_QE =
+structure LangfordQE: LANGFORD_QE =
struct
val dest_set =
- let
- fun h acc ct =
+ let
+ fun h acc ct =
case term_of ct of
Const (@{const_name Orderings.bot}, _) => acc
| Const (@{const_name insert}, _) $ _ $ t => h (Thm.dest_arg1 ct :: acc) (Thm.dest_arg ct)
in h [] end;
-fun prove_finite cT u =
+fun prove_finite cT u =
let val [th0,th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
fun ins x th =
Thm.implies_elim (instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg)
@@ -31,47 +31,47 @@
(Conv.arg_conv
(Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms ball_simps simp_thms})));
-fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
- case term_of ep of
- Const(@{const_name Ex},_)$_ =>
- let
+fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
+ case term_of ep of
+ Const(@{const_name Ex},_)$_ =>
+ let
val p = Thm.dest_arg ep
val ths =
simplify (put_simpset HOL_basic_ss ctxt addsimps gather) (instantiate' [] [SOME p] stupid)
- val (L,U) =
- let
- val (x,q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
+ val (L,U) =
+ let
+ val (_, q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1)
end
- fun proveneF S =
+ fun proveneF S =
let val (a,A) = Thm.dest_comb S |>> Thm.dest_arg
val cT = ctyp_of_term a
- val ne = instantiate' [SOME cT] [SOME a, SOME A]
+ val ne = instantiate' [SOME cT] [SOME a, SOME A]
@{thm insert_not_empty}
val f = prove_finite cT (dest_set S)
in (ne, f) end
- val qe = case (term_of L, term_of U) of
- (Const (@{const_name Orderings.bot}, _),_) =>
+ val qe = case (term_of L, term_of U) of
+ (Const (@{const_name Orderings.bot}, _),_) =>
let
- val (neU,fU) = proveneF U
+ val (neU,fU) = proveneF U
in simp_rule ctxt (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
- | (_,Const (@{const_name Orderings.bot}, _)) =>
+ | (_,Const (@{const_name Orderings.bot}, _)) =>
let
val (neL,fL) = proveneF L
in simp_rule ctxt (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
- | (_,_) =>
- let
+ | (_,_) =>
+ let
val (neL,fL) = proveneF L
val (neU,fU) = proveneF U
- in simp_rule ctxt (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU]))
+ in simp_rule ctxt (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU]))
end
- in qe end
+ in qe end
| _ => error "dlo_qe : Not an existential formula";
-val all_conjuncts =
- let fun h acc ct =
+val all_conjuncts =
+ let fun h acc ct =
case term_of ct of
@{term HOL.conj}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
| _ => ct::acc
@@ -86,10 +86,10 @@
val list_conj = fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c') ;
-fun mk_conj_tab th =
- let fun h acc th =
+fun mk_conj_tab th =
+ let fun h acc th =
case prop_of th of
- @{term "Trueprop"}$(@{term HOL.conj}$p$q) =>
+ @{term "Trueprop"}$(@{term HOL.conj}$p$q) =>
h (h acc (th RS conjunct2)) (th RS conjunct1)
| @{term "Trueprop"}$p => (p,th)::acc
in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
@@ -97,22 +97,22 @@
fun is_conj (@{term HOL.conj}$_$_) = true
| is_conj _ = false;
-fun prove_conj tab cjs =
- case cjs of
+fun prove_conj tab cjs =
+ case cjs of
[c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c
| c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs];
-fun conj_aci_rule eq =
- let
+fun conj_aci_rule eq =
+ let
val (l,r) = Thm.dest_equals eq
fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c))
fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c))
val ll = Thm.dest_arg l
val rr = Thm.dest_arg r
-
- val thl = prove_conj tabl (conjuncts rr)
+
+ val thl = prove_conj tabl (conjuncts rr)
|> Drule.implies_intr_hyps
- val thr = prove_conj tabr (conjuncts ll)
+ val thr = prove_conj tabr (conjuncts ll)
|> Drule.implies_intr_hyps
val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
@@ -123,53 +123,52 @@
Const(@{const_name HOL.eq},_)$l$r => l aconv term_of x orelse r aconv term_of x
| _ => false ;
-local
-fun proc ctxt ct =
+local
+fun proc ctxt ct =
case term_of ct of
- Const(@{const_name Ex},_)$Abs (xn,_,_) =>
- let
+ Const(@{const_name Ex},_)$Abs (xn,_,_) =>
+ let
val e = Thm.dest_fun ct
val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
- val Pp = Thm.apply @{cterm "Trueprop"} p
+ val Pp = Thm.apply @{cterm "Trueprop"} p
val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
in case eqs of
- [] =>
- let
+ [] =>
+ let
val (dx,ndx) = List.partition (contains x) neqs
in case ndx of [] => NONE
| _ =>
- conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
+ conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
(Thm.apply @{cterm Trueprop} (list_conj (ndx @dx))))
- |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
- |> Conv.fconv_rule (Conv.arg_conv
+ |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
+ |> Conv.fconv_rule (Conv.arg_conv
(Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
|> SOME
end
- | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
+ | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
(Thm.apply @{cterm Trueprop} (list_conj (eqs@neqs))))
- |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
- |> Conv.fconv_rule (Conv.arg_conv
+ |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
+ |> Conv.fconv_rule (Conv.arg_conv
(Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
|> SOME
end
| _ => NONE;
-in val reduce_ex_simproc =
- Simplifier.make_simproc
+in val reduce_ex_simproc =
+ Simplifier.make_simproc
{lhss = [@{cpat "EX x. ?P x"}] , name = "reduce_ex_simproc",
proc = K proc, identifier = []}
end;
-fun raw_dlo_conv ctxt dlo_ss
- ({qe_bnds, qe_nolb, qe_noub, gst, gs, atoms}:Langford_Data.entry) =
- let
+fun raw_dlo_conv ctxt dlo_ss ({qe_bnds, qe_nolb, qe_noub, gst, gs, ...}: Langford_Data.entry) =
+ let
val ctxt' = put_simpset dlo_ss ctxt addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc]
val dnfex_conv = Simplifier.rewrite ctxt'
val pcv =
Simplifier.rewrite
(put_simpset dlo_ss ctxt
addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
- in fn p =>
- Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
+ in fn p =>
+ Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
(Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive)
(K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
end;
@@ -201,7 +200,7 @@
in h end;
fun dlo_instance ctxt tm =
- (fst (Langford_Data.get ctxt),
+ (fst (Langford_Data.get ctxt),
Langford_Data.match ctxt (grab_atom_bop 0 tm));
fun dlo_conv ctxt tm =
@@ -209,8 +208,8 @@
(_, NONE) => raise CTERM ("dlo_conv (langford): no corresponding instance in context!", [tm])
| (ss, SOME instance) => raw_dlo_conv ctxt ss instance tm);
-fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
- let
+fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
+ let
fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
@@ -219,12 +218,12 @@
fun cfrees ats ct =
- let
+ let
val ins = insert (op aconvc)
- fun h acc t =
+ fun h acc t =
case (term_of t) of
- b$_$_ => if member (op aconvc) ats (Thm.dest_fun2 t)
- then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc)
+ _$_$_ => if member (op aconvc) ats (Thm.dest_fun2 t)
+ then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc)
else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
| _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
| Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
--- a/src/HOL/Decision_Procs/mir_tac.ML Sat Feb 15 18:28:18 2014 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sat Feb 15 18:48:43 2014 +0100
@@ -4,16 +4,12 @@
signature MIR_TAC =
sig
- val trace: bool Unsynchronized.ref
val mir_tac: Proof.context -> bool -> int -> tactic
end
-structure Mir_Tac =
+structure Mir_Tac: MIR_TAC =
struct
-val trace = Unsynchronized.ref false;
-fun trace_msg s = if !trace then tracing s else ();
-
val mir_ss =
let val ths = [@{thm "real_of_int_inject"}, @{thm "real_of_int_less_iff"}, @{thm "real_of_int_le_iff"}]
in simpset_of (@{context} delsimps ths addsimps (map (fn th => th RS sym) ths))
@@ -38,21 +34,8 @@
val comp_ths = ths @ comp_arith @ @{thms simp_thms};
-val zdvd_int = @{thm "zdvd_int"};
-val zdiff_int_split = @{thm "zdiff_int_split"};
-val all_nat = @{thm "all_nat"};
-val ex_nat = @{thm "ex_nat"};
-val split_zdiv = @{thm "split_zdiv"};
-val split_zmod = @{thm "split_zmod"};
val mod_div_equality' = @{thm "mod_div_equality'"};
-val split_div' = @{thm "split_div'"};
-val imp_le_cong = @{thm "imp_le_cong"};
-val conj_le_cong = @{thm "conj_le_cong"};
val mod_add_eq = @{thm "mod_add_eq"} RS sym;
-val mod_add_left_eq = @{thm "mod_add_left_eq"} RS sym;
-val mod_add_right_eq = @{thm "mod_add_right_eq"} RS sym;
-val nat_div_add_eq = @{thm "div_add1_eq"} RS sym;
-val int_div_add_eq = @{thm "zdiv_zadd1_eq"} RS sym;
fun prepare_for_mir q fm =
let
@@ -136,10 +119,8 @@
then mirfr_oracle (false, cterm_of thy (Envir.eta_long [] t1))
else mirfr_oracle (true, cterm_of thy (Envir.eta_long [] t1))
in
- (trace_msg ("calling procedure with term:\n" ^
- Syntax.string_of_term ctxt t1);
- ((pth RS iffD2) RS pre_thm,
- assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
+ ((pth RS iffD2) RS pre_thm,
+ assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
end
| _ => (pre_thm, assm_tac i)
in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);