60 | vc_of (@{term assert_at} $ Free (n, _) $ t) = |
60 | vc_of (@{term assert_at} $ Free (n, _) $ t) = |
61 SOME (Assert ((n, t), True)) |
61 SOME (Assert ((n, t), True)) |
62 | vc_of (@{term HOL.implies} $ @{term True} $ u) = vc_of u |
62 | vc_of (@{term HOL.implies} $ @{term True} $ u) = vc_of u |
63 | vc_of (@{term HOL.implies} $ t $ u) = |
63 | vc_of (@{term HOL.implies} $ t $ u) = |
64 vc_of u |> Option.map (assume t) |
64 vc_of u |> Option.map (assume t) |
65 | vc_of (@{term "op &"} $ (@{term assert_at} $ Free (n, _) $ t) $ u) = |
65 | vc_of (@{term HOL.conj} $ (@{term assert_at} $ Free (n, _) $ t) $ u) = |
66 SOME (vc_of u |> the_default True |> assert (n, t)) |
66 SOME (vc_of u |> the_default True |> assert (n, t)) |
67 | vc_of (@{term "op &"} $ t $ u) = |
67 | vc_of (@{term HOL.conj} $ t $ u) = |
68 (case (vc_of t, vc_of u) of |
68 (case (vc_of t, vc_of u) of |
69 (NONE, r) => r |
69 (NONE, r) => r |
70 | (l, NONE) => l |
70 | (l, NONE) => l |
71 | (SOME lv, SOME rv) => SOME (Choice (lv, rv))) |
71 | (SOME lv, SOME rv) => SOME (Choice (lv, rv))) |
72 | vc_of t = raise TERM ("vc_of_term", [t]) |
72 | vc_of t = raise TERM ("vc_of_term", [t]) |
73 in the_default True o vc_of end |
73 in the_default True o vc_of end |
74 |
74 |
75 val prop_of_vc = |
75 val prop_of_vc = |
76 let |
76 let |
77 fun mk_conj t u = @{term "op &"} $ t $ u |
77 fun mk_conj t u = @{term HOL.conj} $ t $ u |
78 |
78 |
79 fun term_of (Assume (t, v)) = @{term HOL.implies} $ t $ term_of v |
79 fun term_of (Assume (t, v)) = @{term HOL.implies} $ t $ term_of v |
80 | term_of (Assert ((n, t), v)) = |
80 | term_of (Assert ((n, t), v)) = |
81 mk_conj (@{term assert_at} $ Free (n, @{typ bool}) $ t) (term_of v) |
81 mk_conj (@{term assert_at} $ Free (n, @{typ bool}) $ t) (term_of v) |
82 | term_of (Ignore v) = term_of v |
82 | term_of (Ignore v) = term_of v |