src/HOL/Library/size_change_termination.ML

       measures
     end
 
 
 
-val mk_number = HOLogic.mk_nat
-val dest_number = HOLogic.dest_nat
+val mk_number = HOLogic.mk_nat o IntInf.fromInt
+val dest_number = IntInf.toInt o HOLogic.dest_nat
 
 fun nums_to i = map mk_number (0 upto (i - 1))
 
 
 fun unfold_then_auto thm = 

       |> cterm_of thy 
       |> try_to_prove (unfold_then_auto decreq_def)
       |> simple_result
 
 
-fun pr_tac (st : thm) = Seq.single (Output.warning (PolyML.makestring st); st)
-fun pr_thm (st : thm) = (Output.warning (PolyML.makestring st); st)
-
-
 fun build_approximating_graph thy Dtab Mtab Mss mlens mint nint =
     let 
       val D1 = Dtab mint and D2 = Dtab nint
       val Mst1 = Mtab mint and Mst2 = Mtab nint
 

     in
       tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st)
     end
                   
 
-
-
-
-
-
-
-
-
-
-
-(* Faster implementation of transitive closures *)
-
-(* sedge: Only relevant edges. Qtrees have separate value for 0 *)
-datatype sedge = LESS | LEQ | BOTH
-
-
-
-datatype key = KHere | K0 of key | K1 of key
-
-datatype 'a stree = 
-  sLeaf of 'a
-  | sBranch of ('a * 'a stree * 'a stree)
-
-(*
-fun lookup (sLeaf x) KHere = x
-  | lookup (sBranch x s t) KHere = x
-  | lookup (sBranch x s t) (K0 k) = lookup s k
-  | lookup (sBranch x s t) (K1 k) = lookup t k
-  | lookup _ _ = raise Match
-*)
-
-datatype 'a qtree =
-  QEmpty
-  | QNode of 'a
-  | QQuad of ('a qtree * 'a qtree * 'a qtree * 'a qtree)
-
-fun qlookup z QEmpty k l = z
-  | qlookup z (QNode S) k l = S
-  | qlookup z (QQuad (a, b, c, d)) (K0 k) (K0 l) = qlookup z a k l
-  | qlookup z (QQuad (a, b, c, d)) (K0 k) (K1 l) = qlookup z b k l
-  | qlookup z (QQuad (a, b, c, d)) (K1 k) (K0 l) = qlookup z c k l
-  | qlookup z (QQuad (a, b, c, d)) (K1 k) (K1 l) = qlookup z d k l
-  | qlookup _ _ _ _ = raise Match
-
-
-
-(* Size-change graphs *)
-
-type
-  scg = sedge qtree
-
-
-(* addition of single edges *)
-fun add_sedge BOTH _ = BOTH
-  | add_sedge LESS LESS = LESS
-  | add_sedge LESS _ = BOTH
-  | add_sedge LEQ LEQ = LEQ
-  | add_sedge LEQ _ = BOTH
-
-fun mult_sedge LESS _ = LESS
-  | mult_sedge _ LESS = LESS
-  | mult_sedge LEQ x = x
-  | mult_sedge BOTH _ = BOTH
-
-fun subsumes_edge LESS LESS = true
-  | subsumes_edge LEQ _ = true
-  | subsumes_edge _ _ = false
-
-
-
-
-(* subsumes_SCG G H := G contains strictly less estimations than H *)
-fun subsumes_SCG (QEmpty : scg) (H : scg) = true
-  | subsumes_SCG (QQuad (a, b, c, d)) (QQuad (e,f,g,h)) =
-    (subsumes_SCG a e) andalso (subsumes_SCG b f)
-    andalso (subsumes_SCG c g) andalso (subsumes_SCG d h)
-  | subsumes_SCG (QNode e) (QNode e') = subsumes_edge e e'
-  | subsumes_SCG _ QEmpty = false
-  | subsumes_SCG _ _ = raise Match
-
-
-(* managing lists of SCGs. *)
-
-(* 
- Graphs are partially ordered. A list of graphs has the invariant that no G,H with G <= H.
- To maintain this when adding a new graph G, check 
-   (1) G <= H for some H in l => Do nothing
-   (2) has to be added. Then, all H <= G can be removed. 
-
- We can check (2) first, removing all smaller graphs. 
- If we could remove at least one, just add G in the end (Invariant!).
- Otherwise, check again, if G needs to be added at all. 
-
- OTOH, doing (1) first is probably better, because it does not produce garbage unless needed.
-
- The definition is tail-recursive. Order is not preserved (unneccessary).
-*)
-
-
-
-fun add_scg' G Hs = (* returns a flag indicating if the graph was really added *)
-    if exists (fn H => subsumes_SCG H G) Hs then (false, Hs)  (* redundant addition *)
-    else (true, G :: remove (uncurry subsumes_SCG) G Hs) (* remove all new redundancy and add G *)
-         (* NB: This does the second checks twice :-( *)
-
-(* Simpler version *)
-fun add_scg' G Hs = (not (member (op =) Hs G), insert (op =) G Hs)
-
-
-val add_scg = snd oo add_scg' (* without flag *)
-
-
-
-
-
-(* quadtrees *)
-
-fun keylen 0 = 0 
-  | keylen n = (keylen (n div 2)) + 1
-
-fun mk_key 0 _  = KHere
-  | mk_key l m = if m mod 2 = 0 
-                 then K0 (mk_key (l - 1) (m div 2)) 
-                 else K1 (mk_key (l - 1) (m div 2)) 
-
-
-fun qupdate f KHere KHere n = f n
-  | qupdate f (K0 k) (K0 k') (QQuad (a, b, c, d)) = QQuad (qupdate f k k' a, b, c, d)
-  | qupdate f (K0 k) (K1 k') (QQuad (a, b, c, d)) = QQuad (a, qupdate f k k' b, c, d)
-  | qupdate f (K1 k) (K0 k') (QQuad (a, b, c, d)) = QQuad (a, b, qupdate f k k' c, d)
-  | qupdate f (K1 k) (K1 k') (QQuad (a, b, c, d)) = QQuad (a, b, c, qupdate f k k' d)
-
-
-
-
-
-
-
-
-(* quadtree composition *)
-
-fun qadd A QEmpty q = q
-  | qadd A q QEmpty = q
-  | qadd A (QNode s) (QNode t) = QNode (A s t)
-  | qadd A (QQuad (a, b, c, d)) (QQuad (e, f, g, h)) =
-    QQuad (qadd A a e, qadd A b f, qadd A c g, qadd A d h)
-  | qadd _ _ _ = raise Match
-
-
-fun qmult A m QEmpty H = QEmpty
-  | qmult A m G QEmpty = QEmpty
-  | qmult A m (QNode x) (QNode y) = QNode (m x y)
-  | qmult A m (QQuad (a, b, c, d)) (QQuad (e, f, g, h)) = 
-    QQuad ((qadd A (qmult A m a e) (qmult A m b g)),
-           (qadd A (qmult A m a f) (qmult A m b h)),
-           (qadd A (qmult A m c e) (qmult A m d g)),
-           (qadd A (qmult A m c f) (qmult A m d h)))
-  | qmult _ _ _ _ = raise Match
-
-
-val (mult_scg : scg -> scg -> scg) = qmult add_sedge mult_sedge
-
-(* Misc notes:
-
-- When building the tcl: Check on addition and raise FAIL if the property is not true... (pract)
-
-- Can we reduce subsumption checking by some integer fingerprints?
-
- Number of edges: LESS(G) LEQ(G)
-  G <= H ==> E(G) <= E(H)
-  
-
-
-How to check:
-
-For each pair of adjacent edges: n -> m -> q
- compute all product SCGS and check if they are subsumed by something in the tcl.
-
- all midnode m: all fromnode n: all tonode q: alledges (n,m) e: alledges (m,q) e': subsumes (e*e') (edgs m,q)
-
- This is still quite a lot of checking... But: no garbage, just inspection. Can probably be done in logic. 
-
-*)
-
-
-
-(* Operations on lists: These preserve the invariants *)
-fun SCGs_mult Gs Hs = fold (fn (G,H) => add_scg (mult_scg G H)) (product Gs Hs) []
-val SCGs_plus = fold add_scg
-
-
-fun add_scgs Gs Hs = fold_rev (fn G => fn (Xs,As) => 
-                                      let val (b, Xs') = add_scg' G Xs
-                                      in (Xs', if b then G::As else As) end)
-                          Gs (Hs,[])
-
-(* Transitive Closure for lists of SCGs *)
-fun SCGs_tcl Gs =
-    let
-      fun aux S [] = S
-        | aux S (H::HS) =
-          let val (S', Ns) = add_scgs (map (mult_scg H) Gs) S
-          in aux S' (SCGs_plus Ns HS) end
-    in
-      aux Gs Gs
-    end
-
-
-
-(* Kleene algorithm: DP version, with imperative array... *)
-
-
-
-
-(* Terrible imperative stuff: *)
-type matrix = scg list array array
-
-fun mupdate i j f M = 
-    let 
-      val row = Array.sub (M, i)
-      val x = Array.sub (row, j)
-    in 
-      Array.update (row, j, f x)
-    end
-
-fun mget i j M = Array.sub(Array.sub(M,i),j)
-
-fun print_scg (x : scg) = Output.warning (PolyML.makestring x);
-
-
-fun kleene add mult tcl M =
-    let
-      val n = Array.length M
-
-      fun update Mkk i j k = 
-          let
-            val Mik = mget i k M
-            val Mkj = mget k j M
-          in
-            mupdate i j (fn X => X |> add (mult Mik (mult Mkk Mkj))
-                                   |> add (mult Mik Mkj))
-                    M
-          end
-
-      fun step k () =
-          let
-            val _ = mupdate k k tcl M
-            val Mkk = mget k k M
-
-            val no_k = filter_out (fn i => i = k) (0 upto (n - 1)) 
-            val _ = fold (fn i => fold (fn j => K (update Mkk i j k)) no_k) no_k ()
-
-            val _ = fold (fn i => K (update Mkk i k k)) no_k ()
-
-            val _ = fold (fn j => K (update Mkk k j k)) no_k ()
-          in
-            ()
-          end
-    in
-      fold step (0 upto (n - 1)) ()
-    end
-
-val (SCGs_kleene : matrix -> unit) = kleene SCGs_plus SCGs_mult SCGs_tcl
-
-
-fun andop x y = x andalso y
-fun orop x y = x orelse y
-
-fun array2 n x = Array.tabulate (n, (fn i => Array.array (n, x)))
-
-(*val bool_kleene = kleene orop andop I
-
-
-fun test_bool () =
-    let
-      val M = array2 2 false
-      val _ = mupdate 0 1 (K true) M
-      val _ = mupdate 1 0 (K true) M
-      val _ = bool_kleene M
-    in
-      M
-    end
-*)
-
-(* Standard 2-2-Size-change graphs *)
-
-val swap = QQuad(QEmpty, QNode LEQ,
-                 QNode LEQ, QEmpty)
-
-val swapRTop = QQuad(QNode LESS, QNode LEQ,
-                     QNode LEQ, QEmpty)
-
-val BTopRBot = QQuad(QNode LEQ, QEmpty,
-                     QEmpty, QNode LESS)
-
-val RTopBBot = QQuad(QNode LESS, QEmpty,
-                     QEmpty, QNode LEQ)
-
-val R2Straight = QQuad(QNode LESS, QEmpty,
-                       QEmpty, QNode LESS)
-
-val R3StraightUp = QQuad(QNode LESS, QEmpty,
-                         QNode LESS, QNode LESS)
-
-val R3StraightDn = QQuad(QNode LESS, QNode LESS,
-                         QEmpty, QNode LESS)
-
-
-
-
-val diag = QQuad(QEmpty, QNode LEQ,
-                 QEmpty, QEmpty)
-
-val straight = QQuad(QNode LEQ, QEmpty,
-                     QEmpty, QEmpty)
-
-
-
-val R467913 = ([R2Straight, R3StraightDn, R3StraightDn] @ replicate 11 R2Straight @ [R3StraightUp, R3StraightUp])
-                |> map single
-
-val swapPos = [(0,8),(0,9),(0,10),(3,4),(3,5),(11,12)]
-
-val BRPos = (map (pair 5) (0 :: (3 upto 7)))
-            @ (map (pair 8) [8,9,11,12,13])
-            @ (map (pair 12) [8,9,11,12,13])
-
-val RBPos = map (pair 10) (3 upto 10)
-
-fun afold f arr x = Array.foldl (uncurry f) x arr
-
-fun msize M = afold (afold (curry op + o length)) M 0
-
-fun TestM () =
-    let
-      val M = array2 16 ([] : scg list)
-      val _ = Array.update (M, 4, Array.fromList R467913)
-      val _ = Array.update (M, 6, Array.fromList R467913)
-      val _ = Array.update (M, 7, Array.fromList R467913)
-      val _ = Array.update (M, 9, Array.fromList R467913)
-      val _ = Array.update (M, 13, Array.fromList R467913)
-
-      val _ = map (fn (i,j) => mupdate i j (K [swap]) M) swapPos
-      val _ = map (fn (i,j) => mupdate i j (K [BTopRBot]) M) BRPos
-      val _ = map (fn (i,j) => mupdate i j (K [RTopBBot]) M) RBPos
-
-      val _ = mupdate 1 14 (K [swapRTop]) M
-      val _ = mupdate 2 15 (K [swapRTop]) M
-
-      val G = [QQuad (QNode LEQ, QNode LESS, QEmpty, QNode LESS)]
-      val _ = mupdate 5 1 (K G) M
-      val _ = mupdate 8 2 (K G) M
-      val _ = mupdate 12 2 (K G) M
-
-      val G = [QQuad (QNode LESS, QEmpty, QNode LESS, QNode LEQ)]
-      val _ = mupdate 10 14 (K G) M
-
-      val G = [QQuad (QEmpty, QNode LEQ, QNode LESS, QNode LESS)]
-      val _ = mupdate 14 1 (K G) M
-      val _ = mupdate 14 2 (K G) M
-      val _ = mupdate 15 1 (K G) M
-      val _ = mupdate 15 2 (K G) M
-    in
-      M
-    end
-
-
-
-
-
-fun add_edge x QEmpty = QNode x
-  | add_edge x (QNode y) = QNode (add_sedge x y)
-
-
-fun sedge2ML (Const ("SCT_Definition.sedge.LESS", _)) = LESS
-  | sedge2ML (Const ("SCT_Definition.sedge.LEQ", _)) = LEQ
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
 end