--- a/src/HOL/Arith.ML Thu Sep 03 16:40:02 1998 +0200
+++ b/src/HOL/Arith.ML Fri Sep 04 11:01:59 1998 +0200
@@ -613,6 +613,17 @@
by (Asm_full_simp_tac 1);
qed "add_less_imp_less_diff";
+Goal "(i < j-k) = (i+k < (j::nat))";
+br iffI 1;
+ by(case_tac "k <= j" 1);
+ bd le_add_diff_inverse2 1;
+ by(dres_inst_tac [("k","k")] add_less_mono1 1);
+ by(Asm_full_simp_tac 1);
+ by(rotate_tac 1 1);
+ by(asm_full_simp_tac (simpset() addSolver cut_trans_tac) 1);
+be add_less_imp_less_diff 1;
+qed "less_diff_conv";
+
Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
by (asm_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);
qed "Suc_diff_Suc";
--- a/src/HOL/List.ML Thu Sep 03 16:40:02 1998 +0200
+++ b/src/HOL/List.ML Fri Sep 04 11:01:59 1998 +0200
@@ -246,6 +246,63 @@
qed "append_eq_appendI";
+(***
+Simplification procedure for all list equalities.
+Currently only tries to rearranges @ to see if
+- both lists end in a singleton list,
+- or both lists end in the same list.
+***)
+local
+
+val list_eq_pattern =
+ read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
+
+fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
+ (case xs of Const("List.list.[]",_) => cons | _ => last xs)
+ | last (Const("List.op @",_) $ _ $ ys) = last ys
+ | last t = t;
+
+fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
+ | list1 _ = false;
+
+fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
+ (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
+ | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
+ | butlast xs = Const("List.list.[]",fastype_of xs);
+
+val rearr_tac =
+ simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
+
+fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
+ let
+ val lastl = last lhs and lastr = last rhs
+ fun rearr conv =
+ let val lhs1 = butlast lhs and rhs1 = butlast rhs
+ val Type(_,listT::_) = eqT
+ val appT = [listT,listT] ---> listT
+ val app = Const("List.op @",appT)
+ val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
+ val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
+ val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
+ handle ERROR =>
+ error("The error(s) above occurred while trying to prove " ^
+ string_of_cterm ct)
+ in Some((conv RS (thm RS trans)) RS eq_reflection) end
+
+ in if list1 lastl andalso list1 lastr
+ then rearr append1_eq_conv
+ else
+ if lastl aconv lastr
+ then rearr append_same_eq
+ else None
+ end;
+in
+val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq;
+end;
+
+Addsimprocs [list_eq_simproc];
+
+
(** map **)
section "map";
@@ -827,27 +884,59 @@
(** upto **)
-Goal "!i j. ~ j < i --> j - i < Suc j - i";
-by(strip_tac 1);
-br diff_less_Suc_diff 1;
-be leI 1;
-val lemma = result();
+(* Does not terminate! *)
+Goal "[i..j(] = (if i<j then i#[Suc i..j(] else [])";
+by(induct_tac "j" 1);
+by Auto_tac;
+by(REPEAT(trans_tac 1));
+qed "upt_rec";
-Goalw [upto_def] "j<i ==> [i..j] = []";
+Goal "j<=i ==> [i..j(] = []";
+by(stac upt_rec 1);
+by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
+qed "upt_conv_Nil";
+Addsimps [upt_conv_Nil];
+
+Goal "i<=j ==> [i..(Suc j)(] = [i..j(]@[j]";
+by (Asm_simp_tac 1);
+qed "upt_Suc";
+
+Goal "i<j ==> [i..j(] = i#[Suc i..j(]";
br trans 1;
-brs paired_upto.rules 1;
-br lemma 1;
-by(Asm_simp_tac 1);
-qed "upto_conv_Nil";
+by(stac upt_rec 1);
+br refl 2;
+by (Asm_simp_tac 1);
+qed "upt_conv_Cons";
+
+Goal "length [i..j(] = j-i";
+by(induct_tac "j" 1);
+ by (Simp_tac 1);
+by(asm_simp_tac (simpset() addsimps [Suc_diff_le] addSolver cut_trans_tac) 1);
+qed "length_upt";
+Addsimps [length_upt];
-Goalw [upto_def] "i<=j ==> [i..j] = i#[Suc i..j]";
-br trans 1;
-brs paired_upto.rules 1;
-br lemma 1;
-by(asm_simp_tac (simpset() addsimps [leD]) 1);
-qed "upto_conv_Cons";
+Goal "i+k < j --> [i..j(] ! k = i+k";
+by(induct_tac "j" 1);
+ by(Simp_tac 1);
+by(asm_simp_tac (simpset() addsimps ([nth_append,less_diff_conv]@add_ac)
+ addSolver cut_trans_tac) 1);
+br conjI 1;
+ by(Clarify_tac 1);
+ bd add_lessD1 1;
+ by(trans_tac 1);
+by(Clarify_tac 1);
+br conjI 1;
+ by(Clarify_tac 1);
+ by(subgoal_tac "n=i+k" 1);
+ by(Asm_full_simp_tac 1);
+ by(trans_tac 1);
+by(Clarify_tac 1);
+by(subgoal_tac "n=i+k" 1);
+ by(Asm_full_simp_tac 1);
+by(trans_tac 1);
+qed_spec_mp "nth_upt";
+Addsimps [nth_upt];
-Addsimps [upto_conv_Nil,upto_conv_Cons];
(** nodups & remdups **)
section "nodups & remdups";
@@ -973,60 +1062,3 @@
by (Blast_tac 1);
qed "Cons_in_lex";
AddIffs [Cons_in_lex];
-
-
-(***
-Simplification procedure for all list equalities.
-Currently only tries to rearranges @ to see if
-- both lists end in a singleton list,
-- or both lists end in the same list.
-***)
-local
-
-val list_eq_pattern =
- read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
-
-fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
- (case xs of Const("List.list.[]",_) => cons | _ => last xs)
- | last (Const("List.op @",_) $ _ $ ys) = last ys
- | last t = t;
-
-fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
- | list1 _ = false;
-
-fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
- (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
- | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
- | butlast xs = Const("List.list.[]",fastype_of xs);
-
-val rearr_tac =
- simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
-
-fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
- let
- val lastl = last lhs and lastr = last rhs
- fun rearr conv =
- let val lhs1 = butlast lhs and rhs1 = butlast rhs
- val Type(_,listT::_) = eqT
- val appT = [listT,listT] ---> listT
- val app = Const("List.op @",appT)
- val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
- val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
- val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
- handle ERROR =>
- error("The error(s) above occurred while trying to prove " ^
- string_of_cterm ct)
- in Some((conv RS (thm RS trans)) RS eq_reflection) end
-
- in if list1 lastl andalso list1 lastr
- then rearr append1_eq_conv
- else
- if lastl aconv lastr
- then rearr append_same_eq
- else None
- end;
-in
-val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq;
-end;
-
-Addsimprocs [list_eq_simproc];
--- a/src/HOL/List.thy Thu Sep 03 16:40:02 1998 +0200
+++ b/src/HOL/List.thy Fri Sep 04 11:01:59 1998 +0200
@@ -6,7 +6,7 @@
The datatype of finite lists.
*)
-List = Datatype + Recdef +
+List = Datatype + WF_Rel +
datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
@@ -28,8 +28,7 @@
tl, butlast :: 'a list => 'a list
rev :: 'a list => 'a list
zip :: "'a list => 'b list => ('a * 'b) list"
- upto :: nat => nat => nat list ("(1[_../_])")
- paired_upto :: "nat * nat => nat list"
+ upt :: nat => nat => nat list ("(1[_../_'(])")
remdups :: 'a list => 'a list
nodups :: "'a list => bool"
replicate :: nat => 'a => 'a list
@@ -50,6 +49,8 @@
"_lupdbinds" :: [lupdbind, lupdbinds] => lupdbinds ("_,/ _")
"_LUpdate" :: ['a, lupdbinds] => 'a ("_/[(_)]" [900,0] 900)
+ upto :: nat => nat => nat list ("(1[_../_])")
+
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
@@ -58,6 +59,9 @@
"_LUpdate xs (_lupdbinds b bs)" == "_LUpdate (_LUpdate xs b) bs"
"xs[i:=x]" == "list_update xs i x"
+ "[i..j]" == "[i..(Suc j)(]"
+
+
syntax (symbols)
"@filter" :: [pttrn, 'a list, bool] => 'a list ("(1[_\\<in>_ ./ _])")
@@ -137,9 +141,9 @@
primrec
"zip xs [] = []"
"zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys"
-recdef paired_upto "measure(%(i,j). (Suc j)-i)"
- "paired_upto(i,j) = (if j<i then [] else i#paired_upto(Suc i,j))"
-defs upto_def "[i..j] == paired_upto(i,j)"
+primrec
+ "[i..0(] = []"
+ "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
primrec
"nodups [] = True"
"nodups (x#xs) = (x ~: set xs & nodups xs)"