src/Pure/Isar/calculation.ML
author wenzelm
Wed Jun 02 11:09:26 2010 +0200 (2010-06-02 ago)
changeset 37251 72c7e636067b
parent 37047 4a95a50d0ec4
child 38332 6551e310e7cb
permissions -rw-r--r--
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
     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.seq
    17   val also_cmd: (Facts.ref * Attrib.src list) list option ->
    18     bool -> Proof.state -> Proof.state Seq.seq
    19   val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
    20   val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
    21     Proof.state -> Proof.state 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 fun print_rules ctxt =
    41   let val ((trans, sym), _) = Data.get (Context.Proof ctxt) in
    42     [Pretty.big_list "transitivity rules:"
    43         (map (Display.pretty_thm ctxt) (Item_Net.content trans)),
    44       Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
    45     |> Pretty.chunks |> Pretty.writeln
    46   end;
    47 
    48 
    49 (* access calculation *)
    50 
    51 fun get_calculation state =
    52   (case #2 (Data.get (Context.Proof (Proof.context_of state))) of
    53     NONE => NONE
    54   | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
    55 
    56 val calculationN = "calculation";
    57 
    58 fun put_calculation calc =
    59   `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
    60      (Data.map (apsnd (K (Option.map (rpair lev) calc))))))
    61   #> Proof.put_thms false (calculationN, calc);
    62 
    63 
    64 
    65 (** attributes **)
    66 
    67 (* add/del rules *)
    68 
    69 val trans_add = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update);
    70 val trans_del = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove);
    71 
    72 val sym_add =
    73   Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.add_thm)
    74   #> Context_Rules.elim_query NONE;
    75 
    76 val sym_del =
    77   Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.del_thm)
    78   #> Context_Rules.rule_del;
    79 
    80 
    81 (* symmetric *)
    82 
    83 val symmetric = Thm.rule_attribute (fn x => fn th =>
    84   (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (Data.get x)))) of
    85     ([th'], _) => Drule.zero_var_indexes th'
    86   | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
    87   | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
    88 
    89 
    90 (* concrete syntax *)
    91 
    92 val _ = Context.>> (Context.map_theory
    93  (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
    94     "declaration of transitivity rule" #>
    95   Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
    96     "declaration of symmetry rule" #>
    97   Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
    98     "resolution with symmetry rule" #>
    99   PureThy.add_thms
   100    [((Binding.empty, transitive_thm), [trans_add]),
   101     ((Binding.empty, symmetric_thm), [sym_add])] #> snd));
   102 
   103 
   104 
   105 (** proof commands **)
   106 
   107 fun assert_sane final =
   108   if final then Proof.assert_forward else Proof.assert_forward_or_chain;
   109 
   110 fun maintain_calculation int final calc state =
   111   let
   112     val state' = put_calculation (SOME calc) state;
   113     val ctxt' = Proof.context_of state';
   114     val _ =
   115       if int then
   116         Pretty.writeln
   117           (ProofContext.pretty_fact ctxt'
   118             (ProofContext.full_name ctxt' (Binding.name calculationN), calc))
   119       else ();
   120   in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end;
   121 
   122 
   123 (* also and finally *)
   124 
   125 val get_rules = #1 o Data.get o Context.Proof o Proof.context_of;
   126 
   127 fun calculate prep_rules final raw_rules int state =
   128   let
   129     val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
   130     val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
   131     fun projection ths th = exists (curry eq_prop th) ths;
   132 
   133     val opt_rules = Option.map (prep_rules state) raw_rules;
   134     fun combine ths =
   135       (case opt_rules of SOME rules => rules
   136       | NONE =>
   137           (case ths of
   138             [] => Item_Net.content (#1 (get_rules state))
   139           | th :: _ => Item_Net.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
   140       |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
   141       |> Seq.filter (not o projection ths);
   142 
   143     val facts = Proof.the_facts (assert_sane final state);
   144     val (initial, calculations) =
   145       (case get_calculation state of
   146         NONE => (true, Seq.single facts)
   147       | SOME calc => (false, Seq.map single (combine (calc @ facts))));
   148 
   149     val _ = initial andalso final andalso error "No calculation yet";
   150     val _ = initial andalso is_some opt_rules andalso
   151       error "Initial calculation -- no rules to be given";
   152   in
   153     calculations |> Seq.map (fn calc => maintain_calculation int final calc state)
   154   end;
   155 
   156 val also = calculate (K I) false;
   157 val also_cmd = calculate Proof.get_thmss_cmd false;
   158 val finally = calculate (K I) true;
   159 val finally_cmd = calculate Proof.get_thmss_cmd true;
   160 
   161 
   162 (* moreover and ultimately *)
   163 
   164 fun collect final int state =
   165   let
   166     val facts = Proof.the_facts (assert_sane final state);
   167     val (initial, thms) =
   168       (case get_calculation state of
   169         NONE => (true, [])
   170       | SOME thms => (false, thms));
   171     val calc = thms @ facts;
   172     val _ = initial andalso final andalso error "No calculation yet";
   173   in maintain_calculation int final calc state end;
   174 
   175 val moreover = collect false;
   176 val ultimately = collect true;
   177 
   178 end;