src/Pure/Isar/element.ML
author wenzelm
Tue, 30 Jul 2013 15:09:25 +0200
changeset 52788 da1fdbfebd39
parent 52732 b4da1f2ec73f
child 52789 44fd3add1348
permissions -rw-r--r--
type theory is purely value-oriented;
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
    Author:     Makarius
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
     3
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
     4
Explicit data structures for some Isar language elements, with derived
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
     5
logical operations.
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
     6
*)
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
signature ELEMENT =
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
     9
sig
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    10
  datatype ('typ, 'term) stmt =
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    11
    Shows of (Attrib.binding * ('term * 'term list) list) list |
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
    12
    Obtains of (binding * ((binding * 'typ option) list * 'term list)) list
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25739
diff changeset
    13
  type statement = (string, string) stmt
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25739
diff changeset
    14
  type statement_i = (typ, term) stmt
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    15
  datatype ('typ, 'term, 'fact) ctxt =
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
    16
    Fixes of (binding * 'typ option * mixfix) list |
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    17
    Constrains of (string * 'typ) list |
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    18
    Assumes of (Attrib.binding * ('term * 'term list) list) list |
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    19
    Defines of (Attrib.binding * ('term * 'term list)) list |
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    20
    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
    21
  type context = (string, string, Facts.ref) ctxt
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25739
diff changeset
    22
  type context_i = (typ, term, thm list) ctxt
29603
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
    23
  val map_ctxt: {binding: binding -> binding, typ: 'typ -> 'a, term: 'term -> 'b,
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
    24
    pattern: 'term -> 'b, fact: 'fact -> 'c, attrib: Attrib.src -> Attrib.src} ->
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
    25
    ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
21528
84e98b5f5af0 added map_ctxt_attrib;
wenzelm
parents: 21521
diff changeset
    26
  val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
84e98b5f5af0 added map_ctxt_attrib;
wenzelm
parents: 21521
diff changeset
    27
    ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
45290
f599ac41e7f5 tuned signature -- refined terminology;
wenzelm
parents: 45289
diff changeset
    28
  val transform_ctxt: morphism -> context_i -> context_i
45601
d5178f19b671 tuned signature;
wenzelm
parents: 45584
diff changeset
    29
  val transform_facts: morphism ->
d5178f19b671 tuned signature;
wenzelm
parents: 45584
diff changeset
    30
    (Attrib.binding * (thm list * Args.src list) list) list ->
d5178f19b671 tuned signature;
wenzelm
parents: 45584
diff changeset
    31
    (Attrib.binding * (thm list * Args.src list) list) list
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    32
  val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    33
  val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    34
  val pretty_statement: Proof.context -> string -> thm -> Pretty.T
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    35
  type witness
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
    36
  val prove_witness: Proof.context -> term -> tactic -> witness
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
    37
  val witness_proof: (witness list list -> Proof.context -> Proof.context) ->
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
    38
    term list list -> Proof.context -> Proof.state
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
    39
  val witness_proof_eqs: (witness list list -> thm list -> Proof.context -> Proof.context) ->
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
    40
    term list list -> term list -> Proof.context -> Proof.state
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
    41
  val witness_local_proof: (witness list list -> Proof.state -> Proof.state) ->
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
    42
    string -> term list list -> Proof.context -> bool -> Proof.state -> Proof.state
38108
b4115423c049 Interpretation in proofs supports mixins.
ballarin
parents: 36674
diff changeset
    43
  val witness_local_proof_eqs: (witness list list -> thm list -> Proof.state -> Proof.state) ->
b4115423c049 Interpretation in proofs supports mixins.
ballarin
parents: 36674
diff changeset
    44
    string -> term list list -> term list -> Proof.context -> bool -> Proof.state ->
b4115423c049 Interpretation in proofs supports mixins.
ballarin
parents: 36674
diff changeset
    45
    Proof.state
45290
f599ac41e7f5 tuned signature -- refined terminology;
wenzelm
parents: 45289
diff changeset
    46
  val transform_witness: morphism -> witness -> witness
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    47
  val conclude_witness: witness -> thm
22658
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22568
diff changeset
    48
  val pretty_witness: Proof.context -> witness -> Pretty.T
21481
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
    49
  val instT_morphism: theory -> typ Symtab.table -> morphism
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
    50
  val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
    51
  val satisfy_morphism: witness list -> morphism
36674
d95f39448121 eq_morphism is always optional: avoid trivial morphism for empty list of equations
haftmann
parents: 36323
diff changeset
    52
  val eq_morphism: theory -> thm list -> morphism option
30775
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
    53
  val init: context_i -> Context.generic -> Context.generic
30777
9960ff945c52 simplified Element.activate(_i): singleton version;
wenzelm
parents: 30775
diff changeset
    54
  val activate_i: context_i -> Proof.context -> context_i * Proof.context
9960ff945c52 simplified Element.activate(_i): singleton version;
wenzelm
parents: 30775
diff changeset
    55
  val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    56
end;
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    57
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    58
structure Element: ELEMENT =
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    59
struct
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    60
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    61
(** language elements **)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    62
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    63
(* statement *)
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    64
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    65
datatype ('typ, 'term) stmt =
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    66
  Shows of (Attrib.binding * ('term * 'term list) list) list |
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
    67
  Obtains of (binding * ((binding * 'typ option) list * 'term list)) list;
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    68
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    69
type statement = (string, string) stmt;
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    70
type statement_i = (typ, term) stmt;
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    71
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
    72
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
    73
(* context *)
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    74
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    75
datatype ('typ, 'term, 'fact) ctxt =
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
    76
  Fixes of (binding * 'typ option * mixfix) list |
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    77
  Constrains of (string * 'typ) list |
28084
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    78
  Assumes of (Attrib.binding * ('term * 'term list) list) list |
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    79
  Defines of (Attrib.binding * ('term * 'term list)) list |
a05ca48ef263 type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents: 28079
diff changeset
    80
  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
    81
26336
a0e2b706ce73 renamed datatype thmref to Facts.ref, tuned interfaces;
wenzelm
parents: 25739
diff changeset
    82
type context = (string, string, Facts.ref) ctxt;
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    83
type context_i = (typ, term, thm list) ctxt;
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    84
29603
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
    85
fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
    86
  fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
    87
   | Constrains xs => Constrains (xs |> map (fn (x, T) =>
42494
eef1a23c9077 tuned signature -- eliminated odd comment;
wenzelm
parents: 42488
diff changeset
    88
      (Variable.check_name (binding (Binding.name x)), typ T)))
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    89
   | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
29603
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
    90
      ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps)))))
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    91
   | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
29603
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
    92
      ((binding a, map attrib atts), (term t, map pattern ps))))
21440
807a39221a58 notes: proper kind;
wenzelm
parents: 21032
diff changeset
    93
   | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28888
diff changeset
    94
      ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
    95
21528
84e98b5f5af0 added map_ctxt_attrib;
wenzelm
parents: 21521
diff changeset
    96
fun map_ctxt_attrib attrib =
29603
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
    97
  map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib};
21528
84e98b5f5af0 added map_ctxt_attrib;
wenzelm
parents: 21521
diff changeset
    98
45290
f599ac41e7f5 tuned signature -- refined terminology;
wenzelm
parents: 45289
diff changeset
    99
fun transform_ctxt phi = map_ctxt
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28888
diff changeset
   100
 {binding = Morphism.binding phi,
21481
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
   101
  typ = Morphism.typ phi,
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
   102
  term = Morphism.term phi,
29603
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
   103
  pattern = Morphism.term phi,
21521
095f4963beed simultaneous fact morphism;
wenzelm
parents: 21497
diff changeset
   104
  fact = Morphism.fact phi,
45290
f599ac41e7f5 tuned signature -- refined terminology;
wenzelm
parents: 45289
diff changeset
   105
  attrib = Args.transform_values phi};
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   106
45601
d5178f19b671 tuned signature;
wenzelm
parents: 45584
diff changeset
   107
fun transform_facts phi facts =
d5178f19b671 tuned signature;
wenzelm
parents: 45584
diff changeset
   108
  Notes ("", facts) |> transform_ctxt phi |> (fn Notes (_, facts') => facts');
d5178f19b671 tuned signature;
wenzelm
parents: 45584
diff changeset
   109
19808
396dd23c54ef added facts_of;
wenzelm
parents: 19777
diff changeset
   110
18894
9c8c60853966 added concluding statements: Shows/Obtains;
wenzelm
parents: 18669
diff changeset
   111
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   112
(** pretty printing **)
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   113
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   114
fun pretty_items _ _ [] = []
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   115
  | pretty_items keyword sep (x :: ys) =
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   116
      Pretty.block [Pretty.keyword keyword, Pretty.brk 1, x] ::
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   117
        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
   118
28862
53f13f763d4f tuned name bindings
haftmann
parents: 28850
diff changeset
   119
fun pretty_name_atts ctxt (b, atts) sep =
45584
41a768a431a6 do not store vacuous theorem specifications -- relevant for frugal local theory content;
wenzelm
parents: 45390
diff changeset
   120
  if Attrib.is_empty_binding (b, atts) then []
43547
f3a8476285c6 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm
parents: 42495
diff changeset
   121
  else
f3a8476285c6 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm
parents: 42495
diff changeset
   122
    [Pretty.block (Pretty.breaks
f3a8476285c6 clarified Binding.pretty/print: no quotes, only markup -- Binding.str_of is rendered obsolete;
wenzelm
parents: 42495
diff changeset
   123
      (Binding.pretty b :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))];
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   124
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   125
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   126
(* pretty_stmt *)
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   127
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   128
fun pretty_stmt ctxt =
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   129
  let
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24637
diff changeset
   130
    val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24637
diff changeset
   131
    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   132
    val prt_terms = separate (Pretty.keyword "and") o map prt_term;
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   133
    val prt_name_atts = pretty_name_atts ctxt;
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   134
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   135
    fun prt_show (a, ts) =
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   136
      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   137
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   138
    fun prt_var (x, SOME T) = Pretty.block
30223
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30219
diff changeset
   139
          [Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30219
diff changeset
   140
      | prt_var (x, NONE) = Pretty.str (Binding.name_of x);
26721
wenzelm
parents: 26716
diff changeset
   141
    val prt_vars = separate (Pretty.keyword "and") o map prt_var;
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   142
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   143
    fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   144
      | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks
19585
70a1ce3b23ae removed 'concl is' patterns;
wenzelm
parents: 19482
diff changeset
   145
          (prt_vars xs @ [Pretty.keyword "where"] @ prt_terms ts));
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   146
  in
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   147
    fn Shows shows => pretty_items "shows" "and" (map prt_show shows)
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   148
     | Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains)
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   149
  end;
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   150
18894
9c8c60853966 added concluding statements: Shows/Obtains;
wenzelm
parents: 18669
diff changeset
   151
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   152
(* pretty_ctxt *)
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   153
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   154
fun pretty_ctxt ctxt =
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   155
  let
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24637
diff changeset
   156
    val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24637
diff changeset
   157
    val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
32091
30e2ffbba718 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents: 31794
diff changeset
   158
    val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   159
    val prt_name_atts = pretty_name_atts ctxt;
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   160
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   161
    fun prt_mixfix NoSyn = []
42287
d98eb048a2e4 discontinued special treatment of structure Mixfix;
wenzelm
parents: 41581
diff changeset
   162
      | prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx];
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   163
30223
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30219
diff changeset
   164
    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.name_of x ^ " ::") ::
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   165
          Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
30223
24d975352879 renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
wenzelm
parents: 30219
diff changeset
   166
      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.name_of x) ::
28079
955c42c8a5e4 explicit type Name.binding for higher-specification elements;
wenzelm
parents: 27865
diff changeset
   167
          Pretty.brk 1 :: prt_mixfix mx);
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28888
diff changeset
   168
    fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
18894
9c8c60853966 added concluding statements: Shows/Obtains;
wenzelm
parents: 18669
diff changeset
   169
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   170
    fun prt_asm (a, ts) =
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   171
      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts));
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   172
    fun prt_def (a, (t, _)) =
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   173
      Pretty.block (Pretty.breaks (prt_name_atts a ":" @ [prt_term t]));
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   174
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   175
    fun prt_fact (ths, []) = map prt_thm ths
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   176
      | prt_fact (ths, atts) = Pretty.enclose "(" ")"
21032
a4b85340d6bd Attrib.pretty_attrib;
wenzelm
parents: 20886
diff changeset
   177
          (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   178
    fun prt_note (a, ths) =
19482
9f11af8f7ef9 tuned basic list operators (flat, maps, map_filter);
wenzelm
parents: 19466
diff changeset
   179
      Pretty.block (Pretty.breaks (flat (prt_name_atts a "=" :: map prt_fact ths)));
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   180
  in
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   181
    fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes)
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   182
     | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs)
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   183
     | Assumes asms => pretty_items "assumes" "and" (map prt_asm asms)
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   184
     | Defines defs => pretty_items "defines" "and" (map prt_def defs)
21440
807a39221a58 notes: proper kind;
wenzelm
parents: 21032
diff changeset
   185
     | Notes ("", facts) => pretty_items "notes" "and" (map prt_note facts)
807a39221a58 notes: proper kind;
wenzelm
parents: 21032
diff changeset
   186
     | Notes (kind, facts) => pretty_items ("notes " ^ kind) "and" (map prt_note facts)
19259
196d3b7c8ad1 added pretty_stmt;
wenzelm
parents: 18906
diff changeset
   187
  end;
18894
9c8c60853966 added concluding statements: Shows/Obtains;
wenzelm
parents: 18669
diff changeset
   188
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   189
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   190
(* pretty_statement *)
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   191
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   192
local
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   193
41581
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41425
diff changeset
   194
fun standard_elim th =
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41425
diff changeset
   195
  (case Object_Logic.elim_concl th of
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41425
diff changeset
   196
    SOME C =>
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41425
diff changeset
   197
      let
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41425
diff changeset
   198
        val cert = Thm.cterm_of (Thm.theory_of_thm th);
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41425
diff changeset
   199
        val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41425
diff changeset
   200
        val th' = Thm.instantiate ([], [(cert C, cert thesis)]) th;
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41425
diff changeset
   201
      in (th', true) end
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41425
diff changeset
   202
  | NONE => (th, false));
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41425
diff changeset
   203
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   204
fun thm_name kind th prts =
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   205
  let val head =
27865
27a8ad9612a3 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
wenzelm
parents: 26721
diff changeset
   206
    if Thm.has_name_hint th then
21965
7120ef5bc378 pretty_statement: more careful handling of name_hint;
wenzelm
parents: 21646
diff changeset
   207
      Pretty.block [Pretty.command kind,
30364
577edc39b501 moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents: 30280
diff changeset
   208
        Pretty.brk 1, Pretty.str (Long_Name.base_name (Thm.get_name_hint th) ^ ":")]
21965
7120ef5bc378 pretty_statement: more careful handling of name_hint;
wenzelm
parents: 21646
diff changeset
   209
    else Pretty.command kind
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   210
  in Pretty.block (Pretty.fbreaks (head :: prts)) end;
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   211
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   212
fun obtain prop ctxt =
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   213
  let
41581
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41425
diff changeset
   214
    val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
42488
4638622bcaa1 reorganized fixes as specialized (global) name space;
wenzelm
parents: 42360
diff changeset
   215
    fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T);
42495
1af81b70cf09 clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
wenzelm
parents: 42494
diff changeset
   216
    val xs = map (fix o #2) ps;
1af81b70cf09 clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
wenzelm
parents: 42494
diff changeset
   217
    val As = Logic.strip_imp_prems prop';
41581
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41425
diff changeset
   218
  in ((Binding.empty, (xs, As)), ctxt') end;
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   219
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   220
in
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   221
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   222
fun pretty_statement ctxt kind raw_th =
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   223
  let
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42357
diff changeset
   224
    val thy = Proof_Context.theory_of ctxt;
20150
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   225
41581
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41425
diff changeset
   226
    val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th);
72a02e3dec7e clarified pretty_statement: more robust treatment of fixes and conclusion of elimination (e.g. for classical rule);
wenzelm
parents: 41425
diff changeset
   227
    val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt);
20150
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   228
    val prop = Thm.prop_of th';
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   229
    val (prems, concl) = Logic.strip_horn prop;
35625
9c818cab0dd0 modernized structure Object_Logic;
wenzelm
parents: 35624
diff changeset
   230
    val concl_term = Object_Logic.drop_judgment thy concl;
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   231
20150
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   232
    val fixes = fold_aterms (fn v as Free (x, T) =>
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   233
        if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
42488
4638622bcaa1 reorganized fixes as specialized (global) name space;
wenzelm
parents: 42360
diff changeset
   234
        then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop [] |> rev;
20150
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   235
    val (assumes, cases) = take_suffix (fn prem =>
baa589c574ff print_statement: tuned Variable operations;
wenzelm
parents: 20068
diff changeset
   236
      is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   237
  in
28965
1de908189869 cleaned up binding module and related code
haftmann
parents: 28888
diff changeset
   238
    pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) fixes)) @
1de908189869 cleaned up binding module and related code
haftmann
parents: 28888
diff changeset
   239
    pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.empty_binding, [(t, [])])) assumes)) @
1de908189869 cleaned up binding module and related code
haftmann
parents: 28888
diff changeset
   240
     (if null cases then pretty_stmt ctxt' (Shows [(Attrib.empty_binding, [(concl, [])])])
26716
8690e75e1395 print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
wenzelm
parents: 26628
diff changeset
   241
      else
42495
1af81b70cf09 clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
wenzelm
parents: 42494
diff changeset
   242
        let val (clauses, ctxt'') = fold_map obtain cases ctxt'
26716
8690e75e1395 print_statement: reset body mode, i.e. invent global frees (no need for revert_skolem);
wenzelm
parents: 26628
diff changeset
   243
        in pretty_stmt ctxt'' (Obtains clauses) end)
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   244
  end |> thm_name kind raw_th;
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   245
18140
691c64d615a5 Explicit data structures for some Isar language elements.
wenzelm
parents:
diff changeset
   246
end;
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   247
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   248
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   249
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   250
(** logical operations **)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   251
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   252
(* witnesses -- hypotheses as protected facts *)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   253
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   254
datatype witness = Witness of term * thm;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   255
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   256
val mark_witness = Logic.protect;
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   257
fun witness_prop (Witness (t, _)) = t;
44058
ae85c5d64913 misc tuning -- eliminated old-fashioned rep_thm;
wenzelm
parents: 43842
diff changeset
   258
fun witness_hyps (Witness (_, th)) = Thm.hyps_of th;
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   259
fun map_witness f (Witness witn) = Witness (f witn);
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   260
45290
f599ac41e7f5 tuned signature -- refined terminology;
wenzelm
parents: 45289
diff changeset
   261
fun transform_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
21481
025ab31286d8 added morph_ctxt, morph_witness;
wenzelm
parents: 21440
diff changeset
   262
20058
7d035e26e5f9 prove_witness: context;
wenzelm
parents: 20007
diff changeset
   263
fun prove_witness ctxt t tac =
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52230
diff changeset
   264
  Witness (t,
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52230
diff changeset
   265
    Thm.close_derivation
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52230
diff changeset
   266
      (Goal.prove ctxt [] [] (mark_witness t) (fn _ => rtac Drule.protectI 1 THEN tac)));
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   267
29603
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
   268
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   269
local
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   270
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   271
val refine_witness =
30510
4120fc59dd85 unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents: 30438
diff changeset
   272
  Proof.refine (Method.Basic (K (RAW_METHOD
52732
b4da1f2ec73f standardized aliases;
wenzelm
parents: 52230
diff changeset
   273
    (K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (rtac Drule.protectI))))))))));
25624
04b67ee73327 added close_witness;
wenzelm
parents: 25302
diff changeset
   274
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   275
fun gen_witness_proof proof after_qed wit_propss eq_props =
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   276
  let
46896
wenzelm
parents: 46856
diff changeset
   277
    val propss =
wenzelm
parents: 46856
diff changeset
   278
      (map o map) (fn prop => (mark_witness prop, [])) wit_propss @
wenzelm
parents: 46856
diff changeset
   279
        [map (rpair []) eq_props];
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   280
    fun after_qed' thmss =
29603
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
   281
      let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   282
      in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   283
  in proof after_qed' propss #> refine_witness #> Seq.hd end;
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   284
38108
b4115423c049 Interpretation in proofs supports mixins.
ballarin
parents: 36674
diff changeset
   285
fun proof_local cmd goal_ctxt int after_qed' propss =
45329
dd8208a3655a tuned whitespace;
wenzelm
parents: 45295
diff changeset
   286
  Proof.map_context (K goal_ctxt) #>
46899
58110c1e02bc refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;
wenzelm
parents: 46896
diff changeset
   287
  Proof.local_goal (K (K ())) (K I) Proof_Context.bind_propp_i cmd NONE
58110c1e02bc refined 'interpret': reset facts ("this") and print_result, which merely consist of internal / protected statement;
wenzelm
parents: 46896
diff changeset
   288
    after_qed' (map (pair Thm.empty_binding) propss);
41425
9acb7c501530 tuned whitespace
haftmann
parents: 41228
diff changeset
   289
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   290
in
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   291
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   292
fun witness_proof after_qed wit_propss =
36323
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 35767
diff changeset
   293
  gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits)
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   294
    wit_propss [];
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   295
36323
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 35767
diff changeset
   296
val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE);
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   297
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   298
fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
38108
b4115423c049 Interpretation in proofs supports mixins.
ballarin
parents: 36674
diff changeset
   299
  gen_witness_proof (proof_local cmd goal_ctxt int)
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   300
    (fn wits => fn _ => after_qed wits) wit_propss [];
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   301
38108
b4115423c049 Interpretation in proofs supports mixins.
ballarin
parents: 36674
diff changeset
   302
fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt int =
b4115423c049 Interpretation in proofs supports mixins.
ballarin
parents: 36674
diff changeset
   303
  gen_witness_proof (proof_local cmd goal_ctxt int) after_qed wit_propss eq_props;
41425
9acb7c501530 tuned whitespace
haftmann
parents: 41228
diff changeset
   304
29603
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
   305
end;
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
   306
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   307
25302
19b1729f1bd4 tuned satisfy_thm;
wenzelm
parents: 25285
diff changeset
   308
fun compose_witness (Witness (_, th)) r =
19b1729f1bd4 tuned satisfy_thm;
wenzelm
parents: 25285
diff changeset
   309
  let
19b1729f1bd4 tuned satisfy_thm;
wenzelm
parents: 25285
diff changeset
   310
    val th' = Goal.conclude th;
19b1729f1bd4 tuned satisfy_thm;
wenzelm
parents: 25285
diff changeset
   311
    val A = Thm.cprem_of r 1;
25739
9da2343deb92 Fixed eta constraction issue in compose_witness
ballarin
parents: 25624
diff changeset
   312
  in
9da2343deb92 Fixed eta constraction issue in compose_witness
ballarin
parents: 25624
diff changeset
   313
    Thm.implies_elim
9da2343deb92 Fixed eta constraction issue in compose_witness
ballarin
parents: 25624
diff changeset
   314
      (Conv.gconv_rule Drule.beta_eta_conversion 1 r)
9da2343deb92 Fixed eta constraction issue in compose_witness
ballarin
parents: 25624
diff changeset
   315
      (Conv.fconv_rule Drule.beta_eta_conversion
9da2343deb92 Fixed eta constraction issue in compose_witness
ballarin
parents: 25624
diff changeset
   316
        (Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th'))
9da2343deb92 Fixed eta constraction issue in compose_witness
ballarin
parents: 25624
diff changeset
   317
  end;
25302
19b1729f1bd4 tuned satisfy_thm;
wenzelm
parents: 25285
diff changeset
   318
29578
8c4e961fcb08 refined witness algebra
haftmann
parents: 29525
diff changeset
   319
fun conclude_witness (Witness (_, th)) =
41228
e1fce873b814 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
wenzelm
parents: 39557
diff changeset
   320
  Thm.close_derivation (Raw_Simplifier.norm_hhf_protect (Goal.conclude th));
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   321
22658
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22568
diff changeset
   322
fun pretty_witness ctxt witn =
24920
2a45e400fdad generic Syntax.pretty/string_of operations;
wenzelm
parents: 24637
diff changeset
   323
  let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
22658
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22568
diff changeset
   324
    Pretty.block (prt_term (witness_prop witn) ::
39166
19efc2af3e6c turned show_hyps and show_tags into proper configuration option;
wenzelm
parents: 38709
diff changeset
   325
      (if Config.get ctxt show_hyps then [Pretty.brk 2, Pretty.list "[" "]"
22658
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22568
diff changeset
   326
         (map prt_term (witness_hyps witn))] else []))
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22568
diff changeset
   327
  end;
263d42253f53 Experimental interpretation code for definitions.
ballarin
parents: 22568
diff changeset
   328
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   329
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   330
(* derived rules *)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   331
20007
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   332
fun instantiate_tfrees thy subst th =
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   333
  let
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   334
    val certT = Thm.ctyp_of thy;
20007
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   335
    val idx = Thm.maxidx_of th + 1;
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   336
    fun cert_inst (a, (S, T)) = (certT (TVar ((a, idx), S)), certT T);
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   337
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   338
    fun add_inst (a, S) insts =
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   339
      if AList.defined (op =) insts a then insts
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   340
      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
   341
    val insts =
45346
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   342
      (Term.fold_types o Term.fold_atyps) (fn TFree v => add_inst v | _ => I)
20007
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   343
        (Thm.full_prop_of th) [];
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   344
  in
20007
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   345
    th
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   346
    |> Thm.generalize (map fst insts, []) idx
8f9e6255108e instantiate_tfrees: Thm.generalize;
wenzelm
parents: 19931
diff changeset
   347
    |> Thm.instantiate (map cert_inst insts, [])
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   348
  end;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   349
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   350
fun instantiate_frees thy subst =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   351
  let val cert = Thm.cterm_of thy in
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   352
    Drule.forall_intr_list (map (cert o Free o fst) subst) #>
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   353
    Drule.forall_elim_list (map (cert o snd) subst)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   354
  end;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   355
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   356
fun hyps_rule rule th =
21521
095f4963beed simultaneous fact morphism;
wenzelm
parents: 21497
diff changeset
   357
  let val {hyps, ...} = Thm.crep_thm th in
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   358
    Drule.implies_elim_list
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   359
      (rule (Drule.implies_intr_list hyps th))
21521
095f4963beed simultaneous fact morphism;
wenzelm
parents: 21497
diff changeset
   360
      (map (Thm.assume o Drule.cterm_rule rule) hyps)
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   361
  end;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   362
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   363
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   364
(* instantiate types *)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   365
45346
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   366
fun instT_type_same env =
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   367
  if Symtab.is_empty env then Same.same
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   368
  else
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   369
    Term_Subst.map_atypsT_same
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   370
      (fn TFree (a, _) => (case Symtab.lookup env a of SOME T => T | NONE => raise Same.SAME)
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   371
        | _ => raise Same.SAME);
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   372
45346
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   373
fun instT_term_same env =
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   374
  if Symtab.is_empty env then Same.same
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   375
  else Term_Subst.map_types_same (instT_type_same env);
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   376
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   377
val instT_type = Same.commit o instT_type_same;
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   378
val instT_term = Same.commit o instT_term_same;
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   379
45346
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   380
fun instT_subst env th =
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   381
  (Thm.fold_terms o Term.fold_types o Term.fold_atyps)
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   382
    (fn T as TFree (a, _) =>
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   383
      let val T' = the_default T (Symtab.lookup env a)
45349
7fb63b469cd2 more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents: 45346
diff changeset
   384
      in if T = T' then I else insert (eq_fst (op =)) (a, T') end
45346
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   385
    | _ => I) th [];
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   386
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   387
fun instT_thm thy env th =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   388
  if Symtab.is_empty env then th
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   389
  else
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   390
    let val subst = instT_subst env th
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   391
    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
   392
22672
777af26d5713 inst(T)_morphism: avoid reference to static theory value;
wenzelm
parents: 22658
diff changeset
   393
fun instT_morphism thy env =
52788
da1fdbfebd39 type theory is purely value-oriented;
wenzelm
parents: 52732
diff changeset
   394
  Morphism.morphism
da1fdbfebd39 type theory is purely value-oriented;
wenzelm
parents: 52732
diff changeset
   395
   {binding = [],
da1fdbfebd39 type theory is purely value-oriented;
wenzelm
parents: 52732
diff changeset
   396
    typ = [instT_type env],
da1fdbfebd39 type theory is purely value-oriented;
wenzelm
parents: 52732
diff changeset
   397
    term = [instT_term env],
da1fdbfebd39 type theory is purely value-oriented;
wenzelm
parents: 52732
diff changeset
   398
    fact = [map (fn th => instT_thm thy env th)]};
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   399
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   400
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   401
(* instantiate types and terms *)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   402
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   403
fun inst_term (envT, env) =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   404
  if Symtab.is_empty env then instT_term envT
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   405
  else
45346
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   406
    instT_term envT #>
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   407
    Same.commit (Term_Subst.map_aterms_same
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   408
      (fn Free (x, _) => (case Symtab.lookup env x of SOME t => t | NONE => raise Same.SAME)
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   409
        | _ => raise Same.SAME)) #>
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   410
    Envir.beta_norm;
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   411
45349
7fb63b469cd2 more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents: 45346
diff changeset
   412
fun inst_subst (envT, env) th =
7fb63b469cd2 more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents: 45346
diff changeset
   413
  (Thm.fold_terms o Term.fold_aterms)
7fb63b469cd2 more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents: 45346
diff changeset
   414
    (fn Free (x, T) =>
7fb63b469cd2 more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents: 45346
diff changeset
   415
      let
7fb63b469cd2 more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents: 45346
diff changeset
   416
        val T' = instT_type envT T;
7fb63b469cd2 more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents: 45346
diff changeset
   417
        val t = Free (x, T');
7fb63b469cd2 more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents: 45346
diff changeset
   418
        val t' = the_default t (Symtab.lookup env x);
7fb63b469cd2 more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents: 45346
diff changeset
   419
      in if t aconv t' then I else insert (eq_fst (op =)) ((x, T'), t') end
7fb63b469cd2 more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents: 45346
diff changeset
   420
    | _ => I) th [];
7fb63b469cd2 more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents: 45346
diff changeset
   421
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   422
fun inst_thm thy (envT, env) th =
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   423
  if Symtab.is_empty env then instT_thm thy envT th
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   424
  else
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   425
    let
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   426
      val substT = instT_subst envT th;
45349
7fb63b469cd2 more uniform instT_subst vs. inst_subst: compare variable names only;
wenzelm
parents: 45346
diff changeset
   427
      val subst = inst_subst (envT, env) th;
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   428
    in
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   429
      if null substT andalso null subst then th
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   430
      else th |> hyps_rule
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   431
       (instantiate_tfrees thy substT #>
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   432
        instantiate_frees thy subst #>
22900
f8a7c10e1bd0 moved conversions to structure Conv;
wenzelm
parents: 22691
diff changeset
   433
        Conv.fconv_rule (Thm.beta_conversion true))
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   434
    end;
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   435
45346
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   436
fun inst_morphism thy (envT, env) =
52788
da1fdbfebd39 type theory is purely value-oriented;
wenzelm
parents: 52732
diff changeset
   437
  Morphism.morphism
da1fdbfebd39 type theory is purely value-oriented;
wenzelm
parents: 52732
diff changeset
   438
   {binding = [],
da1fdbfebd39 type theory is purely value-oriented;
wenzelm
parents: 52732
diff changeset
   439
    typ = [instT_type envT],
da1fdbfebd39 type theory is purely value-oriented;
wenzelm
parents: 52732
diff changeset
   440
    term = [inst_term (envT, env)],
da1fdbfebd39 type theory is purely value-oriented;
wenzelm
parents: 52732
diff changeset
   441
    fact = [map (fn th => inst_thm thy (envT, env) th)]};
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   442
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   443
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   444
(* satisfy hypotheses *)
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   445
45346
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   446
fun satisfy_thm witns thm =
439101d8eeec some performance tuning via Term_Subst/Same.operation;
wenzelm
parents: 45345
diff changeset
   447
  thm |> fold (fn hyp =>
19777
77929c3d2b74 added params_of, prems_of;
wenzelm
parents: 19731
diff changeset
   448
    (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
   449
      NONE => I
25302
19b1729f1bd4 tuned satisfy_thm;
wenzelm
parents: 25285
diff changeset
   450
    | 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
   451
29603
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
   452
val satisfy_morphism = Morphism.thm_morphism o satisfy_thm;
20264
f09a4003e12d added generalize_facts;
wenzelm
parents: 20233
diff changeset
   453
f09a4003e12d added generalize_facts;
wenzelm
parents: 20233
diff changeset
   454
29525
ad7991d7b5bb explicit equation morphism
haftmann
parents: 29218
diff changeset
   455
(* rewriting with equalities *)
ad7991d7b5bb explicit equation morphism
haftmann
parents: 29218
diff changeset
   456
46856
wenzelm
parents: 46728
diff changeset
   457
fun eq_morphism _ [] = NONE
wenzelm
parents: 46728
diff changeset
   458
  | eq_morphism thy thms =
wenzelm
parents: 46728
diff changeset
   459
      SOME (Morphism.morphism
wenzelm
parents: 46728
diff changeset
   460
       {binding = [],
wenzelm
parents: 46728
diff changeset
   461
        typ = [],
wenzelm
parents: 46728
diff changeset
   462
        term = [Raw_Simplifier.rewrite_term thy thms []],
52230
1105b3b5aa77 standardized aliases;
wenzelm
parents: 49750
diff changeset
   463
        fact = [map (rewrite_rule thms)]});
29525
ad7991d7b5bb explicit equation morphism
haftmann
parents: 29218
diff changeset
   464
ad7991d7b5bb explicit equation morphism
haftmann
parents: 29218
diff changeset
   465
29218
f7ffe90879e2 Transfer morphism with theory closure.
ballarin
parents: 29217
diff changeset
   466
30775
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   467
(** activate in context **)
28832
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   468
30775
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   469
(* init *)
28832
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   470
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42357
diff changeset
   471
fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
30775
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   472
  | init (Constrains _) = I
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   473
  | init (Assumes asms) = Context.map_proof (fn ctxt =>
28832
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   474
      let
47815
43f677b3ae91 clarified signature;
wenzelm
parents: 47249
diff changeset
   475
        val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms;
30775
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   476
        val (_, ctxt') = ctxt
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   477
          |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42357
diff changeset
   478
          |> Proof_Context.add_assms_i Assumption.assume_export asms';
30775
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   479
      in ctxt' end)
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   480
  | init (Defines defs) = Context.map_proof (fn ctxt =>
28832
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   481
      let
47815
43f677b3ae91 clarified signature;
wenzelm
parents: 47249
diff changeset
   482
        val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
49750
444cfaa331c9 clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
wenzelm
parents: 47815
diff changeset
   483
        val asms = defs' |> map (fn (b, (t, ps)) =>
444cfaa331c9 clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
wenzelm
parents: 47815
diff changeset
   484
            let val (_, t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
444cfaa331c9 clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
wenzelm
parents: 47815
diff changeset
   485
            in (t', (b, [(t', ps)])) end);
30775
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   486
        val (_, ctxt') = ctxt
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   487
          |> fold Variable.auto_fixes (map #1 asms)
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42357
diff changeset
   488
          |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
30775
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   489
      in ctxt' end)
47249
c0481c3c2a6c added Attrib.global_notes/local_notes/generic_notes convenience;
wenzelm
parents: 46899
diff changeset
   490
  | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
30775
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   491
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   492
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   493
(* activate *)
71f777103225 added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML;
wenzelm
parents: 30763
diff changeset
   494
30777
9960ff945c52 simplified Element.activate(_i): singleton version;
wenzelm
parents: 30775
diff changeset
   495
fun activate_i elem ctxt =
28832
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   496
  let
49750
444cfaa331c9 clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
wenzelm
parents: 47815
diff changeset
   497
    val elem' =
444cfaa331c9 clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
wenzelm
parents: 47815
diff changeset
   498
      (case map_ctxt_attrib Args.assignable elem of
444cfaa331c9 clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
wenzelm
parents: 47815
diff changeset
   499
        Defines defs =>
444cfaa331c9 clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
wenzelm
parents: 47815
diff changeset
   500
          Defines (defs |> map (fn ((a, atts), (t, ps)) =>
444cfaa331c9 clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
wenzelm
parents: 47815
diff changeset
   501
            ((Thm.def_binding_optional (Binding.name (#1 (#1 (Local_Defs.cert_def ctxt t)))) a, atts),
444cfaa331c9 clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
wenzelm
parents: 47815
diff changeset
   502
              (t, ps))))
444cfaa331c9 clarified Element.init vs. Element.activate: refrain from hard-wiring Thm.def_binding_optional to avoid duplicate facts;
wenzelm
parents: 47815
diff changeset
   503
      | e => e);
30777
9960ff945c52 simplified Element.activate(_i): singleton version;
wenzelm
parents: 30775
diff changeset
   504
    val ctxt' = Context.proof_map (init elem') ctxt;
9960ff945c52 simplified Element.activate(_i): singleton version;
wenzelm
parents: 30775
diff changeset
   505
  in (map_ctxt_attrib Args.closure elem', ctxt') end;
28832
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   506
30777
9960ff945c52 simplified Element.activate(_i): singleton version;
wenzelm
parents: 30775
diff changeset
   507
fun activate raw_elem ctxt =
9960ff945c52 simplified Element.activate(_i): singleton version;
wenzelm
parents: 30775
diff changeset
   508
  let val elem = raw_elem |> map_ctxt
43842
f035d867fb41 Element.activate: leave check of binding where actually applied to the context -- allow internal qualifications, or non-identifier fact names like "assumes *: A" (see also 1183951365de);
wenzelm
parents: 43837
diff changeset
   509
   {binding = I,
29603
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
   510
    typ = I,
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
   511
    term = I,
b660ee46f2f6 eliminated obsolete var morphism;
wenzelm
parents: 29578
diff changeset
   512
    pattern = I,
42360
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42357
diff changeset
   513
    fact = Proof_Context.get_fact ctxt,
da8817d01e7c modernized structure Proof_Context;
wenzelm
parents: 42357
diff changeset
   514
    attrib = Attrib.intern_src (Proof_Context.theory_of ctxt)}
30777
9960ff945c52 simplified Element.activate(_i): singleton version;
wenzelm
parents: 30775
diff changeset
   515
  in activate_i elem ctxt end;
28832
cf7237498e7a Activate elements moved to element.ML.
ballarin
parents: 28737
diff changeset
   516
19267
fdb4658eab26 added pretty_statement;
wenzelm
parents: 19259
diff changeset
   517
end;