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_bv_01.proof
author wenzelm
Sat, 24 Oct 2009 19:22:39 +0200
changeset 33093 d010f61d3702
parent 33010 39f73a59e855
permissions -rw-r--r--
eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already; fully authentic merge;
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
 
#6 := 0::int
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     3
 
decl uf_1 :: (-> bv[2] int)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     4
 
#4 := bv[0:2]
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     5
 
#5 := (uf_1 bv[0:2])
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     6
 
#225 := (<= #5 0::int)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     7
 
#311 := (not #225)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     8
 
#20 := (:var 0 bv[2])
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
     9
 
#21 := (uf_1 #20)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    10
 
#640 := (pattern #21)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    11
 
#54 := (<= #21 0::int)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    12
 
#55 := (not #54)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    13
 
#641 := (forall (vars (?x1 bv[2])) (:pat #640) #55)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    14
 
#58 := (forall (vars (?x1 bv[2])) #55)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    15
 
#644 := (iff #58 #641)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    16
 
#642 := (iff #55 #55)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    17
 
#643 := [refl]: #642
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    18
 
#645 := [quant-intro #643]: #644
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    19
 
#113 := (~ #58 #58)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    20
 
#115 := (~ #55 #55)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    21
 
#116 := [refl]: #115
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    22
 
#114 := [nnf-pos #116]: #113
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    23
 
#22 := (< 0::int #21)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    24
 
#23 := (forall (vars (?x1 bv[2])) #22)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    25
 
#59 := (iff #23 #58)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    26
 
#56 := (iff #22 #55)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    27
 
#57 := [rewrite]: #56
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    28
 
#60 := [quant-intro #57]: #59
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    29
 
#51 := [asserted]: #23
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    30
 
#61 := [mp #51 #60]: #58
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    31
 
#111 := [mp~ #61 #114]: #58
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    32
 
#646 := [mp #111 #645]: #641
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    33
 
#227 := (not #641)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    34
 
#313 := (or #227 #311)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    35
 
#304 := [quant-inst]: #313
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    36
 
#635 := [unit-resolution #304 #646]: #311
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    37
 
#7 := (= #5 0::int)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    38
 
#47 := [asserted]: #7
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    39
 
#638 := (not #7)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    40
 
#633 := (or #638 #225)
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    41
 
#639 := [th-lemma]: #633
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    42
 
[unit-resolution #639 #47 #635]: false
39f73a59e855 added proof reconstructon for Z3,
boehmes
parents:
diff changeset 
    43
 
unsat
isabelle