User Tools
start
Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Last revision Both sides next revision | ||
|
start [2012/04/13 11:55] 131.246.92.39 [Methods] |
start [2012/07/19 14:59] 131.246.92.39 [Assorted gimmicks] |
||
|---|---|---|---|
| Line 6: | Line 6: | ||
| {{ :isabelle_hol.gif?nolink&200 |}} | {{ :isabelle_hol.gif?nolink&200 |}} | ||
| - | Please use the [[faq|FAQ - Ask Questions]] page to post and view questions and the [[exam|Exam Questions]] page to collect possible questions for the exams. The [[official:goals|Goals of the Exercises]] page summarizes what you should have learned by doing them. | + | Please use the [[faq]] page to post and view questions and the [[exam]] page to collect possible questions for the exams. The [[official:goals]] page summarizes what you should have learned by doing them. |
| For best practices in Isabelle/HOL, see the [[best_practices|corresponding page]]. | For best practices in Isabelle/HOL, see the [[best_practices|corresponding page]]. | ||
| - | Please also check out and add stuff concerning the [[editor|Editor]], [[syntax|Isabelle/HOL Syntax]] and useful [[references|External References]]. | + | Please also check out and add stuff concerning the [[editor]], [[syntax]] and useful [[references]]. |
| Last but not least, you can post and check out [[code_repository|Example Code]]. | Last but not least, you can post and check out [[code_repository|Example Code]]. | ||
| - | Help us to improve the Wiki by checking and complementing existing content, as well as creating [[wanted pages|needed entries]]! | + | Help us to improve the Wiki by checking and complementing existing content, as well as creating [[wanted pages]]! |
| ===== Shortcuts ===== | ===== Shortcuts ===== | ||
| Line 20: | Line 20: | ||
| * ''C-x C-f'' -- open a file | * ''C-x C-f'' -- open a file | ||
| + | * ''C-x C-s'' -- save the current file | ||
| * ''C-k'' -- delete the rest of the line | * ''C-k'' -- delete the rest of the line | ||
| * ''C-a'' -- jump to the beginning of the current line | * ''C-a'' -- jump to the beginning of the current line | ||
| Line 43: | Line 44: | ||
| ==== Menu Magic ==== | ==== Menu Magic ==== | ||
| - | * [Options → C-x/C-c/C-v Cut and Paste (CUA)] -- enable standard hotkeys for copy and paste | + | * [Options -> C-x/C-c/C-v Cut and Paste (CUA)] -- enable standard hotkeys for copy and paste |
| - | * [Isabelle → Show Me → Methods] -- Prints a list of all available methods | + | * [Isabelle -> Show Me -> Methods] -- Prints a list of all available methods |
| - | * [Isabelle → Settings → Display] -- show hidden symbols such as types or parentheses for debugging. (in theory mode) | + | * [Isabelle -> Settings -> Display] -- show hidden symbols such as types or parentheses for debugging. (in theory mode) |
| - | * [Isabelle → Help → Isabelle Documentation] -- documentation | + | * [Isabelle -> Help -> Isabelle Documentation] -- documentation |
| - | * [Proof-General → Quick Options → Display → Use Three Panes] -- check to have a more comfortable setup (in theory mode) | + | * [Proof-General -> Quick Options -> Display -> Use Three Panes] -- check to have a more comfortable setup (in theory mode) |
| + | * [Proof-General -> Advanced -> Customize -> Faces -> Proof Locked Face] -- change the color of the "locked" region of proofs (e.g. Khaki: #F0E68C) | ||
| ===== Syntax ===== | ===== Syntax ===== | ||
| Line 69: | Line 71: | ||
| ^ Logics | $\land$ | $\lor$ | $\neg$ | $\longrightarrow$ | $\leftrightarrow$ | $\forall$ | $\exists$ | | ^ Logics | $\land$ | $\lor$ | $\neg$ | $\longrightarrow$ | $\leftrightarrow$ | $\forall$ | $\exists$ | | ||
| - | ^ ASCII | ''/\'' | ''\/'' | ''\not'' | ''<nowiki>--></nowiki>'' | ''='' | ''ALL'' | ''EX'' | | + | ^ ASCII | ''/\'' | ''\/'' | ''\not'' | ''<nowiki>--></nowiki>'' | ''<nowiki><-></nowiki>'' or ''='' | ''ALL'' | ''EX'' | |
| ^ Meta | $\bigwedge$ | $\Longrightarrow$ | $\equiv$ | $[|$ | $|]$ | | ^ Meta | $\bigwedge$ | $\Longrightarrow$ | $\equiv$ | $[|$ | $|]$ | | ||
| Line 112: | Line 114: | ||
| done | done | ||
| ==== Methods ==== | ==== Methods ==== | ||
| + | |||
| === Basic Methods === | === Basic Methods === | ||
| - | ^ Name ^ Parameters ^ All goals ^ Safe ^ New Goals ^ Variants ^ | + | |
| - | | ''[[reference:assumption]]'' | --- | | x | | | | + | ^ Name ^ Parameters ^ All goals ^ Safe ^ New Goals ^ Variants ^ |
| - | | ''[[reference:cases]]'' | an expression | | x | x | ''case_tac'' | | + | | ''[[reference:assumption|assumption]]'' | --- | | x | | | |
| - | | ''[[reference:drule]]'' | a rule | | | x | ''drule(k)'', ''drule_tac'' | | + | | ''[[reference:cases|cases]]'' | an expression | | x | x | ''case_tac'' | |
| - | | ''[[reference:erule]]'' | a rule | | | x | ''erule(k)'', ''erule_tac'' | | + | | ''[[reference:drule|drule]]'' | a rule | | | x | ''drule(k)'', ''drule_tac'' | |
| - | | ''[[reference:fold]]'' | ? | x | x | ? | | | + | | ''[[reference:erule|erule]]'' | a rule | | | x | ''erule(k)'', ''erule_tac'' | |
| - | | ''[[reference:frule]]'' | a rule | | x | x | ''frule(k)'', ''frule_tac'' | | + | | ''[[reference:fold|fold]]'' | a definition (or equation) | x | x | | | |
| - | | ''[[reference:induct]]'' | a variable | | | x | ''induct_tac'' | | + | | ''[[reference:frule|frule]]'' | a rule | | x | x | ''frule(k)'', ''frule_tac'' | |
| - | | ''[[reference:insert]]'' | a theorem | x | x | | ''cut_tac'' | | + | | ''[[reference:induct|induct]]'' | a variable | | | x | ''induct_tac'' | |
| - | | ''[[reference:rename_tac]]'' | list of identifiers | | | | | | + | | ''[[reference:insert|insert]]'' | a theorem | x | x | | ''cut_tac'' | |
| - | | ''[[reference:rotate_tac]]'' | an integer | | x | | | | + | | ''[[reference:rename_tac|rename_tac]]'' | list of identifiers | | | | | |
| - | | ''[[reference:rule (method)|rule]]'' | a rule | | | x | ''rule(k)'', ''rule_tac'' | | + | | ''[[reference:rotate_tac|rotate_tac]]'' | an integer | | x | | | |
| - | | ''[[reference:split]]'' | a splitting rule | | ? | x | | | + | | ''[[reference:rule (method)|rule]]'' | a rule | | | x | ''rule(k)'', ''rule_tac'' | |
| - | | ''[[reference:subgoal_tac]]'' | a formula | | | x | | | + | | ''[[reference:split|split]]'' | a splitting rule | | ? | x | | |
| - | | ''[[reference:subst]]'' | ? | | x | x | ''subst (asm)'' | | + | | ''[[reference:subgoal_tac|subgoal_tac]]'' | a formula | | | x | | |
| - | | ''[[reference:thin_tac]]'' | a formula | | | | | | + | | ''[[reference:subst|subst]]'' | a definition (or equation) | | x | x | ''subst (asm)'' | |
| - | | ''[[reference:unfold]]'' | a definition | x | x | ? | | | + | | ''[[reference:thin_tac|thin_tac]]'' | a formula | | | | | |
| + | | ''[[reference:unfold|unfold]]'' | a definition (or equation) | x | x | ? | | | ||
| === Automated Methods === | === Automated Methods === | ||
| + | |||
| ^ Name ^ Classical ^ Simp ^ All goals ^ Safe ^ Splits ^ Finishes ^ Strength ^ Weakness ^ | ^ Name ^ Classical ^ Simp ^ All goals ^ Safe ^ Splits ^ Finishes ^ Strength ^ Weakness ^ | ||
| - | | ''[[reference:arith]]'' | | | | x | | x | linear arithmetics | exponentially slow for many operators | | + | | ''[[reference:arith|arith]]'' | | | | x | | x | linear arithmetics | exponentially slow for many operators | |
| - | | ''[[reference:auto]]'' | x | x | x | | x | | | | | + | | ''[[reference:auto|auto]]'' | x | x | x | | x | | | | |
| - | | ''[[reference:blast]]'' | x | | | x | | x | logics, sets; fast | | | + | | ''[[reference:blast|blast]]'' | x | | | x | | x | logics, sets; fast | | |
| - | | ''[[reference:clarify]]'' | x | | | x | | | | | | + | | ''[[reference:clarify|clarify]]'' | x | | | x | | | | | |
| - | | ''[[reference:clarsimp]]'' | x | x | | x | | | | | | + | | ''[[reference:clarsimp|clarsimp]]'' | x | x | | x | | | | | |
| - | | ''[[reference:force]]'' | x | x | | x | | x | | | | + | | ''[[reference:force|force]]'' | x | x | | x | | x | | | |
| - | | ''[[reference:metis]]'' | x | | | x | | x | logics | no sets | | + | | ''[[reference:metis|metis]]'' | x | | | x | | x | logics | no sets | |
| - | | ''[[reference:safe]]'' | x | | x | x | x | | | | | + | | ''[[reference:safe|safe]]'' | x | | x | x | x | | | | |
| - | | ''[[reference:simp]]'' | | x | | x | x | | | | | + | | ''[[reference:simp|simp]]'' | | x | | x | x | | | | |
| - | | ''[[reference:simp_all]]'' | | x | x | x | x | | | | | + | | ''[[reference:simp_all|simp_all]]'' | | x | x | x | x | | | | |
| Note that safety of automated proof methods can be sabotaged by adding unsafe rules to rule sets used. | Note that safety of automated proof methods can be sabotaged by adding unsafe rules to rule sets used. | ||
| Line 211: | Line 217: | ||
| * ''f(x := y)'' -- the //function update//: the result of this expression is the function ''f'' updated such that it now returns ''y'' for parameter ''x''; the other values do not change. | * ''f(x := y)'' -- the //function update//: the result of this expression is the function ''f'' updated such that it now returns ''y'' for parameter ''x''; the other values do not change. | ||
| * ''{x. P x}'' -- the set of values fulfilling predicate ''P''. For instance, ''{x::nat. x dvd 125}'' is the set of (natural) divisors of $125$. | * ''{x. P x}'' -- the set of values fulfilling predicate ''P''. For instance, ''{x::nat. x dvd 125}'' is the set of (natural) divisors of $125$. | ||
| + | * ''{E x | x. P x}'' -- the set of values created by expression ''E'', for all values fulfilling predicate ''P'', ''{x + y | x y. x < 10 /\ y < 10}'' is the set of sums of all pairs of natural numbers with a single digit. | ||
start.txt · Last modified: 2014/04/30 15:28 by peter
Page Tools
