equal
deleted
inserted
replaced
16 (*<*)term "A \<union> B" term "A \<inter> B" term "A - B" |
16 (*<*)term "A \<union> B" term "A \<inter> B" term "A - B" |
17 term "a \<in> A" term "b \<notin> A" |
17 term "a \<in> A" term "b \<notin> A" |
18 term "{a,b}" term "{x. P x}" |
18 term "{a,b}" term "{x. P x}" |
19 term "\<Union> M" term "\<Union>a \<in> A. F a"(*>*) |
19 term "\<Union> M" term "\<Union>a \<in> A. F a"(*>*) |
20 |
20 |
|
21 |
21 subsection{*Some Functions*} |
22 subsection{*Some Functions*} |
22 |
23 |
23 text{* |
24 text{* |
24 \begin{tabular}{l} |
25 \begin{tabular}{l} |
25 @{thm id_def}\\ |
26 @{thm id_def}\\ |
26 @{thm o_def[no_vars]}\\ |
27 @{thm o_def[no_vars]}\\ |
27 @{thm image_def[no_vars]}\\ |
28 @{thm image_def[no_vars]}\\ |
28 @{thm vimage_def[no_vars]} |
29 @{thm vimage_def[no_vars]} |
29 \end{tabular}*} |
30 \end{tabular}*} |
30 (*<*)thm id_def o_def[no_vars] image_def[no_vars] vimage_def[no_vars](*>*) |
31 (*<*)thm id_def o_def[no_vars] image_def[no_vars] vimage_def[no_vars](*>*) |
|
32 |
31 |
33 |
32 subsection{*Some Relations*} |
34 subsection{*Some Relations*} |
33 |
35 |
34 text{* |
36 text{* |
35 \begin{tabular}{l} |
37 \begin{tabular}{l} |
45 thm Image_def[no_vars] |
47 thm Image_def[no_vars] |
46 thm relpow.simps[no_vars] |
48 thm relpow.simps[no_vars] |
47 thm rtrancl.intros[no_vars] |
49 thm rtrancl.intros[no_vars] |
48 thm trancl_def[no_vars](*>*) |
50 thm trancl_def[no_vars](*>*) |
49 |
51 |
|
52 |
50 subsection{*Wellfoundedness*} |
53 subsection{*Wellfoundedness*} |
51 |
54 |
52 text{* |
55 text{* |
53 \begin{tabular}{l} |
56 \begin{tabular}{l} |
54 @{thm wf_def[no_vars]}\\ |
57 @{thm wf_def[no_vars]}\\ |
55 @{thm wf_iff_no_infinite_down_chain[no_vars]} |
58 @{thm wf_iff_no_infinite_down_chain[no_vars]} |
56 \end{tabular}*} |
59 \end{tabular}*} |
57 (*<*)thm wf_def[no_vars] |
60 (*<*)thm wf_def[no_vars] |
58 thm wf_iff_no_infinite_down_chain[no_vars](*>*) |
61 thm wf_iff_no_infinite_down_chain[no_vars](*>*) |
|
62 |
59 |
63 |
60 subsection{*Fixed Point Operators*} |
64 subsection{*Fixed Point Operators*} |
61 |
65 |
62 text{* |
66 text{* |
63 \begin{tabular}{l} |
67 \begin{tabular}{l} |
67 \end{tabular}*} |
71 \end{tabular}*} |
68 (*<*)thm lfp_def gfp_def |
72 (*<*)thm lfp_def gfp_def |
69 thm lfp_unfold |
73 thm lfp_unfold |
70 thm lfp_induct(*>*) |
74 thm lfp_induct(*>*) |
71 |
75 |
|
76 |
72 subsection{*Case Study: Verified Model Checking*} |
77 subsection{*Case Study: Verified Model Checking*} |
73 |
|
74 |
78 |
75 typedecl state |
79 typedecl state |
76 |
80 |
77 consts M :: "(state \<times> state)set" |
81 consts M :: "(state \<times> state)set" |
78 |
82 |
79 typedecl atom |
83 typedecl atom |
80 |
84 |
81 consts L :: "state \<Rightarrow> atom set" |
85 consts L :: "state \<Rightarrow> atom set" |
82 |
86 |
83 datatype formula = Atom atom |
87 datatype formula = Atom atom |
84 | Neg formula |
88 | Neg formula |
85 | And formula formula |
89 | And formula formula |
86 | AX formula |
90 | AX formula |
87 | EF formula |
91 | EF formula |
88 |
92 |
89 consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80) |
93 consts valid :: "state \<Rightarrow> formula \<Rightarrow> bool" ("(_ \<Turnstile> _)" [80,80] 80) |
90 |
94 |
91 primrec |
95 primrec |
92 "s \<Turnstile> Atom a = (a \<in> L s)" |
96 "s \<Turnstile> Atom a = (a \<in> L s)" |