# HG changeset patch # User wenzelm # Date 1135207723 -3600 # Node ID 9a1458cb295618f703bcdf714331faa72f8732b9 # Parent 2b102759160da870677dc2ad2aba795ad6f88257 tuned induct proofs; diff -r 2b102759160d -r 9a1458cb2956 src/HOL/Induct/QuoDataType.thy --- a/src/HOL/Induct/QuoDataType.thy Thu Dec 22 00:28:41 2005 +0100 +++ b/src/HOL/Induct/QuoDataType.thy Thu Dec 22 00:28:43 2005 +0100 @@ -49,13 +49,14 @@ text{*Proving that it is an equivalence relation*} lemma msgrel_refl: "X \ X" -by (induct X, (blast intro: msgrel.intros)+) + by (induct X) (blast intro: msgrel.intros)+ theorem equiv_msgrel: "equiv UNIV msgrel" -proof (simp add: equiv_def, intro conjI) - show "reflexive msgrel" by (simp add: refl_def msgrel_refl) - show "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM) - show "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS) +proof - + have "reflexive msgrel" by (simp add: refl_def msgrel_refl) + moreover have "sym msgrel" by (simp add: sym_def, blast intro: msgrel.SYM) + moreover have "trans msgrel" by (simp add: trans_def, blast intro: msgrel.TRANS) + ultimately show ?thesis by (simp add: equiv_def) qed @@ -78,7 +79,7 @@ equivalence relation. It also helps us prove that Nonce (the abstract constructor) is injective*} theorem msgrel_imp_eq_freenonces: "U \ V \ freenonces U = freenonces V" -by (erule msgrel.induct, auto) + by (induct set: msgrel) auto subsubsection{*The Left Projection*} @@ -97,7 +98,7 @@ (the abstract constructor) is injective*} theorem msgrel_imp_eqv_freeleft: "U \ V \ freeleft U \ freeleft V" -by (erule msgrel.induct, auto intro: msgrel.intros) + by (induct set: msgrel) (auto intro: msgrel.intros) subsubsection{*The Right Projection*} @@ -115,7 +116,7 @@ (the abstract constructor) is injective*} theorem msgrel_imp_eqv_freeright: "U \ V \ freeright U \ freeright V" -by (erule msgrel.induct, auto intro: msgrel.intros) + by (induct set: msgrel) (auto intro: msgrel.intros) subsubsection{*The Discriminator for Constructors*} @@ -131,13 +132,13 @@ text{*This theorem helps us prove @{term "Nonce N \ MPair X Y"}*} theorem msgrel_imp_eq_freediscrim: "U \ V \ freediscrim U = freediscrim V" -by (erule msgrel.induct, auto) + by (induct set: msgrel) auto subsection{*The Initial Algebra: A Quotiented Message Type*} typedef (Msg) msg = "UNIV//msgrel" - by (auto simp add: quotient_def) + by (auto simp add: quotient_def) text{*The abstract message constructors*} @@ -402,9 +403,9 @@ and C: "\K X. P X \ P (Crypt K X)" and D: "\K X. P X \ P (Decrypt K X)" shows "P msg" -proof (cases msg, erule ssubst) - fix U::freemsg - show "P (Abs_Msg (msgrel `` {U}))" +proof (cases msg) + case (Abs_Msg U) + have "P (Abs_Msg (msgrel `` {U}))" proof (induct U) case (NONCE N) with N show ?case by (simp add: Nonce_def) @@ -421,6 +422,7 @@ with D [of "Abs_Msg (msgrel `` {X})"] show ?case by (simp add: Decrypt) qed + with Abs_Msg show ?thesis by (simp only:) qed diff -r 2b102759160d -r 9a1458cb2956 src/HOL/Induct/QuoNestedDataType.thy --- a/src/HOL/Induct/QuoNestedDataType.thy Thu Dec 22 00:28:41 2005 +0100 +++ b/src/HOL/Induct/QuoNestedDataType.thy Thu Dec 22 00:28:43 2005 +0100 @@ -45,23 +45,20 @@ text{*Proving that it is an equivalence relation*} -lemma exprel_refl_conj: "X \ X & (Xs,Xs) \ listrel(exprel)" -apply (induct X and Xs) -apply (blast intro: exprel.intros listrel.intros)+ -done - -lemmas exprel_refl = exprel_refl_conj [THEN conjunct1] -lemmas list_exprel_refl = exprel_refl_conj [THEN conjunct2] +lemma exprel_refl: "X \ X" + and list_exprel_refl: "(Xs,Xs) \ listrel(exprel)" + by (induct X and Xs) (blast intro: exprel.intros listrel.intros)+ theorem equiv_exprel: "equiv UNIV exprel" -proof (simp add: equiv_def, intro conjI) - show "reflexive exprel" by (simp add: refl_def exprel_refl) - show "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM) - show "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS) +proof - + have "reflexive exprel" by (simp add: refl_def exprel_refl) + moreover have "sym exprel" by (simp add: sym_def, blast intro: exprel.SYM) + moreover have "trans exprel" by (simp add: trans_def, blast intro: exprel.TRANS) + ultimately show ?thesis by (simp add: equiv_def) qed theorem equiv_list_exprel: "equiv UNIV (listrel exprel)" -by (insert equiv_listrel [OF equiv_exprel], simp) + using equiv_listrel [OF equiv_exprel] by simp lemma FNCALL_Nil: "FNCALL F [] \ FNCALL F []" @@ -100,7 +97,7 @@ equivalence relation. It also helps us prove that Variable (the abstract constructor) is injective*} theorem exprel_imp_eq_freevars: "U \ V \ freevars U = freevars V" -apply (erule exprel.induct) +apply (induct set: exprel) apply (erule_tac [4] listrel.induct) apply (simp_all add: Un_assoc) done @@ -118,7 +115,7 @@ theorem exprel_imp_eq_freediscrim: "U \ V \ freediscrim U = freediscrim V" -by (erule exprel.induct, auto) + by (induct set: exprel) auto text{*This function, which returns the function name, is used to @@ -132,7 +129,7 @@ theorem exprel_imp_eq_freefun: "U \ V \ freefun U = freefun V" -by (erule exprel.induct, simp_all add: listrel.intros) + by (induct set: exprel) (simp_all add: listrel.intros) text{*This function, which returns the list of function arguments, is used to @@ -145,7 +142,7 @@ theorem exprel_imp_eqv_freeargs: "U \ V \ (freeargs U, freeargs V) \ listrel exprel" -apply (erule exprel.induct) +apply (induct set: exprel) apply (erule_tac [4] listrel.induct) apply (simp_all add: listrel.intros) apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]]) @@ -265,7 +262,7 @@ lemma listset_Rep_Exp_Abs_Exp: "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}"; -by (induct Us, simp_all add: listrel_Cons Abs_ExpList_def) + by (induct Us) (simp_all add: listrel_Cons Abs_ExpList_def) lemma FnCall: "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})" @@ -372,7 +369,7 @@ relations, but with little benefit here.*} lemma Abs_ExpList_eq: "(y, z) \ listrel exprel \ Abs_ExpList (y) = Abs_ExpList (z)" -by (erule listrel.induct, simp_all) + by (induct set: listrel) simp_all lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel" by (simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) @@ -426,19 +423,19 @@ text{*The structural induction rule for the abstract type*} -theorem exp_induct: +theorem exp_inducts: assumes V: "\nat. P1 (Var nat)" and P: "\exp1 exp2. \P1 exp1; P1 exp2\ \ P1 (Plus exp1 exp2)" and F: "\nat list. P2 list \ P1 (FnCall nat list)" and Nil: "P2 []" and Cons: "\exp list. \P1 exp; P2 list\ \ P2 (exp # list)" - shows "P1 exp & P2 list" -proof (cases exp, rule eq_Abs_ExpList [of list], clarify) - fix U Us - show "P1 (Abs_Exp (exprel `` {U})) \ - P2 (Abs_ExpList Us)" + shows "P1 exp" and "P2 list" +proof - + obtain U where exp: "exp = (Abs_Exp (exprel `` {U}))" by (cases exp) + obtain Us where list: "list = Abs_ExpList Us" by (rule eq_Abs_ExpList) + have "P1 (Abs_Exp (exprel `` {U}))" and "P2 (Abs_ExpList Us)" proof (induct U and Us) - case (VAR nat) + case (VAR nat) with V show ?case by (simp add: Var_def) next case (PLUS X Y) @@ -453,9 +450,9 @@ with Nil show ?case by simp next case Cons_freeExp - with Cons - show ?case by simp + with Cons show ?case by simp qed + with exp and list show "P1 exp" and "P2 list" by (simp_all only:) qed end diff -r 2b102759160d -r 9a1458cb2956 src/HOL/Isar_examples/NestedDatatype.thy --- a/src/HOL/Isar_examples/NestedDatatype.thy Thu Dec 22 00:28:41 2005 +0100 +++ b/src/HOL/Isar_examples/NestedDatatype.thy Thu Dec 22 00:28:43 2005 +0100 @@ -27,10 +27,9 @@ \medskip A simple lemma about composition of substitutions. *} -lemma - "subst_term (subst_term f1 o f2) t = - subst_term f1 (subst_term f2 t) & - subst_term_list (subst_term f1 o f2) ts = +lemma "subst_term (subst_term f1 o f2) t = + subst_term f1 (subst_term f2 t)" + and "subst_term_list (subst_term f1 o f2) ts = subst_term_list f1 (subst_term_list f2 ts)" by (induct t and ts) simp_all diff -r 2b102759160d -r 9a1458cb2956 src/HOL/Lambda/Eta.thy --- a/src/HOL/Lambda/Eta.thy Thu Dec 22 00:28:41 2005 +0100 +++ b/src/HOL/Lambda/Eta.thy Thu Dec 22 00:28:43 2005 +0100 @@ -392,47 +392,46 @@ *} theorem par_eta_beta: "s \\<^sub>\ t \ t => u \ \t'. s => t' \ t' \\<^sub>\ u" -proof (induct t fixing: s u - rule: measure_induct [of size, rule_format]) - case (1 t) - from 1(3) +proof (induct t fixing: s u taking: "size :: dB \ nat" rule: measure_induct_rule) + case (less t) + from `t => u` show ?case proof cases case (var n) - with 1 show ?thesis + with less show ?thesis by (auto intro: par_beta_refl) next case (abs r' r'') - with 1 have "s \\<^sub>\ Abs r'" by simp + with less have "s \\<^sub>\ Abs r'" by simp then obtain r k where s: "s = eta_expand k (Abs r)" and rr: "r \\<^sub>\ r'" by (blast dest: par_eta_elim_abs) from abs have "size r' < size t" by simp with abs(2) rr obtain t' where rt: "r => t'" and t': "t' \\<^sub>\ r''" - by (blast dest: 1) + by (blast dest: less) with s abs show ?thesis by (auto intro: eta_expand_red eta_expand_eta) next case (app q' q'' r' r'') - with 1 have "s \\<^sub>\ q' \ r'" by simp + with less have "s \\<^sub>\ q' \ r'" by simp then obtain q r k where s: "s = eta_expand k (q \ r)" and qq: "q \\<^sub>\ q'" and rr: "r \\<^sub>\ r'" by (blast dest: par_eta_elim_app [OF _ refl]) from app have "size q' < size t" and "size r' < size t" by simp_all with app(2,3) qq rr obtain t' t'' where "q => t'" and "t' \\<^sub>\ q''" and "r => t''" and "t'' \\<^sub>\ r''" - by (blast dest: 1) + by (blast dest: less) with s app show ?thesis by (fastsimp intro: eta_expand_red eta_expand_eta) next case (beta q' q'' r' r'') - with 1 have "s \\<^sub>\ Abs q' \ r'" by simp + with less have "s \\<^sub>\ Abs q' \ r'" by simp then obtain q r k k' where s: "s = eta_expand k (eta_expand k' (Abs q) \ r)" and qq: "q \\<^sub>\ q'" and rr: "r \\<^sub>\ r'" by (blast dest: par_eta_elim_app par_eta_elim_abs) from beta have "size q' < size t" and "size r' < size t" by simp_all with beta(2,3) qq rr obtain t' t'' where "q => t'" and "t' \\<^sub>\ q''" and "r => t''" and "t'' \\<^sub>\ r''" - by (blast dest: 1) + by (blast dest: less) with s beta show ?thesis by (auto intro: eta_expand_red eta_expand_beta eta_expand_eta par_eta_subst) qed diff -r 2b102759160d -r 9a1458cb2956 src/ZF/Induct/Tree_Forest.thy --- a/src/ZF/Induct/Tree_Forest.thy Thu Dec 22 00:28:41 2005 +0100 +++ b/src/ZF/Induct/Tree_Forest.thy Thu Dec 22 00:28:43 2005 +0100 @@ -18,6 +18,12 @@ datatype "tree(A)" = Tcons ("a \ A", "f \ forest(A)") and "forest(A)" = Fnil | Fcons ("t \ tree(A)", "f \ forest(A)") +(* FIXME *) +lemmas tree'induct = + tree_forest.mutual_induct [THEN conjunct1, THEN spec, THEN [2] rev_mp, of concl: _ t, standard, consumes 1] + and forest'induct = + tree_forest.mutual_induct [THEN conjunct2, THEN spec, THEN [2] rev_mp, of concl: _ f, standard, consumes 1] + declare tree_forest.intros [simp, TC] lemma tree_def: "tree(A) == Part(tree_forest(A), Inl)" @@ -158,36 +164,28 @@ lemma list_of_TF_type [TC]: "z \ tree_forest(A) ==> list_of_TF(z) \ list(tree(A))" - apply (erule tree_forest.induct) - apply simp_all - done + by (induct set: tree_forest) simp_all lemma of_list_type [TC]: "l \ list(tree(A)) ==> of_list(l) \ forest(A)" - apply (erule list.induct) - apply simp_all - done + by (induct set: list) simp_all text {* \medskip @{text map}. *} lemma - assumes h_type: "!!x. x \ A ==> h(x): B" + assumes "!!x. x \ A ==> h(x): B" shows map_tree_type: "t \ tree(A) ==> map(h,t) \ tree(B)" and map_forest_type: "f \ forest(A) ==> map(h,f) \ forest(B)" - apply (induct rule: tree_forest.mutual_induct) - apply (insert h_type) - apply simp_all - done + using prems + by (induct rule: tree'induct forest'induct) simp_all text {* \medskip @{text size}. *} lemma size_type [TC]: "z \ tree_forest(A) ==> size(z) \ nat" - apply (erule tree_forest.induct) - apply simp_all - done + by (induct set: tree_forest) simp_all text {* @@ -195,9 +193,7 @@ *} lemma preorder_type [TC]: "z \ tree_forest(A) ==> preorder(z) \ list(A)" - apply (erule tree_forest.induct) - apply simp_all - done + by (induct set: tree_forest) simp_all text {* @@ -229,15 +225,11 @@ *} lemma map_ident: "z \ tree_forest(A) ==> map(\u. u, z) = z" - apply (erule tree_forest.induct) - apply simp_all - done + by (induct set: tree_forest) simp_all lemma map_compose: "z \ tree_forest(A) ==> map(h, map(j,z)) = map(\u. h(j(u)), z)" - apply (erule tree_forest.induct) - apply simp_all - done + by (induct set: tree_forest) simp_all text {* @@ -245,14 +237,10 @@ *} lemma size_map: "z \ tree_forest(A) ==> size(map(h,z)) = size(z)" - apply (erule tree_forest.induct) - apply simp_all - done + by (induct set: tree_forest) simp_all lemma size_length: "z \ tree_forest(A) ==> size(z) = length(preorder(z))" - apply (erule tree_forest.induct) - apply (simp_all add: length_app) - done + by (induct set: tree_forest) (simp_all add: length_app) text {* \medskip Theorems about @{text preorder}. @@ -260,8 +248,6 @@ lemma preorder_map: "z \ tree_forest(A) ==> preorder(map(h,z)) = List.map(h, preorder(z))" - apply (erule tree_forest.induct) - apply (simp_all add: map_app_distrib) - done + by (induct set: tree_forest) (simp_all add: map_app_distrib) end