author | nipkow |
Fri, 04 Dec 2020 15:07:47 +0100 | |
changeset 72806 | 4fa08e083865 |
parent 69597 | ff784d5a5bfb |
child 72987 | b1be35908165 |
permissions | -rw-r--r-- |
42153 | 1 |
(* Title: HOL/Hoare/hoare_syntax.ML |
2 |
Author: Leonor Prensa Nieto & Tobias Nipkow |
|
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
3 |
Author: Walter Guttmann (extension to total-correctness proofs) |
42153 | 4 |
|
5 |
Syntax translations for Hoare logic. |
|
6 |
*) |
|
7 |
||
8 |
signature HOARE_SYNTAX = |
|
9 |
sig |
|
10 |
val hoare_vars_tr: term list -> term |
|
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
11 |
val hoare_tc_vars_tr: term list -> term |
42153 | 12 |
val spec_tr': string -> term list -> term |
13 |
end; |
|
14 |
||
15 |
structure Hoare_Syntax: HOARE_SYNTAX = |
|
16 |
struct |
|
17 |
||
18 |
(** parse translation **) |
|
19 |
||
20 |
local |
|
21 |
||
22 |
fun idt_name (Free (x, _)) = SOME x |
|
69597 | 23 |
| idt_name (Const (\<^syntax_const>\<open>_constrain\<close>, _) $ t $ _) = idt_name t |
42153 | 24 |
| idt_name _ = NONE; |
25 |
||
26 |
fun eq_idt tu = |
|
59058
a78612c67ec0
renamed "pairself" to "apply2", in accordance to @{apply 2};
wenzelm
parents:
55659
diff
changeset
|
27 |
(case apply2 idt_name tu of |
42153 | 28 |
(SOME x, SOME y) => x = y |
29 |
| _ => false); |
|
30 |
||
42284 | 31 |
fun mk_abstuple [x] body = Syntax_Trans.abs_tr [x, body] |
42153 | 32 |
| mk_abstuple (x :: xs) body = |
69597 | 33 |
Syntax.const \<^const_syntax>\<open>case_prod\<close> $ Syntax_Trans.abs_tr [x, mk_abstuple xs body]; |
42153 | 34 |
|
35 |
fun mk_fbody x e [y] = if eq_idt (x, y) then e else y |
|
36 |
| mk_fbody x e (y :: xs) = |
|
69597 | 37 |
Syntax.const \<^const_syntax>\<open>Pair\<close> $ |
42153 | 38 |
(if eq_idt (x, y) then e else y) $ mk_fbody x e xs; |
39 |
||
40 |
fun mk_fexp x e xs = mk_abstuple xs (mk_fbody x e xs); |
|
41 |
||
42 |
||
43 |
(* bexp_tr & assn_tr *) |
|
44 |
(*all meta-variables for bexp except for TRUE are translated as if they |
|
45 |
were boolean expressions*) |
|
46 |
||
55659 | 47 |
fun bexp_tr (Const ("TRUE", _)) _ = Syntax.const "TRUE" (* FIXME !? *) |
69597 | 48 |
| bexp_tr b xs = Syntax.const \<^const_syntax>\<open>Collect\<close> $ mk_abstuple xs b; |
42153 | 49 |
|
69597 | 50 |
fun assn_tr r xs = Syntax.const \<^const_syntax>\<open>Collect\<close> $ mk_abstuple xs r; |
42153 | 51 |
|
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
52 |
fun var_tr v xs = mk_abstuple xs v; |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
53 |
|
42153 | 54 |
|
55 |
(* com_tr *) |
|
56 |
||
69597 | 57 |
fun com_tr (Const (\<^syntax_const>\<open>_assign\<close>, _) $ x $ e) xs = |
58 |
Syntax.const \<^const_syntax>\<open>Basic\<close> $ mk_fexp x e xs |
|
59 |
| com_tr (Const (\<^const_syntax>\<open>Basic\<close>,_) $ f) _ = Syntax.const \<^const_syntax>\<open>Basic\<close> $ f |
|
60 |
| com_tr (Const (\<^const_syntax>\<open>Seq\<close>,_) $ c1 $ c2) xs = |
|
61 |
Syntax.const \<^const_syntax>\<open>Seq\<close> $ com_tr c1 xs $ com_tr c2 xs |
|
62 |
| com_tr (Const (\<^const_syntax>\<open>Cond\<close>,_) $ b $ c1 $ c2) xs = |
|
63 |
Syntax.const \<^const_syntax>\<open>Cond\<close> $ bexp_tr b xs $ com_tr c1 xs $ com_tr c2 xs |
|
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
64 |
| com_tr (Const (\<^const_syntax>\<open>While\<close>,_) $ b $ I $ V $ c) xs = |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
65 |
Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr b xs $ assn_tr I xs $ var_tr V xs $ com_tr c xs |
42153 | 66 |
| com_tr t _ = t; |
67 |
||
69597 | 68 |
fun vars_tr (Const (\<^syntax_const>\<open>_idts\<close>, _) $ idt $ vars) = idt :: vars_tr vars |
42153 | 69 |
| vars_tr t = [t]; |
70 |
||
71 |
in |
|
72 |
||
73 |
fun hoare_vars_tr [vars, pre, prg, post] = |
|
74 |
let val xs = vars_tr vars |
|
69597 | 75 |
in Syntax.const \<^const_syntax>\<open>Valid\<close> $ |
42153 | 76 |
assn_tr pre xs $ com_tr prg xs $ assn_tr post xs |
77 |
end |
|
78 |
| hoare_vars_tr ts = raise TERM ("hoare_vars_tr", ts); |
|
79 |
||
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
80 |
fun hoare_tc_vars_tr [vars, pre, prg, post] = |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
81 |
let val xs = vars_tr vars |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
82 |
in Syntax.const \<^const_syntax>\<open>ValidTC\<close> $ |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
83 |
assn_tr pre xs $ com_tr prg xs $ assn_tr post xs |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
84 |
end |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
85 |
| hoare_tc_vars_tr ts = raise TERM ("hoare_tc_vars_tr", ts); |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
86 |
|
42153 | 87 |
end; |
88 |
||
89 |
||
90 |
||
91 |
(** print translation **) |
|
92 |
||
93 |
local |
|
94 |
||
95 |
fun dest_abstuple |
|
69597 | 96 |
(Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (v, _, body)) = |
42153 | 97 |
subst_bound (Syntax.free v, dest_abstuple body) |
98 |
| dest_abstuple (Abs (v,_, body)) = subst_bound (Syntax.free v, body) |
|
99 |
| dest_abstuple tm = tm; |
|
100 |
||
69597 | 101 |
fun abs2list (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t |
55659 | 102 |
| abs2list (Abs (x, T, _)) = [Free (x, T)] |
42153 | 103 |
| abs2list _ = []; |
104 |
||
69597 | 105 |
fun mk_ts (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs (_, _, t)) = mk_ts t |
55659 | 106 |
| mk_ts (Abs (_, _, t)) = mk_ts t |
69597 | 107 |
| mk_ts (Const (\<^const_syntax>\<open>Pair\<close>, _) $ a $ b) = a :: mk_ts b |
42153 | 108 |
| mk_ts t = [t]; |
109 |
||
69597 | 110 |
fun mk_vts (Const (\<^const_syntax>\<open>case_prod\<close>,_) $ Abs (x, _, t)) = |
42153 | 111 |
(Syntax.free x :: abs2list t, mk_ts t) |
112 |
| mk_vts (Abs (x, _, t)) = ([Syntax.free x], [t]) |
|
55659 | 113 |
| mk_vts _ = raise Match; |
42153 | 114 |
|
55659 | 115 |
fun find_ch [] _ _ = (false, (Syntax.free "not_ch", Syntax.free "not_ch")) (* FIXME no_ch!? *) |
42153 | 116 |
| find_ch ((v, t) :: vts) i xs = |
117 |
if t = Bound i then find_ch vts (i - 1) xs |
|
118 |
else (true, (v, subst_bounds (xs, t))); |
|
119 |
||
69597 | 120 |
fun is_f (Const (\<^const_syntax>\<open>case_prod\<close>, _) $ Abs _) = true |
55659 | 121 |
| is_f (Abs _) = true |
122 |
| is_f _ = false; |
|
42153 | 123 |
|
124 |
||
125 |
(* assn_tr' & bexp_tr'*) |
|
126 |
||
69597 | 127 |
fun assn_tr' (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T) = dest_abstuple T |
128 |
| assn_tr' (Const (\<^const_syntax>\<open>inter\<close>, _) $ |
|
129 |
(Const (\<^const_syntax>\<open>Collect\<close>, _) $ T1) $ (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T2)) = |
|
130 |
Syntax.const \<^const_syntax>\<open>inter\<close> $ dest_abstuple T1 $ dest_abstuple T2 |
|
42153 | 131 |
| assn_tr' t = t; |
132 |
||
69597 | 133 |
fun bexp_tr' (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T) = dest_abstuple T |
42153 | 134 |
| bexp_tr' t = t; |
135 |
||
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
136 |
fun var_tr' (Const (\<^const_syntax>\<open>Collect\<close>, _) $ T) = dest_abstuple T |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
137 |
| var_tr' t = t; |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
138 |
|
42153 | 139 |
|
140 |
(* com_tr' *) |
|
141 |
||
142 |
fun mk_assign f = |
|
143 |
let |
|
144 |
val (vs, ts) = mk_vts f; |
|
145 |
val (ch, which) = find_ch (vs ~~ ts) (length vs - 1) (rev vs); |
|
146 |
in |
|
147 |
if ch |
|
69597 | 148 |
then Syntax.const \<^syntax_const>\<open>_assign\<close> $ fst which $ snd which |
149 |
else Syntax.const \<^const_syntax>\<open>annskip\<close> |
|
42153 | 150 |
end; |
151 |
||
69597 | 152 |
fun com_tr' (Const (\<^const_syntax>\<open>Basic\<close>, _) $ f) = |
42153 | 153 |
if is_f f then mk_assign f |
69597 | 154 |
else Syntax.const \<^const_syntax>\<open>Basic\<close> $ f |
155 |
| com_tr' (Const (\<^const_syntax>\<open>Seq\<close>,_) $ c1 $ c2) = |
|
156 |
Syntax.const \<^const_syntax>\<open>Seq\<close> $ com_tr' c1 $ com_tr' c2 |
|
157 |
| com_tr' (Const (\<^const_syntax>\<open>Cond\<close>, _) $ b $ c1 $ c2) = |
|
158 |
Syntax.const \<^const_syntax>\<open>Cond\<close> $ bexp_tr' b $ com_tr' c1 $ com_tr' c2 |
|
72806
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
159 |
| com_tr' (Const (\<^const_syntax>\<open>While\<close>, _) $ b $ I $ V $ c) = |
4fa08e083865
Extension of session HOL/Hoare with total correctness proof system by Walter Guttmann
nipkow
parents:
69597
diff
changeset
|
160 |
Syntax.const \<^const_syntax>\<open>While\<close> $ bexp_tr' b $ assn_tr' I $ var_tr' V $ com_tr' c |
42153 | 161 |
| com_tr' t = t; |
162 |
||
163 |
in |
|
164 |
||
55659 | 165 |
fun spec_tr' syn [p, c, q] = Syntax.const syn $ assn_tr' p $ com_tr' c $ assn_tr' q; |
42153 | 166 |
|
167 |
end; |
|
168 |
||
169 |
end; |
|
170 |