[7cfccc]: thys / Recursion-Theory-I / Utils.ML  Maximize  Restore  History

Download this file

79 lines (61 with data), 2.5 kB

(*  Title:      Recursion-Theory-I/Utils.ML
    Author:     Michael Nedzelsky, email: MichaelNedzelsky <at> yandex <dot> ru

Some utilities for work with primitive recursive functions.
*)

(******** Utility functions. ***************)

exception BadArgument

fun extract_prop_arg (Const ("prop", _) $ t)  = t
  | extract_prop_arg  _ = raise BadArgument

fun extract_trueprop_arg (Const ("Trueprop", _) $ t)  = t
  | extract_trueprop_arg  _ = raise BadArgument

fun extract_set_args (Const (@{const_name Set.member}, _) $ t1 $ t2)  = (t1, t2)
  | extract_set_args  _ = raise BadArgument

fun get_num_by_set "PRecFun.PrimRec1" = 1
  | get_num_by_set "PRecFun.PrimRec2" = 2
  | get_num_by_set "PRecFun.PrimRec3" = 3
  | get_num_by_set _ = raise BadArgument

fun remove_abs (Abs (_, _, t)) = remove_abs t
  | remove_abs t = t

fun extract_free_from_app (t1 $ t2) (n:int) = extract_free_from_app t1 (n+1)
  | extract_free_from_app (Free (s, tp)) n = (s, tp, n)
  | extract_free_from_app (Const (s, tp)) n = (s, tp, n)
  | extract_free_from_app _ n = raise BadArgument

fun extract_free_arg t = extract_free_from_app (remove_abs t) 0

fun get_comp_by_indexes (1,1) = @{thm pr_comp1_1}
  | get_comp_by_indexes (1,2) = @{thm pr_comp1_2}
  | get_comp_by_indexes (1,3) = @{thm pr_comp1_3}
  | get_comp_by_indexes (2,1) = @{thm pr_comp2_1}
  | get_comp_by_indexes (2,2) = @{thm pr_comp2_2}
  | get_comp_by_indexes (2,3) = @{thm pr_comp2_3}
  | get_comp_by_indexes (3,1) = @{thm pr_comp3_1}
  | get_comp_by_indexes (3,2) = @{thm pr_comp3_2}
  | get_comp_by_indexes (3,3) = @{thm pr_comp3_3}
  | get_comp_by_indexes _ = raise BadArgument

(* t = [Cons ("==>", tp)...] $ ... *)
fun is_impl_first (Const("==>",_) $ _) = true
  | is_impl_first _ = false

(* Result = Cons("Trueprop", tp) $ ... *)
fun extract_right_expr (t:term) =
  case t of
      t1 $ t2 => (if (is_impl_first t1) then (extract_right_expr t2) else t)
    | _ => t


(************ Tactic. ***************)

fun pr_comp_tac ctxt = SUBGOAL (fn (t,i) =>
  let
    val t = extract_trueprop_arg (extract_right_expr t)
    val (t1, t2) = extract_set_args t
    val n2 =
      let
        val Const(s, _) = t2
      in
        get_num_by_set s
      end
    val (name, _, n1) = extract_free_arg t1
    val comp = get_comp_by_indexes (n1, n2)
  in
    res_inst_tac ctxt [(("f", 0), ProofContext.revert_skolem ctxt name)] comp i
  end
  handle BadArgument => no_tac)

fun prec0_tac ctxt facts i =
  Method.insert_tac facts i THEN
  REPEAT (assume_tac i ORELSE pr_comp_tac ctxt i)

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks