# HG changeset patch # User paulson # Date 1094136741 -7200 # Node ID 73069e033a0b581270cf152061519d18c6918afa # Parent e0cd537c43258edb1f6f5675d6bbab6385b657ad new example of a quotiented nested data type diff -r e0cd537c4325 -r 73069e033a0b src/HOL/Induct/QuoDataType.thy --- a/src/HOL/Induct/QuoDataType.thy Thu Sep 02 14:50:00 2004 +0200 +++ b/src/HOL/Induct/QuoDataType.thy Thu Sep 02 16:52:21 2004 +0200 @@ -373,7 +373,7 @@ by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim) text{*...and many similar results*} -theorem Crypt_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) \ Nonce N" +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) theorem Crypt_Crypt_eq [iff]: "(Crypt K X = Crypt K X') = (X=X')" diff -r e0cd537c4325 -r 73069e033a0b src/HOL/Induct/QuoNestedDataType.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Induct/QuoNestedDataType.thy Thu Sep 02 16:52:21 2004 +0200 @@ -0,0 +1,462 @@ +(* Title: HOL/Induct/QuoNestedDataType + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 2004 University of Cambridge + +*) + +header{*Quotienting a Free Algebra Involving Nested Recursion*} + +theory QuoNestedDataType = Main: + +subsection{*Defining the Free Algebra*} + +text{*Messages with encryption and decryption as free constructors.*} +datatype + freeExp = VAR nat + | PLUS freeExp freeExp + | FNCALL nat "freeExp list" + +text{*The equivalence relation, which makes PLUS associative.*} +consts exprel :: "(freeExp * freeExp) set" + +syntax + "_exprel" :: "[freeExp, freeExp] => bool" (infixl "~~" 50) +syntax (xsymbols) + "_exprel" :: "[freeExp, freeExp] => bool" (infixl "\" 50) +syntax (HTML output) + "_exprel" :: "[freeExp, freeExp] => bool" (infixl "\" 50) +translations + "X \ Y" == "(X,Y) \ exprel" + +text{*The first rule is the desired equation. The next three rules +make the equations applicable to subterms. The last two rules are symmetry +and transitivity.*} +inductive "exprel" + intros + 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'" + FNCALL: "(Xs,Xs') \ listrel exprel \ FNCALL F Xs \ FNCALL F Xs'" + SYM: "X \ Y \ Y \ X" + TRANS: "\X \ Y; Y \ Z\ \ X \ Z" + monos listrel_mono + + +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] + +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) +qed + +theorem equiv_list_exprel: "equiv UNIV (listrel exprel)" +by (insert equiv_listrel [OF equiv_exprel], 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) + + + +subsection{*Some Functions on the Free Algebra*} + +subsubsection{*The Set of Variables*} + +text{*A function to return the set of variables present in a message. It will +be lifted to the initial algrebra, 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.*} +consts + freevars :: "freeExp \ nat set" + freevars_list :: "freeExp list \ nat set" + +primrec + "freevars (VAR N) = {N}" + "freevars (PLUS X Y) = freevars X \ freevars Y" + "freevars (FNCALL F Xs) = freevars_list Xs" + + "freevars_list [] = {}" + "freevars_list (X # Xs) = freevars X \ freevars_list Xs" + +text{*This theorem lets us prove that the vars function respects the +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 (erule_tac [4] listrel.induct) +apply (simp_all add: Un_assoc) +done + + + +subsubsection{*Functions for Freeness*} + +text{*A discriminator function to distinguish vars, sums and function calls*} +consts freediscrim :: "freeExp \ int" +primrec + "freediscrim (VAR N) = 0" + "freediscrim (PLUS X Y) = 1" + "freediscrim (FNCALL F Xs) = 2" + +theorem exprel_imp_eq_freediscrim: + "U \ V \ freediscrim U = freediscrim V" +by (erule exprel.induct, auto) + + +text{*This function, which returns the function name, is used to +prove part of the injectivity property for FnCall.*} +consts freefun :: "freeExp \ nat" + +primrec + "freefun (VAR N) = 0" + "freefun (PLUS X Y) = 0" + "freefun (FNCALL F Xs) = F" + +theorem exprel_imp_eq_freefun: + "U \ V \ freefun U = freefun V" +by (erule exprel.induct, simp_all add: listrel.intros) + + +text{*This function, which returns the list of function arguments, is used to +prove part of the injectivity property for FnCall.*} +consts freeargs :: "freeExp \ freeExp list" +primrec + "freeargs (VAR N) = []" + "freeargs (PLUS X Y) = []" + "freeargs (FNCALL F Xs) = Xs" + +theorem exprel_imp_eqv_freeargs: + "U \ V \ (freeargs U, freeargs V) \ listrel exprel" +apply (erule exprel.induct) +apply (erule_tac [4] listrel.induct) +apply (simp_all add: listrel.intros) +apply (blast intro: symD [OF equiv.sym [OF equiv_list_exprel]]) +apply (blast intro: transD [OF equiv.trans [OF equiv_list_exprel]]) +done + + + +subsection{*The Initial Algebra: A Quotiented Message Type*} + + +typedef (Exp) exp = "UNIV//exprel" + by (auto simp add: quotient_def) + +text{*The abstract message constructors*} + +constdefs + Var :: "nat \ exp" + "Var N == Abs_Exp(exprel``{VAR N})" + + Plus :: "[exp,exp] \ exp" + "Plus X Y == + Abs_Exp (\U \ Rep_Exp X. \V \ Rep_Exp Y. exprel``{PLUS U V})" + + FnCall :: "[nat, exp list] \ exp" + "FnCall F Xs == + 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)"} *} +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 inj_on_Abs_Exp: "inj_on Abs_Exp Exp" +apply (rule inj_on_inverseI) +apply (erule Abs_Exp_inverse) +done + +text{*Reduces equality on abstractions to equality on representatives*} +declare inj_on_Abs_Exp [THEN inj_on_iff, simp] + +declare Abs_Exp_inverse [simp] + + +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 + + +subsection{*Every list of abstract expressions can be expressed in terms of a + list of concrete expressions*} + +constdefs Abs_ExpList :: "freeExp list => exp list" + "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_Cons [simp]: + "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 (rule_tac [2] z=a in eq_Abs_Exp) +apply (auto simp add: Abs_ExpList_def 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) + + +subsubsection{*Characteristic Equations for the Abstract Constructors*} + +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" + by (simp add: congruent2_def exprel.PLUS) + thus ?thesis + by (simp add: Plus_def UN_equiv_class2 [OF equiv_exprel equiv_exprel]) +qed + +text{*It is not clear what to do with FnCall: it's argument is an abstraction +of an @{typ "exp list"}. Is it just Nil or Cons? What seems to work best is to +regard an @{typ "exp list"} as a @{term "listrel exprel"} equivalence class*} + +text{*This theorem is easily proved but never used. There's no obvious way +even to state the analogous result, @{text FnCall_Cons}.*} +lemma FnCall_Nil: "FnCall F [] = Abs_Exp (exprel``{FNCALL F []})" + by (simp add: FnCall_def) + +lemma FnCall_respects: + "(\Us. exprel `` {FNCALL F Us}) respects (listrel exprel)" + by (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" + by (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}"; +by (induct_tac 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)" + by (simp add: congruent_def exprel.FNCALL) + thus ?thesis + by (simp add: FnCall_def UN_equiv_class [OF equiv_list_exprel] + listset_Rep_Exp_Abs_Exp) +qed + + +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) + + + +subsection{*The Abstract Function to Return the Set of Variables*} + +constdefs + vars :: "exp \ nat set" + "vars X == \U \ Rep_Exp X. freevars U" + +lemma vars_respects: "freevars respects exprel" +by (simp add: congruent_def exprel_imp_eq_freevars) + +text{*The extension of the function @{term vars} to lists*} +consts vars_list :: "exp list \ nat set" +primrec + "vars_list [] = {}" + "vars_list(E#Es) = vars E \ vars_list Es" + + +text{*Now prove the three equations for @{term vars}*} + +lemma vars_Variable [simp]: "vars (Var N) = {N}" +by (simp add: vars_def Var_def + 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 + +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 + +lemma vars_FnCall_Nil: "vars (FnCall F Nil) = {}" +by simp + +lemma vars_FnCall_Cons: "vars (FnCall F (X#Xs)) = vars X \ vars_list Xs" +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) + +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) + +lemma VAR_neqv_PLUS: "VAR m \ PLUS X Y \ False" +by (drule exprel_imp_eq_freediscrim, simp) + +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 + +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 + +subsection{*Injectivity of @{term FnCall}*} + +constdefs + fun :: "exp \ nat" + "fun X == contents (\U \ Rep_Exp X. {freefun U})" + +lemma fun_respects: "(%U. {freefun U}) respects exprel" +by (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 + +constdefs + args :: "exp \ exp list" + "args X == contents (\U \ Rep_Exp X. {Abs_ExpList (freeargs U)})" + +text{*This result can probably be generalized to arbitrary equivalence +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) + +lemma args_respects: "(%U. {Abs_ExpList (freeargs U)}) respects exprel" +by (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 + + +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 + + +subsection{*The Abstract Discriminator*} +text{*However, as @{text FnCall_Var_neq_Var} illustrates, we don't need this +function in order to prove discrimination theorems.*} + +constdefs + discrim :: "exp \ int" + "discrim X == contents (\U \ Rep_Exp X. {freediscrim U})" + +lemma discrim_respects: "(\U. {freediscrim U}) respects exprel" +by (simp add: congruent_def exprel_imp_eq_freediscrim) + +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]) + +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 + +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 + + +text{*The structural induction rule for the abstract type*} +theorem exp_induct: + 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)" + proof (induct U and Us) + 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})"] + show ?case by (simp add: Plus) + next + case (FNCALL nat list) + with F [of "Abs_ExpList list"] + show ?case by (simp add: FnCall) + next + case Nil_freeExp + with Nil show ?case by simp + next + case Cons_freeExp + with Cons + show ?case by simp + qed +qed + +end + diff -r e0cd537c4325 -r 73069e033a0b src/HOL/Induct/ROOT.ML --- a/src/HOL/Induct/ROOT.ML Thu Sep 02 14:50:00 2004 +0200 +++ b/src/HOL/Induct/ROOT.ML Thu Sep 02 16:52:21 2004 +0200 @@ -1,6 +1,7 @@ time_use_thy "Mutil"; time_use_thy "QuoDataType"; +time_use_thy "QuoNestedDataType"; time_use_thy "Term"; time_use_thy "ABexp"; time_use_thy "Tree"; diff -r e0cd537c4325 -r 73069e033a0b src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Sep 02 14:50:00 2004 +0200 +++ b/src/HOL/IsaMakefile Thu Sep 02 16:52:21 2004 +0200 @@ -209,7 +209,8 @@ $(LOG)/HOL-Induct.gz: $(OUT)/HOL \ Induct/Com.thy Induct/Comb.thy Induct/LFilter.thy \ Induct/LList.thy Induct/Mutil.thy Induct/Ordinals.thy \ - Induct/PropLog.thy Induct/QuoDataType.thy Induct/ROOT.ML \ + Induct/PropLog.thy Induct/QuoNestedDataType.thy Induct/QuoDataType.thy\ + Induct/ROOT.ML \ Induct/Sexp.thy Induct/Sigma_Algebra.thy \ Induct/SList.thy Induct/ABexp.thy Induct/Term.thy \ Induct/Tree.thy Induct/document/root.tex