author | krauss |
Wed, 28 Feb 2007 11:12:12 +0100 | |
changeset 22371 | c9f5895972b0 |
parent 22370 | 44679bbcf43b |
permissions | -rw-r--r-- |
22371 | 1 |
(* Title: HOL/Library/size_change_termination.ML |
2 |
ID: $Id$ |
|
3 |
Author: Alexander Krauss, TU Muenchen |
|
4 |
*) |
|
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
5 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
6 |
structure SCT = struct |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
7 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
8 |
fun matrix [] ys = [] |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
9 |
| matrix (x::xs) ys = map (pair x) ys :: matrix xs ys |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
10 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
11 |
fun map_matrix f xss = map (map f) xss |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
12 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
13 |
val scgT = Sign.read_typ (the_context (), K NONE) "scg" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
14 |
val acgT = Sign.read_typ (the_context (), K NONE) "acg" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
15 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
16 |
fun edgeT nT eT = HOLogic.mk_prodT (nT, HOLogic.mk_prodT (eT, nT)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
17 |
fun graphT nT eT = Type ("Graphs.graph", [nT, eT]) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
18 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
19 |
fun graph_const nT eT = Const ("Graphs.graph.Graph", HOLogic.mk_setT (edgeT nT eT) --> graphT nT eT) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
20 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
21 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
22 |
val no_step_const = "SCT_Interpretation.no_step" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
23 |
val no_step_def = thm "SCT_Interpretation.no_step_def" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
24 |
val no_stepI = thm "SCT_Interpretation.no_stepI" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
25 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
26 |
fun mk_no_step RD1 RD2 = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
27 |
let val RDT = fastype_of RD1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
28 |
in Const (no_step_const, RDT --> RDT --> HOLogic.boolT) $ RD1 $ RD2 end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
29 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
30 |
val decr_const = "SCT_Interpretation.decr" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
31 |
val decr_def = thm "SCT_Interpretation.decr_def" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
32 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
33 |
fun mk_decr RD1 RD2 M1 M2 = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
34 |
let val RDT = fastype_of RD1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
35 |
val MT = fastype_of M1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
36 |
in Const (decr_const, RDT --> RDT --> MT --> MT --> HOLogic.boolT) $ RD1 $ RD2 $ M1 $ M2 end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
37 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
38 |
val decreq_const = "SCT_Interpretation.decreq" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
39 |
val decreq_def = thm "SCT_Interpretation.decreq_def" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
40 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
41 |
fun mk_decreq RD1 RD2 M1 M2 = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
42 |
let val RDT = fastype_of RD1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
43 |
val MT = fastype_of M1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
44 |
in Const (decreq_const, RDT --> RDT --> MT --> MT --> HOLogic.boolT) $ RD1 $ RD2 $ M1 $ M2 end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
45 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
46 |
val stepP_const = "SCT_Interpretation.stepP" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
47 |
val stepP_def = thm "SCT_Interpretation.stepP.simps" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
48 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
49 |
fun mk_stepP RD1 RD2 M1 M2 Rel = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
50 |
let val RDT = fastype_of RD1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
51 |
val MT = fastype_of M1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
52 |
in |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
53 |
Const (stepP_const, RDT --> RDT --> MT --> MT --> (fastype_of Rel) --> HOLogic.boolT) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
54 |
$ RD1 $ RD2 $ M1 $ M2 $ Rel |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
55 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
56 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
57 |
val approx_const = "SCT_Interpretation.approx" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
58 |
val approx_empty = thm "SCT_Interpretation.approx_empty" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
59 |
val approx_less = thm "SCT_Interpretation.approx_less" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
60 |
val approx_leq = thm "SCT_Interpretation.approx_leq" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
61 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
62 |
fun mk_approx G RD1 RD2 Ms1 Ms2 = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
63 |
let val RDT = fastype_of RD1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
64 |
val MsT = fastype_of Ms1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
65 |
in Const (approx_const, scgT --> RDT --> RDT --> MsT --> MsT --> HOLogic.boolT) $ G $ RD1 $ RD2 $ Ms1 $ Ms2 end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
66 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
67 |
val sound_int_const = "SCT_Interpretation.sound_int" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
68 |
val sound_int_def = thm "SCT_Interpretation.sound_int_def" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
69 |
fun mk_sound_int A RDs M = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
70 |
let val RDsT = fastype_of RDs |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
71 |
val MT = fastype_of M |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
72 |
in Const (sound_int_const, acgT --> RDsT --> MT --> HOLogic.boolT) $ A $ RDs $ M end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
73 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
74 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
75 |
val nth_const = "List.nth" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
76 |
fun mk_nth xs = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
77 |
let val lT as Type (_, [T]) = fastype_of xs |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
78 |
in Const (nth_const, lT --> HOLogic.natT --> T) $ xs end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
79 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
80 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
81 |
val less_nat_const = Const ("Orderings.less", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
82 |
val lesseq_nat_const = Const ("Orderings.less_eq", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
83 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
84 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
85 |
(* |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
86 |
val has_edge_const = "Graphs.has_edge" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
87 |
fun mk_has_edge G n e n' = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
88 |
let val nT = fastype_of n and eT = fastype_of e |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
89 |
in Const (has_edge_const, graphT nT eT --> nT --> eT --> nT --> HOLogic.boolT) $ n $ e $ n' end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
90 |
*) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
91 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
92 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
93 |
val has_edge_simps = [thm "Graphs.has_edge_def", thm "Graphs.dest_graph.simps"] |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
94 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
95 |
val all_less_zero = thm "SCT_Interpretation.all_less_zero" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
96 |
val all_less_Suc = thm "SCT_Interpretation.all_less_Suc" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
97 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
98 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
99 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
100 |
(* Lists as finite multisets *) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
101 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
102 |
(* --> Library *) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
103 |
fun del_index n [] = [] |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
104 |
| del_index n (x :: xs) = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
105 |
if n>0 then x :: del_index (n - 1) xs else xs |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
106 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
107 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
108 |
fun remove1 eq x [] = [] |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
109 |
| remove1 eq x (y :: ys) = if eq (x, y) then ys else y :: remove1 eq x ys |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
110 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
111 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
112 |
fun multi_union eq [] ys = ys |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
113 |
| multi_union eq (x::xs) ys = x :: multi_union eq xs (remove1 eq x ys) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
114 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
115 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
116 |
fun dest_ex (Const ("Ex", _) $ Abs (a as (_,T,_))) = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
117 |
let |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
118 |
val (n, body) = Term.dest_abs a |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
119 |
in |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
120 |
(Free (n, T), body) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
121 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
122 |
| dest_ex _ = raise Match |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
123 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
124 |
fun dest_all_ex (t as (Const ("Ex",_) $ _)) = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
125 |
let |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
126 |
val (v,b) = dest_ex t |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
127 |
val (vs, b') = dest_all_ex b |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
128 |
in |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
129 |
(v :: vs, b') |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
130 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
131 |
| dest_all_ex t = ([],t) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
132 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
133 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
134 |
fun dist_vars [] vs = (assert (null vs) "dist_vars"; []) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
135 |
| dist_vars (T::Ts) vs = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
136 |
case find_index (fn v => fastype_of v = T) vs of |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
137 |
~1 => Free ("", T) :: dist_vars Ts vs |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
138 |
| i => (nth vs i) :: dist_vars Ts (del_index i vs) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
139 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
140 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
141 |
fun dest_case rebind t = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
142 |
let |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
143 |
val (_ $ _ $ rhs :: _ $ _ $ match :: guards) = HOLogic.dest_conj t |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
144 |
val guard = case guards of [] => HOLogic.true_const | gs => foldr1 HOLogic.mk_conj gs |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
145 |
in |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
146 |
foldr1 HOLogic.mk_prod [rebind guard, rebind rhs, rebind match] |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
147 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
148 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
149 |
fun bind_many [] = I |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
150 |
| bind_many vs = FundefLib.tupled_lambda (foldr1 HOLogic.mk_prod vs) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
151 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
152 |
(* Builds relation descriptions from a relation definition *) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
153 |
fun mk_reldescs (Abs a) = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
154 |
let |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
155 |
val (_, Abs a') = Term.dest_abs a |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
156 |
val (_, b) = Term.dest_abs a' |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
157 |
val cases = HOLogic.dest_disj b |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
158 |
val (vss, bs) = split_list (map dest_all_ex cases) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
159 |
val unionTs = fold (multi_union (op =)) (map (map fastype_of) vss) [] |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
160 |
val rebind = map (bind_many o dist_vars unionTs) vss |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
161 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
162 |
val RDs = map2 dest_case rebind bs |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
163 |
in |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
164 |
HOLogic.mk_list (fastype_of (hd RDs)) RDs |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
165 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
166 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
167 |
fun abs_rel_tac (st : thm) = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
168 |
let |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
169 |
val thy = theory_of_thm st |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
170 |
val (def, rd) = HOLogic.dest_eq (HOLogic.dest_Trueprop (hd (prems_of st))) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
171 |
val RDs = cterm_of thy (mk_reldescs def) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
172 |
val rdvar = Var (the_single (Term.add_vars rd [])) |> cterm_of thy |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
173 |
in |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
174 |
Seq.single (cterm_instantiate [(rdvar, RDs)] st) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
175 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
176 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
177 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
178 |
(* very primitive *) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
179 |
fun measures_of RD = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
180 |
let |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
181 |
val domT = range_type (fastype_of (fst (HOLogic.dest_prod (snd (HOLogic.dest_prod RD))))) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
182 |
val measures = LexicographicOrder.mk_base_funs domT |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
183 |
in |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
184 |
measures |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
185 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
186 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
187 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
188 |
|
22370 | 189 |
val mk_number = HOLogic.mk_nat o IntInf.fromInt |
190 |
val dest_number = IntInf.toInt o HOLogic.dest_nat |
|
22359
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
191 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
192 |
fun nums_to i = map mk_number (0 upto (i - 1)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
193 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
194 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
195 |
fun unfold_then_auto thm = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
196 |
(SIMPSET (unfold_tac [thm])) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
197 |
THEN (CLASIMPSET auto_tac) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
198 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
199 |
val nth_simps = [thm "List.nth_Cons_0", thm "List.nth_Cons_Suc"] |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
200 |
val nth_ss = (HOL_basic_ss addsimps nth_simps) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
201 |
val simp_nth_tac = simp_tac nth_ss |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
202 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
203 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
204 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
205 |
fun tabulate_tlist thy l = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
206 |
let |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
207 |
val n = length (HOLogic.dest_list l) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
208 |
val table = Inttab.make (map (fn i => (i, Simplifier.rewrite nth_ss (cterm_of thy (mk_nth l $ mk_number i)))) (0 upto n - 1)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
209 |
in |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
210 |
the o Inttab.lookup table |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
211 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
212 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
213 |
val get_elem = snd o Logic.dest_equals o prop_of |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
214 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
215 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
216 |
(* Attempt a proof of a given goal *) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
217 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
218 |
datatype proof_result = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
219 |
Success of thm |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
220 |
| Stuck of thm |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
221 |
| Fail |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
222 |
| False |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
223 |
| Timeout (* not implemented *) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
224 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
225 |
fun try_to_prove tactic cgoal = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
226 |
case SINGLE tactic (Goal.init cgoal) of |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
227 |
NONE => Fail |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
228 |
| SOME st => if Thm.no_prems st |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
229 |
then Success (Goal.finish st) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
230 |
else if prems_of st = [HOLogic.Trueprop $ HOLogic.false_const] then False |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
231 |
else Stuck st |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
232 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
233 |
fun simple_result (Success thm) = SOME thm |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
234 |
| simple_result _ = NONE |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
235 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
236 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
237 |
fun inst_nums thy i j (t:thm) = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
238 |
instantiate' [] [NONE, NONE, NONE, SOME (cterm_of thy (mk_number i)), NONE, SOME (cterm_of thy (mk_number j))] t |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
239 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
240 |
datatype call_fact = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
241 |
NoStep of thm |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
242 |
| Graph of (term * thm) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
243 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
244 |
fun rand (_ $ t) = t |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
245 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
246 |
fun setup_probe_goal thy domT Dtab Mtab (i, j) = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
247 |
let |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
248 |
val RD1 = get_elem (Dtab i) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
249 |
val RD2 = get_elem (Dtab j) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
250 |
val Ms1 = get_elem (Mtab i) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
251 |
val Ms2 = get_elem (Mtab j) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
252 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
253 |
val Mst1 = HOLogic.dest_list (rand Ms1) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
254 |
val Mst2 = HOLogic.dest_list (rand Ms2) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
255 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
256 |
val mvar1 = Free ("sctmfv1", domT --> HOLogic.natT) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
257 |
val mvar2 = Free ("sctmfv2", domT --> HOLogic.natT) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
258 |
val relvar = Free ("sctmfrel", HOLogic.natT --> HOLogic.natT --> HOLogic.boolT) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
259 |
val N = length Mst1 and M = length Mst2 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
260 |
val saved_state = HOLogic.mk_Trueprop (mk_stepP RD1 RD2 mvar1 mvar2 relvar) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
261 |
|> cterm_of thy |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
262 |
|> Goal.init |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
263 |
|> CLASIMPSET auto_tac |> Seq.hd |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
264 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
265 |
val no_step = saved_state |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
266 |
|> forall_intr (cterm_of thy relvar) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
267 |
|> forall_elim (cterm_of thy (Abs ("", HOLogic.natT, Abs ("", HOLogic.natT, HOLogic.false_const)))) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
268 |
|> CLASIMPSET auto_tac |> Seq.hd |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
269 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
270 |
in |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
271 |
if Thm.no_prems no_step |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
272 |
then NoStep (Goal.finish no_step RS no_stepI) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
273 |
else |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
274 |
let |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
275 |
fun set_m1 i = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
276 |
let |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
277 |
val M1 = nth Mst1 i |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
278 |
val with_m1 = saved_state |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
279 |
|> forall_intr (cterm_of thy mvar1) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
280 |
|> forall_elim (cterm_of thy M1) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
281 |
|> CLASIMPSET auto_tac |> Seq.hd |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
282 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
283 |
fun set_m2 j = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
284 |
let |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
285 |
val M2 = nth Mst2 j |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
286 |
val with_m2 = with_m1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
287 |
|> forall_intr (cterm_of thy mvar2) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
288 |
|> forall_elim (cterm_of thy M2) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
289 |
|> CLASIMPSET auto_tac |> Seq.hd |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
290 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
291 |
val decr = forall_intr (cterm_of thy relvar) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
292 |
#> forall_elim (cterm_of thy less_nat_const) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
293 |
#> CLASIMPSET auto_tac #> Seq.hd |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
294 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
295 |
val decreq = forall_intr (cterm_of thy relvar) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
296 |
#> forall_elim (cterm_of thy lesseq_nat_const) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
297 |
#> CLASIMPSET auto_tac #> Seq.hd |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
298 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
299 |
val thm1 = decr with_m2 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
300 |
in |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
301 |
if Thm.no_prems thm1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
302 |
then ((rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm1) 1)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
303 |
else let val thm2 = decreq with_m2 in |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
304 |
if Thm.no_prems thm2 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
305 |
then ((rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac (Goal.finish thm2) 1)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
306 |
else all_tac end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
307 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
308 |
in set_m2 end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
309 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
310 |
val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
311 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
312 |
val tac = (EVERY (map (fn n => EVERY (map (set_m1 n) (0 upto M - 1))) (0 upto N - 1))) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
313 |
THEN (rtac approx_empty 1) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
314 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
315 |
val approx_thm = goal |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
316 |
|> cterm_of thy |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
317 |
|> Goal.init |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
318 |
|> tac |> Seq.hd |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
319 |
|> Goal.finish |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
320 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
321 |
val _ $ (_ $ G $ _ $ _ $ _ $ _) = prop_of approx_thm |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
322 |
in |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
323 |
Graph (G, approx_thm) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
324 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
325 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
326 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
327 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
328 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
329 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
330 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
331 |
fun probe_nostep thy Dtab i j = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
332 |
HOLogic.mk_Trueprop (mk_no_step (get_elem (Dtab i)) (get_elem (Dtab j))) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
333 |
|> cterm_of thy |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
334 |
|> try_to_prove (unfold_then_auto no_step_def) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
335 |
|> simple_result |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
336 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
337 |
fun probe_decr thy RD1 RD2 m1 m2 = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
338 |
HOLogic.mk_Trueprop (mk_decr RD1 RD2 m1 m2) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
339 |
|> cterm_of thy |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
340 |
|> try_to_prove (unfold_then_auto decr_def) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
341 |
|> simple_result |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
342 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
343 |
fun probe_decreq thy RD1 RD2 m1 m2 = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
344 |
HOLogic.mk_Trueprop (mk_decreq RD1 RD2 m1 m2) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
345 |
|> cterm_of thy |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
346 |
|> try_to_prove (unfold_then_auto decreq_def) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
347 |
|> simple_result |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
348 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
349 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
350 |
fun build_approximating_graph thy Dtab Mtab Mss mlens mint nint = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
351 |
let |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
352 |
val D1 = Dtab mint and D2 = Dtab nint |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
353 |
val Mst1 = Mtab mint and Mst2 = Mtab nint |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
354 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
355 |
val RD1 = get_elem D1 and RD2 = get_elem D2 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
356 |
val Ms1 = get_elem Mst1 and Ms2 = get_elem Mst2 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
357 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
358 |
val goal = HOLogic.mk_Trueprop (mk_approx (Var (("G", 0), scgT)) RD1 RD2 Ms1 Ms2) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
359 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
360 |
val Ms1 = nth (nth Mss mint) and Ms2 = nth (nth Mss mint) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
361 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
362 |
fun add_edge (i,j) = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
363 |
case timeap_msg ("decr(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")") |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
364 |
(probe_decr thy RD1 RD2 (Ms1 i)) (Ms2 j) of |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
365 |
SOME thm => (Output.warning "Success"; (rtac (inst_nums thy i j approx_less) 1) THEN (simp_nth_tac 1) THEN (rtac thm 1)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
366 |
| NONE => case timeap_msg ("decr(" ^ string_of_int i ^ "," ^ string_of_int j ^ ")") |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
367 |
(probe_decreq thy RD1 RD2 (Ms1 i)) (Ms2 j) of |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
368 |
SOME thm => (Output.warning "Success"; (rtac (inst_nums thy i j approx_leq) 1) THEN (simp_nth_tac 1) THEN (rtac thm 1)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
369 |
| NONE => all_tac |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
370 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
371 |
val approx_thm = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
372 |
goal |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
373 |
|> cterm_of thy |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
374 |
|> Goal.init |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
375 |
|> SINGLE ((EVERY (map add_edge (product (0 upto (nth mlens mint) - 1) (0 upto (nth mlens nint) - 1)))) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
376 |
THEN (rtac approx_empty 1)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
377 |
|> the |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
378 |
|> Goal.finish |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
379 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
380 |
val _ $ (_ $ G $ _ $ _ $ _ $ _) = prop_of approx_thm |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
381 |
in |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
382 |
(G, approx_thm) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
383 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
384 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
385 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
386 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
387 |
fun prove_call_fact thy Dtab Mtab Mss mlens (m, n) = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
388 |
case probe_nostep thy Dtab m n of |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
389 |
SOME thm => (Output.warning "NoStep"; NoStep thm) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
390 |
| NONE => Graph (build_approximating_graph thy Dtab Mtab Mss mlens m n) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
391 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
392 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
393 |
fun mk_edge m G n = HOLogic.mk_prod (m, HOLogic.mk_prod (G, n)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
394 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
395 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
396 |
fun mk_set T [] = Const ("{}", HOLogic.mk_setT T) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
397 |
| mk_set T (x :: xs) = Const ("insert", |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
398 |
T --> HOLogic.mk_setT T --> HOLogic.mk_setT T) $ x $ mk_set T xs |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
399 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
400 |
fun dest_set (Const ("{}", _)) = [] |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
401 |
| dest_set (Const ("insert", _) $ x $ xs) = x :: dest_set xs |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
402 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
403 |
val pr_graph = Sign.string_of_term |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
404 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
405 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
406 |
fun pr_matrix thy = map_matrix (fn Graph (G, _) => pr_graph thy G | _ => "X") |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
407 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
408 |
val in_graph_tac = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
409 |
simp_tac (HOL_basic_ss addsimps has_edge_simps) 1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
410 |
THEN SIMPSET (fn x => simp_tac x 1) (* FIXME reduce simpset *) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
411 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
412 |
fun approx_tac (NoStep thm) = rtac disjI1 1 THEN rtac thm 1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
413 |
| approx_tac (Graph (G, thm)) = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
414 |
rtac disjI2 1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
415 |
THEN rtac exI 1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
416 |
THEN rtac conjI 1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
417 |
THEN rtac thm 2 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
418 |
THEN in_graph_tac |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
419 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
420 |
fun all_less_tac [] = rtac all_less_zero 1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
421 |
| all_less_tac (t :: ts) = rtac all_less_Suc 1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
422 |
THEN simp_nth_tac 1 |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
423 |
THEN t |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
424 |
THEN all_less_tac ts |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
425 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
426 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
427 |
val length_const = "Nat.size" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
428 |
fun mk_length l = Const (length_const, fastype_of l --> HOLogic.natT) $ l |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
429 |
val length_simps = thms "SCT_Interpretation.length_simps" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
430 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
431 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
432 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
433 |
fun mk_call_graph (st : thm) = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
434 |
let |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
435 |
val thy = theory_of_thm st |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
436 |
val _ $ _ $ RDlist $ _ = HOLogic.dest_Trueprop (hd (prems_of st)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
437 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
438 |
val RDs = HOLogic.dest_list RDlist |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
439 |
val n = length RDs |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
440 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
441 |
val Mss = map measures_of RDs |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
442 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
443 |
val domT = domain_type (fastype_of (hd (hd Mss))) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
444 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
445 |
val mfuns = map (fn Ms => mk_nth (HOLogic.mk_list (fastype_of (hd Ms)) Ms)) Mss |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
446 |
|> (fn l => HOLogic.mk_list (fastype_of (hd l)) l) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
447 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
448 |
val Dtab = tabulate_tlist thy RDlist |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
449 |
val Mtab = tabulate_tlist thy mfuns |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
450 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
451 |
val len_simp = Simplifier.rewrite (HOL_basic_ss addsimps length_simps) (cterm_of thy (mk_length RDlist)) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
452 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
453 |
val mlens = map length Mss |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
454 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
455 |
val indices = (n - 1 downto 0) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
456 |
val pairs = matrix indices indices |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
457 |
val parts = map_matrix (fn (n,m) => |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
458 |
(timeap_msg (string_of_int n ^ "," ^ string_of_int m) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
459 |
(setup_probe_goal thy domT Dtab Mtab) (n,m))) pairs |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
460 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
461 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
462 |
val s = fold_index (fn (i, cs) => fold_index (fn (j, Graph (G, _)) => prefix ("(" ^ string_of_int i ^ "," ^ string_of_int j ^ "): " ^ |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
463 |
pr_graph thy G ^ ",\n") |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
464 |
| _ => I) cs) parts "" |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
465 |
val _ = Output.warning s |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
466 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
467 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
468 |
val ACG = map_filter (fn (Graph (G, _),(m, n)) => SOME (mk_edge (mk_number m) G (mk_number n)) | _ => NONE) (flat parts ~~ flat pairs) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
469 |
|> mk_set (edgeT HOLogic.natT scgT) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
470 |
|> curry op $ (graph_const HOLogic.natT scgT) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
471 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
472 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
473 |
val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
474 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
475 |
val tac = |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
476 |
(SIMPSET (unfold_tac [sound_int_def, len_simp])) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
477 |
THEN all_less_tac (map (all_less_tac o map approx_tac) parts) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
478 |
in |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
479 |
tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st) |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
480 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
481 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
482 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
483 |
end |
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
484 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
485 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
486 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
487 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
488 |
|
94a794672c8b
Added formalization of size-change principle (experimental).
krauss
parents:
diff
changeset
|
489 |