equal
deleted
inserted
replaced
329 val lctab = vector_lincombs (map snd (filter (not o fst) ntms)) |
329 val lctab = vector_lincombs (map snd (filter (not o fst) ntms)) |
330 val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt |
330 val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt |
331 fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) |
331 fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) |
332 fun mk_norm t = Thm.capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t |
332 fun mk_norm t = Thm.capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t |
333 fun mk_equals l r = Thm.capply (Thm.capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r |
333 fun mk_equals l r = Thm.capply (Thm.capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r |
334 val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns |
334 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 |
335 val replace_conv = try_conv (rewrs_conv asl) |
335 val replace_conv = try_conv (rewrs_conv asl) |
336 val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv)) |
336 val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv)) |
337 val ges' = |
337 val ges' = |
338 fold_rev (fn th => fn ths => conjunct1(norm_mp th)::ths) |
338 fold_rev (fn th => fn ths => conjunct1(norm_mp th)::ths) |
339 asl (map replace_rule ges) |
339 asl (map replace_rule ges) |