# HG changeset patch # User wenzelm # Date 1635105576 -7200 # Node ID 08b4292abe2ba0b83fdbfe221db33f5c6d1317c0 # Parent d3e36521fcc77efc33609e5b97805efc51cf1f6e more antiquotations; diff -r d3e36521fcc7 -r 08b4292abe2b src/HOL/Analysis/normarith.ML --- a/src/HOL/Analysis/normarith.ML Sun Oct 24 21:19:55 2021 +0200 +++ b/src/HOL/Analysis/normarith.ML Sun Oct 24 21:59:36 2021 +0200 @@ -16,21 +16,21 @@ open Conv; val bool_eq = op = : bool *bool -> bool fun dest_ratconst t = case Thm.term_of t of - Const(\<^const_name>\divide\, _)$a$b => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd) - | Const(\<^const_name>\inverse\, _)$a => Rat.make(1, HOLogic.dest_number a |> snd) - | _ => Rat.of_int (HOLogic.dest_number (Thm.term_of t) |> snd) + \<^Const_>\divide _ for a b\ => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd) + | \<^Const_>\inverse _ for a\ => Rat.make(1, HOLogic.dest_number a |> snd) + | _ => Rat.of_int (HOLogic.dest_number (Thm.term_of t) |> snd) fun is_ratconst t = can dest_ratconst t fun augment_norm b t acc = case Thm.term_of t of - Const(\<^const_name>\norm\, _) $ _ => insert (eq_pair bool_eq (op aconvc)) (b,Thm.dest_arg t) acc + \<^Const_>\norm _ for _\ => insert (eq_pair bool_eq (op aconvc)) (b,Thm.dest_arg t) acc | _ => acc fun find_normedterms t acc = case Thm.term_of t of - \<^term>\(+) :: real => _\$_$_ => + \<^Const_>\plus \<^typ>\real\ for _ _\ => find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc) - | \<^term>\(*) :: real => _\$_$_ => + | \<^Const_>\times \<^typ>\real\ for _ _\ => if not (is_ratconst (Thm.dest_arg1 t)) then acc else augment_norm (dest_ratconst (Thm.dest_arg1 t) >= @0) (Thm.dest_arg t) acc - | _ => augment_norm true t acc + | _ => augment_norm true t acc val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K ~) fun cterm_lincomb_cmul c t = @@ -51,13 +51,13 @@ *) fun vector_lincomb t = case Thm.term_of t of - Const(\<^const_name>\plus\, _) $ _ $ _ => + \<^Const_>\plus _ for _ _\ => cterm_lincomb_add (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) - | Const(\<^const_name>\minus\, _) $ _ $ _ => + | \<^Const_>\minus _ for _ _\ => cterm_lincomb_sub (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) - | Const(\<^const_name>\scaleR\, _)$_$_ => + | \<^Const_>\scaleR _ for _ _\ => cterm_lincomb_cmul (dest_ratconst (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) - | Const(\<^const_name>\uminus\, _)$_ => + | \<^Const_>\uminus _ for _\ => cterm_lincomb_neg (vector_lincomb (Thm.dest_arg t)) (* FIXME: how should we handle numerals? | Const(@ {const_name vec},_)$_ => @@ -82,8 +82,8 @@ | SOME _ => fns) ts [] fun replacenegnorms cv t = case Thm.term_of t of - \<^term>\(+) :: real => _\$_$_ => binop_conv (replacenegnorms cv) t -| \<^term>\(*) :: real => _\$_$_ => + \<^Const_>\plus \<^typ>\real\ for _ _\ => binop_conv (replacenegnorms cv) t +| \<^Const_>\times \<^typ>\real\ for _ _\ => if dest_ratconst (Thm.dest_arg1 t) < @0 then arg_conv cv t else Thm.reflexive t | _ => Thm.reflexive t (* @@ -148,10 +148,12 @@ fun cterm_of_rat x = let val (a, b) = Rat.dest x in - if b = 1 then Numeral.mk_cnumber \<^ctyp>\real\ a - else Thm.apply (Thm.apply \<^cterm>\(/) :: real => _\ - (Numeral.mk_cnumber \<^ctyp>\real\ a)) - (Numeral.mk_cnumber \<^ctyp>\real\ b) + if b = 1 then Numeral.mk_cnumber \<^ctyp>\real\ a + else + \<^instantiate>\ + a = \Numeral.mk_cnumber \<^ctyp>\real\ a\ and + b = \Numeral.mk_cnumber \<^ctyp>\real\ b\ + in cterm \a / b\ for a b :: real\ end; fun norm_cmul_rule c th = Thm.instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm}); @@ -190,9 +192,8 @@ val apply_pthd = try_conv (rewr_conv @{thm pth_d}); fun headvector t = case t of - Const(\<^const_name>\plus\, _)$ - (Const(\<^const_name>\scaleR\, _)$_$v)$_ => v - | Const(\<^const_name>\scaleR\, _)$_$v => v + \<^Const_>\plus _ for \<^Const_>\scaleR _ for _ v\ _\ => v + | \<^Const_>\scaleR _ for _ v\ => v | _ => error "headvector: non-canonical term" fun vector_cmul_conv ctxt ct = @@ -204,7 +205,7 @@ (apply_pth8 ctxt ct handle CTERM _ => (case Thm.term_of ct of - Const(\<^const_name>\plus\,_)$lt$rt => + \<^Const_>\plus _ for lt rt\ => let val l = headvector lt val r = headvector rt @@ -220,7 +221,7 @@ | _ => Thm.reflexive ct)) fun vector_canon_conv ctxt ct = case Thm.term_of ct of - Const(\<^const_name>\plus\,_)$_$_ => + \<^Const_>\plus _ for _ _\ => let val ((p,l),r) = Thm.dest_comb ct |>> Thm.dest_comb val lth = vector_canon_conv ctxt l @@ -228,16 +229,16 @@ val th = Drule.binop_cong_rule p lth rth in fconv_rule (arg_conv (vector_add_conv ctxt)) th end -| Const(\<^const_name>\scaleR\, _)$_$_ => +| \<^Const_>\scaleR _ for _ _\ => let val (p,r) = Thm.dest_comb ct val rth = Drule.arg_cong_rule p (vector_canon_conv ctxt r) in fconv_rule (arg_conv (apply_pth4 else_conv (vector_cmul_conv ctxt))) rth end -| Const(\<^const_name>\minus\,_)$_$_ => (apply_pth2 then_conv (vector_canon_conv ctxt)) ct +| \<^Const_>\minus _ for _ _\ => (apply_pth2 then_conv (vector_canon_conv ctxt)) ct -| Const(\<^const_name>\uminus\,_)$_ => (apply_pth3 then_conv (vector_canon_conv ctxt)) ct +| \<^Const_>\uminus _ for _\ => (apply_pth3 then_conv (vector_canon_conv ctxt)) ct (* FIXME | Const(@{const_name vec},_)$n => @@ -249,7 +250,7 @@ | _ => apply_pth1 ct fun norm_canon_conv ctxt ct = case Thm.term_of ct of - Const(\<^const_name>\norm\,_)$_ => arg_conv (vector_canon_conv ctxt) ct + \<^Const_>\norm _ for _\ => arg_conv (vector_canon_conv ctxt) ct | _ => raise CTERM ("norm_canon_conv", [ct]) fun int_flip v eq = @@ -345,15 +346,12 @@ val ntms = fold_rev find_normedterms (map (Thm.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 (Thm.instantiate' ty tms) 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 + let val T = Thm.ctyp_of_cterm t + in \<^instantiate>\'a = T and t in cterm \norm 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 + let val T = Thm.ctyp_of_cterm l + in \<^instantiate>\'a = T and l and r in cterm \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))