author | wenzelm |
Thu, 09 Jul 2009 22:01:41 +0200 | |
changeset 31971 | 8c1b845ed105 |
parent 31775 | 2b04504fcb69 |
child 32149 | ef59550a55d3 |
permissions | -rw-r--r-- |
31775 | 1 |
(* Title: HOL/Tools/Function/decompose.ML |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, TU Muenchen |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
3 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
4 |
Graph decomposition using "Shallow Dependency Pairs". |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
5 |
*) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
6 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
7 |
signature DECOMPOSE = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
8 |
sig |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
9 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
10 |
val derive_chains : Proof.context -> tactic |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
11 |
-> (Termination.data -> int -> tactic) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
12 |
-> Termination.data -> int -> tactic |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
13 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
14 |
val decompose_tac : Proof.context -> tactic |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
15 |
-> Termination.ttac |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
16 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
17 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
18 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
19 |
structure Decompose : DECOMPOSE = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
20 |
struct |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
21 |
|
31971
8c1b845ed105
renamed functor TableFun to Table, and GraphFun to Graph;
wenzelm
parents:
31775
diff
changeset
|
22 |
structure TermGraph = Graph(type key = term val ord = TermOrd.fast_term_ord); |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
23 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
24 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
25 |
fun derive_chains ctxt chain_tac cont D = Termination.CALLS (fn (cs, i) => |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
26 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
27 |
val thy = ProofContext.theory_of ctxt |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
28 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
29 |
fun prove_chain c1 c2 D = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
30 |
if is_some (Termination.get_chain D c1 c2) then D else |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
31 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
32 |
val goal = HOLogic.mk_eq (HOLogic.mk_binop @{const_name "Relation.rel_comp"} (c1, c2), |
30304
d8e4cd2ac2a1
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
haftmann
parents:
29269
diff
changeset
|
33 |
Const (@{const_name Set.empty}, fastype_of c1)) |
29125
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
34 |
|> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
35 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
36 |
val chain = case FundefLib.try_proof (cterm_of thy goal) chain_tac of |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
37 |
FundefLib.Solved thm => SOME thm |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
38 |
| _ => NONE |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
39 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
40 |
Termination.note_chain c1 c2 chain D |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
41 |
end |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
42 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
43 |
cont (fold_product prove_chain cs cs D) i |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
44 |
end) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
45 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
46 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
47 |
fun mk_dgraph D cs = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
48 |
TermGraph.empty |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
49 |
|> fold (fn c => TermGraph.new_node (c,())) cs |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
50 |
|> fold_product (fn c1 => fn c2 => |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
51 |
if is_none (Termination.get_chain D c1 c2 |> the_default NONE) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
52 |
then TermGraph.add_edge (c1, c2) else I) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
53 |
cs cs |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
54 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
55 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
56 |
fun ucomp_empty_tac T = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
57 |
REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR} |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
58 |
ORELSE' rtac @{thm union_comp_emptyL} |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
59 |
ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i)) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
60 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
61 |
fun regroup_calls_tac cs = Termination.CALLS (fn (cs', i) => |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
62 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
63 |
val is = map (fn c => find_index (curry op aconv c) cs') cs |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
64 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
65 |
CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv is))) i |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
66 |
end) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
67 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
68 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
69 |
fun solve_trivial_tac D = Termination.CALLS |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
70 |
(fn ([c], i) => |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
71 |
(case Termination.get_chain D c c of |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
72 |
SOME (SOME thm) => rtac @{thm wf_no_loop} i |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
73 |
THEN rtac thm i |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
74 |
| _ => no_tac) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
75 |
| _ => no_tac) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
76 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
77 |
fun decompose_tac' ctxt cont err_cont D = Termination.CALLS (fn (cs, i) => |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
78 |
let |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
79 |
val G = mk_dgraph D cs |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
80 |
val sccs = TermGraph.strong_conn G |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
81 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
82 |
fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
83 |
| split (SCC::rest) i = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
84 |
regroup_calls_tac SCC i |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
85 |
THEN rtac @{thm wf_union_compatible} i |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
86 |
THEN rtac @{thm less_by_empty} (i + 2) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
87 |
THEN ucomp_empty_tac (the o the oo Termination.get_chain D) (i + 2) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
88 |
THEN split rest (i + 1) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
89 |
THEN (solve_trivial_tac D i ORELSE cont D i) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
90 |
in |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
91 |
if length sccs > 1 then split sccs i |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
92 |
else solve_trivial_tac D i ORELSE err_cont D i |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
93 |
end) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
94 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
95 |
fun decompose_tac ctxt chain_tac cont err_cont = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
96 |
derive_chains ctxt chain_tac |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
97 |
(decompose_tac' ctxt cont err_cont) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
98 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
99 |
fun auto_decompose_tac ctxt = |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
100 |
Termination.TERMINATION ctxt |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
101 |
(decompose_tac ctxt (auto_tac (local_clasimpset_of ctxt)) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
102 |
(K (K all_tac)) (K (K no_tac))) |
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
103 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
104 |
|
d41182a8135c
method "sizechange" proves termination of functions; added more infrastructure for termination proofs
krauss
parents:
diff
changeset
|
105 |
end |