equal
deleted
inserted
replaced
11 (*>*) |
11 (*>*) |
12 |
12 |
13 chapter {* Tactical Reasoning\label{chp:tactical} *} |
13 chapter {* Tactical Reasoning\label{chp:tactical} *} |
14 |
14 |
15 text {* |
15 text {* |
|
16 \begin{flushright} |
|
17 {\em ``The most effective debugging tool is still careful thought, coupled with |
|
18 judiciously placed print statements.''} \\[1ex] |
|
19 Brian Kernighan |
|
20 \end{flushright} |
|
21 |
|
22 \medskip |
16 One of the main reason for descending to the ML-level of Isabelle is to be |
23 One of the main reason for descending to the ML-level of Isabelle is to be |
17 able to implement automatic proof procedures. Such proof procedures can |
24 able to implement automatic proof procedures. Such proof procedures can |
18 considerably lessen the burden of manual reasoning. They are centred around |
25 considerably lessen the burden of manual reasoning. They are centred around |
19 the idea of refining a goal state using tactics. This is similar to the |
26 the idea of refining a goal state using tactics. This is similar to the |
20 \isacommand{apply}-style reasoning at the user-level, where goals are |
27 \isacommand{apply}-style reasoning at the user-level, where goals are |
1579 |
1586 |
1580 text_raw {* |
1587 text_raw {* |
1581 \begin{figure}[p] |
1588 \begin{figure}[p] |
1582 \begin{boxedminipage}{\textwidth} |
1589 \begin{boxedminipage}{\textwidth} |
1583 \begin{isabelle} *} |
1590 \begin{isabelle} *} |
1584 types prm = "(nat \<times> nat) list" |
1591 type_synonym prm = "(nat \<times> nat) list" |
1585 consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet> _" [80,80] 80) |
1592 consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a" ("_ \<bullet> _" [80,80] 80) |
1586 |
1593 |
1587 overloading |
1594 overloading |
1588 perm_nat \<equiv> "perm :: prm \<Rightarrow> nat \<Rightarrow> nat" |
1595 perm_nat \<equiv> "perm :: prm \<Rightarrow> nat \<Rightarrow> nat" |
1589 perm_prod \<equiv> "perm :: prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" |
1596 perm_prod \<equiv> "perm :: prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" |
2470 let |
2477 let |
2471 val (lhs, rhs) = Thm.dest_equals (cprop_of def) |
2478 val (lhs, rhs) = Thm.dest_equals (cprop_of def) |
2472 val xs = strip_abs_vars (term_of rhs) |
2479 val xs = strip_abs_vars (term_of rhs) |
2473 val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt |
2480 val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt |
2474 |
2481 |
2475 val thy = ProofContext.theory_of ctxt' |
2482 val thy = Proof_Context.theory_of ctxt' |
2476 val cxs = map (cterm_of thy o Free) xs |
2483 val cxs = map (cterm_of thy o Free) xs |
2477 val new_lhs = Drule.list_comb (lhs, cxs) |
2484 val new_lhs = Drule.list_comb (lhs, cxs) |
2478 |
2485 |
2479 fun get_conv [] = Conv.rewr_conv def |
2486 fun get_conv [] = Conv.rewr_conv def |
2480 | get_conv (_::xs) = Conv.fun_conv (get_conv xs) |
2487 | get_conv (_::xs) = Conv.fun_conv (get_conv xs) |
2481 in |
2488 in |
2482 get_conv xs new_lhs |> |
2489 get_conv xs new_lhs |> |
2483 singleton (ProofContext.export ctxt' ctxt) |
2490 singleton (Proof_Context.export ctxt' ctxt) |
2484 end*} |
2491 end*} |
2485 |
2492 |
2486 text {* |
2493 text {* |
2487 In Line 3 we destruct the meta-equality into the @{ML_type cterm}s |
2494 In Line 3 we destruct the meta-equality into the @{ML_type cterm}s |
2488 corresponding to the left-hand and right-hand side of the meta-equality. The |
2495 corresponding to the left-hand and right-hand side of the meta-equality. The |