src/HOL/Library/normarith.ML
 author haftmann Wed Oct 21 12:02:56 2009 +0200 (2009-10-21) changeset 33042 ddf1f03a9ad9 parent 33039 5018f6a76b3f child 33043 ff71cadefb14 permissions -rw-r--r--
curried union as canonical list operation
 chaieb@31118 ` 1` ```(* Title: Library/normarith.ML ``` chaieb@31118 ` 2` ``` Author: Amine Chaieb, University of Cambridge ``` chaieb@31118 ` 3` ``` Description: A simple decision procedure for linear problems in euclidean space ``` chaieb@31118 ` 4` ```*) ``` chaieb@29841 ` 5` chaieb@29841 ` 6` ``` (* Now the norm procedure for euclidean spaces *) ``` chaieb@29841 ` 7` chaieb@29841 ` 8` chaieb@29841 ` 9` ```signature NORM_ARITH = ``` chaieb@29841 ` 10` ```sig ``` chaieb@29841 ` 11` ``` val norm_arith : Proof.context -> conv ``` chaieb@29841 ` 12` ``` val norm_arith_tac : Proof.context -> int -> tactic ``` chaieb@29841 ` 13` ```end ``` chaieb@29841 ` 14` chaieb@29841 ` 15` ```structure NormArith : NORM_ARITH = ``` chaieb@29841 ` 16` ```struct ``` chaieb@29841 ` 17` Philipp@32832 ` 18` ``` open Conv; ``` chaieb@29841 ` 19` ``` val bool_eq = op = : bool *bool -> bool ``` chaieb@30868 ` 20` ``` fun dest_ratconst t = case term_of t of ``` chaieb@29841 ` 21` ``` Const(@{const_name divide}, _)\$a\$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd) ``` chaieb@30868 ` 22` ``` | Const(@{const_name inverse}, _)\$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd) ``` chaieb@29841 ` 23` ``` | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd) ``` chaieb@29841 ` 24` ``` fun is_ratconst t = can dest_ratconst t ``` chaieb@29841 ` 25` ``` fun augment_norm b t acc = case term_of t of ``` Philipp@32832 ` 26` ``` Const(@{const_name norm}, _) \$ _ => insert (eq_pair bool_eq (op aconvc)) (b,Thm.dest_arg t) acc ``` chaieb@29841 ` 27` ``` | _ => acc ``` chaieb@29841 ` 28` ``` fun find_normedterms t acc = case term_of t of ``` chaieb@29841 ` 29` ``` @{term "op + :: real => _"}\$_\$_ => ``` Philipp@32832 ` 30` ``` find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc) ``` chaieb@29841 ` 31` ``` | @{term "op * :: real => _"}\$_\$n => ``` Philipp@32832 ` 32` ``` if not (is_ratconst (Thm.dest_arg1 t)) then acc else ``` Philipp@32832 ` 33` ``` augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero) ``` Philipp@32832 ` 34` ``` (Thm.dest_arg t) acc ``` chaieb@29841 ` 35` ``` | _ => augment_norm true t acc ``` chaieb@29841 ` 36` Philipp@32832 ` 37` ``` val cterm_lincomb_neg = FuncUtil.Ctermfunc.map Rat.neg ``` chaieb@29841 ` 38` ``` fun cterm_lincomb_cmul c t = ``` Philipp@32832 ` 39` ``` if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn x => x */ c) t ``` Philipp@32832 ` 40` ``` fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r ``` chaieb@29841 ` 41` ``` fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r) ``` Philipp@32832 ` 42` ``` fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r) ``` chaieb@29841 ` 43` Philipp@32832 ` 44` ``` val int_lincomb_neg = FuncUtil.Intfunc.map Rat.neg ``` chaieb@29841 ` 45` ``` fun int_lincomb_cmul c t = ``` Philipp@32832 ` 46` ``` if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn x => x */ c) t ``` Philipp@32832 ` 47` ``` fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r ``` chaieb@29841 ` 48` ``` fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r) ``` Philipp@32832 ` 49` ``` fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r) ``` chaieb@29841 ` 50` chaieb@29841 ` 51` ```fun vector_lincomb t = case term_of t of ``` huffman@31445 ` 52` ``` Const(@{const_name plus}, _) \$ _ \$ _ => ``` Philipp@32832 ` 53` ``` cterm_lincomb_add (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) ``` huffman@31445 ` 54` ``` | Const(@{const_name minus}, _) \$ _ \$ _ => ``` Philipp@32832 ` 55` ``` cterm_lincomb_sub (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) ``` huffman@31445 ` 56` ``` | Const(@{const_name scaleR}, _)\$_\$_ => ``` Philipp@32832 ` 57` ``` cterm_lincomb_cmul (dest_ratconst (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) ``` huffman@31445 ` 58` ``` | Const(@{const_name uminus}, _)\$_ => ``` Philipp@32832 ` 59` ``` cterm_lincomb_neg (vector_lincomb (Thm.dest_arg t)) ``` huffman@31445 ` 60` ```(* FIXME: how should we handle numerals? ``` huffman@31445 ` 61` ``` | Const(@ {const_name vec},_)\$_ => ``` chaieb@29841 ` 62` ``` let ``` Philipp@32832 ` 63` ``` val b = ((snd o HOLogic.dest_number o term_of o Thm.dest_arg) t = 0 ``` chaieb@29841 ` 64` ``` handle TERM _=> false) ``` Philipp@32832 ` 65` ``` in if b then FuncUtil.Ctermfunc.onefunc (t,Rat.one) ``` Philipp@32832 ` 66` ``` else FuncUtil.Ctermfunc.empty ``` chaieb@29841 ` 67` ``` end ``` huffman@31445 ` 68` ```*) ``` Philipp@32832 ` 69` ``` | _ => FuncUtil.Ctermfunc.onefunc (t,Rat.one) ``` chaieb@29841 ` 70` chaieb@29841 ` 71` ``` fun vector_lincombs ts = ``` chaieb@29841 ` 72` ``` fold_rev ``` chaieb@29841 ` 73` ``` (fn t => fn fns => case AList.lookup (op aconvc) fns t of ``` chaieb@29841 ` 74` ``` NONE => ``` chaieb@29841 ` 75` ``` let val f = vector_lincomb t ``` chaieb@29841 ` 76` ``` in case find_first (fn (_,f') => cterm_lincomb_eq f f') fns of ``` chaieb@29841 ` 77` ``` SOME (_,f') => (t,f') :: fns ``` chaieb@29841 ` 78` ``` | NONE => (t,f) :: fns ``` chaieb@29841 ` 79` ``` end ``` chaieb@29841 ` 80` ``` | SOME _ => fns) ts [] ``` chaieb@29841 ` 81` chaieb@29841 ` 82` ```fun replacenegnorms cv t = case term_of t of ``` chaieb@29841 ` 83` ``` @{term "op + :: real => _"}\$_\$_ => binop_conv (replacenegnorms cv) t ``` chaieb@29841 ` 84` ```| @{term "op * :: real => _"}\$_\$_ => ``` Philipp@32832 ` 85` ``` if dest_ratconst (Thm.dest_arg1 t) reflexive t ``` chaieb@29841 ` 87` ```fun flip v eq = ``` Philipp@32832 ` 88` ``` if FuncUtil.Ctermfunc.defined eq v ``` Philipp@32832 ` 89` ``` then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq ``` chaieb@29841 ` 90` ```fun allsubsets s = case s of ``` chaieb@29841 ` 91` ``` [] => [[]] ``` chaieb@29841 ` 92` ```|(a::t) => let val res = allsubsets t in ``` chaieb@29841 ` 93` ``` map (cons a) res @ res end ``` chaieb@29841 ` 94` ```fun evaluate env lin = ``` Philipp@32832 ` 95` ``` FuncUtil.Intfunc.fold (fn (x,c) => fn s => s +/ c */ (FuncUtil.Intfunc.apply env x)) ``` chaieb@29841 ` 96` ``` lin Rat.zero ``` chaieb@29841 ` 97` chaieb@29841 ` 98` ```fun solve (vs,eqs) = case (vs,eqs) of ``` Philipp@32832 ` 99` ``` ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,Rat.one)) ``` chaieb@29841 ` 100` ``` |(_,eq::oeqs) => ``` Philipp@32832 ` 101` ``` (case filter (member (op =) vs) (FuncUtil.Intfunc.dom eq) of (*FIXME use find_first here*) ``` chaieb@29841 ` 102` ``` [] => NONE ``` chaieb@29841 ` 103` ``` | v::_ => ``` Philipp@32832 ` 104` ``` if FuncUtil.Intfunc.defined eq v ``` chaieb@29841 ` 105` ``` then ``` chaieb@29841 ` 106` ``` let ``` Philipp@32832 ` 107` ``` val c = FuncUtil.Intfunc.apply eq v ``` chaieb@29841 ` 108` ``` val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq ``` Philipp@32832 ` 109` ``` fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn ``` Philipp@32832 ` 110` ``` else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn ``` chaieb@29841 ` 111` ``` in (case solve (vs \ v,map eliminate oeqs) of ``` chaieb@29841 ` 112` ``` NONE => NONE ``` Philipp@32832 ` 113` ``` | SOME soln => SOME (FuncUtil.Intfunc.update (v, evaluate soln (FuncUtil.Intfunc.delete_safe v vdef)) soln)) ``` chaieb@29841 ` 114` ``` end ``` chaieb@29841 ` 115` ``` else NONE) ``` chaieb@29841 ` 116` chaieb@29841 ` 117` ```fun combinations k l = if k = 0 then [[]] else ``` chaieb@29841 ` 118` ``` case l of ``` chaieb@29841 ` 119` ``` [] => [] ``` chaieb@29841 ` 120` ```| h::t => map (cons h) (combinations (k - 1) t) @ combinations k t ``` chaieb@29841 ` 121` chaieb@29841 ` 122` chaieb@29841 ` 123` ```fun forall2 p l1 l2 = case (l1,l2) of ``` chaieb@29841 ` 124` ``` ([],[]) => true ``` chaieb@29841 ` 125` ``` | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2 ``` chaieb@29841 ` 126` ``` | _ => false; ``` chaieb@29841 ` 127` chaieb@29841 ` 128` chaieb@29841 ` 129` ```fun vertices vs eqs = ``` chaieb@29841 ` 130` ``` let ``` chaieb@29841 ` 131` ``` fun vertex cmb = case solve(vs,cmb) of ``` chaieb@29841 ` 132` ``` NONE => NONE ``` Philipp@32832 ` 133` ``` | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs) ``` chaieb@29841 ` 134` ``` val rawvs = map_filter vertex (combinations (length vs) eqs) ``` chaieb@29841 ` 135` ``` val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs ``` chaieb@29841 ` 136` ``` in fold_rev (insert (uncurry (forall2 (curry op =/)))) unset [] ``` chaieb@29841 ` 137` ``` end ``` chaieb@29841 ` 138` chaieb@29841 ` 139` ```fun subsumes l m = forall2 (fn x => fn y => Rat.abs x <=/ Rat.abs y) l m ``` chaieb@29841 ` 140` chaieb@29841 ` 141` ```fun subsume todo dun = case todo of ``` chaieb@29841 ` 142` ``` [] => dun ``` chaieb@29841 ` 143` ```|v::ovs => ``` chaieb@29841 ` 144` ``` let val dun' = if exists (fn w => subsumes w v) dun then dun ``` chaieb@29841 ` 145` ``` else v::(filter (fn w => not(subsumes v w)) dun) ``` chaieb@29841 ` 146` ``` in subsume ovs dun' ``` chaieb@29841 ` 147` ``` end; ``` chaieb@29841 ` 148` chaieb@29841 ` 149` ```fun match_mp PQ P = P RS PQ; ``` chaieb@29841 ` 150` chaieb@29841 ` 151` ```fun cterm_of_rat x = ``` chaieb@29841 ` 152` ```let val (a, b) = Rat.quotient_of_rat x ``` chaieb@29841 ` 153` ```in ``` chaieb@29841 ` 154` ``` if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a ``` chaieb@29841 ` 155` ``` else Thm.capply (Thm.capply @{cterm "op / :: real => _"} ``` chaieb@29841 ` 156` ``` (Numeral.mk_cnumber @{ctyp "real"} a)) ``` chaieb@29841 ` 157` ``` (Numeral.mk_cnumber @{ctyp "real"} b) ``` chaieb@29841 ` 158` ```end; ``` chaieb@29841 ` 159` chaieb@29841 ` 160` ```fun norm_cmul_rule c th = instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm}); ``` chaieb@29841 ` 161` chaieb@29841 ` 162` ```fun norm_add_rule th1 th2 = [th1, th2] MRS @{thm norm_add_rule_thm}; ``` chaieb@29841 ` 163` chaieb@29841 ` 164` ``` (* I think here the static context should be sufficient!! *) ``` chaieb@29841 ` 165` ```fun inequality_canon_rule ctxt = ``` chaieb@29841 ` 166` ``` let ``` chaieb@29841 ` 167` ``` (* FIXME : Should be computed statically!! *) ``` chaieb@29841 ` 168` ``` val real_poly_conv = ``` chaieb@29841 ` 169` ``` Normalizer.semiring_normalize_wrapper ctxt ``` wenzelm@33035 ` 170` ``` (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) ``` chaieb@29841 ` 171` ``` in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (field_comp_conv then_conv real_poly_conv))) ``` chaieb@29841 ` 172` ```end; ``` chaieb@29841 ` 173` chaieb@29841 ` 174` ``` fun absc cv ct = case term_of ct of ``` chaieb@29841 ` 175` ``` Abs (v,_, _) => ``` chaieb@29841 ` 176` ``` let val (x,t) = Thm.dest_abs (SOME v) ct ``` chaieb@29841 ` 177` ``` in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t) ``` chaieb@29841 ` 178` ``` end ``` chaieb@29841 ` 179` ``` | _ => all_conv ct; ``` chaieb@29841 ` 180` chaieb@29841 ` 181` ```fun sub_conv cv ct = (comb_conv cv else_conv absc cv) ct; ``` chaieb@29841 ` 182` ```fun botc1 conv ct = ``` chaieb@29841 ` 183` ``` ((sub_conv (botc1 conv)) then_conv (conv else_conv all_conv)) ct; ``` chaieb@29841 ` 184` chaieb@29841 ` 185` ``` fun rewrs_conv eqs ct = first_conv (map rewr_conv eqs) ct; ``` chaieb@29841 ` 186` ``` val apply_pth1 = rewr_conv @{thm pth_1}; ``` chaieb@29841 ` 187` ``` val apply_pth2 = rewr_conv @{thm pth_2}; ``` chaieb@29841 ` 188` ``` val apply_pth3 = rewr_conv @{thm pth_3}; ``` chaieb@29841 ` 189` ``` val apply_pth4 = rewrs_conv @{thms pth_4}; ``` chaieb@29841 ` 190` ``` val apply_pth5 = rewr_conv @{thm pth_5}; ``` chaieb@29841 ` 191` ``` val apply_pth6 = rewr_conv @{thm pth_6}; ``` chaieb@29841 ` 192` ``` val apply_pth7 = rewrs_conv @{thms pth_7}; ``` huffman@31445 ` 193` ``` val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left}))); ``` chaieb@29841 ` 194` ``` val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv field_comp_conv); ``` chaieb@29841 ` 195` ``` val apply_ptha = rewr_conv @{thm pth_a}; ``` chaieb@29841 ` 196` ``` val apply_pthb = rewrs_conv @{thms pth_b}; ``` chaieb@29841 ` 197` ``` val apply_pthc = rewrs_conv @{thms pth_c}; ``` chaieb@29841 ` 198` ``` val apply_pthd = try_conv (rewr_conv @{thm pth_d}); ``` chaieb@29841 ` 199` chaieb@29841 ` 200` ```fun headvector t = case t of ``` huffman@31445 ` 201` ``` Const(@{const_name plus}, _)\$ ``` huffman@31445 ` 202` ``` (Const(@{const_name scaleR}, _)\$l\$v)\$r => v ``` huffman@31445 ` 203` ``` | Const(@{const_name scaleR}, _)\$l\$v => v ``` chaieb@29841 ` 204` ``` | _ => error "headvector: non-canonical term" ``` chaieb@29841 ` 205` chaieb@29841 ` 206` ```fun vector_cmul_conv ct = ``` chaieb@29841 ` 207` ``` ((apply_pth5 then_conv arg1_conv field_comp_conv) else_conv ``` chaieb@29841 ` 208` ``` (apply_pth6 then_conv binop_conv vector_cmul_conv)) ct ``` chaieb@29841 ` 209` chaieb@29841 ` 210` ```fun vector_add_conv ct = apply_pth7 ct ``` chaieb@29841 ` 211` ``` handle CTERM _ => ``` chaieb@29841 ` 212` ``` (apply_pth8 ct ``` chaieb@29841 ` 213` ``` handle CTERM _ => ``` chaieb@29841 ` 214` ``` (case term_of ct of ``` chaieb@29841 ` 215` ``` Const(@{const_name plus},_)\$lt\$rt => ``` chaieb@29841 ` 216` ``` let ``` chaieb@29841 ` 217` ``` val l = headvector lt ``` chaieb@29841 ` 218` ``` val r = headvector rt ``` chaieb@29841 ` 219` ``` in (case TermOrd.fast_term_ord (l,r) of ``` chaieb@29841 ` 220` ``` LESS => (apply_pthb then_conv arg_conv vector_add_conv ``` chaieb@29841 ` 221` ``` then_conv apply_pthd) ct ``` chaieb@29841 ` 222` ``` | GREATER => (apply_pthc then_conv arg_conv vector_add_conv ``` chaieb@29841 ` 223` ``` then_conv apply_pthd) ct ``` chaieb@29841 ` 224` ``` | EQUAL => (apply_pth9 then_conv ``` chaieb@29841 ` 225` ``` ((apply_ptha then_conv vector_add_conv) else_conv ``` chaieb@29841 ` 226` ``` arg_conv vector_add_conv then_conv apply_pthd)) ct) ``` chaieb@29841 ` 227` ``` end ``` chaieb@29841 ` 228` ``` | _ => reflexive ct)) ``` chaieb@29841 ` 229` chaieb@29841 ` 230` ```fun vector_canon_conv ct = case term_of ct of ``` chaieb@29841 ` 231` ``` Const(@{const_name plus},_)\$_\$_ => ``` chaieb@29841 ` 232` ``` let ``` chaieb@29841 ` 233` ``` val ((p,l),r) = Thm.dest_comb ct |>> Thm.dest_comb ``` chaieb@29841 ` 234` ``` val lth = vector_canon_conv l ``` chaieb@29841 ` 235` ``` val rth = vector_canon_conv r ``` chaieb@29841 ` 236` ``` val th = Drule.binop_cong_rule p lth rth ``` chaieb@29841 ` 237` ``` in fconv_rule (arg_conv vector_add_conv) th end ``` chaieb@29841 ` 238` huffman@31445 ` 239` ```| Const(@{const_name scaleR}, _)\$_\$_ => ``` chaieb@29841 ` 240` ``` let ``` chaieb@29841 ` 241` ``` val (p,r) = Thm.dest_comb ct ``` chaieb@29841 ` 242` ``` val rth = Drule.arg_cong_rule p (vector_canon_conv r) ``` chaieb@29841 ` 243` ``` in fconv_rule (arg_conv (apply_pth4 else_conv vector_cmul_conv)) rth ``` chaieb@29841 ` 244` ``` end ``` chaieb@29841 ` 245` chaieb@29841 ` 246` ```| Const(@{const_name minus},_)\$_\$_ => (apply_pth2 then_conv vector_canon_conv) ct ``` chaieb@29841 ` 247` chaieb@29841 ` 248` ```| Const(@{const_name uminus},_)\$_ => (apply_pth3 then_conv vector_canon_conv) ct ``` chaieb@29841 ` 249` huffman@31445 ` 250` ```(* FIXME ``` chaieb@29841 ` 251` ```| Const(@{const_name vec},_)\$n => ``` chaieb@29841 ` 252` ``` let val n = Thm.dest_arg ct ``` chaieb@29841 ` 253` ``` in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero) ``` chaieb@29841 ` 254` ``` then reflexive ct else apply_pth1 ct ``` chaieb@29841 ` 255` ``` end ``` huffman@31445 ` 256` ```*) ``` chaieb@29841 ` 257` ```| _ => apply_pth1 ct ``` chaieb@29841 ` 258` chaieb@29841 ` 259` ```fun norm_canon_conv ct = case term_of ct of ``` chaieb@29841 ` 260` ``` Const(@{const_name norm},_)\$_ => arg_conv vector_canon_conv ct ``` chaieb@29841 ` 261` ``` | _ => raise CTERM ("norm_canon_conv", [ct]) ``` chaieb@29841 ` 262` chaieb@29841 ` 263` ```fun fold_rev2 f [] [] z = z ``` chaieb@29841 ` 264` ``` | fold_rev2 f (x::xs) (y::ys) z = f x y (fold_rev2 f xs ys z) ``` chaieb@29841 ` 265` ``` | fold_rev2 f _ _ _ = raise UnequalLengths; ``` chaieb@29841 ` 266` chaieb@29841 ` 267` ```fun int_flip v eq = ``` Philipp@32832 ` 268` ``` if FuncUtil.Intfunc.defined eq v ``` Philipp@32832 ` 269` ``` then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq; ``` chaieb@29841 ` 270` chaieb@29841 ` 271` ```local ``` huffman@31445 ` 272` ``` val pth_zero = @{thm norm_zero} ``` Philipp@32832 ` 273` ``` val tv_n = (ctyp_of_term o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o cprop_of) ``` chaieb@29841 ` 274` ``` pth_zero ``` Philipp@32832 ` 275` ``` val concl = Thm.dest_arg o cprop_of ``` chaieb@29841 ` 276` ``` fun real_vector_combo_prover ctxt translator (nubs,ges,gts) = ``` chaieb@29841 ` 277` ``` let ``` chaieb@29841 ` 278` ``` (* FIXME: Should be computed statically!!*) ``` chaieb@29841 ` 279` ``` val real_poly_conv = ``` chaieb@29841 ` 280` ``` Normalizer.semiring_normalize_wrapper ctxt ``` wenzelm@33035 ` 281` ``` (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) ``` Philipp@32832 ` 282` ``` val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs ``` Philipp@32832 ` 283` ``` val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) [] ``` chaieb@29841 ` 284` ``` val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" ``` chaieb@29841 ` 285` ``` else () ``` chaieb@29841 ` 286` ``` val dests = distinct (op aconvc) (map snd rawdests) ``` chaieb@29841 ` 287` ``` val srcfuns = map vector_lincomb sources ``` chaieb@29841 ` 288` ``` val destfuns = map vector_lincomb dests ``` haftmann@33042 ` 289` ``` val vvs = fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) [] ``` chaieb@29841 ` 290` ``` val n = length srcfuns ``` chaieb@29841 ` 291` ``` val nvs = 1 upto n ``` chaieb@29841 ` 292` ``` val srccombs = srcfuns ~~ nvs ``` chaieb@29841 ` 293` ``` fun consider d = ``` chaieb@29841 ` 294` ``` let ``` chaieb@29841 ` 295` ``` fun coefficients x = ``` chaieb@29841 ` 296` ``` let ``` Philipp@32832 ` 297` ``` val inp = if FuncUtil.Ctermfunc.defined d x then FuncUtil.Intfunc.onefunc (0, Rat.neg(FuncUtil.Ctermfunc.apply d x)) ``` Philipp@32832 ` 298` ``` else FuncUtil.Intfunc.empty ``` Philipp@32832 ` 299` ``` in fold_rev (fn (f,v) => fn g => if FuncUtil.Ctermfunc.defined f x then FuncUtil.Intfunc.update (v, FuncUtil.Ctermfunc.apply f x) g else g) srccombs inp ``` chaieb@29841 ` 300` ``` end ``` chaieb@29841 ` 301` ``` val equations = map coefficients vvs ``` Philipp@32832 ` 302` ``` val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,Rat.one)) nvs ``` chaieb@29841 ` 303` ``` fun plausiblevertices f = ``` chaieb@29841 ` 304` ``` let ``` chaieb@29841 ` 305` ``` val flippedequations = map (fold_rev int_flip f) equations ``` chaieb@29841 ` 306` ``` val constraints = flippedequations @ inequalities ``` chaieb@29841 ` 307` ``` val rawverts = vertices nvs constraints ``` chaieb@29841 ` 308` ``` fun check_solution v = ``` chaieb@29841 ` 309` ``` let ``` Philipp@32832 ` 310` ``` val f = fold_rev2 (curry FuncUtil.Intfunc.update) nvs v (FuncUtil.Intfunc.onefunc (0, Rat.one)) ``` chaieb@29841 ` 311` ``` in forall (fn e => evaluate f e =/ Rat.zero) flippedequations ``` chaieb@29841 ` 312` ``` end ``` chaieb@29841 ` 313` ``` val goodverts = filter check_solution rawverts ``` chaieb@29841 ` 314` ``` val signfixups = map (fn n => if n mem_int f then ~1 else 1) nvs ``` chaieb@29841 ` 315` ``` in map (map2 (fn s => fn c => Rat.rat_of_int s */ c) signfixups) goodverts ``` chaieb@29841 ` 316` ``` end ``` chaieb@29841 ` 317` ``` val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) [] ``` chaieb@29841 ` 318` ``` in subsume allverts [] ``` chaieb@29841 ` 319` ``` end ``` chaieb@29841 ` 320` ``` fun compute_ineq v = ``` chaieb@29841 ` 321` ``` let ``` chaieb@29841 ` 322` ``` val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE ``` chaieb@29841 ` 323` ``` else SOME(norm_cmul_rule v t)) ``` chaieb@29841 ` 324` ``` (v ~~ nubs) ``` boehmes@32402 ` 325` ``` fun end_itlist f xs = split_last xs |> uncurry (fold_rev f) ``` chaieb@29841 ` 326` ``` in inequality_canon_rule ctxt (end_itlist norm_add_rule ths) ``` chaieb@29841 ` 327` ``` end ``` chaieb@29841 ` 328` ``` val ges' = map_filter (try compute_ineq) (fold_rev (append o consider) destfuns []) @ ``` chaieb@29841 ` 329` ``` map (inequality_canon_rule ctxt) nubs @ ges ``` chaieb@29841 ` 330` ``` val zerodests = filter ``` Philipp@32832 ` 331` ``` (fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests) ``` chaieb@29841 ` 332` Philipp@32645 ` 333` ``` in fst (RealArith.real_linear_prover translator ``` huffman@31445 ` 334` ``` (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero) ``` chaieb@29841 ` 335` ``` zerodests, ``` boehmes@32402 ` 336` ``` map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv ``` chaieb@29841 ` 337` ``` arg_conv (arg_conv real_poly_conv))) ges', ``` boehmes@32402 ` 338` ``` map (fconv_rule (try_conv (More_Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv ``` Philipp@32645 ` 339` ``` arg_conv (arg_conv real_poly_conv))) gts)) ``` chaieb@29841 ` 340` ``` end ``` chaieb@29841 ` 341` ```in val real_vector_combo_prover = real_vector_combo_prover ``` chaieb@29841 ` 342` ```end; ``` chaieb@29841 ` 343` chaieb@29841 ` 344` ```local ``` chaieb@29841 ` 345` ``` val pth = @{thm norm_imp_pos_and_ge} ``` chaieb@29841 ` 346` ``` val norm_mp = match_mp pth ``` Philipp@32832 ` 347` ``` val concl = Thm.dest_arg o cprop_of ``` chaieb@29841 ` 348` ``` fun conjunct1 th = th RS @{thm conjunct1} ``` chaieb@29841 ` 349` ``` fun conjunct2 th = th RS @{thm conjunct2} ``` chaieb@29841 ` 350` ```fun real_vector_ineq_prover ctxt translator (ges,gts) = ``` chaieb@29841 ` 351` ``` let ``` chaieb@29841 ` 352` ```(* val _ = error "real_vector_ineq_prover: pause" *) ``` Philipp@32832 ` 353` ``` val ntms = fold_rev find_normedterms (map (Thm.dest_arg o concl) (ges @ gts)) [] ``` chaieb@29841 ` 354` ``` val lctab = vector_lincombs (map snd (filter (not o fst) ntms)) ``` chaieb@29841 ` 355` ``` val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt ``` boehmes@32402 ` 356` ``` fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) ``` Philipp@32832 ` 357` ``` fun mk_norm t = Thm.capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t ``` Philipp@32832 ` 358` ``` fun mk_equals l r = Thm.capply (Thm.capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r ``` chaieb@29841 ` 359` ``` val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns ``` chaieb@29841 ` 360` ``` val replace_conv = try_conv (rewrs_conv asl) ``` chaieb@29841 ` 361` ``` val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv)) ``` chaieb@29841 ` 362` ``` val ges' = ``` chaieb@29841 ` 363` ``` fold_rev (fn th => fn ths => conjunct1(norm_mp th)::ths) ``` chaieb@29841 ` 364` ``` asl (map replace_rule ges) ``` chaieb@29841 ` 365` ``` val gts' = map replace_rule gts ``` chaieb@29841 ` 366` ``` val nubs = map (conjunct2 o norm_mp) asl ``` chaieb@29841 ` 367` ``` val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts') ``` chaieb@29841 ` 368` ``` val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1)) ``` chaieb@29841 ` 369` ``` val th11 = hd (Variable.export ctxt' ctxt [fold implies_intr shs th1]) ``` Philipp@32832 ` 370` ``` val cps = map (swap o Thm.dest_equals) (cprems_of th11) ``` chaieb@29841 ` 371` ``` val th12 = instantiate ([], cps) th11 ``` wenzelm@32934 ` 372` ``` val th13 = fold Thm.elim_implies (map (reflexive o snd) cps) th12; ``` chaieb@29841 ` 373` ``` in hd (Variable.export ctxt' ctxt [th13]) ``` chaieb@29841 ` 374` ``` end ``` chaieb@29841 ` 375` ```in val real_vector_ineq_prover = real_vector_ineq_prover ``` chaieb@29841 ` 376` ```end; ``` chaieb@29841 ` 377` chaieb@29841 ` 378` ```local ``` chaieb@29841 ` 379` ``` val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0})) ``` chaieb@29841 ` 380` ``` fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2}) ``` chaieb@29841 ` 381` ``` fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS; ``` chaieb@29841 ` 382` ``` (* FIXME: Lookup in the context every time!!! Fix this !!!*) ``` chaieb@29841 ` 383` ``` fun splitequation ctxt th acc = ``` chaieb@29841 ` 384` ``` let ``` chaieb@29841 ` 385` ``` val real_poly_neg_conv = #neg ``` chaieb@29841 ` 386` ``` (Normalizer.semiring_normalizers_ord_wrapper ctxt ``` wenzelm@33035 ` 387` ``` (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord) ``` chaieb@29841 ` 388` ``` val (th1,th2) = conj_pair(rawrule th) ``` chaieb@29841 ` 389` ``` in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc ``` chaieb@29841 ` 390` ``` end ``` Philipp@32645 ` 391` ```in fun real_vector_prover ctxt _ translator (eqs,ges,gts) = ``` Philipp@32645 ` 392` ``` (real_vector_ineq_prover ctxt translator ``` Philipp@32645 ` 393` ``` (fold_rev (splitequation ctxt) eqs ges,gts), RealArith.Trivial) ``` chaieb@29841 ` 394` ```end; ``` chaieb@29841 ` 395` chaieb@29841 ` 396` ``` fun init_conv ctxt = ``` chaieb@29841 ` 397` ``` Simplifier.rewrite (Simplifier.context ctxt ``` huffman@31445 ` 398` ``` (HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm vector_dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) ``` chaieb@29841 ` 399` ``` then_conv field_comp_conv ``` chaieb@29841 ` 400` ``` then_conv nnf_conv ``` chaieb@29841 ` 401` Philipp@32645 ` 402` ``` fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt); ``` chaieb@29841 ` 403` ``` fun norm_arith ctxt ct = ``` chaieb@29841 ` 404` ``` let ``` chaieb@29841 ` 405` ``` val ctxt' = Variable.declare_term (term_of ct) ctxt ``` chaieb@29841 ` 406` ``` val th = init_conv ctxt' ct ``` chaieb@29841 ` 407` ``` in equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (symmetric th)) ``` Philipp@32832 ` 408` ``` (pure ctxt' (Thm.rhs_of th)) ``` chaieb@29841 ` 409` ``` end ``` chaieb@29841 ` 410` chaieb@29841 ` 411` ``` fun norm_arith_tac ctxt = ``` chaieb@29841 ` 412` ``` clarify_tac HOL_cs THEN' ``` chaieb@29841 ` 413` ``` ObjectLogic.full_atomize_tac THEN' ``` chaieb@29841 ` 414` ``` CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i); ``` chaieb@29841 ` 415` huffman@31445 ` 416` ```end; ```