src/HOL/Eisbach/Tests.thy
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (22 months ago)
changeset 66924 b4d4027f743b
parent 63186 dc221b8945f2
child 69216 1a52baa70aed
permissions -rw-r--r--
more permissive;
wenzelm@60248
     1
(*  Title:      HOL/Eisbach/Tests.thy
wenzelm@60119
     2
    Author:     Daniel Matichuk, NICTA/UNSW
wenzelm@60119
     3
*)
wenzelm@60119
     4
wenzelm@60119
     5
section \<open>Miscellaneous Eisbach tests\<close>
wenzelm@60119
     6
wenzelm@60119
     7
theory Tests
wenzelm@60119
     8
imports Main Eisbach_Tools
wenzelm@60119
     9
begin
wenzelm@60119
    10
wenzelm@60209
    11
wenzelm@60285
    12
subsection \<open>Named Theorems Tests\<close>
wenzelm@60119
    13
wenzelm@60119
    14
named_theorems foo
wenzelm@60119
    15
wenzelm@60209
    16
method foo declares foo = (rule foo)
wenzelm@60119
    17
wenzelm@60119
    18
lemma
wenzelm@60119
    19
  assumes A [foo]: A
wenzelm@60119
    20
  shows A
wenzelm@60119
    21
  apply foo
wenzelm@60119
    22
  done
wenzelm@60119
    23
wenzelm@61912
    24
method abs_used for P = (match (P) in "\<lambda>a. ?Q" \<Rightarrow> fail \<bar> _ \<Rightarrow> -)
wenzelm@60119
    25
wenzelm@60285
    26
wenzelm@60285
    27
subsection \<open>Match Tests\<close>
wenzelm@60119
    28
wenzelm@60119
    29
notepad
wenzelm@60119
    30
begin
wenzelm@60119
    31
  have dup: "\<And>A. A \<Longrightarrow> A \<Longrightarrow> A" by simp
wenzelm@60119
    32
wenzelm@60119
    33
  fix A y
wenzelm@60119
    34
  have "(\<And>x. A x) \<Longrightarrow> A y"
wenzelm@60209
    35
    apply (rule dup, match premises in Y: "\<And>B. P B" for P \<Rightarrow> \<open>match (P) in A \<Rightarrow> \<open>print_fact Y, rule Y\<close>\<close>)
wenzelm@60209
    36
    apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match (P) in A \<Rightarrow> \<open>print_fact Y, rule Y\<close>\<close>)
wenzelm@60209
    37
    apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match conclusion in "P y" for y \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=y]\<close>\<close>)
wenzelm@60209
    38
    apply (rule dup, match premises in Y: "\<And>B :: 'a. P B" for P \<Rightarrow> \<open>match conclusion in "P z" for z \<Rightarrow> \<open>print_fact Y, print_term y, rule Y[where B=z]\<close>\<close>)
wenzelm@60209
    39
    apply (rule dup, match conclusion in "P y" for P \<Rightarrow> \<open>match premises in Y: "\<And>z. P z" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
wenzelm@60209
    40
    apply (match premises in Y: "\<And>z :: 'a. P z" for P \<Rightarrow> \<open>match conclusion in "P y" \<Rightarrow> \<open>print_fact Y, rule Y[where z=y]\<close>\<close>)
wenzelm@60119
    41
    done
wenzelm@60119
    42
wenzelm@60119
    43
  assume X: "\<And>x. A x" "A y"
wenzelm@60119
    44
  have "A y"
wenzelm@60119
    45
    apply (match X in Y:"\<And>B. A B" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y[where B=y], print_term B\<close>)
wenzelm@60119
    46
    apply (match X in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
wenzelm@60119
    47
    apply (match X in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B, print_term x\<close>)
wenzelm@60119
    48
    apply (insert X)
wenzelm@60209
    49
    apply (match premises in Y:"\<And>B. A B" and Y':"B y" for B and y :: 'a \<Rightarrow> \<open>print_fact Y[where B=y], print_term B\<close>)
wenzelm@60209
    50
    apply (match premises in Y:"B ?x" and Y':"B ?x" for B \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
wenzelm@60209
    51
    apply (match premises in Y:"B x" and Y':"B x" for B x \<Rightarrow> \<open>print_fact Y, print_term B\<close>)
wenzelm@60209
    52
    apply (match conclusion in "P x" and "P y" for P x \<Rightarrow> \<open>print_term P, print_term x\<close>)
wenzelm@60119
    53
    apply assumption
wenzelm@60119
    54
    done
wenzelm@60119
    55
wenzelm@60209
    56
  {
wenzelm@60209
    57
   fix B x y
wenzelm@60209
    58
   assume X: "\<And>x y. B x x y"
wenzelm@60209
    59
   have "B x x y"
wenzelm@60209
    60
     by (match X in Y:"\<And>y. B y y z" for z \<Rightarrow> \<open>rule Y[where y=x]\<close>)
wenzelm@60209
    61
wenzelm@60209
    62
   fix A B
wenzelm@60209
    63
   have "(\<And>x y. A (B x) y) \<Longrightarrow> A (B x) y"
wenzelm@60209
    64
     by (match premises in Y: "\<And>xx. ?H (B xx)" \<Rightarrow> \<open>rule Y\<close>)
wenzelm@60209
    65
  }
wenzelm@60209
    66
wenzelm@60119
    67
  (* match focusing retains prems *)
wenzelm@60119
    68
  fix B x
wenzelm@60119
    69
  have "(\<And>x. A x) \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x"
wenzelm@60209
    70
    apply (match premises in Y: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>match premises in Y': "\<And>z :: 'b. B z" \<Rightarrow> \<open>print_fact Y, print_fact Y', rule Y'[where z=x]\<close>\<close>)
wenzelm@60119
    71
    done
wenzelm@60119
    72
wenzelm@60119
    73
  (*Attributes *)
wenzelm@60119
    74
  fix C
wenzelm@60119
    75
  have "(\<And>x :: 'a. A x)  \<Longrightarrow> (\<And>z. B z) \<Longrightarrow> A y \<Longrightarrow> B x \<and> B x \<and> A y"
wenzelm@60119
    76
    apply (intro conjI)
wenzelm@61912
    77
    apply (match premises in Y: "\<And>z :: 'a. A z" and Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> fastforce)
wenzelm@61912
    78
    apply (match premises in Y: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>match premises in Y'[intro]:"\<And>z :: 'b. B z" \<Rightarrow> fastforce\<close>)
wenzelm@60285
    79
    apply (match premises in Y[thin]: "\<And>z :: 'a. A z"  \<Rightarrow> \<open>(match premises in Y':"\<And>z :: 'a. A z" \<Rightarrow> \<open>print_fact Y,fail\<close> \<bar> _ \<Rightarrow> \<open>print_fact Y\<close>)\<close>)
wenzelm@61912
    80
    (*apply (match premises in Y: "\<And>z :: 'b. B z"  \<Rightarrow> \<open>(match premises in Y'[thin]:"\<And>z :: 'b. B z" \<Rightarrow> \<open>(match premises in Y':"\<And>z :: 'a. A z" \<Rightarrow> fail \<bar> Y': _ \<Rightarrow> -)\<close>)\<close>)*)
wenzelm@60119
    81
    apply assumption
wenzelm@60119
    82
    done
wenzelm@60119
    83
wenzelm@60119
    84
  fix A B C D
wenzelm@60119
    85
  have "\<And>uu'' uu''' uu uu'. (\<And>x :: 'a. A uu' x)  \<Longrightarrow> D uu y \<Longrightarrow> (\<And>z. B uu z) \<Longrightarrow> C uu y \<Longrightarrow> (\<And>z y. C uu z)  \<Longrightarrow> B uu x \<and> B uu x \<and> C uu y"
wenzelm@60209
    86
    apply (match premises in Y[thin]: "\<And>z :: 'a. A ?zz' z" and
wenzelm@60119
    87
                          Y'[thin]: "\<And>rr :: 'b. B ?zz rr" \<Rightarrow>
wenzelm@60119
    88
          \<open>print_fact Y, print_fact Y', intro conjI, rule Y', insert Y', insert Y'[where rr=x]\<close>)
wenzelm@60209
    89
    apply (match premises in Y:"B ?u ?x" \<Rightarrow> \<open>rule Y\<close>)
wenzelm@60119
    90
    apply (insert TrueI)
wenzelm@60209
    91
    apply (match premises in Y'[thin]: "\<And>ff. B uu ff" for uu \<Rightarrow> \<open>insert Y', drule meta_spec[where x=x]\<close>)
wenzelm@60119
    92
    apply assumption
wenzelm@60119
    93
    done
wenzelm@60119
    94
wenzelm@60119
    95
wenzelm@60119
    96
  (* Multi-matches. As many facts as match are bound. *)
wenzelm@60119
    97
  fix A B C x
wenzelm@60119
    98
  have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
wenzelm@60209
    99
    apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
wenzelm@61912
   100
    apply (match premises in Y[thin]: "\<And>z :: 'a. ?A z" (multi) \<Rightarrow> fail \<bar> "C y" \<Rightarrow> -) (* multi-match must bind something *)
wenzelm@60209
   101
    apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
wenzelm@60119
   102
    done
wenzelm@60119
   103
wenzelm@60119
   104
  fix A B C x
wenzelm@60119
   105
  have "(\<And>x :: 'a. A x) \<Longrightarrow> (\<And>y :: 'a. B y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
wenzelm@60209
   106
    apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> \<open>intro conjI, (rule Y)+\<close>)
wenzelm@61912
   107
    apply (match premises in Y[thin]: "\<And>z. ?A z" (multi) \<Rightarrow> fail \<bar> "C y" \<Rightarrow> -) (* multi-match must bind something *)
wenzelm@60209
   108
    apply (match premises in Y: "C y" \<Rightarrow> \<open>rule Y\<close>)
wenzelm@60119
   109
    done
wenzelm@60119
   110
wenzelm@60285
   111
  fix A B C P Q and x :: 'a and y :: 'a
wenzelm@60285
   112
  have "(\<And>x y :: 'a. A x y \<and> Q) \<Longrightarrow> (\<And>a b. B (a :: 'a) (b :: 'a) \<and> Q) \<Longrightarrow> (\<And>x y. C (x :: 'a) (y :: 'a) \<and> P) \<Longrightarrow> A y x \<and> B y x"
wenzelm@60285
   113
    by (match premises in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule conjI, rule Y[where z=x,THEN conjunct1], rule Y[THEN conjunct1]\<close>)
wenzelm@60285
   114
wenzelm@60119
   115
wenzelm@60119
   116
  (*We may use for-fixes in multi-matches too. All bound facts must agree on the fixed term *)
wenzelm@60119
   117
  fix A B C x
wenzelm@60119
   118
  have "(\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> (\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
wenzelm@60285
   119
    apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow>
wenzelm@61912
   120
                                  \<open>match (P) in B \<Rightarrow> fail
wenzelm@61912
   121
                                        \<bar> "\<lambda>a. B" \<Rightarrow> fail
wenzelm@61912
   122
                                        \<bar> _ \<Rightarrow> -,
wenzelm@60285
   123
                                  intro conjI, (rule Y[THEN conjunct1])\<close>)
wenzelm@60285
   124
    apply (rule dup)
wenzelm@60285
   125
    apply (match premises in Y':"\<And>x :: 'a. ?U x \<and> Q x" and Y: "\<And>x :: 'a. Q x \<and> ?U x" (multi)  for Q \<Rightarrow> \<open>insert Y[THEN conjunct1]\<close>)
wenzelm@60285
   126
    apply assumption (* Previous match requires that Q is consistent *)
wenzelm@60209
   127
    apply (match premises in Y: "\<And>z :: 'a. ?A z \<longrightarrow> False" (multi) \<Rightarrow> \<open>print_fact Y, fail\<close> \<bar> "C y" \<Rightarrow> \<open>print_term C\<close>) (* multi-match must bind something *)
wenzelm@60209
   128
    apply (match premises in Y: "\<And>x. B x \<and> C x" \<Rightarrow> \<open>intro conjI Y[THEN conjunct1]\<close>)
wenzelm@60209
   129
    apply (match premises in Y: "C ?x" \<Rightarrow> \<open>rule Y\<close>)
wenzelm@60119
   130
    done
wenzelm@60119
   131
wenzelm@60285
   132
  (* All bindings must be tried for a particular theorem.
wenzelm@60285
   133
     However all combinations are NOT explored. *)
wenzelm@60285
   134
  fix B A C
wenzelm@60285
   135
  assume asms:"\<And>a b. B (a :: 'a) (b :: 'a) \<and> Q" "\<And>x :: 'a. A x x \<and> Q" "\<And>a b. C (a :: 'a) (b :: 'a) \<and> Q"
wenzelm@60285
   136
  have "B y x \<and> C x y \<and> B x y \<and> C y x \<and> A x x"
wenzelm@60285
   137
    apply (intro conjI)
wenzelm@60285
   138
    apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where z=x,THEN conjunct1]\<close>)
wenzelm@60285
   139
    apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where a=x,THEN conjunct1]\<close>)
wenzelm@60285
   140
    apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where a=x,THEN conjunct1]\<close>)
wenzelm@60285
   141
    apply (match asms in Y: "\<And>z a. ?A (z :: 'a) (a :: 'a) \<and> R" (multi) for R \<Rightarrow> \<open>rule Y[where z=x,THEN conjunct1]\<close>)
wenzelm@61912
   142
    apply (match asms in Y: "\<And>z a. A (z :: 'a) (a :: 'a) \<and> R"  for R \<Rightarrow> fail \<bar> _ \<Rightarrow> -)
wenzelm@60285
   143
    apply (rule asms[THEN conjunct1])
wenzelm@60285
   144
    done
wenzelm@60285
   145
wenzelm@60119
   146
  (* Attributes *)
wenzelm@60119
   147
  fix A B C x
wenzelm@60119
   148
  have "(\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> (\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
wenzelm@60209
   149
    apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match Y[THEN conjunct1]  in Y':"?H"  (multi) \<Rightarrow> \<open>intro conjI,rule Y'\<close>\<close>)
wenzelm@60209
   150
    apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match Y[THEN conjunct2]  in Y':"?H"  (multi) \<Rightarrow> \<open>rule Y'\<close>\<close>)
wenzelm@60119
   151
    apply assumption
wenzelm@60119
   152
    done
wenzelm@60119
   153
wenzelm@60119
   154
(* Removed feature for now *)
wenzelm@60119
   155
(*
wenzelm@60119
   156
  fix A B C x
wenzelm@60119
   157
  have "(\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> (\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
wenzelm@60119
   158
  apply (match prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match \<open>K @{thms Y TrueI}\<close> in Y':"?H"  (multi) \<Rightarrow> \<open>rule conjI; (rule Y')?\<close>\<close>)
wenzelm@60119
   159
  apply (match prems in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>match \<open>K [@{thm Y}]\<close> in Y':"?H"  (multi) \<Rightarrow> \<open>rule Y'\<close>\<close>)
wenzelm@60119
   160
  done
wenzelm@60119
   161
*)
wenzelm@60119
   162
  (* Testing THEN_ALL_NEW within match *)
wenzelm@60119
   163
  fix A B C x
wenzelm@60119
   164
  have "(\<And>x :: 'a. A x \<and> B x) \<Longrightarrow> (\<And>y :: 'a. A y \<and> C y) \<Longrightarrow> (\<And>y :: 'a. B y \<and> C y) \<Longrightarrow> C y \<Longrightarrow> (A x \<and> B y \<and> C y)"
wenzelm@60209
   165
    apply (match premises in Y: "\<And>x :: 'a. P x \<and> ?U x" (multi) for P \<Rightarrow> \<open>intro conjI ; ((rule Y[THEN conjunct1])?); rule Y[THEN conjunct2] \<close>)
wenzelm@60119
   166
    done
wenzelm@60119
   167
wenzelm@60119
   168
  (* Cut tests *)
wenzelm@60119
   169
  fix A B C
wenzelm@60119
   170
wenzelm@60119
   171
  have "D \<and> C  \<Longrightarrow> A \<and> B  \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C"
wenzelm@60209
   172
    by (((match premises in I: "P \<and> Q" (cut)
wenzelm@60119
   173
              and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?), simp)
wenzelm@60119
   174
wenzelm@60285
   175
  have "D \<and> C  \<Longrightarrow> A \<and> B  \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> D \<longrightarrow> True \<Longrightarrow> C"
wenzelm@60285
   176
    by (match premises in I: "P \<and> Q" (cut 2)
wenzelm@60285
   177
              and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)
wenzelm@60285
   178
wenzelm@60119
   179
  have "A \<and> B \<Longrightarrow> A \<longrightarrow> C \<Longrightarrow> C"
wenzelm@60209
   180
    by (((match premises in I: "P \<and> Q" (cut)
wenzelm@60119
   181
              and I': "P \<longrightarrow> ?U" for P Q \<Rightarrow> \<open>rule mp [OF I' I[THEN conjunct1]]\<close>)?, simp) | simp)
wenzelm@60119
   182
wenzelm@60209
   183
  fix f x y
wenzelm@60209
   184
  have "f x y \<Longrightarrow> f x y"
wenzelm@60209
   185
    by (match conclusion in "f x y" for f x y  \<Rightarrow> \<open>print_term f\<close>)
wenzelm@60209
   186
wenzelm@60209
   187
  fix A B C
wenzelm@60209
   188
  assume X: "A \<and> B" "A \<and> C" C
wenzelm@60209
   189
  have "A \<and> B \<and> C"
wenzelm@60285
   190
    by (match X in H: "A \<and> ?H" (multi, cut) \<Rightarrow>
wenzelm@61912
   191
          \<open>match H in "A \<and> C" and "A \<and> B" \<Rightarrow> fail\<close>
wenzelm@60209
   192
        | simp add: X)
wenzelm@60209
   193
wenzelm@60285
   194
wenzelm@60285
   195
  (* Thinning an inner focus *)
wenzelm@60285
   196
  (* Thinning should persist within a match, even when on an external premise *)
wenzelm@60285
   197
wenzelm@60285
   198
  fix A
wenzelm@60285
   199
  have "(\<And>x. A x \<and> B) \<Longrightarrow> B \<and> C \<Longrightarrow> C"
wenzelm@60285
   200
    apply (match premises in H:"\<And>x. A x \<and> B" \<Rightarrow>
wenzelm@60285
   201
                     \<open>match premises in H'[thin]: "\<And>x. A x \<and> B" \<Rightarrow>
wenzelm@61912
   202
                      \<open>match premises in H'':"\<And>x. A x \<and> B" \<Rightarrow> fail
wenzelm@61912
   203
                                         \<bar> _ \<Rightarrow> -\<close>
wenzelm@61912
   204
                      ,match premises in H'':"\<And>x. A x \<and> B" \<Rightarrow> fail \<bar> _ \<Rightarrow> -\<close>)
wenzelm@61912
   205
    apply (match premises in H:"\<And>x. A x \<and> B" \<Rightarrow> fail
wenzelm@60285
   206
                              \<bar> H':_ \<Rightarrow> \<open>rule H'[THEN conjunct2]\<close>)
wenzelm@60285
   207
    done
wenzelm@60285
   208
wenzelm@60285
   209
wenzelm@60285
   210
  (* Local premises *)
wenzelm@60285
   211
  (* Only match premises which actually existed in the goal we just focused.*)
wenzelm@60285
   212
wenzelm@60285
   213
  fix A
wenzelm@60285
   214
  assume asms: "C \<and> D"
wenzelm@60285
   215
  have "B \<and> C \<Longrightarrow> C"
wenzelm@60285
   216
    by (match premises in _ \<Rightarrow> \<open>insert asms,
wenzelm@61912
   217
            match premises (local) in "B \<and> C" \<Rightarrow> fail
wenzelm@60285
   218
                                  \<bar> H:"C \<and> D" \<Rightarrow> \<open>rule H[THEN conjunct1]\<close>\<close>)
wenzelm@60119
   219
end
wenzelm@60119
   220
wenzelm@60248
   221
wenzelm@60285
   222
wenzelm@60119
   223
(* Testing inner focusing. This fails if we don't smash flex-flex pairs produced
wenzelm@60119
   224
   by retrofitting. This needs to be done more carefully to avoid smashing
wenzelm@60119
   225
   legitimate pairs.*)
wenzelm@60119
   226
wenzelm@61337
   227
schematic_goal "?A x \<Longrightarrow> A x"
wenzelm@60209
   228
  apply (match conclusion in "H" for H \<Rightarrow> \<open>match conclusion in Y for Y \<Rightarrow> \<open>print_term Y\<close>\<close>)
wenzelm@60119
   229
  apply assumption
wenzelm@60119
   230
  done
wenzelm@60119
   231
wenzelm@60119
   232
(* Ensure short-circuit after first match failure *)
wenzelm@60119
   233
lemma
wenzelm@60119
   234
  assumes A: "P \<and> Q"
wenzelm@60119
   235
  shows "P"
wenzelm@61912
   236
  by ((match A in "P \<and> Q" \<Rightarrow> fail \<bar> "?H" \<Rightarrow> -) | simp add: A)
wenzelm@60119
   237
wenzelm@60119
   238
lemma
wenzelm@60119
   239
  assumes A: "D \<and> C" "A \<and> B" "A \<longrightarrow> B"
wenzelm@60119
   240
  shows "A"
wenzelm@60119
   241
  apply ((match A in U: "P \<and> Q" (cut) and "P' \<longrightarrow> Q'" for P Q P' Q' \<Rightarrow>
wenzelm@61912
   242
      \<open>simp add: U\<close> \<bar> "?H" \<Rightarrow> -) | -)
wenzelm@60119
   243
  apply (simp add: A)
wenzelm@60119
   244
  done
wenzelm@60119
   245
wenzelm@60119
   246
wenzelm@60119
   247
subsection \<open>Uses Tests\<close>
wenzelm@60119
   248
wenzelm@60119
   249
ML \<open>
wenzelm@60119
   250
  fun test_internal_fact ctxt factnm =
wenzelm@60119
   251
    (case try (Proof_Context.get_thms ctxt) factnm of
wenzelm@60119
   252
      NONE => ()
wenzelm@60285
   253
    | SOME _ => error "Found internal fact");
wenzelm@60285
   254
\<close>
wenzelm@60119
   255
wenzelm@60209
   256
method uses_test\<^sub>1 uses uses_test\<^sub>1_uses = (rule uses_test\<^sub>1_uses)
wenzelm@60119
   257
wenzelm@60119
   258
lemma assumes A shows A by (uses_test\<^sub>1 uses_test\<^sub>1_uses: assms)
wenzelm@60119
   259
wenzelm@60119
   260
ML \<open>test_internal_fact @{context} "uses_test\<^sub>1_uses"\<close>
wenzelm@60119
   261
wenzelm@60119
   262
ML \<open>test_internal_fact @{context} "Tests.uses_test\<^sub>1_uses"\<close>
wenzelm@60119
   263
ML \<open>test_internal_fact @{context} "Tests.uses_test\<^sub>1.uses_test\<^sub>1_uses"\<close>
wenzelm@60119
   264
daniel@63185
   265
subsection \<open>Basic fact passing\<close>
daniel@63185
   266
daniel@63185
   267
method find_fact for x y :: bool uses facts1 facts2 =
daniel@63185
   268
  (match facts1 in U: "x" \<Rightarrow> \<open>insert U,
daniel@63185
   269
      match facts2 in U: "y" \<Rightarrow> \<open>insert U\<close>\<close>)
daniel@63185
   270
daniel@63185
   271
lemma assumes A: A and B: B shows "A \<and> B"
daniel@63185
   272
  apply (find_fact "A" "B" facts1: A facts2: B)
daniel@63185
   273
  apply (rule conjI; assumption)
daniel@63185
   274
  done
daniel@63185
   275
wenzelm@60119
   276
wenzelm@60285
   277
subsection \<open>Testing term and fact passing in recursion\<close>
wenzelm@60119
   278
daniel@63185
   279
wenzelm@60119
   280
method recursion_example for x :: bool uses facts =
wenzelm@60209
   281
  (match (x) in
wenzelm@60119
   282
    "A \<and> B" for A B \<Rightarrow> \<open>(recursion_example A facts: facts, recursion_example B facts: facts)\<close>
wenzelm@60209
   283
  \<bar> "?H" \<Rightarrow> \<open>match facts in U: "x" \<Rightarrow> \<open>insert U\<close>\<close>)
wenzelm@60119
   284
wenzelm@60119
   285
lemma
wenzelm@60119
   286
  assumes asms: "A" "B" "C" "D"
wenzelm@60119
   287
  shows "(A \<and> B) \<and> (C \<and> D)"
wenzelm@60119
   288
  apply (recursion_example "(A \<and> B) \<and> (C \<and> D)" facts: asms)
wenzelm@60119
   289
  apply simp
wenzelm@60119
   290
  done
wenzelm@60119
   291
wenzelm@60285
   292
(* uses facts are not accumulated *)
wenzelm@60285
   293
wenzelm@60285
   294
method recursion_example' for A :: bool and B :: bool uses facts =
wenzelm@60285
   295
  (match facts in
wenzelm@60285
   296
    H: "A" and H': "B" \<Rightarrow> \<open>recursion_example' "A" "B" facts: H TrueI\<close>
wenzelm@60285
   297
  \<bar> "A" and "True" \<Rightarrow> \<open>recursion_example' "A" "B" facts: TrueI\<close>
wenzelm@61912
   298
  \<bar> "True" \<Rightarrow> -
wenzelm@61912
   299
  \<bar> "PROP ?P" \<Rightarrow> fail)
wenzelm@60285
   300
wenzelm@60285
   301
lemma
wenzelm@60285
   302
  assumes asms: "A" "B"
wenzelm@60285
   303
  shows "True"
wenzelm@60285
   304
  apply (recursion_example' "A" "B" facts: asms)
wenzelm@60285
   305
  apply simp
wenzelm@60285
   306
  done
wenzelm@60285
   307
wenzelm@60285
   308
wenzelm@60119
   309
(*Method.sections in existing method*)
wenzelm@60209
   310
method my_simp\<^sub>1 uses my_simp\<^sub>1_facts = (simp add: my_simp\<^sub>1_facts)
wenzelm@60119
   311
lemma assumes A shows A by (my_simp\<^sub>1 my_simp\<^sub>1_facts: assms)
wenzelm@60119
   312
wenzelm@60119
   313
(*Method.sections via Eisbach argument parser*)
wenzelm@60209
   314
method uses_test\<^sub>2 uses uses_test\<^sub>2_uses = (uses_test\<^sub>1 uses_test\<^sub>1_uses: uses_test\<^sub>2_uses)
wenzelm@60119
   315
lemma assumes A shows A by (uses_test\<^sub>2 uses_test\<^sub>2_uses: assms)
wenzelm@60119
   316
wenzelm@60119
   317
wenzelm@60119
   318
subsection \<open>Declaration Tests\<close>
wenzelm@60119
   319
wenzelm@60119
   320
named_theorems declare_facts\<^sub>1
wenzelm@60119
   321
wenzelm@60209
   322
method declares_test\<^sub>1 declares declare_facts\<^sub>1 = (rule declare_facts\<^sub>1)
wenzelm@60119
   323
wenzelm@60119
   324
lemma assumes A shows A by (declares_test\<^sub>1 declare_facts\<^sub>1: assms)
wenzelm@60119
   325
wenzelm@60119
   326
lemma assumes A[declare_facts\<^sub>1]: A shows A by declares_test\<^sub>1
wenzelm@60119
   327
wenzelm@60119
   328
wenzelm@60119
   329
subsection \<open>Rule Instantiation Tests\<close>
wenzelm@60119
   330
wenzelm@60119
   331
method my_allE\<^sub>1 for x :: 'a and P :: "'a \<Rightarrow> bool" =
wenzelm@60209
   332
  (erule allE [where x = x and P = P])
wenzelm@60119
   333
wenzelm@60119
   334
lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>1 x Q)
wenzelm@60119
   335
wenzelm@60119
   336
method my_allE\<^sub>2 for x :: 'a and P :: "'a \<Rightarrow> bool" =
wenzelm@60209
   337
  (erule allE [of P x])
wenzelm@60119
   338
wenzelm@60119
   339
lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>2 x Q)
wenzelm@60119
   340
wenzelm@60119
   341
method my_allE\<^sub>3 for x :: 'a and P :: "'a \<Rightarrow> bool" =
wenzelm@60209
   342
  (match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow>
wenzelm@60209
   343
    \<open>erule X [where x = x and P = P]\<close>)
wenzelm@60119
   344
wenzelm@60119
   345
lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>3 x Q)
wenzelm@60119
   346
wenzelm@60119
   347
method my_allE\<^sub>4 for x :: 'a and P :: "'a \<Rightarrow> bool" =
wenzelm@60209
   348
  (match allE [where 'a = 'a] in X: "\<And>(x :: 'a) P R. \<forall>x. P x \<Longrightarrow> (P x \<Longrightarrow> R) \<Longrightarrow> R" \<Rightarrow>
wenzelm@60209
   349
    \<open>erule X [of x P]\<close>)
wenzelm@60119
   350
wenzelm@60119
   351
lemma "\<forall>x. Q x \<Longrightarrow> Q x" by (my_allE\<^sub>4 x Q)
wenzelm@60119
   352
wenzelm@60119
   353
wenzelm@60209
   354
wenzelm@60285
   355
subsection \<open>Polymorphism test\<close>
wenzelm@60209
   356
wenzelm@60209
   357
axiomatization foo' :: "'a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> bool"
wenzelm@60209
   358
axiomatization where foo'_ax1: "foo' x y z \<Longrightarrow> z \<and> y"
wenzelm@60209
   359
axiomatization where foo'_ax2: "foo' x y y \<Longrightarrow> x \<and> z"
wenzelm@60285
   360
axiomatization where foo'_ax3: "foo' (x :: int) y y \<Longrightarrow> y \<and> y"
wenzelm@60209
   361
wenzelm@60285
   362
lemmas my_thms = foo'_ax1 foo'_ax2 foo'_ax3
wenzelm@60209
   363
wenzelm@60209
   364
definition first_id where "first_id x = x"
wenzelm@60209
   365
wenzelm@60209
   366
lemmas my_thms' = my_thms[of "first_id x" for x]
wenzelm@60209
   367
wenzelm@60209
   368
method print_conclusion = (match conclusion in concl for concl \<Rightarrow> \<open>print_term concl\<close>)
wenzelm@60209
   369
wenzelm@60209
   370
lemma
wenzelm@60209
   371
  assumes foo: "\<And>x (y :: bool). foo' (A x) B (A x)"
wenzelm@60209
   372
  shows "\<And>z. A z \<and> B"
wenzelm@60209
   373
  apply
wenzelm@60209
   374
    (match conclusion in "f x y" for f y and x :: "'d :: type" \<Rightarrow> \<open>
wenzelm@60209
   375
      match my_thms' in R:"\<And>(x :: 'f :: type). ?P (first_id x) \<Longrightarrow> ?R"
wenzelm@60209
   376
                     and R':"\<And>(x :: 'f :: type). ?P' (first_id x) \<Longrightarrow> ?R'" \<Rightarrow> \<open>
wenzelm@60209
   377
        match (x) in "q :: 'f" for q \<Rightarrow> \<open>
wenzelm@60209
   378
          rule R[of q,simplified first_id_def],
wenzelm@60209
   379
          print_conclusion,
wenzelm@60209
   380
          rule foo
wenzelm@60209
   381
      \<close>\<close>\<close>)
wenzelm@60209
   382
  done
wenzelm@60209
   383
wenzelm@60209
   384
wenzelm@60285
   385
subsection \<open>Unchecked rule instantiation, with the possibility of runtime errors\<close>
wenzelm@60285
   386
wenzelm@60285
   387
named_theorems my_thms_named
wenzelm@60285
   388
wenzelm@60285
   389
declare foo'_ax3[my_thms_named]
wenzelm@60285
   390
wenzelm@60285
   391
method foo_method3 declares my_thms_named =
wenzelm@60285
   392
  (match my_thms_named[of (unchecked) z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>)
wenzelm@60285
   393
wenzelm@60285
   394
notepad
wenzelm@60285
   395
begin
wenzelm@60285
   396
wenzelm@60285
   397
  (*FIXME: Shouldn't need unchecked keyword here. See Tests_Failing.thy *)
wenzelm@60285
   398
  fix A B x
wenzelm@60285
   399
  have "foo' x B A \<Longrightarrow> A \<and> B"
wenzelm@60285
   400
    by (match my_thms[of (unchecked) z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>)
wenzelm@60285
   401
wenzelm@60285
   402
  fix A B x
wenzelm@60285
   403
  note foo'_ax1[my_thms_named]
wenzelm@60285
   404
  have "foo' x B A \<Longrightarrow> A \<and> B"
wenzelm@60285
   405
    by (match my_thms_named[where x=z for z] in R:"PROP ?H" \<Rightarrow> \<open>rule R\<close>)
wenzelm@60285
   406
wenzelm@60285
   407
  fix A B x
wenzelm@60285
   408
  note foo'_ax1[my_thms_named] foo'_ax2[my_thms_named] foo'_ax3[my_thms_named]
wenzelm@60285
   409
  have "foo' x B A \<Longrightarrow> A \<and> B"
wenzelm@60285
   410
   by foo_method3
wenzelm@60285
   411
wenzelm@60285
   412
end
wenzelm@60285
   413
wenzelm@60285
   414
wenzelm@60248
   415
ML \<open>
wenzelm@60119
   416
structure Data = Generic_Data
wenzelm@60119
   417
(
wenzelm@60119
   418
  type T = thm list;
wenzelm@60119
   419
  val empty: T = [];
wenzelm@60119
   420
  val extend = I;
wenzelm@60119
   421
  fun merge data : T = Thm.merge_thms data;
wenzelm@60119
   422
);
wenzelm@60248
   423
\<close>
wenzelm@60119
   424
wenzelm@60119
   425
local_setup \<open>Local_Theory.add_thms_dynamic (@{binding test_dyn}, Data.get)\<close>
wenzelm@60119
   426
wenzelm@60119
   427
setup \<open>Context.theory_map (Data.put @{thms TrueI})\<close>
wenzelm@60119
   428
wenzelm@60209
   429
method dynamic_thms_test = (rule test_dyn)
wenzelm@60119
   430
wenzelm@60119
   431
locale foo =
wenzelm@60119
   432
  fixes A
wenzelm@60119
   433
  assumes A : "A"
wenzelm@60119
   434
begin
wenzelm@60119
   435
wenzelm@60119
   436
local_setup
wenzelm@60119
   437
  \<open>Local_Theory.declaration {pervasive = false, syntax = false}
wenzelm@60119
   438
    (fn phi => Data.put (Morphism.fact phi @{thms A}))\<close>
wenzelm@60119
   439
wenzelm@60119
   440
lemma A by dynamic_thms_test
wenzelm@60119
   441
wenzelm@60119
   442
end
wenzelm@60119
   443
wenzelm@60248
   444
wenzelm@60285
   445
notepad
wenzelm@60285
   446
begin
wenzelm@60248
   447
  fix A x
wenzelm@60248
   448
  assume X: "\<And>x. A x"
wenzelm@60248
   449
  have "A x"
wenzelm@60285
   450
    by (match X in H[of x]:"\<And>x. A x" \<Rightarrow> \<open>print_fact H,match H in "A x" \<Rightarrow> \<open>rule H\<close>\<close>)
wenzelm@60248
   451
wenzelm@60248
   452
  fix A x B
wenzelm@60248
   453
  assume X: "\<And>x :: bool. A x \<Longrightarrow> B" "\<And>x. A x"
wenzelm@60248
   454
  assume Y: "A B"
wenzelm@60248
   455
  have "B \<and> B \<and> B \<and> B \<and> B \<and> B"
wenzelm@60285
   456
    apply (intro conjI)
wenzelm@60285
   457
    apply (match X in H[OF X(2)]:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H,rule H\<close>)
wenzelm@60285
   458
    apply (match X in H':"\<And>x. A x" and H[OF H']:"\<And>x. A x \<Longrightarrow> B" \<Rightarrow> \<open>print_fact H',print_fact H,rule H\<close>)
wenzelm@60285
   459
    apply (match X in H[of Q]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H, rule Y\<close>)
wenzelm@60285
   460
    apply (match X in H[of Q,OF Y]:"\<And>x. A x \<Longrightarrow> ?R" and "?P \<Longrightarrow> Q" for Q \<Rightarrow> \<open>print_fact H,rule H\<close>)
wenzelm@60285
   461
    apply (match X in H[OF Y,intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>print_fact H,fastforce\<close>)
wenzelm@60285
   462
    apply (match X in H[intro]:"\<And>x. A x \<Longrightarrow> ?R" \<Rightarrow> \<open>rule H[where x=B], rule Y\<close>)
wenzelm@60285
   463
    done
wenzelm@60285
   464
wenzelm@60248
   465
  fix x :: "prop" and A
wenzelm@60248
   466
  assume X: "TERM x"
wenzelm@60248
   467
  assume Y: "\<And>x :: prop. A x"
wenzelm@60248
   468
  have "A TERM x"
wenzelm@60285
   469
    apply (match X in "PROP y" for y \<Rightarrow> \<open>rule Y[where x="PROP y"]\<close>)
wenzelm@60285
   470
    done
wenzelm@60248
   471
end
wenzelm@60248
   472
wenzelm@60287
   473
subsection \<open>Proper context for method parameters\<close>
wenzelm@60287
   474
wenzelm@61912
   475
method add_simp methods m uses f = (match f in H[simp]:_ \<Rightarrow> m)
wenzelm@60287
   476
wenzelm@61912
   477
method add_my_thms methods m uses f = (match f in H[my_thms_named]:_ \<Rightarrow> m)
wenzelm@60287
   478
wenzelm@60287
   479
method rule_my_thms = (rule my_thms_named)
wenzelm@60287
   480
method rule_my_thms' declares my_thms_named = (rule my_thms_named)
wenzelm@60287
   481
wenzelm@60287
   482
lemma
wenzelm@60287
   483
  assumes A: A and B: B
wenzelm@60287
   484
  shows
wenzelm@60287
   485
  "(A \<or> B) \<and> A \<and> A \<and> A"
wenzelm@60287
   486
  apply (intro conjI)
wenzelm@61912
   487
  apply (add_simp \<open>add_simp simp f: B\<close> f: A)
wenzelm@61912
   488
  apply (add_my_thms rule_my_thms f:A)
wenzelm@61912
   489
  apply (add_my_thms rule_my_thms' f:A)
wenzelm@60287
   490
  apply (add_my_thms \<open>rule my_thms_named\<close> f:A)
wenzelm@60287
   491
  done
wenzelm@60287
   492
wenzelm@62070
   493
wenzelm@60287
   494
subsection \<open>Shallow parser tests\<close>
wenzelm@60287
   495
wenzelm@61813
   496
method all_args for A B methods m1 m2 uses f1 f2 declares my_thms_named = fail
wenzelm@60287
   497
wenzelm@60287
   498
lemma True
wenzelm@61912
   499
  by (all_args True False - fail f1: TrueI f2: TrueI my_thms_named: TrueI | rule TrueI)
wenzelm@60285
   500
wenzelm@62070
   501
wenzelm@60285
   502
subsection \<open>Method name internalization test\<close>
wenzelm@60209
   503
wenzelm@60287
   504
wenzelm@60209
   505
method test2 = (simp)
wenzelm@60209
   506
wenzelm@60209
   507
method simp = fail
wenzelm@60209
   508
wenzelm@60209
   509
lemma "A \<Longrightarrow> A" by test2
wenzelm@60209
   510
wenzelm@62070
   511
wenzelm@62078
   512
subsection \<open>Dynamic facts\<close>
wenzelm@62078
   513
wenzelm@62078
   514
named_theorems my_thms_named'
wenzelm@62078
   515
wenzelm@62078
   516
method foo_method1 for x =
wenzelm@62078
   517
  (match my_thms_named' [of (unchecked) x] in R: "PROP ?H" \<Rightarrow> \<open>rule R\<close>)
wenzelm@62078
   518
wenzelm@62078
   519
lemma
wenzelm@62078
   520
  assumes A [my_thms_named']: "\<And>x. A x"
wenzelm@62078
   521
  shows "A y"
wenzelm@62078
   522
  by (foo_method1 y)
wenzelm@62078
   523
wenzelm@62078
   524
wenzelm@62070
   525
subsection \<open>Eisbach method invocation from ML\<close>
wenzelm@62070
   526
wenzelm@62070
   527
method test_method for x y uses r = (print_term x, print_term y, rule r)
wenzelm@62070
   528
wenzelm@62070
   529
method_setup test_method' = \<open>
wenzelm@62070
   530
  Args.term -- Args.term --
wenzelm@62070
   531
  (Scan.lift (Args.$$$ "rule" -- Args.colon) |-- Attrib.thms) >>
wenzelm@62070
   532
    (fn ((x, y), r) => fn ctxt =>
wenzelm@62075
   533
      Method_Closure.apply_method ctxt @{method test_method} [x, y] [r] [] ctxt);
wenzelm@62070
   534
\<close>
wenzelm@62070
   535
wenzelm@62070
   536
lemma
wenzelm@62070
   537
  fixes a b :: nat
wenzelm@62070
   538
  assumes "a = b"
wenzelm@62070
   539
  shows "b = a"
wenzelm@62070
   540
  apply (test_method a b)?
wenzelm@62070
   541
  apply (test_method' a b rule: refl)?
wenzelm@62070
   542
  apply (test_method' a b rule: assms [symmetric])?
wenzelm@62070
   543
  done
wenzelm@62070
   544
daniel@63185
   545
subsection \<open>Eisbach methods in locales\<close>
daniel@63185
   546
daniel@63185
   547
locale my_locale1 = fixes A assumes A: A begin
daniel@63185
   548
daniel@63185
   549
method apply_A =
daniel@63185
   550
  (match conclusion in "A" \<Rightarrow>
daniel@63185
   551
    \<open>match A in U:"A" \<Rightarrow>
daniel@63185
   552
      \<open>print_term A, print_fact A, rule U\<close>\<close>)
daniel@63185
   553
wenzelm@60119
   554
end
daniel@63185
   555
daniel@63185
   556
locale my_locale2 = fixes B assumes B: B begin
daniel@63185
   557
daniel@63185
   558
interpretation my_locale1 B by (unfold_locales; rule B)
daniel@63185
   559
daniel@63185
   560
lemma B by apply_A
daniel@63185
   561
daniel@63185
   562
end
daniel@63185
   563
daniel@63185
   564
context fixes C assumes C: C begin
daniel@63185
   565
daniel@63185
   566
interpretation my_locale1 C by (unfold_locales; rule C)
daniel@63185
   567
daniel@63185
   568
lemma C by apply_A
daniel@63185
   569
daniel@63185
   570
end
daniel@63185
   571
daniel@63185
   572
context begin
daniel@63185
   573
daniel@63185
   574
interpretation my_locale1 "True \<longrightarrow> True" by (unfold_locales; blast)
daniel@63185
   575
daniel@63185
   576
lemma "True \<longrightarrow> True" by apply_A
daniel@63185
   577
daniel@63185
   578
end
daniel@63185
   579
daniel@63185
   580
locale locale_poly = fixes P assumes P: "\<And>x :: 'a. P x" begin
daniel@63185
   581
daniel@63185
   582
method solve_P for z :: 'a = (rule P[where x = z]) 
daniel@63185
   583
daniel@63185
   584
end
daniel@63185
   585
daniel@63185
   586
context begin
daniel@63185
   587
daniel@63185
   588
interpretation locale_poly "\<lambda>x:: nat. 0 \<le> x" by (unfold_locales; blast)
daniel@63185
   589
daniel@63185
   590
lemma "0 \<le> (n :: nat)" by (solve_P n)
daniel@63185
   591
daniel@63185
   592
end
daniel@63185
   593
daniel@63186
   594
subsection \<open>Mutual recursion via higher-order methods\<close>
daniel@63186
   595
daniel@63186
   596
experiment begin
daniel@63186
   597
daniel@63186
   598
method inner_method methods passed_method = (rule conjI; passed_method)
daniel@63186
   599
daniel@63186
   600
method outer_method = (inner_method \<open>outer_method\<close> | assumption)
daniel@63186
   601
daniel@63186
   602
lemma "Q \<Longrightarrow> R \<Longrightarrow> P \<Longrightarrow> (Q \<and> R) \<and> P"
daniel@63186
   603
  by outer_method
daniel@63186
   604
daniel@63185
   605
end
daniel@63186
   606
daniel@63186
   607
end