equal
deleted
inserted
replaced
1073 done |
1073 done |
1074 |
1074 |
1075 lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> = |
1075 lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> = |
1076 {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>) |
1076 {((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>) |
1077 , [Class Base])}" |
1077 , [Class Base])}" |
1078 apply (unfold max_spec_def) |
1078 by (simp (no_asm) add: max_spec_def appl_methds_Base_foo) |
1079 apply (simp (no_asm) add: appl_methds_Base_foo) |
|
1080 apply auto |
|
1081 done |
|
1082 |
1079 |
1083 section "well-typedness" |
1080 section "well-typedness" |
1084 |
1081 |
1085 lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>" |
1082 lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>" |
1086 apply (unfold test_def arr_viewed_from_def) |
1083 apply (unfold test_def arr_viewed_from_def) |