src/Pure/Isar/calculation.ML
author wenzelm
Sun Jul 08 19:51:58 2007 +0200 (2007-07-08)
changeset 23655 d2d1138e0ddc
parent 22846 fb79144af9a3
child 24039 273698405054
permissions -rw-r--r--
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
     1 (*  Title:      Pure/Isar/calculation.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Generic calculational proofs.
     6 *)
     7 
     8 signature CALCULATION =
     9 sig
    10   val print_rules: Proof.context -> unit
    11   val get_calculation: Proof.state -> thm list option
    12   val trans_add: attribute
    13   val trans_del: attribute
    14   val sym_add: attribute
    15   val sym_del: attribute
    16   val symmetric: attribute
    17   val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
    18   val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
    19   val finally_: (thmref * Attrib.src list) list option -> bool ->
    20     Proof.state -> Proof.state Seq.seq
    21   val finally_i: thm list option -> bool -> 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 CalculationData = GenericDataFun
    32 (
    33   type T = (thm NetRules.T * thm list) * (thm list * int) option;
    34   val empty = ((NetRules.elim, []), NONE);
    35   val extend = I;
    36 
    37   fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
    38     ((NetRules.merge (trans1, trans2), Drule.merge_rules (sym1, sym2)), NONE);
    39 );
    40 
    41 fun print_rules ctxt =
    42   let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in
    43     [Pretty.big_list "transitivity rules:"
    44         (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
    45       Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
    46     |> Pretty.chunks |> Pretty.writeln
    47   end;
    48 
    49 
    50 (* access calculation *)
    51 
    52 fun get_calculation state =
    53   (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of
    54     NONE => NONE
    55   | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
    56 
    57 val calculationN = "calculation";
    58 
    59 fun put_calculation calc =
    60   `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map
    61      (CalculationData.map (apsnd (K (Option.map (rpair lev) calc))))))
    62   #> Proof.put_thms (calculationN, calc);
    63 
    64 
    65 
    66 (** attributes **)
    67 
    68 (* add/del rules *)
    69 
    70 val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.insert);
    71 val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o NetRules.delete);
    72 
    73 val sym_add =
    74   Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.add_rule)
    75   #> ContextRules.elim_query NONE;
    76 val sym_del =
    77   Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Drule.del_rule)
    78   #> ContextRules.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 (CalculationData.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 trans_att = Attrib.add_del_args trans_add trans_del;
    93 val sym_att = Attrib.add_del_args sym_add sym_del;
    94 
    95 val _ = Context.add_setup
    96  (Attrib.add_attributes
    97    [("trans", trans_att, "declaration of transitivity rule"),
    98     ("sym", sym_att, "declaration of symmetry rule"),
    99     ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
   100   PureThy.add_thms
   101    [(("", transitive_thm), [trans_add]),
   102     (("", symmetric_thm), [sym_add])] #> snd);
   103 
   104 
   105 
   106 (** proof commands **)
   107 
   108 fun err_if b msg = if b then error msg else ();
   109 
   110 fun assert_sane final =
   111   if final then Proof.assert_forward else Proof.assert_forward_or_chain;
   112 
   113 fun maintain_calculation false calc = put_calculation (SOME calc)
   114   | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc;
   115 
   116 fun print_calculation false _ _ = ()
   117   | print_calculation true ctxt calc =
   118       Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc));
   119 
   120 
   121 (* also and finally *)
   122 
   123 val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of;
   124 
   125 fun calculate prep_rules final raw_rules int state =
   126   let
   127     val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
   128     val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
   129     fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
   130 
   131     val opt_rules = Option.map (prep_rules state) raw_rules;
   132     fun combine ths =
   133       (case opt_rules of SOME rules => rules
   134       | NONE =>
   135           (case ths of [] => NetRules.rules (#1 (get_rules state))
   136           | th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
   137       |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
   138       |> Seq.filter (not o projection ths);
   139 
   140     val facts = Proof.the_facts (assert_sane final state);
   141     val (initial, calculations) =
   142       (case get_calculation state of
   143         NONE => (true, Seq.single facts)
   144       | SOME calc => (false, Seq.map single (combine (calc @ facts))));
   145   in
   146     err_if (initial andalso final) "No calculation yet";
   147     err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
   148     calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc;
   149         state |> maintain_calculation final calc))
   150   end;
   151 
   152 val also = calculate Proof.get_thmss false;
   153 val also_i = calculate (K I) false;
   154 val finally_ = calculate Proof.get_thmss true;
   155 val finally_i = calculate (K I) true;
   156 
   157 
   158 (* moreover and ultimately *)
   159 
   160 fun collect final int state =
   161   let
   162     val facts = Proof.the_facts (assert_sane final state);
   163     val (initial, thms) =
   164       (case get_calculation state of
   165         NONE => (true, [])
   166       | SOME thms => (false, thms));
   167     val calc = thms @ facts;
   168   in
   169     err_if (initial andalso final) "No calculation yet";
   170     print_calculation int (Proof.context_of state) calc;
   171     state |> maintain_calculation final calc
   172   end;
   173 
   174 val moreover = collect false;
   175 val ultimately = collect true;
   176 
   177 end;