147 |
147 |
148 fun cterm_of_rat x = |
148 fun cterm_of_rat x = |
149 let val (a, b) = Rat.quotient_of_rat x |
149 let val (a, b) = Rat.quotient_of_rat x |
150 in |
150 in |
151 if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a |
151 if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a |
152 else Thm.capply (Thm.capply @{cterm "op / :: real => _"} |
152 else Thm.apply (Thm.apply @{cterm "op / :: real => _"} |
153 (Numeral.mk_cnumber @{ctyp "real"} a)) |
153 (Numeral.mk_cnumber @{ctyp "real"} a)) |
154 (Numeral.mk_cnumber @{ctyp "real"} b) |
154 (Numeral.mk_cnumber @{ctyp "real"} b) |
155 end; |
155 end; |
156 |
156 |
157 fun norm_cmul_rule c th = instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm}); |
157 fun norm_cmul_rule c th = instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm}); |
333 (* val _ = error "real_vector_ineq_prover: pause" *) |
333 (* val _ = error "real_vector_ineq_prover: pause" *) |
334 val ntms = fold_rev find_normedterms (map (Thm.dest_arg o concl) (ges @ gts)) [] |
334 val ntms = fold_rev find_normedterms (map (Thm.dest_arg o concl) (ges @ gts)) [] |
335 val lctab = vector_lincombs (map snd (filter (not o fst) ntms)) |
335 val lctab = vector_lincombs (map snd (filter (not o fst) ntms)) |
336 val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt |
336 val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt |
337 fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) |
337 fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) |
338 fun mk_norm t = Thm.capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t |
338 fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t |
339 fun mk_equals l r = Thm.capply (Thm.capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r |
339 fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r |
340 val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (cterm_of (Proof_Context.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns |
340 val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (cterm_of (Proof_Context.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns |
341 val replace_conv = try_conv (rewrs_conv asl) |
341 val replace_conv = try_conv (rewrs_conv asl) |
342 val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv)) |
342 val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv)) |
343 val ges' = |
343 val ges' = |
344 fold_rev (fn th => fn ths => conjunct1(norm_mp th)::ths) |
344 fold_rev (fn th => fn ths => conjunct1(norm_mp th)::ths) |