equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/Comp/Index.thy |
1 (* Title: HOL/MicroJava/Comp/Index.thy |
2 ID: $Id$ |
|
3 Author: Martin Strecker |
2 Author: Martin Strecker |
4 *) |
3 *) |
5 |
4 |
6 (* Index of variable in list of parameter names and local variables *) |
5 (* Index of variable in list of parameter names and local variables *) |
7 |
6 |
103 constdefs |
102 constdefs |
104 disjoint_varnames :: "[vname list, (vname \<times> ty) list] \<Rightarrow> bool" |
103 disjoint_varnames :: "[vname list, (vname \<times> ty) list] \<Rightarrow> bool" |
105 (* This corresponds to the original def in wf_java_mdecl: |
104 (* This corresponds to the original def in wf_java_mdecl: |
106 "disjoint_varnames pns lvars \<equiv> |
105 "disjoint_varnames pns lvars \<equiv> |
107 nodups pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> |
106 nodups pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> |
108 (\<forall>pn\<in>set pns. map_of lvars pn = None)" |
107 (\<forall>pn\<in>set pns. map_of lvars pn = None)" |
109 *) |
108 *) |
110 |
109 |
111 "disjoint_varnames pns lvars \<equiv> |
110 "disjoint_varnames pns lvars \<equiv> |
112 distinct pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> |
111 distinct pns \<and> unique lvars \<and> This \<notin> set pns \<and> This \<notin> set (map fst lvars) \<and> |
113 (\<forall>pn\<in>set pns. pn \<notin> set (map fst lvars))" |
112 (\<forall>pn\<in>set pns. pn \<notin> set (map fst lvars))" |