7 

     8 thm LAMBDA_PRS

     9 

    10 ML {*

    11 let

    12    val parser = Args.context -- Scan.lift Args.name_source

    13    fun term_pat (ctxt, str) =

    14       str |> ProofContext.read_term_pattern ctxt

    15           |> ML_Syntax.print_term

    16           |> ML_Syntax.atomic

    17 in

    18    ML_Antiquote.inline "term_pat" (parser >> term_pat)

    19 end

    20 *}

    21 

    22 ML {*

    23 fun make_inst lhs t =

    24   let

    25     val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;

    26     val _ $ (Abs (_, _, g)) = t;

    27     fun mk_abs i t =

    28       if incr_boundvars i u aconv t then Bound i

    29       else (case t of

    30         t1 $ t2 => mk_abs i t1 $ mk_abs i t2

    31       | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')

    32       | Bound j => if i = j then error "make_inst" else t

    33       | _ => t);

    34   in (f, Abs ("x", T, mk_abs 0 g)) end;

    35 *}

    36 

    37 ML {* 

    38   val trm1 = @{term_pat "(P::(nat\<Rightarrow>bool)\<Rightarrow>bool) (\<lambda>(x::nat). (?f ((g::nat\<Rightarrow>nat) x)))"}; 

    39   val trm2 = @{term_pat "(P::(nat\<Rightarrow>bool)\<Rightarrow>bool) (\<lambda>(x::nat). (h (g x) ((g::nat\<Rightarrow>nat) x)))"}

    40 *}

    41 

    42 ML {*

    43 fun test trm =

    44   case trm of

    45   (_ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u))) => (1,f)

    46   | (_ $ (Abs (_, _, (f as (Var (_, _)) $ u)))) => (2,f)

    47   | (_ $ (Abs (_, _, (f $ u)))) => (3,f)

    48 *}

    49 

    50 ML {* test trm1 *}

    51 

    52 ML {*

    53  make_inst trm1 trm2

    54   |> pairself (Syntax.string_of_term @{context})

    55   |> pairself writeln

    56 *}

    57 

    58 

    59