# HG changeset patch # User wenzelm # Date 1441121136 -7200 # Node ID f6b0d827240ebbc30cb079ed65ae1f048adaba82 # Parent 44a8cd035dfbe5de4814984eae709b4f4ea89816 tuned -- avoid slightly odd @{cpat}; diff -r 44a8cd035dfb -r f6b0d827240e src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Mon Aug 31 22:45:40 2015 +0200 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Tue Sep 01 17:25:36 2015 +0200 @@ -902,15 +902,6 @@ | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd) | t => Rat.rat_of_int (snd (HOLogic.dest_number t)) -fun mk_frac phi cT x = - let val (a, b) = Rat.quotient_of_rat x - in if b = 1 then Numeral.mk_cnumber cT a - else Thm.apply - (Thm.apply (Drule.cterm_rule (Thm.instantiate' [SOME cT] []) @{cpat "op /"}) - (Numeral.mk_cnumber cT a)) - (Numeral.mk_cnumber cT b) - end - fun whatis x ct = case Thm.term_of ct of Const(@{const_name Groups.plus}, _)$(Const(@{const_name Groups.times},_)$_$y)$_ => if y aconv Thm.term_of x then ("c*x+t",[(funpow 2 Thm.dest_arg1) ct, Thm.dest_arg ct]) @@ -973,9 +964,10 @@ (case whatis x (Thm.dest_arg1 ct) of ("c*x+t",[c,t]) => let - val T = Thm.ctyp_of_cterm x + val T = Thm.typ_of_cterm x + val cT = Thm.ctyp_of_cterm x val cr = dest_frac c - val clt = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "op <"} + val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool})) val cz = Thm.dest_arg ct val neg = cr let - val T = Thm.ctyp_of_cterm x + val T = Thm.typ_of_cterm x + val cT = Thm.ctyp_of_cterm x val cr = dest_frac c - val clt = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "op <"} + val clt = Thm.cterm_of ctxt (Const (@{const_name ord_class.less}, T --> T --> @{typ bool})) val cz = Thm.dest_arg ct val neg = cr ferrack_conv ctxt (thy,{isolate_conv = isolate_conv ctxt, whatis = whatis, simpset = ss}) vs diff -r 44a8cd035dfb -r f6b0d827240e src/HOL/Decision_Procs/langford.ML --- a/src/HOL/Decision_Procs/langford.ML Mon Aug 31 22:45:40 2015 +0200 +++ b/src/HOL/Decision_Procs/langford.ML Tue Sep 01 17:25:36 2015 +0200 @@ -190,7 +190,7 @@ 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 + Qelim.gen_qelim_conv ctxt pcv pcv dnfex_conv cons (Drule.cterm_add_frees p []) (K Thm.reflexive) (K Thm.reflexive) (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p end; @@ -228,12 +228,12 @@ (_, 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, _) => PRIMITIVE (fn st => +fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st => let - fun all T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "Pure.all"} - fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t) - val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p) - val p' = fold_rev gen ts p + fun all x t = + Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t) + val ts = sort (fn (a, b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p) + val p' = fold_rev all ts p in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end)); fun cfrees ats ct = @@ -259,7 +259,7 @@ Object_Logic.full_atomize_tac ctxt i THEN simp_tac (put_simpset ss ctxt) i THEN (CONVERSION Thm.eta_long_conversion) i - THEN (TRY o generalize_tac (cfrees (#atoms instance))) i + THEN (TRY o generalize_tac ctxt (cfrees (#atoms instance))) i THEN Object_Logic.full_atomize_tac ctxt i THEN CONVERSION (Object_Logic.judgment_conv ctxt (raw_dlo_conv ctxt ss instance)) i THEN (simp_tac (put_simpset ss ctxt) i))); diff -r 44a8cd035dfb -r f6b0d827240e src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Mon Aug 31 22:45:40 2015 +0200 +++ b/src/HOL/Library/positivstellensatz.ML Tue Sep 01 17:25:36 2015 +0200 @@ -514,14 +514,15 @@ | _ => "x" fun mk_forall x th = - Drule.arg_cong_rule - (instantiate_cterm' [SOME (Thm.ctyp_of_cterm x)] [] @{cpat "All :: (?'a => bool) => _" }) - (Thm.abstract_rule (name_of x) x th) + let + val T = Thm.typ_of_cterm x + val all = Thm.cterm_of ctxt (Const (@{const_name All}, (T --> @{typ bool}) --> @{typ bool})) + in Drule.arg_cong_rule all (Thm.abstract_rule (name_of x) x th) end val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec)); - fun ext T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat Ex} - fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t) + fun ext T = Thm.cterm_of ctxt (Const (@{const_name Ex}, (T --> @{typ bool}) --> @{typ bool})) + fun mk_ex v t = Thm.apply (ext (Thm.typ_of_cterm v)) (Thm.lambda v t) fun choose v th th' = case Thm.concl_of th of diff -r 44a8cd035dfb -r f6b0d827240e src/HOL/Multivariate_Analysis/normarith.ML --- a/src/HOL/Multivariate_Analysis/normarith.ML Mon Aug 31 22:45:40 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Tue Sep 01 17:25:36 2015 +0200 @@ -343,8 +343,14 @@ 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 (Thm.instantiate' ty tms) - fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t - fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm l)] [] @{cpat "op == :: ?'a =>_"}) l) r + fun mk_norm t = + let val T = Thm.typ_of_cterm t + in Thm.apply (Thm.cterm_of ctxt' (Const (@{const_name norm}, T --> @{typ real}))) t end + fun mk_equals l r = + let + val T = Thm.typ_of_cterm l + val eq = Thm.cterm_of ctxt (Const (@{const_name Pure.eq}, T --> T --> propT)) + in Thm.apply (Thm.apply eq l) r end val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (Thm.cterm_of ctxt' (Free(n,@{typ real}))))) lctab fxns val replace_conv = try_conv (rewrs_conv asl) val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv)) diff -r 44a8cd035dfb -r f6b0d827240e src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Mon Aug 31 22:45:40 2015 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Tue Sep 01 17:25:36 2015 +0200 @@ -569,7 +569,7 @@ [not_all, all_not_ex, @{thm ex_disj_distrib}])); fun conv ctxt p = - Qelim.gen_qelim_conv + Qelim.gen_qelim_conv ctxt (Simplifier.rewrite (put_simpset conv_ss ctxt)) (Simplifier.rewrite (put_simpset presburger_ss ctxt)) (Simplifier.rewrite (put_simpset conv_ss ctxt)) @@ -799,12 +799,12 @@ in h [] ct end end; -fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st => +fun generalize_tac ctxt f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st => let - fun all T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat "Pure.all"} - fun gen x t = Thm.apply (all (Thm.ctyp_of_cterm x)) (Thm.lambda x t) - val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p) - val p' = fold_rev gen ts p + fun all x t = + Thm.apply (Thm.cterm_of ctxt (Logic.all_const (Thm.typ_of_cterm x))) (Thm.lambda x t) + val ts = sort (fn (a, b) => Term_Ord.fast_term_ord (Thm.term_of a, Thm.term_of b)) (f p) + val p' = fold_rev all ts p in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end)); local @@ -875,7 +875,7 @@ THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt THEN_ALL_NEW CONVERSION Thm.eta_long_conversion THEN_ALL_NEW simp_tac simpset_ctxt - THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt)) + THEN_ALL_NEW (TRY o generalize_tac ctxt (int_nat_terms ctxt)) THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt THEN_ALL_NEW (thin_prems_tac ctxt (is_relevant ctxt)) THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt diff -r 44a8cd035dfb -r f6b0d827240e src/HOL/Tools/Qelim/qelim.ML --- a/src/HOL/Tools/Qelim/qelim.ML Mon Aug 31 22:45:40 2015 +0200 +++ b/src/HOL/Tools/Qelim/qelim.ML Tue Sep 01 17:25:36 2015 +0200 @@ -6,7 +6,7 @@ signature QELIM = sig - val gen_qelim_conv: conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a -> + val gen_qelim_conv: Proof.context -> conv -> conv -> conv -> (cterm -> 'a -> 'a) -> 'a -> ('a -> conv) -> ('a -> conv) -> ('a -> conv) -> conv val standard_qelim_conv: Proof.context -> (cterm list -> conv) -> (cterm list -> conv) -> @@ -18,7 +18,7 @@ val all_not_ex = mk_meta_eq @{thm "all_not_ex"}; -fun gen_qelim_conv precv postcv simpex_conv ins env atcv ncv qcv = +fun gen_qelim_conv ctxt precv postcv simpex_conv ins env atcv ncv qcv = let fun conv env p = case Thm.term_of p of @@ -41,10 +41,10 @@ in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th)) else Thm.transitive (Thm.transitive th th') (conv env r) end | Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p - | Const(@{const_name All},_)$_ => + | Const(@{const_name All}, allT)$_ => let + val T = Thm.ctyp_of ctxt (#1 (Term.dest_funT (#1 (Term.dest_funT allT)))) val p = Thm.dest_arg p - val ([(_,T)],[]) = Thm.match (@{cpat "All"}, Thm.dest_fun p) val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex in Thm.transitive th (conv env (Thm.rhs_of th)) end @@ -65,7 +65,7 @@ fun standard_qelim_conv ctxt atcv ncv qcv p = let val pcv = pcv ctxt - in gen_qelim_conv pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end + in gen_qelim_conv ctxt pcv pcv pcv cons (Drule.cterm_add_frees p []) atcv ncv qcv p end end; diff -r 44a8cd035dfb -r f6b0d827240e src/HOL/Tools/Transfer/transfer.ML --- a/src/HOL/Tools/Transfer/transfer.ML Mon Aug 31 22:45:40 2015 +0200 +++ b/src/HOL/Tools/Transfer/transfer.ML Tue Sep 01 17:25:36 2015 +0200 @@ -709,7 +709,8 @@ (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules) THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 handle TERM (_, ts) => raise TERM (err_msg, ts) - val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac) + val goal = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), @{typ bool}))) + val thm3 = Goal.prove_internal ctxt' [] goal (K tac) val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT in thm3 @@ -746,7 +747,8 @@ (SOLVED' (REPEAT_ALL_NEW (resolve_tac ctxt' rules) THEN_ALL_NEW (DETERM o eq_rules_tac ctxt' eq_rules)))) 1 handle TERM (_, ts) => raise TERM (err_msg, ts) - val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac) + val goal = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (Var (("P", 0), @{typ bool}))) + val thm3 = Goal.prove_internal ctxt' [] goal (K tac) val tnames = map (fst o dest_TFree o Thm.typ_of o snd) instT in thm3 diff -r 44a8cd035dfb -r f6b0d827240e src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Mon Aug 31 22:45:40 2015 +0200 +++ b/src/HOL/Tools/groebner.ML Tue Sep 01 17:25:36 2015 +0200 @@ -478,8 +478,8 @@ (* Conversion for the equivalence of existential statements where EX quantifiers are rearranged differently *) - fun ext T = Drule.cterm_rule (Thm.instantiate' [SOME T] []) @{cpat Ex} - fun mk_ex v t = Thm.apply (ext (Thm.ctyp_of_cterm v)) (Thm.lambda v t) +fun ext ctxt T = Thm.cterm_of ctxt (Const (@{const_name Ex}, (T --> @{typ bool}) --> @{typ bool})) +fun mk_ex ctxt v t = Thm.apply (ext ctxt (Thm.typ_of_cterm v)) (Thm.lambda v t) fun choose v th th' = case Thm.concl_of th of @{term Trueprop} $ (Const(@{const_name Ex},_)$_) => @@ -494,8 +494,8 @@ in Thm.implies_elim (Thm.implies_elim th0 th) th1 end | _ => error "" (* FIXME ? *) -fun simple_choose v th = - choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v) +fun simple_choose ctxt v th = + choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex ctxt v) (Thm.dest_arg (hd (Thm.chyps_of th))))) th @@ -507,14 +507,14 @@ (Thm.instantiate' [SOME (Thm.ctyp_of_cterm v)] [SOME p, SOME v] @{thm exI})) th end - fun ex_eq_conv t = + fun ex_eq_conv ctxt t = let val (p0,q0) = Thm.dest_binop t val (vs',P) = strip_exists p0 val (vs,_) = strip_exists q0 val th = Thm.assume (Thm.apply @{cterm Trueprop} P) - val th1 = implies_intr_hyps (fold simple_choose vs' (fold mkexi vs th)) - val th2 = implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th)) + val th1 = implies_intr_hyps (fold (simple_choose ctxt) vs' (fold mkexi vs th)) + val th2 = implies_intr_hyps (fold (simple_choose ctxt) vs (fold mkexi vs' th)) val p = (Thm.dest_arg o Thm.dest_arg1 o Thm.cprop_of) th1 val q = (Thm.dest_arg o Thm.dest_arg o Thm.cprop_of) th1 in Thm.implies_elim (Thm.implies_elim (Thm.instantiate' [] [SOME p, SOME q] iffI) th1) th2 @@ -527,7 +527,7 @@ | Var ((s,_),_) => s | _ => "x" fun mk_eq s t = Thm.apply (Thm.apply @{cterm "op == :: bool => _"} s) t - fun mk_exists v th = Drule.arg_cong_rule (ext (Thm.ctyp_of_cterm v)) + fun mk_exists ctxt v th = Drule.arg_cong_rule (ext ctxt (Thm.typ_of_cterm v)) (Thm.abstract_rule (getname v) v th) fun simp_ex_conv ctxt = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms(39)}) @@ -738,9 +738,10 @@ fun ring ctxt tm = let fun mk_forall x p = - Thm.apply - (Drule.cterm_rule (Thm.instantiate' [SOME (Thm.ctyp_of_cterm x)] []) - @{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p) + let + val T = Thm.typ_of_cterm x; + val all = Thm.cterm_of ctxt (Const (@{const_name All}, (T --> @{typ bool}) --> @{typ bool})) + in Thm.apply all (Thm.lambda x p) end val avs = Drule.cterm_add_frees tm [] val P' = fold mk_forall avs tm val th1 = initial_conv ctxt (mk_neg P') @@ -829,9 +830,9 @@ (Drule.binop_cong_rule @{cterm HOL.conj} th1 (Thm.reflexive (Thm.dest_arg (Thm.rhs_of th2)))) val v = Thm.dest_arg1(Thm.dest_arg1(Thm.rhs_of th3)) - val th4 = Conv.fconv_rule (Conv.arg_conv (simp_ex_conv ctxt)) (mk_exists v th3) - val th5 = ex_eq_conv (mk_eq tm (fold mk_ex (remove op aconvc v vars) (Thm.lhs_of th4))) - in Thm.transitive th5 (fold mk_exists (remove op aconvc v vars) th4) + val th4 = Conv.fconv_rule (Conv.arg_conv (simp_ex_conv ctxt)) (mk_exists ctxt v th3) + val th5 = ex_eq_conv ctxt (mk_eq tm (fold (mk_ex ctxt) (remove op aconvc v vars) (Thm.lhs_of th4))) + in Thm.transitive th5 (fold (mk_exists ctxt) (remove op aconvc v vars) th4) end; end diff -r 44a8cd035dfb -r f6b0d827240e src/HOL/Tools/semiring_normalizer.ML --- a/src/HOL/Tools/semiring_normalizer.ML Mon Aug 31 22:45:40 2015 +0200 +++ b/src/HOL/Tools/semiring_normalizer.ML Tue Sep 01 17:25:36 2015 +0200 @@ -123,6 +123,9 @@ Simplifier.rewrite (put_simpset semiring_norm_ss ctxt) then_conv Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms numeral_1_eq_1}))}; +val divide_const = Thm.cterm_of @{context} (Logic.varify_global @{term "op /"}); +val [divide_tvar] = Term.add_tvars (Thm.term_of divide_const) []; + val field_funs = let fun numeral_is_const ct = @@ -142,7 +145,7 @@ let val (a, b) = Rat.quotient_of_rat x in if b = 1 then Numeral.mk_cnumber cT a else Thm.apply - (Thm.apply (Drule.cterm_rule (Thm.instantiate' [SOME cT] []) @{cpat "op /"}) + (Thm.apply (Thm.instantiate_cterm ([(divide_tvar, cT)], []) divide_const) (Numeral.mk_cnumber cT a)) (Numeral.mk_cnumber cT b) end