1815 in |
1815 in |
1816 if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE () |
1816 if forall is_good_head main then (side, main, concl) else raise NO_TRIPLE () |
1817 end |
1817 end |
1818 |
1818 |
1819 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb |
1819 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb |
1820 |
|
1821 fun wf_constraint_for rel side concl main = |
1820 fun wf_constraint_for rel side concl main = |
1822 let |
1821 let |
1823 val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main, |
1822 val core = HOLogic.mk_mem (HOLogic.mk_prod |
1824 tuple_for_args concl), Var rel) |
1823 (pairself tuple_for_args (main, concl)), Var rel) |
1825 val t = List.foldl HOLogic.mk_imp core side |
1824 val t = List.foldl HOLogic.mk_imp core side |
1826 val vars = filter (not_equal rel) (Term.add_vars t []) |
1825 val vars = filter_out (curry (op =) rel) (Term.add_vars t []) |
1827 in |
1826 in |
1828 Library.foldl (fn (t', ((x, j), T)) => |
1827 Library.foldl (fn (t', ((x, j), T)) => |
1829 HOLogic.all_const T |
1828 HOLogic.all_const T |
1830 $ Abs (x, T, abstract_over (Var ((x, j), T), t'))) |
1829 $ Abs (x, T, abstract_over (Var ((x, j), T), t'))) |
1831 (t, vars) |
1830 (t, vars) |
1832 end |
1831 end |
1833 |
|
1834 fun wf_constraint_for_triple rel (side, main, concl) = |
1832 fun wf_constraint_for_triple rel (side, main, concl) = |
1835 map (wf_constraint_for rel side concl) main |> foldr1 s_conj |
1833 map (wf_constraint_for rel side concl) main |> foldr1 s_conj |
1836 |
1834 |
1837 fun terminates_by ctxt timeout goal tac = |
1835 fun terminates_by ctxt timeout goal tac = |
1838 can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the |
1836 can (SINGLE (Classical.safe_tac (claset_of ctxt)) #> the |