equal
deleted
inserted
replaced
16 |
16 |
17 fun mk_is_measure t = |
17 fun mk_is_measure t = |
18 Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t |
18 Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t |
19 |
19 |
20 fun find_measures ctxt T = |
20 fun find_measures ctxt T = |
21 DEPTH_SOLVE (resolve_tac (rev (Named_Theorems.get ctxt @{named_theorems measure_function})) 1) |
21 DEPTH_SOLVE (resolve_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems measure_function})) 1) |
22 (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT))) |
22 (HOLogic.mk_Trueprop (mk_is_measure (Var (("f",0), T --> HOLogic.natT))) |
23 |> cterm_of (Proof_Context.theory_of ctxt) |> Goal.init) |
23 |> cterm_of (Proof_Context.theory_of ctxt) |> Goal.init) |
24 |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f)) |
24 |> Seq.map (prop_of #> (fn _ $ (_ $ (_ $ f)) => f)) |
25 |> Seq.list_of |
25 |> Seq.list_of |
26 |
26 |