src/HOLCF/IOA/meta_theory/Sequence.thy
author berghofe
Wed, 11 Jul 2007 11:54:21 +0200
changeset 23778 18f426a137a9
parent 19741 f65265d71426
child 25131 2c8caac48ade
permissions -rw-r--r--
Adapted to new inductive definition package.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     1
(*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
     2
    ID:         $Id$
12218
wenzelm
parents: 12114
diff changeset
     3
    Author:     Olaf Müller
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     4
12218
wenzelm
parents: 12114
diff changeset
     5
Sequences over flat domains with lifted elements.
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     6
*)
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     7
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     8
theory Sequence
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     9
imports Seq
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    10
begin
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    11
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    12
defaultsort type
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    13
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    14
types 'a Seq = "'a::type lift seq"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    15
3952
dca1bce88ec8 replaced ops by consts;
wenzelm
parents: 3275
diff changeset
    16
consts
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    17
7229
6773ba0c36d5 renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents: 4559
diff changeset
    18
  Consq            ::"'a            => 'a Seq -> 'a Seq"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    19
  Filter           ::"('a => bool)  => 'a Seq -> 'a Seq"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    20
  Map              ::"('a => 'b)    => 'a Seq -> 'b Seq"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    21
  Forall           ::"('a => bool)  => 'a Seq => bool"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    22
  Last             ::"'a Seq        -> 'a lift"
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    23
  Dropwhile        ::"('a => bool)  => 'a Seq -> 'a Seq"
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    24
  Takewhile        ::"('a => bool)  => 'a Seq -> 'a Seq"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    25
  Zip              ::"'a Seq        -> 'b Seq -> ('a * 'b) Seq"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    26
  Flat             ::"('a Seq) seq   -> 'a Seq"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    27
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    28
  Filter2          ::"('a => bool)  => 'a Seq -> 'a Seq"
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    29
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    30
syntax
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    31
7229
6773ba0c36d5 renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents: 4559
diff changeset
    32
 "@Consq"         ::"'a => 'a Seq => 'a Seq"       ("(_/>>_)"  [66,65] 65)
4283
92707e24b62b managed merge details;
mueller
parents: 3952
diff changeset
    33
 (* list Enumeration *)
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    34
  "_totlist"      :: "args => 'a Seq"              ("[(_)!]")
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    35
  "_partlist"     :: "args => 'a Seq"              ("[(_)?]")
4283
92707e24b62b managed merge details;
mueller
parents: 3952
diff changeset
    36
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    37
12114
a8e860c86252 eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents: 12028
diff changeset
    38
syntax (xsymbols)
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    39
  "@Consq"     ::"'a => 'a Seq => 'a Seq"       ("(_\<leadsto>_)"  [66,65] 65)
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    40
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    41
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    42
translations
10835
nipkow
parents: 7229
diff changeset
    43
  "a>>s"         == "Consq a$s"
4283
92707e24b62b managed merge details;
mueller
parents: 3952
diff changeset
    44
  "[x, xs!]"     == "x>>[xs!]"
92707e24b62b managed merge details;
mueller
parents: 3952
diff changeset
    45
  "[x!]"         == "x>>nil"
92707e24b62b managed merge details;
mueller
parents: 3952
diff changeset
    46
  "[x, xs?]"     == "x>>[xs?]"
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    47
  "[x?]"         == "x>>UU"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    48
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    49
defs
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    50
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    51
Consq_def:     "Consq a == LAM s. Def a ## s"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    52
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    53
Filter_def:    "Filter P == sfilter$(flift2 P)"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    54
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    55
Map_def:       "Map f  == smap$(flift2 f)"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    56
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    57
Forall_def:    "Forall P == sforall (flift2 P)"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    58
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    59
Last_def:      "Last == slast"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    60
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    61
Dropwhile_def: "Dropwhile P == sdropwhile$(flift2 P)"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    62
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    63
Takewhile_def: "Takewhile P == stakewhile$(flift2 P)"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    64
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    65
Flat_def:      "Flat == sflat"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    66
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    67
Zip_def:
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    68
  "Zip == (fix$(LAM h t1 t2. case t1 of
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    69
               nil   => nil
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    70
             | x##xs => (case t2 of
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    71
                          nil => UU
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    72
                        | y##ys => (case x of
12028
52aa183c15bb replaced Undef by UU;
wenzelm
parents: 10835
diff changeset
    73
                                      UU  => UU
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    74
                                    | Def a => (case y of
12028
52aa183c15bb replaced Undef by UU;
wenzelm
parents: 10835
diff changeset
    75
                                                  UU => UU
10835
nipkow
parents: 7229
diff changeset
    76
                                                | Def b => Def (a,b)##(h$xs$ys))))))"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    77
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    78
Filter2_def:    "Filter2 P == (fix$(LAM h t. case t of
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    79
            nil => nil
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    80
          | x##xs => (case x of UU => UU | Def y => (if P y
10835
nipkow
parents: 7229
diff changeset
    81
                     then x##(h$xs)
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    82
                     else     h$xs))))"
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
    83
19551
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    84
declare andalso_and [simp]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    85
declare andalso_or [simp]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    86
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    87
subsection "recursive equations of operators"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    88
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    89
subsubsection "Map"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    90
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    91
lemma Map_UU: "Map f$UU =UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    92
by (simp add: Map_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    93
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    94
lemma Map_nil: "Map f$nil =nil"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    95
by (simp add: Map_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    96
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    97
lemma Map_cons: "Map f$(x>>xs)=(f x) >> Map f$xs"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    98
by (simp add: Map_def Consq_def flift2_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
    99
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   100
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   101
subsubsection {* Filter *}
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   102
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   103
lemma Filter_UU: "Filter P$UU =UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   104
by (simp add: Filter_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   105
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   106
lemma Filter_nil: "Filter P$nil =nil"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   107
by (simp add: Filter_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   108
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   109
lemma Filter_cons:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   110
  "Filter P$(x>>xs)= (if P x then x>>(Filter P$xs) else Filter P$xs)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   111
by (simp add: Filter_def Consq_def flift2_def If_and_if)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   112
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   113
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   114
subsubsection {* Forall *}
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   115
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   116
lemma Forall_UU: "Forall P UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   117
by (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   118
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   119
lemma Forall_nil: "Forall P nil"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   120
by (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   121
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   122
lemma Forall_cons: "Forall P (x>>xs)= (P x & Forall P xs)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   123
by (simp add: Forall_def sforall_def Consq_def flift2_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   124
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   125
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   126
subsubsection {* Conc *}
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   127
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   128
lemma Conc_cons: "(x>>xs) @@ y = x>>(xs @@y)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   129
by (simp add: Consq_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   130
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   131
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   132
subsubsection {* Takewhile *}
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   133
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   134
lemma Takewhile_UU: "Takewhile P$UU =UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   135
by (simp add: Takewhile_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   136
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   137
lemma Takewhile_nil: "Takewhile P$nil =nil"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   138
by (simp add: Takewhile_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   139
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   140
lemma Takewhile_cons:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   141
  "Takewhile P$(x>>xs)= (if P x then x>>(Takewhile P$xs) else nil)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   142
by (simp add: Takewhile_def Consq_def flift2_def If_and_if)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   143
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   144
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   145
subsubsection {* DropWhile *}
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   146
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   147
lemma Dropwhile_UU: "Dropwhile P$UU =UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   148
by (simp add: Dropwhile_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   149
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   150
lemma Dropwhile_nil: "Dropwhile P$nil =nil"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   151
by (simp add: Dropwhile_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   152
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   153
lemma Dropwhile_cons:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   154
  "Dropwhile P$(x>>xs)= (if P x then Dropwhile P$xs else x>>xs)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   155
by (simp add: Dropwhile_def Consq_def flift2_def If_and_if)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   156
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   157
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   158
subsubsection {* Last *}
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   159
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   160
lemma Last_UU: "Last$UU =UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   161
by (simp add: Last_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   162
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   163
lemma Last_nil: "Last$nil =UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   164
by (simp add: Last_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   165
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   166
lemma Last_cons: "Last$(x>>xs)= (if xs=nil then Def x else Last$xs)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   167
apply (simp add: Last_def Consq_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   168
apply (rule_tac x="xs" in seq.casedist)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   169
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   170
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   171
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   172
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   173
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   174
subsubsection {* Flat *}
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   175
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   176
lemma Flat_UU: "Flat$UU =UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   177
by (simp add: Flat_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   178
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   179
lemma Flat_nil: "Flat$nil =nil"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   180
by (simp add: Flat_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   181
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   182
lemma Flat_cons: "Flat$(x##xs)= x @@ (Flat$xs)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   183
by (simp add: Flat_def Consq_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   184
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   185
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   186
subsubsection {* Zip *}
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   187
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   188
lemma Zip_unfold:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   189
"Zip = (LAM t1 t2. case t1 of
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   190
                nil   => nil
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   191
              | x##xs => (case t2 of
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   192
                           nil => UU
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   193
                         | y##ys => (case x of
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   194
                                       UU  => UU
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   195
                                     | Def a => (case y of
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   196
                                                   UU => UU
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   197
                                                 | Def b => Def (a,b)##(Zip$xs$ys)))))"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   198
apply (rule trans)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   199
apply (rule fix_eq2)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   200
apply (rule Zip_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   201
apply (rule beta_cfun)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   202
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   203
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   204
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   205
lemma Zip_UU1: "Zip$UU$y =UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   206
apply (subst Zip_unfold)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   207
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   208
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   209
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   210
lemma Zip_UU2: "x~=nil ==> Zip$x$UU =UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   211
apply (subst Zip_unfold)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   212
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   213
apply (rule_tac x="x" in seq.casedist)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   214
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   215
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   216
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   217
lemma Zip_nil: "Zip$nil$y =nil"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   218
apply (subst Zip_unfold)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   219
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   220
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   221
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   222
lemma Zip_cons_nil: "Zip$(x>>xs)$nil= UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   223
apply (subst Zip_unfold)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   224
apply (simp add: Consq_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   225
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   226
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   227
lemma Zip_cons: "Zip$(x>>xs)$(y>>ys)= (x,y) >> Zip$xs$ys"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   228
apply (rule trans)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   229
apply (subst Zip_unfold)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   230
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   231
apply (simp add: Consq_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   232
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   233
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   234
lemmas [simp del] =
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   235
  sfilter_UU sfilter_nil sfilter_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   236
  smap_UU smap_nil smap_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   237
  sforall2_UU sforall2_nil sforall2_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   238
  slast_UU slast_nil slast_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   239
  stakewhile_UU  stakewhile_nil  stakewhile_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   240
  sdropwhile_UU  sdropwhile_nil  sdropwhile_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   241
  sflat_UU sflat_nil sflat_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   242
  szip_UU1 szip_UU2 szip_nil szip_cons_nil szip_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   243
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   244
lemmas [simp] =
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   245
  Filter_UU Filter_nil Filter_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   246
  Map_UU Map_nil Map_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   247
  Forall_UU Forall_nil Forall_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   248
  Last_UU Last_nil Last_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   249
  Conc_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   250
  Takewhile_UU Takewhile_nil Takewhile_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   251
  Dropwhile_UU Dropwhile_nil Dropwhile_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   252
  Zip_UU1 Zip_UU2 Zip_nil Zip_cons_nil Zip_cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   253
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   254
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   255
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   256
section "Cons"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   257
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   258
lemma Consq_def2: "a>>s = (Def a)##s"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   259
apply (simp add: Consq_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   260
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   261
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   262
lemma Seq_exhaust: "x = UU | x = nil | (? a s. x = a >> s)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   263
apply (simp add: Consq_def2)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   264
apply (cut_tac seq.exhaust)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   265
apply (fast dest: not_Undef_is_Def [THEN iffD1])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   266
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   267
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   268
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   269
lemma Seq_cases:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   270
"!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s  ==> P |] ==> P"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   271
apply (cut_tac x="x" in Seq_exhaust)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   272
apply (erule disjE)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   273
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   274
apply (erule disjE)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   275
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   276
apply (erule exE)+
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   277
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   278
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   279
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   280
(*
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   281
fun Seq_case_tac s i = rule_tac x",s)] Seq_cases i
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   282
          THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   283
*)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   284
(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   285
(*
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   286
fun Seq_case_simp_tac s i = Seq_case_tac s i THEN Asm_simp_tac (i+2)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   287
                                             THEN Asm_full_simp_tac (i+1)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   288
                                             THEN Asm_full_simp_tac i;
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   289
*)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   290
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   291
lemma Cons_not_UU: "a>>s ~= UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   292
apply (subst Consq_def2)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   293
apply (rule seq.con_rews)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   294
apply (rule Def_not_UU)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   295
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   296
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   297
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   298
lemma Cons_not_less_UU: "~(a>>x) << UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   299
apply (rule notI)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   300
apply (drule antisym_less)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   301
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   302
apply (simp add: Cons_not_UU)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   303
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   304
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   305
lemma Cons_not_less_nil: "~a>>s << nil"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   306
apply (subst Consq_def2)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   307
apply (rule seq.rews)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   308
apply (rule Def_not_UU)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   309
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   310
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   311
lemma Cons_not_nil: "a>>s ~= nil"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   312
apply (subst Consq_def2)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   313
apply (rule seq.rews)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   314
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   315
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   316
lemma Cons_not_nil2: "nil ~= a>>s"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   317
apply (simp add: Consq_def2)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   318
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   319
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   320
lemma Cons_inject_eq: "(a>>s = b>>t) = (a = b & s = t)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   321
apply (simp only: Consq_def2)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   322
apply (simp add: scons_inject_eq)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   323
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   324
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   325
lemma Cons_inject_less_eq: "(a>>s<<b>>t) = (a = b & s<<t)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   326
apply (simp add: Consq_def2)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   327
apply (simp add: seq.inverts)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   328
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   329
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   330
lemma seq_take_Cons: "seq_take (Suc n)$(a>>x) = a>> (seq_take n$x)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   331
apply (simp add: Consq_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   332
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   333
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   334
lemmas [simp] =
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   335
  Cons_not_nil2 Cons_inject_eq Cons_inject_less_eq seq_take_Cons
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   336
  Cons_not_UU Cons_not_less_UU Cons_not_less_nil Cons_not_nil
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   337
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   338
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   339
subsection "induction"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   340
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   341
lemma Seq_induct:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   342
"!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   343
apply (erule (2) seq.ind)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   344
apply (tactic {* def_tac 1 *})
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   345
apply (simp add: Consq_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   346
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   347
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   348
lemma Seq_FinitePartial_ind:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   349
"!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   350
                ==> seq_finite x --> P x"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   351
apply (erule (1) seq_finite_ind)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   352
apply (tactic {* def_tac 1 *})
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   353
apply (simp add: Consq_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   354
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   355
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   356
lemma Seq_Finite_ind:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   357
"!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x"
23778
18f426a137a9 Adapted to new inductive definition package.
berghofe
parents: 19741
diff changeset
   358
apply (erule (1) Finite.induct)
19551
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   359
apply (tactic {* def_tac 1 *})
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   360
apply (simp add: Consq_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   361
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   362
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   363
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   364
(* rws are definitions to be unfolded for admissibility check *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   365
(*
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   366
fun Seq_induct_tac s rws i = rule_tac x",s)] Seq_induct i
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   367
                         THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac (i+1))))
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   368
                         THEN simp add: rws) i;
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   369
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   370
fun Seq_Finite_induct_tac i = erule Seq_Finite_ind i
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   371
                              THEN (REPEAT_DETERM (CHANGED (Asm_simp_tac i)));
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   372
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   373
fun pair_tac s = rule_tac p",s)] PairE
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   374
                          THEN' hyp_subst_tac THEN' Simp_tac;
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   375
*)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   376
(* induction on a sequence of pairs with pairsplitting and simplification *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   377
(*
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   378
fun pair_induct_tac s rws i =
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   379
           rule_tac x",s)] Seq_induct i
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   380
           THEN pair_tac "a" (i+3)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   381
           THEN (REPEAT_DETERM (CHANGED (Simp_tac (i+1))))
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   382
           THEN simp add: rws) i;
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   383
*)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   384
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   385
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   386
(* ------------------------------------------------------------------------------------ *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   387
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   388
subsection "HD,TL"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   389
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   390
lemma HD_Cons [simp]: "HD$(x>>y) = Def x"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   391
apply (simp add: Consq_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   392
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   393
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   394
lemma TL_Cons [simp]: "TL$(x>>y) = y"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   395
apply (simp add: Consq_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   396
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   397
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   398
(* ------------------------------------------------------------------------------------ *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   399
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   400
subsection "Finite, Partial, Infinite"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   401
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   402
lemma Finite_Cons [simp]: "Finite (a>>xs) = Finite xs"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   403
apply (simp add: Consq_def2 Finite_cons)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   404
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   405
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   406
lemma FiniteConc_1: "Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   407
apply (erule Seq_Finite_ind, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   408
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   409
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   410
lemma FiniteConc_2:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   411
"Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   412
apply (erule Seq_Finite_ind)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   413
(* nil*)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   414
apply (intro strip)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   415
apply (rule_tac x="x" in Seq_cases, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   416
(* cons *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   417
apply (intro strip)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   418
apply (rule_tac x="x" in Seq_cases, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   419
apply (rule_tac x="y" in Seq_cases, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   420
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   421
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   422
lemma FiniteConc [simp]: "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   423
apply (rule iffI)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   424
apply (erule FiniteConc_2 [rule_format])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   425
apply (rule refl)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   426
apply (rule FiniteConc_1 [rule_format])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   427
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   428
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   429
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   430
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   431
lemma FiniteMap1: "Finite s ==> Finite (Map f$s)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   432
apply (erule Seq_Finite_ind, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   433
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   434
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   435
lemma FiniteMap2: "Finite s ==> ! t. (s = Map f$t) --> Finite t"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   436
apply (erule Seq_Finite_ind)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   437
apply (intro strip)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   438
apply (rule_tac x="t" in Seq_cases, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   439
(* main case *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   440
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   441
apply (rule_tac x="t" in Seq_cases, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   442
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   443
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   444
lemma Map2Finite: "Finite (Map f$s) = Finite s"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   445
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   446
apply (erule FiniteMap2 [rule_format])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   447
apply (rule refl)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   448
apply (erule FiniteMap1)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   449
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   450
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   451
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   452
lemma FiniteFilter: "Finite s ==> Finite (Filter P$s)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   453
apply (erule Seq_Finite_ind, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   454
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   455
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   456
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   457
(* ----------------------------------------------------------------------------------- *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   458
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   459
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   460
subsection "admissibility"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   461
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   462
(* Finite x is proven to be adm: Finite_flat shows that there are only chains of length one.
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   463
   Then the assumption that an _infinite_ chain exists (from admI2) is set to a contradiction
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   464
   to Finite_flat *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   465
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   466
lemma Finite_flat [rule_format]:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   467
"!! (x:: 'a Seq). Finite x ==> !y. Finite (y:: 'a Seq) & x<<y --> x=y"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   468
apply (erule Seq_Finite_ind)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   469
apply (intro strip)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   470
apply (erule conjE)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   471
apply (erule nil_less_is_nil)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   472
(* main case *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   473
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   474
apply (rule_tac x="y" in Seq_cases)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   475
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   476
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   477
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   478
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   479
lemma adm_Finite [simp]: "adm(%(x:: 'a Seq).Finite x)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   480
apply (rule admI2)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   481
apply (erule_tac x="0" in allE)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   482
back
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   483
apply (erule exE)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   484
apply (erule conjE)+
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   485
apply (rule_tac x="0" in allE)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   486
apply assumption
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   487
apply (erule_tac x="j" in allE)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   488
apply (cut_tac x="Y 0" and y="Y j" in Finite_flat)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   489
(* Generates a contradiction in subgoal 3 *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   490
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   491
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   492
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   493
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   494
(* ------------------------------------------------------------------------------------ *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   495
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   496
subsection "Conc"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   497
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   498
lemma Conc_cong: "!! x::'a Seq. Finite x ==> ((x @@ y) = (x @@ z)) = (y = z)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   499
apply (erule Seq_Finite_ind, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   500
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   501
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   502
lemma Conc_assoc: "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   503
apply (rule_tac x="x" in Seq_induct, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   504
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   505
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   506
lemma nilConc [simp]: "s@@ nil = s"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   507
apply (rule_tac x="s" in seq.ind)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   508
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   509
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   510
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   511
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   512
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   513
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   514
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   515
(* should be same as nil_is_Conc2 when all nils are turned to right side !! *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   516
lemma nil_is_Conc: "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   517
apply (rule_tac x="x" in Seq_cases)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   518
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   519
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   520
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   521
lemma nil_is_Conc2: "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   522
apply (rule_tac x="x" in Seq_cases)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   523
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   524
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   525
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   526
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   527
(* ------------------------------------------------------------------------------------ *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   528
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   529
subsection "Last"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   530
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   531
lemma Finite_Last1: "Finite s ==> s~=nil --> Last$s~=UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   532
apply (erule Seq_Finite_ind, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   533
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   534
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   535
lemma Finite_Last2: "Finite s ==> Last$s=UU --> s=nil"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   536
apply (erule Seq_Finite_ind, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   537
apply fast
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   538
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   539
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   540
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   541
(* ------------------------------------------------------------------------------------ *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   542
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   543
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   544
subsection "Filter, Conc"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   545
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   546
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   547
lemma FilterPQ: "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   548
apply (rule_tac x="s" in Seq_induct, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   549
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   550
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   551
lemma FilterConc: "Filter P$(x @@ y) = (Filter P$x @@ Filter P$y)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   552
apply (simp add: Filter_def sfiltersconc)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   553
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   554
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   555
(* ------------------------------------------------------------------------------------ *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   556
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   557
subsection "Map"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   558
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   559
lemma MapMap: "Map f$(Map g$s) = Map (f o g)$s"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   560
apply (rule_tac x="s" in Seq_induct, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   561
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   562
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   563
lemma MapConc: "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   564
apply (rule_tac x="x" in Seq_induct, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   565
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   566
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   567
lemma MapFilter: "Filter P$(Map f$x) = Map f$(Filter (P o f)$x)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   568
apply (rule_tac x="x" in Seq_induct, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   569
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   570
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   571
lemma nilMap: "nil = (Map f$s) --> s= nil"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   572
apply (rule_tac x="s" in Seq_cases, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   573
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   574
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   575
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   576
lemma ForallMap: "Forall P (Map f$s) = Forall (P o f) s"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   577
apply (rule_tac x="s" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   578
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   579
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   580
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   581
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   582
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   583
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   584
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   585
(* ------------------------------------------------------------------------------------ *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   586
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   587
subsection "Forall"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   588
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   589
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   590
lemma ForallPForallQ1: "Forall P ys & (! x. P x --> Q x) \
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   591
\         --> Forall Q ys"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   592
apply (rule_tac x="ys" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   593
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   594
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   595
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   596
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   597
lemmas ForallPForallQ =
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   598
  ForallPForallQ1 [THEN mp, OF conjI, OF _ allI, OF _ impI]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   599
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   600
lemma Forall_Conc_impl: "(Forall P x & Forall P y) --> Forall P (x @@ y)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   601
apply (rule_tac x="x" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   602
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   603
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   604
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   605
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   606
lemma Forall_Conc [simp]:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   607
  "Finite x ==> Forall P (x @@ y) = (Forall P x & Forall P y)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   608
apply (erule Seq_Finite_ind, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   609
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   610
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   611
lemma ForallTL1: "Forall P s  --> Forall P (TL$s)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   612
apply (rule_tac x="s" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   613
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   614
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   615
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   616
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   617
lemmas ForallTL = ForallTL1 [THEN mp]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   618
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   619
lemma ForallDropwhile1: "Forall P s  --> Forall P (Dropwhile Q$s)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   620
apply (rule_tac x="s" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   621
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   622
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   623
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   624
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   625
lemmas ForallDropwhile = ForallDropwhile1 [THEN mp]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   626
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   627
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   628
(* only admissible in t, not if done in s *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   629
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   630
lemma Forall_prefix: "! s. Forall P s --> t<<s --> Forall P t"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   631
apply (rule_tac x="t" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   632
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   633
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   634
apply (intro strip)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   635
apply (rule_tac x="sa" in Seq_cases)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   636
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   637
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   638
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   639
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   640
lemmas Forall_prefixclosed = Forall_prefix [rule_format]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   641
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   642
lemma Forall_postfixclosed:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   643
  "[| Finite h; Forall P s; s= h @@ t |] ==> Forall P t"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   644
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   645
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   646
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   647
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   648
lemma ForallPFilterQR1:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   649
  "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q$tr = Filter R$tr"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   650
apply (rule_tac x="tr" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   651
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   652
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   653
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   654
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   655
lemmas ForallPFilterQR = ForallPFilterQR1 [THEN mp, OF conjI, OF allI]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   656
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   657
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   658
(* ------------------------------------------------------------------------------------- *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   659
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   660
subsection "Forall, Filter"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   661
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   662
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   663
lemma ForallPFilterP: "Forall P (Filter P$x)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   664
apply (simp add: Filter_def Forall_def forallPsfilterP)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   665
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   666
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   667
(* holds also in other direction, then equal to forallPfilterP *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   668
lemma ForallPFilterPid1: "Forall P x --> Filter P$x = x"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   669
apply (rule_tac x="x" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   670
apply (simp add: Forall_def sforall_def Filter_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   671
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   672
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   673
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   674
lemmas ForallPFilterPid = ForallPFilterPid1 [THEN mp]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   675
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   676
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   677
(* holds also in other direction *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   678
lemma ForallnPFilterPnil1: "!! ys . Finite ys ==>
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   679
   Forall (%x. ~P x) ys --> Filter P$ys = nil "
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   680
apply (erule Seq_Finite_ind, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   681
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   682
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   683
lemmas ForallnPFilterPnil = ForallnPFilterPnil1 [THEN mp]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   684
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   685
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   686
(* holds also in other direction *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   687
lemma ForallnPFilterPUU1: "~Finite ys & Forall (%x. ~P x) ys \
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   688
\                  --> Filter P$ys = UU "
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   689
apply (rule_tac x="ys" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   690
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   691
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   692
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   693
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   694
lemmas ForallnPFilterPUU = ForallnPFilterPUU1 [THEN mp, OF conjI]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   695
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   696
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   697
(* inverse of ForallnPFilterPnil *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   698
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   699
lemma FilternPnilForallP1: "!! ys . Filter P$ys = nil -->
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   700
   (Forall (%x. ~P x) ys & Finite ys)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   701
apply (rule_tac x="ys" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   702
(* adm *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   703
apply (simp add: seq.compacts Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   704
(* base cases *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   705
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   706
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   707
(* main case *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   708
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   709
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   710
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   711
lemmas FilternPnilForallP = FilternPnilForallP1 [THEN mp]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   712
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   713
(* inverse of ForallnPFilterPUU. proved apply 2 lemmas because of adm problems *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   714
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   715
lemma FilterUU_nFinite_lemma1: "Finite ys ==> Filter P$ys ~= UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   716
apply (erule Seq_Finite_ind, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   717
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   718
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   719
lemma FilterUU_nFinite_lemma2: "~ Forall (%x. ~P x) ys --> Filter P$ys ~= UU"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   720
apply (rule_tac x="ys" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   721
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   722
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   723
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   724
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   725
lemma FilternPUUForallP:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   726
  "Filter P$ys = UU ==> (Forall (%x. ~P x) ys  & ~Finite ys)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   727
apply (rule conjI)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   728
apply (cut_tac FilterUU_nFinite_lemma2 [THEN mp, COMP rev_contrapos])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   729
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   730
apply (blast dest!: FilterUU_nFinite_lemma1)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   731
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   732
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   733
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   734
lemma ForallQFilterPnil:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   735
  "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   736
    ==> Filter P$ys = nil"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   737
apply (erule ForallnPFilterPnil)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   738
apply (erule ForallPForallQ)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   739
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   740
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   741
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   742
lemma ForallQFilterPUU:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   743
 "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   744
    ==> Filter P$ys = UU "
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   745
apply (erule ForallnPFilterPUU)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   746
apply (erule ForallPForallQ)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   747
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   748
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   749
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   750
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   751
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   752
(* ------------------------------------------------------------------------------------- *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   753
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   754
subsection "Takewhile, Forall, Filter"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   755
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   756
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   757
lemma ForallPTakewhileP [simp]: "Forall P (Takewhile P$x)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   758
apply (simp add: Forall_def Takewhile_def sforallPstakewhileP)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   759
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   760
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   761
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   762
lemma ForallPTakewhileQ [simp]:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   763
"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q$x)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   764
apply (rule ForallPForallQ)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   765
apply (rule ForallPTakewhileP)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   766
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   767
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   768
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   769
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   770
lemma FilterPTakewhileQnil [simp]:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   771
  "!! Q P.[| Finite (Takewhile Q$ys); !!x. Q x ==> ~P x |] \
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   772
\   ==> Filter P$(Takewhile Q$ys) = nil"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   773
apply (erule ForallnPFilterPnil)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   774
apply (rule ForallPForallQ)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   775
apply (rule ForallPTakewhileP)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   776
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   777
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   778
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   779
lemma FilterPTakewhileQid [simp]:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   780
 "!! Q P. [| !!x. Q x ==> P x |] ==> \
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   781
\            Filter P$(Takewhile Q$ys) = (Takewhile Q$ys)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   782
apply (rule ForallPFilterPid)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   783
apply (rule ForallPForallQ)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   784
apply (rule ForallPTakewhileP)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   785
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   786
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   787
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   788
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   789
lemma Takewhile_idempotent: "Takewhile P$(Takewhile P$s) = Takewhile P$s"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   790
apply (rule_tac x="s" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   791
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   792
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   793
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   794
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   795
lemma ForallPTakewhileQnP [simp]:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   796
 "Forall P s --> Takewhile (%x. Q x | (~P x))$s = Takewhile Q$s"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   797
apply (rule_tac x="s" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   798
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   799
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   800
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   801
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   802
lemma ForallPDropwhileQnP [simp]:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   803
 "Forall P s --> Dropwhile (%x. Q x | (~P x))$s = Dropwhile Q$s"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   804
apply (rule_tac x="s" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   805
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   806
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   807
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   808
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   809
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   810
lemma TakewhileConc1:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   811
 "Forall P s --> Takewhile P$(s @@ t) = s @@ (Takewhile P$t)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   812
apply (rule_tac x="s" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   813
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   814
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   815
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   816
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   817
lemmas TakewhileConc = TakewhileConc1 [THEN mp]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   818
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   819
lemma DropwhileConc1:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   820
 "Finite s ==> Forall P s --> Dropwhile P$(s @@ t) = Dropwhile P$t"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   821
apply (erule Seq_Finite_ind, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   822
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   823
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   824
lemmas DropwhileConc = DropwhileConc1 [THEN mp]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   825
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   826
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   827
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   828
(* ----------------------------------------------------------------------------------- *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   829
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   830
subsection "coinductive characterizations of Filter"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   831
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   832
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   833
lemma divide_Seq_lemma:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   834
 "HD$(Filter P$y) = Def x
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   835
    --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y))) 
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   836
             & Finite (Takewhile (%x. ~ P x)$y)  & P x"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   837
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   838
(* FIX: pay attention: is only admissible with chain-finite package to be added to
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   839
        adm test and Finite f x admissibility *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   840
apply (rule_tac x="y" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   841
apply (simp add: adm_subst [OF _ adm_Finite])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   842
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   843
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   844
apply (case_tac "P a")
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   845
 apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   846
 apply blast
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   847
(* ~ P a *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   848
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   849
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   850
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   851
lemma divide_Seq: "(x>>xs) << Filter P$y 
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   852
   ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y)))
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   853
      & Finite (Takewhile (%a. ~ P a)$y)  & P x"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   854
apply (rule divide_Seq_lemma [THEN mp])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   855
apply (drule_tac f="HD" and x="x>>xs" in  monofun_cfun_arg)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   856
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   857
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   858
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   859
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   860
lemma nForall_HDFilter:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   861
 "~Forall P y --> (? x. HD$(Filter (%a. ~P a)$y) = Def x)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   862
(* Pay attention: is only admissible with chain-finite package to be added to
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   863
        adm test *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   864
apply (rule_tac x="y" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   865
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   866
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   867
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   868
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   869
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   870
lemma divide_Seq2: "~Forall P y
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   871
  ==> ? x. y= (Takewhile P$y @@ (x >> TL$(Dropwhile P$y))) &
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   872
      Finite (Takewhile P$y) & (~ P x)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   873
apply (drule nForall_HDFilter [THEN mp])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   874
apply safe
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   875
apply (rule_tac x="x" in exI)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   876
apply (cut_tac P1="%x. ~ P x" in divide_Seq_lemma [THEN mp])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   877
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   878
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   879
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   880
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   881
lemma divide_Seq3: "~Forall P y
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   882
  ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   883
apply (drule divide_Seq2)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   884
(*Auto_tac no longer proves it*)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   885
apply fastsimp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   886
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   887
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   888
lemmas [simp] = FilterPQ FilterConc Conc_cong
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   889
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   890
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   891
(* ------------------------------------------------------------------------------------- *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   892
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   893
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   894
subsection "take_lemma"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   895
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   896
lemma seq_take_lemma: "(!n. seq_take n$x = seq_take n$x') = (x = x')"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   897
apply (rule iffI)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   898
apply (rule seq.take_lemmas)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   899
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   900
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   901
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   902
lemma take_reduction1:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   903
"  ! n. ((! k. k < n --> seq_take k$y1 = seq_take k$y2)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   904
    --> seq_take n$(x @@ (t>>y1)) =  seq_take n$(x @@ (t>>y2)))"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   905
apply (rule_tac x="x" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   906
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   907
apply (intro strip)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   908
apply (case_tac "n")
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   909
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   910
apply (case_tac "n")
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   911
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   912
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   913
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   914
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   915
lemma take_reduction:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   916
 "!! n.[| x=y; s=t; !! k. k<n ==> seq_take k$y1 = seq_take k$y2|]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   917
  ==> seq_take n$(x @@ (s>>y1)) =  seq_take n$(y @@ (t>>y2))"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   918
apply (auto intro!: take_reduction1 [rule_format])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   919
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   920
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   921
(* ------------------------------------------------------------------
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   922
          take-lemma and take_reduction for << instead of =
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   923
   ------------------------------------------------------------------ *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   924
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   925
lemma take_reduction_less1:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   926
"  ! n. ((! k. k < n --> seq_take k$y1 << seq_take k$y2)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   927
    --> seq_take n$(x @@ (t>>y1)) <<  seq_take n$(x @@ (t>>y2)))"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   928
apply (rule_tac x="x" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   929
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   930
apply (intro strip)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   931
apply (case_tac "n")
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   932
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   933
apply (case_tac "n")
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   934
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   935
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   936
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   937
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   938
lemma take_reduction_less:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   939
 "!! n.[| x=y; s=t;!! k. k<n ==> seq_take k$y1 << seq_take k$y2|]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   940
  ==> seq_take n$(x @@ (s>>y1)) <<  seq_take n$(y @@ (t>>y2))"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   941
apply (auto intro!: take_reduction_less1 [rule_format])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   942
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   943
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   944
lemma take_lemma_less1:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   945
  assumes "!! n. seq_take n$s1 << seq_take n$s2"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   946
  shows "s1<<s2"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   947
apply (rule_tac t="s1" in seq.reach [THEN subst])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   948
apply (rule_tac t="s2" in seq.reach [THEN subst])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   949
apply (rule fix_def2 [THEN ssubst])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   950
apply (subst contlub_cfun_fun)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   951
apply (rule chain_iterate)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   952
apply (subst contlub_cfun_fun)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   953
apply (rule chain_iterate)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   954
apply (rule lub_mono)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   955
apply (rule chain_iterate [THEN ch2ch_Rep_CFunL])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   956
apply (rule chain_iterate [THEN ch2ch_Rep_CFunL])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   957
apply (rule allI)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   958
apply (rule prems [unfolded seq.take_def])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   959
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   960
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   961
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   962
lemma take_lemma_less: "(!n. seq_take n$x << seq_take n$x') = (x << x')"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   963
apply (rule iffI)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   964
apply (rule take_lemma_less1)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   965
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   966
apply (erule monofun_cfun_arg)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   967
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   968
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   969
(* ------------------------------------------------------------------
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   970
          take-lemma proof principles
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   971
   ------------------------------------------------------------------ *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   972
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   973
lemma take_lemma_principle1:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   974
 "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   975
            !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   976
                          ==> (f (s1 @@ y>>s2)) = (g (s1 @@ y>>s2)) |]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   977
               ==> A x --> (f x)=(g x)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   978
apply (case_tac "Forall Q x")
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   979
apply (auto dest!: divide_Seq3)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   980
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   981
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   982
lemma take_lemma_principle2:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   983
  "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   984
           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   985
                          ==> ! n. seq_take n$(f (s1 @@ y>>s2))
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   986
                                 = seq_take n$(g (s1 @@ y>>s2)) |]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   987
               ==> A x --> (f x)=(g x)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   988
apply (case_tac "Forall Q x")
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   989
apply (auto dest!: divide_Seq3)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   990
apply (rule seq.take_lemmas)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   991
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   992
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   993
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   994
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   995
(* Note: in the following proofs the ordering of proof steps is very
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   996
         important, as otherwise either (Forall Q s1) would be in the IH as
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   997
         assumption (then rule useless) or it is not possible to strengthen
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   998
         the IH apply doing a forall closure of the sequence t (then rule also useless).
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
   999
         This is also the reason why the induction rule (nat_less_induct or nat_induct) has to
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1000
         to be imbuilt into the rule, as induction has to be done early and the take lemma
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1001
         has to be used in the trivial direction afterwards for the (Forall Q x) case.  *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1002
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1003
lemma take_lemma_induct:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1004
"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1005
         !! s1 s2 y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1006
                          Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1007
                          ==>   seq_take (Suc n)$(f (s1 @@ y>>s2))
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1008
                              = seq_take (Suc n)$(g (s1 @@ y>>s2)) |]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1009
               ==> A x --> (f x)=(g x)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1010
apply (rule impI)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1011
apply (rule seq.take_lemmas)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1012
apply (rule mp)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1013
prefer 2 apply assumption
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1014
apply (rule_tac x="x" in spec)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1015
apply (rule nat_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1016
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1017
apply (rule allI)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1018
apply (case_tac "Forall Q xa")
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1019
apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1020
apply (auto dest!: divide_Seq3)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1021
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1022
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1023
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1024
lemma take_lemma_less_induct:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1025
"!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ;
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1026
        !! s1 s2 y n. [| ! t m. m < n --> A t --> seq_take m$(f t) = seq_take m$(g t);
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1027
                          Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) |]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1028
                          ==>   seq_take n$(f (s1 @@ y>>s2))
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1029
                              = seq_take n$(g (s1 @@ y>>s2)) |]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1030
               ==> A x --> (f x)=(g x)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1031
apply (rule impI)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1032
apply (rule seq.take_lemmas)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1033
apply (rule mp)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1034
prefer 2 apply assumption
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1035
apply (rule_tac x="x" in spec)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1036
apply (rule nat_less_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1037
apply (rule allI)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1038
apply (case_tac "Forall Q xa")
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1039
apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1040
apply (auto dest!: divide_Seq3)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1041
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1042
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1043
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1044
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1045
lemma take_lemma_in_eq_out:
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1046
"!! Q. [| A UU  ==> (f UU) = (g UU) ;
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1047
          A nil ==> (f nil) = (g nil) ;
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1048
          !! s y n. [| ! t. A t --> seq_take n$(f t) = seq_take n$(g t);
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1049
                     A (y>>s) |]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1050
                     ==>   seq_take (Suc n)$(f (y>>s))
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1051
                         = seq_take (Suc n)$(g (y>>s)) |]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1052
               ==> A x --> (f x)=(g x)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1053
apply (rule impI)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1054
apply (rule seq.take_lemmas)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1055
apply (rule mp)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1056
prefer 2 apply assumption
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1057
apply (rule_tac x="x" in spec)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1058
apply (rule nat_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1059
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1060
apply (rule allI)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1061
apply (rule_tac x="xa" in Seq_cases)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1062
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1063
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1064
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1065
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1066
(* ------------------------------------------------------------------------------------ *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1067
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1068
subsection "alternative take_lemma proofs"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1069
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1070
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1071
(* --------------------------------------------------------------- *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1072
(*              Alternative Proof of FilterPQ                      *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1073
(* --------------------------------------------------------------- *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1074
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1075
declare FilterPQ [simp del]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1076
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1077
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1078
(* In general: How to do this case without the same adm problems
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1079
   as for the entire proof ? *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1080
lemma Filter_lemma1: "Forall (%x.~(P x & Q x)) s
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1081
          --> Filter P$(Filter Q$s) =
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1082
              Filter (%x. P x & Q x)$s"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1083
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1084
apply (rule_tac x="s" in Seq_induct)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1085
apply (simp add: Forall_def sforall_def)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1086
apply simp_all
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1087
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1088
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1089
lemma Filter_lemma2: "Finite s ==>
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1090
          (Forall (%x. (~P x) | (~ Q x)) s
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1091
          --> Filter P$(Filter Q$s) = nil)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1092
apply (erule Seq_Finite_ind, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1093
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1094
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1095
lemma Filter_lemma3: "Finite s ==>
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1096
          Forall (%x. (~P x) | (~ Q x)) s
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1097
          --> Filter (%x. P x & Q x)$s = nil"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1098
apply (erule Seq_Finite_ind, simp_all)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1099
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1100
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1101
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1102
lemma FilterPQ_takelemma: "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1103
apply (rule_tac A1="%x. True" and
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1104
                 Q1="%x.~(P x & Q x)" and x1="s" in
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1105
                 take_lemma_induct [THEN mp])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1106
(* better support for A = %x. True *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1107
apply (simp add: Filter_lemma1)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1108
apply (simp add: Filter_lemma2 Filter_lemma3)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1109
apply simp
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1110
done
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1111
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1112
declare FilterPQ [simp]
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1113
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1114
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1115
(* --------------------------------------------------------------- *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1116
(*              Alternative Proof of MapConc                       *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1117
(* --------------------------------------------------------------- *)
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1118
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1119
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1120
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1121
lemma MapConc_takelemma: "Map f$(x@@y) = (Map f$x) @@ (Map f$y)"
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1122
apply (rule_tac A1="%x. True" and x1="x" in
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1123
    take_lemma_in_eq_out [THEN mp])
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1124
apply auto
4103954f3668 converted to isar theory; removed unsound adm_all axiom
huffman
parents: 17233
diff changeset
  1125
done
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
  1126
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1127
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1128
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1129
ML {*
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1130
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1131
local
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1132
  val Seq_cases = thm "Seq_cases"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1133
  val Seq_induct = thm "Seq_induct"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1134
  val Seq_Finite_ind = thm "Seq_Finite_ind"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1135
in
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1136
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1137
fun Seq_case_tac s i = res_inst_tac [("x",s)] Seq_cases i
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1138
          THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1139
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1140
(* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1141
fun Seq_case_simp_tac s i = Seq_case_tac s i THEN SIMPSET' asm_simp_tac (i+2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1142
                                             THEN SIMPSET' asm_full_simp_tac (i+1)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1143
                                             THEN SIMPSET' asm_full_simp_tac i;
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1144
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1145
(* rws are definitions to be unfolded for admissibility check *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1146
fun Seq_induct_tac s rws i = res_inst_tac [("x",s)] Seq_induct i
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1147
                         THEN (REPEAT_DETERM (CHANGED (SIMPSET' asm_simp_tac (i+1))))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1148
                         THEN SIMPSET' (fn ss => simp_tac (ss addsimps rws)) i;
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1149
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1150
fun Seq_Finite_induct_tac i = etac Seq_Finite_ind i
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1151
                              THEN (REPEAT_DETERM (CHANGED (SIMPSET' asm_simp_tac i)));
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1152
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1153
fun pair_tac s = res_inst_tac [("p",s)] PairE
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1154
                          THEN' hyp_subst_tac THEN' SIMPSET' asm_full_simp_tac;
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1155
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1156
(* induction on a sequence of pairs with pairsplitting and simplification *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1157
fun pair_induct_tac s rws i =
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1158
           res_inst_tac [("x",s)] Seq_induct i
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1159
           THEN pair_tac "a" (i+3)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1160
           THEN (REPEAT_DETERM (CHANGED (SIMPSET' simp_tac (i+1))))
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1161
           THEN SIMPSET' (fn ss => simp_tac (ss addsimps rws)) i;
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
  1162
12338
de0f4a63baa5 renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents: 12218
diff changeset
  1163
end
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1164
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1165
*}
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1166
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1167
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 19551
diff changeset
  1168
end