70 |
70 |
71 text{*A function to return the set of variables present in a message. It will |
71 text{*A function to return the set of variables present in a message. It will |
72 be lifted to the initial algrebra, to serve as an example of that process. |
72 be lifted to the initial algrebra, to serve as an example of that process. |
73 Note that the "free" refers to the free datatype rather than to the concept |
73 Note that the "free" refers to the free datatype rather than to the concept |
74 of a free variable.*} |
74 of a free variable.*} |
75 consts |
75 primrec freevars :: "freeExp \<Rightarrow> nat set" |
76 freevars :: "freeExp \<Rightarrow> nat set" |
76 and freevars_list :: "freeExp list \<Rightarrow> nat set" where |
77 freevars_list :: "freeExp list \<Rightarrow> nat set" |
77 "freevars (VAR N) = {N}" |
78 |
78 | "freevars (PLUS X Y) = freevars X \<union> freevars Y" |
79 primrec |
79 | "freevars (FNCALL F Xs) = freevars_list Xs" |
80 "freevars (VAR N) = {N}" |
80 |
81 "freevars (PLUS X Y) = freevars X \<union> freevars Y" |
81 | "freevars_list [] = {}" |
82 "freevars (FNCALL F Xs) = freevars_list Xs" |
82 | "freevars_list (X # Xs) = freevars X \<union> freevars_list Xs" |
83 |
|
84 "freevars_list [] = {}" |
|
85 "freevars_list (X # Xs) = freevars X \<union> freevars_list Xs" |
|
86 |
83 |
87 text{*This theorem lets us prove that the vars function respects the |
84 text{*This theorem lets us prove that the vars function respects the |
88 equivalence relation. It also helps us prove that Variable |
85 equivalence relation. It also helps us prove that Variable |
89 (the abstract constructor) is injective*} |
86 (the abstract constructor) is injective*} |
90 theorem exprel_imp_eq_freevars: "U \<sim> V \<Longrightarrow> freevars U = freevars V" |
87 theorem exprel_imp_eq_freevars: "U \<sim> V \<Longrightarrow> freevars U = freevars V" |
96 |
93 |
97 |
94 |
98 subsubsection{*Functions for Freeness*} |
95 subsubsection{*Functions for Freeness*} |
99 |
96 |
100 text{*A discriminator function to distinguish vars, sums and function calls*} |
97 text{*A discriminator function to distinguish vars, sums and function calls*} |
101 consts freediscrim :: "freeExp \<Rightarrow> int" |
98 primrec freediscrim :: "freeExp \<Rightarrow> int" where |
102 primrec |
99 "freediscrim (VAR N) = 0" |
103 "freediscrim (VAR N) = 0" |
100 | "freediscrim (PLUS X Y) = 1" |
104 "freediscrim (PLUS X Y) = 1" |
101 | "freediscrim (FNCALL F Xs) = 2" |
105 "freediscrim (FNCALL F Xs) = 2" |
|
106 |
102 |
107 theorem exprel_imp_eq_freediscrim: |
103 theorem exprel_imp_eq_freediscrim: |
108 "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V" |
104 "U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V" |
109 by (induct set: exprel) auto |
105 by (induct set: exprel) auto |
110 |
106 |
111 |
107 |
112 text{*This function, which returns the function name, is used to |
108 text{*This function, which returns the function name, is used to |
113 prove part of the injectivity property for FnCall.*} |
109 prove part of the injectivity property for FnCall.*} |
114 consts freefun :: "freeExp \<Rightarrow> nat" |
110 primrec freefun :: "freeExp \<Rightarrow> nat" where |
115 |
111 "freefun (VAR N) = 0" |
116 primrec |
112 | "freefun (PLUS X Y) = 0" |
117 "freefun (VAR N) = 0" |
113 | "freefun (FNCALL F Xs) = F" |
118 "freefun (PLUS X Y) = 0" |
|
119 "freefun (FNCALL F Xs) = F" |
|
120 |
114 |
121 theorem exprel_imp_eq_freefun: |
115 theorem exprel_imp_eq_freefun: |
122 "U \<sim> V \<Longrightarrow> freefun U = freefun V" |
116 "U \<sim> V \<Longrightarrow> freefun U = freefun V" |
123 by (induct set: exprel) (simp_all add: listrel.intros) |
117 by (induct set: exprel) (simp_all add: listrel.intros) |
124 |
118 |
125 |
119 |
126 text{*This function, which returns the list of function arguments, is used to |
120 text{*This function, which returns the list of function arguments, is used to |
127 prove part of the injectivity property for FnCall.*} |
121 prove part of the injectivity property for FnCall.*} |
128 consts freeargs :: "freeExp \<Rightarrow> freeExp list" |
122 primrec freeargs :: "freeExp \<Rightarrow> freeExp list" where |
129 primrec |
123 "freeargs (VAR N) = []" |
130 "freeargs (VAR N) = []" |
124 | "freeargs (PLUS X Y) = []" |
131 "freeargs (PLUS X Y) = []" |
125 | "freeargs (FNCALL F Xs) = Xs" |
132 "freeargs (FNCALL F Xs) = Xs" |
|
133 |
126 |
134 theorem exprel_imp_eqv_freeargs: |
127 theorem exprel_imp_eqv_freeargs: |
135 "U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel" |
128 "U \<sim> V \<Longrightarrow> (freeargs U, freeargs V) \<in> listrel exprel" |
136 apply (induct set: exprel) |
129 apply (induct set: exprel) |
137 apply (erule_tac [4] listrel.induct) |
130 apply (erule_tac [4] listrel.induct) |
283 |
276 |
284 lemma vars_respects: "freevars respects exprel" |
277 lemma vars_respects: "freevars respects exprel" |
285 by (simp add: congruent_def exprel_imp_eq_freevars) |
278 by (simp add: congruent_def exprel_imp_eq_freevars) |
286 |
279 |
287 text{*The extension of the function @{term vars} to lists*} |
280 text{*The extension of the function @{term vars} to lists*} |
288 consts vars_list :: "exp list \<Rightarrow> nat set" |
281 primrec vars_list :: "exp list \<Rightarrow> nat set" where |
289 primrec |
282 "vars_list [] = {}" |
290 "vars_list [] = {}" |
283 | "vars_list(E#Es) = vars E \<union> vars_list Es" |
291 "vars_list(E#Es) = vars E \<union> vars_list Es" |
|
292 |
284 |
293 |
285 |
294 text{*Now prove the three equations for @{term vars}*} |
286 text{*Now prove the three equations for @{term vars}*} |
295 |
287 |
296 lemma vars_Variable [simp]: "vars (Var N) = {N}" |
288 lemma vars_Variable [simp]: "vars (Var N) = {N}" |