src/Pure/Isar/element.ML
author ballarin
Wed, 19 Nov 2008 17:00:00 +0100
changeset 28850 6882e110c29a
parent 28832 cf7237498e7a
child 28862 53f13f763d4f
permissions -rw-r--r--
Basic types not qualified.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/element.ML
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
     4
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
     5
Explicit data structures for some Isar language elements, with derived
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
     6
logical operations.
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
     7
*)
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
     8
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
     9
signature ELEMENT =
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    10
sig
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    11
  datatype ('typ, 'term) stmt =
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    12
    Shows of (Attrib.binding * ('term * 'term list) list) list |
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
    13
    Obtains of (Name.binding * ((Name.binding * 'typ option) list * 'term list)) list
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25739
diff changeset
    14
  type statement = (string, string) stmt
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25739
diff changeset
    15
  type statement_i = (typ, term) stmt
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    16
  datatype ('typ, 'term, 'fact) ctxt =
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
    17
    Fixes of (Name.binding * 'typ option * mixfix) list |
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    18
    Constrains of (string * 'typ) list |
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    19
    Assumes of (Attrib.binding * ('term * 'term list) list) list |
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    20
    Defines of (Attrib.binding * ('term * 'term list)) list |
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    21
    Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25739
diff changeset
    22
  type context = (string, string, Facts.ref) ctxt
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25739
diff changeset
    23
  type context_i = (typ, term, thm list) ctxt
21581
7799b1739a51 added facts_map;
wenzelm
parents: 21528
diff changeset
    24
  val facts_map: (('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt) ->
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    25
   (Attrib.binding * ('fact * Attrib.src list) list) list ->
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    26
   (Attrib.binding * ('c * Attrib.src list) list) list
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
    27
  val map_ctxt: {name: Name.binding -> Name.binding,
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
    28
    var: Name.binding * mixfix -> Name.binding * mixfix,
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    29
    typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    30
    attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
21528
84e98b5f5af0 added map_ctxt_attrib;
wenzelm
parents: 21521
diff changeset
    31
  val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
84e98b5f5af0 added map_ctxt_attrib;
wenzelm
parents: 21521
diff changeset
    32
    ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
21481
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
    33
  val morph_ctxt: morphism -> context_i -> context_i
19808
396dd23c54ef added facts_of;
wenzelm
parents: 19777
diff changeset
    34
  val params_of: context_i -> (string * typ) list
396dd23c54ef added facts_of;
wenzelm
parents: 19777
diff changeset
    35
  val prems_of: context_i -> term list
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    36
  val facts_of: theory -> context_i -> (Attrib.binding * (thm list * Attrib.src list) list) list
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    37
  val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    38
  val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    39
  val pretty_statement: Proof.context -> string -> thm -> Pretty.T
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    40
  type witness
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    41
  val map_witness: (term * thm -> term * thm) -> witness -> witness
21481
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
    42
  val morph_witness: morphism -> witness -> witness
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    43
  val witness_prop: witness -> term
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    44
  val witness_hyps: witness -> term list
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    45
  val assume_witness: theory -> term -> witness
20058
7d035e26e5f9 prove_witness: context;
wenzelm
parents: 20007
diff changeset
    46
  val prove_witness: Proof.context -> term -> tactic -> witness
25624
04b67ee73327 added close_witness;
wenzelm
parents: 25302
diff changeset
    47
  val close_witness: witness -> witness
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    48
  val conclude_witness: witness -> thm
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    49
  val mark_witness: term -> term
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    50
  val make_witness: term -> thm -> witness
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19897
diff changeset
    51
  val dest_witness: witness -> term * thm
20068
19c7361db4a3 New function transfer_witness lifting Thm.transfer to witnesses.
ballarin
parents: 20058
diff changeset
    52
  val transfer_witness: theory -> witness -> witness
19808
396dd23c54ef added facts_of;
wenzelm
parents: 19777
diff changeset
    53
  val refine_witness: Proof.state -> Proof.state Seq.seq
22658
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22568
diff changeset
    54
  val pretty_witness: Proof.context -> witness -> Pretty.T
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    55
  val rename: (string * (string * mixfix option)) list -> string -> string
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
    56
  val rename_var_name: (string * (string * mixfix option)) list ->
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
    57
    string * mixfix -> string * mixfix
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
    58
  val rename_var: (string * (string * mixfix option)) list ->
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
    59
    Name.binding * mixfix -> Name.binding * mixfix
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    60
  val rename_term: (string * (string * mixfix option)) list -> term -> term
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    61
  val rename_thm: (string * (string * mixfix option)) list -> thm -> thm
21481
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
    62
  val rename_morphism: (string * (string * mixfix option)) list -> morphism
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    63
  val instT_type: typ Symtab.table -> typ -> typ
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    64
  val instT_term: typ Symtab.table -> term -> term
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    65
  val instT_thm: theory -> typ Symtab.table -> thm -> thm
21481
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
    66
  val instT_morphism: theory -> typ Symtab.table -> morphism
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    67
  val inst_term: typ Symtab.table * term Symtab.table -> term -> term
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    68
  val inst_thm: theory -> typ Symtab.table * term Symtab.table -> thm -> thm
21481
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
    69
  val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    70
  val satisfy_thm: witness list -> thm -> thm
21481
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
    71
  val satisfy_morphism: witness list -> morphism
20264
f09a4003e12d added generalize_facts;
wenzelm
parents: 20233
diff changeset
    72
  val satisfy_facts: witness list ->
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    73
    (Attrib.binding * (thm list * Attrib.src list) list) list ->
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    74
    (Attrib.binding * (thm list * Attrib.src list) list) list
21581
7799b1739a51 added facts_map;
wenzelm
parents: 21528
diff changeset
    75
  val generalize_facts: Proof.context -> Proof.context ->
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    76
    (Attrib.binding * (thm list * Attrib.src list) list) list ->
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    77
    (Attrib.binding * (thm list * Attrib.src list) list) list
28850
6882e110c29a Basic types not qualified.
ballarin
parents: 28832
diff changeset
    78
  val activate: (typ, term, Facts.ref) ctxt list -> Proof.context ->
28832
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
    79
    (context_i list * (Name.binding * Thm.thm list) list) * Proof.context
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
    80
  val activate_i: context_i list -> Proof.context ->
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
    81
    (context_i list * (Name.binding * Thm.thm list) list) * Proof.context
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    82
end;
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    83
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    84
structure Element: ELEMENT =
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    85
struct
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    86
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    87
(** language elements **)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    88
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    89
(* statement *)
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    90
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    91
datatype ('typ, 'term) stmt =
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    92
  Shows of (Attrib.binding * ('term * 'term list) list) list |
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
    93
  Obtains of (Name.binding * ((Name.binding * 'typ option) list * 'term list)) list;
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    94
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    95
type statement = (string, string) stmt;
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    96
type statement_i = (typ, term) stmt;
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    97
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    98
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    99
(* context *)
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   100
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   101
datatype ('typ, 'term, 'fact) ctxt =
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   102
  Fixes of (Name.binding * 'typ option * mixfix) list |
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   103
  Constrains of (string * 'typ) list |
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
   104
  Assumes of (Attrib.binding * ('term * 'term list) list) list |
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
   105
  Defines of (Attrib.binding * ('term * 'term list)) list |
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
   106
  Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list;
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   107
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25739
diff changeset
   108
type context = (string, string, Facts.ref) ctxt;
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   109
type context_i = (typ, term, thm list) ctxt;
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   110
21581
7799b1739a51 added facts_map;
wenzelm
parents: 21528
diff changeset
   111
fun facts_map f facts = Notes ("", facts) |> f |> (fn Notes (_, facts') => facts');
7799b1739a51 added facts_map;
wenzelm
parents: 21528
diff changeset
   112
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   113
fun map_ctxt {name, var, typ, term, fact, attrib} =
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   114
  fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   115
       let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   116
   | Constrains xs => Constrains (xs |> map (fn (x, T) =>
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   117
       let val x' = Name.name_of (#1 (var (Name.binding x, NoSyn))) in (x', typ T) end))
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   118
   | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
19585
70a1ce3b23ae removed 'concl is' patterns;
wenzelm
parents: 19482
diff changeset
   119
      ((name a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   120
   | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   121
      ((name a, map attrib atts), (term t, map term ps))))
21440
807a39221a58 notes: proper kind;
wenzelm
parents: 21032
diff changeset
   122
   | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   123
      ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   124
21528
84e98b5f5af0 added map_ctxt_attrib;
wenzelm
parents: 21521
diff changeset
   125
fun map_ctxt_attrib attrib =
84e98b5f5af0 added map_ctxt_attrib;
wenzelm
parents: 21521
diff changeset
   126
  map_ctxt {name = I, var = I, typ = I, term = I, fact = I, attrib = attrib};
84e98b5f5af0 added map_ctxt_attrib;
wenzelm
parents: 21521
diff changeset
   127
21481
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
   128
fun morph_ctxt phi = map_ctxt
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
   129
 {name = Morphism.name phi,
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
   130
  var = Morphism.var phi,
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
   131
  typ = Morphism.typ phi,
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
   132
  term = Morphism.term phi,
21521
095f4963beed simultaneous fact morphism;
wenzelm
parents: 21497
diff changeset
   133
  fact = Morphism.fact phi,
21481
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
   134
  attrib = Args.morph_values phi};
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   135
19808
396dd23c54ef added facts_of;
wenzelm
parents: 19777
diff changeset
   136
396dd23c54ef added facts_of;
wenzelm
parents: 19777
diff changeset
   137
(* logical content *)
396dd23c54ef added facts_of;
wenzelm
parents: 19777
diff changeset
   138
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   139
fun params_of (Fixes fixes) = fixes |> map
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   140
    (fn (x, SOME T, _) => (Name.name_of x, T)
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   141
      | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Name.name_of x), []))
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   142
  | params_of _ = [];
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   143
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   144
fun prems_of (Assumes asms) = maps (map fst o snd) asms
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   145
  | prems_of (Defines defs) = map (fst o snd) defs
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   146
  | prems_of _ = [];
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   147
20233
ece639738db3 Assumption.assume;
wenzelm
parents: 20218
diff changeset
   148
fun assume thy t = Assumption.assume (Thm.cterm_of thy t);
19808
396dd23c54ef added facts_of;
wenzelm
parents: 19777
diff changeset
   149
396dd23c54ef added facts_of;
wenzelm
parents: 19777
diff changeset
   150
fun facts_of thy (Assumes asms) = map (apsnd (map (fn (t, _) => ([assume thy t], [])))) asms
396dd23c54ef added facts_of;
wenzelm
parents: 19777
diff changeset
   151
  | facts_of thy (Defines defs) = map (apsnd (fn (t, _) => [([assume thy t], [])])) defs
21440
807a39221a58 notes: proper kind;
wenzelm
parents: 21032
diff changeset
   152
  | facts_of _ (Notes (_, facts)) = facts
19808
396dd23c54ef added facts_of;
wenzelm
parents: 19777
diff changeset
   153
  | facts_of _ _ = [];
396dd23c54ef added facts_of;
wenzelm
parents: 19777
diff changeset
   154
18894
9c8c60853966 added concluding statements: Shows/Obtains;
wenzelm
parents: 18669
diff changeset
   155
9c8c60853966 added concluding statements: Shows/Obtains;
wenzelm
parents: 18669
diff changeset
   156
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   157
(** pretty printing **)
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   158
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   159
fun pretty_items _ _ [] = []
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   160
  | pretty_items keyword sep (x :: ys) =
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   161
      Pretty.block [Pretty.keyword keyword, Pretty.brk 1, x] ::
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   162
        map (fn y => Pretty.block [Pretty.str "  ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   163
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   164
fun pretty_name_atts ctxt (binding, atts) sep =
28733
18ffcbf1b3ae more verbose element printing
haftmann
parents: 28084
diff changeset
   165
  let
28737
8cbb7cfcfb5b diagnostic output for name bindings
haftmann
parents: 28733
diff changeset
   166
    val name = Name.output binding;
28733
18ffcbf1b3ae more verbose element printing
haftmann
parents: 28084
diff changeset
   167
  in if name = "" andalso null atts then []
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   168
    else [Pretty.block
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   169
      (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   170
  end;
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   171
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   172
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   173
(* pretty_stmt *)
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   174
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   175
fun pretty_stmt ctxt =
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   176
  let
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24637
diff changeset
   177
    val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24637
diff changeset
   178
    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   179
    val prt_terms = separate (Pretty.keyword "and") o map prt_term;
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   180
    val prt_name_atts = pretty_name_atts ctxt;
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   181
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   182
    fun prt_show (a, ts) =
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   183
      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   184
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   185
    fun prt_var (x, SOME T) = Pretty.block
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   186
          [Pretty.str (Name.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   187
      | prt_var (x, NONE) = Pretty.str (Name.name_of x);
26721
wenzelm
parents: 26716
diff changeset
   188
    val prt_vars = separate (Pretty.keyword "and") o map prt_var;
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   189
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   190
    fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   191
      | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks
19585
70a1ce3b23ae removed 'concl is' patterns;
wenzelm
parents: 19482
diff changeset
   192
          (prt_vars xs @ [Pretty.keyword "where"] @ prt_terms ts));
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   193
  in
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   194
    fn Shows shows => pretty_items "shows" "and" (map prt_show shows)
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   195
     | Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains)
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   196
  end;
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   197
18894
9c8c60853966 added concluding statements: Shows/Obtains;
wenzelm
parents: 18669
diff changeset
   198
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   199
(* pretty_ctxt *)
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   200
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   201
fun pretty_ctxt ctxt =
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   202
  let
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24637
diff changeset
   203
    val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24637
diff changeset
   204
    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   205
    val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   206
    val prt_name_atts = pretty_name_atts ctxt;
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   207
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   208
    fun prt_mixfix NoSyn = []
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   209
      | prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx];
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   210
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   211
    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Name.name_of x ^ " ::") ::
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   212
          Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   213
      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Name.name_of x) ::
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   214
          Pretty.brk 1 :: prt_mixfix mx);
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   215
    fun prt_constrain (x, T) = prt_fix (Name.binding x, SOME T, NoSyn);
18894
9c8c60853966 added concluding statements: Shows/Obtains;
wenzelm
parents: 18669
diff changeset
   216
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   217
    fun prt_asm (a, ts) =
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   218
      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts));
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   219
    fun prt_def (a, (t, _)) =
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   220
      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ [prt_term t]));
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   221
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   222
    fun prt_fact (ths, []) = map prt_thm ths
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   223
      | prt_fact (ths, atts) = Pretty.enclose "(" ")"
21032
a4b85340d6bd Attrib.pretty_attrib;
wenzelm
parents: 20886
diff changeset
   224
          (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   225
    fun prt_note (a, ths) =
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19466
diff changeset
   226
      Pretty.block (Pretty.breaks (flat (prt_name_atts a "=" :: map prt_fact ths)));
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   227
  in
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   228
    fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes)
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   229
     | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs)
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   230
     | Assumes asms => pretty_items "assumes" "and" (map prt_asm asms)
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   231
     | Defines defs => pretty_items "defines" "and" (map prt_def defs)
21440
807a39221a58 notes: proper kind;
wenzelm
parents: 21032
diff changeset
   232
     | Notes ("", facts) => pretty_items "notes" "and" (map prt_note facts)
807a39221a58 notes: proper kind;
wenzelm
parents: 21032
diff changeset
   233
     | Notes (kind, facts) => pretty_items ("notes " ^ kind) "and" (map prt_note facts)
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   234
  end;
18894
9c8c60853966 added concluding statements: Shows/Obtains;
wenzelm
parents: 18669
diff changeset
   235
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   236
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   237
(* pretty_statement *)
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   238
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   239
local
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   240
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   241
fun thm_name kind th prts =
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   242
  let val head =
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 26721
diff changeset
   243
    if Thm.has_name_hint th then
21965
7120ef5bc378 pretty_statement: more careful handling of name_hint;
wenzelm
parents: 21646
diff changeset
   244
      Pretty.block [Pretty.command kind,
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 26721
diff changeset
   245
        Pretty.brk 1, Pretty.str (Sign.base_name (Thm.get_name_hint th) ^ ":")]
21965
7120ef5bc378 pretty_statement: more careful handling of name_hint;
wenzelm
parents: 21646
diff changeset
   246
    else Pretty.command kind
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   247
  in Pretty.block (Pretty.fbreaks (head :: prts)) end;
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   248
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   249
fun fix (x, T) = (Name.binding x, SOME T);
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   250
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   251
fun obtain prop ctxt =
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   252
  let
20150
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   253
    val ((xs, prop'), ctxt') = Variable.focus prop ctxt;
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   254
    val As = Logic.strip_imp_prems (Thm.term_of prop');
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   255
  in ((Name.no_binding, (map (fix o Term.dest_Free o Thm.term_of) xs, As)), ctxt') end;
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   256
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   257
in
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   258
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   259
fun pretty_statement ctxt kind raw_th =
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   260
  let
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   261
    val thy = ProofContext.theory_of ctxt;
20150
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   262
    val cert = Thm.cterm_of thy;
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   263
21605
4e7307e229b3 qualified MetaSimplifier.norm_hhf(_protect);
wenzelm
parents: 21581
diff changeset
   264
    val th = MetaSimplifier.norm_hhf raw_th;
20150
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   265
    val is_elim = ObjectLogic.is_elim th;
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   266
26716
8690e75e1395 print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
wenzelm
parents: 26628
diff changeset
   267
    val ((_, [th']), ctxt') = Variable.import_thms true [th] (Variable.set_body false ctxt);
20150
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   268
    val prop = Thm.prop_of th';
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   269
    val (prems, concl) = Logic.strip_horn prop;
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   270
    val concl_term = ObjectLogic.drop_judgment thy concl;
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   271
20150
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   272
    val fixes = fold_aterms (fn v as Free (x, T) =>
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   273
        if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
26716
8690e75e1395 print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
wenzelm
parents: 26628
diff changeset
   274
        then insert (op =) (x, T) else I | _ => I) prop [] |> rev;
20150
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   275
    val (assumes, cases) = take_suffix (fn prem =>
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   276
      is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   277
  in
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   278
    pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Name.binding x, SOME T, NoSyn)) fixes)) @
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
   279
    pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.no_binding, [(t, [])])) assumes)) @
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
   280
     (if null cases then pretty_stmt ctxt' (Shows [(Attrib.no_binding, [(concl, [])])])
26716
8690e75e1395 print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
wenzelm
parents: 26628
diff changeset
   281
      else
8690e75e1395 print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
wenzelm
parents: 26628
diff changeset
   282
        let val (clauses, ctxt'') = fold_map (obtain o cert) cases ctxt'
8690e75e1395 print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
wenzelm
parents: 26628
diff changeset
   283
        in pretty_stmt ctxt'' (Obtains clauses) end)
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   284
  end |> thm_name kind raw_th;
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   285
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   286
end;
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   287
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   288
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   289
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   290
(** logical operations **)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   291
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   292
(* witnesses -- hypotheses as protected facts *)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   293
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   294
datatype witness = Witness of term * thm;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   295
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   296
fun map_witness f (Witness witn) = Witness (f witn);
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   297
21481
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
   298
fun morph_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
   299
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   300
fun witness_prop (Witness (t, _)) = t;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   301
fun witness_hyps (Witness (_, th)) = #hyps (Thm.rep_thm th);
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   302
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   303
fun assume_witness thy t =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   304
  Witness (t, Goal.protect (Thm.assume (Thm.cterm_of thy t)));
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   305
20058
7d035e26e5f9 prove_witness: context;
wenzelm
parents: 20007
diff changeset
   306
fun prove_witness ctxt t tac =
26628
63306cb94313 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
wenzelm
parents: 26336
diff changeset
   307
  Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (Logic.protect t) (fn _ =>
25202
3a539d9995fb proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;
wenzelm
parents: 24920
diff changeset
   308
    Tactic.rtac Drule.protectI 1 THEN tac)));
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   309
26628
63306cb94313 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
wenzelm
parents: 26336
diff changeset
   310
val close_witness = map_witness (fn (t, th) => (t, Thm.close_derivation th));
25624
04b67ee73327 added close_witness;
wenzelm
parents: 25302
diff changeset
   311
25202
3a539d9995fb proven witness: proper Goal.close_result save huge amounts of resources when using proof terms;
wenzelm
parents: 24920
diff changeset
   312
fun conclude_witness (Witness (_, th)) =
26628
63306cb94313 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
wenzelm
parents: 26336
diff changeset
   313
  Thm.close_derivation (MetaSimplifier.norm_hhf_protect (Goal.conclude th));
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   314
25302
19b1729f1bd4 tuned satisfy_thm;
wenzelm
parents: 25285
diff changeset
   315
fun compose_witness (Witness (_, th)) r =
19b1729f1bd4 tuned satisfy_thm;
wenzelm
parents: 25285
diff changeset
   316
  let
19b1729f1bd4 tuned satisfy_thm;
wenzelm
parents: 25285
diff changeset
   317
    val th' = Goal.conclude th;
19b1729f1bd4 tuned satisfy_thm;
wenzelm
parents: 25285
diff changeset
   318
    val A = Thm.cprem_of r 1;
25739
9da2343deb92 Fixed eta constraction issue in compose_witness
ballarin
parents: 25624
diff changeset
   319
  in
9da2343deb92 Fixed eta constraction issue in compose_witness
ballarin
parents: 25624
diff changeset
   320
    Thm.implies_elim
9da2343deb92 Fixed eta constraction issue in compose_witness
ballarin
parents: 25624
diff changeset
   321
      (Conv.gconv_rule Drule.beta_eta_conversion 1 r)
9da2343deb92 Fixed eta constraction issue in compose_witness
ballarin
parents: 25624
diff changeset
   322
      (Conv.fconv_rule Drule.beta_eta_conversion
9da2343deb92 Fixed eta constraction issue in compose_witness
ballarin
parents: 25624
diff changeset
   323
        (Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th'))
9da2343deb92 Fixed eta constraction issue in compose_witness
ballarin
parents: 25624
diff changeset
   324
  end;
25302
19b1729f1bd4 tuned satisfy_thm;
wenzelm
parents: 25285
diff changeset
   325
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   326
val mark_witness = Logic.protect;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   327
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   328
fun make_witness t th = Witness (t, th);
19931
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19897
diff changeset
   329
fun dest_witness (Witness w) = w;
fb32b43e7f80 Restructured locales with predicates: import is now an interpretation.
ballarin
parents: 19897
diff changeset
   330
20068
19c7361db4a3 New function transfer_witness lifting Thm.transfer to witnesses.
ballarin
parents: 20058
diff changeset
   331
fun transfer_witness thy (Witness (t, th)) = Witness (t, Thm.transfer thy th);
19c7361db4a3 New function transfer_witness lifting Thm.transfer to witnesses.
ballarin
parents: 20058
diff changeset
   332
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   333
val refine_witness =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   334
  Proof.refine (Method.Basic (K (Method.RAW_METHOD
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   335
    (K (ALLGOALS
23414
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23351
diff changeset
   336
      (CONJUNCTS (ALLGOALS
927203ad4b3a tuned conjunction tactics: slightly smaller proof terms;
wenzelm
parents: 23351
diff changeset
   337
        (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   338
22658
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22568
diff changeset
   339
fun pretty_witness ctxt witn =
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24637
diff changeset
   340
  let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
22658
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22568
diff changeset
   341
    Pretty.block (prt_term (witness_prop witn) ::
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22568
diff changeset
   342
      (if ! show_hyps then [Pretty.brk 2, Pretty.list "[" "]"
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22568
diff changeset
   343
         (map prt_term (witness_hyps witn))] else []))
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22568
diff changeset
   344
  end;
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22568
diff changeset
   345
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   346
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   347
(* derived rules *)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   348
20007
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   349
fun instantiate_tfrees thy subst th =
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   350
  let
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   351
    val certT = Thm.ctyp_of thy;
20007
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   352
    val idx = Thm.maxidx_of th + 1;
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   353
    fun cert_inst (a, (S, T)) = (certT (TVar ((a, idx), S)), certT T);
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   354
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   355
    fun add_inst (a, S) insts =
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   356
      if AList.defined (op =) insts a then insts
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   357
      else (case AList.lookup (op =) subst a of NONE => insts | SOME T => (a, (S, T)) :: insts);
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   358
    val insts =
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   359
      Term.fold_types (Term.fold_atyps (fn TFree v => add_inst v | _ => I))
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   360
        (Thm.full_prop_of th) [];
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   361
  in
20007
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   362
    th
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   363
    |> Thm.generalize (map fst insts, []) idx
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   364
    |> Thm.instantiate (map cert_inst insts, [])
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   365
  end;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   366
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   367
fun instantiate_frees thy subst =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   368
  let val cert = Thm.cterm_of thy in
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   369
    Drule.forall_intr_list (map (cert o Free o fst) subst) #>
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   370
    Drule.forall_elim_list (map (cert o snd) subst)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   371
  end;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   372
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   373
fun hyps_rule rule th =
21521
095f4963beed simultaneous fact morphism;
wenzelm
parents: 21497
diff changeset
   374
  let val {hyps, ...} = Thm.crep_thm th in
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   375
    Drule.implies_elim_list
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   376
      (rule (Drule.implies_intr_list hyps th))
21521
095f4963beed simultaneous fact morphism;
wenzelm
parents: 21497
diff changeset
   377
      (map (Thm.assume o Drule.cterm_rule rule) hyps)
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   378
  end;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   379
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   380
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   381
(* rename *)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   382
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   383
fun rename ren x =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   384
  (case AList.lookup (op =) ren (x: string) of
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   385
    NONE => x
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   386
  | SOME (x', _) => x');
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   387
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   388
fun rename_var_name ren (x, mx) =
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   389
  (case (AList.lookup (op =) ren x, mx) of
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   390
    (NONE, _) => (x, mx)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   391
  | (SOME (x', NONE), Structure) => (x', mx)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   392
  | (SOME (x', SOME _), Structure) =>
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   393
      error ("Attempt to change syntax of structure parameter " ^ quote x)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   394
  | (SOME (x', NONE), _) => (x', NoSyn)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   395
  | (SOME (x', SOME mx'), _) => (x', mx'));
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   396
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   397
fun rename_var ren (binding, mx) =
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   398
  let
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   399
    val x = Name.name_of binding;
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   400
    val (x', mx') = rename_var_name ren (x, mx);
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   401
  in (Name.binding x', mx') end;
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   402
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   403
fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   404
  | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   405
  | rename_term ren (Abs (x, T, t)) = Abs (x, T, rename_term ren t)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   406
  | rename_term _ a = a;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   407
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   408
fun rename_thm ren th =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   409
  let
20304
500a3373c93c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20264
diff changeset
   410
    val thy = Thm.theory_of_thm th;
22691
290454649b8c Thm.fold_terms;
wenzelm
parents: 22672
diff changeset
   411
    val subst = (Thm.fold_terms o Term.fold_aterms)
20304
500a3373c93c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20264
diff changeset
   412
      (fn Free (x, T) =>
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   413
        let val x' = rename ren x
20304
500a3373c93c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20264
diff changeset
   414
        in if x = x' then I else insert (eq_fst (op =)) ((x, T), Free (x', T)) end
500a3373c93c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20264
diff changeset
   415
      | _ => I) th [];
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   416
  in
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   417
    if null subst then th
20304
500a3373c93c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20264
diff changeset
   418
    else th |> hyps_rule (instantiate_frees thy subst)
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   419
  end;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   420
21481
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
   421
fun rename_morphism ren = Morphism.morphism
21521
095f4963beed simultaneous fact morphism;
wenzelm
parents: 21497
diff changeset
   422
  {name = I, var = rename_var ren, typ = I, term = rename_term ren, fact = map (rename_thm ren)};
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   423
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   424
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   425
(* instantiate types *)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   426
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   427
fun instT_type env =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   428
  if Symtab.is_empty env then I
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   429
  else Term.map_type_tfree (fn (x, S) => the_default (TFree (x, S)) (Symtab.lookup env x));
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   430
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   431
fun instT_term env =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   432
  if Symtab.is_empty env then I
20548
8ef25fe585a8 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents: 20304
diff changeset
   433
  else Term.map_types (instT_type env);
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   434
22691
290454649b8c Thm.fold_terms;
wenzelm
parents: 22672
diff changeset
   435
fun instT_subst env th = (Thm.fold_terms o Term.fold_types o Term.fold_atyps)
20304
500a3373c93c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20264
diff changeset
   436
  (fn T as TFree (a, _) =>
500a3373c93c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20264
diff changeset
   437
    let val T' = the_default T (Symtab.lookup env a)
500a3373c93c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20264
diff changeset
   438
    in if T = T' then I else insert (op =) (a, T') end
500a3373c93c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20264
diff changeset
   439
  | _ => I) th [];
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   440
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   441
fun instT_thm thy env th =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   442
  if Symtab.is_empty env then th
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   443
  else
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   444
    let val subst = instT_subst env th
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   445
    in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   446
22672
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   447
fun instT_morphism thy env =
24137
8d7896398147 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents: 23414
diff changeset
   448
  let val thy_ref = Theory.check_thy thy in
22672
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   449
    Morphism.morphism
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   450
     {name = I, var = I,
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   451
      typ = instT_type env,
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   452
      term = instT_term env,
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   453
      fact = map (fn th => instT_thm (Theory.deref thy_ref) env th)}
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   454
  end;
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   455
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   456
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   457
(* instantiate types and terms *)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   458
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   459
fun inst_term (envT, env) =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   460
  if Symtab.is_empty env then instT_term envT
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   461
  else
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   462
    let
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   463
      val instT = instT_type envT;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   464
      fun inst (Const (x, T)) = Const (x, instT T)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   465
        | inst (Free (x, T)) =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   466
            (case Symtab.lookup env x of
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   467
              NONE => Free (x, instT T)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   468
            | SOME t => t)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   469
        | inst (Var (xi, T)) = Var (xi, instT T)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   470
        | inst (b as Bound _) = b
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   471
        | inst (Abs (x, T, t)) = Abs (x, instT T, inst t)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   472
        | inst (t $ u) = inst t $ inst u;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   473
    in Envir.beta_norm o inst end;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   474
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   475
fun inst_thm thy (envT, env) th =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   476
  if Symtab.is_empty env then instT_thm thy envT th
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   477
  else
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   478
    let
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   479
      val substT = instT_subst envT th;
22691
290454649b8c Thm.fold_terms;
wenzelm
parents: 22672
diff changeset
   480
      val subst = (Thm.fold_terms o Term.fold_aterms)
20304
500a3373c93c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20264
diff changeset
   481
       (fn Free (x, T) =>
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   482
          let
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   483
            val T' = instT_type envT T;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   484
            val t = Free (x, T');
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   485
            val t' = the_default t (Symtab.lookup env x);
20304
500a3373c93c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20264
diff changeset
   486
          in if t aconv t' then I else insert (eq_fst (op =)) ((x, T'), t') end
500a3373c93c removed obsolete Drule.frees/vars_of etc.;
wenzelm
parents: 20264
diff changeset
   487
       | _ => I) th [];
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   488
    in
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   489
      if null substT andalso null subst then th
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   490
      else th |> hyps_rule
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   491
       (instantiate_tfrees thy substT #>
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   492
        instantiate_frees thy subst #>
22900
f8a7c10e1bd0 moved conversions to structure Conv;
wenzelm
parents: 22691
diff changeset
   493
        Conv.fconv_rule (Thm.beta_conversion true))
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   494
    end;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   495
22672
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   496
fun inst_morphism thy envs =
24137
8d7896398147 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
wenzelm
parents: 23414
diff changeset
   497
  let val thy_ref = Theory.check_thy thy in
22672
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   498
    Morphism.morphism
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   499
     {name = I, var = I,
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   500
      typ = instT_type (#1 envs),
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   501
      term = inst_term envs,
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   502
      fact = map (fn th => inst_thm (Theory.deref thy_ref) envs th)}
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   503
  end;
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   504
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   505
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   506
(* satisfy hypotheses *)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   507
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   508
fun satisfy_thm witns thm = thm |> fold (fn hyp =>
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   509
    (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   510
      NONE => I
25302
19b1729f1bd4 tuned satisfy_thm;
wenzelm
parents: 25285
diff changeset
   511
    | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   512
21497
4d330a487586 Morphism.thm_morphism;
wenzelm
parents: 21481
diff changeset
   513
fun satisfy_morphism witns = Morphism.thm_morphism (satisfy_thm witns);
19843
67cb97e856ff added satisfy_ctxt;
wenzelm
parents: 19808
diff changeset
   514
21581
7799b1739a51 added facts_map;
wenzelm
parents: 21528
diff changeset
   515
fun satisfy_facts witns = facts_map (morph_ctxt (satisfy_morphism witns));
20264
f09a4003e12d added generalize_facts;
wenzelm
parents: 20233
diff changeset
   516
f09a4003e12d added generalize_facts;
wenzelm
parents: 20233
diff changeset
   517
f09a4003e12d added generalize_facts;
wenzelm
parents: 20233
diff changeset
   518
(* generalize type/term parameters *)
f09a4003e12d added generalize_facts;
wenzelm
parents: 20233
diff changeset
   519
f09a4003e12d added generalize_facts;
wenzelm
parents: 20233
diff changeset
   520
val maxidx_atts = fold Args.maxidx_values;
f09a4003e12d added generalize_facts;
wenzelm
parents: 20233
diff changeset
   521
21581
7799b1739a51 added facts_map;
wenzelm
parents: 21528
diff changeset
   522
fun generalize_facts inner outer facts =
20264
f09a4003e12d added generalize_facts;
wenzelm
parents: 20233
diff changeset
   523
  let
f09a4003e12d added generalize_facts;
wenzelm
parents: 20233
diff changeset
   524
    val thy = ProofContext.theory_of inner;
f09a4003e12d added generalize_facts;
wenzelm
parents: 20233
diff changeset
   525
    val maxidx =
f09a4003e12d added generalize_facts;
wenzelm
parents: 20233
diff changeset
   526
      fold (fn ((_, atts), bs) => maxidx_atts atts #> fold (maxidx_atts o #2) bs) facts ~1;
21581
7799b1739a51 added facts_map;
wenzelm
parents: 21528
diff changeset
   527
    val exp_fact = map (Thm.adjust_maxidx_thm maxidx) #> Variable.export inner outer;
21521
095f4963beed simultaneous fact morphism;
wenzelm
parents: 21497
diff changeset
   528
    val exp_term = Drule.term_rule thy (singleton exp_fact);
095f4963beed simultaneous fact morphism;
wenzelm
parents: 21497
diff changeset
   529
    val exp_typ = Logic.type_map exp_term;
095f4963beed simultaneous fact morphism;
wenzelm
parents: 21497
diff changeset
   530
    val morphism =
095f4963beed simultaneous fact morphism;
wenzelm
parents: 21497
diff changeset
   531
      Morphism.morphism {name = I, var = I, typ = exp_typ, term = exp_term, fact = exp_fact};
21581
7799b1739a51 added facts_map;
wenzelm
parents: 21528
diff changeset
   532
  in facts_map (morph_ctxt morphism) facts end;
20886
f26672c248ee replaced generalize_facts by full export_(standard_)facts;
wenzelm
parents: 20548
diff changeset
   533
28832
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   534
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   535
(** activate in context, return elements and facts **)
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   536
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   537
local
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   538
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   539
fun axioms_export axs _ As =
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   540
  (satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   541
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   542
fun activate_elem (Fixes fixes) ctxt =
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   543
      ([], ctxt |> ProofContext.add_fixes_i fixes |> snd)
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   544
  | activate_elem (Constrains _) ctxt =
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   545
      ([], ctxt)
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   546
  | activate_elem (Assumes asms) ctxt =
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   547
      let
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   548
        val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   549
        val ts = maps (map #1 o #2) asms';
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   550
        val (_, ctxt') =
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   551
          ctxt |> fold Variable.auto_fixes ts
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   552
          |> ProofContext.add_assms_i (axioms_export []) asms';
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   553
      in ([], ctxt') end
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   554
  | activate_elem (Defines defs) ctxt =
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   555
      let
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   556
        val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   557
        val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   558
            let val ((c, _), t') = LocalDefs.cert_def ctxt t
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   559
            in (t', ((Name.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   560
        val (_, ctxt') =
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   561
          ctxt |> fold (Variable.auto_fixes o #1) asms
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   562
          |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   563
      in ([], ctxt') end
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   564
  | activate_elem (Notes (kind, facts)) ctxt =
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   565
      let
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   566
        val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   567
        val (res, ctxt') = ctxt |> ProofContext.note_thmss_i kind facts';
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   568
      in ((map (#1 o #1) facts' ~~ map #2 res), ctxt') end;
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   569
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   570
fun gen_activate prep_facts raw_elems ctxt =
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   571
  let
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   572
    val elems = map (map_ctxt_attrib Args.assignable o prep_facts ctxt) raw_elems;
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   573
    val (res, ctxt') = fold_map activate_elem elems (ProofContext.qualified_names ctxt);
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   574
    val elems' = elems |> map (map_ctxt_attrib Args.closure);
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   575
  in ((elems', flat res), ProofContext.restore_naming ctxt ctxt') end;
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   576
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   577
fun check_name name =
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   578
  if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   579
  else name;
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   580
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   581
fun prep_facts prep_name get intern ctxt elem = elem |> map_ctxt
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   582
     {var = I, typ = I, term = I,
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   583
      name = Name.map_name prep_name,
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   584
      fact = get ctxt,
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   585
      attrib = intern (ProofContext.theory_of ctxt)};
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   586
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   587
in
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   588
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   589
fun activate x = gen_activate (prep_facts check_name ProofContext.get_fact Attrib.intern_src) x;
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   590
fun activate_i x = gen_activate (K I) x;
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   591
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   592
end;
28832
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   593
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   594
end;