352 val (ctxt', _, cases, concl) = dest_hhf ctxt t |
352 val (ctxt', _, cases, concl) = dest_hhf ctxt t |
353 val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl |
353 val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl |
354 val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt' |
354 val ([Rn,xn], ctxt'') = Variable.variant_fixes ["R","x"] ctxt' |
355 val R = Free (Rn, mk_relT ST) |
355 val R = Free (Rn, mk_relT ST) |
356 val x = Free (xn, ST) |
356 val x = Free (xn, ST) |
357 val cert = cterm_of (Proof_Context.theory_of ctxt) |
357 val cert = Proof_Context.cterm_of ctxt |
358 |
358 |
359 val ineqss = mk_ineqs R scheme |> map (map (apply2 (Thm.assume o cert))) |
359 val ineqss = mk_ineqs R scheme |> map (map (apply2 (Thm.assume o cert))) |
360 val complete = |
360 val complete = |
361 map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches) |
361 map_range (mk_completeness ctxt scheme #> cert #> Thm.assume) (length branches) |
362 val wf_thm = mk_wf R scheme |> cert |> Thm.assume |
362 val wf_thm = mk_wf R scheme |> cert |> Thm.assume |