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;
     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: Context.generic -> unit
    11   val get_calculation: Proof.state -> thm list option
    12   val trans_add: Context.generic attribute
    13   val trans_del: Context.generic attribute
    14   val sym_add: Context.generic attribute
    15   val sym_del: Context.generic attribute
    16   val symmetric: Context.generic 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 -> Proof.state -> Proof.state Seq.seq
    20   val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
    21   val moreover: bool -> Proof.state -> Proof.state
    22   val ultimately: bool -> Proof.state -> Proof.state
    23 end;
    24 
    25 structure Calculation: CALCULATION =
    26 struct
    27 
    28 (** calculation data **)
    29 
    30 structure CalculationData = GenericDataFun
    31 (
    32   val name = "Isar/calculation";
    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   fun print generic ((trans, sym), _) =
    41     let val ctxt = Context.proof_of generic in
    42       [Pretty.big_list "transitivity rules:"
    43           (map (ProofContext.pretty_thm ctxt) (NetRules.rules trans)),
    44         Pretty.big_list "symmetry rules:" (map (ProofContext.pretty_thm ctxt) sym)]
    45       |> Pretty.chunks |> Pretty.writeln
    46     end;
    47 );
    48 
    49 val _ = Context.add_setup CalculationData.init;
    50 val print_rules = CalculationData.print;
    51 
    52 
    53 (* access calculation *)
    54 
    55 fun get_calculation state =
    56   (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of
    57     NONE => NONE
    58   | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE);
    59 
    60 val calculationN = "calculation";
    61 
    62 fun put_calculation calc =
    63   `Proof.level #-> (fn lev =>
    64     Proof.map_context (Context.the_proof o
    65         CalculationData.map (apsnd (K (Option.map (rpair lev) calc))) o Context.Proof))
    66   #> Proof.put_thms (calculationN, calc);
    67 
    68 
    69 
    70 (** attributes **)
    71 
    72 (* add/del rules *)
    73 
    74 val trans_add = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.insert);
    75 val trans_del = Attrib.declaration (CalculationData.map o apfst o apfst o NetRules.delete);
    76 
    77 val sym_add =
    78   Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.add_rule)
    79   #> ContextRules.elim_query NONE;
    80 val sym_del =
    81   Attrib.declaration (CalculationData.map o apfst o apsnd o Drule.del_rule)
    82   #> ContextRules.rule_del;
    83 
    84 
    85 (* symmetric *)
    86 
    87 val symmetric = Attrib.rule (fn x => fn th =>
    88   (case Seq.chop (2, Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
    89     ([th'], _) => th'
    90   | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
    91   | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));
    92 
    93 
    94 (* concrete syntax *)
    95 
    96 val trans_att = Attrib.add_del_args trans_add trans_del;
    97 val sym_att = Attrib.add_del_args sym_add sym_del;
    98 
    99 val _ = Context.add_setup
   100  (Attrib.add_attributes
   101    [("trans", Attrib.common trans_att, "declaration of transitivity rule"),
   102     ("sym", Attrib.common sym_att, "declaration of symmetry rule"),
   103     ("symmetric", Attrib.common (Attrib.no_args symmetric), "resolution with symmetry rule")] #>
   104   PureThy.add_thms
   105    [(("", transitive_thm), [Attrib.theory trans_add]),
   106     (("", symmetric_thm), [Attrib.theory sym_add])] #> snd);
   107 
   108 
   109 
   110 (** proof commands **)
   111 
   112 fun err_if b msg = if b then error msg else ();
   113 
   114 fun assert_sane final =
   115   if final then Proof.assert_forward else Proof.assert_forward_or_chain;
   116 
   117 fun maintain_calculation false calc = put_calculation (SOME calc)
   118   | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc;
   119 
   120 fun print_calculation false _ _ = ()
   121   | print_calculation true ctxt calc =
   122       Pretty.writeln (ProofContext.pretty_fact ctxt (calculationN, calc));
   123 
   124 
   125 (* also and finally *)
   126 
   127 val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of;
   128 
   129 fun calculate prep_rules final raw_rules int state =
   130   let
   131     val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
   132     val eq_prop = op aconv o pairself (Pattern.eta_contract o strip_assums_concl);
   133     fun projection ths th = Library.exists (Library.curry eq_prop th) ths;
   134 
   135     val opt_rules = Option.map (prep_rules state) raw_rules;
   136     fun combine ths =
   137       (case opt_rules of SOME rules => rules
   138       | NONE =>
   139           (case ths of [] => NetRules.rules (#1 (get_rules state))
   140           | th :: _ => NetRules.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
   141       |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
   142       |> Seq.filter (not o projection ths);
   143 
   144     val facts = Proof.the_facts (assert_sane final state);
   145     val (initial, calculations) =
   146       (case get_calculation state of
   147         NONE => (true, Seq.single facts)
   148       | SOME calc => (false, Seq.map single (combine (calc @ facts))));
   149   in
   150     err_if (initial andalso final) "No calculation yet";
   151     err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
   152     calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc;
   153         state |> maintain_calculation final calc))
   154   end;
   155 
   156 val also = calculate Proof.get_thmss false;
   157 val also_i = calculate (K I) false;
   158 val finally = calculate Proof.get_thmss true;
   159 val finally_i = calculate (K I) 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   in
   173     err_if (initial andalso final) "No calculation yet";
   174     print_calculation int (Proof.context_of state) calc;
   175     state |> maintain_calculation final calc
   176   end;
   177 
   178 val moreover = collect false;
   179 val ultimately = collect true;
   180 
   181 end;