author wenzelm Wed Sep 01 21:14:23 1999 +0200 (1999-09-01) changeset 7414 9bc7797d1249 parent 7413 e25ad9ab0b50 child 7415 bd819d0255e1
calculation: thm list;
filter differ;
```     1.1 --- a/src/Pure/Isar/calculation.ML	Wed Sep 01 21:13:12 1999 +0200
1.2 +++ b/src/Pure/Isar/calculation.ML	Wed Sep 01 21:14:23 1999 +0200
1.3 @@ -13,8 +13,8 @@
1.4    val trans_del_global: theory attribute
1.6    val trans_del_local: Proof.context attribute
1.7 -  val also: thm list option -> (thm -> unit) -> Proof.state -> Proof.state Seq.seq
1.8 -  val finally: thm list option -> (thm -> unit) -> Proof.state -> Proof.state Seq.seq
1.9 +  val also: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
1.10 +  val finally: thm list option -> (thm list -> unit) -> Proof.state -> Proof.state Seq.seq
1.11    val setup: (theory -> theory) list
1.12  end;
1.13
1.14 @@ -27,6 +27,7 @@
1.15  fun print_rules ths =
1.16    Pretty.writeln (Pretty.big_list "calculation rules:" (map Display.pretty_thm ths));
1.17
1.18 +
1.19  (* theory data kind 'Isar/calculation' *)
1.20
1.21  structure GlobalCalculationArgs =
1.22 @@ -50,7 +51,7 @@
1.23  structure LocalCalculationArgs =
1.24  struct
1.25    val name = "Isar/calculation";
1.26 -  type T = thm list * (thm * int) option;
1.27 +  type T = thm list * (thm list * int) option;
1.28
1.29    fun init thy = (GlobalCalculation.get thy, None);
1.30    fun print _ (ths, _) = print_rules ths;
1.31 @@ -66,10 +67,10 @@
1.32  fun get_calculation state =
1.33    (case #2 (LocalCalculation.get_st state) of
1.34      None => None
1.35 -  | Some (thm, lev) => if lev = Proof.level state then Some thm else None);
1.36 +  | Some (thms, lev) => if lev = Proof.level state then Some thms else None);
1.37
1.38 -fun put_calculation thm state =
1.39 -  LocalCalculation.put_st (get_local_rules state, Some (thm, Proof.level state)) state;
1.40 +fun put_calculation thms state =
1.41 +  LocalCalculation.put_st (get_local_rules state, Some (thms, Proof.level state)) state;
1.42
1.43  fun reset_calculation state =
1.44    LocalCalculation.put_st (get_local_rules state, None) state;
1.45 @@ -121,12 +122,18 @@
1.46  fun calculate final opt_rules print state =
1.47    let
1.48      fun err_if b msg = if b then raise Proof.STATE (msg, state) else ();
1.49 -    val fact = Proof.the_fact state;
1.50 +    val facts = Proof.the_facts state;
1.51      val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state);
1.52 +
1.53 +    fun differ thms thms' =
1.54 +      length thms <> length thms' orelse exists2 (not o Thm.eq_thm) (thms, thms');
1.55 +    fun combine thms =
1.56 +      Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules));
1.57 +
1.58      val (initial, calculations) =
1.59        (case get_calculation state of
1.60 -        None => (true, Seq.single fact)
1.61 -      | Some thm => (false, Seq.flat (Seq.map (Method.multi_resolve [thm, fact]) rules)));
1.62 +        None => (true, Seq.single facts)
1.63 +      | Some thms => (false, Seq.filter (differ thms) (combine thms)))
1.64    in
1.65      err_if (initial andalso final) "No calculation yet";
1.66      err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given";
1.67 @@ -136,12 +143,12 @@
1.68            state
1.69            |> reset_calculation
1.70            |> Proof.simple_have_thms calculationN []
1.71 -          |> Proof.simple_have_thms "" [calc]
1.72 +          |> Proof.simple_have_thms "" calc
1.73            |> Proof.chain
1.74          else
1.75            state
1.76            |> put_calculation calc
1.77 -          |> Proof.simple_have_thms calculationN [calc]
1.78 +          |> Proof.simple_have_thms calculationN calc
1.79            |> Proof.reset_facts)))
1.80    end;
1.81
```