doc-src/TutorialI/Inductive/Advanced.thy
author nipkow
Wed Dec 06 13:22:58 2000 +0100 (2000-12-06)
changeset 10608 620647438780
parent 10468 87dda999deca
child 10882 ca41ba5fb8e2
permissions -rw-r--r--
*** empty log message ***
paulson@10370
     1
(* ID:         $Id$ *)
nipkow@10426
     2
theory Advanced = Even:
nipkow@10426
     3
paulson@10468
     4
paulson@10468
     5
datatype 'f gterm = Apply 'f "'f gterm list"
paulson@10468
     6
paulson@10468
     7
datatype integer_op = Number int | UnaryMinus | Plus;
paulson@10468
     8
paulson@10468
     9
consts gterms :: "'f set \<Rightarrow> 'f gterm set"
paulson@10468
    10
inductive "gterms F"
paulson@10468
    11
intros
paulson@10468
    12
step[intro!]: "\<lbrakk>\<forall>t \<in> set args. t \<in> gterms F;  f \<in> F\<rbrakk>
paulson@10468
    13
               \<Longrightarrow> (Apply f args) \<in> gterms F"
paulson@10468
    14
paulson@10468
    15
lemma gterms_mono: "F\<subseteq>G \<Longrightarrow> gterms F \<subseteq> gterms G"
paulson@10468
    16
apply clarify
paulson@10468
    17
apply (erule gterms.induct)
paulson@10468
    18
apply blast
paulson@10468
    19
done
paulson@10468
    20
paulson@10468
    21
text{*
paulson@10468
    22
The situation after induction
nipkow@10426
    23
paulson@10468
    24
proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{2}}\isanewline
paulson@10468
    25
\isanewline
paulson@10468
    26
goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
paulson@10468
    27
F\ {\isasymsubseteq}\ G\ {\isasymLongrightarrow}\ gterms\ F\ {\isasymsubseteq}\ gterms\ G\isanewline
paulson@10468
    28
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
paulson@10468
    29
\ \ \ \ \ \ \ {\isasymlbrakk}F\ {\isasymsubseteq}\ G{\isacharsemicolon}\ {\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ t\ {\isasymin}\ gterms\ G{\isacharsemicolon}\ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
paulson@10468
    30
\ \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G
paulson@10468
    31
*}
paulson@10468
    32
paulson@10468
    33
text{* We completely forgot about "rule inversion". 
paulson@10468
    34
paulson@10468
    35
@{thm[display] even.cases[no_vars]}
paulson@10468
    36
\rulename{even.cases}
paulson@10468
    37
paulson@10468
    38
Just as a demo I include
paulson@10468
    39
the two forms that Markus has made available. First the one for binding the
paulson@10468
    40
result to a name 
paulson@10468
    41
paulson@10468
    42
*}
paulson@10468
    43
paulson@10468
    44
inductive_cases Suc_Suc_cases [elim!]:
nipkow@10426
    45
  "Suc(Suc n) \<in> even"
nipkow@10426
    46
paulson@10468
    47
thm Suc_Suc_cases;
paulson@10468
    48
paulson@10468
    49
text{*
paulson@10468
    50
@{thm[display] Suc_Suc_cases[no_vars]}
paulson@10468
    51
\rulename{Suc_Suc_cases}
paulson@10468
    52
paulson@10468
    53
and now the one for local usage:
paulson@10468
    54
*}
paulson@10468
    55
paulson@10468
    56
lemma "Suc(Suc n) \<in> even \<Longrightarrow> P n";
paulson@10468
    57
apply (ind_cases "Suc(Suc n) \<in> even");
paulson@10468
    58
oops
paulson@10468
    59
paulson@10468
    60
inductive_cases gterm_Apply_elim [elim!]: "Apply f args \<in> gterms F"
paulson@10468
    61
paulson@10468
    62
text{*this is what we get:
paulson@10468
    63
paulson@10468
    64
@{thm[display] gterm_Apply_elim[no_vars]}
paulson@10468
    65
\rulename{gterm_Apply_elim}
paulson@10468
    66
*}
nipkow@10426
    67
paulson@10468
    68
lemma gterms_IntI [rule_format]:
paulson@10468
    69
     "t \<in> gterms F \<Longrightarrow> t \<in> gterms G \<longrightarrow> t \<in> gterms (F\<inter>G)"
paulson@10468
    70
apply (erule gterms.induct)
paulson@10468
    71
apply blast
paulson@10468
    72
done
paulson@10468
    73
paulson@10468
    74
paulson@10468
    75
text{*
paulson@10468
    76
Subgoal after induction.  How would we cope without rule inversion?
paulson@10468
    77
paulson@10468
    78
pr(latex xsymbols symbols)
paulson@10468
    79
paulson@10468
    80
proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
paulson@10468
    81
\isanewline
paulson@10468
    82
goal\ {\isacharparenleft}lemma\ gterms{\isacharunderscore}IntI{\isacharparenright}{\isacharcolon}\isanewline
paulson@10468
    83
t\ {\isasymin}\ gterms\ F\ {\isasymLongrightarrow}\ t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}\isanewline
paulson@10468
    84
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}args\ f{\isachardot}\isanewline
paulson@10468
    85
\ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\ t\ {\isasymin}\ gterms\ F\ {\isasymand}\ {\isacharparenleft}t\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ t\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
paulson@10468
    86
\ \ \ \ \ \ \ \ \ \ f\ {\isasymin}\ F{\isasymrbrakk}\isanewline
paulson@10468
    87
\ \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ G\ {\isasymlongrightarrow}\ Apply\ f\ args\ {\isasymin}\ gterms\ {\isacharparenleft}F\ {\isasyminter}\ G{\isacharparenright}
paulson@10468
    88
paulson@10468
    89
paulson@10468
    90
*}
paulson@10468
    91
paulson@10468
    92
text{*
paulson@10468
    93
@{thm[display] mono_Int[no_vars]}
paulson@10468
    94
\rulename{mono_Int}
paulson@10468
    95
*}
nipkow@10426
    96
paulson@10468
    97
lemma gterms_Int_eq [simp]:
paulson@10468
    98
     "gterms (F\<inter>G) = gterms F \<inter> gterms G"
paulson@10468
    99
apply (rule equalityI)
paulson@10468
   100
apply (blast intro!: mono_Int monoI gterms_mono)
paulson@10468
   101
apply (blast intro!: gterms_IntI)
paulson@10468
   102
done
paulson@10468
   103
paulson@10468
   104
paulson@10468
   105
consts integer_arity :: "integer_op \<Rightarrow> nat"
paulson@10468
   106
primrec
paulson@10468
   107
"integer_arity (Number n)        = #0"
paulson@10468
   108
"integer_arity UnaryMinus        = #1"
paulson@10468
   109
"integer_arity Plus              = #2"
paulson@10468
   110
paulson@10468
   111
consts well_formed_gterm :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
paulson@10468
   112
inductive "well_formed_gterm arity"
paulson@10468
   113
intros
paulson@10468
   114
step[intro!]: "\<lbrakk>\<forall>t \<in> set args. t \<in> well_formed_gterm arity;  
paulson@10468
   115
                length args = arity f\<rbrakk>
paulson@10468
   116
               \<Longrightarrow> (Apply f args) \<in> well_formed_gterm arity"
paulson@10468
   117
nipkow@10426
   118
paulson@10468
   119
consts well_formed_gterm' :: "('f \<Rightarrow> nat) \<Rightarrow> 'f gterm set"
paulson@10468
   120
inductive "well_formed_gterm' arity"
paulson@10468
   121
intros
paulson@10468
   122
step[intro!]: "\<lbrakk>args \<in> lists (well_formed_gterm' arity);  
paulson@10468
   123
                length args = arity f\<rbrakk>
paulson@10468
   124
               \<Longrightarrow> (Apply f args) \<in> well_formed_gterm' arity"
paulson@10468
   125
monos lists_mono
paulson@10468
   126
paulson@10468
   127
lemma "well_formed_gterm arity \<subseteq> well_formed_gterm' arity"
paulson@10468
   128
apply clarify
paulson@10468
   129
apply (erule well_formed_gterm.induct)
paulson@10468
   130
apply auto
paulson@10468
   131
done
paulson@10468
   132
nipkow@10426
   133
paulson@10468
   134
text{*
paulson@10468
   135
The situation after clarify (note the induction hypothesis!)
paulson@10468
   136
paulson@10468
   137
pr(latex xsymbols symbols)
paulson@10468
   138
paulson@10468
   139
proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{2}}\isanewline
paulson@10468
   140
\isanewline
paulson@10468
   141
goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
paulson@10468
   142
well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\isanewline
paulson@10468
   143
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
paulson@10468
   144
\ \ \ \ \ \ \ {\isasymlbrakk}{\isasymforall}t{\isasymin}set\ args{\isachardot}\isanewline
paulson@10468
   145
\ \ \ \ \ \ \ \ \ \ \ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\ {\isasymand}\ t\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity{\isacharsemicolon}\isanewline
paulson@10468
   146
\ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
paulson@10468
   147
\ \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity
nipkow@10426
   148
*}
nipkow@10426
   149
paulson@10370
   150
paulson@10468
   151
lemma "well_formed_gterm' arity \<subseteq> well_formed_gterm arity"
paulson@10468
   152
apply clarify
paulson@10468
   153
apply (erule well_formed_gterm'.induct)
paulson@10468
   154
apply auto
paulson@10468
   155
done
paulson@10370
   156
paulson@10370
   157
paulson@10468
   158
text{*
paulson@10468
   159
@{thm[display] lists_Int_eq[no_vars]}
paulson@10468
   160
\rulename{lists_Int_eq}
paulson@10468
   161
paulson@10468
   162
The situation after clarify (note the strange induction hypothesis!)
paulson@10468
   163
paulson@10468
   164
pr(latex xsymbols symbols)
paulson@10370
   165
paulson@10468
   166
proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{2}}\isanewline
paulson@10468
   167
\isanewline
paulson@10468
   168
goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
paulson@10468
   169
well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasymsubseteq}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity\isanewline
paulson@10468
   170
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}x\ args\ f{\isachardot}\isanewline
paulson@10468
   171
\ \ \ \ \ \ \ {\isasymlbrakk}args\isanewline
paulson@10468
   172
\ \ \ \ \ \ \ \ {\isasymin}\ lists\isanewline
paulson@10468
   173
\ \ \ \ \ \ \ \ \ \ \ {\isacharparenleft}well{\isacharunderscore}formed{\isacharunderscore}gterm{\isacharprime}\ arity\ {\isasyminter}\ {\isacharbraceleft}u{\isachardot}\ u\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity{\isacharbraceright}{\isacharparenright}{\isacharsemicolon}\isanewline
paulson@10468
   174
\ \ \ \ \ \ \ \ \ \ length\ args\ {\isacharequal}\ arity\ f{\isasymrbrakk}\isanewline
paulson@10468
   175
\ \ \ \ \ \ \ {\isasymLongrightarrow}\ Apply\ f\ args\ {\isasymin}\ well{\isacharunderscore}formed{\isacharunderscore}gterm\ arity
paulson@10468
   176
*}
paulson@10468
   177
paulson@10468
   178
text{* the rest isn't used: too complicated.  OK for an exercise though.*}
paulson@10468
   179
paulson@10468
   180
consts integer_signature :: "(integer_op * (unit list * unit)) set"
paulson@10468
   181
inductive "integer_signature"
paulson@10370
   182
intros
paulson@10468
   183
Number:     "(Number n,   ([], ())) \<in> integer_signature"
paulson@10468
   184
UnaryMinus: "(UnaryMinus, ([()], ())) \<in> integer_signature"
paulson@10468
   185
Plus:       "(Plus,       ([(),()], ())) \<in> integer_signature"
paulson@10468
   186
paulson@10370
   187
paulson@10468
   188
consts well_typed_gterm :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f gterm * 't)set"
paulson@10468
   189
inductive "well_typed_gterm sig"
paulson@10370
   190
intros
paulson@10468
   191
step[intro!]: 
paulson@10468
   192
    "\<lbrakk>\<forall>pair \<in> set args. pair \<in> well_typed_gterm sig; 
paulson@10468
   193
      sig f = (map snd args, rtype)\<rbrakk>
paulson@10468
   194
     \<Longrightarrow> (Apply f (map fst args), rtype) 
paulson@10468
   195
         \<in> well_typed_gterm sig"
paulson@10468
   196
paulson@10468
   197
consts well_typed_gterm' :: "('f \<Rightarrow> 't list * 't) \<Rightarrow> ('f gterm * 't)set"
paulson@10468
   198
inductive "well_typed_gterm' sig"
paulson@10468
   199
intros
paulson@10468
   200
step[intro!]: 
paulson@10468
   201
    "\<lbrakk>args \<in> lists(well_typed_gterm' sig); 
paulson@10468
   202
      sig f = (map snd args, rtype)\<rbrakk>
paulson@10468
   203
     \<Longrightarrow> (Apply f (map fst args), rtype) 
paulson@10468
   204
         \<in> well_typed_gterm' sig"
paulson@10370
   205
monos lists_mono
paulson@10370
   206
paulson@10370
   207
paulson@10468
   208
lemma "well_typed_gterm sig \<subseteq> well_typed_gterm' sig"
paulson@10370
   209
apply clarify
paulson@10468
   210
apply (erule well_typed_gterm.induct)
paulson@10370
   211
apply auto
paulson@10370
   212
done
paulson@10370
   213
paulson@10468
   214
lemma "well_typed_gterm' sig \<subseteq> well_typed_gterm sig"
paulson@10370
   215
apply clarify
paulson@10468
   216
apply (erule well_typed_gterm'.induct)
paulson@10370
   217
apply auto
paulson@10370
   218
done
paulson@10370
   219
paulson@10468
   220
paulson@10370
   221
end
paulson@10370
   222