src/Pure/Isar/auto_bind.ML
author wenzelm
Mon, 19 Jul 1999 21:26:33 +0200
changeset 7048 3535eec33c50
parent 6796 c2e5cb8cd50d
child 7331 aee8f76fe54c
permissions -rw-r--r--
facts: no statement_binds;
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
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    22
    val concl = Logic.strip_imp_concl prop;
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    23
    val env = [(name ^ "_prop", prop), (name ^ "_concl", concl)] @
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    24
      (case concl of Const ("Trueprop", _) $ t => [(name, t)] | _ => []);
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    25
  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
    26
6796
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    27
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
    28
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
(* facts *)
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    31
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    32
fun dddot_bind prop =
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    33
  (case Logic.strip_imp_concl prop of
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    34
    Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    35
  | _ => []);
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    36
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    37
fun facts _ [] = []
7048
3535eec33c50 facts: no statement_binds;
wenzelm
parents: 6796
diff changeset
    38
  | facts name [prop] = dddot_bind prop
3535eec33c50 facts: no statement_binds;
wenzelm
parents: 6796
diff changeset
    39
  | facts name props =  dddot_bind (Library.last_elem props);
6796
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    40
      
c2e5cb8cd50d facts: bind named props (from proof.ML/let_thms);
wenzelm
parents: 6783
diff changeset
    41
6783
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    42
end;