author haftmann Mon Oct 31 16:00:15 2005 +0100 (2005-10-31) changeset 18050 652c95961a8b parent 18049 156bba334c12 child 18051 dba086ed50cb
fold_index replacing foldln
 TFL/casesplit.ML file | annotate | diff | revisions src/HOL/Tools/split_rule.ML file | annotate | diff | revisions src/Pure/Isar/rule_cases.ML file | annotate | diff | revisions src/Pure/library.ML file | annotate | diff | revisions
```     1.1 --- a/TFL/casesplit.ML	Mon Oct 31 01:43:22 2005 +0100
1.2 +++ b/TFL/casesplit.ML	Mon Oct 31 16:00:15 2005 +0100
1.3 @@ -336,31 +336,24 @@
1.4
1.5  (* derive eqs, assuming strict, ie the rules have no assumptions = all
1.6     the well-foundness conditions have been solved. *)
1.7 -local
1.8 -  fun get_related_thms i =
1.9 -      List.mapPartial ((fn (r,x) => if x = i then SOME r else NONE));
1.10 -
1.11 -  fun solve_eq (th, [], i) =
1.12 -      raise ERROR_MESSAGE "derive_init_eqs: missing rules"
1.13 -    | solve_eq (th, [a], i) = (a, i)
1.14 -    | solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th,i);
1.15 -in
1.16  fun derive_init_eqs sgn rules eqs =
1.17 -    let
1.18 -      val eqths = map (Thm.trivial o (Thm.cterm_of sgn) o Data.mk_Trueprop)
1.19 -                      eqs
1.20 -    in
1.21 -      (rev o map solve_eq)
1.22 -        (Library.foldln
1.23 -           (fn (e,i) =>
1.24 -               (curry (op ::)) (e, (get_related_thms (i - 1) rules), i - 1))
1.25 -           eqths [])
1.26 -    end;
1.27 -end;
1.28 -(*
1.29 -    val (rs_hwfc, unhidefs) = Library.split_list (map hide_prems rules)
1.30 -    (map2 (op |>) (ths, expfs))
1.31 -*)
1.32 +  let
1.33 +    fun get_related_thms i =
1.34 +      List.mapPartial ((fn (r, x) => if x = i then SOME r else NONE));
1.35 +    fun add_eq (i, e) xs =
1.36 +      (e, (get_related_thms i rules), i) :: xs
1.37 +    fun solve_eq (th, [], i) =
1.38 +          raise ERROR_MESSAGE "derive_init_eqs: missing rules"
1.39 +      | solve_eq (th, [a], i) = (a, i)
1.40 +      | solve_eq (th, splitths as (_ :: _), i) = (splitto splitths th, i);
1.41 +    val eqths =
1.42 +      map (Thm.trivial o Thm.cterm_of sgn o Data.mk_Trueprop) eqs;
1.43 +  in
1.44 +    []
1.45 +    |> fold_index add_eq eqths
1.46 +    |> map solve_eq
1.47 +    |> rev
1.48 +  end;
1.49
1.50  end;
1.51
```
```     2.1 --- a/src/HOL/Tools/split_rule.ML	Mon Oct 31 01:43:22 2005 +0100
2.2 +++ b/src/HOL/Tools/split_rule.ML	Mon Oct 31 16:00:15 2005 +0100
2.3 @@ -120,14 +120,16 @@
2.4
2.5  fun split_rule_goal xss rl =
2.6    let
2.7 -    fun one_split i (th, s) = Tactic.rule_by_tactic (pair_tac s i) th;
2.8 -    fun one_goal (xs, i) th = Library.foldl (one_split i) (th, xs);
2.9 +    fun one_split i s = Tactic.rule_by_tactic (pair_tac s i);
2.10 +    fun one_goal (i, xs) = fold (one_split (i+1)) xs;
2.11    in
2.12 -    Drule.standard (Simplifier.full_simplify split_rule_ss (Library.foldln one_goal xss rl))
2.13 +    rl
2.14 +    |> Library.fold_index one_goal xss
2.15 +    |> Simplifier.full_simplify split_rule_ss
2.16 +    |> Drule.standard
2.17      |> RuleCases.save rl
2.18    end;
2.19
2.20 -
2.21  (* attribute syntax *)
2.22
2.23  (* FIXME dynamically scoped due to Args.name/pair_tac *)
```
```     3.1 --- a/src/Pure/Isar/rule_cases.ML	Mon Oct 31 01:43:22 2005 +0100
3.2 +++ b/src/Pure/Isar/rule_cases.ML	Mon Oct 31 16:00:15 2005 +0100
3.3 @@ -142,7 +142,9 @@
3.4
3.5  (* params *)
3.6
3.7 -fun rename_params xss thm = foldln Thm.rename_params_rule xss thm
3.8 +fun rename_params xss thm =
3.9 +  thm
3.10 +  |> fold_index (fn (i, xs) => Thm.rename_params_rule (xs, i+1)) xss
3.11    |> save thm;
3.12
3.13  fun params xss = Drule.rule_attribute (K (rename_params xss));
```
```     4.1 --- a/src/Pure/library.ML	Mon Oct 31 01:43:22 2005 +0100
4.2 +++ b/src/Pure/library.ML	Mon Oct 31 16:00:15 2005 +0100
4.3 @@ -99,7 +99,7 @@
4.4    val fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
4.5    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
4.6    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
4.7 -  val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
4.8 +  val fold_index: (int * 'a -> 'b -> 'b) -> 'a list -> 'b -> 'b
4.9    val unflat: 'a list list -> 'b list -> 'b list list
4.10    val splitAt: int * 'a list -> 'a list * 'a list
4.11    val dropwhile: ('a -> bool) -> 'a list -> 'a list
4.12 @@ -504,7 +504,11 @@
4.13          | itr (x::l) = f(x, itr l)
4.14    in  itr l  end;
4.15
4.16 -fun foldln f xs e = fst (foldl (fn ((e,i), x) => (f (x,i) e, i+1)) ((e,1),xs));
4.17 +fun fold_index f =
4.18 +  let
4.19 +    fun fold_aux _  [] y = y
4.20 +      | fold_aux i (x :: xs) y = fold_aux (i+1) xs (f (i, x) y);
4.21 +  in fold_aux 0 end;
4.22
4.23  fun foldl_map f =
4.24    let
```