# HG changeset patch # User paulson # Date 1647447262 0 # Node ID 7add2d5322a7a198447b5524c076bd13bd9ffbc5 # Parent 29ee987174c02e8a2bfc4ddf7ad52af8ce5672f0 Tidied several ugly proofs in some elderly examples diff -r 29ee987174c0 -r 7add2d5322a7 src/HOL/Induct/QuoDataType.thy --- a/src/HOL/Induct/QuoDataType.thy Tue Mar 15 14:15:11 2022 +0100 +++ b/src/HOL/Induct/QuoDataType.thy Wed Mar 16 16:14:22 2022 +0000 @@ -5,6 +5,11 @@ section\Defining an Initial Algebra by Quotienting a Free Algebra\ +text \For Lawrence Paulson's paper ``Defining functions on equivalence classes'' +\emph{ACM Transactions on Computational Logic} \textbf{7}:40 (2006), 658--675, +illustrating bare-bones quotient constructions. Any comparison using lifting and transfer +should be done in a separate theory.\ + theory QuoDataType imports Main begin subsection\Defining the Free Algebra\ @@ -163,9 +168,7 @@ by (auto simp add: Msg_def quotient_def intro: msgrel_refl) lemma inj_on_Abs_Msg: "inj_on Abs_Msg Msg" -apply (rule inj_on_inverseI) -apply (erule Abs_Msg_inverse) -done + by (meson Abs_Msg_inject inj_onI) text\Reduces equality on abstractions to equality on representatives\ declare inj_on_Abs_Msg [THEN inj_on_eq_iff, simp] @@ -203,11 +206,8 @@ text\Case analysis on the representation of a msg as an equivalence class.\ lemma eq_Abs_Msg [case_names Abs_Msg, cases type: msg]: - "(!!U. z = Abs_Msg(msgrel``{U}) ==> P) ==> P" -apply (rule Rep_Msg [of z, unfolded Msg_def, THEN quotientE]) -apply (drule arg_cong [where f=Abs_Msg]) -apply (auto simp add: Rep_Msg_inverse intro: msgrel_refl) -done + "(\U. z = Abs_Msg (msgrel `` {U}) \ P) \ P" + by (metis Abs_Msg_cases Msg_def quotientE) text\Establishing these two equations is the point of the whole exercise\ theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X" @@ -234,32 +234,40 @@ UN_equiv_class [OF equiv_msgrel nonces_congruent]) lemma nonces_MPair [simp]: "nonces (MPair X Y) = nonces X \ nonces Y" -apply (cases X, cases Y) -apply (simp add: nonces_def MPair - UN_equiv_class [OF equiv_msgrel nonces_congruent]) -done +proof - + have "\U V. \X = Abs_Msg (msgrel `` {U}); Y = Abs_Msg (msgrel `` {V})\ + \ nonces (MPair X Y) = nonces X \ nonces Y" + by (simp add: nonces_def MPair + UN_equiv_class [OF equiv_msgrel nonces_congruent]) + then show ?thesis + by (meson eq_Abs_Msg) +qed lemma nonces_Crypt [simp]: "nonces (Crypt K X) = nonces X" -apply (cases X) -apply (simp add: nonces_def Crypt - UN_equiv_class [OF equiv_msgrel nonces_congruent]) -done +proof - + have "\U. X = Abs_Msg (msgrel `` {U}) \ nonces (Crypt K X) = nonces X" + by (simp add: nonces_def Crypt UN_equiv_class [OF equiv_msgrel nonces_congruent]) + then show ?thesis + by (meson eq_Abs_Msg) +qed lemma nonces_Decrypt [simp]: "nonces (Decrypt K X) = nonces X" -apply (cases X) -apply (simp add: nonces_def Decrypt - UN_equiv_class [OF equiv_msgrel nonces_congruent]) -done +proof - + have "\U. X = Abs_Msg (msgrel `` {U}) \ nonces (Decrypt K X) = nonces X" + by (simp add: nonces_def Decrypt UN_equiv_class [OF equiv_msgrel nonces_congruent]) + then show ?thesis + by (meson eq_Abs_Msg) +qed subsection\The Abstract Function to Return the Left Part\ definition - left :: "msg \ msg" where - "left X = Abs_Msg (\U \ Rep_Msg X. msgrel``{freeleft U})" + left :: "msg \ msg" + where "left X = Abs_Msg (\U \ Rep_Msg X. msgrel``{freeleft U})" lemma left_congruent: "(\U. msgrel `` {freeleft U}) respects msgrel" -by (auto simp add: congruent_def msgrel_imp_eqv_freeleft) + by (auto simp add: congruent_def msgrel_imp_eqv_freeleft) text\Now prove the four equations for \<^term>\left\\ @@ -268,69 +276,51 @@ UN_equiv_class [OF equiv_msgrel left_congruent]) lemma left_MPair [simp]: "left (MPair X Y) = X" -apply (cases X, cases Y) -apply (simp add: left_def MPair - UN_equiv_class [OF equiv_msgrel left_congruent]) -done + by (cases X, cases Y) (simp add: left_def MPair UN_equiv_class [OF equiv_msgrel left_congruent]) lemma left_Crypt [simp]: "left (Crypt K X) = left X" -apply (cases X) -apply (simp add: left_def Crypt - UN_equiv_class [OF equiv_msgrel left_congruent]) -done + by (cases X) (simp add: left_def Crypt UN_equiv_class [OF equiv_msgrel left_congruent]) lemma left_Decrypt [simp]: "left (Decrypt K X) = left X" -apply (cases X) -apply (simp add: left_def Decrypt - UN_equiv_class [OF equiv_msgrel left_congruent]) -done + by (metis CD_eq left_Crypt) subsection\The Abstract Function to Return the Right Part\ definition - right :: "msg \ msg" where - "right X = Abs_Msg (\U \ Rep_Msg X. msgrel``{freeright U})" + right :: "msg \ msg" + where "right X = Abs_Msg (\U \ Rep_Msg X. msgrel``{freeright U})" lemma right_congruent: "(\U. msgrel `` {freeright U}) respects msgrel" -by (auto simp add: congruent_def msgrel_imp_eqv_freeright) + by (auto simp add: congruent_def msgrel_imp_eqv_freeright) text\Now prove the four equations for \<^term>\right\\ lemma right_Nonce [simp]: "right (Nonce N) = Nonce N" -by (simp add: right_def Nonce_def - UN_equiv_class [OF equiv_msgrel right_congruent]) + by (simp add: right_def Nonce_def + UN_equiv_class [OF equiv_msgrel right_congruent]) lemma right_MPair [simp]: "right (MPair X Y) = Y" -apply (cases X, cases Y) -apply (simp add: right_def MPair - UN_equiv_class [OF equiv_msgrel right_congruent]) -done + by (cases X, cases Y) (simp add: right_def MPair UN_equiv_class [OF equiv_msgrel right_congruent]) lemma right_Crypt [simp]: "right (Crypt K X) = right X" -apply (cases X) -apply (simp add: right_def Crypt - UN_equiv_class [OF equiv_msgrel right_congruent]) -done + by (cases X) (simp add: right_def Crypt UN_equiv_class [OF equiv_msgrel right_congruent]) lemma right_Decrypt [simp]: "right (Decrypt K X) = right X" -apply (cases X) -apply (simp add: right_def Decrypt - UN_equiv_class [OF equiv_msgrel right_congruent]) -done + by (metis CD_eq right_Crypt) subsection\Injectivity Properties of Some Constructors\ lemma NONCE_imp_eq: "NONCE m \ NONCE n \ m = n" -by (drule msgrel_imp_eq_freenonces, simp) + by (drule msgrel_imp_eq_freenonces, simp) text\Can also be proved using the function \<^term>\nonces\\ lemma Nonce_Nonce_eq [iff]: "(Nonce m = Nonce n) = (m = n)" -by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq) + by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq) lemma MPAIR_imp_eqv_left: "MPAIR X Y \ MPAIR X' Y' \ X \ X'" -by (drule msgrel_imp_eqv_freeleft, simp) + by (drule msgrel_imp_eqv_freeleft, simp) lemma MPair_imp_eq_left: assumes eq: "MPair X Y = MPair X' Y'" shows "X = X'" @@ -341,33 +331,27 @@ qed lemma MPAIR_imp_eqv_right: "MPAIR X Y \ MPAIR X' Y' \ Y \ Y'" -by (drule msgrel_imp_eqv_freeright, simp) + by (drule msgrel_imp_eqv_freeright, simp) -lemma MPair_imp_eq_right: "MPair X Y = MPair X' Y' \ Y = Y'" -apply (cases X, cases X', cases Y, cases Y') -apply (simp add: MPair) -apply (erule MPAIR_imp_eqv_right) -done +lemma MPair_imp_eq_right: "MPair X Y = MPair X' Y' \ Y = Y'" + by (metis right_MPair) theorem MPair_MPair_eq [iff]: "(MPair X Y = MPair X' Y') = (X=X' & Y=Y')" -by (blast dest: MPair_imp_eq_left MPair_imp_eq_right) + by (blast dest: MPair_imp_eq_left MPair_imp_eq_right) lemma NONCE_neqv_MPAIR: "NONCE m \ MPAIR X Y \ False" -by (drule msgrel_imp_eq_freediscrim, simp) + by (drule msgrel_imp_eq_freediscrim, simp) theorem Nonce_neq_MPair [iff]: "Nonce N \ MPair X Y" -apply (cases X, cases Y) -apply (simp add: Nonce_def MPair) -apply (blast dest: NONCE_neqv_MPAIR) -done + by (cases X, cases Y) (use MPair NONCE_neqv_MPAIR Nonce_def in fastforce) text\Example suggested by a referee\ theorem Crypt_Nonce_neq_Nonce: "Crypt K (Nonce M) \ Nonce N" -by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim) + by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim) text\...and many similar results\ theorem Crypt2_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) \ Nonce N" -by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim) + by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim) theorem Crypt_Crypt_eq [iff]: "(Crypt K X = Crypt K X') = (X=X')" proof @@ -428,32 +412,27 @@ "discrim X = the_elem (\U \ Rep_Msg X. {freediscrim U})" lemma discrim_congruent: "(\U. {freediscrim U}) respects msgrel" -by (auto simp add: congruent_def msgrel_imp_eq_freediscrim) + by (auto simp add: congruent_def msgrel_imp_eq_freediscrim) text\Now prove the four equations for \<^term>\discrim\\ lemma discrim_Nonce [simp]: "discrim (Nonce N) = 0" -by (simp add: discrim_def Nonce_def - UN_equiv_class [OF equiv_msgrel discrim_congruent]) + by (simp add: discrim_def Nonce_def + UN_equiv_class [OF equiv_msgrel discrim_congruent]) lemma discrim_MPair [simp]: "discrim (MPair X Y) = 1" -apply (cases X, cases Y) -apply (simp add: discrim_def MPair - UN_equiv_class [OF equiv_msgrel discrim_congruent]) -done +proof - + have "\U V. discrim (MPair (Abs_Msg (msgrel `` {U})) (Abs_Msg (msgrel `` {V}))) = 1" + by (simp add: discrim_def MPair UN_equiv_class [OF equiv_msgrel discrim_congruent]) + then show ?thesis + by (metis eq_Abs_Msg) +qed lemma discrim_Crypt [simp]: "discrim (Crypt K X) = discrim X + 2" -apply (cases X) -apply (simp add: discrim_def Crypt - UN_equiv_class [OF equiv_msgrel discrim_congruent]) -done + by (cases X) (use Crypt UN_equiv_class discrim_congruent discrim_def equiv_msgrel in fastforce) lemma discrim_Decrypt [simp]: "discrim (Decrypt K X) = discrim X - 2" -apply (cases X) -apply (simp add: discrim_def Decrypt - UN_equiv_class [OF equiv_msgrel discrim_congruent]) -done - + by (cases X) (use Decrypt UN_equiv_class discrim_congruent discrim_def equiv_msgrel in fastforce) end diff -r 29ee987174c0 -r 7add2d5322a7 src/HOL/Induct/QuoNestedDataType.thy --- a/src/HOL/Induct/QuoNestedDataType.thy Tue Mar 15 14:15:11 2022 +0100 +++ b/src/HOL/Induct/QuoNestedDataType.thy Wed Mar 16 16:14:22 2022 +0000 @@ -5,6 +5,11 @@ section\Quotienting a Free Algebra Involving Nested Recursion\ +text \This is the development promised in Lawrence Paulson's paper ``Defining functions on equivalence classes'' +\emph{ACM Transactions on Computational Logic} \textbf{7}:40 (2006), 658--675, +illustrating bare-bones quotient constructions. Any comparison using lifting and transfer +should be done in a separate theory.\ + theory QuoNestedDataType imports Main begin subsection\Defining the Free Algebra\ @@ -26,7 +31,7 @@ exprel :: "(freeExp * freeExp) set" and exp_rel :: "[freeExp, freeExp] => bool" (infixl "\" 50) where - "X \ Y == (X,Y) \ exprel" + "X \ Y \ (X,Y) \ exprel" | ASSOC: "PLUS X (PLUS Y Z) \ PLUS (PLUS X Y) Z" | VAR: "VAR N \ VAR N" | PLUS: "\X \ X'; Y \ Y'\ \ PLUS X Y \ PLUS X' Y'" @@ -54,17 +59,9 @@ theorem equiv_list_exprel: "equiv UNIV (listrel exprel)" using equiv_listrel [OF equiv_exprel] by simp - -lemma FNCALL_Nil: "FNCALL F [] \ FNCALL F []" -apply (rule exprel.intros) -apply (rule listrel.intros) -done - lemma FNCALL_Cons: - "\X \ X'; (Xs,Xs') \ listrel(exprel)\ - \ FNCALL F (X#Xs) \ FNCALL F (X'#Xs')" -by (blast intro: exprel.intros listrel.intros) - + "\X \ X'; (Xs,Xs') \ listrel(exprel)\ \ FNCALL F (X#Xs) \ FNCALL F (X'#Xs')" + by (blast intro: exprel.intros listrel.intros) subsection\Some Functions on the Free Algebra\ @@ -75,8 +72,8 @@ be lifted to the initial algebra, to serve as an example of that process. Note that the "free" refers to the free datatype rather than to the concept of a free variable.\ -primrec freevars :: "freeExp \ nat set" - and freevars_list :: "freeExp list \ nat set" where +primrec freevars :: "freeExp \ nat set" and freevars_list :: "freeExp list \ nat set" + where "freevars (VAR N) = {N}" | "freevars (PLUS X Y) = freevars X \ freevars Y" | "freevars (FNCALL F Xs) = freevars_list Xs" @@ -88,11 +85,11 @@ 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 (induct set: exprel) -apply (erule_tac [4] listrel.induct) -apply (simp_all add: Un_assoc) -done - +proof (induct set: exprel) + case (FNCALL Xs Xs' F) + then show ?case + by (induct rule: listrel.induct) auto +qed (simp_all add: Un_assoc) subsubsection\Functions for Freeness\ @@ -127,20 +124,24 @@ | "freeargs (PLUS X Y) = []" | "freeargs (FNCALL F Xs) = Xs" + theorem exprel_imp_eqv_freeargs: assumes "U \ V" shows "(freeargs U, freeargs V) \ listrel exprel" -proof - - from equiv_list_exprel have sym: "sym (listrel exprel)" by (rule equivE) - from equiv_list_exprel have trans: "trans (listrel exprel)" by (rule equivE) - from assms show ?thesis - apply induct - apply (erule_tac [4] listrel.induct) - apply (simp_all add: listrel.intros) - apply (blast intro: symD [OF sym]) - apply (blast intro: transD [OF trans]) - done -qed + using assms +proof induction + case (FNCALL Xs Xs' F) + then show ?case + by (simp add: listrel_iff_nth) +next + case (SYM X Y) + then show ?case + by (meson equivE equiv_list_exprel symD) +next + case (TRANS X Y Z) + then show ?case + by (meson equivE equiv_list_exprel transD) +qed (use listrel.simps in auto) subsection\The Initial Algebra: A Quotiented Message Type\ @@ -165,24 +166,22 @@ definition FnCall :: "[nat, exp list] \ exp" where "FnCall F Xs = - Abs_Exp (\Us \ listset (map Rep_Exp Xs). exprel `` {FNCALL F Us})" + Abs_Exp (\Us \ listset (map Rep_Exp Xs). exprel``{FNCALL F Us})" text\Reduces equality of equivalence classes to the \<^term>\exprel\ relation: - \<^term>\(exprel `` {x} = exprel `` {y}) = ((x,y) \ exprel)\\ + \<^term>\(exprel``{x} = exprel``{y}) = ((x,y) \ exprel)\\ lemmas equiv_exprel_iff = eq_equiv_class_iff [OF equiv_exprel UNIV_I UNIV_I] declare equiv_exprel_iff [simp] text\All equivalence classes belong to set of representatives\ -lemma [simp]: "exprel``{U} \ Exp" -by (auto simp add: Exp_def quotient_def intro: exprel_refl) +lemma exprel_in_Exp [simp]: "exprel``{U} \ Exp" + by (simp add: Exp_def quotientI) lemma inj_on_Abs_Exp: "inj_on Abs_Exp Exp" -apply (rule inj_on_inverseI) -apply (erule Abs_Exp_inverse) -done + by (meson Abs_Exp_inject inj_onI) text\Reduces equality on abstractions to equality on representatives\ declare inj_on_Abs_Exp [THEN inj_on_eq_iff, simp] @@ -192,11 +191,8 @@ text\Case analysis on the representation of a exp as an equivalence class.\ lemma eq_Abs_Exp [case_names Abs_Exp, cases type: exp]: - "(!!U. z = Abs_Exp(exprel``{U}) ==> P) ==> P" -apply (rule Rep_Exp [of z, unfolded Exp_def, THEN quotientE]) -apply (drule arg_cong [where f=Abs_Exp]) -apply (auto simp add: Rep_Exp_inverse intro: exprel_refl) -done + "(\U. z = Abs_Exp (exprel``{U}) \ P) \ P" + by (metis Abs_Exp_cases Exp_def quotientE) subsection\Every list of abstract expressions can be expressed in terms of a @@ -204,25 +200,17 @@ definition Abs_ExpList :: "freeExp list => exp list" where - "Abs_ExpList Xs = map (%U. Abs_Exp(exprel``{U})) Xs" + "Abs_ExpList Xs \ map (\U. Abs_Exp(exprel``{U})) Xs" -lemma Abs_ExpList_Nil [simp]: "Abs_ExpList [] == []" -by (simp add: Abs_ExpList_def) +lemma Abs_ExpList_Nil [simp]: "Abs_ExpList [] = []" + by (simp add: Abs_ExpList_def) lemma Abs_ExpList_Cons [simp]: - "Abs_ExpList (X#Xs) == Abs_Exp (exprel``{X}) # Abs_ExpList Xs" -by (simp add: Abs_ExpList_def) + "Abs_ExpList (X#Xs) = Abs_Exp (exprel``{X}) # Abs_ExpList Xs" + by (simp add: Abs_ExpList_def) lemma ExpList_rep: "\Us. z = Abs_ExpList Us" -apply (induct z) -apply (rename_tac [2] a b) -apply (rule_tac [2] z=a in eq_Abs_Exp) -apply (auto simp add: Abs_ExpList_def Cons_eq_map_conv intro: exprel_refl) -done - -lemma eq_Abs_ExpList [case_names Abs_ExpList]: - "(!!Us. z = Abs_ExpList Us ==> P) ==> P" -by (rule exE [OF ExpList_rep], blast) + by (smt (verit, del_insts) Abs_ExpList_def eq_Abs_Exp ex_map_conv) subsubsection\Characteristic Equations for the Abstract Constructors\ @@ -230,7 +218,7 @@ lemma Plus: "Plus (Abs_Exp(exprel``{U})) (Abs_Exp(exprel``{V})) = Abs_Exp (exprel``{PLUS U V})" proof - - have "(\U V. exprel `` {PLUS U V}) respects2 exprel" + have "(\U V. exprel``{PLUS U V}) respects2 exprel" by (auto simp add: congruent2_def exprel.PLUS) thus ?thesis by (simp add: Plus_def UN_equiv_class2 [OF equiv_exprel equiv_exprel]) @@ -246,26 +234,26 @@ by (simp add: FnCall_def) lemma FnCall_respects: - "(\Us. exprel `` {FNCALL F Us}) respects (listrel exprel)" + "(\Us. exprel``{FNCALL F Us}) respects (listrel exprel)" by (auto simp add: congruent_def exprel.FNCALL) lemma FnCall_sing: "FnCall F [Abs_Exp(exprel``{U})] = Abs_Exp (exprel``{FNCALL F [U]})" proof - - have "(\U. exprel `` {FNCALL F [U]}) respects exprel" + have "(\U. exprel``{FNCALL F [U]}) respects exprel" by (auto simp add: congruent_def FNCALL_Cons listrel.intros) thus ?thesis by (simp add: FnCall_def UN_equiv_class [OF equiv_exprel]) qed lemma listset_Rep_Exp_Abs_Exp: - "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel `` {Us}" + "listset (map Rep_Exp (Abs_ExpList Us)) = listrel exprel``{Us}" by (induct Us) (simp_all add: listrel_Cons Abs_ExpList_def) lemma FnCall: "FnCall F (Abs_ExpList Us) = Abs_Exp (exprel``{FNCALL F Us})" proof - - have "(\Us. exprel `` {FNCALL F Us}) respects (listrel exprel)" + have "(\Us. exprel``{FNCALL F Us}) respects (listrel exprel)" by (auto simp add: congruent_def exprel.FNCALL) thus ?thesis by (simp add: FnCall_def UN_equiv_class [OF equiv_list_exprel] @@ -275,15 +263,14 @@ text\Establishing this equation is the point of the whole exercise\ theorem Plus_assoc: "Plus X (Plus Y Z) = Plus (Plus X Y) Z" -by (cases X, cases Y, cases Z, simp add: Plus exprel.ASSOC) + by (cases X, cases Y, cases Z, simp add: Plus exprel.ASSOC) subsection\The Abstract Function to Return the Set of Variables\ definition - vars :: "exp \ nat set" where - "vars X = (\U \ Rep_Exp X. freevars U)" + vars :: "exp \ nat set" where "vars X \ (\U \ Rep_Exp X. freevars U)" lemma vars_respects: "freevars respects exprel" by (auto simp add: congruent_def exprel_imp_eq_freevars) @@ -301,62 +288,73 @@ UN_equiv_class [OF equiv_exprel vars_respects]) lemma vars_Plus [simp]: "vars (Plus X Y) = vars X \ vars Y" -apply (cases X, cases Y) -apply (simp add: vars_def Plus - UN_equiv_class [OF equiv_exprel vars_respects]) -done +proof - + have "\U V. \X = Abs_Exp (exprel``{U}); Y = Abs_Exp (exprel``{V})\ + \ vars (Plus X Y) = vars X \ vars Y" + by (simp add: vars_def Plus UN_equiv_class [OF equiv_exprel vars_respects]) + then show ?thesis + by (meson eq_Abs_Exp) +qed lemma vars_FnCall [simp]: "vars (FnCall F Xs) = vars_list Xs" -apply (cases Xs rule: eq_Abs_ExpList) -apply (simp add: FnCall) -apply (induct_tac Us) -apply (simp_all add: vars_def UN_equiv_class [OF equiv_exprel vars_respects]) -done +proof - + have "vars (Abs_Exp (exprel``{FNCALL F Us})) = vars_list (Abs_ExpList Us)" for Us + by (induct Us) (auto simp: vars_def UN_equiv_class [OF equiv_exprel vars_respects]) + then show ?thesis + by (metis ExpList_rep FnCall) +qed lemma vars_FnCall_Nil: "vars (FnCall F Nil) = {}" -by simp + by simp lemma vars_FnCall_Cons: "vars (FnCall F (X#Xs)) = vars X \ vars_list Xs" -by simp + by simp subsection\Injectivity Properties of Some Constructors\ lemma VAR_imp_eq: "VAR m \ VAR n \ m = n" -by (drule exprel_imp_eq_freevars, simp) + by (drule exprel_imp_eq_freevars, simp) text\Can also be proved using the function \<^term>\vars\\ lemma Var_Var_eq [iff]: "(Var m = Var n) = (m = n)" -by (auto simp add: Var_def exprel_refl dest: VAR_imp_eq) + by (auto simp add: Var_def exprel_refl dest: VAR_imp_eq) lemma VAR_neqv_PLUS: "VAR m \ PLUS X Y \ False" -by (drule exprel_imp_eq_freediscrim, simp) + using exprel_imp_eq_freediscrim by force theorem Var_neq_Plus [iff]: "Var N \ Plus X Y" -apply (cases X, cases Y) -apply (simp add: Var_def Plus) -apply (blast dest: VAR_neqv_PLUS) -done +proof - + have "\U V. \X = Abs_Exp (exprel``{U}); Y = Abs_Exp (exprel``{V})\ \ Var N \ Plus X Y" + using Plus VAR_neqv_PLUS Var_def by force + then show ?thesis + by (meson eq_Abs_Exp) +qed theorem Var_neq_FnCall [iff]: "Var N \ FnCall F Xs" -apply (cases Xs rule: eq_Abs_ExpList) -apply (auto simp add: FnCall Var_def) -apply (drule exprel_imp_eq_freediscrim, simp) -done +proof - + have "\Us. Var N \ FnCall F (Abs_ExpList Us)" + using FnCall Var_def exprel_imp_eq_freediscrim by fastforce + then show ?thesis + by (metis ExpList_rep) +qed subsection\Injectivity of \<^term>\FnCall\\ definition - "fun" :: "exp \ nat" where - "fun X = the_elem (\U \ Rep_Exp X. {freefun U})" + "fun" :: "exp \ nat" + where "fun X \ the_elem (\U \ Rep_Exp X. {freefun U})" -lemma fun_respects: "(%U. {freefun U}) respects exprel" -by (auto simp add: congruent_def exprel_imp_eq_freefun) +lemma fun_respects: "(\U. {freefun U}) respects exprel" + by (auto simp add: congruent_def exprel_imp_eq_freefun) lemma fun_FnCall [simp]: "fun (FnCall F Xs) = F" -apply (cases Xs rule: eq_Abs_ExpList) -apply (simp add: FnCall fun_def UN_equiv_class [OF equiv_exprel fun_respects]) -done +proof - + have "\Us. fun (FnCall F (Abs_ExpList Us)) = F" + using FnCall UN_equiv_class [OF equiv_exprel] fun_def fun_respects by fastforce + then show ?thesis + by (metis ExpList_rep) +qed definition args :: "exp \ exp list" where @@ -368,25 +366,19 @@ "(y, z) \ listrel exprel \ Abs_ExpList (y) = Abs_ExpList (z)" by (induct set: listrel) simp_all -lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel" -by (auto simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) +lemma args_respects: "(\U. {Abs_ExpList (freeargs U)}) respects exprel" + by (auto simp add: congruent_def Abs_ExpList_eq exprel_imp_eqv_freeargs) lemma args_FnCall [simp]: "args (FnCall F Xs) = Xs" -apply (cases Xs rule: eq_Abs_ExpList) -apply (simp add: FnCall args_def UN_equiv_class [OF equiv_exprel args_respects]) -done - +proof - + have "\Us. Xs = Abs_ExpList Us \ args (FnCall F Xs) = Xs" + by (simp add: FnCall args_def UN_equiv_class [OF equiv_exprel args_respects]) + then show ?thesis + by (metis ExpList_rep) +qed -lemma FnCall_FnCall_eq [iff]: - "(FnCall F Xs = FnCall F' Xs') = (F=F' & Xs=Xs')" -proof - assume "FnCall F Xs = FnCall F' Xs'" - hence "fun (FnCall F Xs) = fun (FnCall F' Xs')" - and "args (FnCall F Xs) = args (FnCall F' Xs')" by auto - thus "F=F' & Xs=Xs'" by simp -next - assume "F=F' & Xs=Xs'" thus "FnCall F Xs = FnCall F' Xs'" by simp -qed +lemma FnCall_FnCall_eq [iff]: "(FnCall F Xs = FnCall F' Xs') \ (F=F' \ Xs=Xs')" + by (metis args_FnCall fun_FnCall) subsection\The Abstract Discriminator\ @@ -403,21 +395,23 @@ text\Now prove the four equations for \<^term>\discrim\\ lemma discrim_Var [simp]: "discrim (Var N) = 0" -by (simp add: discrim_def Var_def - UN_equiv_class [OF equiv_exprel discrim_respects]) + by (simp add: discrim_def Var_def UN_equiv_class [OF equiv_exprel discrim_respects]) lemma discrim_Plus [simp]: "discrim (Plus X Y) = 1" -apply (cases X, cases Y) -apply (simp add: discrim_def Plus - UN_equiv_class [OF equiv_exprel discrim_respects]) -done +proof - + have "\U V. \X = Abs_Exp (exprel``{U}); Y = Abs_Exp (exprel``{V})\ \ discrim (Plus X Y) = 1" + by (simp add: discrim_def Plus UN_equiv_class [OF equiv_exprel discrim_respects]) + then show ?thesis + by (meson eq_Abs_Exp) +qed lemma discrim_FnCall [simp]: "discrim (FnCall F Xs) = 2" -apply (rule_tac z=Xs in eq_Abs_ExpList) -apply (simp add: discrim_def FnCall - UN_equiv_class [OF equiv_exprel discrim_respects]) -done - +proof - + have "discrim (FnCall F (Abs_ExpList Us)) = 2" for Us + by (simp add: discrim_def FnCall UN_equiv_class [OF equiv_exprel discrim_respects]) + then show ?thesis + by (metis ExpList_rep) +qed text\The structural induction rule for the abstract type\ theorem exp_inducts: @@ -428,15 +422,15 @@ and Cons: "\exp list. \P1 exp; P2 list\ \ P2 (exp # list)" 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)" + obtain U where exp: "exp = (Abs_Exp (exprel``{U}))" by (cases exp) + obtain Us where list: "list = Abs_ExpList Us" by (metis ExpList_rep) + have "P1 (Abs_Exp (exprel``{U}))" and "P2 (Abs_ExpList Us)" proof (induct U and Us rule: compat_freeExp.induct compat_freeExp_list.induct) case (VAR nat) with V show ?case by (simp add: Var_def) next case (PLUS X Y) - with P [of "Abs_Exp (exprel `` {X})" "Abs_Exp (exprel `` {Y})"] + with P [of "Abs_Exp (exprel``{X})" "Abs_Exp (exprel``{Y})"] show ?case by (simp add: Plus) next case (FNCALL nat list)