Arith: less_diff_conv
authornipkow
Fri Sep 04 11:01:59 1998 +0200 (1998-09-04)
changeset 542726c9a7c0b36b
parent 5426 566f47250bd0
child 5428 5a6c4f666a25
Arith: less_diff_conv
List: [i..j]
src/HOL/Arith.ML
src/HOL/List.ML
src/HOL/List.thy
     1.1 --- a/src/HOL/Arith.ML	Thu Sep 03 16:40:02 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri Sep 04 11:01:59 1998 +0200
     1.3 @@ -613,6 +613,17 @@
     1.4  by (Asm_full_simp_tac 1);
     1.5  qed "add_less_imp_less_diff";
     1.6  
     1.7 +Goal "(i < j-k) = (i+k < (j::nat))";
     1.8 +br iffI 1;
     1.9 + by(case_tac "k <= j" 1);
    1.10 +  bd le_add_diff_inverse2 1;
    1.11 +  by(dres_inst_tac [("k","k")] add_less_mono1 1);
    1.12 +  by(Asm_full_simp_tac 1);
    1.13 + by(rotate_tac 1 1);
    1.14 + by(asm_full_simp_tac (simpset() addSolver cut_trans_tac) 1);
    1.15 +be add_less_imp_less_diff 1;
    1.16 +qed "less_diff_conv";
    1.17 +
    1.18  Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
    1.19  by (asm_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);
    1.20  qed "Suc_diff_Suc";
     2.1 --- a/src/HOL/List.ML	Thu Sep 03 16:40:02 1998 +0200
     2.2 +++ b/src/HOL/List.ML	Fri Sep 04 11:01:59 1998 +0200
     2.3 @@ -246,6 +246,63 @@
     2.4  qed "append_eq_appendI";
     2.5  
     2.6  
     2.7 +(***
     2.8 +Simplification procedure for all list equalities.
     2.9 +Currently only tries to rearranges @ to see if
    2.10 +- both lists end in a singleton list,
    2.11 +- or both lists end in the same list.
    2.12 +***)
    2.13 +local
    2.14 +
    2.15 +val list_eq_pattern =
    2.16 +  read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
    2.17 +
    2.18 +fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
    2.19 +      (case xs of Const("List.list.[]",_) => cons | _ => last xs)
    2.20 +  | last (Const("List.op @",_) $ _ $ ys) = last ys
    2.21 +  | last t = t;
    2.22 +
    2.23 +fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
    2.24 +  | list1 _ = false;
    2.25 +
    2.26 +fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
    2.27 +      (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
    2.28 +  | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
    2.29 +  | butlast xs = Const("List.list.[]",fastype_of xs);
    2.30 +
    2.31 +val rearr_tac =
    2.32 +  simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
    2.33 +
    2.34 +fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
    2.35 +  let
    2.36 +    val lastl = last lhs and lastr = last rhs
    2.37 +    fun rearr conv =
    2.38 +      let val lhs1 = butlast lhs and rhs1 = butlast rhs
    2.39 +          val Type(_,listT::_) = eqT
    2.40 +          val appT = [listT,listT] ---> listT
    2.41 +          val app = Const("List.op @",appT)
    2.42 +          val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
    2.43 +          val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
    2.44 +          val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
    2.45 +            handle ERROR =>
    2.46 +            error("The error(s) above occurred while trying to prove " ^
    2.47 +                  string_of_cterm ct)
    2.48 +      in Some((conv RS (thm RS trans)) RS eq_reflection) end
    2.49 +
    2.50 +  in if list1 lastl andalso list1 lastr
    2.51 +     then rearr append1_eq_conv
    2.52 +     else
    2.53 +     if lastl aconv lastr
    2.54 +     then rearr append_same_eq
    2.55 +     else None
    2.56 +  end;
    2.57 +in
    2.58 +val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq;
    2.59 +end;
    2.60 +
    2.61 +Addsimprocs [list_eq_simproc];
    2.62 +
    2.63 +
    2.64  (** map **)
    2.65  
    2.66  section "map";
    2.67 @@ -827,27 +884,59 @@
    2.68  
    2.69  (** upto **)
    2.70  
    2.71 -Goal "!i j. ~ j < i --> j - i < Suc j - i";
    2.72 -by(strip_tac 1);
    2.73 -br diff_less_Suc_diff 1;
    2.74 -be leI 1;
    2.75 -val lemma = result();
    2.76 +(* Does not terminate! *)
    2.77 +Goal "[i..j(] = (if i<j then i#[Suc i..j(] else [])";
    2.78 +by(induct_tac "j" 1);
    2.79 +by Auto_tac;
    2.80 +by(REPEAT(trans_tac 1));
    2.81 +qed "upt_rec";
    2.82  
    2.83 -Goalw [upto_def] "j<i ==> [i..j] = []";
    2.84 +Goal "j<=i ==> [i..j(] = []";
    2.85 +by(stac upt_rec 1);
    2.86 +by(asm_simp_tac (simpset() addSolver cut_trans_tac) 1);
    2.87 +qed "upt_conv_Nil";
    2.88 +Addsimps [upt_conv_Nil];
    2.89 +
    2.90 +Goal "i<=j ==> [i..(Suc j)(] = [i..j(]@[j]";
    2.91 +by (Asm_simp_tac 1);
    2.92 +qed "upt_Suc";
    2.93 +
    2.94 +Goal "i<j ==> [i..j(] = i#[Suc i..j(]";
    2.95  br trans 1;
    2.96 -brs paired_upto.rules 1;
    2.97 -br lemma 1;
    2.98 -by(Asm_simp_tac 1);
    2.99 -qed "upto_conv_Nil";
   2.100 +by(stac upt_rec 1);
   2.101 +br refl 2;
   2.102 +by (Asm_simp_tac 1);
   2.103 +qed "upt_conv_Cons";
   2.104 +
   2.105 +Goal "length [i..j(] = j-i";
   2.106 +by(induct_tac "j" 1);
   2.107 + by (Simp_tac 1);
   2.108 +by(asm_simp_tac (simpset() addsimps [Suc_diff_le] addSolver cut_trans_tac) 1);
   2.109 +qed "length_upt";
   2.110 +Addsimps [length_upt];
   2.111  
   2.112 -Goalw [upto_def] "i<=j ==> [i..j] = i#[Suc i..j]";
   2.113 -br trans 1;
   2.114 -brs paired_upto.rules 1;
   2.115 -br lemma 1;
   2.116 -by(asm_simp_tac (simpset() addsimps [leD]) 1);
   2.117 -qed "upto_conv_Cons";
   2.118 +Goal "i+k < j --> [i..j(] ! k = i+k";
   2.119 +by(induct_tac "j" 1);
   2.120 + by(Simp_tac 1);
   2.121 +by(asm_simp_tac (simpset() addsimps ([nth_append,less_diff_conv]@add_ac)
   2.122 +                           addSolver cut_trans_tac) 1);
   2.123 +br conjI 1;
   2.124 + by(Clarify_tac 1);
   2.125 + bd add_lessD1 1;
   2.126 + by(trans_tac 1);
   2.127 +by(Clarify_tac 1);
   2.128 +br conjI 1;
   2.129 + by(Clarify_tac 1);
   2.130 + by(subgoal_tac "n=i+k" 1);
   2.131 +  by(Asm_full_simp_tac 1);
   2.132 + by(trans_tac 1);
   2.133 +by(Clarify_tac 1);
   2.134 +by(subgoal_tac "n=i+k" 1);
   2.135 + by(Asm_full_simp_tac 1);
   2.136 +by(trans_tac 1);
   2.137 +qed_spec_mp "nth_upt";
   2.138 +Addsimps [nth_upt];
   2.139  
   2.140 -Addsimps [upto_conv_Nil,upto_conv_Cons];
   2.141  
   2.142  (** nodups & remdups **)
   2.143  section "nodups & remdups";
   2.144 @@ -973,60 +1062,3 @@
   2.145  by (Blast_tac 1);
   2.146  qed "Cons_in_lex";
   2.147  AddIffs [Cons_in_lex];
   2.148 -
   2.149 -
   2.150 -(***
   2.151 -Simplification procedure for all list equalities.
   2.152 -Currently only tries to rearranges @ to see if
   2.153 -- both lists end in a singleton list,
   2.154 -- or both lists end in the same list.
   2.155 -***)
   2.156 -local
   2.157 -
   2.158 -val list_eq_pattern =
   2.159 -  read_cterm (sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
   2.160 -
   2.161 -fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
   2.162 -      (case xs of Const("List.list.[]",_) => cons | _ => last xs)
   2.163 -  | last (Const("List.op @",_) $ _ $ ys) = last ys
   2.164 -  | last t = t;
   2.165 -
   2.166 -fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
   2.167 -  | list1 _ = false;
   2.168 -
   2.169 -fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
   2.170 -      (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
   2.171 -  | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
   2.172 -  | butlast xs = Const("List.list.[]",fastype_of xs);
   2.173 -
   2.174 -val rearr_tac =
   2.175 -  simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
   2.176 -
   2.177 -fun list_eq sg _ (F as (eq as Const(_,eqT)) $ lhs $ rhs) =
   2.178 -  let
   2.179 -    val lastl = last lhs and lastr = last rhs
   2.180 -    fun rearr conv =
   2.181 -      let val lhs1 = butlast lhs and rhs1 = butlast rhs
   2.182 -          val Type(_,listT::_) = eqT
   2.183 -          val appT = [listT,listT] ---> listT
   2.184 -          val app = Const("List.op @",appT)
   2.185 -          val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
   2.186 -          val ct = cterm_of sg (HOLogic.mk_Trueprop(HOLogic.mk_eq(F,F2)))
   2.187 -          val thm = prove_goalw_cterm [] ct (K [rearr_tac 1])
   2.188 -            handle ERROR =>
   2.189 -            error("The error(s) above occurred while trying to prove " ^
   2.190 -                  string_of_cterm ct)
   2.191 -      in Some((conv RS (thm RS trans)) RS eq_reflection) end
   2.192 -
   2.193 -  in if list1 lastl andalso list1 lastr
   2.194 -     then rearr append1_eq_conv
   2.195 -     else
   2.196 -     if lastl aconv lastr
   2.197 -     then rearr append_same_eq
   2.198 -     else None
   2.199 -  end;
   2.200 -in
   2.201 -val list_eq_simproc = mk_simproc "list_eq" [list_eq_pattern] list_eq;
   2.202 -end;
   2.203 -
   2.204 -Addsimprocs [list_eq_simproc];
     3.1 --- a/src/HOL/List.thy	Thu Sep 03 16:40:02 1998 +0200
     3.2 +++ b/src/HOL/List.thy	Fri Sep 04 11:01:59 1998 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  The datatype of finite lists.
     3.5  *)
     3.6  
     3.7 -List = Datatype + Recdef +
     3.8 +List = Datatype + WF_Rel +
     3.9  
    3.10  datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
    3.11  
    3.12 @@ -28,8 +28,7 @@
    3.13    tl, butlast :: 'a list => 'a list
    3.14    rev         :: 'a list => 'a list
    3.15    zip	      :: "'a list => 'b list => ('a * 'b) list"
    3.16 -  upto        :: nat => nat => nat list                   ("(1[_../_])")
    3.17 -  paired_upto :: "nat * nat => nat list"
    3.18 +  upt         :: nat => nat => nat list                   ("(1[_../_'(])")
    3.19    remdups     :: 'a list => 'a list
    3.20    nodups      :: "'a list => bool"
    3.21    replicate   :: nat => 'a => 'a list
    3.22 @@ -50,6 +49,8 @@
    3.23    "_lupdbinds"     :: [lupdbind, lupdbinds] => lupdbinds ("_,/ _")
    3.24    "_LUpdate"       :: ['a, lupdbinds] => 'a           ("_/[(_)]" [900,0] 900)
    3.25  
    3.26 +  upto        :: nat => nat => nat list                   ("(1[_../_])")
    3.27 +
    3.28  translations
    3.29    "[x, xs]"     == "x#[xs]"
    3.30    "[x]"         == "x#[]"
    3.31 @@ -58,6 +59,9 @@
    3.32    "_LUpdate xs (_lupdbinds b bs)"  == "_LUpdate (_LUpdate xs b) bs"
    3.33    "xs[i:=x]"                       == "list_update xs i x"
    3.34  
    3.35 +  "[i..j]" == "[i..(Suc j)(]"
    3.36 +
    3.37 +
    3.38  syntax (symbols)
    3.39    "@filter"   :: [pttrn, 'a list, bool] => 'a list        ("(1[_\\<in>_ ./ _])")
    3.40  
    3.41 @@ -137,9 +141,9 @@
    3.42  primrec
    3.43    "zip xs []     = []"
    3.44    "zip xs (y#ys) = (hd xs,y)#zip (tl xs) ys"
    3.45 -recdef paired_upto "measure(%(i,j). (Suc j)-i)"
    3.46 -  "paired_upto(i,j) = (if j<i then [] else i#paired_upto(Suc i,j))"
    3.47 -defs upto_def  "[i..j] == paired_upto(i,j)"
    3.48 +primrec
    3.49 +  "[i..0(] = []"
    3.50 +  "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
    3.51  primrec
    3.52    "nodups []     = True"
    3.53    "nodups (x#xs) = (x ~: set xs & nodups xs)"