# HG changeset patch # User nipkow # Date 1327829642 -3600 # Node ID 25f081f779158dfb0cfad5a237a25832af584f18 # Parent 73b03235799a43d6ce5ea4c646ca43b961e44bd5# Parent 66486acfa26a32f704896d100bf0bd826c8b4077 merged diff -r 73b03235799a -r 25f081f77915 src/HOL/IMP/Abs_Int0_const.thy --- a/src/HOL/IMP/Abs_Int0_const.thy Sat Jan 28 12:05:26 2012 +0100 +++ b/src/HOL/IMP/Abs_Int0_const.thy Sun Jan 29 10:34:02 2012 +0100 @@ -72,6 +72,46 @@ proof qed +subsubsection "Tests" + +value "show_acom (((step_const \)^^0) (\\<^sub>c test1_const))" +value "show_acom (((step_const \)^^1) (\\<^sub>c test1_const))" +value "show_acom (((step_const \)^^2) (\\<^sub>c test1_const))" +value "show_acom (((step_const \)^^3) (\\<^sub>c test1_const))" +value "show_acom_opt (AI_const test1_const)" + +value "show_acom_opt (AI_const test2_const)" +value "show_acom_opt (AI_const test3_const)" + +value "show_acom (((step_const \)^^0) (\\<^sub>c test4_const))" +value "show_acom (((step_const \)^^1) (\\<^sub>c test4_const))" +value "show_acom (((step_const \)^^2) (\\<^sub>c test4_const))" +value "show_acom (((step_const \)^^3) (\\<^sub>c test4_const))" +value "show_acom_opt (AI_const test4_const)" + +value "show_acom (((step_const \)^^0) (\\<^sub>c test5_const))" +value "show_acom (((step_const \)^^1) (\\<^sub>c test5_const))" +value "show_acom (((step_const \)^^2) (\\<^sub>c test5_const))" +value "show_acom (((step_const \)^^3) (\\<^sub>c test5_const))" +value "show_acom (((step_const \)^^4) (\\<^sub>c test5_const))" +value "show_acom (((step_const \)^^5) (\\<^sub>c test5_const))" +value "show_acom_opt (AI_const test5_const)" + +value "show_acom (((step_const \)^^0) (\\<^sub>c test6_const))" +value "show_acom (((step_const \)^^1) (\\<^sub>c test6_const))" +value "show_acom (((step_const \)^^2) (\\<^sub>c test6_const))" +value "show_acom (((step_const \)^^3) (\\<^sub>c test6_const))" +value "show_acom (((step_const \)^^4) (\\<^sub>c test6_const))" +value "show_acom (((step_const \)^^5) (\\<^sub>c test6_const))" +value "show_acom (((step_const \)^^6) (\\<^sub>c test6_const))" +value "show_acom (((step_const \)^^7) (\\<^sub>c test6_const))" +value "show_acom (((step_const \)^^8) (\\<^sub>c test6_const))" +value "show_acom (((step_const \)^^9) (\\<^sub>c test6_const))" +value "show_acom (((step_const \)^^10) (\\<^sub>c test6_const))" +value "show_acom (((step_const \)^^11) (\\<^sub>c test6_const))" +value "show_acom_opt (AI_const test6_const)" + + text{* Monotonicity: *} interpretation Abs_Int_mono @@ -96,32 +136,4 @@ lemma "EX c'. AI_const c = Some c'" by(rule AI_Some_measure[OF measure_const measure_const_eq]) - -subsubsection "Tests" - -value [code] "show_acom (((step_const \)^^0) (\\<^sub>c test1_const))" -value [code] "show_acom (((step_const \)^^1) (\\<^sub>c test1_const))" -value [code] "show_acom (((step_const \)^^2) (\\<^sub>c test1_const))" -value [code] "show_acom (((step_const \)^^3) (\\<^sub>c test1_const))" -value [code] "show_acom_opt (AI_const test1_const)" - -value [code] "show_acom_opt (AI_const test2_const)" -value [code] "show_acom_opt (AI_const test3_const)" - -value [code] "show_acom (((step_const \)^^0) (\\<^sub>c test4_const))" -value [code] "show_acom (((step_const \)^^1) (\\<^sub>c test4_const))" -value [code] "show_acom (((step_const \)^^2) (\\<^sub>c test4_const))" -value [code] "show_acom (((step_const \)^^3) (\\<^sub>c test4_const))" -value [code] "show_acom_opt (AI_const test4_const)" - -value [code] "show_acom (((step_const \)^^0) (\\<^sub>c test5_const))" -value [code] "show_acom (((step_const \)^^1) (\\<^sub>c test5_const))" -value [code] "show_acom (((step_const \)^^2) (\\<^sub>c test5_const))" -value [code] "show_acom (((step_const \)^^3) (\\<^sub>c test5_const))" -value [code] "show_acom (((step_const \)^^4) (\\<^sub>c test5_const))" -value [code] "show_acom (((step_const \)^^5) (\\<^sub>c test5_const))" -value [code] "show_acom_opt (AI_const test5_const)" - -value [code] "show_acom_opt (AI_const test6_const)" - end