1.1 --- a/src/HOL/Induct/QuoDataType.thy Thu Sep 02 14:50:00 2004 +0200
1.2 +++ b/src/HOL/Induct/QuoDataType.thy Thu Sep 02 16:52:21 2004 +0200
1.3 @@ -373,7 +373,7 @@
1.4 by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)
1.5
1.6 text{*...and many similar results*}
1.7 -theorem Crypt_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
1.8 +theorem Crypt2_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
1.9 by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)
1.10
1.11 theorem Crypt_Crypt_eq [iff]: "(Crypt K X = Crypt K X') = (X=X')"
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/Induct/QuoNestedDataType.thy Thu Sep 02 16:52:21 2004 +0200
2.3 @@ -0,0 +1,462 @@
2.4 +(* Title: HOL/Induct/QuoNestedDataType
2.5 + ID: $Id$
2.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
2.7 + Copyright 2004 University of Cambridge
2.8 +
2.9 +*)
2.10 +
2.11 +header{*Quotienting a Free Algebra Involving Nested Recursion*}
2.12 +
2.13 +theory QuoNestedDataType = Main:
2.14 +
2.15 +subsection{*Defining the Free Algebra*}
2.16 +
2.17 +text{*Messages with encryption and decryption as free constructors.*}
2.18 +datatype
2.19 + freeExp = VAR nat
2.20 + | PLUS freeExp freeExp
2.21 + | FNCALL nat "freeExp list"
2.22 +
2.23 +text{*The equivalence relation, which makes PLUS associative.*}
2.24 +consts exprel :: "(freeExp * freeExp) set"
2.25 +
2.26 +syntax
2.27 + "_exprel" :: "[freeExp, freeExp] => bool" (infixl "~~" 50)
2.28 +syntax (xsymbols)
2.29 + "_exprel" :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50)
2.30 +syntax (HTML output)
2.31 + "_exprel" :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50)
2.32 +translations
2.33 + "X \<sim> Y" == "(X,Y) \<in> exprel"
2.34 +
2.35 +text{*The first rule is the desired equation. The next three rules
2.36 +make the equations applicable to subterms. The last two rules are symmetry
2.37 +and transitivity.*}
2.38 +inductive "exprel"
2.39 + intros
2.40 + ASSOC: "PLUS X (PLUS Y Z) \<sim> PLUS (PLUS X Y) Z"
2.41 + VAR: "VAR N \<sim> VAR N"
2.42 + PLUS: "\<lbrakk>X \<sim> X'; Y \<sim> Y'\<rbrakk> \<Longrightarrow> PLUS X Y \<sim> PLUS X' Y'"
2.43 + FNCALL: "(Xs,Xs') \<in> listrel exprel \<Longrightarrow> FNCALL F Xs \<sim> FNCALL F Xs'"
2.44 + SYM: "X \<sim> Y \<Longrightarrow> Y \<sim> X"
2.45 + TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
2.46 + monos listrel_mono
2.47 +
2.48 +
2.49 +text{*Proving that it is an equivalence relation*}
2.50 +
2.51 +lemma exprel_refl_conj: "X \<sim> X & (Xs,Xs) \<in> listrel(exprel)"
2.52 +apply (induct X and Xs)
2.53 +apply (blast intro: exprel.intros listrel.intros)+
2.54 +done
2.55 +
2.56 +lemmas exprel_refl = exprel_refl_conj [THEN conjunct1]
2.57 +lemmas list_exprel_refl = exprel_refl_conj [THEN conjunct2]
2.58 +
2.59 +theorem equiv_exprel: "equiv UNIV exprel"
2.60 +proof (simp add: equiv_def, intro conjI)
2.61 + show "reflexive exprel" by (simp add: refl_def exprel_refl)
2.62 + show "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM)
2.63 + show "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS)
2.64 +qed
2.65 +
2.66 +theorem equiv_list_exprel: "equiv UNIV (listrel exprel)"
2.67 +by (insert equiv_listrel [OF equiv_exprel], simp)
2.68 +
2.69 +
2.70 +lemma FNCALL_Nil: "FNCALL F [] \<sim> FNCALL F []"
2.71 +apply (rule exprel.intros)
2.72 +apply (rule listrel.intros)
2.73 +done
2.74 +
2.75 +lemma FNCALL_Cons:
2.76 + "\<lbrakk>X \<sim> X'; (Xs,Xs') \<in> listrel(exprel)\<rbrakk>
2.77 + \<Longrightarrow> FNCALL F (X#Xs) \<sim> FNCALL F (X'#Xs')"
2.78 +by (blast intro: exprel.intros listrel.intros)
2.79 +
2.80 +
2.81 +
2.82 +subsection{*Some Functions on the Free Algebra*}
2.83 +
2.84 +subsubsection{*The Set of Variables*}
2.85 +
2.86 +text{*A function to return the set of variables present in a message. It will
2.87 +be lifted to the initial algrebra, to serve as an example of that process.
2.88 +Note that the "free" refers to the free datatype rather than to the concept
2.89 +of a free variable.*}
2.90 +consts
2.91 + freevars :: "freeExp \<Rightarrow> nat set"
2.92 + freevars_list :: "freeExp list \<Rightarrow> nat set"
2.93 +
2.94 +primrec
2.95 + "freevars (VAR N) = {N}"
2.96 + "freevars (PLUS X Y) = freevars X \<union> freevars Y"
2.97 + "freevars (FNCALL F Xs) = freevars_list Xs"
2.98 +
2.99 + "freevars_list [] = {}"
2.100 + "freevars_list (X # Xs) = freevars X \<union> freevars_list Xs"
2.101 +
2.102 +text{*This theorem lets us prove that the vars function respects the
2.103 +equivalence relation. It also helps us prove that Variable
2.104 + (the abstract constructor) is injective*}
2.105 +theorem exprel_imp_eq_freevars: "U \<sim> V \<Longrightarrow> freevars U = freevars V"
2.106 +apply (erule exprel.induct)
2.107 +apply (erule_tac [4] listrel.induct)
2.108 +apply (simp_all add: Un_assoc)
2.109 +done
2.110 +
2.111 +
2.112 +
2.113 +subsubsection{*Functions for Freeness*}
2.114 +
2.115 +text{*A discriminator function to distinguish vars, sums and function calls*}
2.116 +consts freediscrim :: "freeExp \<Rightarrow> int"
2.117 +primrec
2.118 + "freediscrim (VAR N) = 0"
2.119 + "freediscrim (PLUS X Y) = 1"
2.120 + "freediscrim (FNCALL F Xs) = 2"
2.121 +
2.122 +theorem exprel_imp_eq_freediscrim:
2.123 + "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
2.124 +by (erule exprel.induct, auto)
2.125 +
2.126 +
2.127 +text{*This function, which returns the function name, is used to
2.128 +prove part of the injectivity property for FnCall.*}
2.129 +consts freefun :: "freeExp \<Rightarrow> nat"
2.130 +
2.131 +primrec
2.132 + "freefun (VAR N) = 0"
2.133 + "freefun (PLUS X Y) = 0"
2.134 + "freefun (FNCALL F Xs) = F"
2.135 +
2.136 +theorem exprel_imp_eq_freefun:
2.137 + "U \<sim> V \<Longrightarrow> freefun U = freefun V"
2.138 +by (erule exprel.induct, simp_all add: listrel.intros)
2.139 +
2.140 +
2.141 +text{*This function, which returns the list of function arguments, is used to
2.142 +prove part of the injectivity property for FnCall.*}
2.143 +consts freeargs :: "freeExp \<Rightarrow> freeExp list"
2.144 +primrec
2.145 + "freeargs (VAR N) = []"
2.146 + "freeargs (PLUS X Y) = []"
2.147 + "freeargs (FNCALL F Xs) = Xs"
2.148 +
2.149 +theorem exprel_imp_eqv_freeargs:
2.150 + "U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel"
2.151 +apply (erule exprel.induct)
2.152 +apply (erule_tac [4] listrel.induct)
2.153 +apply (simp_all add: listrel.intros)
2.154 +apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]])
2.155 +apply (blast intro: transD [OF equiv.trans [OF equiv_list_exprel]])
2.156 +done
2.157 +
2.158 +
2.159 +
2.160 +subsection{*The Initial Algebra: A Quotiented Message Type*}
2.161 +
2.162 +
2.163 +typedef (Exp) exp = "UNIV//exprel"
2.164 + by (auto simp add: quotient_def)
2.165 +
2.166 +text{*The abstract message constructors*}
2.167 +
2.168 +constdefs
2.169 + Var :: "nat \<Rightarrow> exp"
2.170 + "Var N == Abs_Exp(exprel``{VAR N})"
2.171 +
2.172 + Plus :: "[exp,exp] \<Rightarrow> exp"
2.173 + "Plus X Y ==
2.174 + Abs_Exp (\<Union>U \<in> Rep_Exp X. \<Union>V \<in> Rep_Exp Y. exprel``{PLUS U V})"
2.175 +
2.176 + FnCall :: "[nat, exp list] \<Rightarrow> exp"
2.177 + "FnCall F Xs ==
2.178 + Abs_Exp (\<Union>Us \<in> listset (map Rep_Exp Xs). exprel `` {FNCALL F Us})"
2.179 +
2.180 +
2.181 +text{*Reduces equality of equivalence classes to the @{term exprel} relation:
2.182 + @{term "(exprel `` {x} = exprel `` {y}) = ((x,y) \<in> exprel)"} *}
2.183 +lemmas equiv_exprel_iff = eq_equiv_class_iff [OF equiv_exprel UNIV_I UNIV_I]
2.184 +
2.185 +declare equiv_exprel_iff [simp]
2.186 +
2.187 +
2.188 +text{*All equivalence classes belong to set of representatives*}
2.189 +lemma [simp]: "exprel``{U} \<in> Exp"
2.190 +by (auto simp add: Exp_def quotient_def intro: exprel_refl)
2.191 +
2.192 +lemma inj_on_Abs_Exp: "inj_on Abs_Exp Exp"
2.193 +apply (rule inj_on_inverseI)
2.194 +apply (erule Abs_Exp_inverse)
2.195 +done
2.196 +
2.197 +text{*Reduces equality on abstractions to equality on representatives*}
2.198 +declare inj_on_Abs_Exp [THEN inj_on_iff, simp]
2.199 +
2.200 +declare Abs_Exp_inverse [simp]
2.201 +
2.202 +
2.203 +text{*Case analysis on the representation of a exp as an equivalence class.*}
2.204 +lemma eq_Abs_Exp [case_names Abs_Exp, cases type: exp]:
2.205 + "(!!U. z = Abs_Exp(exprel``{U}) ==> P) ==> P"
2.206 +apply (rule Rep_Exp [of z, unfolded Exp_def, THEN quotientE])
2.207 +apply (drule arg_cong [where f=Abs_Exp])
2.208 +apply (auto simp add: Rep_Exp_inverse intro: exprel_refl)
2.209 +done
2.210 +
2.211 +
2.212 +subsection{*Every list of abstract expressions can be expressed in terms of a
2.213 + list of concrete expressions*}
2.214 +
2.215 +constdefs Abs_ExpList :: "freeExp list => exp list"
2.216 + "Abs_ExpList Xs == map (%U. Abs_Exp(exprel``{U})) Xs"
2.217 +
2.218 +lemma Abs_ExpList_Nil [simp]: "Abs_ExpList [] == []"
2.219 +by (simp add: Abs_ExpList_def)
2.220 +
2.221 +lemma Abs_ExpList_Cons [simp]:
2.222 + "Abs_ExpList (X#Xs) == Abs_Exp (exprel``{X}) # Abs_ExpList Xs"
2.223 +by (simp add: Abs_ExpList_def)
2.224 +
2.225 +lemma ExpList_rep: "\<exists>Us. z = Abs_ExpList Us"
2.226 +apply (induct z)
2.227 +apply (rule_tac [2] z=a in eq_Abs_Exp)
2.228 +apply (auto simp add: Abs_ExpList_def intro: exprel_refl)
2.229 +done
2.230 +
2.231 +lemma eq_Abs_ExpList [case_names Abs_ExpList]:
2.232 + "(!!Us. z = Abs_ExpList Us ==> P) ==> P"
2.233 +by (rule exE [OF ExpList_rep], blast)
2.234 +
2.235 +
2.236 +subsubsection{*Characteristic Equations for the Abstract Constructors*}
2.237 +
2.238 +lemma Plus: "Plus (Abs_Exp(exprel``{U})) (Abs_Exp(exprel``{V})) =
2.239 + Abs_Exp (exprel``{PLUS U V})"
2.240 +proof -
2.241 + have "(\<lambda>U V. exprel `` {PLUS U V}) respects2 exprel"
2.242 + by (simp add: congruent2_def exprel.PLUS)
2.243 + thus ?thesis
2.244 + by (simp add: Plus_def UN_equiv_class2 [OF equiv_exprel equiv_exprel])
2.245 +qed
2.246 +
2.247 +text{*It is not clear what to do with FnCall: it's argument is an abstraction
2.248 +of an @{typ "exp list"}. Is it just Nil or Cons? What seems to work best is to
2.249 +regard an @{typ "exp list"} as a @{term "listrel exprel"} equivalence class*}
2.250 +
2.251 +text{*This theorem is easily proved but never used. There's no obvious way
2.252 +even to state the analogous result, @{text FnCall_Cons}.*}
2.253 +lemma FnCall_Nil: "FnCall F [] = Abs_Exp (exprel``{FNCALL F []})"
2.254 + by (simp add: FnCall_def)
2.255 +
2.256 +lemma FnCall_respects:
2.257 + "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"
2.258 + by (simp add: congruent_def exprel.FNCALL)
2.259 +
2.260 +lemma FnCall_sing:
2.261 + "FnCall F [Abs_Exp(exprel``{U})] = Abs_Exp (exprel``{FNCALL F [U]})"
2.262 +proof -
2.263 + have "(\<lambda>U. exprel `` {FNCALL F [U]}) respects exprel"
2.264 + by (simp add: congruent_def FNCALL_Cons listrel.intros)
2.265 + thus ?thesis
2.266 + by (simp add: FnCall_def UN_equiv_class [OF equiv_exprel])
2.267 +qed
2.268 +
2.269 +lemma listset_Rep_Exp_Abs_Exp:
2.270 + "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}";
2.271 +by (induct_tac Us, simp_all add: listrel_Cons Abs_ExpList_def)
2.272 +
2.273 +lemma FnCall:
2.274 + "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})"
2.275 +proof -
2.276 + have "(\<lambda>Us. exprel `` {FNCALL F Us}) respects (listrel exprel)"
2.277 + by (simp add: congruent_def exprel.FNCALL)
2.278 + thus ?thesis
2.279 + by (simp add: FnCall_def UN_equiv_class [OF equiv_list_exprel]
2.280 + listset_Rep_Exp_Abs_Exp)
2.281 +qed
2.282 +
2.283 +
2.284 +text{*Establishing this equation is the point of the whole exercise*}
2.285 +theorem Plus_assoc: "Plus X (Plus Y Z) = Plus (Plus X Y) Z"
2.286 +by (cases X, cases Y, cases Z, simp add: Plus exprel.ASSOC)
2.287 +
2.288 +
2.289 +
2.290 +subsection{*The Abstract Function to Return the Set of Variables*}
2.291 +
2.292 +constdefs
2.293 + vars :: "exp \<Rightarrow> nat set"
2.294 + "vars X == \<Union>U \<in> Rep_Exp X. freevars U"
2.295 +
2.296 +lemma vars_respects: "freevars respects exprel"
2.297 +by (simp add: congruent_def exprel_imp_eq_freevars)
2.298 +
2.299 +text{*The extension of the function @{term vars} to lists*}
2.300 +consts vars_list :: "exp list \<Rightarrow> nat set"
2.301 +primrec
2.302 + "vars_list [] = {}"
2.303 + "vars_list(E#Es) = vars E \<union> vars_list Es"
2.304 +
2.305 +
2.306 +text{*Now prove the three equations for @{term vars}*}
2.307 +
2.308 +lemma vars_Variable [simp]: "vars (Var N) = {N}"
2.309 +by (simp add: vars_def Var_def
2.310 + UN_equiv_class [OF equiv_exprel vars_respects])
2.311 +
2.312 +lemma vars_Plus [simp]: "vars (Plus X Y) = vars X \<union> vars Y"
2.313 +apply (cases X, cases Y)
2.314 +apply (simp add: vars_def Plus
2.315 + UN_equiv_class [OF equiv_exprel vars_respects])
2.316 +done
2.317 +
2.318 +lemma vars_FnCall [simp]: "vars (FnCall F Xs) = vars_list Xs"
2.319 +apply (cases Xs rule: eq_Abs_ExpList)
2.320 +apply (simp add: FnCall)
2.321 +apply (induct_tac Us)
2.322 +apply (simp_all add: vars_def UN_equiv_class [OF equiv_exprel vars_respects])
2.323 +done
2.324 +
2.325 +lemma vars_FnCall_Nil: "vars (FnCall F Nil) = {}"
2.326 +by simp
2.327 +
2.328 +lemma vars_FnCall_Cons: "vars (FnCall F (X#Xs)) = vars X \<union> vars_list Xs"
2.329 +by simp
2.330 +
2.331 +
2.332 +subsection{*Injectivity Properties of Some Constructors*}
2.333 +
2.334 +lemma VAR_imp_eq: "VAR m \<sim> VAR n \<Longrightarrow> m = n"
2.335 +by (drule exprel_imp_eq_freevars, simp)
2.336 +
2.337 +text{*Can also be proved using the function @{term vars}*}
2.338 +lemma Var_Var_eq [iff]: "(Var m = Var n) = (m = n)"
2.339 +by (auto simp add: Var_def exprel_refl dest: VAR_imp_eq)
2.340 +
2.341 +lemma VAR_neqv_PLUS: "VAR m \<sim> PLUS X Y \<Longrightarrow> False"
2.342 +by (drule exprel_imp_eq_freediscrim, simp)
2.343 +
2.344 +theorem Var_neq_Plus [iff]: "Var N \<noteq> Plus X Y"
2.345 +apply (cases X, cases Y)
2.346 +apply (simp add: Var_def Plus)
2.347 +apply (blast dest: VAR_neqv_PLUS)
2.348 +done
2.349 +
2.350 +theorem Var_neq_FnCall [iff]: "Var N \<noteq> FnCall F Xs"
2.351 +apply (cases Xs rule: eq_Abs_ExpList)
2.352 +apply (auto simp add: FnCall Var_def)
2.353 +apply (drule exprel_imp_eq_freediscrim, simp)
2.354 +done
2.355 +
2.356 +subsection{*Injectivity of @{term FnCall}*}
2.357 +
2.358 +constdefs
2.359 + fun :: "exp \<Rightarrow> nat"
2.360 + "fun X == contents (\<Union>U \<in> Rep_Exp X. {freefun U})"
2.361 +
2.362 +lemma fun_respects: "(%U. {freefun U}) respects exprel"
2.363 +by (simp add: congruent_def exprel_imp_eq_freefun)
2.364 +
2.365 +lemma fun_FnCall [simp]: "fun (FnCall F Xs) = F"
2.366 +apply (cases Xs rule: eq_Abs_ExpList)
2.367 +apply (simp add: FnCall fun_def UN_equiv_class [OF equiv_exprel fun_respects])
2.368 +done
2.369 +
2.370 +constdefs
2.371 + args :: "exp \<Rightarrow> exp list"
2.372 + "args X == contents (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
2.373 +
2.374 +text{*This result can probably be generalized to arbitrary equivalence
2.375 +relations, but with little benefit here.*}
2.376 +lemma Abs_ExpList_eq:
2.377 + "(y, z) \<in> listrel exprel \<Longrightarrow> Abs_ExpList (y) = Abs_ExpList (z)"
2.378 +by (erule listrel.induct, simp_all)
2.379 +
2.380 +lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel"
2.381 +by (simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs)
2.382 +
2.383 +lemma args_FnCall [simp]: "args (FnCall F Xs) = Xs"
2.384 +apply (cases Xs rule: eq_Abs_ExpList)
2.385 +apply (simp add: FnCall args_def UN_equiv_class [OF equiv_exprel args_respects])
2.386 +done
2.387 +
2.388 +
2.389 +lemma FnCall_FnCall_eq [iff]:
2.390 + "(FnCall F Xs = FnCall F' Xs') = (F=F' & Xs=Xs')"
2.391 +proof
2.392 + assume "FnCall F Xs = FnCall F' Xs'"
2.393 + hence "fun (FnCall F Xs) = fun (FnCall F' Xs')"
2.394 + and "args (FnCall F Xs) = args (FnCall F' Xs')" by auto
2.395 + thus "F=F' & Xs=Xs'" by simp
2.396 +next
2.397 + assume "F=F' & Xs=Xs'" thus "FnCall F Xs = FnCall F' Xs'" by simp
2.398 +qed
2.399 +
2.400 +
2.401 +subsection{*The Abstract Discriminator*}
2.402 +text{*However, as @{text FnCall_Var_neq_Var} illustrates, we don't need this
2.403 +function in order to prove discrimination theorems.*}
2.404 +
2.405 +constdefs
2.406 + discrim :: "exp \<Rightarrow> int"
2.407 + "discrim X == contents (\<Union>U \<in> Rep_Exp X. {freediscrim U})"
2.408 +
2.409 +lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
2.410 +by (simp add: congruent_def exprel_imp_eq_freediscrim)
2.411 +
2.412 +text{*Now prove the four equations for @{term discrim}*}
2.413 +
2.414 +lemma discrim_Var [simp]: "discrim (Var N) = 0"
2.415 +by (simp add: discrim_def Var_def
2.416 + UN_equiv_class [OF equiv_exprel discrim_respects])
2.417 +
2.418 +lemma discrim_Plus [simp]: "discrim (Plus X Y) = 1"
2.419 +apply (cases X, cases Y)
2.420 +apply (simp add: discrim_def Plus
2.421 + UN_equiv_class [OF equiv_exprel discrim_respects])
2.422 +done
2.423 +
2.424 +lemma discrim_FnCall [simp]: "discrim (FnCall F Xs) = 2"
2.425 +apply (rule_tac z=Xs in eq_Abs_ExpList)
2.426 +apply (simp add: discrim_def FnCall
2.427 + UN_equiv_class [OF equiv_exprel discrim_respects])
2.428 +done
2.429 +
2.430 +
2.431 +text{*The structural induction rule for the abstract type*}
2.432 +theorem exp_induct:
2.433 + assumes V: "\<And>nat. P1 (Var nat)"
2.434 + and P: "\<And>exp1 exp2. \<lbrakk>P1 exp1; P1 exp2\<rbrakk> \<Longrightarrow> P1 (Plus exp1 exp2)"
2.435 + and F: "\<And>nat list. P2 list \<Longrightarrow> P1 (FnCall nat list)"
2.436 + and Nil: "P2 []"
2.437 + and Cons: "\<And>exp list. \<lbrakk>P1 exp; P2 list\<rbrakk> \<Longrightarrow> P2 (exp # list)"
2.438 + shows "P1 exp & P2 list"
2.439 +proof (cases exp, rule eq_Abs_ExpList [of list], clarify)
2.440 + fix U Us
2.441 + show "P1 (Abs_Exp (exprel `` {U})) \<and>
2.442 + P2 (Abs_ExpList Us)"
2.443 + proof (induct U and Us)
2.444 + case (VAR nat)
2.445 + with V show ?case by (simp add: Var_def)
2.446 + next
2.447 + case (PLUS X Y)
2.448 + with P [of "Abs_Exp (exprel `` {X})" "Abs_Exp (exprel `` {Y})"]
2.449 + show ?case by (simp add: Plus)
2.450 + next
2.451 + case (FNCALL nat list)
2.452 + with F [of "Abs_ExpList list"]
2.453 + show ?case by (simp add: FnCall)
2.454 + next
2.455 + case Nil_freeExp
2.456 + with Nil show ?case by simp
2.457 + next
2.458 + case Cons_freeExp
2.459 + with Cons
2.460 + show ?case by simp
2.461 + qed
2.462 +qed
2.463 +
2.464 +end
2.465 +
3.1 --- a/src/HOL/Induct/ROOT.ML Thu Sep 02 14:50:00 2004 +0200
3.2 +++ b/src/HOL/Induct/ROOT.ML Thu Sep 02 16:52:21 2004 +0200
3.3 @@ -1,6 +1,7 @@
3.4
3.5 time_use_thy "Mutil";
3.6 time_use_thy "QuoDataType";
3.7 +time_use_thy "QuoNestedDataType";
3.8 time_use_thy "Term";
3.9 time_use_thy "ABexp";
3.10 time_use_thy "Tree";
4.1 --- a/src/HOL/IsaMakefile Thu Sep 02 14:50:00 2004 +0200
4.2 +++ b/src/HOL/IsaMakefile Thu Sep 02 16:52:21 2004 +0200
4.3 @@ -209,7 +209,8 @@
4.4 $(LOG)/HOL-Induct.gz: $(OUT)/HOL \
4.5 Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \
4.6 Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \
4.7 - Induct/PropLog.thy Induct/QuoDataType.thy Induct/ROOT.ML \
4.8 + Induct/PropLog.thy Induct/QuoNestedDataType.thy Induct/QuoDataType.thy\
4.9 + Induct/ROOT.ML \
4.10 Induct/Sexp.thy Induct/Sigma_Algebra.thy \
4.11 Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \
4.12 Induct/Tree.thy Induct/document/root.tex