Mercurial Mercurial > repos > isabelle / 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.
src/HOL/SMT/Examples/cert/z3_mono_01.proof
author ballarin
Mon, 09 Nov 2009 21:33:22 +0100
changeset 33541 e716c6ad381b
parent 33010 39f73a59e855
permissions -rw-r--r--
Removed obsolete code.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33010
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     1
 
#2 := false
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     2
 
decl up_35 :: (-> int bool)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     3
 
#112 := 1::int
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     4
 
#113 := (up_35 1::int)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     5
 
#114 := (not #113)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     6
 
#297 := [asserted]: #114
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     7
 
#103 := (:var 0 int)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     8
 
#104 := (up_35 #103)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     9
 
#911 := (pattern #104)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    10
 
#912 := (forall (vars (?x12 int)) (:pat #911) #104)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    11
 
#294 := (forall (vars (?x12 int)) #104)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    12
 
#915 := (iff #294 #912)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    13
 
#913 := (iff #104 #104)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    14
 
#914 := [refl]: #913
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    15
 
#916 := [quant-intro #914]: #915
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    16
 
#320 := (~ #294 #294)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    17
 
#361 := (~ #104 #104)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    18
 
#362 := [refl]: #361
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    19
 
#321 := [nnf-pos #362]: #320
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    20
 
decl up_32 :: (-> T13 bool)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    21
 
decl uf_36 :: (-> int T13 T13)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    22
 
decl uf_37 :: T13
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    23
 
#105 := uf_37
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    24
 
#106 := (uf_36 #103 uf_37)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    25
 
#107 := (up_32 #106)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    26
 
#108 := (not #107)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    27
 
#109 := (or #107 #108)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    28
 
#110 := (and #104 #109)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    29
 
#111 := (forall (vars (?x12 int)) #110)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    30
 
#295 := (iff #111 #294)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    31
 
#292 := (iff #110 #104)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    32
 
#1 := true
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    33
 
#287 := (and #104 true)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    34
 
#290 := (iff #287 #104)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    35
 
#291 := [rewrite]: #290
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    36
 
#288 := (iff #110 #287)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    37
 
#284 := (iff #109 true)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    38
 
#286 := [rewrite]: #284
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    39
 
#289 := [monotonicity #286]: #288
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    40
 
#293 := [trans #289 #291]: #292
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    41
 
#296 := [quant-intro #293]: #295
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    42
 
#283 := [asserted]: #111
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    43
 
#299 := [mp #283 #296]: #294
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    44
 
#363 := [mp~ #299 #321]: #294
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    45
 
#917 := [mp #363 #916]: #912
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    46
 
#418 := (not #912)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    47
 
#504 := (or #418 #113)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    48
 
#419 := [quant-inst]: #504
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    49
 
[unit-resolution #419 #917 #297]: false
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    50
 
unsat
isabelle