src/Pure/Isar/calculation.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 30189 3633f560f4c3
child 30279 84097bba7bdc
permissions -rw-r--r--
use long names for old-style fold combinators;
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@26336
    16
  val also: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
wenzelm@17350
    17
  val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
wenzelm@30189
    18
  val finally: (Facts.ref * Attrib.src list) list option -> bool ->
wenzelm@22573
    19
    Proof.state -> Proof.state Seq.seq
wenzelm@17350
    20
  val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
wenzelm@17350
    21
  val moreover: bool -> Proof.state -> Proof.state
wenzelm@17350
    22
  val ultimately: bool -> Proof.state -> Proof.state
wenzelm@6778
    23
end;
wenzelm@6778
    24
wenzelm@6778
    25
structure Calculation: CALCULATION =
wenzelm@6778
    26
struct
wenzelm@6778
    27
wenzelm@18637
    28
(** calculation data **)
wenzelm@6778
    29
wenzelm@18637
    30
structure CalculationData = GenericDataFun
wenzelm@18637
    31
(
wenzelm@12379
    32
  type T = (thm NetRules.T * thm list) * (thm list * int) option;
wenzelm@18637
    33
  val empty = ((NetRules.elim, []), NONE);
wenzelm@18637
    34
  val extend = I;
wenzelm@6778
    35
wenzelm@18637
    36
  fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
wenzelm@24039
    37
    ((NetRules.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
wenzelm@18637
    38
);
wenzelm@18637
    39
wenzelm@22846
    40
fun print_rules ctxt =
wenzelm@22846
    41
  let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
wenzelm@22846
    42
    [Pretty.big_list "transitivity rules:"
wenzelm@22846
    43
        (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
wenzelm@22846
    44
      Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
wenzelm@22846
    45
    |> Pretty.chunks |> Pretty.writeln
wenzelm@22846
    46
  end;
wenzelm@6778
    47
wenzelm@6778
    48
wenzelm@6778
    49
(* access calculation *)
wenzelm@6778
    50
wenzelm@6778
    51
fun get_calculation state =
wenzelm@18637
    52
  (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of
skalberg@15531
    53
    NONE => NONE
skalberg@15531
    54
  | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
wenzelm@6778
    55
wenzelm@17350
    56
val calculationN = "calculation";
wenzelm@6778
    57
wenzelm@17350
    58
fun put_calculation calc =
wenzelm@18728
    59
  `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
wenzelm@18728
    60
     (CalculationData.map (apsnd (K (Option.map (rpair lev) calc))))))
wenzelm@26252
    61
  #> Proof.put_thms false (calculationN, calc);
wenzelm@6778
    62
wenzelm@6778
    63
wenzelm@18637
    64
wenzelm@6778
    65
(** attributes **)
wenzelm@6778
    66
wenzelm@12379
    67
(* add/del rules *)
wenzelm@12379
    68
wenzelm@18728
    69
val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.insert);
wenzelm@18728
    70
val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete);
wenzelm@6778
    71
wenzelm@18637
    72
val sym_add =
wenzelm@24039
    73
  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
wenzelm@18637
    74
  #> ContextRules.elim_query NONE;
wenzelm@18637
    75
val sym_del =
wenzelm@24039
    76
  Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm)
wenzelm@18637
    77
  #> ContextRules.rule_del;
wenzelm@12379
    78
wenzelm@12379
    79
wenzelm@18637
    80
(* symmetric *)
wenzelm@12379
    81
wenzelm@18728
    82
val symmetric = Thm.rule_attribute (fn x => fn th =>
wenzelm@19861
    83
  (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
wenzelm@20898
    84
    ([th'], _) => Drule.zero_var_indexes th'
wenzelm@12379
    85
  | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
wenzelm@12379
    86
  | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
wenzelm@12379
    87
wenzelm@6778
    88
wenzelm@6778
    89
(* concrete syntax *)
wenzelm@6778
    90
wenzelm@18637
    91
val trans_att = Attrib.add_del_args trans_add trans_del;
wenzelm@18637
    92
val sym_att = Attrib.add_del_args sym_add sym_del;
wenzelm@12379
    93
wenzelm@26463
    94
val _ = Context.>> (Context.map_theory
wenzelm@18708
    95
 (Attrib.add_attributes
wenzelm@18728
    96
   [("trans", trans_att, "declaration of transitivity rule"),
wenzelm@18728
    97
    ("sym", sym_att, "declaration of symmetry rule"),
wenzelm@18728
    98
    ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
wenzelm@18708
    99
  PureThy.add_thms
haftmann@29579
   100
   [((Binding.empty, transitive_thm), [trans_add]),
haftmann@29579
   101
    ((Binding.empty, symmetric_thm), [sym_add])] #> snd));
wenzelm@15801
   102
wenzelm@6778
   103
wenzelm@6787
   104
wenzelm@6778
   105
(** proof commands **)
wenzelm@6778
   106
wenzelm@18678
   107
fun err_if b msg = if b then error msg else ();
wenzelm@17350
   108
wenzelm@14555
   109
fun assert_sane final =
wenzelm@14555
   110
  if final then Proof.assert_forward else Proof.assert_forward_or_chain;
wenzelm@14555
   111
wenzelm@17350
   112
fun maintain_calculation false calc = put_calculation (SOME calc)
wenzelm@17350
   113
  | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc;
wenzelm@6778
   114
wenzelm@17350
   115
fun print_calculation false _ _ = ()
wenzelm@28210
   116
  | print_calculation true ctxt calc = Pretty.writeln
haftmann@28965
   117
      (ProofContext.pretty_fact ctxt (ProofContext.full_bname ctxt calculationN, calc));
wenzelm@8562
   118
wenzelm@8562
   119
wenzelm@17350
   120
(* also and finally *)
wenzelm@8562
   121
wenzelm@18637
   122
val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of;
wenzelm@18637
   123
wenzelm@17350
   124
fun calculate prep_rules final raw_rules int state =
wenzelm@6778
   125
  let
wenzelm@12805
   126
    val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
wenzelm@18947
   127
    val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
wenzelm@11097
   128
    fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
wenzelm@8300
   129
wenzelm@17350
   130
    val opt_rules = Option.map (prep_rules state) raw_rules;
wenzelm@11097
   131
    fun combine ths =
skalberg@15531
   132
      (case opt_rules of SOME rules => rules
skalberg@15531
   133
      | NONE =>
wenzelm@18637
   134
          (case ths of [] => NetRules.rules (#1 (get_rules state))
wenzelm@18637
   135
          | th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
wenzelm@18223
   136
      |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
wenzelm@11097
   137
      |> Seq.filter (not o projection ths);
wenzelm@7414
   138
wenzelm@14555
   139
    val facts = Proof.the_facts (assert_sane final state);
wenzelm@6903
   140
    val (initial, calculations) =
wenzelm@6778
   141
      (case get_calculation state of
skalberg@15531
   142
        NONE => (true, Seq.single facts)
skalberg@15531
   143
      | SOME calc => (false, Seq.map single (combine (calc @ facts))));
wenzelm@6778
   144
  in
wenzelm@18678
   145
    err_if (initial andalso final) "No calculation yet";
wenzelm@18678
   146
    err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
wenzelm@17350
   147
    calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc;
wenzelm@12055
   148
        state |> maintain_calculation final calc))
wenzelm@6778
   149
  end;
wenzelm@6778
   150
wenzelm@17350
   151
val also = calculate Proof.get_thmss false;
wenzelm@17350
   152
val also_i = calculate (K I) false;
wenzelm@30189
   153
val finally = calculate Proof.get_thmss true;
wenzelm@17350
   154
val finally_i = calculate (K I) true;
wenzelm@6778
   155
wenzelm@6778
   156
wenzelm@17350
   157
(* moreover and ultimately *)
wenzelm@8562
   158
wenzelm@17350
   159
fun collect final int state =
wenzelm@8588
   160
  let
wenzelm@14555
   161
    val facts = Proof.the_facts (assert_sane final state);
wenzelm@8588
   162
    val (initial, thms) =
wenzelm@8588
   163
      (case get_calculation state of
skalberg@15531
   164
        NONE => (true, [])
skalberg@15531
   165
      | SOME thms => (false, thms));
wenzelm@8588
   166
    val calc = thms @ facts;
wenzelm@8588
   167
  in
wenzelm@18678
   168
    err_if (initial andalso final) "No calculation yet";
wenzelm@17350
   169
    print_calculation int (Proof.context_of state) calc;
wenzelm@8588
   170
    state |> maintain_calculation final calc
wenzelm@8588
   171
  end;
wenzelm@8588
   172
wenzelm@17350
   173
val moreover = collect false;
wenzelm@17350
   174
val ultimately = collect true;
wenzelm@8562
   175
wenzelm@6778
   176
end;