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/18 14:38] 131.246.92.39 [General Emacs] |
start [2012/07/19 14:59] 131.246.92.39 [Assorted gimmicks] |
||
---|---|---|---|
Line 117: | Line 117: | ||
=== Basic Methods === | === Basic Methods === | ||
- | ^ Name ^ Parameters ^ All goals ^ Safe ^ New Goals ^ Variants ^ | + | ^ Name ^ Parameters ^ All goals ^ Safe ^ New Goals ^ Variants ^ |
| ''[[reference:assumption|assumption]]'' | --- | | x | | | | | ''[[reference:assumption|assumption]]'' | --- | | x | | | | ||
| ''[[reference:cases|cases]]'' | an expression | | x | x | ''case_tac'' | | | ''[[reference:cases|cases]]'' | an expression | | x | x | ''case_tac'' | | ||
| ''[[reference:drule|drule]]'' | a rule | | | x | ''drule(k)'', ''drule_tac'' | | | ''[[reference:drule|drule]]'' | a rule | | | x | ''drule(k)'', ''drule_tac'' | | ||
| ''[[reference:erule|erule]]'' | a rule | | | x | ''erule(k)'', ''erule_tac'' | | | ''[[reference:erule|erule]]'' | a rule | | | x | ''erule(k)'', ''erule_tac'' | | ||
- | | ''[[reference:fold|fold]]'' | ? | x | x | ? | | | + | | ''[[reference:fold|fold]]'' | a definition (or equation) | x | x | | | |
| ''[[reference:frule|frule]]'' | a rule | | x | x | ''frule(k)'', ''frule_tac'' | | | ''[[reference:frule|frule]]'' | a rule | | x | x | ''frule(k)'', ''frule_tac'' | | ||
| ''[[reference:induct|induct]]'' | a variable | | | x | ''induct_tac'' | | | ''[[reference:induct|induct]]'' | a variable | | | x | ''induct_tac'' | | ||
Line 128: | Line 128: | ||
| ''[[reference:rename_tac|rename_tac]]'' | list of identifiers | | | | | | | ''[[reference:rename_tac|rename_tac]]'' | list of identifiers | | | | | | ||
| ''[[reference:rotate_tac|rotate_tac]]'' | an integer | | x | | | | | ''[[reference:rotate_tac|rotate_tac]]'' | an integer | | x | | | | ||
- | | ''[[reference:rule (method)|rule]]'' | a rule | | | x | ''rule(k)'', ''rule_tac'' | | + | | ''[[reference:rule (method)|rule]]'' | a rule | | | x | ''rule(k)'', ''rule_tac'' | |
| ''[[reference:split|split]]'' | a splitting rule | | ? | x | | | | ''[[reference:split|split]]'' | a splitting rule | | ? | x | | | ||
| ''[[reference:subgoal_tac|subgoal_tac]]'' | a formula | | | x | | | | ''[[reference:subgoal_tac|subgoal_tac]]'' | a formula | | | x | | | ||
- | | ''[[reference:subst|subst]]'' | ? | | x | x | ''subst (asm)'' | | + | | ''[[reference:subst|subst]]'' | a definition (or equation) | | x | x | ''subst (asm)'' | |
| ''[[reference:thin_tac|thin_tac]]'' | a formula | | | | | | | ''[[reference:thin_tac|thin_tac]]'' | a formula | | | | | | ||
- | | ''[[reference:unfold|unfold]]'' | a definition | x | x | ? | | | + | | ''[[reference:unfold|unfold]]'' | a definition (or equation) | x | x | ? | | |
=== Automated Methods === | === Automated Methods === | ||
Line 217: | 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. |