src/HOL/HOLCF/IOA/meta_theory/TL.thy
author wenzelm
Wed, 30 Dec 2015 22:09:44 +0100
changeset 62004 8c6226d88ced
parent 62002 f1599e98c4d0
child 62005 68db98c2cd97
permissions -rw-r--r--
more symbols;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
42151
4da4fc77664b tuned headers;
wenzelm
parents: 41476
diff changeset
     1
(*  Title:      HOL/HOLCF/IOA/meta_theory/TL.thy
40945
b8703f63bfb2 recoded latin1 as utf8;
wenzelm
parents: 40774
diff changeset
     2
    Author:     Olaf Müller
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     3
*)
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
     4
62002
f1599e98c4d0 isabelle update_cartouches -c -t;
wenzelm
parents: 62001
diff changeset
     5
section \<open>A General Temporal Logic\<close>
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
     6
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     7
theory TL
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     8
imports Pred Sequence
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     9
begin
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    10
36452
d37c6eed8117 renamed command 'defaultsort' to 'default_sort';
wenzelm
parents: 35174
diff changeset
    11
default_sort type
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    12
41476
0fa9629aa399 types -> type_synonym
huffman
parents: 40945
diff changeset
    13
type_synonym
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    14
  'a temporal = "'a Seq predicate"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    15
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    16
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    17
consts
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    18
suffix     :: "'a Seq => 'a Seq => bool"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    19
tsuffix    :: "'a Seq => 'a Seq => bool"
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
validT     :: "'a Seq predicate => bool"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    22
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    23
unlift     ::  "'a lift => 'a"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    24
62004
8c6226d88ced more symbols;
wenzelm
parents: 62002
diff changeset
    25
Init       :: "'a predicate => 'a temporal"  ("\<langle>_\<rangle>" [0] 1000)
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    26
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    27
Box        :: "'a temporal => 'a temporal"   ("\<box>(_)" [80] 80)
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    28
Diamond    :: "'a temporal => 'a temporal"   ("\<diamond>(_)" [80] 80)
61999
89291b5d0ede more symbols;
wenzelm
parents: 58880
diff changeset
    29
Next       :: "'a temporal => 'a temporal"
89291b5d0ede more symbols;
wenzelm
parents: 58880
diff changeset
    30
Leadsto    :: "'a temporal => 'a temporal => 'a temporal"  (infixr "\<leadsto>" 22)
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    31
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    32
defs
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    33
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    34
unlift_def:
28524
644b62cf678f arbitrary is undefined
haftmann
parents: 27208
diff changeset
    35
  "unlift x == (case x of Def y   => y)"
4559
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
(* this means that for nil and UU the effect is unpredictable *)
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    38
Init_def:
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    39
  "Init P s ==  (P (unlift (HD$s)))"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    40
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    41
suffix_def:
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    42
  "suffix s2 s == ? s1. (Finite s1  & s = s1 @@ s2)"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    43
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    44
tsuffix_def:
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    45
  "tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s"
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    46
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    47
Box_def:
61999
89291b5d0ede more symbols;
wenzelm
parents: 58880
diff changeset
    48
  "(\<box>P) s == ! s2. tsuffix s2 s --> P s2"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    49
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    50
Next_def:
10835
nipkow
parents: 5976
diff changeset
    51
  "(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    52
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    53
Diamond_def:
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    54
  "\<diamond>P == \<^bold>\<not> (\<box>(\<^bold>\<not> P))"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    55
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    56
Leadsto_def:
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    57
   "P \<leadsto> Q == (\<box>(P \<^bold>\<longrightarrow> (\<diamond>Q)))"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    58
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    59
validT_def:
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    60
  "validT P == ! s. s~=UU & s~=nil --> (s \<Turnstile> P)"
4559
8e604d885b54 added files containing temproal logic and abstraction;
mueller
parents:
diff changeset
    61
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    62
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    63
lemma simple: "\<box>\<diamond>(\<^bold>\<not> P) = (\<^bold>\<not> \<diamond>\<box>P)"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    64
apply (rule ext)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    65
apply (simp add: Diamond_def NOT_def Box_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    66
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    67
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    68
lemma Boxnil: "nil \<Turnstile> \<box>P"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    69
apply (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    70
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    71
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    72
lemma Diamondnil: "~(nil \<Turnstile> \<diamond>P)"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    73
apply (simp add: Diamond_def satisfies_def NOT_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    74
apply (cut_tac Boxnil)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    75
apply (simp add: satisfies_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    76
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    77
61999
89291b5d0ede more symbols;
wenzelm
parents: 58880
diff changeset
    78
lemma Diamond_def2: "(\<diamond>F) s = (? s2. tsuffix s2 s & F s2)"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    79
apply (simp add: Diamond_def NOT_def Box_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    80
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    81
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    82
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    83
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    84
subsection "TLA Axiomatization by Merz"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    85
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    86
lemma suffix_refl: "suffix s s"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    87
apply (simp add: suffix_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    88
apply (rule_tac x = "nil" in exI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    89
apply auto
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    90
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    91
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
    92
lemma reflT: "s~=UU & s~=nil --> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> F)"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    93
apply (simp add: satisfies_def IMPLIES_def Box_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    94
apply (rule impI)+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    95
apply (erule_tac x = "s" in allE)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    96
apply (simp add: tsuffix_def suffix_refl)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    97
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    98
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
    99
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   100
lemma suffix_trans: "[| suffix y x ; suffix z y |]  ==> suffix z x"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   101
apply (simp add: suffix_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   102
apply auto
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   103
apply (rule_tac x = "s1 @@ s1a" in exI)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   104
apply auto
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   105
apply (simp (no_asm) add: Conc_assoc)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   106
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   107
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
   108
lemma transT: "s \<Turnstile> \<box>F \<^bold>\<longrightarrow> \<box>\<box>F"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   109
apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def tsuffix_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   110
apply auto
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   111
apply (drule suffix_trans)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   112
apply assumption
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   113
apply (erule_tac x = "s2a" in allE)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   114
apply auto
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   115
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   116
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   117
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
   118
lemma normalT: "s \<Turnstile> \<box>(F \<^bold>\<longrightarrow> G) \<^bold>\<longrightarrow> \<box>F \<^bold>\<longrightarrow> \<box>G"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   119
apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   120
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   121
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   122
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   123
subsection "TLA Rules by Lamport"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   124
61999
89291b5d0ede more symbols;
wenzelm
parents: 58880
diff changeset
   125
lemma STL1a: "validT P ==> validT (\<box>P)"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   126
apply (simp add: validT_def satisfies_def Box_def tsuffix_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
lemma STL1b: "valid P ==> validT (Init P)"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   130
apply (simp add: valid_def validT_def satisfies_def Init_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   131
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   132
61999
89291b5d0ede more symbols;
wenzelm
parents: 58880
diff changeset
   133
lemma STL1: "valid P ==> validT (\<box>(Init P))"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   134
apply (rule STL1a)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   135
apply (erule STL1b)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   136
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   137
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   138
(* Note that unlift and HD is not at all used !!! *)
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
   139
lemma STL4: "valid (P \<^bold>\<longrightarrow> Q)  ==> validT (\<box>(Init P) \<^bold>\<longrightarrow> \<box>(Init Q))"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   140
apply (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_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
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   144
subsection "LTL Axioms by Manna/Pnueli"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   145
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   146
lemma tsuffix_TL [rule_format (no_asm)]: 
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   147
"s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s"
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   148
apply (unfold tsuffix_def suffix_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   149
apply auto
62002
f1599e98c4d0 isabelle update_cartouches -c -t;
wenzelm
parents: 62001
diff changeset
   150
apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
62001
1f2788fb0b8b more symbols;
wenzelm
parents: 62000
diff changeset
   151
apply (rule_tac x = "a\<leadsto>s1" in exI)
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   152
apply auto
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   153
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   154
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   155
lemmas tsuffix_TL2 = conjI [THEN tsuffix_TL]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   156
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   157
declare split_if [split del]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   158
lemma LTL1: 
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
   159
   "s~=UU & s~=nil --> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> (F \<^bold>\<and> (Next (\<box>F))))"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   160
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   161
apply auto
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
   162
(* \<box>F \<^bold>\<longrightarrow> F *)
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   163
apply (erule_tac x = "s" in allE)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   164
apply (simp add: tsuffix_def suffix_refl)
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
   165
(* \<box>F \<^bold>\<longrightarrow> Next \<box>F *)
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   166
apply (simp split add: split_if)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   167
apply auto
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   168
apply (drule tsuffix_TL2)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   169
apply assumption+
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   170
apply auto
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   171
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   172
declare split_if [split]
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   173
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   174
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   175
lemma LTL2a: 
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
   176
    "s \<Turnstile> \<^bold>\<not> (Next F) \<^bold>\<longrightarrow> (Next (\<^bold>\<not> F))"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   177
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   178
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   179
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   180
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   181
lemma LTL2b: 
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
   182
    "s \<Turnstile> (Next (\<^bold>\<not> F)) \<^bold>\<longrightarrow> (\<^bold>\<not> (Next F))"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   183
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   184
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   185
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   186
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   187
lemma LTL3: 
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
   188
"ex \<Turnstile> (Next (F \<^bold>\<longrightarrow> G)) \<^bold>\<longrightarrow> (Next F) \<^bold>\<longrightarrow> (Next G)"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   189
apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   190
apply simp
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   191
done
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   192
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   193
62000
8cba509ace9c more symbols;
wenzelm
parents: 61999
diff changeset
   194
lemma ModusPonens: "[| validT (P \<^bold>\<longrightarrow> Q); validT P |] ==> validT Q"
19741
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   195
apply (simp add: validT_def satisfies_def IMPLIES_def)
f65265d71426 removed legacy ML scripts;
wenzelm
parents: 17233
diff changeset
   196
done
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   197
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
   198
end