author | ballarin |
Fri, 13 Apr 2007 10:00:04 +0200 | |
changeset 22657 | 731622340817 |
parent 21524 | 7843e2fd14a9 |
child 22819 | a7b425bb668c |
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 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
74 |
end |
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
75 |
|
2eba94dc5951
added modelchecker mucke besides modelchecker eindhoven;
mueller
parents:
diff
changeset
|
76 |