equal
deleted
inserted
replaced
728 |
728 |
729 declare split_paired_All [simp del] split_paired_Ex [simp del] |
729 declare split_paired_All [simp del] split_paired_Ex [simp del] |
730 declare split_if [split del] split_if_asm [split del] |
730 declare split_if [split del] split_if_asm [split del] |
731 option.split [split del] option.split_asm [split del] |
731 option.split [split del] option.split_asm [split del] |
732 ML_setup {* |
732 ML_setup {* |
733 simpset_ref() := simpset() delloop "split_all_tac"; |
733 change_simpset (fn ss => ss delloop "split_all_tac"); |
734 claset_ref () := claset () delSWrapper "split_all_tac" |
734 change_claset (fn cs => cs delSWrapper "split_all_tac"); |
735 *} |
735 *} |
736 lemma FVar_lemma: |
736 lemma FVar_lemma: |
737 "\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2); |
737 "\<lbrakk>((v, f), Norm s2') = fvar statDeclC (static field) fn a (x2, s2); |
738 G\<turnstile>statC\<preceq>\<^sub>C statDeclC; |
738 G\<turnstile>statC\<preceq>\<^sub>C statDeclC; |
739 table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some field; |
739 table_of (DeclConcepts.fields G statC) (fn, statDeclC) = Some field; |
758 done |
758 done |
759 declare split_paired_All [simp] split_paired_Ex [simp] |
759 declare split_paired_All [simp] split_paired_Ex [simp] |
760 declare split_if [split] split_if_asm [split] |
760 declare split_if [split] split_if_asm [split] |
761 option.split [split] option.split_asm [split] |
761 option.split [split] option.split_asm [split] |
762 ML_setup {* |
762 ML_setup {* |
763 claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac); |
763 change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac)); |
764 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) |
764 change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac)); |
765 *} |
765 *} |
766 |
766 |
767 |
767 |
768 lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i; |
768 lemma AVar_lemma1: "\<lbrakk>globs s (Inl a) = Some obj;tag obj=Arr ty i; |
769 the_Intg i' in_bounds i; wf_prog G; G\<turnstile>ty.[]\<preceq>Tb.[]; Norm s\<Colon>\<preceq>(G, L) |
769 the_Intg i' in_bounds i; wf_prog G; G\<turnstile>ty.[]\<preceq>Tb.[]; Norm s\<Colon>\<preceq>(G, L) |
876 |
876 |
877 declare split_paired_All [simp del] split_paired_Ex [simp del] |
877 declare split_paired_All [simp del] split_paired_Ex [simp del] |
878 declare split_if [split del] split_if_asm [split del] |
878 declare split_if [split del] split_if_asm [split del] |
879 option.split [split del] option.split_asm [split del] |
879 option.split [split del] option.split_asm [split del] |
880 ML_setup {* |
880 ML_setup {* |
881 simpset_ref() := simpset() delloop "split_all_tac"; |
881 change_simpset (fn ss => ss delloop "split_all_tac"); |
882 claset_ref () := claset () delSWrapper "split_all_tac" |
882 change_claset (fn cs => cs delSWrapper "split_all_tac"); |
883 *} |
883 *} |
884 lemma conforms_init_lvars: |
884 lemma conforms_init_lvars: |
885 "\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G; |
885 "\<lbrakk>wf_mhead G (pid declC) sig (mhead (mthd dm)); wf_prog G; |
886 list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig); |
886 list_all2 (conf G s) pvs pTsa; G\<turnstile>pTsa[\<preceq>](parTs sig); |
887 (x, s)\<Colon>\<preceq>(G, L); |
887 (x, s)\<Colon>\<preceq>(G, L); |
930 done |
930 done |
931 declare split_paired_All [simp] split_paired_Ex [simp] |
931 declare split_paired_All [simp] split_paired_Ex [simp] |
932 declare split_if [split] split_if_asm [split] |
932 declare split_if [split] split_if_asm [split] |
933 option.split [split] option.split_asm [split] |
933 option.split [split] option.split_asm [split] |
934 ML_setup {* |
934 ML_setup {* |
935 claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac); |
935 change_claset (fn cs => cs addSbefore ("split_all_tac", split_all_tac)); |
936 simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) |
936 change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac)); |
937 *} |
937 *} |
938 |
938 |
939 |
939 |
940 subsection "accessibility" |
940 subsection "accessibility" |
941 |
941 |