21 val cont_I = @{thm cont_id} |
21 val cont_I = @{thm cont_id} |
22 val cont_A = @{thm cont2cont_APP} |
22 val cont_A = @{thm cont2cont_APP} |
23 val cont_L = @{thm cont2cont_LAM} |
23 val cont_L = @{thm cont2cont_LAM} |
24 val cont_R = @{thm cont_Rep_cfun2} |
24 val cont_R = @{thm cont_Rep_cfun2} |
25 |
25 |
26 (* checks whether a term contains no dangling bound variables *) |
|
27 fun is_closed_term t = not (Term.loose_bvar (t, 0)) |
|
28 |
|
29 (* checks whether a term is written entirely in the LCF sublanguage *) |
26 (* checks whether a term is written entirely in the LCF sublanguage *) |
30 fun is_lcf_term (Const (@{const_name Rep_cfun}, _) $ t $ u) = |
27 fun is_lcf_term (Const (@{const_name Rep_cfun}, _) $ t $ u) = |
31 is_lcf_term t andalso is_lcf_term u |
28 is_lcf_term t andalso is_lcf_term u |
32 | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) = |
29 | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) = |
33 is_lcf_term t |
30 is_lcf_term t |
34 | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ t) = |
31 | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ t) = |
35 is_lcf_term (Term.incr_boundvars 1 t $ Bound 0) |
32 is_lcf_term (Term.incr_boundvars 1 t $ Bound 0) |
36 | is_lcf_term (Bound _) = true |
33 | is_lcf_term (Bound _) = true |
37 | is_lcf_term t = is_closed_term t |
34 | is_lcf_term t = not (Term.is_open t) |
38 |
35 |
39 (* |
36 (* |
40 efficiently generates a cont thm for every LAM abstraction in a term, |
37 efficiently generates a cont thm for every LAM abstraction in a term, |
41 using forward proof and reusing common subgoals |
38 using forward proof and reusing common subgoals |
42 *) |
39 *) |