summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Intro/theorems.txt

author | boehmes |

Tue, 07 Dec 2010 15:44:38 +0100 | |

changeset 41064 | 0c447a17770a |

parent 459 | 03b445551763 |

permissions | -rw-r--r-- |

updated SMT certificates

Pretty.setmargin 72; (*existing macros just allow this margin*) print_depth 0; (*operations for "thm"*) prth mp; prth (mp RS mp); prth (conjunct1 RS mp); prth (conjunct1 RSN (2,mp)); prth (mp RS conjunct1); prth (spec RS it); prth (standard it); prth spec; prth (it RS mp); prth (it RS conjunct1); prth (standard it); - prth spec; ALL x. ?P(x) ==> ?P(?x) - prth (it RS mp); [| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==> ?Q2(?x1) - prth (it RS conjunct1); [| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==> ?P6(?x2) - prth (standard it); [| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==> ?Pa(?x) (*flexflex pairs*) - prth refl; ?a = ?a - prth exI; ?P(?x) ==> EX x. ?P(x) - prth (refl RS exI); ?a3(?x) == ?a2(?x) ==> EX x. ?a3(x) = ?a2(x) - prthq (flexflex_rule it); EX x. ?a4 = ?a4 (*Usage of RL*) - val reflk = prth (read_instantiate [("a","k")] refl); k = k val reflk = Thm {hyps=#,maxidx=#,prop=#,sign=#} : thm - prth (reflk RS exI); uncaught exception THM - prths ([reflk] RL [exI]); EX x. x = x EX x. k = x EX x. x = k EX x. k = k (*tactics *) goal FOL.thy "P|P --> P"; by (resolve_tac [impI] 1); by (resolve_tac [disjE] 1); by (assume_tac 3); by (assume_tac 2); by (assume_tac 1); val mythm = prth(result()); goal FOL.thy "(P & Q) | R --> (P | R)"; by (resolve_tac [impI] 1); by (eresolve_tac [disjE] 1); by (dresolve_tac [conjunct1] 1); by (resolve_tac [disjI1] 1); by (resolve_tac [disjI2] 2); by (REPEAT (assume_tac 1)); - goal FOL.thy "(P & Q) | R --> (P | R)"; Level 0 P & Q | R --> P | R 1. P & Q | R --> P | R - by (resolve_tac [impI] 1); Level 1 P & Q | R --> P | R 1. P & Q | R ==> P | R - by (eresolve_tac [disjE] 1); Level 2 P & Q | R --> P | R 1. P & Q ==> P | R 2. R ==> P | R - by (dresolve_tac [conjunct1] 1); Level 3 P & Q | R --> P | R 1. P ==> P | R 2. R ==> P | R - by (resolve_tac [disjI1] 1); Level 4 P & Q | R --> P | R 1. P ==> P 2. R ==> P | R - by (resolve_tac [disjI2] 2); Level 5 P & Q | R --> P | R 1. P ==> P 2. R ==> R - by (REPEAT (assume_tac 1)); Level 6 P & Q | R --> P | R No subgoals! goal FOL.thy "(P | Q) | R --> P | (Q | R)"; by (resolve_tac [impI] 1); by (eresolve_tac [disjE] 1); by (eresolve_tac [disjE] 1); by (resolve_tac [disjI1] 1); by (resolve_tac [disjI2] 2); by (resolve_tac [disjI1] 2); by (resolve_tac [disjI2] 3); by (resolve_tac [disjI2] 3); by (REPEAT (assume_tac 1));