author | wenzelm |
Fri, 19 Dec 2014 23:01:46 +0100 | |
changeset 59159 | 9312710451f5 |
parent 47701 | 157e6108a342 |
child 59580 | cbc38731d42f |
permissions | -rw-r--r-- |
33100 | 1 |
(* Title: HOL/Tools/Function/relation.ML |
2 |
Author: Alexander Krauss, TU Muenchen |
|
3 |
||
47701 | 4 |
Tactics to start a termination proof using a user-specified relation. |
33100 | 5 |
*) |
6 |
||
7 |
signature FUNCTION_RELATION = |
|
8 |
sig |
|
40445
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
9 |
val relation_tac: Proof.context -> (typ -> term) -> int -> tactic |
47701 | 10 |
val relation_infer_tac: Proof.context -> term -> int -> tactic |
33100 | 11 |
end |
12 |
||
13 |
structure Function_Relation : FUNCTION_RELATION = |
|
14 |
struct |
|
15 |
||
40445
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
16 |
(* tactic version *) |
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
17 |
|
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
18 |
fun inst_state_tac inst st = |
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
19 |
case Term.add_vars (prop_of st) [] of |
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
20 |
[v as (_, T)] => |
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
21 |
let val cert = Thm.cterm_of (Thm.theory_of_thm st); |
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
22 |
in PRIMITIVE (Thm.instantiate ([], [(cert (Var v), cert (inst T))])) st end |
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
23 |
| _ => Seq.empty; |
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
24 |
|
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
25 |
fun relation_tac ctxt rel i = |
59159 | 26 |
TRY (Function_Common.termination_rule_tac ctxt i) |
40445
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
27 |
THEN inst_state_tac rel; |
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
28 |
|
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
29 |
|
47701 | 30 |
(* version with type inference *) |
40445
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
31 |
|
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
32 |
fun inst_state_infer_tac ctxt rel st = |
40057
b237f757b215
relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version
krauss
parents:
36636
diff
changeset
|
33 |
case Term.add_vars (prop_of st) [] of |
b237f757b215
relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version
krauss
parents:
36636
diff
changeset
|
34 |
[v as (_, T)] => |
b237f757b215
relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version
krauss
parents:
36636
diff
changeset
|
35 |
let |
42361 | 36 |
val cert = Thm.cterm_of (Proof_Context.theory_of ctxt); |
40445
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
37 |
val rel' = singleton (Variable.polymorphic ctxt) rel |
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
38 |
|> map_types Type_Infer.paramify_vars |
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
39 |
|> Type.constraint T |
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
40 |
|> Syntax.check_term ctxt |
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
41 |
|> cert; |
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
42 |
in |
65bd37d7d501
removed type-inference-like behaviour from relation_tac completely; tuned
krauss
parents:
40057
diff
changeset
|
43 |
PRIMITIVE (Thm.instantiate ([], [(cert (Var v), rel')])) st |
40057
b237f757b215
relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version
krauss
parents:
36636
diff
changeset
|
44 |
end |
b237f757b215
relation method: re-check given term with type constraints to avoid unspecific failure if ill-typed -- keep old behaviour for tactic version
krauss
parents:
36636
diff
changeset
|
45 |
| _ => Seq.empty; |
33100 | 46 |
|
47701 | 47 |
fun relation_infer_tac ctxt rel i = |
59159 | 48 |
TRY (Function_Common.termination_rule_tac ctxt i) |
47701 | 49 |
THEN inst_state_infer_tac ctxt rel; |
33100 | 50 |
|
51 |
end |