New class "order" and accompanying changes.
authornipkow
Wed Feb 12 18:54:39 1997 +0100 (1997-02-12)
changeset 26094370e5f0fa3f
parent 2608 450c9b682a92
child 2610 655dc064a28c
New class "order" and accompanying changes.
src/HOL/Lex/AutoChopper.ML
src/HOL/Lex/Chopper.thy
src/HOL/ex/Puzzle.ML
     1.1 --- a/src/HOL/Lex/AutoChopper.ML	Wed Feb 12 18:53:59 1997 +0100
     1.2 +++ b/src/HOL/Lex/AutoChopper.ML	Wed Feb 12 18:54:39 1997 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4  goal AutoChopper.thy
     1.5  "! r erk l rst st ys yss zs::'a list. \
     1.6  \    acc xs st erk r (l,rst) A = (ys#yss, zs) --> \
     1.7 -\    ys@flat(yss)@zs = (if acc_prefix A st xs then r@xs else erk@flat(l)@rst)";
     1.8 +\    ys@concat(yss)@zs = (if acc_prefix A st xs then r@xs else erk@concat(l)@rst)";
     1.9  by (list.induct_tac "xs" 1);
    1.10   by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
    1.11  by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    1.12 @@ -133,7 +133,7 @@
    1.13   "! st erk r l rest ys yss zs. \
    1.14  \   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
    1.15  \     (if acc_prefix A st xs       \
    1.16 -\      then acc(flat(yss)@zs)(start A) [] [] ([],flat(yss)@zs) A = (yss,zs) \
    1.17 +\      then acc(concat(yss)@zs)(start A) [] [] ([],concat(yss)@zs) A = (yss,zs) \
    1.18  \      else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
    1.19  by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    1.20  by (list.induct_tac "xs" 1);
    1.21 @@ -151,7 +151,7 @@
    1.22   by (subgoal_tac "r@[a] ~= []" 2);
    1.23    by (Fast_tac 2);
    1.24   by (Simp_tac 2);
    1.25 -by (subgoal_tac "flat(yss) @ zs = list" 1);
    1.26 +by (subgoal_tac "concat(yss) @ zs = list" 1);
    1.27   by (hyp_subst_tac 1);
    1.28   by (atac 1);
    1.29  by (case_tac "yss = []" 1);
     2.1 --- a/src/HOL/Lex/Chopper.thy	Wed Feb 12 18:53:59 1997 +0100
     2.2 +++ b/src/HOL/Lex/Chopper.thy	Wed Feb 12 18:54:39 1997 +0100
     2.3 @@ -25,8 +25,8 @@
     2.4         (!zs. chopper(xs) = ([],zs) -->
     2.5               zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) &
     2.6         (!ys yss zs. chopper(xs) = (ys#yss,zs) -->
     2.7 -          ys ~= [] & L(ys) & xs=ys@flat(yss)@zs &
     2.8 -          chopper(flat(yss)@zs) = (yss,zs) &
     2.9 +          ys ~= [] & L(ys) & xs=ys@concat(yss)@zs &
    2.10 +          chopper(concat(yss)@zs) = (yss,zs) &
    2.11            (!as. as <= xs & ys <= as & ys ~= as --> ~L(as)))"
    2.12  
    2.13  end
     3.1 --- a/src/HOL/ex/Puzzle.ML	Wed Feb 12 18:53:59 1997 +0100
     3.2 +++ b/src/HOL/ex/Puzzle.ML	Wed Feb 12 18:54:39 1997 +0100
     3.3 @@ -23,7 +23,7 @@
     3.4  by (subgoal_tac "f(na) <= f(f(na))" 1);
     3.5  by (fast_tac (!claset addIs [Puzzle.f_ax]) 2);
     3.6  by (rtac lessD 1);
     3.7 -by (best_tac (!claset delrules [le_refl] 
     3.8 +by (fast_tac (!claset delrules [order_refl] 
     3.9                        addIs [Puzzle.f_ax, le_less_trans]) 1);
    3.10  val lemma = result() RS spec RS mp;
    3.11