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