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
```