src/HOL/Lex/Prefix.ML
author nipkow
Tue, 24 Feb 1998 10:44:53 +0100
changeset 4647 42af8ae6e2c1
parent 4643 1b40fcac5a09
child 4936 e67949e15255
permissions -rw-r--r--
Added some lemmas.
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
(* Junk: *)
3842
b55686a7b22c fixed dots;
wenzelm
parents: 2130
diff changeset
     8
val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l. Q(l)";
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1344
diff changeset
     9
by (rtac allI 1);
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    10
by (list.induct_tac "l" 1);
1465
5d7a7e439cec expanded tabs
clasohm
parents: 1344
diff changeset
    11
by (rtac maj 1);
5d7a7e439cec expanded tabs
clasohm
parents: 1344
diff changeset
    12
by (rtac min 1);
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    13
val list_cases = result();
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    14
4643
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    15
(** <= is a partial order: **)
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    16
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    17
goalw thy [prefix_def] "xs <= (xs::'a list)";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    18
by(Simp_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    19
qed "prefix_refl";
4647
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    20
AddIffs[prefix_refl];
4643
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    21
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    22
goalw thy [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    23
by(Clarify_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    24
by(Simp_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    25
qed "prefix_trans";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    26
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    27
goalw thy [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    28
by(Clarify_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    29
by(Asm_full_simp_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    30
qed "prefix_antisym";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    31
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    32
(** recursion equations **)
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    33
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    34
goalw Prefix.thy [prefix_def] "[] <= xs";
4089
96fba19bcbe2 isatool fixclasimp;
wenzelm
parents: 3842
diff changeset
    35
by (simp_tac (simpset() addsimps [eq_sym_conv]) 1);
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    36
qed "Nil_prefix";
4647
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    37
AddIffs[Nil_prefix];
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    38
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    39
goalw Prefix.thy [prefix_def] "(xs <= []) = (xs = [])";
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    40
by (list.induct_tac "xs" 1);
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    41
by (Simp_tac 1);
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    42
by (Simp_tac 1);
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    43
qed "prefix_Nil";
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    44
Addsimps [prefix_Nil];
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    45
4643
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    46
goalw thy [prefix_def] "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    47
br iffI 1;
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    48
 be exE 1;
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    49
 by(rename_tac "zs" 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    50
 by(res_inst_tac [("xs","zs")] snoc_eq_cases 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    51
  by(Asm_full_simp_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    52
 by(hyp_subst_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    53
 by(asm_full_simp_tac (simpset() delsimps [append_assoc]
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    54
                                 addsimps [append_assoc RS sym])1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    55
be disjE 1;
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    56
 by(Asm_simp_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    57
by(Clarify_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    58
by (Simp_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    59
qed "prefix_snoc";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    60
Addsimps [prefix_snoc];
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    61
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    62
goalw Prefix.thy [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    63
by (Simp_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    64
by (Fast_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    65
qed"Cons_prefix_Cons";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    66
Addsimps [Cons_prefix_Cons];
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    67
4647
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    68
goal thy "(xs@ys <= xs@zs) = (ys <= zs)";
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    69
by (induct_tac "xs" 1);
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    70
by(ALLGOALS Asm_simp_tac);
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    71
qed "same_prefix_prefix";
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    72
Addsimps [same_prefix_prefix];
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    73
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    74
AddIffs
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    75
 [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    76
4643
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    77
goalw thy [prefix_def] "!!xs. xs <= ys ==> xs <= ys@zs";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    78
by(Clarify_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    79
by (Simp_tac 1);
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    80
qed "prefix_prefix";
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    81
Addsimps [prefix_prefix];
1b40fcac5a09 New induction schemas for lists (length and snoc).
nipkow
parents: 4423
diff changeset
    82
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    83
(* nicht sehr elegant bewiesen - Induktion eigentlich ueberfluessig *)
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    84
goalw Prefix.thy [prefix_def]
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    85
   "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    86
by (list.induct_tac "xs" 1);
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    87
by (Simp_tac 1);
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    88
by (Simp_tac 1);
1894
c2c8279d40f0 Classical tactics now use default claset.
berghofe
parents: 1465
diff changeset
    89
by (Fast_tac 1);
1344
f172a7f14e49 Half a lexical analyzer generator.
nipkow
parents:
diff changeset
    90
qed "prefix_Cons";
4647
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    91
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    92
goal thy "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    93
by(res_inst_tac [("xs","zs")] snoc_induct 1);
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    94
 by(Simp_tac 1);
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    95
 by(Blast_tac 1);
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    96
by(asm_full_simp_tac (simpset() delsimps [append_assoc]
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    97
                                addsimps [append_assoc RS sym])1);
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    98
by(Simp_tac 1);
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
    99
by(Blast_tac 1);
42af8ae6e2c1 Added some lemmas.
nipkow
parents: 4643
diff changeset
   100
qed "prefix_append";