src/Pure/Isar/auto_bind.ML
author wenzelm
Fri, 03 Sep 1999 14:52:19 +0200
changeset 7452 c2289eabf706
parent 7331 aee8f76fe54c
child 7474 43cedde6d52a
permissions -rw-r--r--
"this";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6783
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/auto_bind.ML
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
     4
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
     5
Automatic term bindings -- logic specific patterns.
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
     6
*)
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
     7
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
     8
signature AUTO_BIND =
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
     9
sig
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    10
  val goal: term -> (indexname * term) list
6796
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    11
  val facts: string -> term list -> (indexname * term) list
6783
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    12
end;
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    13
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    14
structure AutoBind: AUTO_BIND =
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    15
struct
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    16
6796
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    17
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    18
(* goals *)
6783
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    19
6796
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    20
fun statement_binds (name, prop) =
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    21
  let
7331
aee8f76fe54c ??thesis: include params;
wenzelm
parents: 7048
diff changeset
    22
    val concl = Logic.strip_assums_concl prop;
aee8f76fe54c ??thesis: include params;
wenzelm
parents: 7048
diff changeset
    23
    val parms = Logic.strip_params prop;
aee8f76fe54c ??thesis: include params;
wenzelm
parents: 7048
diff changeset
    24
    fun list_abs tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
aee8f76fe54c ??thesis: include params;
wenzelm
parents: 7048
diff changeset
    25
aee8f76fe54c ??thesis: include params;
wenzelm
parents: 7048
diff changeset
    26
    val env = [(name ^ "_prop", prop), (name ^ "_concl", list_abs concl)] @
aee8f76fe54c ??thesis: include params;
wenzelm
parents: 7048
diff changeset
    27
      (case concl of Const ("Trueprop", _) $ t => [(name, list_abs t)] | _ => []);
6796
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    28
  in map (fn (s, t) => ((Syntax.binding s, 0), t)) env end;
6783
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    29
6796
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    30
fun goal prop = statement_binds ("thesis", prop);
6783
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    31
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    32
6796
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    33
(* facts *)
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    34
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    35
fun dddot_bind prop =
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    36
  (case Logic.strip_imp_concl prop of
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    37
    Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    38
  | _ => []);
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    39
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    40
fun facts _ [] = []
7452
c2289eabf706 "this";
wenzelm
parents: 7331
diff changeset
    41
  | facts name props =
c2289eabf706 "this";
wenzelm
parents: 7331
diff changeset
    42
      let val prop = Library.last_elem props
c2289eabf706 "this";
wenzelm
parents: 7331
diff changeset
    43
      in dddot_bind prop @ statement_binds ("this", prop) end;
6796
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    44
      
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    45
6783
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    46
end;