Mercurial Mercurial > hg > lexing / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
thys/Re1.thy.rej
author Christian Urban <christian dot urban at kcl dot ac dot uk>
Mon, 06 Oct 2014 15:24:41 +0100
changeset 20 c11651bbebf5
parent 18 8c9349065477
permissions -rw-r--r--
some small changes
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
18
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
     1
 
--- thys/Re1.thy
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
     2
 
+++ thys/Re1.thy
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
     3
 
@@ -168,6 +168,33 @@
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
     4
 
 done
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
     5
 
 *)
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
     6
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
     7
 
+
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
     8
 
+
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
     9
 
+
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    10
 
+lemma POSIX_ALT2:
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    11
 
+  assumes "POSIX (Left v1) (ALT r1 r2)"
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    12
 
+  shows "POSIX v1 r1"
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    13
 
+using assms
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    14
 
+unfolding POSIX_def
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    15
 
+apply(auto)
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    16
 
+apply(drule_tac x="Left v'" in spec)
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    17
 
+apply(simp)
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    18
 
+apply(drule mp)
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    19
 
+apply(rule Prf.intros)
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    20
 
+apply(auto)
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    21
 
+apply(erule ValOrd.cases)
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    22
 
+apply(simp_all)
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    23
 
+done
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    24
 
+
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    25
 
+lemma POSIX2_ALT:
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    26
 
+  assumes "POSIX2 (Left v1) (ALT r1 r2)"
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    27
 
+  shows "POSIX2 v1 r1"
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    28
 
+using assms
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    29
 
+unfolding POSIX2_def
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    30
 
+apply(auto)
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    31
 
+
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    32
 
+done
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    33
 
+
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    34
 
 lemma POSIX_ALT:
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    35
 
   assumes "POSIX (Left v1) (ALT r1 r2)"
fahadausaf <fahad.ausaf@icloud.com>
parents:
diff changeset 
    36
 
   shows "POSIX v1 r1"
lexing