src/HOL/Induct/LFilter.ML
author berghofe
Fri, 24 Jul 1998 13:39:47 +0200
changeset 5191 8ceaa19f7717
parent 5143 b94cd208f073
child 5223 4cb05273f764
permissions -rw-r--r--
Renamed '$' to 'Scons' because of clashes with constants of the same name in theories using datatypes.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     1
(*  Title:      HOL/ex/LFilter
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     2
    ID:         $Id$
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     4
    Copyright   1997  University of Cambridge
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     5
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     6
The "filter" functional for coinductive lists
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     7
  --defined by a combination of induction and coinduction
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     8
*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     9
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    10
open LFilter;
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    11
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    12
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    13
(*** findRel: basic laws ****)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    15
val findRel_LConsE = 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    16
    findRel.mk_cases [LCons_LCons_eq] "(LCons x l, l'') : findRel p";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    17
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    18
AddSEs [findRel_LConsE];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    19
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    20
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    21
Goal "(l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    22
by (etac findRel.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    23
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    24
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    25
qed_spec_mp "findRel_functional";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    26
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    27
Goal "(l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    28
by (etac findRel.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    29
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    30
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    31
qed_spec_mp "findRel_imp_LCons";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    32
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    33
Goal "(LNil,l): findRel p ==> R";
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    34
by (blast_tac (claset() addEs [findRel.elim]) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    35
qed "findRel_LNil";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    36
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    37
AddSEs [findRel_LNil];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    38
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    39
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    40
(*** Properties of Domain (findRel p) ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    41
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    42
Goal "LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    43
by (case_tac "p x" 1);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    44
by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    45
qed "LCons_Domain_findRel";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    46
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    47
Addsimps [LCons_Domain_findRel];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    48
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    49
val major::prems = 
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    50
Goal "[| l: Domain (findRel p);                                   \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    51
\            !!x l'. [| (l, LCons x l') : findRel p;  p x |] ==> Q    \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    52
\         |] ==> Q";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    53
by (rtac (major RS DomainE) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    54
by (forward_tac [findRel_imp_LCons] 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    55
by (REPEAT (eresolve_tac [exE,conjE] 1));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    56
by (hyp_subst_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    57
by (REPEAT (ares_tac prems 1));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    58
qed "Domain_findRelE";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    59
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    60
val prems = goal thy
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    61
    "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)";
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3120
diff changeset
    62
by (Clarify_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    63
by (etac findRel.induct 1);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    64
by (blast_tac (claset() addIs (findRel.intrs@prems)) 1);
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    65
by (blast_tac (claset() addIs findRel.intrs) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    66
qed "Domain_findRel_mono";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    67
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    68
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    69
(*** find: basic equations ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    70
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
    71
Goalw [find_def] "find p LNil = LNil";
4535
f24cebc299e4 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
    72
by (Blast_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    73
qed "find_LNil";
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
    74
Addsimps [find_LNil];
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    75
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    76
Goalw [find_def] "(l,l') : findRel p ==> find p l = l'";
4535
f24cebc299e4 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
    77
by (blast_tac (claset() addDs [findRel_functional]) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    78
qed "findRel_imp_find";
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
    79
Addsimps [findRel_imp_find];
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    80
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    81
Goal "p x ==> find p (LCons x l) = LCons x l";
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    82
by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    83
qed "find_LCons_found";
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
    84
Addsimps [find_LCons_found];
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    85
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    86
Goalw [find_def] "l ~: Domain(findRel p) ==> find p l = LNil";
4535
f24cebc299e4 added select_equality to the implicit claset
oheimb
parents: 4521
diff changeset
    87
by (Blast_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    88
qed "diverge_find_LNil";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    89
Addsimps [diverge_find_LNil];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    90
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
    91
Goal "~ (p x) ==> find p (LCons x l) = find p l";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    92
by (case_tac "LCons x l : Domain(findRel p)" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    93
by (Asm_full_simp_tac 2);
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3120
diff changeset
    94
by (Clarify_tac 1);
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
    95
by (Asm_simp_tac 1);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
    96
by (blast_tac (claset() addIs (findRel_imp_find::findRel.intrs)) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    97
qed "find_LCons_seek";
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
    98
Addsimps [find_LCons_seek];
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    99
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   100
Goal "find p (LCons x l) = (if p x then LCons x l else find p l)";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4535
diff changeset
   101
by (Asm_simp_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   102
qed "find_LCons";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   103
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   104
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   105
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   106
(*** lfilter: basic equations ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   107
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   108
Goal "lfilter p LNil = LNil";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   109
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   110
by (Simp_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   111
qed "lfilter_LNil";
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   112
Addsimps [lfilter_LNil];
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   113
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   114
Goal "l ~: Domain(findRel p) ==> lfilter p l = LNil";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   115
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   116
by (Asm_simp_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   117
qed "diverge_lfilter_LNil";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   118
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   119
Addsimps [diverge_lfilter_LNil];
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   120
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   121
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   122
Goal "p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   123
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   124
by (Asm_simp_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   125
qed "lfilter_LCons_found";
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   126
(*This rewrite and lfilter_LCons_seek are NOT added because lfilter_LCons
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   127
  subsumes both*)
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   128
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   129
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   130
Goal "(l, LCons x l') : findRel p \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   131
\              ==> lfilter p l = LCons x (lfilter p l')";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   132
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   133
by (Asm_simp_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   134
qed "findRel_imp_lfilter";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   135
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   136
Addsimps [findRel_imp_lfilter];
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   137
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   138
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   139
Goal "~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   140
by (rtac (lfilter_def RS def_llist_corec RS trans) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   141
by (case_tac "LCons x l : Domain(findRel p)" 1);
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   142
by (Asm_full_simp_tac 2);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   143
by (etac Domain_findRelE 1);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   144
by (safe_tac (claset() delrules [conjI]));
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   145
by (Asm_full_simp_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   146
qed "lfilter_LCons_seek";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   147
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   148
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   149
Goal "lfilter p (LCons x l) = \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   150
\         (if p x then LCons x (lfilter p l) else lfilter p l)";
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4535
diff changeset
   151
by (asm_simp_tac (simpset() addsimps [lfilter_LCons_found, lfilter_LCons_seek]) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   152
qed "lfilter_LCons";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   153
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   154
AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   155
Addsimps [lfilter_LCons];
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   156
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   157
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   158
Goal "lfilter p l = LNil ==> l ~: Domain(findRel p)";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   159
by (rtac notI 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   160
by (etac Domain_findRelE 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   161
by (etac rev_mp 1);
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   162
by (Asm_simp_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   163
qed "lfilter_eq_LNil";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   164
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   165
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   166
Goal "lfilter p l = LCons x l' -->     \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   167
\              (EX l''. l' = lfilter p l'' & (l, LCons x l'') : findRel p)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   168
by (stac (lfilter_def RS def_llist_corec) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   169
by (case_tac "l : Domain(findRel p)" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   170
by (etac Domain_findRelE 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   171
by (Asm_simp_tac 2);
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   172
by (Asm_simp_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   173
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   174
qed_spec_mp "lfilter_eq_LCons";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   175
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   176
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   177
Goal "lfilter p l = LNil  |  \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   178
\         (EX y l'. lfilter p l = LCons y (lfilter p l') & p y)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   179
by (case_tac "l : Domain(findRel p)" 1);
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   180
by (Asm_simp_tac 2);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   181
by (blast_tac (claset() addSEs [Domain_findRelE] 
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   182
                        addIs  [findRel_imp_lfilter]) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   183
qed "lfilter_cases";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   184
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   185
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   186
(*** lfilter: simple facts by coinduction ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   187
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   188
Goal "lfilter (%x. True) l = l";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   189
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   190
by (ALLGOALS Simp_tac);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   191
qed "lfilter_K_True";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   192
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   193
Goal "lfilter p (lfilter p l) = lfilter p l";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   194
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4535
diff changeset
   195
by (ALLGOALS Simp_tac);
3724
f33e301a89f5 Step_tac -> Safe_tac
paulson
parents: 3718
diff changeset
   196
by Safe_tac;
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   197
(*Cases: p x is true or false*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   198
by (rtac (lfilter_cases RS disjE) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   199
by (etac ssubst 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4090
diff changeset
   200
by Auto_tac;
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   201
qed "lfilter_idem";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   202
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   203
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   204
(*** Numerous lemmas required to prove lfilter_conj:
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   205
     lfilter p (lfilter q l) = lfilter (%x. p x & q x) l
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   206
 ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   207
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   208
Goal "(l,l') : findRel q \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   209
\           ==> l' = LCons x l'' --> p x --> (l,l') : findRel (%x. p x & q x)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   210
by (etac findRel.induct 1);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   211
by (blast_tac (claset() addIs findRel.intrs) 1);
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   212
by (blast_tac (claset() addIs findRel.intrs) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   213
qed_spec_mp "findRel_conj_lemma";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   214
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   215
val findRel_conj = refl RSN (2, findRel_conj_lemma);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   216
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   217
Goal "(l,l'') : findRel (%x. p x & q x) \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   218
\              ==> (l, LCons x l') : findRel q --> ~ p x     \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   219
\                  --> l' : Domain (findRel (%x. p x & q x))";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   220
by (etac findRel.induct 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4090
diff changeset
   221
by Auto_tac;
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   222
qed_spec_mp "findRel_not_conj_Domain";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   223
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   224
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   225
Goal "(l,lxx) : findRel q ==> \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   226
\            lxx = LCons x lx --> (lx,lz) : findRel(%x. p x & q x) --> ~ p x \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   227
\            --> (l,lz) : findRel (%x. p x & q x)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   228
by (etac findRel.induct 1);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   229
by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   230
qed_spec_mp "findRel_conj2";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   231
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   232
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   233
Goal "(lx,ly) : findRel p \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   234
\              ==> ALL l. lx = lfilter q l \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   235
\                  --> l : Domain (findRel(%x. p x & q x))";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   236
by (etac findRel.induct 1);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   237
by (blast_tac (claset() addSDs [sym RS lfilter_eq_LCons]
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   238
                        addIs  [findRel_conj]) 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4090
diff changeset
   239
by Auto_tac;
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   240
by (dtac (sym RS lfilter_eq_LCons) 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4090
diff changeset
   241
by Auto_tac;
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   242
by (dtac spec 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   243
by (dtac (refl RS rev_mp) 1);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   244
by (blast_tac (claset() addIs [findRel_conj2]) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   245
qed_spec_mp "findRel_lfilter_Domain_conj";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   246
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   247
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   248
Goal "(l,l'') : findRel(%x. p x & q x) \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   249
\              ==> l'' = LCons y l' --> \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   250
\                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   251
by (etac findRel.induct 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4535
diff changeset
   252
by (ALLGOALS Asm_simp_tac);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   253
by (ALLGOALS (blast_tac (claset() addIs findRel.intrs)));
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   254
qed_spec_mp "findRel_conj_lfilter";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   255
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   256
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   257
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   258
Goal "(lfilter p (lfilter q l), lfilter (%x. p x & q x) l)  \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   259
\         : llistD_Fun (range                                   \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   260
\                       (%u. (lfilter p (lfilter q u),          \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   261
\                             lfilter (%x. p x & q x) u)))";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   262
by (case_tac "l : Domain(findRel q)" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   263
by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   264
by (blast_tac (claset() addIs [impOfSubs Domain_findRel_mono]) 3);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   265
(*There are no qs in l: both lists are LNil*)
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   266
by (Asm_simp_tac 2);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   267
by (etac Domain_findRelE 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   268
(*case q x*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   269
by (case_tac "p x" 1);
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   270
by (asm_simp_tac (simpset() addsimps [findRel_conj RS findRel_imp_lfilter]) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   271
(*case q x and ~(p x) *)
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   272
by (Asm_simp_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   273
by (case_tac "l' : Domain (findRel (%x. p x & q x))" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   274
(*subcase: there is no p&q in l' and therefore none in l*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   275
by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   276
by (blast_tac (claset() addIs [findRel_not_conj_Domain]) 3);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   277
by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   278
by (blast_tac (claset() addIs [findRel_lfilter_Domain_conj]) 3);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   279
(*    ...and therefore too, no p in lfilter q l'.  Both results are Lnil*)
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   280
by (Asm_simp_tac 2);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   281
(*subcase: there is a p&q in l' and therefore also one in l*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   282
by (etac Domain_findRelE 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   283
by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   284
by (blast_tac (claset() addIs [findRel_conj2]) 2);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   285
by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   286
by (blast_tac (claset() addIs [findRel_conj_lfilter]) 2);
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   287
by (Asm_simp_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   288
val lemma = result();
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   289
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   290
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   291
Goal "lfilter p (lfilter q l) = lfilter (%x. p x & q x) l";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   292
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4535
diff changeset
   293
by (ALLGOALS Simp_tac);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   294
by (blast_tac (claset() addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   295
qed "lfilter_conj";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   296
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   297
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   298
(*** Numerous lemmas required to prove ??:
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   299
     lfilter p (lmap f l) = lmap f (lfilter (%x. p(f x)) l)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   300
 ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   301
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   302
Goal "(l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   303
by (etac findRel.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   304
by (ALLGOALS Asm_full_simp_tac);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   305
qed "findRel_lmap_Domain";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   306
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   307
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   308
Goal "lmap f l = LCons x l' -->     \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   309
\              (EX y l''. x = f y & l' = lmap f l'' & l = LCons y l'')";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   310
by (stac (lmap_def RS def_llist_corec) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   311
by (res_inst_tac [("l", "l")] llistE 1);
4477
b3e5857d8d99 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents: 4090
diff changeset
   312
by Auto_tac;
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   313
qed_spec_mp "lmap_eq_LCons";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   314
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   315
5143
b94cd208f073 Removal of leading "\!\!..." from most Goal commands
paulson
parents: 5069
diff changeset
   316
Goal "(lx,ly) : findRel p ==>  \
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   317
\    ALL l. lmap f l = lx --> ly = LCons x l' --> \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   318
\    (EX y l''. x = f y & l' = lmap f l'' &       \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   319
\    (l, LCons y l'') : findRel(%x. p(f x)))";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   320
by (etac findRel.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   321
by (ALLGOALS Asm_simp_tac);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   322
by (safe_tac (claset() addSDs [lmap_eq_LCons]));
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   323
by (blast_tac (claset() addIs findRel.intrs) 1);
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   324
by (blast_tac (claset() addIs findRel.intrs) 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   325
qed_spec_mp "lmap_LCons_findRel_lemma";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   326
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   327
val lmap_LCons_findRel = refl RSN (2, refl RSN (2, lmap_LCons_findRel_lemma));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   328
5069
3ea049f7979d isatool fixgoal;
wenzelm
parents: 4686
diff changeset
   329
Goal "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   330
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
4686
74a12e86b20b Removed `addsplits [expand_if]'
nipkow
parents: 4535
diff changeset
   331
by (ALLGOALS Simp_tac);
3724
f33e301a89f5 Step_tac -> Safe_tac
paulson
parents: 3718
diff changeset
   332
by Safe_tac;
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   333
by (case_tac "lmap f l : Domain (findRel p)" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   334
by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
4090
9f1eaab75e8c isatool fixclasimp;
wenzelm
parents: 3919
diff changeset
   335
by (blast_tac (claset() addIs [findRel_lmap_Domain]) 3);
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   336
by (Asm_simp_tac 2);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   337
by (etac Domain_findRelE 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   338
by (forward_tac [lmap_LCons_findRel] 1);
3718
d78cf498a88c Minor tidying to use Clarify_tac, etc.
paulson
parents: 3120
diff changeset
   339
by (Clarify_tac 1);
4521
c7f56322a84b Tidied by adding more default simprules
paulson
parents: 4477
diff changeset
   340
by (Asm_simp_tac 1);
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   341
qed "lfilter_lmap";