src/HOLCF/IOA/meta_theory/TLS.thy
author wenzelm
Wed, 19 Mar 2008 22:47:35 +0100
changeset 26339 7825c83c9eff
parent 19741 f65265d71426
child 26359 6d437bde2f1d
permissions -rw-r--r--
eliminated change_claset/simpset;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
     1
(*  Title:      HOLCF/IOA/meta_theory/TLS.thy
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
     2
    ID:         $Id$
12218
wenzelm
parents: 10835
diff changeset
     3
    Author:     Olaf Müller
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     4
*)
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
     5
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     6
header {* Temporal Logic of Steps -- tailored for I/O automata *}
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
     7
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     8
theory TLS
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     9
imports IOA TL
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    10
begin
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    11
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    12
defaultsort type
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    13
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    14
types
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    15
  ('a, 's) ioa_temp  = "('a option,'s)transition temporal"
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    16
  ('a, 's) step_pred = "('a option,'s)transition predicate"
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    17
  's state_pred      = "'s predicate"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    18
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    19
consts
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    20
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    21
option_lift :: "('a => 'b) => 'b => ('a option => 'b)"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    22
plift       :: "('a => bool) => ('a option => bool)"
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    23
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    24
temp_sat   :: "('a,'s)execution => ('a,'s)ioa_temp => bool"    (infixr "|==" 22)
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    25
xt1        :: "'s predicate => ('a,'s)step_pred"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    26
xt2        :: "'a option predicate => ('a,'s)step_pred"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    27
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    28
validTE    :: "('a,'s)ioa_temp => bool"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    29
validIOA   :: "('a,'s)ioa => ('a,'s)ioa_temp => bool"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    30
5677
4feffde494cf another little bug ;-) and minor changes in TLS.*;
mueller
parents: 4577
diff changeset
    31
mkfin      :: "'a Seq => 'a Seq"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    32
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    33
ex2seq     :: "('a,'s)execution => ('a option,'s)transition Seq"
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    34
ex2seqC    :: "('a,'s)pairs -> ('s => ('a option,'s)transition Seq)"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    35
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    36
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    37
defs
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    38
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    39
mkfin_def:
5677
4feffde494cf another little bug ;-) and minor changes in TLS.*;
mueller
parents: 4577
diff changeset
    40
  "mkfin s == if Partial s then @t. Finite t & s = t @@ UU
4feffde494cf another little bug ;-) and minor changes in TLS.*;
mueller
parents: 4577
diff changeset
    41
                           else s"
4feffde494cf another little bug ;-) and minor changes in TLS.*;
mueller
parents: 4577
diff changeset
    42
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    43
option_lift_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    44
  "option_lift f s y == case y of None => s | Some x => (f x)"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    45
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    46
(* plift is used to determine that None action is always false in
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    47
   transition predicates *)
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    48
plift_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    49
  "plift P == option_lift P False"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    50
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    51
temp_sat_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    52
  "ex |== P == ((ex2seq ex) |= P)"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    53
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    54
xt1_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    55
  "xt1 P tr == P (fst tr)"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    56
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    57
xt2_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    58
  "xt2 P tr == P (fst (snd tr))"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    59
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    60
ex2seq_def:
10835
nipkow
parents: 5976
diff changeset
    61
  "ex2seq ex == ((ex2seqC $(mkfin (snd ex))) (fst ex))"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    62
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    63
ex2seqC_def:
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    64
  "ex2seqC == (fix$(LAM h ex. (%s. case ex of
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    65
      nil =>  (s,None,s)>>nil
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    66
    | x##xs => (flift1 (%pr.
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    67
                (s,Some (fst pr), snd pr)>> (h$xs) (snd pr))
10835
nipkow
parents: 5976
diff changeset
    68
                $x)
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    69
      )))"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    70
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    71
validTE_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    72
  "validTE P == ! ex. (ex |== P)"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    73
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    74
validIOA_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    75
  "validIOA A P == ! ex : executions A . (ex |== P)"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    76
5976
44290b71a85f tuning to assimiliate it with PhD;
mueller
parents: 5677
diff changeset
    77
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    78
axioms
5976
44290b71a85f tuning to assimiliate it with PhD;
mueller
parents: 5677
diff changeset
    79
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    80
mkfin_UU:
5677
4feffde494cf another little bug ;-) and minor changes in TLS.*;
mueller
parents: 4577
diff changeset
    81
  "mkfin UU = nil"
4feffde494cf another little bug ;-) and minor changes in TLS.*;
mueller
parents: 4577
diff changeset
    82
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    83
mkfin_nil:
5677
4feffde494cf another little bug ;-) and minor changes in TLS.*;
mueller
parents: 4577
diff changeset
    84
  "mkfin nil =nil"
4feffde494cf another little bug ;-) and minor changes in TLS.*;
mueller
parents: 4577
diff changeset
    85
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    86
mkfin_cons:
5677
4feffde494cf another little bug ;-) and minor changes in TLS.*;
mueller
parents: 4577
diff changeset
    87
  "(mkfin (a>>s)) = (a>>(mkfin s))"
4feffde494cf another little bug ;-) and minor changes in TLS.*;
mueller
parents: 4577
diff changeset
    88
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    89
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    90
lemmas [simp del] = ex_simps all_simps split_paired_Ex
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    91
declare Let_def [simp]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    92
26339
7825c83c9eff eliminated change_claset/simpset;
wenzelm
parents: 19741
diff changeset
    93
declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *}
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    94
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    95
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    96
subsection {* ex2seqC *}
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    97
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    98
lemma ex2seqC_unfold: "ex2seqC  = (LAM ex. (%s. case ex of  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    99
       nil =>  (s,None,s)>>nil    
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   100
     | x##xs => (flift1 (%pr.  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   101
                 (s,Some (fst pr), snd pr)>> (ex2seqC$xs) (snd pr))   
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   102
                 $x)   
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   103
       ))"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   104
apply (rule trans)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   105
apply (rule fix_eq2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   106
apply (rule ex2seqC_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   107
apply (rule beta_cfun)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   108
apply (simp add: flift1_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   109
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   110
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   111
lemma ex2seqC_UU: "(ex2seqC $UU) s=UU"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   112
apply (subst ex2seqC_unfold)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   113
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   114
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   115
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   116
lemma ex2seqC_nil: "(ex2seqC $nil) s = (s,None,s)>>nil"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   117
apply (subst ex2seqC_unfold)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   118
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   119
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   120
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   121
lemma ex2seqC_cons: "(ex2seqC $((a,t)>>xs)) s =  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   122
           (s,Some a,t)>> ((ex2seqC$xs) t)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   123
apply (rule trans)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   124
apply (subst ex2seqC_unfold)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   125
apply (simp add: Consq_def flift1_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   126
apply (simp add: Consq_def flift1_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   127
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   128
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   129
declare ex2seqC_UU [simp] ex2seqC_nil [simp] ex2seqC_cons [simp]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   130
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   131
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   132
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   133
declare mkfin_UU [simp] mkfin_nil [simp] mkfin_cons [simp]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   134
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   135
lemma ex2seq_UU: "ex2seq (s, UU) = (s,None,s)>>nil"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   136
apply (simp add: ex2seq_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   137
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   138
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   139
lemma ex2seq_nil: "ex2seq (s, nil) = (s,None,s)>>nil"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   140
apply (simp add: ex2seq_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   141
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   142
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   143
lemma ex2seq_cons: "ex2seq (s, (a,t)>>ex) = (s,Some a,t) >> ex2seq (t, ex)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   144
apply (simp add: ex2seq_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   145
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   146
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   147
declare ex2seqC_UU [simp del] ex2seqC_nil [simp del] ex2seqC_cons [simp del]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   148
declare ex2seq_UU [simp] ex2seq_nil [simp] ex2seq_cons [simp]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   149
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   150
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   151
lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   152
apply (tactic {* pair_tac "exec" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   153
apply (tactic {* Seq_case_simp_tac "y" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   154
apply (tactic {* pair_tac "a" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   155
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   156
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   157
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   158
subsection {* Interface TL -- TLS *}
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   159
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   160
(* uses the fact that in executions states overlap, which is lost in 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   161
   after the translation via ex2seq !! *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   162
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   163
lemma TL_TLS: 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   164
 "[| ! s a t. (P s) & s-a--A-> t --> (Q t) |] 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   165
   ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t)  
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   166
              .--> (Next (Init (%(s,a,t).Q s))))"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   167
apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   168
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   169
apply (tactic "clarify_tac set_cs 1")
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   170
apply (simp split add: split_if)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   171
(* TL = UU *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   172
apply (rule conjI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   173
apply (tactic {* pair_tac "ex" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   174
apply (tactic {* Seq_case_simp_tac "y" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   175
apply (tactic {* pair_tac "a" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   176
apply (tactic {* Seq_case_simp_tac "s" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   177
apply (tactic {* pair_tac "a" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   178
(* TL = nil *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   179
apply (rule conjI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   180
apply (tactic {* pair_tac "ex" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   181
apply (tactic {* Seq_case_tac "y" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   182
apply (simp add: unlift_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   183
apply fast
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   184
apply (simp add: unlift_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   185
apply fast
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   186
apply (simp add: unlift_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   187
apply (tactic {* pair_tac "a" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   188
apply (tactic {* Seq_case_simp_tac "s" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   189
apply (tactic {* pair_tac "a" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   190
(* TL =cons *)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   191
apply (simp add: unlift_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   192
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   193
apply (tactic {* pair_tac "ex" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   194
apply (tactic {* Seq_case_simp_tac "y" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   195
apply (tactic {* pair_tac "a" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   196
apply (tactic {* Seq_case_simp_tac "s" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   197
apply blast
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   198
apply fastsimp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   199
apply (tactic {* pair_tac "a" 1 *})
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   200
 apply fastsimp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   201
done
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
   202
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
   203
end