equal
deleted
inserted
replaced
438 "(a, b)\<Colon>\<preceq>(G, L) \<longrightarrow> (absorb j a, b)\<Colon>\<preceq>(G, L)" |
438 "(a, b)\<Colon>\<preceq>(G, L) \<longrightarrow> (absorb j a, b)\<Colon>\<preceq>(G, L)" |
439 apply (rule impI) |
439 apply (rule impI) |
440 apply (case_tac a) |
440 apply (case_tac a) |
441 apply (case_tac "absorb j a") |
441 apply (case_tac "absorb j a") |
442 apply auto |
442 apply auto |
443 apply (rename_tac a) |
443 apply (rename_tac a') |
444 apply (case_tac "absorb j (Some a)",auto) |
444 apply (case_tac "absorb j (Some a')",auto) |
445 apply (erule conforms_NormI) |
445 apply (erule conforms_NormI) |
446 done |
446 done |
447 |
447 |
448 lemma conformsI: "\<lbrakk>\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r; |
448 lemma conformsI: "\<lbrakk>\<forall>r. \<forall>obj\<in>globs s r: G,s\<turnstile>obj\<Colon>\<preceq>\<surd>r; |
449 G,s\<turnstile>locals s[\<sim>\<Colon>\<preceq>]L; |
449 G,s\<turnstile>locals s[\<sim>\<Colon>\<preceq>]L; |