{"action":"created","issue":{"url":"https://api.github.com/repos/tip-org/tools/issues/7","repository_url":"https://api.github.com/repos/tip-org/tools","labels_url":"https://api.github.com/repos/tip-org/tools/issues/7/labels{/name}","comments_url":"https://api.github.com/repos/tip-org/tools/issues/7/comments","events_url":"https://api.github.com/repos/tip-org/tools/issues/7/events","html_url":"https://github.com/tip-org/tools/issues/7","id":160590883,"number":7,"title":"Bugs in TIP-to-Isabelle translation","user":{"login":"moajohansson","id":1147797,"avatar_url":"https://avatars.githubusercontent.com/u/1147797?v=3","gravatar_id":"","url":"https://api.github.com/users/moajohansson","html_url":"https://github.com/moajohansson","followers_url":"https://api.github.com/users/moajohansson/followers","following_url":"https://api.github.com/users/moajohansson/following{/other_user}","gists_url":"https://api.github.com/users/moajohansson/gists{/gist_id}","starred_url":"https://api.github.com/users/moajohansson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/moajohansson/subscriptions","organizations_url":"https://api.github.com/users/moajohansson/orgs","repos_url":"https://api.github.com/users/moajohansson/repos","events_url":"https://api.github.com/users/moajohansson/events{/privacy}","received_events_url":"https://api.github.com/users/moajohansson/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"moajohansson","id":1147797,"avatar_url":"https://avatars.githubusercontent.com/u/1147797?v=3","gravatar_id":"","url":"https://api.github.com/users/moajohansson","html_url":"https://github.com/moajohansson","followers_url":"https://api.github.com/users/moajohansson/followers","following_url":"https://api.github.com/users/moajohansson/following{/other_user}","gists_url":"https://api.github.com/users/moajohansson/gists{/gist_id}","starred_url":"https://api.github.com/users/moajohansson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/moajohansson/subscriptions","organizations_url":"https://api.github.com/users/moajohansson/orgs","repos_url":"https://api.github.com/users/moajohansson/repos","events_url":"https://api.github.com/users/moajohansson/events{/privacy}","received_events_url":"https://api.github.com/users/moajohansson/received_events","type":"User","site_admin":false},"assignees":[{"login":"moajohansson","id":1147797,"avatar_url":"https://avatars.githubusercontent.com/u/1147797?v=3","gravatar_id":"","url":"https://api.github.com/users/moajohansson","html_url":"https://github.com/moajohansson","followers_url":"https://api.github.com/users/moajohansson/followers","following_url":"https://api.github.com/users/moajohansson/following{/other_user}","gists_url":"https://api.github.com/users/moajohansson/gists{/gist_id}","starred_url":"https://api.github.com/users/moajohansson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/moajohansson/subscriptions","organizations_url":"https://api.github.com/users/moajohansson/orgs","repos_url":"https://api.github.com/users/moajohansson/repos","events_url":"https://api.github.com/users/moajohansson/events{/privacy}","received_events_url":"https://api.github.com/users/moajohansson/received_events","type":"User","site_admin":false},{"login":"Airini","id":1323224,"avatar_url":"https://avatars.githubusercontent.com/u/1323224?v=3","gravatar_id":"","url":"https://api.github.com/users/Airini","html_url":"https://github.com/Airini","followers_url":"https://api.github.com/users/Airini/followers","following_url":"https://api.github.com/users/Airini/following{/other_user}","gists_url":"https://api.github.com/users/Airini/gists{/gist_id}","starred_url":"https://api.github.com/users/Airini/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/Airini/subscriptions","organizations_url":"https://api.github.com/users/Airini/orgs","repos_url":"https://api.github.com/users/Airini/repos","events_url":"https://api.github.com/users/Airini/events{/privacy}","received_events_url":"https://api.github.com/users/Airini/received_events","type":"User","site_admin":false}],"milestone":null,"comments":1,"created_at":"2016-06-16T06:57:55Z","updated_at":"2016-07-07T09:08:50Z","closed_at":null,"body":"Omar Montano Rivas has tested the TIP-to-Isabelle translation and found a number of bugs:\r\n\r\nHe also wishes to have a pass which translates properties to Isabelle with Frees instead of Vars (i.e. x not ?x). \r\n\r\n-- Variable names are not translated properly to Isabelle/HOL as they sometimes clash with the ASCII representation of HOL constants. e.g. 'EX'\r\n, 'o', etc. For example, the following definition is not accepted by the Isabelle outer syntax parser. The culprit is the name of the variable 'o' in the last equation of the definition. A potential solution would be to just rename the variable 'o' to some new fresh variable.\r\n\r\nfun minus :: \"Nat => Nat => Integer\" where\r\n\"minus (Z) (Z) = P Z\"\r\n| \"minus (Z) (S n) = N n\"\r\n| \"minus (S m) (Z) = P (S m)\"\r\n| \"minus (S m) (S o) = minus m o\"\r\n\r\n-- Identifiers in SMT files such as '1' are not properly translated into Isabelle/HOL. e.g.\r\n\r\nfun 1 :: \"Nat\" where\r\n\"1 = S Z\"\r\n\r\nA potential solution would be to use the definition command using a proper identifier. e.g.\r\n\r\ndefinition id1 :: \"Nat\" (\"1\") where\r\n[simp]: \"id1 = S Z\"\r\n\r\nHere we use the fresh identifier 'id1' and add it to Isabelle/HOL's simpset to simulate the fun command. An alternative would be to use a syntax translation.\r\n\r\n-- Constants with non-functional type are not properly translated to Isabelle/HOL as fun does not support the definition of functions with atomic type (Probably a syntax translation or the definition command would be more suitable). e.g.\r\n\r\nfun one :: \"Nat\" where\r\n\"one = S Z\"\r\n\r\nI think the previous suggested solution would work here.\r\n\r\n-- A harder problem to fix is that some definition translations, can not be proved to terminate automatically by fun such as:\r\n\r\nfun interleave :: \"'a list => 'a list => 'a list\" where\r\n\"interleave (nil2) y = y\"\r\n| \"interleave (cons2 z xs) y = cons2 z (interleave y xs)\"\r\n\r\nHere it occurs to me to make a call to 'isabelle_process' to see if fun can handle the definition. If not, the definition can be phrased with the 'function' command to give it a try to the size_change automatic method, which in this case solves the pending goals.\r\n\r\nfunction (sequential) interleave :: \"'a list => 'a list => 'a list\" where\r\n\"interleave (nil2) y = y\"\r\n| \"interleave (cons2 z xs) y = cons2 z (interleave y xs)\"\r\nby pat_completeness auto\r\ntermination by size_change\r\n\r\nOf course this will not work in all cases such as:\r\n\r\nfunction (sequential) weirdconcat :: \"('a list) list => 'a list\" where\r\n\"weirdconcat (nil2) = nil2\"\r\n| \"weirdconcat (cons2 (nil2) xss) = weirdconcat xss\"\r\n| \"weirdconcat (cons2 (cons2 z xs) xss) =\r\n     cons2 z (weirdconcat (cons2 xs xss))\"\r\nby pat_completeness auto\r\ntermination by size_change\r\n\r\nThe 'relation' method can be used for such cases but I think it would be more difficult to come up with the decreasing measure automatically. One last think that can be done and will work on most cases is to use partiality. For example, if lexicographic order and size_change fail, instead making the translation like this:\r\n\r\nfun m :: \"int => int\" where\r\n\"m x = (if x > 100 then x - 10 else m (m (x + 11)))\"\r\n\r\ntheorem x0 :\r\n  \"!! (n :: int) . ((n <= 100) ==> ((m n) = 91))\"\r\n  by induct_auto_astar\r\n\r\nWe can do it with the equivalent (where m is partial and terminates under n (\"m_dom n\" holds)):\r\n\r\nfunction m :: \"int => int\" where\r\n\"m x = (if x > 100 then x - 10 else m (m (x + 11)))\"\r\nby pat_completeness auto\r\n\r\ntheorem x0 :\r\n  \"!! (n :: int) . m_dom n ⟹ ((n <= 100) ==> ((m n) = 91))\"\r\n\r\n-- Other problem is not produced by the translator itself but by the smt2 file. e.g. the file tip2015/list_z_elem.smt2 only contains \"(check-sat)\". This can be just me not downloading an updated version of the repository.\r\n\r\n-- Another one is not the fault of the translator because Isabelle does not support non-linear datatypes. e.g polyrec_seq_index.smt2 file produces.\r\n\r\ndatatype 'a list = nil2 | cons2 \"'a\" \"'a list\"\r\ndatatype ('a, 'b) Pair = Pair2 \"'a\" \"'b\"\r\ndatatype 'a Maybe = Nothing | Just \"'a\"\r\ndatatype 'a Seq = Nil2 | Cons2 \"'a\" \"(('a, ('a Maybe)) Pair) Seq\"\r\n\r\n-- I can see the translator uses partiality to some extend with the file propositional_AndCommutative.smt2 but some errors are produced. My first guess is that non-constructor patterns are used in definitions:\r\n\r\ne.g.\r\n\r\nmodels ( p q) y = models2 q (models p y)\"\r\n"},"comment":{"url":"https://api.github.com/repos/tip-org/tools/issues/comments/231024395","html_url":"https://github.com/tip-org/tools/issues/7#issuecomment-231024395","issue_url":"https://api.github.com/repos/tip-org/tools/issues/7","id":231024395,"user":{"login":"moajohansson","id":1147797,"avatar_url":"https://avatars.githubusercontent.com/u/1147797?v=3","gravatar_id":"","url":"https://api.github.com/users/moajohansson","html_url":"https://github.com/moajohansson","followers_url":"https://api.github.com/users/moajohansson/followers","following_url":"https://api.github.com/users/moajohansson/following{/other_user}","gists_url":"https://api.github.com/users/moajohansson/gists{/gist_id}","starred_url":"https://api.github.com/users/moajohansson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/moajohansson/subscriptions","organizations_url":"https://api.github.com/users/moajohansson/orgs","repos_url":"https://api.github.com/users/moajohansson/repos","events_url":"https://api.github.com/users/moajohansson/events{/privacy}","received_events_url":"https://api.github.com/users/moajohansson/received_events","type":"User","site_admin":false},"created_at":"2016-07-07T09:08:50Z","updated_at":"2016-07-07T09:08:50Z","body":"There is now an option to remove the explicit top-level forall quantifiers in Isabelle, and one to leave them in. See: \r\ntip --isabelle\r\ntip --isabelle-explicit-forall"}}
{"actor":{"display_login":"moajohansson"}}