author | wenzelm |
Mon, 17 Oct 2005 23:10:13 +0200 | |
changeset 17876 | b9c92f384109 |
parent 17233 | 41eee2e7b465 |
child 19360 | f47412f922ab |
permissions | -rw-r--r-- |
4559 | 1 |
(* Title: HOLCF/IOA/meta_theory/TLS.ML |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller |
5976 | 4 |
*) |
4559 | 5 |
|
4815
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4577
diff
changeset
|
6 |
(* 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
|
7 |
Delsimps (ex_simps @ all_simps); |
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4577
diff
changeset
|
8 |
Delsimps [split_paired_Ex]; |
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4577
diff
changeset
|
9 |
Addsimps [Let_def]; |
17876 | 10 |
change_claset (fn cs => cs delSWrapper "split_all_tac"); |
4815
b8a32ef742d9
removed split_all_tac from claset() globally within IOA
oheimb
parents:
4577
diff
changeset
|
11 |
|
4559 | 12 |
|
13 |
(* ---------------------------------------------------------------- *) |
|
14 |
(* ex2seqC *) |
|
15 |
(* ---------------------------------------------------------------- *) |
|
16 |
||
5068 | 17 |
Goal "ex2seqC = (LAM ex. (%s. case ex of \ |
4559 | 18 |
\ nil => (s,None,s)>>nil \ |
19 |
\ | x##xs => (flift1 (%pr. \ |
|
10835 | 20 |
\ (s,Some (fst pr), snd pr)>> (ex2seqC$xs) (snd pr)) \ |
21 |
\ $x) \ |
|
4559 | 22 |
\ ))"; |
23 |
by (rtac trans 1); |
|
24 |
by (rtac fix_eq2 1); |
|
25 |
by (rtac ex2seqC_def 1); |
|
26 |
by (rtac beta_cfun 1); |
|
27 |
by (simp_tac (simpset() addsimps [flift1_def]) 1); |
|
28 |
qed"ex2seqC_unfold"; |
|
29 |
||
10835 | 30 |
Goal "(ex2seqC $UU) s=UU"; |
4559 | 31 |
by (stac ex2seqC_unfold 1); |
32 |
by (Simp_tac 1); |
|
33 |
qed"ex2seqC_UU"; |
|
34 |
||
10835 | 35 |
Goal "(ex2seqC $nil) s = (s,None,s)>>nil"; |
4559 | 36 |
by (stac ex2seqC_unfold 1); |
37 |
by (Simp_tac 1); |
|
38 |
qed"ex2seqC_nil"; |
|
39 |
||
10835 | 40 |
Goal "(ex2seqC $((a,t)>>xs)) s = \ |
41 |
\ (s,Some a,t)>> ((ex2seqC$xs) t)"; |
|
4559 | 42 |
by (rtac trans 1); |
43 |
by (stac ex2seqC_unfold 1); |
|
7229
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
44 |
by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1); |
6773ba0c36d5
renamed Cons to Consq in order to avoid clash with List.Cons;
wenzelm
parents:
6161
diff
changeset
|
45 |
by (asm_full_simp_tac (simpset() addsimps [Consq_def,flift1_def]) 1); |
4559 | 46 |
qed"ex2seqC_cons"; |
47 |
||
48 |
Addsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons]; |
|
49 |
||
50 |
||
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
51 |
|
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
52 |
Addsimps [mkfin_UU,mkfin_nil,mkfin_cons]; |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
53 |
|
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
54 |
Goal "ex2seq (s, UU) = (s,None,s)>>nil"; |
4559 | 55 |
by (simp_tac (simpset() addsimps [ex2seq_def]) 1); |
56 |
qed"ex2seq_UU"; |
|
57 |
||
5068 | 58 |
Goal "ex2seq (s, nil) = (s,None,s)>>nil"; |
4559 | 59 |
by (simp_tac (simpset() addsimps [ex2seq_def]) 1); |
60 |
qed"ex2seq_nil"; |
|
61 |
||
5068 | 62 |
Goal "ex2seq (s, (a,t)>>ex) = (s,Some a,t) >> ex2seq (t, ex)"; |
4559 | 63 |
by (simp_tac (simpset() addsimps [ex2seq_def]) 1); |
64 |
qed"ex2seq_cons"; |
|
65 |
||
66 |
Delsimps [ex2seqC_UU,ex2seqC_nil,ex2seqC_cons]; |
|
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
67 |
Addsimps [ex2seq_UU,ex2seq_nil, ex2seq_cons]; |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
68 |
|
4559 | 69 |
|
5068 | 70 |
Goal "ex2seq exec ~= UU & ex2seq exec ~= nil"; |
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
71 |
by (pair_tac "exec" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
72 |
by (Seq_case_simp_tac "y" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
73 |
by (pair_tac "a" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
74 |
qed"ex2seq_nUUnnil"; |
4559 | 75 |
|
76 |
||
77 |
(* ----------------------------------------------------------- *) |
|
78 |
(* Interface TL -- TLS *) |
|
79 |
(* ---------------------------------------------------------- *) |
|
80 |
||
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
81 |
|
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
82 |
(* 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
|
83 |
after the translation via ex2seq !! *) |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
84 |
|
5068 | 85 |
Goalw [Init_def,Next_def,temp_sat_def,satisfies_def,IMPLIES_def,AND_def] |
6161 | 86 |
"[| ! s a t. (P s) & s-a--A-> t --> (Q t) |]\ |
4559 | 87 |
\ ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t) \ |
88 |
\ .--> (Next (Init (%(s,a,t).Q s))))"; |
|
89 |
||
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
90 |
by (clarify_tac set_cs 1); |
9385 | 91 |
by (asm_full_simp_tac (simpset() addsplits [split_if]) 1); |
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
92 |
(* TL = UU *) |
6161 | 93 |
by (rtac conjI 1); |
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
94 |
by (pair_tac "ex" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
95 |
by (Seq_case_simp_tac "y" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
96 |
by (pair_tac "a" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
97 |
by (Seq_case_simp_tac "s" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
98 |
by (pair_tac "a" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
99 |
(* TL = nil *) |
6161 | 100 |
by (rtac conjI 1); |
4559 | 101 |
by (pair_tac "ex" 1); |
102 |
by (Seq_case_simp_tac "y" 1); |
|
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
103 |
by (asm_full_simp_tac (simpset() addsimps [unlift_def])1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
104 |
by (Fast_tac 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
105 |
by (asm_full_simp_tac (simpset() addsimps [unlift_def])1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
106 |
by (Fast_tac 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
107 |
by (asm_full_simp_tac (simpset() addsimps [unlift_def])1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
108 |
by (pair_tac "a" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
109 |
by (Seq_case_simp_tac "s" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
110 |
by (pair_tac "a" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
111 |
(* TL =cons *) |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
112 |
by (asm_full_simp_tac (simpset() addsimps [unlift_def])1); |
4559 | 113 |
|
5677
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
114 |
by (pair_tac "ex" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
115 |
by (Seq_case_simp_tac "y" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
116 |
by (pair_tac "a" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
117 |
by (Seq_case_simp_tac "s" 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
118 |
by (Fast_tac 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
119 |
by (Fast_tac 1); |
4feffde494cf
another little bug ;-) and minor changes in TLS.*;
mueller
parents:
5068
diff
changeset
|
120 |
by (pair_tac "a" 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 |
qed"TL_TLS"; |