author | mueller |
Thu, 26 Nov 1998 16:37:56 +0100 | |
changeset 5976 | 44290b71a85f |
parent 5677 | 4feffde494cf |
child 6161 | bc2a76ce1ea3 |
permissions | -rw-r--r-- |
4559 | 1 |
(* Title: HOLCF/IOA/meta_theory/TLS.ML |
2 |
ID: $Id$ |
|
3 |
Author: Olaf M"uller |
|
4 |
Copyright 1997 TU Muenchen |
|
5 |
||
6 |
Temporal Logic of Steps -- tailored for I/O automata |
|
5976 | 7 |
*) |
4559 | 8 |
|
4815
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4577
diff
changeset
|
9 |
(* global changes to simpset() and claset(), repeated from Traces.ML *) |
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4577
diff
changeset
|
10 |
Delsimps (ex_simps @ all_simps); |
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4577
diff
changeset
|
11 |
Delsimps [split_paired_Ex]; |
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4577
diff
changeset
|
12 |
Addsimps [Let_def]; |
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4577
diff
changeset
|
13 |
claset_ref() := claset() delSWrapper "split_all_tac"; |
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4577
diff
changeset
|
14 |
|
4559 | 15 |
|
16 |
(* ---------------------------------------------------------------- *) |
|
17 |
(* ex2seqC *) |
|
18 |
(* ---------------------------------------------------------------- *) |
|
19 |
||
5068 | 20 |
Goal "ex2seqC = (LAM ex. (%s. case ex of \ |
4559 | 21 |
\ nil => (s,None,s)>>nil \ |
22 |
\ | x##xs => (flift1 (%pr. \ |
|
23 |
\ (s,Some (fst pr), snd pr)>> (ex2seqC`xs) (snd pr)) \ |
|
24 |
\ `x) \ |
|
25 |
\ ))"; |
|
26 |
by (rtac trans 1); |
|
27 |
by (rtac fix_eq2 1); |
|
28 |
by (rtac ex2seqC_def 1); |
|
29 |
by (rtac beta_cfun 1); |
|
30 |
by (simp_tac (simpset() addsimps [flift1_def]) 1); |
|
31 |
qed"ex2seqC_unfold"; |
|
32 |
||
5068 | 33 |
Goal "(ex2seqC `UU) s=UU"; |
4559 | 34 |
by (stac ex2seqC_unfold 1); |
35 |
by (Simp_tac 1); |
|
36 |
qed"ex2seqC_UU"; |
|
37 |
||
5068 | 38 |
Goal "(ex2seqC `nil) s = (s,None,s)>>nil"; |
4559 | 39 |
by (stac ex2seqC_unfold 1); |
40 |
by (Simp_tac 1); |
|
41 |
qed"ex2seqC_nil"; |
|
42 |
||
5068 | 43 |
Goal "(ex2seqC `((a,t)>>xs)) s = \ |
4559 | 44 |
\ (s,Some a,t)>> ((ex2seqC`xs) t)"; |
45 |
by (rtac trans 1); |
|
46 |
by (stac ex2seqC_unfold 1); |
|
47 |
by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1); |
|
48 |
by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1); |
|
49 |
qed"ex2seqC_cons"; |
|
50 |
||
51 |
Addsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons]; |
|
52 |
||
53 |
||
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
54 |
|
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
55 |
Addsimps [mkfin_UU,mkfin_nil,mkfin_cons]; |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
56 |
|
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
57 |
Goal "ex2seq (s, UU) = (s,None,s)>>nil"; |
4559 | 58 |
by (simp_tac (simpset() addsimps [ex2seq_def]) 1); |
59 |
qed"ex2seq_UU"; |
|
60 |
||
5068 | 61 |
Goal "ex2seq (s, nil) = (s,None,s)>>nil"; |
4559 | 62 |
by (simp_tac (simpset() addsimps [ex2seq_def]) 1); |
63 |
qed"ex2seq_nil"; |
|
64 |
||
5068 | 65 |
Goal "ex2seq (s, (a,t)>>ex) = (s,Some a,t) >> ex2seq (t, ex)"; |
4559 | 66 |
by (simp_tac (simpset() addsimps [ex2seq_def]) 1); |
67 |
qed"ex2seq_cons"; |
|
68 |
||
69 |
Delsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons]; |
|
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
70 |
Addsimps [ex2seq_UU,ex2seq_nil, ex2seq_cons]; |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
71 |
|
4559 | 72 |
|
5068 | 73 |
Goal "ex2seq exec ~= UU & ex2seq exec ~= nil"; |
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
74 |
by (pair_tac "exec" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
75 |
by (Seq_case_simp_tac "y" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
76 |
by (pair_tac "a" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
77 |
qed"ex2seq_nUUnnil"; |
4559 | 78 |
|
79 |
||
80 |
(* ----------------------------------------------------------- *) |
|
81 |
(* Interface TL -- TLS *) |
|
82 |
(* ---------------------------------------------------------- *) |
|
83 |
||
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
84 |
|
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
85 |
(* uses the fact that in executions states overlap, which is lost in |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
86 |
after the translation via ex2seq !! *) |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
87 |
|
5068 | 88 |
Goalw [Init_def,Next_def,temp_sat_def,satisfies_def,IMPLIES_def,AND_def] |
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
89 |
"!! A. [| ! s a t. (P s) & s-a--A-> t --> (Q t) |]\ |
4559 | 90 |
\ ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t) \ |
91 |
\ .--> (Next (Init (%(s,a,t).Q s))))"; |
|
92 |
||
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
93 |
by (clarify_tac set_cs 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
94 |
by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
95 |
(* TL = UU *) |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
96 |
br conjI 1; |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
97 |
by (pair_tac "ex" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
98 |
by (Seq_case_simp_tac "y" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
99 |
by (pair_tac "a" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
100 |
by (Seq_case_simp_tac "s" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
101 |
by (pair_tac "a" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
102 |
(* TL = nil *) |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
103 |
br conjI 1; |
4559 | 104 |
by (pair_tac "ex" 1); |
105 |
by (Seq_case_simp_tac "y" 1); |
|
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
106 |
by (asm_full_simp_tac (simpset() addsimps [unlift_def])1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
107 |
by (Fast_tac 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
108 |
by (asm_full_simp_tac (simpset() addsimps [unlift_def])1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
109 |
by (Fast_tac 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
110 |
by (asm_full_simp_tac (simpset() addsimps [unlift_def])1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
111 |
by (pair_tac "a" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
112 |
by (Seq_case_simp_tac "s" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
113 |
by (pair_tac "a" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
114 |
(* TL =cons *) |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
115 |
by (asm_full_simp_tac (simpset() addsimps [unlift_def])1); |
4559 | 116 |
|
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
117 |
by (pair_tac "ex" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
118 |
by (Seq_case_simp_tac "y" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
119 |
by (pair_tac "a" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
120 |
by (Seq_case_simp_tac "s" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
121 |
by (Fast_tac 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
122 |
by (Fast_tac 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
123 |
by (pair_tac "a" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
124 |
by (Fast_tac 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
125 |
qed"TL_TLS"; |