# HG changeset patch # User wenzelm # Date 1392486523 -3600 # Node ID 46f3e31c5a87e77caddfdb1e44d20fb31cd12a40 # Parent 2a1ca7f6607be0a1bf71857ed44f0990b89ca84d removed dead code; tuned; diff -r 2a1ca7f6607b -r 46f3e31c5a87 src/HOL/Decision_Procs/Approximation.thy --- 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 \ x \ x \ b \ \ x \ { a .. b } \ P\ \ 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 \ real \ real"} $ @@ -3529,7 +3529,8 @@ in @{term "atLeastAtMost :: real \ real \ 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 diff -r 2a1ca7f6607b -r 46f3e31c5a87 src/HOL/Decision_Procs/ferrante_rackoff_data.ML --- 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 diff -r 2a1ca7f6607b -r 46f3e31c5a87 src/HOL/Decision_Procs/langford.ML --- 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)) diff -r 2a1ca7f6607b -r 46f3e31c5a87 src/HOL/Decision_Procs/mir_tac.ML --- 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);