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