author | wenzelm |
Wed, 04 Mar 2015 19:53:18 +0100 | |
changeset 59582 | 0fbed69ff081 |
parent 59498 | 50b60f501b05 |
child 59621 | 291934bac95e |
permissions | -rw-r--r-- |
42151 | 1 |
(* Title: HOL/HOLCF/Tools/cont_proc.ML |
23152 | 2 |
Author: Brian Huffman |
3 |
*) |
|
4 |
||
5 |
signature CONT_PROC = |
|
6 |
sig |
|
7 |
val is_lcf_term: term -> bool |
|
8 |
val cont_thms: term -> thm list |
|
9 |
val all_cont_thms: term -> thm list |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
10 |
val cont_tac: Proof.context -> int -> tactic |
23152 | 11 |
val cont_proc: theory -> simproc |
12 |
val setup: theory -> theory |
|
40832 | 13 |
end |
23152 | 14 |
|
41296
6aaf80ea9715
switch to transparent ascription, to avoid warning messages
huffman
parents:
40832
diff
changeset
|
15 |
structure ContProc : CONT_PROC = |
23152 | 16 |
struct |
17 |
||
18 |
(** theory context references **) |
|
19 |
||
40832 | 20 |
val cont_K = @{thm cont_const} |
21 |
val cont_I = @{thm cont_id} |
|
22 |
val cont_A = @{thm cont2cont_APP} |
|
23 |
val cont_L = @{thm cont2cont_LAM} |
|
24 |
val cont_R = @{thm cont_Rep_cfun2} |
|
23152 | 25 |
|
26 |
(* checks whether a term is written entirely in the LCF sublanguage *) |
|
40327 | 27 |
fun is_lcf_term (Const (@{const_name Rep_cfun}, _) $ t $ u) = |
23152 | 28 |
is_lcf_term t andalso is_lcf_term u |
40327 | 29 |
| is_lcf_term (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) = |
29047 | 30 |
is_lcf_term t |
40327 | 31 |
| is_lcf_term (Const (@{const_name Abs_cfun}, _) $ t) = |
29373 | 32 |
is_lcf_term (Term.incr_boundvars 1 t $ Bound 0) |
23152 | 33 |
| is_lcf_term (Bound _) = true |
42083
e1209fc7ecdc
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
wenzelm
parents:
41296
diff
changeset
|
34 |
| is_lcf_term t = not (Term.is_open t) |
23152 | 35 |
|
36 |
(* |
|
37 |
efficiently generates a cont thm for every LAM abstraction in a term, |
|
38 |
using forward proof and reusing common subgoals |
|
39 |
*) |
|
40 |
local |
|
41 |
fun var 0 = [SOME cont_I] |
|
40832 | 42 |
| var n = NONE :: var (n-1) |
23152 | 43 |
|
44 |
fun k NONE = cont_K |
|
40832 | 45 |
| k (SOME x) = x |
23152 | 46 |
|
47 |
fun ap NONE NONE = NONE |
|
40832 | 48 |
| ap x y = SOME (k y RS (k x RS cont_A)) |
23152 | 49 |
|
50 |
fun zip [] [] = [] |
|
51 |
| zip [] (y::ys) = (ap NONE y ) :: zip [] ys |
|
52 |
| zip (x::xs) [] = (ap x NONE) :: zip xs [] |
|
53 |
| zip (x::xs) (y::ys) = (ap x y ) :: zip xs ys |
|
54 |
||
55 |
fun lam [] = ([], cont_K) |
|
56 |
| lam (x::ys) = |
|
57 |
let |
|
29371 | 58 |
(* should use "close_derivation" for thms that are used multiple times *) |
23152 | 59 |
(* it seems to allow for sharing in explicit proof objects *) |
40832 | 60 |
val x' = Thm.close_derivation (k x) |
61 |
val Lx = x' RS cont_L |
|
62 |
in (map (fn y => SOME (k y RS Lx)) ys, x') end |
|
23152 | 63 |
|
64 |
(* first list: cont thm for each dangling bound variable *) |
|
65 |
(* second list: cont thm for each LAM in t *) |
|
66 |
(* if b = false, only return cont thm for outermost LAMs *) |
|
40327 | 67 |
fun cont_thms1 b (Const (@{const_name Rep_cfun}, _) $ f $ t) = |
23152 | 68 |
let |
40832 | 69 |
val (cs1,ls1) = cont_thms1 b f |
70 |
val (cs2,ls2) = cont_thms1 b t |
|
23152 | 71 |
in (zip cs1 cs2, if b then ls1 @ ls2 else []) end |
40327 | 72 |
| cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) = |
23152 | 73 |
let |
40832 | 74 |
val (cs, ls) = cont_thms1 b t |
75 |
val (cs', l) = lam cs |
|
23152 | 76 |
in (cs', l::ls) end |
40327 | 77 |
| cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ t) = |
29373 | 78 |
let |
40832 | 79 |
val t' = Term.incr_boundvars 1 t $ Bound 0 |
80 |
val (cs, ls) = cont_thms1 b t' |
|
81 |
val (cs', l) = lam cs |
|
29373 | 82 |
in (cs', l::ls) end |
23152 | 83 |
| cont_thms1 _ (Bound n) = (var n, []) |
40832 | 84 |
| cont_thms1 _ _ = ([], []) |
23152 | 85 |
in |
86 |
(* precondition: is_lcf_term t = true *) |
|
40832 | 87 |
fun cont_thms t = snd (cont_thms1 false t) |
88 |
fun all_cont_thms t = snd (cont_thms1 true t) |
|
89 |
end |
|
23152 | 90 |
|
91 |
(* |
|
92 |
Given the term "cont f", the procedure tries to construct the |
|
93 |
theorem "cont f == True". If this theorem cannot be completely |
|
94 |
solved by the introduction rules, then the procedure returns a |
|
95 |
conditional rewrite rule with the unsolved subgoals as premises. |
|
96 |
*) |
|
97 |
||
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
98 |
fun cont_tac ctxt = |
29048
0735d0f89172
implement cont_proc theorem cache using theory data
huffman
parents:
29047
diff
changeset
|
99 |
let |
40832 | 100 |
val rules = [cont_K, cont_I, cont_R, cont_A, cont_L] |
23152 | 101 |
|
29662 | 102 |
fun new_cont_tac f' i = |
29048
0735d0f89172
implement cont_proc theorem cache using theory data
huffman
parents:
29047
diff
changeset
|
103 |
case all_cont_thms f' of |
29662 | 104 |
[] => no_tac |
44080
53d95b52954c
HOLCF: fix warnings about unreferenced identifiers
huffman
parents:
42795
diff
changeset
|
105 |
| (c::_) => rtac c i |
23152 | 106 |
|
29048
0735d0f89172
implement cont_proc theorem cache using theory data
huffman
parents:
29047
diff
changeset
|
107 |
fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) = |
0735d0f89172
implement cont_proc theorem cache using theory data
huffman
parents:
29047
diff
changeset
|
108 |
let |
40832 | 109 |
val f' = Const (@{const_name Abs_cfun}, dummyT) $ f |
29048
0735d0f89172
implement cont_proc theorem cache using theory data
huffman
parents:
29047
diff
changeset
|
110 |
in |
0735d0f89172
implement cont_proc theorem cache using theory data
huffman
parents:
29047
diff
changeset
|
111 |
if is_lcf_term f' |
29662 | 112 |
then new_cont_tac f' |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
113 |
else REPEAT_ALL_NEW (resolve_tac ctxt rules) |
29048
0735d0f89172
implement cont_proc theorem cache using theory data
huffman
parents:
29047
diff
changeset
|
114 |
end |
40832 | 115 |
| cont_tac_of_term _ = K no_tac |
29048
0735d0f89172
implement cont_proc theorem cache using theory data
huffman
parents:
29047
diff
changeset
|
116 |
in |
0735d0f89172
implement cont_proc theorem cache using theory data
huffman
parents:
29047
diff
changeset
|
117 |
SUBGOAL (fn (t, i) => |
0735d0f89172
implement cont_proc theorem cache using theory data
huffman
parents:
29047
diff
changeset
|
118 |
cont_tac_of_term (HOLogic.dest_Trueprop t) i) |
40832 | 119 |
end |
23152 | 120 |
|
121 |
local |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46161
diff
changeset
|
122 |
fun solve_cont ctxt t = |
23152 | 123 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46161
diff
changeset
|
124 |
val thy = Proof_Context.theory_of ctxt |
59582 | 125 |
val tr = instantiate' [] [SOME (Thm.cterm_of thy t)] @{thm Eq_TrueI} |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
51717
diff
changeset
|
126 |
in Option.map fst (Seq.pull (cont_tac ctxt 1 tr)) end |
23152 | 127 |
in |
128 |
fun cont_proc thy = |
|
40832 | 129 |
Simplifier.simproc_global thy "cont_proc" ["cont f"] solve_cont |
130 |
end |
|
23152 | 131 |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46161
diff
changeset
|
132 |
fun setup thy = map_theory_simpset (fn ctxt => ctxt addsimprocs [cont_proc thy]) thy |
23152 | 133 |
|
40832 | 134 |
end |