src/Pure/Isar/auto_bind.ML
author wenzelm
Sat, 21 Jan 2006 23:02:14 +0100
changeset 18728 6790126ab5f6
parent 18605 b971e113dee7
child 19075 12833c7e0fa6
permissions -rw-r--r--
simplified type attribute;
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
17349
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
     5
Automatic bindings of Isar text elements.
6783
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
17349
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    10
  val rule_contextN: string
9296
0d2b31e1ea1b export thesisN separately;
wenzelm
parents: 8807
diff changeset
    11
  val thesisN: string
17349
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    12
  val thisN: string
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    13
  val goal: theory -> term list -> (indexname * term option) list
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    14
  val cases: theory -> term list -> (string * RuleCases.T option) list
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    15
  val facts: theory -> term list -> (indexname * term option) list
17852
a06b185a26d7 added no_facts;
wenzelm
parents: 17349
diff changeset
    16
  val no_facts: (indexname * term option) list
6783
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    17
end;
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    18
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    19
structure AutoBind: AUTO_BIND =
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    20
struct
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    21
10359
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    22
(** bindings **)
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    23
17349
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    24
val rule_contextN = "rule_context";
10359
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    25
val thesisN = "thesis";
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    26
val thisN = "this";
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    27
17349
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    28
fun strip_judgment thy = ObjectLogic.drop_judgment thy o Logic.strip_assums_concl;
11764
fd780dd6e0b4 use ObjectLogic;
wenzelm
parents: 10808
diff changeset
    29
17349
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    30
fun statement_binds thy name prop =
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    31
  [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
10359
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    32
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    33
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    34
(* goal *)
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    35
17349
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    36
fun goal thy [prop] = statement_binds thy thesisN prop
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    37
  | goal _ _ = [((thesisN, 0), NONE)];
10359
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    38
18605
b971e113dee7 RuleCases.make_simple;
wenzelm
parents: 18472
diff changeset
    39
fun cases thy [prop] = RuleCases.make_simple true (thy, prop) rule_contextN
b971e113dee7 RuleCases.make_simple;
wenzelm
parents: 18472
diff changeset
    40
  | cases _ _ = [(rule_contextN, NONE)];
17349
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    41
10359
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    42
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    43
(* facts *)
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    44
17349
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    45
fun get_arg thy prop =
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    46
  (case strip_judgment thy prop of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    47
    _ $ t => SOME (Term.list_abs (Logic.strip_params prop, t))
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 14981
diff changeset
    48
  | _ => NONE);
10359
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    49
12140
a987beab002d facts: multiple args;
wenzelm
parents: 11764
diff changeset
    50
fun facts _ [] = []
17349
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    51
  | facts thy props =
10359
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    52
      let val prop = Library.last_elem props
17349
03fafcdfdfa7 added cases, rule_contextN;
wenzelm
parents: 15531
diff changeset
    53
      in [(Syntax.dddot_indexname, get_arg thy prop)] @ statement_binds thy thisN prop end;
10359
445e3b87f28b improved statement bindings for props;
wenzelm
parents: 9464
diff changeset
    54
17852
a06b185a26d7 added no_facts;
wenzelm
parents: 17349
diff changeset
    55
val no_facts = [(Syntax.dddot_indexname, NONE), ((thisN, 0), NONE)];
10808
cc4a3ed7e70b added drop_judgment;
wenzelm
parents: 10377
diff changeset
    56
6783
9cf9c17d9e35 renamed object_logic.ML to Isar/auto_bind.ML and tuned this module;
wenzelm
parents:
diff changeset
    57
end;