Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/IMP/Abs_Int1_const.thy
author nipkow
Mon, 17 Sep 2012 02:25:38 +0200
changeset 50414 a9d9f3483b71
parent 50411 73fb17ed2e08
child 50448 1095f240146a
permissions -rw-r--r--
tuned 
     1 (* Author: Tobias Nipkow *)

     2 

     3 theory Abs_Int1_const

     4 imports Abs_Int1

     5 begin

     6 

     7 subsection "Constant Propagation"

     8 

     9 datatype const = Const val | Any

    10 

    11 fun \<gamma>_const where

    12 "\<gamma>_const (Const n) = {n}" |

    13 "\<gamma>_const (Any) = UNIV"

    14 

    15 fun plus_const where

    16 "plus_const (Const m) (Const n) = Const(m+n)" |

    17 "plus_const _ _ = Any"

    18 

    19 lemma plus_const_cases: "plus_const a1 a2 =

    20   (case (a1,a2) of (Const m, Const n) \<Rightarrow> Const(m+n) | _ \<Rightarrow> Any)"

    21 by(auto split: prod.split const.split)

    22 

    23 instantiation const :: semilattice

    24 begin

    25 

    26 fun le_const where

    27 "_ \<sqsubseteq> Any = True" |

    28 "Const n \<sqsubseteq> Const m = (n=m)" |

    29 "Any \<sqsubseteq> Const _ = False"

    30 

    31 fun join_const where

    32 "Const m \<squnion> Const n = (if n=m then Const m else Any)" |

    33 "_ \<squnion> _ = Any"

    34 

    35 definition "\<top> = Any"

    36 

    37 instance

    38 proof

    39   case goal1 thus ?case by (cases x) simp_all

    40 next

    41   case goal2 thus ?case by(cases z, cases y, cases x, simp_all)

    42 next

    43   case goal3 thus ?case by(cases x, cases y, simp_all)

    44 next

    45   case goal4 thus ?case by(cases y, cases x, simp_all)

    46 next

    47   case goal5 thus ?case by(cases z, cases y, cases x, simp_all)

    48 next

    49   case goal6 thus ?case by(simp add: Top_const_def)

    50 qed

    51 

    52 end

    53 

    54 

    55 interpretation Val_abs

    56 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const

    57 proof

    58   case goal1 thus ?case

    59     by(cases a, cases b, simp, simp, cases b, simp, simp)

    60 next

    61   case goal2 show ?case by(simp add: Top_const_def)

    62 next

    63   case goal3 show ?case by simp

    64 next

    65   case goal4 thus ?case

    66     by(auto simp: plus_const_cases split: const.split)

    67 qed

    68 

    69 interpretation Abs_Int

    70 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const

    71 defines AI_const is AI and step_const is step' and aval'_const is aval'

    72 ..

    73 

    74 

    75 subsubsection "Tests"

    76 

    77 definition "steps c i = (step_const(top c) ^^ i) (bot c)"

    78 

    79 value "show_acom (steps test1_const 0)"

    80 value "show_acom (steps test1_const 1)"

    81 value "show_acom (steps test1_const 2)"

    82 value "show_acom (steps test1_const 3)"

    83 value "show_acom_opt (AI_const test1_const)"

    84 

    85 value "show_acom_opt (AI_const test2_const)"

    86 value "show_acom_opt (AI_const test3_const)"

    87 

    88 value "show_acom (steps test4_const 0)"

    89 value "show_acom (steps test4_const 1)"

    90 value "show_acom (steps test4_const 2)"

    91 value "show_acom (steps test4_const 3)"

    92 value "show_acom (steps test4_const 4)"

    93 value "show_acom_opt (AI_const test4_const)"

    94 

    95 value "show_acom (steps test5_const 0)"

    96 value "show_acom (steps test5_const 1)"

    97 value "show_acom (steps test5_const 2)"

    98 value "show_acom (steps test5_const 3)"

    99 value "show_acom (steps test5_const 4)"

   100 value "show_acom (steps test5_const 5)"

   101 value "show_acom (steps test5_const 6)"

   102 value "show_acom_opt (AI_const test5_const)"

   103 

   104 value "show_acom (steps test6_const 0)"

   105 value "show_acom (steps test6_const 1)"

   106 value "show_acom (steps test6_const 2)"

   107 value "show_acom (steps test6_const 3)"

   108 value "show_acom (steps test6_const 4)"

   109 value "show_acom (steps test6_const 5)"

   110 value "show_acom (steps test6_const 6)"

   111 value "show_acom (steps test6_const 7)"

   112 value "show_acom (steps test6_const 8)"

   113 value "show_acom (steps test6_const 9)"

   114 value "show_acom (steps test6_const 10)"

   115 value "show_acom (steps test6_const 11)"

   116 value "show_acom (steps test6_const 12)"

   117 value "show_acom (steps test6_const 13)"

   118 value "show_acom_opt (AI_const test6_const)"

   119 

   120 

   121 text{* Monotonicity: *}

   122 

   123 interpretation Abs_Int_mono

   124 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const

   125 proof

   126   case goal1 thus ?case

   127     by(auto simp: plus_const_cases split: const.split)

   128 qed

   129 

   130 text{* Termination: *}

   131 

   132 definition "m_const x = (case x of Const _ \<Rightarrow> 1 | Any \<Rightarrow> 0)"

   133 

   134 interpretation Abs_Int_measure

   135 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const

   136 and m = m_const and h = "2"

   137 proof

   138   case goal1 thus ?case by(auto simp: m_const_def split: const.splits)

   139 next

   140   case goal2 thus ?case by(auto simp: m_const_def split: const.splits)

   141 next

   142   case goal3 thus ?case by(auto simp: m_const_def split: const.splits)

   143 qed

   144 

   145 thm AI_Some_measure

   146 

   147 end
wneuper/isa