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