author | haftmann |
Sun, 23 Jul 2006 07:21:41 +0200 | |
changeset 20187 | af47971ea304 |
parent 19594 | a1e630503c57 |
permissions | -rw-r--r-- |
16386 | 1 |
(* Title: HOLCF/cont_proc.ML |
2 |
ID: $Id$ |
|
3 |
Author: Brian Huffman |
|
4 |
*) |
|
5 |
||
6 |
signature CONT_PROC = |
|
7 |
sig |
|
8 |
val is_lcf_term: term -> bool |
|
9 |
val cont_thms: term -> thm list |
|
16403 | 10 |
val all_cont_thms: term -> thm list |
16629 | 11 |
val cont_tac: int -> tactic |
16386 | 12 |
val cont_proc: theory -> simproc |
18708 | 13 |
val setup: theory -> theory |
16386 | 14 |
end; |
15 |
||
16 |
structure ContProc: CONT_PROC = |
|
17 |
struct |
|
18 |
||
19 |
(** theory context references **) |
|
20 |
||
21 |
val cont_K = thm "cont_const"; |
|
22 |
val cont_I = thm "cont_id"; |
|
23 |
val cont_A = thm "cont2cont_Rep_CFun"; |
|
24 |
val cont_L = thm "cont2cont_LAM"; |
|
25 |
val cont_R = thm "cont_Rep_CFun2"; |
|
26 |
||
19594
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
27 |
(* checks whether a term contains no dangling bound variables *) |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
28 |
val is_closed_term = |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
29 |
let |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
30 |
fun bound_less i (t $ u) = |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
31 |
bound_less i t andalso bound_less i u |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
32 |
| bound_less i (Abs (_, _, t)) = bound_less (i+1) t |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
33 |
| bound_less i (Bound n) = n < i |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
34 |
| bound_less i _ = true; (* Const, Free, and Var are OK *) |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
35 |
in bound_less 0 end; |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
36 |
|
16386 | 37 |
(* checks whether a term is written entirely in the LCF sublanguage *) |
19594
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
38 |
fun is_lcf_term (Const ("Cfun.Rep_CFun", _) $ t $ u) = |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
39 |
is_lcf_term t andalso is_lcf_term u |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
40 |
| is_lcf_term (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) = is_lcf_term t |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
41 |
| is_lcf_term (Const ("Cfun.Abs_CFun", _) $ _) = false |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
42 |
| is_lcf_term (Bound _) = true |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
43 |
| is_lcf_term t = is_closed_term t; |
16386 | 44 |
|
45 |
(* |
|
46 |
efficiently generates a cont thm for every LAM abstraction in a term, |
|
47 |
using forward proof and reusing common subgoals |
|
48 |
*) |
|
49 |
local |
|
50 |
fun var 0 = [SOME cont_I] |
|
51 |
| var n = NONE :: var (n-1); |
|
52 |
||
53 |
fun k NONE = cont_K |
|
54 |
| k (SOME x) = x; |
|
55 |
||
56 |
fun ap NONE NONE = NONE |
|
57 |
| ap x y = SOME (k y RS (k x RS cont_A)); |
|
58 |
||
59 |
fun zip [] [] = [] |
|
60 |
| zip [] (y::ys) = (ap NONE y ) :: zip [] ys |
|
61 |
| zip (x::xs) [] = (ap x NONE) :: zip xs [] |
|
62 |
| zip (x::xs) (y::ys) = (ap x y ) :: zip xs ys |
|
63 |
||
64 |
fun lam [] = ([], cont_K) |
|
19594
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
65 |
| lam (x::ys) = |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
66 |
let |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
67 |
(* should use "standard" for thms that are used multiple times *) |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
68 |
(* it seems to allow for sharing in explicit proof objects *) |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
69 |
val x' = standard (k x); |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
70 |
val Lx = x' RS cont_L; |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
71 |
in (map (fn y => SOME (k y RS Lx)) ys, x') end; |
16386 | 72 |
|
73 |
(* first list: cont thm for each dangling bound variable *) |
|
16403 | 74 |
(* second list: cont thm for each LAM in t *) |
75 |
(* if b = false, only return cont thm for outermost LAMs *) |
|
19594
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
76 |
fun cont_thms1 b (Const ("Cfun.Rep_CFun", _) $ f $ t) = |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
77 |
let |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
78 |
val (cs1,ls1) = cont_thms1 b f; |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
79 |
val (cs2,ls2) = cont_thms1 b t; |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
80 |
in (zip cs1 cs2, if b then ls1 @ ls2 else []) end |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
81 |
| cont_thms1 b (Const ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) = |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
82 |
let |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
83 |
val (cs, ls) = cont_thms1 b t; |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
84 |
val (cs', l) = lam cs; |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
85 |
in (cs', l::ls) end |
16403 | 86 |
| cont_thms1 _ (Bound n) = (var n, []) |
19594
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
87 |
| cont_thms1 _ _ = ([], []); |
16386 | 88 |
in |
89 |
(* precondition: is_lcf_term t = true *) |
|
16403 | 90 |
fun cont_thms t = snd (cont_thms1 false t); |
91 |
fun all_cont_thms t = snd (cont_thms1 true t); |
|
16386 | 92 |
end; |
93 |
||
94 |
(* |
|
95 |
Given the term "cont f", the procedure tries to construct the |
|
96 |
theorem "cont f == True". If this theorem cannot be completely |
|
97 |
solved by the introduction rules, then the procedure returns a |
|
98 |
conditional rewrite rule with the unsolved subgoals as premises. |
|
99 |
*) |
|
100 |
||
101 |
local |
|
16629 | 102 |
val rules = [cont_K, cont_I, cont_R, cont_A, cont_L]; |
103 |
||
19594
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
104 |
val prev_cont_thms : thm list ref = ref []; |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
105 |
|
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
106 |
fun old_cont_tac i thm = |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
107 |
case !prev_cont_thms of |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
108 |
[] => no_tac thm |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
109 |
| (c::cs) => (prev_cont_thms := cs; rtac c i thm); |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
110 |
|
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
111 |
fun new_cont_tac f' i thm = |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
112 |
case all_cont_thms f' of |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
113 |
[] => no_tac thm |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
114 |
| (c::cs) => (prev_cont_thms := cs; rtac c i thm); |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
115 |
|
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
116 |
fun cont_tac_of_term (Const ("Cont.cont", _) $ f) = |
16386 | 117 |
let |
19594
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
118 |
val f' = Const ("Cfun.Abs_CFun", dummyT) $ f; |
16629 | 119 |
in |
120 |
if is_lcf_term f' |
|
19594
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
121 |
then old_cont_tac ORELSE' new_cont_tac f' |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
122 |
else REPEAT_ALL_NEW (resolve_tac rules) |
16629 | 123 |
end |
124 |
| cont_tac_of_term _ = K no_tac; |
|
16386 | 125 |
in |
19594
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
126 |
val cont_tac = |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
127 |
SUBGOAL (fn (t, i) => cont_tac_of_term (HOLogic.dest_Trueprop t) i); |
16629 | 128 |
end; |
129 |
||
130 |
local |
|
131 |
fun solve_cont thy _ t = |
|
132 |
let |
|
133 |
val tr = instantiate' [] [SOME (cterm_of thy t)] Eq_TrueI; |
|
134 |
in Option.map fst (Seq.pull (cont_tac 1 tr)) end |
|
135 |
in |
|
19594
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
136 |
fun cont_proc thy = |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
137 |
Simplifier.simproc thy "cont_proc" ["cont f"] solve_cont; |
16386 | 138 |
end; |
139 |
||
140 |
val setup = |
|
19594
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
141 |
(fn thy => |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
142 |
(Simplifier.change_simpset_of thy |
a1e630503c57
speed improvements: expand LCF sublanguage to recognize any constant subterm; also add memoization to cont_tac
huffman
parents:
18708
diff
changeset
|
143 |
(fn ss => ss addsimprocs [cont_proc thy]); thy)); |
16386 | 144 |
|
145 |
end; |