src/HOL/Lex/Prefix.ML
author paulson
Wed, 07 Oct 1998 10:31:30 +0200
changeset 5619 76a8c72e3fd4
parent 5609 03d74c85a818
child 6675 63e53327f5e5
permissions -rw-r--r--
new theorems
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1344
diff changeset
     1
(*  Title:      HOL/Lex/Prefix.thy
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1344
diff changeset
     3
    Author:     Richard Mayr & Tobias Nipkow
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     4
    Copyright   1995 TUM
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     5
*)
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
     6
4643
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
     7
(** <= is a partial order: **)
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
     8
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4936
diff changeset
     9
Goalw [prefix_def] "xs <= (xs::'a list)";
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    10
by (Simp_tac 1);
4643
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    11
qed "prefix_refl";
4647
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    12
AddIffs[prefix_refl];
4643
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    13
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4936
diff changeset
    14
Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    15
by (Clarify_tac 1);
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    16
by (Simp_tac 1);
4643
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    17
qed "prefix_trans";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    18
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4936
diff changeset
    19
Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys";
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    20
by (Clarify_tac 1);
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    21
by (Asm_full_simp_tac 1);
4643
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    22
qed "prefix_antisym";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    23
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    24
(** recursion equations **)
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    25
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4936
diff changeset
    26
Goalw [prefix_def] "[] <= xs";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    27
by (simp_tac (simpset() addsimps [eq_sym_conv]) 1);
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    28
qed "Nil_prefix";
4647
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    29
AddIffs[Nil_prefix];
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    30
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4936
diff changeset
    31
Goalw [prefix_def] "(xs <= []) = (xs = [])";
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 5132
diff changeset
    32
by (induct_tac "xs" 1);
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    33
by (Simp_tac 1);
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    34
by (Simp_tac 1);
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    35
qed "prefix_Nil";
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    36
Addsimps [prefix_Nil];
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    37
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4936
diff changeset
    38
Goalw [prefix_def] "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)";
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    39
by (rtac iffI 1);
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    40
 by (etac exE 1);
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    41
 by (rename_tac "zs" 1);
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    42
 by (res_inst_tac [("xs","zs")] rev_exhaust 1);
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    43
  by (Asm_full_simp_tac 1);
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    44
 by (hyp_subst_tac 1);
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    45
 by (asm_full_simp_tac (simpset() delsimps [append_assoc]
4643
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    46
                                 addsimps [append_assoc RS sym])1);
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    47
by (etac disjE 1);
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    48
 by (Asm_simp_tac 1);
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    49
by (Clarify_tac 1);
4643
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    50
by (Simp_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    51
qed "prefix_snoc";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    52
Addsimps [prefix_snoc];
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    53
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4936
diff changeset
    54
Goalw [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
4643
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    55
by (Simp_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    56
by (Fast_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    57
qed"Cons_prefix_Cons";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    58
Addsimps [Cons_prefix_Cons];
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    59
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4936
diff changeset
    60
Goal "(xs@ys <= xs@zs) = (ys <= zs)";
4647
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    61
by (induct_tac "xs" 1);
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    62
by (ALLGOALS Asm_simp_tac);
4647
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    63
qed "same_prefix_prefix";
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    64
Addsimps [same_prefix_prefix];
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    65
5456
paulson
parents: 5184
diff changeset
    66
AddIffs   (* (xs@ys <= xs) = (ys <= []) *)
4647
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    67
 [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    68
5118
6b995dad8a9d Removed leading !! in goals.
nipkow
parents: 5069
diff changeset
    69
Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs";
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    70
by (Clarify_tac 1);
4643
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    71
by (Simp_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    72
qed "prefix_prefix";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    73
Addsimps [prefix_prefix];
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    74
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4936
diff changeset
    75
Goalw [prefix_def]
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    76
   "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
5456
paulson
parents: 5184
diff changeset
    77
by (exhaust_tac "xs" 1);
paulson
parents: 5184
diff changeset
    78
by Auto_tac;
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    79
qed "prefix_Cons";
4647
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    80
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4936
diff changeset
    81
Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    82
by (res_inst_tac [("xs","zs")] rev_induct 1);
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    83
 by (Simp_tac 1);
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    84
 by (Blast_tac 1);
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    85
by (asm_full_simp_tac (simpset() delsimps [append_assoc]
5456
paulson
parents: 5184
diff changeset
    86
                                 addsimps [append_assoc RS sym])1);
5132
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    87
by (Simp_tac 1);
24f992a25adc isatool expandshort;
wenzelm
parents: 5118
diff changeset
    88
by (Blast_tac 1);
4647
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    89
qed "prefix_append";
5619
76a8c72e3fd4 new theorems
paulson
parents: 5609
diff changeset
    90
76a8c72e3fd4 new theorems
paulson
parents: 5609
diff changeset
    91
Goalw [prefix_def]
76a8c72e3fd4 new theorems
paulson
parents: 5609
diff changeset
    92
  "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys";
76a8c72e3fd4 new theorems
paulson
parents: 5609
diff changeset
    93
by (auto_tac(claset(), simpset() addsimps [nth_append]));
76a8c72e3fd4 new theorems
paulson
parents: 5609
diff changeset
    94
by (exhaust_tac "ys" 1);
76a8c72e3fd4 new theorems
paulson
parents: 5609
diff changeset
    95
by Auto_tac;
76a8c72e3fd4 new theorems
paulson
parents: 5609
diff changeset
    96
qed "append_one_prefix";
76a8c72e3fd4 new theorems
paulson
parents: 5609
diff changeset
    97
76a8c72e3fd4 new theorems
paulson
parents: 5609
diff changeset
    98
Goalw [prefix_def] "xs <= ys ==> length xs <= length ys";
76a8c72e3fd4 new theorems
paulson
parents: 5609
diff changeset
    99
by Auto_tac;
76a8c72e3fd4 new theorems
paulson
parents: 5609
diff changeset
   100
qed "prefix_length_le";