## Thursday, November 07, 2013

### Isabelle Keyword Dictionary

Isabelle/Isar Reference Manual
For a comprehensive guide on Isabelle commands

declare thmsdeclares theorems to the current local theory context. No theorem binding is involved here, unlike theorems or lemmas (cf.§5.11), so declare only has the efect of applying attributes as included in the theorem speci cation. Isar manual p85

Locales - A sectioning concept for Isabelle
Locales are a means to de fine local scopes for the interactive proving process of the theorem prover Isabelle. They delimit a range in which fixed assumption are made, and theorems are proved that depend on these assumptions. A locale may also contain constants de fined locally and associated with pretty printing syntax. Locales can be seen as a simple form of modules. read more

Recursive Functions - Defining Recursive Functions in Isabelle/HOL
This tutorial describes the use of the new function package, which
provides general recursive function de nitions for Isabelle/HOL. We start
with very simple examples and then gradually move on to more advanced
topics such as manual termination proofs, nested recursion, partiality, tail
recursion and congruence rules. read tutorial

## Tuesday, October 22, 2013

### Change uuid of harddrive in VirtualBox

When you remove a hard disk from a Virtual PC you cannot put it back into the same Virtual PC. Hence you have to change the UUID of the hard disk before you can attach it to the same Virtual PC. You can do it by issuing the following command:

VBoxManage internalcommands sethduuid disk2.vdi

## Thursday, April 18, 2013

### To enable NTFS copying and modification rights in Mac

Install NTFS-3G for Mac OS X 2010.10.2

2) Install http://www.tuxera.com/mac/macfuse-core-10.5-2.1.9.dmg - RESTART
3) Install http://content.wuala.com/contents/grahamperrin/public/2010/07/31/a/MacFUSE.prefPane-2.0-64-bit-2009-09-10.zip?dl=1

Now you have the latest version of MacFuse and the 64bit prefpane.

### Wordpress : “You do not have sufficient permissions to access this page” after you change database prefix

Have you changed the prefix of your database tables? I'm 90% sure, that this is your problem.
The thing is that WordPress uses the `\$table_prefix` variable for forming the option and usermeta keys names, where it's storing the roles and capabilities information. So once you change the prefix, but don't update your db, you get this error. Here's how to fix it - execute this SQL command through phpMyAdmin, or a different interface for interacting with your DB(you can do it with PHP as well):
``````UPDATE `{%TABLE_PREFIX%}usermeta` SET `meta_key` = replace(`meta_key`, '{%OLD_TABLE_PREFIX%}', '{%NEW_TABLE_PREFIX%}');
UPDATE `{%TABLE_PREFIX%}options` SET `option_name` = replace(`option_name`, '{%OLD_TABLE_PREFIX%}', '{%NEW_TABLE_PREFIX%}');``````
Where:
• `{%TABLE_PREFIX%}` is your current `\$table_prefix`(as set in `wp-config.php`)
• `{%OLD_TABLE_PREFIX%}` is your previous `\$table_prefix`
• `{%NEW_TABLE_PREFIX%}` is your new(current) `\$table_prefix` - it will most-likely be the same as your `{%TABLE_PREFIX%}`.
So if your old `\$table_prefix` was `wp_test_` and your new one is `wp_`, you would do this query:
``````UPDATE `wp_usermeta` SET `meta_key` = replace(`meta_key`, 'wp_test_', 'wp_');
UPDATE `wp_options` SET `option_name` = replace(`option_name`, 'wp_test_', 'wp_');``````
``Link to the Original Post!!!``
``````
``````

## Wednesday, March 20, 2013

### Formal Logic Symbols

$\models$  double turnstile
In logic, the symbol $\vDash$ or $\models$ is called the double turnstile. It is closely related to the turnstile symbol $\vdash$, which has a single bar across the middle. It is often read as "entails", "models" or "is a semantic consequence of".

## Thursday, February 28, 2013

### How to Take a Screenshot in Mac OS X

How to Take a Screenshot in Mac OS X
http://www.wikihow.com/Take-a-Screenshot-in-Mac-OS-X

How To Capture a Screen Shot with Mac OS X

## Saturday, February 23, 2013

### A Compact Introduction to Isabelle/HOL

A Compact Introduction to Isabelle/HOL

I found this tutorial by Tobias to be very useful in understanding isabelle Theorem Prover.

Further, Getting Sarted with isabelle, is for those formalism enthusiasts, who wants to get a first shot at Isabelle Theorem Prover.

### Emacs Commands List

Emacs Commands List
C = Control
M = Meta = Alt|Esc

Basics`C-x C-f `"find" file i.e. open/create a file in buffer
`C-x C-s `save the file
`C-x C-w `write the text to an alternate name
`C-x C-v `find alternate file
`C-x i `insert file at cursor position
`C-x b `create/switch buffers
`C-x C-b `show buffer list
`C-x k `kill buffer
`C-z `suspend emacs
`C-X C-c `close down emacs

Basic movement`C-f `forward char
`C-b `backward char
`C-p `previous line
`C-n `next line
`M-f `forward one word
`M-b `backward one word
`C-a `beginning of line
`C-e `end of line
`C-v `one page up
`M-v `scroll down one page
`M-< `beginning of text
`M-> `end of text

Editing
`M-n `repeat the following command n times
`C-u `repeat the following command 4 times
`C-u n `repeat n times
`C-d `delete a char
`M-d `delete word
`M-Del `delete word backwards
`C-k `kill line

`C-Space `Set beginning mark (for region marking for example)
`C-W `"kill" (delete) the marked region region
`M-W `copy the marked region
`C-y `"yank" (paste) the copied/killed region/line
`M-y `yank earlier text (cycle through kill buffer)
`C-x C-x `exchange cursor and mark

`C-t `transpose two chars
`M-t `transpose two words
`C-x C-t `transpose lines
`M-u `make letters uppercase in word from cursor position to end
`M-c `simply make first letter in word uppercase
`M-l `opposite to M-u

Important`C-g `quit the running/entered command
`C-x u `undo previous action
`M-x revert-buffer RETURN `(insert like this) undo all changes since last save
`M-x recover-file RETURN `Recover text from an autosave-file
`M-x recover-session RETURN `if you edited several files

Online-Help`C-h c `which command does this keystroke invoke
`C-h k `which command does this keystroke invoke and what does it do?
`C-h l `what were my last 100 typed keys
`C-h w `what key-combo does this command have?
`C-h f `what does this function do
`C-h v `what's this variable and what is it's value
`C-h b `show all keycommands for this buffer
`C-h t `start the emacs tutorial
`C-h i `start the info reader
`C-h C-k `start up info reader and go to a certain key-combo point
`C-h F `show the emacs FAQ
`C-h p `show infos about the Elisp package on this machine

Search/Replace`C-s `Search forward
`C-r `search backward
`C-g `return to where search started (if you are still in search mode)
`M-% `query replace
`Space or y `replace this occurence
`Del or n `don't replace
`. `only replace this and exit (replace)
`, `replace and pause (resume with Space or y)
`! `replace all following occurences
`^ `back to previous match
`RETURN or q `quit replace

Search/Replace with regular expressionsCharacters to use in regular expressions:
`^ `beginning of line
`\$ `end of line
`. `single char
`.* `group or null of chars
`\< `beginning of a word
`\> `end of a word
`[] `every char inside the backets (for example [a-z] means every small letter)

`M C-s RETURN `search for regular expression forward
`M C-r RETURN `search for regular expression backward
`M C-s `incremental search
`C-s `repeat incremental search
`M C-r `incremental search backwards
`C-r `repeat backwards
`M-x query-replace-regexp `search and replace

Window-Commands`C-x 2 `split window vertically
`C-x o `change to other window
`C-x 0 `delete window
`C-x 1 `close all windows except the one the cursors in
`C-x ^ `enlarge window
`M-x shrink-window `command says it ;-)
`M C-v `scroll other window
`C-x 4 f `find file in other window
`C-x 4 o `change to other window
`C-x 4 0 `kill buffer and window
`C-x 5 2 `make new frame
`C-x 5 f `find file in other frame
`C-x 5 o `change to other frame
`C-x 5 0 `close this frame

Bookmark commands`C-x r m `set a bookmark at current cursor pos
`C-x r b `jump to bookmark
`M-x bookmark-rename `says it
`M-x bookmark-delete `"
`M-x bookmark-save` "
`C-x r l `list bookmarks
`d `mark bookmark for deletion
`r `rename bookmark
`s `save all listed bookmarks
`f `show bookmark the cursor is over
`m `mark bookmarks to be shown in multiple window
`v `show marked bookmarks (or the one the cursor is over)
`t `toggle listing of the corresponding paths
`w `" path to this file
`x `delete marked bookmarks
`Del `?
`q `quit bookmark list

`M-x bookmark-write `write all bookmarks in given file
`M-x bookmark-load `load bookmark from given file

Shell
`M-x shell `starts shell modus
`C-c C-c `same as C-c under unix (stop running job)
`C-d `delete char forward
`C-c C-d `Send EOF
`C-c C-z `suspend job (C-z under unix)
`M-p `show previous commands

DIRectory EDitor (dired)`C-x d `start up dired
`C `(large C) copy
`d `mark for erase
`D `delete right away
`e or f `open file or directory
`g `reread directory structure from file
`G `change group permissions (chgrp)
`k `delete line from listing on screen (don't actually delete)
`m `mark with *
`n `move to next line
`o `open file in other window and go there
`C-o `open file in other window but don't change there
`P `print file
`q `quit dired
`Q `do query-replace in marked files
`R `rename file
`u `remove mark
`v `view file content
`x `delete files marked with D
`z `compress file
`M-Del `remove all marks (whatever kind)
`~ `mark backup files (name~ files) for deletion
`# `mark auto-save files (#name#) for deletion
`*/ `mark directory with * (C-u * removes that mark again)
`= `compare this file with marked file
`M-= `compare this file with it's backup file
`! `apply shell command to this file
`M-} `change to the next file marked with * od D
`M-{ `" previous "
`% d `mark files described through regular expression for deletion
`% m `" (with *)
`+ `create directory
`> `changed to next dir
`< `change to previous dir
`s `toggle between sorting by name or date

Maybe into this category also fits this command:
`M-x speedbar `starts up a separate window with a directory view

Telnet
`M-x telnet `starts up telnet-modus
`C-d `either delete char or send EOF
`C-c C-c `stop running job (similar to C-c under unix)
`C-c C-d `send EOF
`C-c C-o `clear output of last command
`C-c C-z `suspend execution of command
`C-c C-u `kill line backwards
`M-p `recall previous command

Text
Works only in text mode
`M-s `center line
`M-S `center paragraph
`M-x center-region `name says

Macro-commands`C-x ( `start macro definition
`C-x ) `end of macro definition
`C-x e `execute last definied macro
`M-n C-x e `execute last defined macro n times
`M-x name-last-kbd-macro `give name to macro (for saving)
`M-x insert-keyboard-macro `save named macro into file
`M-x load-file `load macro
`M-x macroname `execute macroname

Programming
`M C-\ `indent region between cursor and mark
`M-m `move to first (non-space) char in this line
`M-^ `attach this line to previous
`M-; `formatize and indent comment
C, C++ and Java Modes
`M-a `beginning of statement
`M-e `end of statement
`M C-a `beginning of function
`M C-e `end of function
`C-c RETURN `Set cursor to beginning of function and mark at the end
`C-c C-q `indent the whole function according to indention style
`C-c C-a `toggle modus in which after electric signs (like {}:';./*) emacs does the indention
`C-c C-d `toggle auto hungry mode in which emacs deletes groups of spaces with one del-press
`C-c C-u `go to beginning of this preprocessor statement
`C-c C-c `comment out marked area
More general (I guess)
`M-x outline-minor-mode `collapses function definitions in a file to a mere {...}
`M-x show-subtree `If you are in one of the collapsed functions, this un-collapses it
In order to achive some of the feats coming up now you have to run etags *.c *.h *.cpp (or what ever ending you source files have) in the source directory
`M-. `(Thats Meta dot) If you are in a function call, this will take you to it's definition
`M-x tags-search ENTER `Searches through all you etaged
`M-, `(Meta comma) jumps to the next occurence for tags-search
`M-x tags-query-replace `yum. This lets you replace some text in all the tagged files

GDB (Debugger)`M-x gdb `starts up gdm in an extra window

Version Control`C-x v d `show all registered files in this dir
`C-x v = `show diff between versions
`C-x v u `remove all changes since last checkin
`C-x v ~ `show certain version in different window
`C-x v l `print log
`C-x v i `mark file for version control add
`C-x v h `insert version control header into file
`C-x v r `check out named snapshot
`C-x v s `create named snapshot
`C-x v a `create changelog file in gnu-style

## Friday, February 22, 2013

### Isabelle Syntax

extract from isabelle- Programming

Basic Syntax
Most statements of logic (inner-syntax) should be places in speech-marks
"numberMonth n = months!(n - 1)"

Isabelle employs LATEX-like tags for unicode syntax
• e.g.x.y.x  is written as per LATEX.
• \forall x.\exists y.y > x
HOL(Higher Order Logic) is a typed logic whose type system resembles that of functional programming languages. Thus there are:
• base types, in particular bool, the type of truth values, nat, the type of natural numbers (), and int, the type of mathematical integers ().
• type constructors, in particular list, the type of lists, and set, the type of sets. Type constructors are written postﬁx, e.g. nat list is the type of lists whose elements are natural numbers.
• function types, denoted by.
• type variables, denoted by 'a, 'b etc., just like in ML

• Formulae are terms of type bool. There are the basic constants True andFalse and the usual logical connectives (in decreasing order of precedence):

Theories
Roughly speaking, a theory is a named collection of types, functions, and theorems, much like a module in a programming language. All the Isabelle text that you ever type needs to go into a theory. The general format of a

theory T is
theory T
imports T1 : : : T n
begin
deﬁnitions, theorems and proofs
end

where T1 : : : T n are the names of existing theories that T is based on. The Ti are the direct parent theories of T. Everything deﬁned in the parent theories (and their parents, recursively) is automatically visible. Each theory T must reside in a theory ﬁle named T:thy.

### Installing Isabelle Theorem Prover

Introduction to Isabelle [ref: wikipedia, York University],

The Isabelle theorem prover is an interactive theorem prover, successor of the Higher Order Logic (HOL) theorem prover. It is an LCF-style theorem prover (written in Standard ML), so it is based on a small logical core guaranteeing logical correctness. Isabelle is generic: it provides a meta-logic (a weak type theory), which is used to encode object logics like First-order logic (FOL), Higher-order logic (HOL) or Zermelo–Fraenkel set theory

Isabelle consists of two components: the proof engine and user interface.

Isabelle has several interfaces available:

• Proof General (emacs) [included]
• PIDE (jEdit) [included]
• I3P (Netbeans)

I just started using isabelle 3 weeks ago and according to advice from Simon Foster I'm sticking with Emacs interface for now.