src/HOL/Lex/MaxChop.ML
author paulson
Thu Feb 19 18:24:08 2004 +0100 (2004-02-19)
changeset 14401 477380c74c1d
parent 10338 291ce4c4b50e
permissions -rw-r--r--
removal of the legacy ML structure List
nipkow@4714
     1
(*  Title:      HOL/Lex/MaxChop.ML
nipkow@4714
     2
    ID:         $Id$
nipkow@4714
     3
    Author:     Tobias Nipkow
nipkow@4714
     4
    Copyright   1998 TUM
nipkow@4714
     5
*)
nipkow@4714
     6
nipkow@4714
     7
(* Termination of chop *)
nipkow@4714
     8
wenzelm@5069
     9
Goalw [reducing_def] "reducing(%qs. maxsplit P ([],qs) [] qs)";
wenzelm@5132
    10
by (asm_full_simp_tac (simpset() addsimps [maxsplit_eq]) 1);
nipkow@4714
    11
qed "reducing_maxsplit";
nipkow@4714
    12
nipkow@4714
    13
val [tc] = chopr.tcs;
nipkow@4714
    14
goalw_cterm [reducing_def] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
wenzelm@5132
    15
by (blast_tac (claset() addDs [sym]) 1);
nipkow@4714
    16
val lemma = result();
nipkow@4714
    17
nipkow@8624
    18
val chopr_rule = let val [chopr_rule] = chopr.simps in lemma RS chopr_rule end;
nipkow@4714
    19
nipkow@5118
    20
Goalw [chop_def] "reducing splitf ==> \
nipkow@4714
    21
\ chop splitf xs = (let (pre,post) = splitf xs \
nipkow@4714
    22
\                   in if pre=[] then ([],xs) \
nipkow@4714
    23
\                      else let (xss,zs) = chop splitf post \
nipkow@4714
    24
\                             in (pre#xss,zs))";
paulson@6918
    25
by (asm_simp_tac (simpset() addsimps [chopr_rule]) 1);
wenzelm@5132
    26
by (simp_tac (simpset() addsimps [Let_def] addsplits [split_split]) 1);
nipkow@4714
    27
qed "chop_rule";
nipkow@4714
    28
wenzelm@5069
    29
Goalw [is_maxsplitter_def,reducing_def]
nipkow@5118
    30
 "is_maxsplitter P splitf ==> reducing splitf";
wenzelm@5132
    31
by (Asm_full_simp_tac 1);
nipkow@4714
    32
qed "is_maxsplitter_reducing";
nipkow@4714
    33
nipkow@5118
    34
Goal "is_maxsplitter P splitf ==> \
nipkow@4714
    35
\ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs";
nipkow@9747
    36
by (induct_thm_tac length_induct "xs" 1);
wenzelm@5132
    37
by (asm_simp_tac (simpset() delsplits [split_if]
paulson@6918
    38
                           addsimps [chop_rule,is_maxsplitter_reducing]) 1);
wenzelm@5132
    39
by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
nipkow@4832
    40
                                addsplits [split_split]) 1);
nipkow@4714
    41
qed_spec_mp "chop_concat";
nipkow@4714
    42
nipkow@5118
    43
Goal "is_maxsplitter P splitf ==> \
nipkow@4714
    44
\ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])";
nipkow@9747
    45
by (induct_thm_tac length_induct "xs" 1);
paulson@6918
    46
by (asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]) 1);
wenzelm@5132
    47
by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
paulson@6918
    48
                                 addsplits [split_split]) 1);
wenzelm@5132
    49
by (simp_tac (simpset() addsimps [Let_def,maxsplit_eq]
paulson@6918
    50
                        addsplits [split_split]) 1);
wenzelm@5132
    51
by (etac thin_rl 1);
wenzelm@5132
    52
by (strip_tac 1);
wenzelm@5132
    53
by (rtac ballI 1);
wenzelm@5132
    54
by (etac exE 1);
wenzelm@5132
    55
by (etac allE 1);
wenzelm@5132
    56
by Auto_tac;
wenzelm@9896
    57
qed "chop_nonempty";
nipkow@4714
    58
nipkow@4714
    59
val [prem] = goalw thy [is_maxchopper_def]
nipkow@4714
    60
 "is_maxsplitter P splitf ==> is_maxchopper P (chop splitf)";
wenzelm@5132
    61
by (Clarify_tac 1);
wenzelm@5132
    62
by (rtac iffI 1);
wenzelm@5132
    63
 by (rtac conjI 1);
wenzelm@5132
    64
  by (etac (prem RS chop_concat) 1);
wenzelm@5132
    65
 by (rtac conjI 1);
wenzelm@9896
    66
  by (etac (prem RS (chop_nonempty RS spec RS spec RS mp)) 1);
wenzelm@5132
    67
 by (etac rev_mp 1);
wenzelm@5132
    68
 by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
wenzelm@5132
    69
 by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
nipkow@4832
    70
                        addsplits [split_split]) 1);
wenzelm@5132
    71
 by (Clarify_tac 1);
wenzelm@5132
    72
 by (rtac conjI 1);
wenzelm@5132
    73
  by (Clarify_tac 1);
wenzelm@5132
    74
 by (Clarify_tac 1);
wenzelm@5132
    75
 by (Asm_full_simp_tac 1);
wenzelm@5132
    76
 by (forward_tac [prem RS chop_concat] 1);
wenzelm@5132
    77
 by (Clarify_tac 1);
wenzelm@5132
    78
by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
nipkow@5161
    79
by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
nipkow@4832
    80
                        addsplits [split_split]) 1);
wenzelm@5132
    81
by (Clarify_tac 1);
wenzelm@5168
    82
by (rename_tac "xs1 ys1 xss1 ys" 1);
paulson@14401
    83
by (split_asm_tac [thm "list.split_asm"] 1);
wenzelm@5132
    84
 by (Asm_full_simp_tac 1);
wenzelm@5132
    85
 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
wenzelm@10338
    86
 by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2]) 1);
nipkow@5161
    87
by (rtac conjI 1);
nipkow@5161
    88
 by (Clarify_tac 1);
wenzelm@5132
    89
 by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
wenzelm@10338
    90
 by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2]) 1);
wenzelm@5132
    91
by (Clarify_tac 1);
wenzelm@5168
    92
by (rename_tac "us uss" 1);
nipkow@5161
    93
by (subgoal_tac "xs1=us" 1);
wenzelm@5132
    94
 by (Asm_full_simp_tac 1);
wenzelm@5132
    95
by (Asm_full_simp_tac 1);
wenzelm@5132
    96
by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
wenzelm@10338
    97
by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2, order_antisym]) 1);
nipkow@4714
    98
qed "is_maxchopper_chop";