# HG changeset patch
# User Philipp Meyer
# Date 1254396723 -7200
# Node ID 4602cb6ae0b558d84071f58affb0746aee65be32
# Parent  1352736e57279aee23552393a27c58394b2d1a77
additional fixes in normarith.ML due to FuncFun and FuncUtil changes

diff -r 1352736e5727 -r 4602cb6ae0b5 src/HOL/Library/normarith.ML
--- a/src/HOL/Library/normarith.ML	Thu Oct 01 11:54:01 2009 +0200
+++ b/src/HOL/Library/normarith.ML	Thu Oct 01 13:32:03 2009 +0200
@@ -15,7 +15,7 @@
 structure NormArith : NORM_ARITH = 
 struct
 
- open Conv Thm FuncUtil;
+ open Conv;
  val bool_eq = op = : bool *bool -> bool
   fun dest_ratconst t = case term_of t of
    Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
@@ -23,50 +23,50 @@
  | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
  fun is_ratconst t = can dest_ratconst t
  fun augment_norm b t acc = case term_of t of 
-     Const(@{const_name norm}, _) $ _ => insert (eq_pair bool_eq (op aconvc)) (b,dest_arg t) acc
+     Const(@{const_name norm}, _) $ _ => insert (eq_pair bool_eq (op aconvc)) (b,Thm.dest_arg t) acc
    | _ => acc
  fun find_normedterms t acc = case term_of t of
     @{term "op + :: real => _"}$_$_ =>
-            find_normedterms (dest_arg1 t) (find_normedterms (dest_arg t) acc)
+            find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
       | @{term "op * :: real => _"}$_$n =>
-            if not (is_ratconst (dest_arg1 t)) then acc else
-            augment_norm (dest_ratconst (dest_arg1 t) >=/ Rat.zero) 
-                      (dest_arg t) acc
+            if not (is_ratconst (Thm.dest_arg1 t)) then acc else
+            augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero) 
+                      (Thm.dest_arg t) acc
       | _ => augment_norm true t acc 
 
- val cterm_lincomb_neg = Ctermfunc.mapf Rat.neg
+ val cterm_lincomb_neg = FuncUtil.Ctermfunc.map Rat.neg
  fun cterm_lincomb_cmul c t = 
-    if c =/ Rat.zero then Ctermfunc.undefined else Ctermfunc.mapf (fn x => x */ c) t
- fun cterm_lincomb_add l r = Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
+    if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn x => x */ c) t
+ fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
  fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
- fun cterm_lincomb_eq l r = Ctermfunc.is_undefined (cterm_lincomb_sub l r)
+ fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
 
- val int_lincomb_neg = Intfunc.mapf Rat.neg
+ val int_lincomb_neg = FuncUtil.Intfunc.map Rat.neg
  fun int_lincomb_cmul c t = 
-    if c =/ Rat.zero then Intfunc.undefined else Intfunc.mapf (fn x => x */ c) t
- fun int_lincomb_add l r = Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
+    if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn x => x */ c) t
+ fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
  fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
- fun int_lincomb_eq l r = Intfunc.is_undefined (int_lincomb_sub l r)
+ fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
 
 fun vector_lincomb t = case term_of t of 
    Const(@{const_name plus}, _) $ _ $ _ =>
-    cterm_lincomb_add (vector_lincomb (dest_arg1 t)) (vector_lincomb (dest_arg t))
+    cterm_lincomb_add (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t))
  | Const(@{const_name minus}, _) $ _ $ _ =>
-    cterm_lincomb_sub (vector_lincomb (dest_arg1 t)) (vector_lincomb (dest_arg t))
+    cterm_lincomb_sub (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t))
  | Const(@{const_name scaleR}, _)$_$_ =>
-    cterm_lincomb_cmul (dest_ratconst (dest_arg1 t)) (vector_lincomb (dest_arg t))
+    cterm_lincomb_cmul (dest_ratconst (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t))
  | Const(@{const_name uminus}, _)$_ =>
-     cterm_lincomb_neg (vector_lincomb (dest_arg t))
+     cterm_lincomb_neg (vector_lincomb (Thm.dest_arg t))
 (* FIXME: how should we handle numerals?
  | Const(@ {const_name vec},_)$_ => 
    let 
-     val b = ((snd o HOLogic.dest_number o term_of o dest_arg) t = 0 
+     val b = ((snd o HOLogic.dest_number o term_of o Thm.dest_arg) t = 0 
                handle TERM _=> false)
-   in if b then Ctermfunc.onefunc (t,Rat.one)
-      else Ctermfunc.undefined
+   in if b then FuncUtil.Ctermfunc.onefunc (t,Rat.one)
+      else FuncUtil.Ctermfunc.empty
    end
 *)
- | _ => Ctermfunc.onefunc (t,Rat.one)
+ | _ => FuncUtil.Ctermfunc.onefunc (t,Rat.one)
 
  fun vector_lincombs ts =
   fold_rev 
@@ -82,35 +82,35 @@
 fun replacenegnorms cv t = case term_of t of 
   @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
 | @{term "op * :: real => _"}$_$_ => 
-    if dest_ratconst (dest_arg1 t) </ Rat.zero then arg_conv cv t else reflexive t
+    if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else reflexive t
 | _ => reflexive t
 fun flip v eq = 
-  if Ctermfunc.defined eq v 
-  then Ctermfunc.update (v, Rat.neg (Ctermfunc.apply eq v)) eq else eq
+  if FuncUtil.Ctermfunc.defined eq v 
+  then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq
 fun allsubsets s = case s of 
   [] => [[]]
 |(a::t) => let val res = allsubsets t in
                map (cons a) res @ res end
 fun evaluate env lin =
- Intfunc.fold (fn (x,c) => fn s => s +/ c */ (Intfunc.apply env x)) 
+ FuncUtil.Intfunc.fold (fn (x,c) => fn s => s +/ c */ (FuncUtil.Intfunc.apply env x)) 
    lin Rat.zero
 
 fun solve (vs,eqs) = case (vs,eqs) of
-  ([],[]) => SOME (Intfunc.onefunc (0,Rat.one))
+  ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,Rat.one))
  |(_,eq::oeqs) => 
-   (case filter (member (op =) vs) (Intfunc.dom eq) of (*FIXME use find_first here*)
+   (case filter (member (op =) vs) (FuncUtil.Intfunc.dom eq) of (*FIXME use find_first here*)
      [] => NONE
     | v::_ => 
-       if Intfunc.defined eq v 
+       if FuncUtil.Intfunc.defined eq v 
        then 
         let 
-         val c = Intfunc.apply eq v
+         val c = FuncUtil.Intfunc.apply eq v
          val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq
-         fun eliminate eqn = if not (Intfunc.defined eqn v) then eqn 
-                             else int_lincomb_add (int_lincomb_cmul (Intfunc.apply eqn v) vdef) eqn
+         fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn 
+                             else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn
         in (case solve (vs \ v,map eliminate oeqs) of
             NONE => NONE
-          | SOME soln => SOME (Intfunc.update (v, evaluate soln (Intfunc.undefine v vdef)) soln))
+          | SOME soln => SOME (FuncUtil.Intfunc.update (v, evaluate soln (FuncUtil.Intfunc.delete_safe v vdef)) soln))
         end
        else NONE)
 
@@ -130,7 +130,7 @@
  let 
   fun vertex cmb = case solve(vs,cmb) of
     NONE => NONE
-   | SOME soln => SOME (map (fn v => Intfunc.tryapplyd soln v Rat.zero) vs)
+   | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs)
   val rawvs = map_filter vertex (combinations (length vs) eqs)
   val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs 
  in fold_rev (insert (uncurry (forall2 (curry op =/)))) unset [] 
@@ -265,28 +265,28 @@
  | fold_rev2 f _ _ _ = raise UnequalLengths;
 
 fun int_flip v eq = 
-  if Intfunc.defined eq v 
-  then Intfunc.update (v, Rat.neg (Intfunc.apply eq v)) eq else eq;
+  if FuncUtil.Intfunc.defined eq v 
+  then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq;
 
 local
  val pth_zero = @{thm norm_zero}
- val tv_n = (ctyp_of_term o dest_arg o dest_arg1 o dest_arg o cprop_of)
+ val tv_n = (ctyp_of_term o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o cprop_of)
              pth_zero
- val concl = dest_arg o cprop_of 
+ val concl = Thm.dest_arg o cprop_of 
  fun real_vector_combo_prover ctxt translator (nubs,ges,gts) = 
   let 
    (* FIXME: Should be computed statically!!*)
    val real_poly_conv = 
       Normalizer.semiring_normalize_wrapper ctxt
        (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
-   val sources = map (dest_arg o dest_arg1 o concl) nubs
-   val rawdests = fold_rev (find_normedterms o dest_arg o concl) (ges @ gts) [] 
+   val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs
+   val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) [] 
    val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" 
            else ()
    val dests = distinct (op aconvc) (map snd rawdests)
    val srcfuns = map vector_lincomb sources
    val destfuns = map vector_lincomb dests 
-   val vvs = fold_rev (curry (gen_union op aconvc) o Ctermfunc.dom) (srcfuns @ destfuns) []
+   val vvs = fold_rev (curry (gen_union op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
    val n = length srcfuns
    val nvs = 1 upto n
    val srccombs = srcfuns ~~ nvs
@@ -294,12 +294,12 @@
     let 
      fun coefficients x =
       let 
-       val inp = if Ctermfunc.defined d x then Intfunc.onefunc (0, Rat.neg(Ctermfunc.apply d x))
-                      else Intfunc.undefined 
-      in fold_rev (fn (f,v) => fn g => if Ctermfunc.defined f x then Intfunc.update (v, Ctermfunc.apply f x) g else g) srccombs inp 
+       val inp = if FuncUtil.Ctermfunc.defined d x then FuncUtil.Intfunc.onefunc (0, Rat.neg(FuncUtil.Ctermfunc.apply d x))
+                      else FuncUtil.Intfunc.empty 
+      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 
       end
      val equations = map coefficients vvs
-     val inequalities = map (fn n => Intfunc.onefunc (n,Rat.one)) nvs
+     val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,Rat.one)) nvs
      fun plausiblevertices f =
       let 
        val flippedequations = map (fold_rev int_flip f) equations
@@ -307,7 +307,7 @@
        val rawverts = vertices nvs constraints
        fun check_solution v =
         let 
-          val f = fold_rev2 (curry Intfunc.update) nvs v (Intfunc.onefunc (0, Rat.one))
+          val f = fold_rev2 (curry FuncUtil.Intfunc.update) nvs v (FuncUtil.Intfunc.onefunc (0, Rat.one))
         in forall (fn e => evaluate f e =/ Rat.zero) flippedequations
         end
        val goodverts = filter check_solution rawverts
@@ -328,7 +328,7 @@
    val ges' = map_filter (try compute_ineq) (fold_rev (append o consider) destfuns []) @
                  map (inequality_canon_rule ctxt) nubs @ ges
    val zerodests = filter
-        (fn t => null (Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
+        (fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
 
   in fst (RealArith.real_linear_prover translator
         (map (fn t => instantiate ([(tv_n, ctyp_of_term t)],[]) pth_zero)
@@ -344,19 +344,19 @@
 local
  val pth = @{thm norm_imp_pos_and_ge}
  val norm_mp = match_mp pth
- val concl = dest_arg o cprop_of
+ val concl = Thm.dest_arg o cprop_of
  fun conjunct1 th = th RS @{thm conjunct1}
  fun conjunct2 th = th RS @{thm conjunct2}
  fun C f x y = f y x
 fun real_vector_ineq_prover ctxt translator (ges,gts) = 
  let 
 (*   val _ = error "real_vector_ineq_prover: pause" *)
-  val ntms = fold_rev find_normedterms (map (dest_arg o concl) (ges @ gts)) []
+  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 (Drule.instantiate' ty tms)
-  fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
-  fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
+  fun mk_norm t = Thm.capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
+  fun mk_equals l r = Thm.capply (Thm.capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
   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
   val replace_conv = try_conv (rewrs_conv asl)
   val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))
@@ -368,7 +368,7 @@
   val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts')
   val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1)) 
   val th11 = hd (Variable.export ctxt' ctxt [fold implies_intr shs th1])
-  val cps = map (swap o dest_equals) (cprems_of th11)
+  val cps = map (swap o Thm.dest_equals) (cprems_of th11)
   val th12 = instantiate ([], cps) th11
   val th13 = fold (C implies_elim) (map (reflexive o snd) cps) th12;
  in hd (Variable.export ctxt' ctxt [th13])
@@ -406,7 +406,7 @@
    val ctxt' = Variable.declare_term (term_of ct) ctxt
    val th = init_conv ctxt' ct
   in equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (symmetric th)) 
-                (pure ctxt' (rhs_of th))
+                (pure ctxt' (Thm.rhs_of th))
  end
 
  fun norm_arith_tac ctxt =