UTP-IMP/Example_Programs.thy at main · isabelle-utp/UTP-IMP · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
theory Example_Programs
  imports "UTP_IMP"
begin

declare [[literal_variables]]

alphabet st =
  x :: int
  y :: int

record_default st

subsection \<open> Toy Programs \<close>

definition myprog1 :: "st prog" where
"myprog1 = x := 0 ; while x < 10 do x := x + 1 od"

definition myprog2 :: "st prog" where
"myprog2 = (x := 0) \<sqinter> (x := 3) \<sqinter> (x := 1)"

execute myprog1

value "final_states myprog1 default"

value "exec_prog myprog1"

lemma "H{True} myprog1 {x = 10}"
  unfolding myprog1_def
  apply (sequence "x = 0")
   apply assign
   apply subst_eval'
  apply simp
  apply (while "x \<le> 10")
    apply simp
   apply assign
   apply subst_eval'
   apply simp
  apply simp
  done

value "final_states myprog2 default"

value "exec_prog myprog2"

subsection \<open> Euclidean algorithm \<close>

program Eucl "(X :: int, Y :: int)" over st =
"x := X;
 y := Y;
 while x \<noteq> y
 do if x < y
    then y := y - x
    else x := x - y
    fi
 od"

execute "Eucl(21, 15)"

lemma Eucl_correct: "H{True} Eucl(X, Y) {\<bar>x\<bar> = gcd X Y}"
  apply (simp add: Eucl_def)
  apply (sequence "x = X")
   apply assign
   apply subst_eval'
   apply simp
  apply (sequence "x = X \<and> y = Y")
   apply assign
     apply subst_eval'
   apply simp
  apply (while "gcd x y = gcd X Y")
    apply simp
   apply if_then_else
    apply assign
  apply subst_eval
    apply (metis (no_types, lifting) SEXP_def gcd.commute gcd_diff1 tautI)
   apply assign
  apply subst_eval
   apply (metis (no_types, lifting) SEXP_def gcd_diff1 tautI)
  apply expr_simp
  done

program Eucl_ann "(X :: int, Y :: int)" over st =
"x := X;
 y := Y;
 while x \<noteq> y
 invariant gcd X Y = gcd x y
 do
    if x < y
    then y := y - x
    else x := x - y
    fi
 od"

lemma Eucl_correct': "H{True} Eucl_ann(X, Y) {\<bar>x\<bar> = gcd X Y}"
  apply vcg
  apply (metis gcd.commute gcd_diff1)
  apply (simp add: gcd_diff1)
  done

end