equal
deleted
inserted
replaced
13 (*>*) |
13 (*>*) |
14 |
14 |
15 chapter {* Parsing\label{chp:parsing} *} |
15 chapter {* Parsing\label{chp:parsing} *} |
16 |
16 |
17 text {* |
17 text {* |
|
18 \begin{flushright} |
|
19 {\em An important principle underlying the success and popularity of Unix\\ is |
|
20 the philosophy of building on the work of others.} \\[1ex] |
|
21 Linus Torwalds in the email exchange\\ with Andrew S.~Tannenbaum |
|
22 \end{flushright} |
|
23 |
|
24 |
18 Isabelle distinguishes between \emph{outer} and \emph{inner} |
25 Isabelle distinguishes between \emph{outer} and \emph{inner} |
19 syntax. Commands, such as \isacommand{definition}, \isacommand{inductive} |
26 syntax. Commands, such as \isacommand{definition}, \isacommand{inductive} |
20 and so on, belong to the outer syntax, whereas terms, types and so on belong |
27 and so on, belong to the outer syntax, whereas terms, types and so on belong |
21 to the inner syntax. For parsing inner syntax, Isabelle uses a rather |
28 to the inner syntax. For parsing inner syntax, Isabelle uses a rather |
22 general and sophisticated algorithm, which is driven by priority |
29 general and sophisticated algorithm, which is driven by priority |
1384 \begin{minipage}{\textwidth} |
1391 \begin{minipage}{\textwidth} |
1385 @{subgoals} |
1392 @{subgoals} |
1386 \end{minipage} *} |
1393 \end{minipage} *} |
1387 (*<*)oops(*>*) |
1394 (*<*)oops(*>*) |
1388 |
1395 |
|
1396 method_setup test = {* Scan.lift (Scan.succeed (K Method.succeed)) *} {* bla *} |
|
1397 |
|
1398 lemma "True" |
|
1399 apply(test) |
|
1400 oops |
|
1401 |
|
1402 method_setup joker = {* Scan.lift (Scan.succeed (fn ctxt => Method.cheating true ctxt)) *} {* bla *} |
|
1403 |
|
1404 lemma "False" |
|
1405 apply(joker) |
|
1406 oops |
|
1407 |
|
1408 text {* if true is set then always works *} |
|
1409 |
|
1410 ML {* atac *} |
|
1411 |
|
1412 method_setup first_atac = {* Scan.lift (Scan.succeed (K (SIMPLE_METHOD (atac 1)))) *} {* bla *} |
|
1413 |
|
1414 ML {* HEADGOAL *} |
|
1415 |
|
1416 lemma "A \<Longrightarrow> A" |
|
1417 apply(first_atac) |
|
1418 oops |
|
1419 |
|
1420 method_setup my_atac = {* Scan.lift (Scan.succeed (K (SIMPLE_METHOD' atac))) *} {* bla *} |
|
1421 |
|
1422 lemma "A \<Longrightarrow> A" |
|
1423 apply(my_atac) |
|
1424 oops |
|
1425 |
|
1426 |
1389 |
1427 |
1390 |
1428 |
1391 |
1429 |
1392 |
1430 |
1393 |
1431 |
1396 ML {* METHOD *} |
1434 ML {* METHOD *} |
1397 ML {* K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1)) *} |
1435 ML {* K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1)) *} |
1398 ML {* Scan.succeed *} |
1436 ML {* Scan.succeed *} |
1399 *) |
1437 *) |
1400 |
1438 |
1401 text {* |
1439 ML {* resolve_tac *} |
|
1440 |
|
1441 method_setup myrule = |
|
1442 {* Scan.lift (Scan.succeed (K (METHOD (fn thms => resolve_tac thms 1)))) *} |
|
1443 {* bla *} |
|
1444 |
|
1445 lemma |
|
1446 assumes a: "A \<Longrightarrow> B \<Longrightarrow> C" |
|
1447 shows "C" |
|
1448 using a |
|
1449 apply(myrule) |
|
1450 oops |
|
1451 |
|
1452 |
|
1453 |
|
1454 text {* |
|
1455 (********************************************************) |
1402 (FIXME: explain a version of rule-tac) |
1456 (FIXME: explain a version of rule-tac) |
1403 *} |
1457 *} |
1404 |
1458 |
1405 (*<*) |
1459 (*<*) |
1406 (* THIS IS AN OLD VERSION OF THE PARSING CHAPTER BY JEREMY DAWSON *) |
1460 (* THIS IS AN OLD VERSION OF THE PARSING CHAPTER BY JEREMY DAWSON *) |