src/Pure/Isar/calculation.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 18678 dd0c569fa43d
child 18728 6790126ab5f6
permissions -rw-r--r--
setup: theory -> theory;
wenzelm@6778
     1
(*  Title:      Pure/Isar/calculation.ML
wenzelm@6778
     2
    ID:         $Id$
wenzelm@6778
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6778
     4
wenzelm@17350
     5
Generic calculational proofs.
wenzelm@6778
     6
*)
wenzelm@6778
     7
wenzelm@6778
     8
signature CALCULATION =
wenzelm@6778
     9
sig
wenzelm@18637
    10
  val print_rules: Context.generic -> unit
wenzelm@16571
    11
  val get_calculation: Proof.state -> thm list option
wenzelm@18637
    12
  val trans_add: Context.generic attribute
wenzelm@18637
    13
  val trans_del: Context.generic attribute
wenzelm@18637
    14
  val sym_add: Context.generic attribute
wenzelm@18637
    15
  val sym_del: Context.generic attribute
wenzelm@18637
    16
  val symmetric: Context.generic attribute
wenzelm@17350
    17
  val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
wenzelm@17350
    18
  val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
wenzelm@18637
    19
  val finally: (thmref * Attrib.src list) list option -> bool -> 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@6778
    32
  val name = "Isar/calculation";
wenzelm@12379
    33
  type T = (thm NetRules.T * thm list) * (thm list * int) option;
wenzelm@18637
    34
  val empty = ((NetRules.elim, []), NONE);
wenzelm@18637
    35
  val extend = I;
wenzelm@6778
    36
wenzelm@18637
    37
  fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
wenzelm@18637
    38
    ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE);
wenzelm@6778
    39
wenzelm@18637
    40
  fun print generic ((trans, sym), _) =
wenzelm@18637
    41
    let val ctxt = Context.proof_of generic in
wenzelm@18637
    42
      [Pretty.big_list "transitivity rules:"
wenzelm@18637
    43
          (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
wenzelm@18637
    44
        Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
wenzelm@18637
    45
      |> Pretty.chunks |> Pretty.writeln
wenzelm@18637
    46
    end;
wenzelm@18637
    47
);
wenzelm@18637
    48
wenzelm@18708
    49
val _ = Context.add_setup CalculationData.init;
wenzelm@18637
    50
val print_rules = CalculationData.print;
wenzelm@6778
    51
wenzelm@6778
    52
wenzelm@6778
    53
(* access calculation *)
wenzelm@6778
    54
wenzelm@6778
    55
fun get_calculation state =
wenzelm@18637
    56
  (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of
skalberg@15531
    57
    NONE => NONE
skalberg@15531
    58
  | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
wenzelm@6778
    59
wenzelm@17350
    60
val calculationN = "calculation";
wenzelm@6778
    61
wenzelm@17350
    62
fun put_calculation calc =
wenzelm@18637
    63
  `Proof.level #-> (fn lev =>
wenzelm@18637
    64
    Proof.map_context (Context.the_proof o
wenzelm@18637
    65
        CalculationData.map (apsnd (K (Option.map (rpair lev) calc))) o Context.Proof))
wenzelm@17350
    66
  #> Proof.put_thms (calculationN, calc);
wenzelm@6778
    67
wenzelm@6778
    68
wenzelm@18637
    69
wenzelm@6778
    70
(** attributes **)
wenzelm@6778
    71
wenzelm@12379
    72
(* add/del rules *)
wenzelm@12379
    73
wenzelm@18637
    74
val trans_add = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.insert);
wenzelm@18637
    75
val trans_del = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.delete);
wenzelm@6778
    76
wenzelm@18637
    77
val sym_add =
wenzelm@18637
    78
  Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.add_rule)
wenzelm@18637
    79
  #> ContextRules.elim_query NONE;
wenzelm@18637
    80
val sym_del =
wenzelm@18637
    81
  Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.del_rule)
wenzelm@18637
    82
  #> ContextRules.rule_del;
wenzelm@12379
    83
wenzelm@12379
    84
wenzelm@18637
    85
(* symmetric *)
wenzelm@12379
    86
wenzelm@18637
    87
val symmetric = Attrib.rule (fn x => fn th =>
wenzelm@18637
    88
  (case Seq.chop (2, Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
wenzelm@12379
    89
    ([th'], _) => 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@18637
    96
val trans_att = Attrib.add_del_args trans_add trans_del;
wenzelm@18637
    97
val sym_att = Attrib.add_del_args sym_add sym_del;
wenzelm@12379
    98
wenzelm@15801
    99
val _ = Context.add_setup
wenzelm@18708
   100
 (Attrib.add_attributes
wenzelm@18637
   101
   [("trans", Attrib.common trans_att, "declaration of transitivity rule"),
wenzelm@18637
   102
    ("sym", Attrib.common sym_att, "declaration of symmetry rule"),
wenzelm@18708
   103
    ("symmetric", Attrib.common (Attrib.no_args symmetric), "resolution with symmetry rule")] #>
wenzelm@18708
   104
  PureThy.add_thms
wenzelm@18637
   105
   [(("", transitive_thm), [Attrib.theory trans_add]),
wenzelm@18708
   106
    (("", symmetric_thm), [Attrib.theory sym_add])] #> snd);
wenzelm@15801
   107
wenzelm@6778
   108
wenzelm@6787
   109
wenzelm@6778
   110
(** proof commands **)
wenzelm@6778
   111
wenzelm@18678
   112
fun err_if b msg = if b then error msg else ();
wenzelm@17350
   113
wenzelm@14555
   114
fun assert_sane final =
wenzelm@14555
   115
  if final then Proof.assert_forward else Proof.assert_forward_or_chain;
wenzelm@14555
   116
wenzelm@17350
   117
fun maintain_calculation false calc = put_calculation (SOME calc)
wenzelm@17350
   118
  | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc;
wenzelm@6778
   119
wenzelm@17350
   120
fun print_calculation false _ _ = ()
wenzelm@17350
   121
  | print_calculation true ctxt calc =
wenzelm@17350
   122
      Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc));
wenzelm@8562
   123
wenzelm@8562
   124
wenzelm@17350
   125
(* also and finally *)
wenzelm@8562
   126
wenzelm@18637
   127
val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of;
wenzelm@18637
   128
wenzelm@17350
   129
fun calculate prep_rules final raw_rules int state =
wenzelm@6778
   130
  let
wenzelm@12805
   131
    val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
wenzelm@9322
   132
    val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
wenzelm@11097
   133
    fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
wenzelm@8300
   134
wenzelm@17350
   135
    val opt_rules = Option.map (prep_rules state) raw_rules;
wenzelm@11097
   136
    fun combine ths =
skalberg@15531
   137
      (case opt_rules of SOME rules => rules
skalberg@15531
   138
      | NONE =>
wenzelm@18637
   139
          (case ths of [] => NetRules.rules (#1 (get_rules state))
wenzelm@18637
   140
          | th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
wenzelm@18223
   141
      |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
wenzelm@11097
   142
      |> Seq.filter (not o projection ths);
wenzelm@7414
   143
wenzelm@14555
   144
    val facts = Proof.the_facts (assert_sane final state);
wenzelm@6903
   145
    val (initial, calculations) =
wenzelm@6778
   146
      (case get_calculation state of
skalberg@15531
   147
        NONE => (true, Seq.single facts)
skalberg@15531
   148
      | SOME calc => (false, Seq.map single (combine (calc @ facts))));
wenzelm@6778
   149
  in
wenzelm@18678
   150
    err_if (initial andalso final) "No calculation yet";
wenzelm@18678
   151
    err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
wenzelm@17350
   152
    calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc;
wenzelm@12055
   153
        state |> maintain_calculation final calc))
wenzelm@6778
   154
  end;
wenzelm@6778
   155
wenzelm@17350
   156
val also = calculate Proof.get_thmss false;
wenzelm@17350
   157
val also_i = calculate (K I) false;
wenzelm@17350
   158
val finally = calculate Proof.get_thmss true;
wenzelm@17350
   159
val finally_i = calculate (K I) true;
wenzelm@6778
   160
wenzelm@6778
   161
wenzelm@17350
   162
(* moreover and ultimately *)
wenzelm@8562
   163
wenzelm@17350
   164
fun collect final int state =
wenzelm@8588
   165
  let
wenzelm@14555
   166
    val facts = Proof.the_facts (assert_sane final state);
wenzelm@8588
   167
    val (initial, thms) =
wenzelm@8588
   168
      (case get_calculation state of
skalberg@15531
   169
        NONE => (true, [])
skalberg@15531
   170
      | SOME thms => (false, thms));
wenzelm@8588
   171
    val calc = thms @ facts;
wenzelm@8588
   172
  in
wenzelm@18678
   173
    err_if (initial andalso final) "No calculation yet";
wenzelm@17350
   174
    print_calculation int (Proof.context_of state) calc;
wenzelm@8588
   175
    state |> maintain_calculation final calc
wenzelm@8588
   176
  end;
wenzelm@8588
   177
wenzelm@17350
   178
val moreover = collect false;
wenzelm@17350
   179
val ultimately = collect true;
wenzelm@8562
   180
wenzelm@6778
   181
end;