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