src/HOL/IMP/Abs_Int0_const.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45200 1f1897ac7877
child 45623 f682f3f7b726
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
nipkow@45111
     1
(* Author: Tobias Nipkow *)
nipkow@45111
     2
nipkow@45111
     3
theory Abs_Int0_const
nipkow@45111
     4
imports Abs_Int0
nipkow@45111
     5
begin
nipkow@45111
     6
nipkow@45111
     7
subsection "Constant Propagation"
nipkow@45111
     8
nipkow@45111
     9
datatype cval = Const val | Any
nipkow@45111
    10
nipkow@45111
    11
fun rep_cval where
nipkow@45111
    12
"rep_cval (Const n) = {n}" |
nipkow@45111
    13
"rep_cval (Any) = UNIV"
nipkow@45111
    14
nipkow@45111
    15
fun plus_cval where
nipkow@45111
    16
"plus_cval (Const m) (Const n) = Const(m+n)" |
nipkow@45111
    17
"plus_cval _ _ = Any"
nipkow@45111
    18
nipkow@45111
    19
lemma plus_cval_cases: "plus_cval a1 a2 =
nipkow@45111
    20
  (case (a1,a2) of (Const m, Const n) \<Rightarrow> Const(m+n) | _ \<Rightarrow> Any)"
nipkow@45111
    21
by(auto split: prod.split cval.split)
nipkow@45111
    22
nipkow@45111
    23
instantiation cval :: SL_top
nipkow@45111
    24
begin
nipkow@45111
    25
nipkow@45111
    26
fun le_cval where
nipkow@45111
    27
"_ \<sqsubseteq> Any = True" |
nipkow@45111
    28
"Const n \<sqsubseteq> Const m = (n=m)" |
nipkow@45111
    29
"Any \<sqsubseteq> Const _ = False"
nipkow@45111
    30
nipkow@45111
    31
fun join_cval where
nipkow@45111
    32
"Const m \<squnion> Const n = (if n=m then Const m else Any)" |
nipkow@45111
    33
"_ \<squnion> _ = Any"
nipkow@45111
    34
nipkow@45111
    35
definition "\<top> = Any"
nipkow@45111
    36
nipkow@45111
    37
instance
nipkow@45111
    38
proof
nipkow@45111
    39
  case goal1 thus ?case by (cases x) simp_all
nipkow@45111
    40
next
nipkow@45111
    41
  case goal2 thus ?case by(cases z, cases y, cases x, simp_all)
nipkow@45111
    42
next
nipkow@45111
    43
  case goal3 thus ?case by(cases x, cases y, simp_all)
nipkow@45111
    44
next
nipkow@45111
    45
  case goal4 thus ?case by(cases y, cases x, simp_all)
nipkow@45111
    46
next
nipkow@45111
    47
  case goal5 thus ?case by(cases z, cases y, cases x, simp_all)
nipkow@45111
    48
next
nipkow@45111
    49
  case goal6 thus ?case by(simp add: Top_cval_def)
nipkow@45111
    50
qed
nipkow@45111
    51
nipkow@45111
    52
end
nipkow@45111
    53
nipkow@45127
    54
nipkow@45127
    55
interpretation Val_abs rep_cval Const plus_cval
nipkow@45111
    56
proof
nipkow@45111
    57
  case goal1 thus ?case
nipkow@45111
    58
    by(cases a, cases b, simp, simp, cases b, simp, simp)
nipkow@45111
    59
next
nipkow@45111
    60
  case goal2 show ?case by(simp add: Top_cval_def)
nipkow@45111
    61
next
nipkow@45127
    62
  case goal3 show ?case by simp
nipkow@45111
    63
next
nipkow@45127
    64
  case goal4 thus ?case
nipkow@45111
    65
    by(auto simp: plus_cval_cases split: cval.split)
nipkow@45111
    66
qed
nipkow@45111
    67
nipkow@45127
    68
interpretation Abs_Int rep_cval Const plus_cval
nipkow@45111
    69
defines AI_const is AI
nipkow@45111
    70
and aval'_const is aval'
nipkow@45111
    71
and step_const is step
nipkow@45127
    72
proof qed
nipkow@45111
    73
nipkow@45111
    74
text{* Straight line code: *}
nipkow@45111
    75
definition "test1_const =
nipkow@45111
    76
 ''y'' ::= N 7;
nipkow@45111
    77
 ''z'' ::= Plus (V ''y'') (N 2);
nipkow@45111
    78
 ''y'' ::= Plus (V ''x'') (N 0)"
nipkow@45111
    79
nipkow@45111
    80
text{* Conditional: *}
nipkow@45111
    81
definition "test2_const =
nipkow@45111
    82
 IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 5"
nipkow@45111
    83
nipkow@45111
    84
text{* Conditional, test is ignored: *}
nipkow@45111
    85
definition "test3_const =
nipkow@45111
    86
 ''x'' ::= N 42;
nipkow@45111
    87
 IF Less (N 41) (V ''x'') THEN ''x'' ::= N 5 ELSE ''x'' ::= N 6"
nipkow@45111
    88
nipkow@45111
    89
text{* While: *}
nipkow@45111
    90
definition "test4_const =
nipkow@45200
    91
 ''x'' ::= N 0; WHILE Bc True DO ''x'' ::= N 0"
nipkow@45111
    92
nipkow@45111
    93
text{* While, test is ignored: *}
nipkow@45111
    94
definition "test5_const =
nipkow@45111
    95
 ''x'' ::= N 0; WHILE Less (V ''x'') (N 1) DO ''x'' ::= N 1"
nipkow@45111
    96
nipkow@45111
    97
text{* Iteration is needed: *}
nipkow@45111
    98
definition "test6_const =
nipkow@45111
    99
  ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 2;
nipkow@45111
   100
  WHILE Less (V ''x'') (N 1) DO (''x'' ::= V ''y''; ''y'' ::= V ''z'')"
nipkow@45111
   101
nipkow@45111
   102
text{* More iteration would be needed: *}
nipkow@45111
   103
definition "test7_const =
nipkow@45111
   104
  ''x'' ::= N 0; ''y'' ::= N 0; ''z'' ::= N 0; ''u'' ::= N 3;
nipkow@45111
   105
  WHILE Less (V ''x'') (N 1)
nipkow@45111
   106
  DO (''x'' ::= V ''y''; ''y'' ::= V ''z''; ''z'' ::= V ''u'')"
nipkow@45111
   107
nipkow@45111
   108
value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test1_const))"
nipkow@45111
   109
value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test1_const))"
nipkow@45111
   110
value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test1_const))"
nipkow@45111
   111
value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test1_const))"
nipkow@45127
   112
value [code] "show_acom_opt (AI_const test1_const)"
nipkow@45111
   113
nipkow@45127
   114
value [code] "show_acom_opt (AI_const test2_const)"
nipkow@45127
   115
value [code] "show_acom_opt (AI_const test3_const)"
nipkow@45111
   116
nipkow@45111
   117
value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test4_const))"
nipkow@45111
   118
value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test4_const))"
nipkow@45111
   119
value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test4_const))"
nipkow@45111
   120
value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test4_const))"
nipkow@45127
   121
value [code] "show_acom_opt (AI_const test4_const)"
nipkow@45111
   122
nipkow@45111
   123
value [code] "show_acom (((step_const \<top>)^^0) (\<bottom>\<^sub>c test5_const))"
nipkow@45111
   124
value [code] "show_acom (((step_const \<top>)^^1) (\<bottom>\<^sub>c test5_const))"
nipkow@45111
   125
value [code] "show_acom (((step_const \<top>)^^2) (\<bottom>\<^sub>c test5_const))"
nipkow@45111
   126
value [code] "show_acom (((step_const \<top>)^^3) (\<bottom>\<^sub>c test5_const))"
nipkow@45111
   127
value [code] "show_acom (((step_const \<top>)^^4) (\<bottom>\<^sub>c test5_const))"
nipkow@45111
   128
value [code] "show_acom (((step_const \<top>)^^5) (\<bottom>\<^sub>c test5_const))"
nipkow@45127
   129
value [code] "show_acom_opt (AI_const test5_const)"
nipkow@45127
   130
nipkow@45127
   131
value [code] "show_acom_opt (AI_const test6_const)"
nipkow@45127
   132
value [code] "show_acom_opt (AI_const test7_const)"
nipkow@45111
   133
nipkow@45127
   134
text{* Monotonicity: *}
nipkow@45127
   135
nipkow@45127
   136
interpretation Abs_Int_mono rep_cval Const plus_cval
nipkow@45127
   137
proof
nipkow@45127
   138
  case goal1 thus ?case
nipkow@45127
   139
    by(auto simp: plus_cval_cases split: cval.split)
nipkow@45127
   140
qed
nipkow@45111
   141
nipkow@45111
   142
end