author | kleing |
Mon, 21 Jun 2004 10:25:57 +0200 | |
changeset 14981 | e73f8140af78 |
parent 12218 | 6597093b77e7 |
child 17233 | 41eee2e7b465 |
permissions | -rw-r--r-- |
4559 | 1 |
(* Title: HOLCF/IOA/meta_theory/TL.ML |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller |
4559 | 4 |
|
12218 | 5 |
Temporal Logic. |
4559 | 6 |
*) |
7 |
||
8 |
||
5068 | 9 |
Goal "[] <> (.~ P) = (.~ <> [] P)"; |
5132 | 10 |
by (rtac ext 1); |
4559 | 11 |
by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1); |
5132 | 12 |
by Auto_tac; |
5976 | 13 |
qed"simple"; |
4559 | 14 |
|
5068 | 15 |
Goal "nil |= [] P"; |
4559 | 16 |
by (asm_full_simp_tac (simpset() addsimps [satisfies_def, |
17 |
Box_def,tsuffix_def,suffix_def,nil_is_Conc])1); |
|
18 |
qed"Boxnil"; |
|
19 |
||
5068 | 20 |
Goal "~(nil |= <> P)"; |
4559 | 21 |
by (simp_tac (simpset() addsimps [Diamond_def,satisfies_def,NOT_def])1); |
22 |
by (cut_inst_tac [] Boxnil 1); |
|
23 |
by (asm_full_simp_tac (simpset() addsimps [satisfies_def])1); |
|
24 |
qed"Diamondnil"; |
|
25 |
||
5068 | 26 |
Goal "(<> F) s = (? s2. tsuffix s2 s & F s2)"; |
4559 | 27 |
by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1); |
28 |
qed"Diamond_def2"; |
|
29 |
||
30 |
||
31 |
||
32 |
section "TLA Axiomatization by Merz"; |
|
33 |
||
34 |
(* ---------------------------------------------------------------- *) |
|
35 |
(* TLA Axiomatization by Merz *) |
|
36 |
(* ---------------------------------------------------------------- *) |
|
37 |
||
5068 | 38 |
Goal "suffix s s"; |
4559 | 39 |
by (simp_tac (simpset() addsimps [suffix_def])1); |
40 |
by (res_inst_tac [("x","nil")] exI 1); |
|
5132 | 41 |
by Auto_tac; |
4559 | 42 |
qed"suffix_refl"; |
43 |
||
5068 | 44 |
Goal "s~=UU & s~=nil --> (s |= [] F .--> F)"; |
4559 | 45 |
by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def])1); |
46 |
by (REPEAT (rtac impI 1)); |
|
47 |
by (eres_inst_tac [("x","s")] allE 1); |
|
48 |
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1); |
|
49 |
qed"reflT"; |
|
50 |
||
51 |
||
6161 | 52 |
Goal "[| suffix y x ; suffix z y |] ==> suffix z x"; |
4559 | 53 |
by (asm_full_simp_tac (simpset() addsimps [suffix_def])1); |
5132 | 54 |
by Auto_tac; |
4559 | 55 |
by (res_inst_tac [("x","s1 @@ s1a")] exI 1); |
5132 | 56 |
by Auto_tac; |
4559 | 57 |
by (simp_tac (simpset() addsimps [Conc_assoc]) 1); |
58 |
qed"suffix_trans"; |
|
59 |
||
5068 | 60 |
Goal "s |= [] F .--> [] [] F"; |
4559 | 61 |
by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def,tsuffix_def])1); |
5132 | 62 |
by Auto_tac; |
63 |
by (dtac suffix_trans 1); |
|
64 |
by (assume_tac 1); |
|
4559 | 65 |
by (eres_inst_tac [("x","s2a")] allE 1); |
5132 | 66 |
by Auto_tac; |
4559 | 67 |
qed"transT"; |
68 |
||
69 |
||
5068 | 70 |
Goal "s |= [] (F .--> G) .--> [] F .--> [] G"; |
4559 | 71 |
by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def])1); |
72 |
qed"normalT"; |
|
73 |
||
74 |
||
75 |
section "TLA Rules by Lamport"; |
|
76 |
||
77 |
(* ---------------------------------------------------------------- *) |
|
78 |
(* TLA Rules by Lamport *) |
|
79 |
(* ---------------------------------------------------------------- *) |
|
80 |
||
6161 | 81 |
Goal "validT P ==> validT ([] P)"; |
4559 | 82 |
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Box_def,tsuffix_def])1); |
83 |
qed"STL1a"; |
|
84 |
||
6161 | 85 |
Goal "valid P ==> validT (Init P)"; |
4559 | 86 |
by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,Init_def])1); |
87 |
qed"STL1b"; |
|
88 |
||
6161 | 89 |
Goal "valid P ==> validT ([] (Init P))"; |
5132 | 90 |
by (rtac STL1a 1); |
91 |
by (etac STL1b 1); |
|
4559 | 92 |
qed"STL1"; |
93 |
||
94 |
(* Note that unlift and HD is not at all used !!! *) |
|
6161 | 95 |
Goal "valid (P .--> Q) ==> validT ([] (Init P) .--> [] (Init Q))"; |
4559 | 96 |
by (asm_full_simp_tac (simpset() addsimps [valid_def,validT_def,satisfies_def,IMPLIES_def,Box_def,Init_def])1); |
97 |
qed"STL4"; |
|
98 |
||
99 |
||
100 |
section "LTL Axioms by Manna/Pnueli"; |
|
101 |
||
102 |
(* ---------------------------------------------------------------- *) |
|
103 |
(* LTL Axioms by Manna/Pnueli *) |
|
104 |
(* ---------------------------------------------------------------- *) |
|
105 |
||
106 |
||
5068 | 107 |
Goalw [tsuffix_def,suffix_def] |
10835 | 108 |
"s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s"; |
5132 | 109 |
by Auto_tac; |
4559 | 110 |
by (Seq_case_simp_tac "s" 1); |
111 |
by (res_inst_tac [("x","a>>s1")] exI 1); |
|
5132 | 112 |
by Auto_tac; |
4559 | 113 |
qed_spec_mp"tsuffix_TL"; |
114 |
||
115 |
val tsuffix_TL2 = conjI RS tsuffix_TL; |
|
116 |
||
4833 | 117 |
Delsplits[split_if]; |
5068 | 118 |
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def] |
4559 | 119 |
"s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))"; |
5132 | 120 |
by Auto_tac; |
4559 | 121 |
(* []F .--> F *) |
122 |
by (eres_inst_tac [("x","s")] allE 1); |
|
123 |
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1); |
|
124 |
(* []F .--> Next [] F *) |
|
4833 | 125 |
by (asm_full_simp_tac (simpset() addsplits [split_if]) 1); |
5132 | 126 |
by Auto_tac; |
127 |
by (dtac tsuffix_TL2 1); |
|
4559 | 128 |
by (REPEAT (atac 1)); |
5132 | 129 |
by Auto_tac; |
4559 | 130 |
qed"LTL1"; |
4833 | 131 |
Addsplits[split_if]; |
4559 | 132 |
|
133 |
||
5068 | 134 |
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def] |
4559 | 135 |
"s |= .~ (Next F) .--> (Next (.~ F))"; |
4833 | 136 |
by (Asm_full_simp_tac 1); |
4559 | 137 |
qed"LTL2a"; |
138 |
||
5068 | 139 |
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def] |
4559 | 140 |
"s |= (Next (.~ F)) .--> (.~ (Next F))"; |
4833 | 141 |
by (Asm_full_simp_tac 1); |
4559 | 142 |
qed"LTL2b"; |
143 |
||
5068 | 144 |
Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def] |
4559 | 145 |
"ex |= (Next (F .--> G)) .--> (Next F) .--> (Next G)"; |
4833 | 146 |
by (Asm_full_simp_tac 1); |
4559 | 147 |
qed"LTL3"; |
148 |
||
5068 | 149 |
Goalw [Next_def,satisfies_def,Box_def,NOT_def,IMPLIES_def] |
4559 | 150 |
"s |= [] (F .--> Next F) .--> F .--> []F"; |
4833 | 151 |
by (Asm_full_simp_tac 1); |
5132 | 152 |
by Auto_tac; |
4559 | 153 |
|
154 |
by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1); |
|
5132 | 155 |
by Auto_tac; |
4559 | 156 |
|
157 |
||
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
158 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
159 |
|
6161 | 160 |
Goal "[| validT (P .--> Q); validT P |] ==> validT Q"; |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
161 |
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,IMPLIES_def])1); |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
162 |
qed"ModusPonens"; |
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
163 |
|
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
164 |
(* works only if validT is defined without restriction to s~=UU, s~=nil *) |
6161 | 165 |
Goal "validT P ==> validT (Next P)"; |
4577
674b0b354feb
added thms wrt weakening and strengthening in Abstraction;
mueller
parents:
4559
diff
changeset
|
166 |
by (asm_full_simp_tac (simpset() addsimps [validT_def,satisfies_def,Next_def])1); |
4681 | 167 |
(* qed"NextTauto"; *) |