src/Pure/Isar/auto_bind.ML
author wenzelm
Sat Jan 06 21:28:30 2001 +0100 (2001-01-06 ago)
changeset 10808 cc4a3ed7e70b
parent 10377 6b595f9ae37e
child 11764 fd780dd6e0b4
permissions -rw-r--r--
added drop_judgment;
wenzelm@6783
     1
(*  Title:      Pure/Isar/auto_bind.ML
wenzelm@6783
     2
    ID:         $Id$
wenzelm@6783
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@8807
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@6783
     5
wenzelm@10359
     6
Logic specific patterns and automatic term bindings.
wenzelm@7675
     7
wenzelm@8227
     8
Note: the current implementation is not quite 'generic', but works
wenzelm@10359
     9
fine with common object-logics (HOL, FOL, ZF etc.).
wenzelm@6783
    10
*)
wenzelm@6783
    11
wenzelm@6783
    12
signature AUTO_BIND =
wenzelm@6783
    13
sig
wenzelm@10359
    14
  val is_judgment: term -> bool
wenzelm@10808
    15
  val drop_judgment: term -> term
wenzelm@10377
    16
  val atomic_judgment: theory -> string -> term
wenzelm@10359
    17
  val add_judgment: bstring * string * mixfix -> theory -> theory
wenzelm@10359
    18
  val add_judgment_i: bstring * typ * mixfix -> theory -> theory
wenzelm@7599
    19
  val goal: term -> (indexname * term option) list
wenzelm@7599
    20
  val facts: string -> term list -> (indexname * term option) list
wenzelm@9296
    21
  val thesisN: string
wenzelm@6783
    22
end;
wenzelm@6783
    23
wenzelm@6783
    24
structure AutoBind: AUTO_BIND =
wenzelm@6783
    25
struct
wenzelm@6783
    26
wenzelm@9464
    27
wenzelm@9464
    28
(** judgments **)
wenzelm@7675
    29
wenzelm@10377
    30
val TruepropN = "Trueprop";
wenzelm@10377
    31
wenzelm@10377
    32
fun is_judgment (Const (c, _) $ _) = c = TruepropN
wenzelm@10377
    33
  | is_judgment _ = false;
wenzelm@10359
    34
wenzelm@10808
    35
fun drop_judgment (Abs (x, T, t)) = Abs (x, T, drop_judgment t)
wenzelm@10808
    36
  | drop_judgment (tm as (Const (c, _) $ t)) = if c = TruepropN then t else tm
wenzelm@10808
    37
  | drop_judgment tm = tm;
wenzelm@10808
    38
wenzelm@10808
    39
val strip_judgment = drop_judgment o Logic.strip_assums_concl;
wenzelm@10808
    40
wenzelm@10377
    41
fun atomic_judgment thy x =
wenzelm@10377
    42
  let  (*be robust wrt. low-level errors*)
wenzelm@10377
    43
    val aT = TFree ("'a", logicS);
wenzelm@10377
    44
    val T =
wenzelm@10377
    45
      if_none (Sign.const_type (Theory.sign_of thy) TruepropN) (aT --> propT)
wenzelm@10377
    46
      |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
wenzelm@10377
    47
    val U = Term.domain_type T handle Match => aT;
wenzelm@10377
    48
  in Const (TruepropN, T) $ Free (x, U) end;
wenzelm@8227
    49
wenzelm@8227
    50
wenzelm@9464
    51
fun gen_add_judgment add (name, T, syn) thy =
wenzelm@10377
    52
  if name = TruepropN then
wenzelm@9464
    53
    thy |> PureThy.global_path |> add [(name, T, syn)] |> PureThy.local_path
wenzelm@10377
    54
  else error ("Judgment name has to be " ^ quote TruepropN);
wenzelm@8227
    55
wenzelm@8227
    56
val add_judgment = gen_add_judgment Theory.add_consts;
wenzelm@8227
    57
val add_judgment_i = gen_add_judgment Theory.add_consts_i;
wenzelm@8227
    58
wenzelm@6796
    59
wenzelm@10359
    60
wenzelm@10359
    61
(** bindings **)
wenzelm@10359
    62
wenzelm@10359
    63
val thesisN = "thesis";
wenzelm@10359
    64
val thisN = "this";
wenzelm@10359
    65
wenzelm@10359
    66
fun statement_binds name prop =
wenzelm@10808
    67
  [((name, 0), Some (Term.list_abs (Logic.strip_params prop, strip_judgment prop)))];
wenzelm@10359
    68
wenzelm@10359
    69
wenzelm@10359
    70
(* goal *)
wenzelm@10359
    71
wenzelm@10359
    72
fun goal prop = statement_binds thesisN prop;
wenzelm@10359
    73
wenzelm@10359
    74
wenzelm@10359
    75
(* facts *)
wenzelm@10359
    76
wenzelm@10359
    77
fun get_arg prop =
wenzelm@10359
    78
  (case strip_judgment prop of
wenzelm@10808
    79
    _ $ t => Some (Term.list_abs (Logic.strip_params prop, t))
wenzelm@10359
    80
  | _ => None);
wenzelm@10359
    81
wenzelm@10359
    82
fun facts _ [] = []
wenzelm@10359
    83
  | facts name props =
wenzelm@10359
    84
      let val prop = Library.last_elem props
wenzelm@10359
    85
      in [(Syntax.dddot_indexname, get_arg prop)] @ statement_binds thisN prop end;
wenzelm@10359
    86
wenzelm@10808
    87
wenzelm@6783
    88
end;