src/Pure/Isar/calculation.ML
changeset 7414 9bc7797d1249
parent 7197 3ddf4a55d765
child 7475 dc4f8d6ee0d2
equal deleted inserted replaced
7413:e25ad9ab0b50 7414:9bc7797d1249
    11   val print_local_rules: Proof.context -> unit
    11   val print_local_rules: Proof.context -> unit
    12   val trans_add_global: theory attribute
    12   val trans_add_global: theory attribute
    13   val trans_del_global: theory attribute
    13   val trans_del_global: theory attribute
    14   val trans_add_local: Proof.context attribute
    14   val trans_add_local: Proof.context attribute
    15   val trans_del_local: Proof.context attribute
    15   val trans_del_local: Proof.context attribute
    16   val also: thm list option -> (thm -> unit) -> Proof.state -> Proof.state Seq.seq
    16   val also: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
    17   val finally: thm list option -> (thm -> unit) -> Proof.state -> Proof.state Seq.seq
    17   val finally: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
    18   val setup: (theory -> theory) list
    18   val setup: (theory -> theory) list
    19 end;
    19 end;
    20 
    20 
    21 structure Calculation: CALCULATION =
    21 structure Calculation: CALCULATION =
    22 struct
    22 struct
    24 
    24 
    25 (** global and local calculation data **)
    25 (** global and local calculation data **)
    26 
    26 
    27 fun print_rules ths =
    27 fun print_rules ths =
    28   Pretty.writeln (Pretty.big_list "calculation rules:" (map Display.pretty_thm ths));
    28   Pretty.writeln (Pretty.big_list "calculation rules:" (map Display.pretty_thm ths));
       
    29 
    29 
    30 
    30 (* theory data kind 'Isar/calculation' *)
    31 (* theory data kind 'Isar/calculation' *)
    31 
    32 
    32 structure GlobalCalculationArgs =
    33 structure GlobalCalculationArgs =
    33 struct
    34 struct
    48 (* proof data kind 'Isar/calculation' *)
    49 (* proof data kind 'Isar/calculation' *)
    49 
    50 
    50 structure LocalCalculationArgs =
    51 structure LocalCalculationArgs =
    51 struct
    52 struct
    52   val name = "Isar/calculation";
    53   val name = "Isar/calculation";
    53   type T = thm list * (thm * int) option;
    54   type T = thm list * (thm list * int) option;
    54 
    55 
    55   fun init thy = (GlobalCalculation.get thy, None);
    56   fun init thy = (GlobalCalculation.get thy, None);
    56   fun print _ (ths, _) = print_rules ths;
    57   fun print _ (ths, _) = print_rules ths;
    57 end;
    58 end;
    58 
    59 
    64 (* access calculation *)
    65 (* access calculation *)
    65 
    66 
    66 fun get_calculation state =
    67 fun get_calculation state =
    67   (case #2 (LocalCalculation.get_st state) of
    68   (case #2 (LocalCalculation.get_st state) of
    68     None => None
    69     None => None
    69   | Some (thm, lev) => if lev = Proof.level state then Some thm else None);
    70   | Some (thms, lev) => if lev = Proof.level state then Some thms else None);
    70 
    71 
    71 fun put_calculation thm state =
    72 fun put_calculation thms state =
    72   LocalCalculation.put_st (get_local_rules state, Some (thm, Proof.level state)) state;
    73   LocalCalculation.put_st (get_local_rules state, Some (thms, Proof.level state)) state;
    73 
    74 
    74 fun reset_calculation state =
    75 fun reset_calculation state =
    75   LocalCalculation.put_st (get_local_rules state, None) state;
    76   LocalCalculation.put_st (get_local_rules state, None) state;
    76 
    77 
    77 
    78 
   119 val calculationN = "calculation";
   120 val calculationN = "calculation";
   120 
   121 
   121 fun calculate final opt_rules print state =
   122 fun calculate final opt_rules print state =
   122   let
   123   let
   123     fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
   124     fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
   124     val fact = Proof.the_fact state;
   125     val facts = Proof.the_facts state;
   125     val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state);
   126     val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state);
       
   127 
       
   128     fun differ thms thms' =
       
   129       length thms <> length thms' orelse exists2 (not o Thm.eq_thm) (thms, thms');
       
   130     fun combine thms =
       
   131       Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules));
       
   132 
   126     val (initial, calculations) =
   133     val (initial, calculations) =
   127       (case get_calculation state of
   134       (case get_calculation state of
   128         None => (true, Seq.single fact)
   135         None => (true, Seq.single facts)
   129       | Some thm => (false, Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules)));
   136       | Some thms => (false, Seq.filter (differ thms) (combine thms)))
   130   in
   137   in
   131     err_if (initial andalso final) "No calculation yet";
   138     err_if (initial andalso final) "No calculation yet";
   132     err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
   139     err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
   133     calculations |> Seq.map (fn calc =>
   140     calculations |> Seq.map (fn calc =>
   134       (print calc;
   141       (print calc;
   135         (if final then
   142         (if final then
   136           state
   143           state
   137           |> reset_calculation
   144           |> reset_calculation
   138           |> Proof.simple_have_thms calculationN []
   145           |> Proof.simple_have_thms calculationN []
   139           |> Proof.simple_have_thms "" [calc]
   146           |> Proof.simple_have_thms "" calc
   140           |> Proof.chain
   147           |> Proof.chain
   141         else
   148         else
   142           state
   149           state
   143           |> put_calculation calc
   150           |> put_calculation calc
   144           |> Proof.simple_have_thms calculationN [calc]
   151           |> Proof.simple_have_thms calculationN calc
   145           |> Proof.reset_facts)))
   152           |> Proof.reset_facts)))
   146   end;
   153   end;
   147 
   154 
   148 fun also print = calculate false print;
   155 fun also print = calculate false print;
   149 fun finally print = calculate true print;
   156 fun finally print = calculate true print;