author | wenzelm |
Mon, 17 Mar 2008 18:37:00 +0100 | |
changeset 26300 | 03def556e26e |
parent 22819 | a7b425bb668c |
child 26342 | 0f65fa163304 |
permissions | -rw-r--r-- |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
1 |
(* Title: HOL/Modelcheck/MuckeSyn.thy |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
3 |
Author: Tobias Hamberger |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
4 |
Copyright 1999 TU Muenchen |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
5 |
*) |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
6 |
|
17272 | 7 |
theory MuckeSyn |
8 |
imports MuCalculus |
|
9 |
uses "mucke_oracle.ML" |
|
10 |
begin |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
11 |
|
17272 | 12 |
(* extended with some operators and case treatment (which requires postprocessing with |
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
13 |
transform_case (from MuCalculus) (TH) *) |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
14 |
|
17272 | 15 |
nonterminals |
16 |
mutype |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
17 |
decl decls |
17272 | 18 |
cases_syn case_syn |
10125 | 19 |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
20 |
syntax (Mucke output) |
17272 | 21 |
True :: bool ("true") |
22 |
False :: bool ("false") |
|
23 |
Not :: "bool => bool" ("! _" [40] 40) |
|
24 |
If :: "[bool, 'a, 'a] => 'a" ("('(if'((_)')/ '((_)')/ else/ '((_)'))')" 10) |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
25 |
|
17272 | 26 |
"op &" :: "[bool, bool] => bool" (infixr "&" 35) |
27 |
"op |" :: "[bool, bool] => bool" (infixr "|" 30) |
|
28 |
"op -->" :: "[bool, bool] => bool" (infixr "->" 25) |
|
29 |
"op =" :: "['a, 'a] => bool" ("(_ =/ _)" [51, 51] 50) |
|
30 |
"_not_equal" :: "['a, 'a] => bool" ("(_ !=/ _)" [51, 51] 50) |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
31 |
|
21524 | 32 |
All_binder :: "[idts, bool] => bool" ("'((3forall _./ _)')" [0, 10] 10) |
33 |
Ex_binder :: "[idts, bool] => bool" ("'((3exists _./ _)')" [0, 10] 10) |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
34 |
|
17272 | 35 |
"_lambda" :: "[idts, 'a] => 'b" ("(3L _./ _)" 10) |
36 |
"_applC" :: "[('b => 'a), cargs] => aprop" ("(1_/ '(_'))" [1000,1000] 999) |
|
37 |
"_cargs" :: "['a, cargs] => cargs" ("_,/ _" [1000,1000] 1000) |
|
38 |
||
39 |
"_idts" :: "[idt, idts] => idts" ("_,/ _" [1, 0] 0) |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
40 |
|
9368 | 41 |
"_tuple" :: "'a => tuple_args => 'a * 'b" ("(1_,/ _)") |
17272 | 42 |
(* "@pttrn" :: "[pttrn, pttrns] => pttrn" ("_,/ _" [1, 0] 0) |
43 |
"_pattern" :: "[pttrn, patterns] => pttrn" ("_,/ _" [1, 0] 0) *) |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
44 |
|
17272 | 45 |
"_decl" :: "[mutype,pttrn] => decl" ("_ _") |
46 |
"_decls" :: "[decl,decls] => decls" ("_,/ _") |
|
47 |
"" :: "decl => decls" ("_") |
|
48 |
"_mu" :: "[decl,decls,'a pred] => 'a pred" ("mu _ '(_') _ ;") |
|
49 |
"_mudec" :: "[decl,decls] => 'a pred" ("mu _ '(_') ;") |
|
50 |
"_nu" :: "[decl,decls,'a pred] => 'a pred" ("nu _ '(_') _ ;") |
|
51 |
"_nudec" :: "[decl,decls] => 'a pred" ("nu _ '(_') ;") |
|
52 |
"_fun" :: "[decl,decls,'a pred] => 'a pred" ("_ '(_') _ ;") |
|
53 |
"_dec" :: "[decl,decls] => 'a pred" ("_ '(_') ;") |
|
54 |
||
55 |
"_Ex" :: "[decl,idts,'a pred] => 'a pred" ("'((3exists _ _./ _)')") |
|
56 |
"_All" :: "[decl,idts,'a pred] => 'a pred" ("'((3forall _ _./ _)')") |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
57 |
|
17272 | 58 |
"Mu " :: "[idts, 'a pred] => 'a pred" ("(3mu _./ _)" 1000) |
59 |
"Nu " :: "[idts, 'a pred] => 'a pred" ("(3nu _./ _)" 1000) |
|
60 |
||
61 |
"_case_syntax":: "['a, cases_syn] => 'b" ("(case*_* / _ / esac*)" 10) |
|
62 |
"_case1" :: "['a, 'b] => case_syn" ("(2*= _ :/ _;)" 10) |
|
63 |
"" :: "case_syn => cases_syn" ("_") |
|
64 |
"_case2" :: "[case_syn, cases_syn] => cases_syn" ("_/ _") |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
65 |
|
17272 | 66 |
(*Terms containing a case statement must be post-processed with the |
67 |
ML function transform_case. There, all asterikses before the "=" |
|
68 |
will be replaced by the expression between the two asterisks |
|
69 |
following "case" and the asterisk after esac will be deleted *) |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
70 |
|
17272 | 71 |
oracle mc_mucke_oracle ("term") = |
72 |
mk_mc_mucke_oracle |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
73 |
|
22819 | 74 |
ML {* |
75 |
(* search_mu t searches for Mu terms in term t. In the case of nested Mu's, |
|
76 |
it yields innermost one. If no Mu term is present, search_mu yields NONE |
|
77 |
*) |
|
78 |
||
79 |
(* extended for treatment of nu (TH) *) |
|
80 |
fun search_mu ((Const("MuCalculus.mu",tp)) $ t2) = |
|
81 |
(case (search_mu t2) of |
|
82 |
SOME t => SOME t |
|
83 |
| NONE => SOME ((Const("MuCalculus.mu",tp)) $ t2)) |
|
84 |
| search_mu ((Const("MuCalculus.nu",tp)) $ t2) = |
|
85 |
(case (search_mu t2) of |
|
86 |
SOME t => SOME t |
|
87 |
| NONE => SOME ((Const("MuCalculus.nu",tp)) $ t2)) |
|
88 |
| search_mu (t1 $ t2) = |
|
89 |
(case (search_mu t1) of |
|
90 |
SOME t => SOME t |
|
91 |
| NONE => search_mu t2) |
|
92 |
| search_mu (Abs(_,_,t)) = search_mu t |
|
93 |
| search_mu _ = NONE; |
|
94 |
||
95 |
||
96 |
||
97 |
||
98 |
(* seraching a variable in a term. Used in move_mus to extract the |
|
99 |
term-rep of var b in hthm *) |
|
100 |
||
101 |
fun search_var s t = |
|
102 |
case t of |
|
103 |
t1 $ t2 => (case (search_var s t1) of |
|
104 |
SOME tt => SOME tt | |
|
105 |
NONE => search_var s t2) | |
|
106 |
Abs(_,_,t) => search_var s t | |
|
107 |
Var((s1,_),_) => if s = s1 then SOME t else NONE | |
|
108 |
_ => NONE; |
|
109 |
||
110 |
||
111 |
(* function move_mus: |
|
112 |
Mucke can't deal with nested Mu terms. move_mus i searches for |
|
113 |
Mu terms in the subgoal i and replaces Mu terms in the conclusion |
|
114 |
by constants and definitions in the premises recursively. |
|
115 |
||
116 |
move_thm is the theorem the performs the replacement. To create NEW |
|
117 |
names for the Mu terms, the indizes of move_thm are incremented by |
|
118 |
max_idx of the subgoal. |
|
119 |
*) |
|
120 |
||
121 |
local |
|
122 |
||
123 |
val move_thm = prove_goal (the_context ()) "[| a = b ==> P a; a = b |] ==> P b" |
|
124 |
(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1, |
|
125 |
REPEAT (resolve_tac prems 1)]); |
|
126 |
||
127 |
val sig_move_thm = Thm.theory_of_thm move_thm; |
|
128 |
val bCterm = cterm_of sig_move_thm (valOf (search_var "b" (concl_of move_thm))); |
|
129 |
val aCterm = cterm_of sig_move_thm (valOf (search_var "a" (hd(prems_of move_thm)))); |
|
130 |
||
131 |
in |
|
132 |
||
133 |
fun move_mus i state = |
|
134 |
let val sign = Thm.theory_of_thm state; |
|
135 |
val (subgoal::_) = Library.drop(i-1,prems_of state); |
|
136 |
val concl = Logic.strip_imp_concl subgoal; (* recursive mu's in prems? *) |
|
137 |
val redex = search_mu concl; |
|
138 |
val idx = let val t = #maxidx (rep_thm state) in |
|
139 |
if t < 0 then 1 else t+1 end; |
|
140 |
in |
|
141 |
case redex of |
|
142 |
NONE => all_tac state | |
|
143 |
SOME redexterm => |
|
144 |
let val Credex = cterm_of sign redexterm; |
|
145 |
val aiCterm = |
|
146 |
cterm_of sig_move_thm (Logic.incr_indexes ([],idx) (term_of aCterm)); |
|
147 |
val inst_move_thm = cterm_instantiate |
|
148 |
[(bCterm,Credex),(aCterm,aiCterm)] move_thm; |
|
149 |
in |
|
150 |
((rtac inst_move_thm i) THEN (dtac eq_reflection i) |
|
151 |
THEN (move_mus i)) state |
|
152 |
end |
|
153 |
end; |
|
154 |
end; |
|
6466
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
155 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
156 |
|
22819 | 157 |
fun call_mucke_tac i state = |
158 |
let val thy = Thm.theory_of_thm state; |
|
159 |
val OraAss = mc_mucke_oracle thy (Logic.nth_prem (i, Thm.prop_of state)) |
|
160 |
in |
|
161 |
(cut_facts_tac [OraAss] i) state |
|
162 |
end; |
|
163 |
||
164 |
||
165 |
(* transforming fun-defs into lambda-defs *) |
|
166 |
||
167 |
val [eq] = goal CPure.thy "(!! x. f x == g x) ==> f == g"; |
|
168 |
by (rtac (extensional eq) 1); |
|
169 |
qed "ext_rl"; |
|
170 |
||
171 |
infix cc; |
|
172 |
||
173 |
fun NONE cc xl = xl |
|
174 |
| (SOME x) cc xl = x::xl; |
|
175 |
||
176 |
fun getargs ((x $ y) $ (Var ((z,_),_))) = getargs (x $ y) ^ " " ^z |
|
177 |
| getargs (x $ (Var ((y,_),_))) = y; |
|
178 |
||
179 |
fun getfun ((x $ y) $ z) = getfun (x $ y) |
|
180 |
| getfun (x $ _) = x; |
|
181 |
||
182 |
local |
|
183 |
||
184 |
fun delete_bold [] = [] |
|
185 |
| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs)) |
|
186 |
then (let val (_::_::_::s) = xs in delete_bold s end) |
|
187 |
else (if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs)) |
|
188 |
then (let val (_::_::_::s) = xs in delete_bold s end) |
|
189 |
else (x::delete_bold xs)); |
|
190 |
||
191 |
fun delete_bold_string s = implode(delete_bold (explode s)); |
|
192 |
||
193 |
in |
|
194 |
||
195 |
(* extension with removing bold font (TH) *) |
|
196 |
fun mk_lam_def (_::_) _ _ = NONE |
|
197 |
| mk_lam_def [] ((Const("==",_) $ (Const _)) $ RHS) t = SOME t |
|
198 |
| mk_lam_def [] ((Const("==",_) $ LHS) $ RHS) t = |
|
199 |
let val thy = theory_of_thm t; |
|
200 |
val fnam = Sign.string_of_term thy (getfun LHS); |
|
201 |
val rhs = Sign.string_of_term thy (freeze_thaw RHS) |
|
202 |
val gl = delete_bold_string (fnam ^" == % " ^ (getargs LHS) ^" . " ^ rhs); |
|
203 |
in |
|
204 |
SOME (prove_goal thy gl (fn prems => |
|
205 |
[(REPEAT (rtac ext_rl 1)), (rtac t 1) ])) |
|
206 |
end |
|
207 |
| mk_lam_def [] _ t= NONE; |
|
208 |
||
209 |
fun mk_lam_defs ([]:thm list) = ([]: thm list) |
|
210 |
| mk_lam_defs (t::l) = |
|
211 |
(mk_lam_def (prems_of t) (concl_of t) t) cc (mk_lam_defs l); |
|
212 |
||
213 |
end; |
|
214 |
||
215 |
||
216 |
(* first simplification, then model checking *) |
|
217 |
||
218 |
val pair_eta_expand = Thm.symmetric (mk_meta_eq (thm "split_eta")); |
|
219 |
||
220 |
val pair_eta_expand_proc = |
|
221 |
Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"] |
|
222 |
(fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE); |
|
223 |
||
224 |
val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def]; |
|
225 |
||
226 |
||
227 |
(* the interface *) |
|
228 |
||
229 |
fun mc_mucke_tac defs i state = |
|
230 |
(case Library.drop (i - 1, Thm.prems_of state) of |
|
231 |
[] => no_tac state |
|
232 |
| subgoal :: _ => |
|
233 |
EVERY [ |
|
234 |
REPEAT (etac thin_rl i), |
|
235 |
cut_facts_tac (mk_lam_defs defs) i, |
|
236 |
full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i, |
|
237 |
move_mus i, call_mucke_tac i,atac i, |
|
238 |
REPEAT (rtac refl i)] state); |
|
239 |
||
240 |
(*check if user has mucke installed*) |
|
241 |
fun mucke_enabled () = getenv "MUCKE_HOME" <> ""; |
|
242 |
fun if_mucke_enabled f x = if mucke_enabled () then f x else (); |
|
243 |
||
244 |
*} |
|
245 |
||
246 |
end |