equal
deleted
inserted
replaced
61 constdefs |
61 constdefs |
62 wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" |
62 wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" |
63 "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and> |
63 "wf_mhead G P \<equiv> \<lambda> sig mh. length (parTs sig) = length (pars mh) \<and> |
64 \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> |
64 \<spacespace> ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> |
65 is_acc_type G P (resTy mh) \<and> |
65 is_acc_type G P (resTy mh) \<and> |
66 \<spacespace> nodups (pars mh)" |
66 \<spacespace> distinct (pars mh)" |
67 |
67 |
68 |
68 |
69 text {* |
69 text {* |
70 A method declaration is wellformed if: |
70 A method declaration is wellformed if: |
71 \begin{itemize} |
71 \begin{itemize} |
101 | This \<Rightarrow> if static m then None else Some (Class C)) |
101 | This \<Rightarrow> if static m then None else Some (Class C)) |
102 \<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>" |
102 \<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>" |
103 |
103 |
104 lemma wf_mheadI: |
104 lemma wf_mheadI: |
105 "\<lbrakk>length (parTs sig) = length (pars m); \<forall>T\<in>set (parTs sig). is_acc_type G P T; |
105 "\<lbrakk>length (parTs sig) = length (pars m); \<forall>T\<in>set (parTs sig). is_acc_type G P T; |
106 is_acc_type G P (resTy m); nodups (pars m)\<rbrakk> \<Longrightarrow> |
106 is_acc_type G P (resTy m); distinct (pars m)\<rbrakk> \<Longrightarrow> |
107 wf_mhead G P sig m" |
107 wf_mhead G P sig m" |
108 apply (unfold wf_mhead_def) |
108 apply (unfold wf_mhead_def) |
109 apply (simp (no_asm_simp)) |
109 apply (simp (no_asm_simp)) |
110 done |
110 done |
111 |
111 |