5 |
5 |
6 signature CONT_PROC = |
6 signature CONT_PROC = |
7 sig |
7 sig |
8 val is_lcf_term: term -> bool |
8 val is_lcf_term: term -> bool |
9 val cont_thms: term -> thm list |
9 val cont_thms: term -> thm list |
|
10 val all_cont_thms: term -> thm list |
10 val cont_proc: theory -> simproc |
11 val cont_proc: theory -> simproc |
11 val setup: (theory -> theory) list |
12 val setup: (theory -> theory) list |
12 end; |
13 end; |
13 |
14 |
14 structure ContProc: CONT_PROC = |
15 structure ContProc: CONT_PROC = |
55 val x' = standard (k x); |
56 val x' = standard (k x); |
56 val Lx = x' RS cont_L; |
57 val Lx = x' RS cont_L; |
57 in (map (fn y => SOME (k y RS Lx)) ys, x') end; |
58 in (map (fn y => SOME (k y RS Lx)) ys, x') end; |
58 |
59 |
59 (* first list: cont thm for each dangling bound variable *) |
60 (* first list: cont thm for each dangling bound variable *) |
60 (* second list: cont thm for each LAM *) |
61 (* second list: cont thm for each LAM in t *) |
61 fun cont_thms1 (Const _ $ f $ t) = let |
62 (* if b = false, only return cont thm for outermost LAMs *) |
62 val (cs1,ls1) = cont_thms1 f; |
63 fun cont_thms1 b (Const _ $ f $ t) = let |
63 val (cs2,ls2) = cont_thms1 t; |
64 val (cs1,ls1) = cont_thms1 b f; |
64 in (zip cs1 cs2, ls1 @ ls2) end |
65 val (cs2,ls2) = cont_thms1 b t; |
65 | cont_thms1 (Const _ $ Abs (_,_,t)) = let |
66 in (zip cs1 cs2, if b then ls1 @ ls2 else []) end |
66 val (cs,ls) = cont_thms1 t; |
67 | cont_thms1 b (Const _ $ Abs (_,_,t)) = let |
|
68 val (cs,ls) = cont_thms1 b t; |
67 val (cs',l) = lam cs; |
69 val (cs',l) = lam cs; |
68 in (cs',l::ls) end |
70 in (cs',l::ls) end |
69 | cont_thms1 (Bound n) = (var n, []) |
71 | cont_thms1 _ (Bound n) = (var n, []) |
70 | cont_thms1 _ = ([],[]); |
72 | cont_thms1 _ _ = ([],[]); |
71 in |
73 in |
72 (* precondition: is_lcf_term t = true *) |
74 (* precondition: is_lcf_term t = true *) |
73 fun cont_thms t = snd (cont_thms1 t); |
75 fun cont_thms t = snd (cont_thms1 false t); |
|
76 fun all_cont_thms t = snd (cont_thms1 true t); |
74 end; |
77 end; |
75 |
78 |
76 (* |
79 (* |
77 Given the term "cont f", the procedure tries to construct the |
80 Given the term "cont f", the procedure tries to construct the |
78 theorem "cont f == True". If this theorem cannot be completely |
81 theorem "cont f == True". If this theorem cannot be completely |