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