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

Then, you should follow these steps in order to have the latest version of MacFuse:
1) Install - RESTART
2) Install - RESTART
3) Install

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

Link to original blogspot

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%}');
  • {%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

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

BasicsC-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 movementC-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

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

ImportantC-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-HelpC-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/ReplaceC-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-CommandsC-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 commandsC-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
mark bookmark for deletion
rename bookmark
save all listed bookmarks
show bookmark the cursor is over
mark bookmarks to be shown in multiple window
show marked bookmarks (or the one the cursor is over)
toggle listing of the corresponding paths
" path to this file
delete marked bookmarks
Del ?
quit bookmark list

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

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
(large C) copy
mark for erase
delete right away
e or f open file or directory
reread directory structure from file
change group permissions (chgrp)
delete line from listing on screen (don't actually delete)
mark with *
move to next line
open file in other window and go there
C-o open file in other window but don't change there
print file
quit dired
do query-replace in marked files
rename file
remove mark
view file content
delete files marked with D
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
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

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

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

Macro-commandsC-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

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 ControlC-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 postfix, 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): 

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
          definitions, theorems and proofs

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 defined in the parent theories (and their parents, recursively) is automatically visible. Each theory T must reside in a theory file 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.

Download Isabelle

Some Shortcuts in Emacs
Ctrl C + N  -> next line in proof checking
Ctrl C + U -> previous line in proof checking

Ctrl C + Ctrl Enter -> go to position
Ctrl C + A + S -> sledge hammer