src/HOL/IMP/ACom.thy
author paulson <lp15@cam.ac.uk>
Mon May 23 15:33:24 2016 +0100 (2016-05-23)
changeset 63114 27afe7af7379
parent 58310 91ea607a34d8
child 67406 23307fd33906
permissions -rw-r--r--
Lots of new material for multivariate analysis
nipkow@45623
     1
(* Author: Tobias Nipkow *)
nipkow@45623
     2
nipkow@45623
     3
theory ACom
nipkow@45623
     4
imports Com
nipkow@45623
     5
begin
nipkow@45623
     6
nipkow@46225
     7
subsection "Annotated Commands"
nipkow@45623
     8
blanchet@58310
     9
datatype 'a acom =
nipkow@47818
    10
  SKIP 'a                           ("SKIP {_}" 61) |
nipkow@47818
    11
  Assign vname aexp 'a              ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
nipkow@52046
    12
  Seq "('a acom)" "('a acom)"       ("_;;//_"  [60, 61] 60) |
nipkow@49095
    13
  If bexp 'a "('a acom)" 'a "('a acom)" 'a
nipkow@49095
    14
    ("(IF _/ THEN ({_}/ _)/ ELSE ({_}/ _)//{_})"  [0, 0, 0, 61, 0, 0] 61) |
nipkow@49095
    15
  While 'a bexp 'a "('a acom)" 'a
nipkow@49138
    16
    ("({_}//WHILE _//DO ({_}//_)//{_})"  [0, 0, 0, 61, 0] 61)
nipkow@45623
    17
nipkow@54941
    18
notation com.SKIP ("SKIP")
nipkow@54941
    19
nipkow@49603
    20
text_raw{*\snip{stripdef}{1}{1}{% *}
nipkow@45623
    21
fun strip :: "'a acom \<Rightarrow> com" where
nipkow@54941
    22
"strip (SKIP {P}) = SKIP" |
nipkow@49603
    23
"strip (x ::= e {P}) = x ::= e" |
wenzelm@53015
    24
"strip (C\<^sub>1;;C\<^sub>2) = strip C\<^sub>1;; strip C\<^sub>2" |
wenzelm@53015
    25
"strip (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {P}) =
wenzelm@53015
    26
  IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2" |
nipkow@49603
    27
"strip ({I} WHILE b DO {P} C {Q}) = WHILE b DO strip C"
nipkow@49603
    28
text_raw{*}%endsnip*}
nipkow@45623
    29
nipkow@52019
    30
text_raw{*\snip{asizedef}{1}{1}{% *}
nipkow@52019
    31
fun asize :: "com \<Rightarrow> nat" where
nipkow@54941
    32
"asize SKIP = 1" |
nipkow@52019
    33
"asize (x ::= e) = 1" |
wenzelm@53015
    34
"asize (C\<^sub>1;;C\<^sub>2) = asize C\<^sub>1 + asize C\<^sub>2" |
wenzelm@53015
    35
"asize (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = asize C\<^sub>1 + asize C\<^sub>2 + 3" |
nipkow@52019
    36
"asize (WHILE b DO C) = asize C + 3"
nipkow@52019
    37
text_raw{*}%endsnip*}
nipkow@52019
    38
nipkow@52019
    39
text_raw{*\snip{annotatedef}{1}{1}{% *}
nipkow@52019
    40
definition shift :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where
nipkow@52019
    41
"shift f n = (\<lambda>p. f(p+n))"
nipkow@52019
    42
nipkow@52019
    43
fun annotate :: "(nat \<Rightarrow> 'a) \<Rightarrow> com \<Rightarrow> 'a acom" where
nipkow@54941
    44
"annotate f SKIP = SKIP {f 0}" |
nipkow@52019
    45
"annotate f (x ::= e) = x ::= e {f 0}" |
wenzelm@53015
    46
"annotate f (c\<^sub>1;;c\<^sub>2) = annotate f c\<^sub>1;; annotate (shift f (asize c\<^sub>1)) c\<^sub>2" |
wenzelm@53015
    47
"annotate f (IF b THEN c\<^sub>1 ELSE c\<^sub>2) =
wenzelm@53015
    48
  IF b THEN {f 0} annotate (shift f 1) c\<^sub>1
wenzelm@53015
    49
  ELSE {f(asize c\<^sub>1 + 1)} annotate (shift f (asize c\<^sub>1 + 2)) c\<^sub>2
wenzelm@53015
    50
  {f(asize c\<^sub>1 + asize c\<^sub>2 + 2)}" |
nipkow@52019
    51
"annotate f (WHILE b DO c) =
nipkow@52019
    52
  {f 0} WHILE b DO {f 1} annotate (shift f 2) c {f(asize c + 2)}"
nipkow@49603
    53
text_raw{*}%endsnip*}
nipkow@45623
    54
nipkow@49603
    55
text_raw{*\snip{annosdef}{1}{1}{% *}
nipkow@47613
    56
fun annos :: "'a acom \<Rightarrow> 'a list" where
nipkow@49603
    57
"annos (SKIP {P}) = [P]" |
nipkow@49603
    58
"annos (x ::= e {P}) = [P]" |
wenzelm@53015
    59
"annos (C\<^sub>1;;C\<^sub>2) = annos C\<^sub>1 @ annos C\<^sub>2" |
wenzelm@53015
    60
"annos (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {Q}) =
wenzelm@53015
    61
  P\<^sub>1 # annos C\<^sub>1 @  P\<^sub>2 # annos C\<^sub>2 @ [Q]" |
nipkow@52019
    62
"annos ({I} WHILE b DO {P} C {Q}) = I # P # annos C @ [Q]"
nipkow@49603
    63
text_raw{*}%endsnip*}
nipkow@47613
    64
nipkow@52019
    65
definition anno :: "'a acom \<Rightarrow> nat \<Rightarrow> 'a" where
nipkow@52019
    66
"anno C p = annos C ! p"
nipkow@52019
    67
nipkow@52019
    68
definition post :: "'a acom \<Rightarrow>'a" where
nipkow@52019
    69
"post C = last(annos C)"
nipkow@52019
    70
nipkow@49603
    71
text_raw{*\snip{mapacomdef}{1}{2}{% *}
nipkow@45623
    72
fun map_acom :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a acom \<Rightarrow> 'b acom" where
nipkow@45746
    73
"map_acom f (SKIP {P}) = SKIP {f P}" |
nipkow@49603
    74
"map_acom f (x ::= e {P}) = x ::= e {f P}" |
wenzelm@53015
    75
"map_acom f (C\<^sub>1;;C\<^sub>2) = map_acom f C\<^sub>1;; map_acom f C\<^sub>2" |
wenzelm@53015
    76
"map_acom f (IF b THEN {P\<^sub>1} C\<^sub>1 ELSE {P\<^sub>2} C\<^sub>2 {Q}) =
wenzelm@53015
    77
  IF b THEN {f P\<^sub>1} map_acom f C\<^sub>1 ELSE {f P\<^sub>2} map_acom f C\<^sub>2
nipkow@49603
    78
  {f Q}" |
nipkow@49603
    79
"map_acom f ({I} WHILE b DO {P} C {Q}) =
nipkow@49603
    80
  {f I} WHILE b DO {f P} map_acom f C {f Q}"
nipkow@49603
    81
text_raw{*}%endsnip*}
nipkow@45623
    82
nipkow@45623
    83
nipkow@52019
    84
lemma annos_ne: "annos C \<noteq> []"
nipkow@52019
    85
by(induction C) auto
nipkow@52019
    86
nipkow@52019
    87
lemma strip_annotate[simp]: "strip(annotate f c) = c"
nipkow@52019
    88
by(induction c arbitrary: f) auto
nipkow@52019
    89
nipkow@52019
    90
lemma length_annos_annotate[simp]: "length (annos (annotate f c)) = asize c"
nipkow@52019
    91
by(induction c arbitrary: f) auto
nipkow@52019
    92
nipkow@52019
    93
lemma size_annos: "size(annos C) = asize(strip C)"
nipkow@52019
    94
by(induction C)(auto)
nipkow@52019
    95
nipkow@52019
    96
lemma size_annos_same: "strip C1 = strip C2 \<Longrightarrow> size(annos C1) = size(annos C2)"
nipkow@52019
    97
apply(induct C2 arbitrary: C1)
nipkow@52019
    98
apply(case_tac C1, simp_all)+
nipkow@52019
    99
done
nipkow@52019
   100
nipkow@52019
   101
lemmas size_annos_same2 = eqTrueI[OF size_annos_same]
nipkow@52019
   102
nipkow@52019
   103
lemma anno_annotate[simp]: "p < asize c \<Longrightarrow> anno (annotate f c) p = f p"
nipkow@52019
   104
apply(induction c arbitrary: f p)
nipkow@52019
   105
apply (auto simp: anno_def nth_append nth_Cons numeral_eq_Suc shift_def
nipkow@52019
   106
            split: nat.split)
haftmann@57512
   107
  apply (metis add_Suc_right add_diff_inverse add.commute)
nipkow@52019
   108
 apply(rule_tac f=f in arg_cong)
nipkow@52019
   109
 apply arith
nipkow@52019
   110
apply (metis less_Suc_eq)
nipkow@52019
   111
done
nipkow@52019
   112
nipkow@52019
   113
lemma eq_acom_iff_strip_annos:
nipkow@52019
   114
  "C1 = C2 \<longleftrightarrow> strip C1 = strip C2 \<and> annos C1 = annos C2"
nipkow@52019
   115
apply(induction C1 arbitrary: C2)
nipkow@52019
   116
apply(case_tac C2, auto simp: size_annos_same2)+
nipkow@52019
   117
done
nipkow@52019
   118
nipkow@52019
   119
lemma eq_acom_iff_strip_anno:
nipkow@52019
   120
  "C1=C2 \<longleftrightarrow> strip C1 = strip C2 \<and> (\<forall>p<size(annos C1). anno C1 p = anno C2 p)"
nipkow@52019
   121
by(auto simp add: eq_acom_iff_strip_annos anno_def
nipkow@52019
   122
     list_eq_iff_nth_eq size_annos_same2)
nipkow@52019
   123
nipkow@49477
   124
lemma post_map_acom[simp]: "post(map_acom f C) = f(post C)"
nipkow@52019
   125
by (induction C) (auto simp: post_def last_append annos_ne)
nipkow@45623
   126
nipkow@52019
   127
lemma strip_map_acom[simp]: "strip (map_acom f C) = strip C"
nipkow@49477
   128
by (induction C) auto
nipkow@45623
   129
nipkow@52019
   130
lemma anno_map_acom: "p < size(annos C) \<Longrightarrow> anno (map_acom f C) p = f(anno C p)"
nipkow@52019
   131
apply(induction C arbitrary: p)
nipkow@52019
   132
apply(auto simp: anno_def nth_append nth_Cons' size_annos)
nipkow@52019
   133
done
nipkow@45623
   134
nipkow@46157
   135
lemma strip_eq_SKIP:
nipkow@54941
   136
  "strip C = SKIP \<longleftrightarrow> (EX P. C = SKIP {P})"
nipkow@49095
   137
by (cases C) simp_all
nipkow@46157
   138
nipkow@46157
   139
lemma strip_eq_Assign:
nipkow@49095
   140
  "strip C = x::=e \<longleftrightarrow> (EX P. C = x::=e {P})"
nipkow@49095
   141
by (cases C) simp_all
nipkow@46157
   142
nipkow@47818
   143
lemma strip_eq_Seq:
nipkow@52046
   144
  "strip C = c1;;c2 \<longleftrightarrow> (EX C1 C2. C = C1;;C2 & strip C1 = c1 & strip C2 = c2)"
nipkow@49095
   145
by (cases C) simp_all
nipkow@45623
   146
nipkow@45623
   147
lemma strip_eq_If:
nipkow@49095
   148
  "strip C = IF b THEN c1 ELSE c2 \<longleftrightarrow>
nipkow@49477
   149
  (EX P1 P2 C1 C2 Q. C = IF b THEN {P1} C1 ELSE {P2} C2 {Q} & strip C1 = c1 & strip C2 = c2)"
nipkow@49095
   150
by (cases C) simp_all
nipkow@45623
   151
nipkow@45623
   152
lemma strip_eq_While:
nipkow@49095
   153
  "strip C = WHILE b DO c1 \<longleftrightarrow>
nipkow@49477
   154
  (EX I P C1 Q. C = {I} WHILE b DO {P} C1 {Q} & strip C1 = c1)"
nipkow@49095
   155
by (cases C) simp_all
nipkow@47613
   156
nipkow@52019
   157
lemma [simp]: "shift (\<lambda>p. a) n = (\<lambda>p. a)"
nipkow@52019
   158
by(simp add:shift_def)
nipkow@47613
   159
nipkow@52019
   160
lemma set_annos_anno[simp]: "set (annos (annotate (\<lambda>p. a) c)) = {a}"
nipkow@52019
   161
by(induction c) simp_all
nipkow@47613
   162
nipkow@51712
   163
lemma post_in_annos: "post C \<in> set(annos C)"
nipkow@52019
   164
by(auto simp: post_def annos_ne)
nipkow@52019
   165
nipkow@52019
   166
lemma post_anno_asize: "post C = anno C (size(annos C) - 1)"
nipkow@52019
   167
by(simp add: post_def last_conv_nth[OF annos_ne] anno_def)
nipkow@51712
   168
nipkow@45623
   169
end