--- a/src/HOL/Library/size_change_termination.ML Wed Feb 28 00:22:26 2007 +0100
+++ b/src/HOL/Library/size_change_termination.ML Wed Feb 28 10:36:10 2007 +0100
@@ -182,8 +182,8 @@
-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))
@@ -343,10 +343,6 @@
|> 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
@@ -480,398 +476,6 @@
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