src/Pure/Isar/calculation.ML
author wenzelm
Fri Mar 29 22:14:27 2013 +0100 (2013-03-29)
changeset 51580 64ef8260dc60
parent 49868 3039922ffd8d
child 51584 98029ceda8ce
permissions -rw-r--r--
Pretty.item markup for improved readability of lists of items;
wenzelm@6778
     1
(*  Title:      Pure/Isar/calculation.ML
wenzelm@6778
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6778
     3
wenzelm@17350
     4
Generic calculational proofs.
wenzelm@6778
     5
*)
wenzelm@6778
     6
wenzelm@6778
     7
signature CALCULATION =
wenzelm@6778
     8
sig
wenzelm@21506
     9
  val print_rules: Proof.context -> unit
wenzelm@16571
    10
  val get_calculation: Proof.state -> thm list option
wenzelm@18728
    11
  val trans_add: attribute
wenzelm@18728
    12
  val trans_del: attribute
wenzelm@18728
    13
  val sym_add: attribute
wenzelm@18728
    14
  val sym_del: attribute
wenzelm@18728
    15
  val symmetric: attribute
wenzelm@49868
    16
  val also: thm list option -> bool -> Proof.state -> Proof.state Seq.result Seq.seq
wenzelm@37047
    17
  val also_cmd: (Facts.ref * Attrib.src list) list option ->
wenzelm@49868
    18
    bool -> Proof.state -> Proof.state Seq.result Seq.seq
wenzelm@49868
    19
  val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.result Seq.seq
wenzelm@36323
    20
  val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
wenzelm@49868
    21
    Proof.state -> Proof.state Seq.result Seq.seq
wenzelm@17350
    22
  val moreover: bool -> Proof.state -> Proof.state
wenzelm@17350
    23
  val ultimately: bool -> Proof.state -> Proof.state
wenzelm@6778
    24
end;
wenzelm@6778
    25
wenzelm@6778
    26
structure Calculation: CALCULATION =
wenzelm@6778
    27
struct
wenzelm@6778
    28
wenzelm@18637
    29
(** calculation data **)
wenzelm@6778
    30
wenzelm@37047
    31
structure Data = Generic_Data
wenzelm@18637
    32
(
wenzelm@30560
    33
  type T = (thm Item_Net.T * thm list) * (thm list * int) option;
wenzelm@30560
    34
  val empty = ((Thm.elim_rules, []), NONE);
wenzelm@18637
    35
  val extend = I;
wenzelm@33519
    36
  fun merge (((trans1, sym1), _), ((trans2, sym2), _)) =
wenzelm@30560
    37
    ((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
wenzelm@18637
    38
);
wenzelm@18637
    39
wenzelm@38332
    40
val get_rules = #1 o Data.get o Context.Proof;
wenzelm@38332
    41
wenzelm@22846
    42
fun print_rules ctxt =
wenzelm@38332
    43
  let val (trans, sym) = get_rules ctxt in
wenzelm@51580
    44
   [Pretty.big_list "transitivity rules:"
wenzelm@51580
    45
     (map (Pretty.item o single o Display.pretty_thm ctxt) (Item_Net.content trans)),
wenzelm@51580
    46
    Pretty.big_list "symmetry rules:"
wenzelm@51580
    47
     (map (Pretty.item o single o Display.pretty_thm ctxt) sym)]
wenzelm@51580
    48
  end |> Pretty.chunks |> Pretty.writeln;
wenzelm@6778
    49
wenzelm@6778
    50
wenzelm@6778
    51
(* access calculation *)
wenzelm@6778
    52
wenzelm@6778
    53
fun get_calculation state =
wenzelm@37047
    54
  (case #2 (Data.get (Context.Proof (Proof.context_of state))) of
skalberg@15531
    55
    NONE => NONE
skalberg@15531
    56
  | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
wenzelm@6778
    57
wenzelm@17350
    58
val calculationN = "calculation";
wenzelm@6778
    59
wenzelm@17350
    60
fun put_calculation calc =
wenzelm@18728
    61
  `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
wenzelm@37047
    62
     (Data.map (apsnd (K (Option.map (rpair lev) calc))))))
wenzelm@26252
    63
  #> Proof.put_thms false (calculationN, calc);
wenzelm@6778
    64
wenzelm@6778
    65
wenzelm@18637
    66
wenzelm@6778
    67
(** attributes **)
wenzelm@6778
    68
wenzelm@12379
    69
(* add/del rules *)
wenzelm@12379
    70
wenzelm@37047
    71
val trans_add = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update);
wenzelm@37047
    72
val trans_del = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove);
wenzelm@6778
    73
wenzelm@18637
    74
val sym_add =
wenzelm@45375
    75
  Thm.declaration_attribute (fn th =>
wenzelm@45375
    76
    (Data.map o apfst o apsnd) (Thm.add_thm th) #>
wenzelm@45375
    77
    Thm.attribute_declaration (Context_Rules.elim_query NONE) th);
wenzelm@33369
    78
wenzelm@18637
    79
val sym_del =
wenzelm@45375
    80
  Thm.declaration_attribute (fn th =>
wenzelm@45375
    81
    (Data.map o apfst o apsnd) (Thm.del_thm th) #>
wenzelm@45375
    82
    Thm.attribute_declaration Context_Rules.rule_del th);
wenzelm@12379
    83
wenzelm@12379
    84
wenzelm@18637
    85
(* symmetric *)
wenzelm@12379
    86
wenzelm@18728
    87
val symmetric = Thm.rule_attribute (fn x => fn th =>
wenzelm@37047
    88
  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (Data.get x)))) of
wenzelm@20898
    89
    ([th'], _) => Drule.zero_var_indexes th'
wenzelm@12379
    90
  | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
wenzelm@12379
    91
  | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
wenzelm@12379
    92
wenzelm@6778
    93
wenzelm@6778
    94
(* concrete syntax *)
wenzelm@6778
    95
wenzelm@26463
    96
val _ = Context.>> (Context.map_theory
wenzelm@30528
    97
 (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
wenzelm@30528
    98
    "declaration of transitivity rule" #>
wenzelm@30528
    99
  Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
wenzelm@30528
   100
    "declaration of symmetry rule" #>
wenzelm@30528
   101
  Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
wenzelm@30528
   102
    "resolution with symmetry rule" #>
wenzelm@39557
   103
  Global_Theory.add_thms
haftmann@29579
   104
   [((Binding.empty, transitive_thm), [trans_add]),
haftmann@29579
   105
    ((Binding.empty, symmetric_thm), [sym_add])] #> snd));
wenzelm@15801
   106
wenzelm@6778
   107
wenzelm@6787
   108
wenzelm@6778
   109
(** proof commands **)
wenzelm@6778
   110
wenzelm@14555
   111
fun assert_sane final =
wenzelm@14555
   112
  if final then Proof.assert_forward else Proof.assert_forward_or_chain;
wenzelm@14555
   113
wenzelm@37047
   114
fun maintain_calculation int final calc state =
wenzelm@37047
   115
  let
wenzelm@37047
   116
    val state' = put_calculation (SOME calc) state;
wenzelm@37047
   117
    val ctxt' = Proof.context_of state';
wenzelm@37047
   118
    val _ =
wenzelm@37047
   119
      if int then
wenzelm@37047
   120
        Pretty.writeln
wenzelm@42360
   121
          (Proof_Context.pretty_fact ctxt'
wenzelm@42360
   122
            (Proof_Context.full_name ctxt' (Binding.name calculationN), calc))
wenzelm@37047
   123
      else ();
wenzelm@37047
   124
  in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
wenzelm@8562
   125
wenzelm@8562
   126
wenzelm@17350
   127
(* also and finally *)
wenzelm@8562
   128
wenzelm@17350
   129
fun calculate prep_rules final raw_rules int state =
wenzelm@6778
   130
  let
wenzelm@38332
   131
    val ctxt = Proof.context_of state;
wenzelm@49868
   132
    val pretty_thm = Display.pretty_thm ctxt;
wenzelm@38332
   133
wenzelm@12805
   134
    val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
wenzelm@18947
   135
    val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
wenzelm@49868
   136
    fun check_projection ths th =
wenzelm@49868
   137
      (case find_index (curry eq_prop th) ths of
wenzelm@49868
   138
        ~1 => Seq.Result [th]
wenzelm@49868
   139
      | i =>
wenzelm@49868
   140
          Seq.Error (fn () =>
wenzelm@49868
   141
            (Pretty.string_of o Pretty.chunks)
wenzelm@49868
   142
             [Pretty.block [Pretty.str "Vacuous calculation result:", Pretty.brk 1, pretty_thm th],
wenzelm@49868
   143
              (Pretty.block o Pretty.fbreaks)
wenzelm@49868
   144
                (Pretty.str ("derived as projection (" ^ string_of_int (i + 1) ^ ") from:") ::
wenzelm@49868
   145
                  map pretty_thm ths)]));
wenzelm@8300
   146
wenzelm@38332
   147
    val opt_rules = Option.map (prep_rules ctxt) raw_rules;
wenzelm@11097
   148
    fun combine ths =
wenzelm@49868
   149
      Seq.append
wenzelm@49868
   150
        ((case opt_rules of
wenzelm@49868
   151
          SOME rules => rules
wenzelm@49868
   152
        | NONE =>
wenzelm@49868
   153
            (case ths of
wenzelm@49868
   154
              [] => Item_Net.content (#1 (get_rules ctxt))
wenzelm@49868
   155
            | th :: _ => Item_Net.retrieve (#1 (get_rules ctxt)) (strip_assums_concl th)))
wenzelm@49868
   156
        |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
wenzelm@49868
   157
        |> Seq.map (check_projection ths))
wenzelm@49868
   158
        (Seq.single (Seq.Error (fn () =>
wenzelm@49868
   159
          (Pretty.string_of o Pretty.block o Pretty.fbreaks)
wenzelm@49868
   160
            (Pretty.str "No matching trans rules for calculation:" ::
wenzelm@49868
   161
              map pretty_thm ths))));
wenzelm@7414
   162
wenzelm@14555
   163
    val facts = Proof.the_facts (assert_sane final state);
wenzelm@6903
   164
    val (initial, calculations) =
wenzelm@6778
   165
      (case get_calculation state of
wenzelm@49868
   166
        NONE => (true, Seq.single (Seq.Result facts))
wenzelm@49868
   167
      | SOME calc => (false, combine (calc @ facts)));
wenzelm@37047
   168
wenzelm@37047
   169
    val _ = initial andalso final andalso error "No calculation yet";
wenzelm@37047
   170
    val _ = initial andalso is_some opt_rules andalso
wenzelm@37047
   171
      error "Initial calculation -- no rules to be given";
wenzelm@6778
   172
  in
wenzelm@49868
   173
    calculations |> Seq.map_result (fn calc => maintain_calculation int final calc state)
wenzelm@6778
   174
  end;
wenzelm@6778
   175
wenzelm@36323
   176
val also = calculate (K I) false;
wenzelm@38332
   177
val also_cmd = calculate Attrib.eval_thms false;
wenzelm@36323
   178
val finally = calculate (K I) true;
wenzelm@38332
   179
val finally_cmd = calculate Attrib.eval_thms true;
wenzelm@6778
   180
wenzelm@6778
   181
wenzelm@17350
   182
(* moreover and ultimately *)
wenzelm@8562
   183
wenzelm@17350
   184
fun collect final int state =
wenzelm@8588
   185
  let
wenzelm@14555
   186
    val facts = Proof.the_facts (assert_sane final state);
wenzelm@8588
   187
    val (initial, thms) =
wenzelm@8588
   188
      (case get_calculation state of
skalberg@15531
   189
        NONE => (true, [])
skalberg@15531
   190
      | SOME thms => (false, thms));
wenzelm@8588
   191
    val calc = thms @ facts;
wenzelm@37047
   192
    val _ = initial andalso final andalso error "No calculation yet";
wenzelm@37047
   193
  in maintain_calculation int final calc state end;
wenzelm@8588
   194
wenzelm@17350
   195
val moreover = collect false;
wenzelm@17350
   196
val ultimately = collect true;
wenzelm@8562
   197
wenzelm@6778
   198
end;