src/HOL/Induct/LFilter.ML
author wenzelm
Thu, 26 Jun 1997 11:14:46 +0200
changeset 3462 3472fa00b1d4
parent 3120 c58423c20740
child 3718 d78cf498a88c
permissions -rw-r--r--
rearrange pages of ps file to be printed as booklet (duplex);
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
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    21
goal thy "!!p. (l,l'): findRel p ==> (l,l''): findRel p --> l'' = l'";
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
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    27
goal thy "!!p. (l,l'): findRel p ==> EX x l''. l' = LCons x l'' & p x";
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
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    33
goal thy "!!p. (LNil,l): findRel p ==> R";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    34
by (blast_tac (!claset addEs [findRel.elim]) 1);
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
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    42
goal thy "!!p. LCons x l : Domain(findRel p) = (p x | l : Domain(findRel p))";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    43
by (case_tac "p x" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    44
by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
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 = 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    50
goal thy "[| l: Domain (findRel p);                                   \
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)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    62
by (Step_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    63
by (etac findRel.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    64
by (blast_tac (!claset addIs (findRel.intrs@prems)) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    65
by (blast_tac (!claset addIs findRel.intrs) 1);
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
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    71
goalw thy [find_def] "find p LNil = LNil";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    72
by (blast_tac (!claset addIs [select_equality]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    73
qed "find_LNil";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    74
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    75
goalw thy [find_def] "!!p. (l,l') : findRel p ==> find p l = l'";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    76
by (blast_tac (!claset addIs [select_equality] addDs [findRel_functional]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    77
qed "findRel_imp_find";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    78
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    79
goal thy "!!p. p x ==> find p (LCons x l) = LCons x l";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    80
by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    81
qed "find_LCons_found";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    82
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    83
goalw thy [find_def] "!!p. l ~: Domain(findRel p) ==> find p l = LNil";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    84
by (blast_tac (!claset addIs [select_equality]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    85
qed "diverge_find_LNil";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    86
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    87
Addsimps [diverge_find_LNil];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    88
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    89
goal thy "!!p. ~ (p x) ==> find p (LCons x l) = find p l";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    90
by (case_tac "LCons x l : Domain(findRel p)" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    91
by (Asm_full_simp_tac 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    92
by (Step_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    93
by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    94
by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    95
qed "find_LCons_seek";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    96
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    97
goal thy "find p (LCons x l) = (if p x then LCons x l else find p l)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    98
by (asm_simp_tac (!simpset addsimps [find_LCons_found, find_LCons_seek]
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    99
                           setloop split_tac[expand_if]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   100
qed "find_LCons";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   101
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   102
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
(*** lfilter: basic equations ***)
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
goal thy "lfilter p LNil = LNil";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   107
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
   108
by (simp_tac (!simpset addsimps [find_LNil]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   109
qed "lfilter_LNil";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   110
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   111
goal thy "!!p. l ~: Domain(findRel p) ==> lfilter p l = LNil";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   112
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
   113
by (Asm_simp_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   114
qed "diverge_lfilter_LNil";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   115
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   116
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   117
goal thy "!!p. p x ==> lfilter p (LCons x l) = LCons x (lfilter p l)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   118
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
   119
by (asm_simp_tac (!simpset addsimps [find_LCons_found]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   120
qed "lfilter_LCons_found";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   121
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   122
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   123
goal thy "!!p. (l, LCons x l') : findRel p \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   124
\              ==> lfilter p l = LCons x (lfilter p l')";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   125
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
   126
by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   127
qed "findRel_imp_lfilter";
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
goal thy "!!p. ~ (p x) ==> lfilter p (LCons x l) = lfilter p l";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   130
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
   131
by (case_tac "LCons x l : Domain(findRel p)" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   132
by (asm_full_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   133
by (etac Domain_findRelE 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   134
by (safe_tac (!claset delrules [conjI]));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   135
by (asm_full_simp_tac 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   136
    (!simpset addsimps [findRel_imp_lfilter, findRel_imp_find,
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   137
                        find_LCons_seek]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   138
qed "lfilter_LCons_seek";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   139
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   140
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   141
goal thy "lfilter p (LCons x l) = \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   142
\         (if p x then LCons x (lfilter p l) else lfilter p l)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   143
by (asm_simp_tac (!simpset addsimps [lfilter_LCons_found, lfilter_LCons_seek]
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   144
                           setloop split_tac[expand_if]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   145
qed "lfilter_LCons";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   146
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   147
AddSIs [llistD_Fun_LNil_I, llistD_Fun_LCons_I];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   148
Addsimps [lfilter_LNil, lfilter_LCons];
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   149
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   150
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   151
goal thy "!!p. lfilter p l = LNil ==> l ~: Domain(findRel p)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   152
by (rtac notI 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   153
by (etac Domain_findRelE 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   154
by (etac rev_mp 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   155
by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   156
qed "lfilter_eq_LNil";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   157
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   158
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   159
goal thy "!!p. lfilter p l = LCons x l' -->     \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   160
\              (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
   161
by (stac (lfilter_def RS def_llist_corec) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   162
by (case_tac "l : Domain(findRel p)" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   163
by (etac Domain_findRelE 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   164
by (Asm_simp_tac 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   165
by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   166
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   167
qed_spec_mp "lfilter_eq_LCons";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   168
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   169
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   170
goal thy "lfilter p l = LNil  |  \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   171
\         (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
   172
by (case_tac "l : Domain(findRel p)" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   173
by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   174
by (blast_tac (!claset addSEs [Domain_findRelE] 
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   175
                       addIs [findRel_imp_lfilter]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   176
qed "lfilter_cases";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   177
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   178
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   179
(*** lfilter: simple facts by coinduction ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   180
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   181
goal thy "lfilter (%x.True) l = l";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   182
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   183
by (ALLGOALS Simp_tac);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   184
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   185
qed "lfilter_K_True";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   186
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   187
goal thy "lfilter p (lfilter p l) = lfilter p l";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   188
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   189
by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   190
by (Step_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   191
(*Cases: p x is true or false*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   192
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   193
by (rtac (lfilter_cases RS disjE) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   194
by (etac ssubst 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   195
by (Auto_tac());
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   196
qed "lfilter_idem";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   197
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   198
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   199
(*** Numerous lemmas required to prove lfilter_conj:
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   200
     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
   201
 ***)
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
goal thy "!!p. (l,l') : findRel q \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   204
\           ==> 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
   205
by (etac findRel.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   206
by (blast_tac (!claset addIs findRel.intrs) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   207
by (blast_tac (!claset addIs findRel.intrs) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   208
qed_spec_mp "findRel_conj_lemma";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   209
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   210
val findRel_conj = refl RSN (2, findRel_conj_lemma);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   211
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   212
goal thy "!!p. (l,l'') : findRel (%x. p x & q x) \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   213
\              ==> (l, LCons x l') : findRel q --> ~ p x     \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   214
\                  --> l' : Domain (findRel (%x. p x & q x))";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   215
by (etac findRel.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   216
by (Auto_tac());
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   217
qed_spec_mp "findRel_not_conj_Domain";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   218
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   219
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   220
goal thy "!!p. (l,lxx) : findRel q ==> \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   221
\            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
   222
\            --> (l,lz) : findRel (%x. p x & q x)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   223
by (etac findRel.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   224
by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   225
qed_spec_mp "findRel_conj2";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   226
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   227
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   228
goal thy "!!p. (lx,ly) : findRel p \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   229
\              ==> ALL l. lx = lfilter q l \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   230
\                  --> l : Domain (findRel(%x. p x & q x))";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   231
by (etac findRel.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   232
by (blast_tac (!claset addSDs [sym RS lfilter_eq_LCons]
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   233
                       addIs  [findRel_conj]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   234
by (Auto_tac());
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   235
by (dtac (sym RS lfilter_eq_LCons) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   236
by (Auto_tac());
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   237
by (dtac spec 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   238
by (dtac (refl RS rev_mp) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   239
by (blast_tac (!claset addIs [findRel_conj2]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   240
qed_spec_mp "findRel_lfilter_Domain_conj";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   241
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   242
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   243
goal thy "!!p. (l,l'') : findRel(%x. p x & q x) \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   244
\              ==> l'' = LCons y l' --> \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   245
\                  (lfilter q l, LCons y (lfilter q l')) : findRel p";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   246
by (etac findRel.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   247
by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac[expand_if])));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   248
by (ALLGOALS (blast_tac (!claset addIs findRel.intrs)));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   249
qed_spec_mp "findRel_conj_lfilter";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   250
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   251
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   252
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   253
goal thy "(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
   254
\         : llistD_Fun (range                                   \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   255
\                       (%u. (lfilter p (lfilter q u),          \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   256
\                             lfilter (%x. p x & q x) u)))";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   257
by (case_tac "l : Domain(findRel q)" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   258
by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   259
by (blast_tac (!claset addIs [impOfSubs Domain_findRel_mono]) 3);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   260
(*There are no qs in l: both lists are LNil*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   261
by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   262
by (etac Domain_findRelE 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   263
(*case q x*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   264
by (case_tac "p x" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   265
by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter,
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   266
                                     findRel_conj RS findRel_imp_lfilter]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   267
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   268
(*case q x and ~(p x) *)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   269
by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   270
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
   271
(*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
   272
by (subgoal_tac "l ~: Domain (findRel (%x. p x & q x))" 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   273
by (blast_tac (!claset addIs [findRel_not_conj_Domain]) 3);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   274
by (subgoal_tac "lfilter q l' ~: Domain(findRel p)" 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   275
by (blast_tac (!claset addIs [findRel_lfilter_Domain_conj]) 3);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   276
(*    ...and therefore too, no p in lfilter q l'.  Both results are Lnil*)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   277
by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   278
(*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
   279
by (etac Domain_findRelE 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   280
by (subgoal_tac "(l, LCons xa l'a) : findRel(%x. p x & q x)" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   281
by (blast_tac (!claset addIs [findRel_conj2]) 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   282
by (subgoal_tac "(lfilter q l', LCons xa (lfilter q l'a)) : findRel p" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   283
by (blast_tac (!claset addIs [findRel_conj_lfilter]) 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   284
by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   285
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   286
val lemma = result();
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   287
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   288
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   289
goal thy "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
   290
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   291
by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   292
by (blast_tac (!claset addIs [lemma, impOfSubs llistD_Fun_mono]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   293
qed "lfilter_conj";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   294
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   295
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   296
(*** Numerous lemmas required to prove ??:
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   297
     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
   298
 ***)
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   299
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   300
goal thy "!!p. (l,l') : findRel(%x. p (f x)) ==> lmap f l : Domain(findRel p)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   301
by (etac findRel.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   302
by (ALLGOALS Asm_full_simp_tac);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   303
qed "findRel_lmap_Domain";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   304
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   305
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   306
goal thy "!!p. lmap f l = LCons x l' -->     \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   307
\              (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
   308
by (stac (lmap_def RS def_llist_corec) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   309
by (res_inst_tac [("l", "l")] llistE 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   310
by (Auto_tac());
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   311
qed_spec_mp "lmap_eq_LCons";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   312
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   313
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   314
goal thy "!!p. (lx,ly) : findRel p ==>  \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   315
\    ALL l. lmap f l = lx --> ly = LCons x l' --> \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   316
\    (EX y l''. x = f y & l' = lmap f l'' &       \
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   317
\    (l, LCons y l'') : findRel(%x. p(f x)))";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   318
by (etac findRel.induct 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   319
by (ALLGOALS Asm_simp_tac);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   320
by (safe_tac (!claset addSDs [lmap_eq_LCons]));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   321
by (blast_tac (!claset addIs findRel.intrs) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   322
by (blast_tac (!claset addIs findRel.intrs) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   323
qed_spec_mp "lmap_LCons_findRel_lemma";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   324
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   325
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
   326
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   327
goal thy "lfilter p (lmap f l) = lmap f (lfilter (p o f) l)";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   328
by (res_inst_tac [("l","l")] llist_fun_equalityI 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   329
by (ALLGOALS (simp_tac (!simpset setloop split_tac[expand_if])));
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   330
by (Step_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   331
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   332
by (case_tac "lmap f l : Domain (findRel p)" 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   333
by (subgoal_tac "l ~: Domain (findRel(%x. p (f x)))" 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   334
by (blast_tac (!claset addIs [findRel_lmap_Domain]) 3);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   335
by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   336
by (etac Domain_findRelE 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   337
by (forward_tac [lmap_LCons_findRel] 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   338
by (Step_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   339
by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   340
by (Blast_tac 1);
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
   341
qed "lfilter_lmap";