author | krauss |
Fri, 25 Feb 2011 16:59:48 +0100 | |
changeset 41846 | b368a7aee46a |
parent 41417 | 211dbd42f95d |
child 42361 | 23f352990944 |
permissions | -rw-r--r-- |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/Function/function_core.ML |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
2 |
Author: Alexander Krauss, TU Muenchen |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
3 |
|
41114 | 4 |
Core of the function package. |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
5 |
*) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
6 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
7 |
signature FUNCTION_CORE = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
8 |
sig |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
9 |
val trace: bool Unsynchronized.ref |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
10 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
11 |
val prepare_function : Function_Common.function_config |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
12 |
-> string (* defname *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
13 |
-> ((bstring * typ) * mixfix) list (* defined symbol *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
14 |
-> ((bstring * typ) list * term list * term * term) list (* specification *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
15 |
-> local_theory |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
16 |
-> (term (* f *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
17 |
* thm (* goalstate *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
18 |
* (thm -> Function_Common.function_result) (* continuation *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
19 |
) * local_theory |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
20 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
21 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
22 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
23 |
structure Function_Core : FUNCTION_CORE = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
24 |
struct |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
25 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
26 |
val trace = Unsynchronized.ref false |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
27 |
fun trace_msg msg = if ! trace then tracing (msg ()) else () |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
28 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
29 |
val boolT = HOLogic.boolT |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
30 |
val mk_eq = HOLogic.mk_eq |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
31 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
32 |
open Function_Lib |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
33 |
open Function_Common |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
34 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
35 |
datatype globals = Globals of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
36 |
{fvar: term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
37 |
domT: typ, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
38 |
ranT: typ, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
39 |
h: term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
40 |
y: term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
41 |
x: term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
42 |
z: term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
43 |
a: term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
44 |
P: term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
45 |
D: term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
46 |
Pbool:term} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
47 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
48 |
datatype rec_call_info = RCInfo of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
49 |
{RIvs: (string * typ) list, (* Call context: fixes and assumes *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
50 |
CCas: thm list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
51 |
rcarg: term, (* The recursive argument *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
52 |
llRI: thm, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
53 |
h_assum: term} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
54 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
55 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
56 |
datatype clause_context = ClauseContext of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
57 |
{ctxt : Proof.context, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
58 |
qs : term list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
59 |
gs : term list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
60 |
lhs: term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
61 |
rhs: term, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
62 |
cqs: cterm list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
63 |
ags: thm list, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
64 |
case_hyp : thm} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
65 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
66 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
67 |
fun transfer_clause_ctx thy (ClauseContext { ctxt, qs, gs, lhs, rhs, cqs, ags, case_hyp }) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
68 |
ClauseContext { ctxt = ProofContext.transfer thy ctxt, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
69 |
qs = qs, gs = gs, lhs = lhs, rhs = rhs, cqs = cqs, ags = ags, case_hyp = case_hyp } |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
70 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
71 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
72 |
datatype clause_info = ClauseInfo of |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
73 |
{no: int, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
74 |
qglr : ((string * typ) list * term list * term * term), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
75 |
cdata : clause_context, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
76 |
tree: Function_Ctx_Tree.ctx_tree, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
77 |
lGI: thm, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
78 |
RCs: rec_call_info list} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
79 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
80 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
81 |
(* Theory dependencies. *) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
82 |
val acc_induct_rule = @{thm accp_induct_rule} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
83 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
84 |
val ex1_implies_ex = @{thm FunDef.fundef_ex1_existence} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
85 |
val ex1_implies_un = @{thm FunDef.fundef_ex1_uniqueness} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
86 |
val ex1_implies_iff = @{thm FunDef.fundef_ex1_iff} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
87 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
88 |
val acc_downward = @{thm accp_downward} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
89 |
val accI = @{thm accp.accI} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
90 |
val case_split = @{thm HOL.case_split} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
91 |
val fundef_default_value = @{thm FunDef.fundef_default_value} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
92 |
val not_acc_down = @{thm not_accp_down} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
93 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
94 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
95 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
96 |
fun find_calls tree = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
97 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
98 |
fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
99 |
([], (fixes, assumes, arg) :: xs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
100 |
| add_Ri _ _ _ _ = raise Match |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
101 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
102 |
rev (Function_Ctx_Tree.traverse_tree add_Ri tree []) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
103 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
104 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
105 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
106 |
(** building proof obligations *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
107 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
108 |
fun mk_compat_proof_obligations domT ranT fvar f glrs = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
109 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
110 |
fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
111 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
112 |
val shift = incr_boundvars (length qs') |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
113 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
114 |
Logic.mk_implies |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
115 |
(HOLogic.mk_Trueprop (HOLogic.eq_const domT $ shift lhs $ lhs'), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
116 |
HOLogic.mk_Trueprop (HOLogic.eq_const ranT $ shift rhs $ rhs')) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
117 |
|> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
118 |
|> fold_rev (fn (n,T) => fn b => Term.all T $ Abs(n,T,b)) (qs @ qs') |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
119 |
|> curry abstract_over fvar |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
120 |
|> curry subst_bound f |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
121 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
122 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
123 |
map mk_impl (unordered_pairs glrs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
124 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
125 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
126 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
127 |
fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
128 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
129 |
fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
130 |
HOLogic.mk_Trueprop Pbool |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
131 |
|> curry Logic.mk_implies (HOLogic.mk_Trueprop (mk_eq (x, lhs))) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
132 |
|> fold_rev (curry Logic.mk_implies) gs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
133 |
|> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
134 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
135 |
HOLogic.mk_Trueprop Pbool |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
136 |
|> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
137 |
|> mk_forall_rename ("x", x) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
138 |
|> mk_forall_rename ("P", Pbool) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
139 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
140 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
141 |
(** making a context with it's own local bindings **) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
142 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
143 |
fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
144 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
145 |
val (qs, ctxt') = Variable.variant_fixes (map fst pre_qs) ctxt |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
146 |
|>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
147 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
148 |
val thy = ProofContext.theory_of ctxt' |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
149 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
150 |
fun inst t = subst_bounds (rev qs, t) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
151 |
val gs = map inst pre_gs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
152 |
val lhs = inst pre_lhs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
153 |
val rhs = inst pre_rhs |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
154 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
155 |
val cqs = map (cterm_of thy) qs |
36945 | 156 |
val ags = map (Thm.assume o cterm_of thy) gs |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
157 |
|
36945 | 158 |
val case_hyp = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs)))) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
159 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
160 |
ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
161 |
cqs = cqs, ags = ags, case_hyp = case_hyp } |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
162 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
163 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
164 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
165 |
(* lowlevel term function. FIXME: remove *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
166 |
fun abstract_over_list vs body = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
167 |
let |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
168 |
fun abs lev v tm = |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
169 |
if v aconv tm then Bound lev |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
170 |
else |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
171 |
(case tm of |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
172 |
Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
173 |
| t $ u => abs lev v t $ abs lev v u |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
174 |
| t => t) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
175 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
176 |
fold_index (fn (i, v) => fn t => abs i v t) vs body |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
177 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
178 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
179 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
180 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
181 |
fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
182 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
183 |
val Globals {h, ...} = globals |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
184 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
185 |
val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
186 |
val cert = Thm.cterm_of (ProofContext.theory_of ctxt) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
187 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
188 |
(* Instantiate the GIntro thm with "f" and import into the clause context. *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
189 |
val lGI = GIntro_thm |
36945 | 190 |
|> Thm.forall_elim (cert f) |
191 |
|> fold Thm.forall_elim cqs |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
192 |
|> fold Thm.elim_implies ags |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
193 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
194 |
fun mk_call_info (rcfix, rcassm, rcarg) RI = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
195 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
196 |
val llRI = RI |
36945 | 197 |
|> fold Thm.forall_elim cqs |
198 |
|> fold (Thm.forall_elim o cert o Free) rcfix |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
199 |
|> fold Thm.elim_implies ags |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
200 |
|> fold Thm.elim_implies rcassm |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
201 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
202 |
val h_assum = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
203 |
HOLogic.mk_Trueprop (G $ rcarg $ (h $ rcarg)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
204 |
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
205 |
|> fold_rev (Logic.all o Free) rcfix |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
206 |
|> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] [] |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
207 |
|> abstract_over_list (rev qs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
208 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
209 |
RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
210 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
211 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
212 |
val RC_infos = map2 mk_call_info RCs RIntro_thms |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
213 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
214 |
ClauseInfo {no=no, cdata=cdata, qglr=qglr, lGI=lGI, RCs=RC_infos, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
215 |
tree=tree} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
216 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
217 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
218 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
219 |
fun store_compat_thms 0 thms = [] |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
220 |
| store_compat_thms n thms = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
221 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
222 |
val (thms1, thms2) = chop n thms |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
223 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
224 |
(thms1 :: store_compat_thms (n - 1) thms2) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
225 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
226 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
227 |
(* expects i <= j *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
228 |
fun lookup_compat_thm i j cts = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
229 |
nth (nth cts (i - 1)) (j - i) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
230 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
231 |
(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
232 |
(* if j < i, then turn around *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
233 |
fun get_compat_thm thy cts i j ctxi ctxj = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
234 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
235 |
val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
236 |
val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
237 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
238 |
val lhsi_eq_lhsj = cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj))) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
239 |
in if j < i then |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
240 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
241 |
val compat = lookup_compat_thm j i cts |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
242 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
243 |
compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
36945 | 244 |
|> fold Thm.forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
245 |
|> fold Thm.elim_implies agsj |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
246 |
|> fold Thm.elim_implies agsi |
36945 | 247 |
|> Thm.elim_implies ((Thm.assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
248 |
end |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
249 |
else |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
250 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
251 |
val compat = lookup_compat_thm i j cts |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
252 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
253 |
compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
36945 | 254 |
|> fold Thm.forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
255 |
|> fold Thm.elim_implies agsi |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
256 |
|> fold Thm.elim_implies agsj |
36945 | 257 |
|> Thm.elim_implies (Thm.assume lhsi_eq_lhsj) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
258 |
|> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
259 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
260 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
261 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
262 |
(* Generates the replacement lemma in fully quantified form. *) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
263 |
fun mk_replacement_lemma thy h ih_elim clause = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
264 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
265 |
val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...}, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
266 |
RCs, tree, ...} = clause |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
267 |
local open Conv in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
268 |
val ih_conv = arg1_conv o arg_conv o arg_conv |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
269 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
270 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
271 |
val ih_elim_case = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
272 |
Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
273 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
274 |
val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
275 |
val h_assums = map (fn RCInfo {h_assum, ...} => |
36945 | 276 |
Thm.assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
277 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
278 |
val (eql, _) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
279 |
Function_Ctx_Tree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
280 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
281 |
val replace_lemma = (eql RS meta_eq_to_obj_eq) |
36945 | 282 |
|> Thm.implies_intr (cprop_of case_hyp) |
283 |
|> fold_rev (Thm.implies_intr o cprop_of) h_assums |
|
284 |
|> fold_rev (Thm.implies_intr o cprop_of) ags |
|
285 |
|> fold_rev Thm.forall_intr cqs |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
286 |
|> Thm.close_derivation |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
287 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
288 |
replace_lemma |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
289 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
290 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
291 |
|
33855
cd8acf137c9c
eliminated dead code and some unused bindings, reported by polyml
krauss
parents:
33766
diff
changeset
|
292 |
fun mk_uniqueness_clause thy globals compat_store clausei clausej RLj = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
293 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
294 |
val Globals {h, y, x, fvar, ...} = globals |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
295 |
val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
296 |
val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
297 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
298 |
val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
299 |
mk_clause_context x ctxti cdescj |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
300 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
301 |
val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
302 |
val compat = get_compat_thm thy compat_store i j cctxi cctxj |
36945 | 303 |
val Ghsj' = map (fn RCInfo {h_assum, ...} => Thm.assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
304 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
305 |
val RLj_import = RLj |
36945 | 306 |
|> fold Thm.forall_elim cqsj' |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
307 |
|> fold Thm.elim_implies agsj' |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
308 |
|> fold Thm.elim_implies Ghsj' |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
309 |
|
36945 | 310 |
val y_eq_rhsj'h = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (y, rhsj'h)))) |
311 |
val lhsi_eq_lhsj' = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (lhsi, lhsj')))) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
312 |
(* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
313 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
314 |
(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) |
36945 | 315 |
|> Thm.implies_elim RLj_import |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
316 |
(* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
317 |
|> (fn it => trans OF [it, compat]) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
318 |
(* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
319 |
|> (fn it => trans OF [y_eq_rhsj'h, it]) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
320 |
(* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) |
36945 | 321 |
|> fold_rev (Thm.implies_intr o cprop_of) Ghsj' |
322 |
|> fold_rev (Thm.implies_intr o cprop_of) agsj' |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
323 |
(* lhs_i = lhs_j' , y = rhs_j_h' |-- Gj', Rj1'...Rjk' ==> y = rhs_i_f *) |
36945 | 324 |
|> Thm.implies_intr (cprop_of y_eq_rhsj'h) |
325 |
|> Thm.implies_intr (cprop_of lhsi_eq_lhsj') |
|
326 |
|> fold_rev Thm.forall_intr (cterm_of thy h :: cqsj') |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
327 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
328 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
329 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
330 |
|
33855
cd8acf137c9c
eliminated dead code and some unused bindings, reported by polyml
krauss
parents:
33766
diff
changeset
|
331 |
fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
332 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
333 |
val Globals {x, y, ranT, fvar, ...} = globals |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
334 |
val ClauseInfo {cdata = ClauseContext {lhs, rhs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
335 |
val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
336 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
337 |
val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
338 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
339 |
fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) |
36945 | 340 |
|> fold_rev (Thm.implies_intr o cprop_of) CCas |
341 |
|> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
342 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
343 |
val existence = fold (curry op COMP o prep_RC) RCs lGI |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
344 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
345 |
val P = cterm_of thy (mk_eq (y, rhsC)) |
36945 | 346 |
val G_lhs_y = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (G $ lhs $ y))) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
347 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
348 |
val unique_clauses = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
349 |
map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
350 |
|
36270
fd95c0514623
tolerate eta-variants in f_graph.cases (from inductive package); added test case;
krauss
parents:
34232
diff
changeset
|
351 |
fun elim_implies_eta A AB = |
fd95c0514623
tolerate eta-variants in f_graph.cases (from inductive package); added test case;
krauss
parents:
34232
diff
changeset
|
352 |
Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single |
fd95c0514623
tolerate eta-variants in f_graph.cases (from inductive package); added test case;
krauss
parents:
34232
diff
changeset
|
353 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
354 |
val uniqueness = G_cases |
36945 | 355 |
|> Thm.forall_elim (cterm_of thy lhs) |
356 |
|> Thm.forall_elim (cterm_of thy y) |
|
357 |
|> Thm.forall_elim P |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
358 |
|> Thm.elim_implies G_lhs_y |
36270
fd95c0514623
tolerate eta-variants in f_graph.cases (from inductive package); added test case;
krauss
parents:
34232
diff
changeset
|
359 |
|> fold elim_implies_eta unique_clauses |
36945 | 360 |
|> Thm.implies_intr (cprop_of G_lhs_y) |
361 |
|> Thm.forall_intr (cterm_of thy y) |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
362 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
363 |
val P2 = cterm_of thy (lambda y (G $ lhs $ y)) (* P2 y := (lhs, y): G *) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
364 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
365 |
val exactly_one = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
366 |
ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)] |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
367 |
|> curry (op COMP) existence |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
368 |
|> curry (op COMP) uniqueness |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
369 |
|> simplify (HOL_basic_ss addsimps [case_hyp RS sym]) |
36945 | 370 |
|> Thm.implies_intr (cprop_of case_hyp) |
371 |
|> fold_rev (Thm.implies_intr o cprop_of) ags |
|
372 |
|> fold_rev Thm.forall_intr cqs |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
373 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
374 |
val function_value = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
375 |
existence |
36945 | 376 |
|> Thm.implies_intr ihyp |
377 |
|> Thm.implies_intr (cprop_of case_hyp) |
|
378 |
|> Thm.forall_intr (cterm_of thy x) |
|
379 |
|> Thm.forall_elim (cterm_of thy lhs) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
380 |
|> curry (op RS) refl |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
381 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
382 |
(exactly_one, function_value) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
383 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
384 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
385 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
386 |
fun prove_stuff ctxt globals G f R clauses complete compat compat_store G_elim f_def = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
387 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
388 |
val Globals {h, domT, ranT, x, ...} = globals |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
389 |
val thy = ProofContext.theory_of ctxt |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
390 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
391 |
(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
392 |
val ihyp = Term.all domT $ Abs ("z", domT, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
393 |
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
38558 | 394 |
HOLogic.mk_Trueprop (Const (@{const_name Ex1}, (ranT --> boolT) --> boolT) $ |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
395 |
Abs ("y", ranT, G $ Bound 1 $ Bound 0)))) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
396 |
|> cterm_of thy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
397 |
|
36945 | 398 |
val ihyp_thm = Thm.assume ihyp |> Thm.forall_elim_vars 0 |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
399 |
val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
400 |
val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
401 |
|> instantiate' [] [NONE, SOME (cterm_of thy h)] |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
402 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
403 |
val _ = trace_msg (K "Proving Replacement lemmas...") |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
404 |
val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
405 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
406 |
val _ = trace_msg (K "Proving cases for unique existence...") |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
407 |
val (ex1s, values) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
408 |
split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
409 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
410 |
val _ = trace_msg (K "Proving: Graph is a function") |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
411 |
val graph_is_function = complete |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
412 |
|> Thm.forall_elim_vars 0 |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
413 |
|> fold (curry op COMP) ex1s |
36945 | 414 |
|> Thm.implies_intr (ihyp) |
415 |
|> Thm.implies_intr (cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ x))) |
|
416 |
|> Thm.forall_intr (cterm_of thy x) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
417 |
|> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) |
36945 | 418 |
|> (fn it => fold (Thm.forall_intr o cterm_of thy o Var) (Term.add_vars (prop_of it) []) it) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
419 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
420 |
val goalstate = Conjunction.intr graph_is_function complete |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
421 |
|> Thm.close_derivation |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
422 |
|> Goal.protect |
36945 | 423 |
|> fold_rev (Thm.implies_intr o cprop_of) compat |
424 |
|> Thm.implies_intr (cprop_of complete) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
425 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
426 |
(goalstate, values) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
427 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
428 |
|
33348
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
429 |
(* wrapper -- restores quantifiers in rule specifications *) |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
430 |
fun inductive_def (binding as ((R, T), _)) intrs lthy = |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
431 |
let |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
432 |
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) = |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
433 |
lthy |
33671 | 434 |
|> Local_Theory.conceal |
33348
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
435 |
|> Inductive.add_inductive_i |
33350 | 436 |
{quiet_mode = true, |
437 |
verbose = ! trace, |
|
33348
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
438 |
alt_name = Binding.empty, |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
439 |
coind = false, |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
440 |
no_elim = false, |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
441 |
no_ind = false, |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
442 |
skip_mono = true, |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
443 |
fork_mono = false} |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
444 |
[binding] (* relation *) |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
445 |
[] (* no parameters *) |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
446 |
(map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *) |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
447 |
[] (* no special monos *) |
33671 | 448 |
||> Local_Theory.restore_naming lthy |
33348
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
449 |
|
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
450 |
val cert = cterm_of (ProofContext.theory_of lthy) |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
451 |
fun requantify orig_intro thm = |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
452 |
let |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
453 |
val (qs, t) = dest_all_all orig_intro |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
454 |
val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T) |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
455 |
val vars = Term.add_vars (prop_of thm) [] |> rev |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
456 |
val varmap = AList.lookup (op =) (frees ~~ map fst vars) |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
457 |
#> the_default ("",0) |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
458 |
in |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
459 |
fold_rev (fn Free (n, T) => |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
460 |
forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
461 |
end |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
462 |
in |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
463 |
((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy) |
33348
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
464 |
end |
bb65583ab70d
absorbed inductive_wrap function into Function_Core; more conventional argument order; tuned
krauss
parents:
33278
diff
changeset
|
465 |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
466 |
fun define_graph Gname fvar domT ranT clauses RCss lthy = |
33349 | 467 |
let |
468 |
val GT = domT --> ranT --> boolT |
|
469 |
val (Gvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Gname, GT) |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
470 |
|
33349 | 471 |
fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs = |
472 |
let |
|
473 |
fun mk_h_assm (rcfix, rcassm, rcarg) = |
|
474 |
HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg)) |
|
475 |
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm |
|
476 |
|> fold_rev (Logic.all o Free) rcfix |
|
477 |
in |
|
478 |
HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs) |
|
479 |
|> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs |
|
480 |
|> fold_rev (curry Logic.mk_implies) gs |
|
481 |
|> fold_rev Logic.all (fvar :: qs) |
|
482 |
end |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
483 |
|
33349 | 484 |
val G_intros = map2 mk_GIntro clauses RCss |
485 |
in |
|
486 |
inductive_def ((Binding.name n, T), NoSyn) G_intros lthy |
|
487 |
end |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
488 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
489 |
fun define_function fdefname (fname, mixfix) domT ranT G default lthy = |
33349 | 490 |
let |
491 |
val f_def = |
|
492 |
Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) |
|
493 |
$ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0)) |
|
494 |
|> Syntax.check_term lthy |
|
495 |
in |
|
33766
c679f05600cd
adapted Local_Theory.define -- eliminated odd thm kind;
wenzelm
parents:
33671
diff
changeset
|
496 |
Local_Theory.define |
33349 | 497 |
((Binding.name (function_name fname), mixfix), |
498 |
((Binding.conceal (Binding.name fdefname), []), f_def)) lthy |
|
499 |
end |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
500 |
|
33855
cd8acf137c9c
eliminated dead code and some unused bindings, reported by polyml
krauss
parents:
33766
diff
changeset
|
501 |
fun define_recursion_relation Rname domT qglrs clauses RCss lthy = |
33349 | 502 |
let |
503 |
val RT = domT --> domT --> boolT |
|
504 |
val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT) |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
505 |
|
33349 | 506 |
fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) = |
507 |
HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs) |
|
508 |
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm |
|
509 |
|> fold_rev (curry Logic.mk_implies) gs |
|
510 |
|> fold_rev (Logic.all o Free) rcfix |
|
511 |
|> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
|
512 |
(* "!!qs xs. CS ==> G => (r, lhs) : R" *) |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
513 |
|
33349 | 514 |
val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
515 |
|
33349 | 516 |
val ((R, RIntro_thms, R_elim, _), lthy) = |
517 |
inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy |
|
518 |
in |
|
519 |
((R, Library.unflat R_intross RIntro_thms, R_elim), lthy) |
|
520 |
end |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
521 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
522 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
523 |
fun fix_globals domT ranT fvar ctxt = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
524 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
525 |
val ([h, y, x, z, a, D, P, Pbool],ctxt') = Variable.variant_fixes |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
526 |
["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
527 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
528 |
(Globals {h = Free (h, domT --> ranT), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
529 |
y = Free (y, ranT), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
530 |
x = Free (x, domT), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
531 |
z = Free (z, domT), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
532 |
a = Free (a, domT), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
533 |
D = Free (D, domT --> boolT), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
534 |
P = Free (P, domT --> boolT), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
535 |
Pbool = Free (Pbool, boolT), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
536 |
fvar = fvar, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
537 |
domT = domT, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
538 |
ranT = ranT}, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
539 |
ctxt') |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
540 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
541 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
542 |
fun inst_RC thy fvar f (rcfix, rcassm, rcarg) = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
543 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
544 |
fun inst_term t = subst_bound(f, abstract_over (fvar, t)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
545 |
in |
36945 | 546 |
(rcfix, map (Thm.assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
547 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
548 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
549 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
550 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
551 |
(********************************************************** |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
552 |
* PROVING THE RULES |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
553 |
**********************************************************) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
554 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
555 |
fun mk_psimps thy globals R clauses valthms f_iff graph_is_function = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
556 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
557 |
val Globals {domT, z, ...} = globals |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
558 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
559 |
fun mk_psimp (ClauseInfo {qglr = (oqs, _, _, _), cdata = ClauseContext {cqs, lhs, ags, ...}, ...}) valthm = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
560 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
561 |
val lhs_acc = cterm_of thy (HOLogic.mk_Trueprop (mk_acc domT R $ lhs)) (* "acc R lhs" *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
562 |
val z_smaller = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ lhs)) (* "R z lhs" *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
563 |
in |
36945 | 564 |
((Thm.assume z_smaller) RS ((Thm.assume lhs_acc) RS acc_downward)) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
565 |
|> (fn it => it COMP graph_is_function) |
36945 | 566 |
|> Thm.implies_intr z_smaller |
567 |
|> Thm.forall_intr (cterm_of thy z) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
568 |
|> (fn it => it COMP valthm) |
36945 | 569 |
|> Thm.implies_intr lhs_acc |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
570 |
|> asm_simplify (HOL_basic_ss addsimps [f_iff]) |
36945 | 571 |
|> fold_rev (Thm.implies_intr o cprop_of) ags |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
572 |
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
573 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
574 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
575 |
map2 mk_psimp clauses valthms |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
576 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
577 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
578 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
579 |
(** Induction rule **) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
580 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
581 |
|
34065
6f8f9835e219
moved predicate rules to Predicate.thy; weakened default dest rule predicate1D (is not that reliable wrt. sets)
haftmann
parents:
33855
diff
changeset
|
582 |
val acc_subset_induct = @{thm predicate1I} RS @{thm accp_subset_induct} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
583 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
584 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
585 |
fun mk_partial_induct_rule thy globals R complete_thm clauses = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
586 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
587 |
val Globals {domT, x, z, a, P, D, ...} = globals |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
588 |
val acc_R = mk_acc domT R |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
589 |
|
36945 | 590 |
val x_D = Thm.assume (cterm_of thy (HOLogic.mk_Trueprop (D $ x))) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
591 |
val a_D = cterm_of thy (HOLogic.mk_Trueprop (D $ a)) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
592 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
593 |
val D_subset = cterm_of thy (Logic.all x |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
594 |
(Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), HOLogic.mk_Trueprop (acc_R $ x)))) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
595 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
596 |
val D_dcl = (* "!!x z. [| x: D; (z,x):R |] ==> z:D" *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
597 |
Logic.all x (Logic.all z (Logic.mk_implies (HOLogic.mk_Trueprop (D $ x), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
598 |
Logic.mk_implies (HOLogic.mk_Trueprop (R $ z $ x), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
599 |
HOLogic.mk_Trueprop (D $ z))))) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
600 |
|> cterm_of thy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
601 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
602 |
(* Inductive Hypothesis: !!z. (z,x):R ==> P z *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
603 |
val ihyp = Term.all domT $ Abs ("z", domT, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
604 |
Logic.mk_implies (HOLogic.mk_Trueprop (R $ Bound 0 $ x), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
605 |
HOLogic.mk_Trueprop (P $ Bound 0))) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
606 |
|> cterm_of thy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
607 |
|
36945 | 608 |
val aihyp = Thm.assume ihyp |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
609 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
610 |
fun prove_case clause = |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
611 |
let |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
612 |
val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
613 |
RCs, qglr = (oqs, _, _, _), ...} = clause |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
614 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
615 |
val case_hyp_conv = K (case_hyp RS eq_reflection) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
616 |
local open Conv in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
617 |
val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
618 |
val sih = |
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36270
diff
changeset
|
619 |
fconv_rule (Conv.binder_conv |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
620 |
(K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
621 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
622 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
623 |
fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) = sih |
36945 | 624 |
|> Thm.forall_elim (cterm_of thy rcarg) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
625 |
|> Thm.elim_implies llRI |
36945 | 626 |
|> fold_rev (Thm.implies_intr o cprop_of) CCas |
627 |
|> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
628 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
629 |
val P_recs = map mk_Prec RCs (* [P rec1, P rec2, ... ] *) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
630 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
631 |
val step = HOLogic.mk_Trueprop (P $ lhs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
632 |
|> fold_rev (curry Logic.mk_implies o prop_of) P_recs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
633 |
|> fold_rev (curry Logic.mk_implies) gs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
634 |
|> curry Logic.mk_implies (HOLogic.mk_Trueprop (D $ lhs)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
635 |
|> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
636 |
|> cterm_of thy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
637 |
|
36945 | 638 |
val P_lhs = Thm.assume step |
639 |
|> fold Thm.forall_elim cqs |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
640 |
|> Thm.elim_implies lhs_D |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
641 |
|> fold Thm.elim_implies ags |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
642 |
|> fold Thm.elim_implies P_recs |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
643 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
644 |
val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
645 |
|> Conv.arg_conv (Conv.arg_conv case_hyp_conv) |
36945 | 646 |
|> Thm.symmetric (* P lhs == P x *) |
647 |
|> (fn eql => Thm.equal_elim eql P_lhs) (* "P x" *) |
|
648 |
|> Thm.implies_intr (cprop_of case_hyp) |
|
649 |
|> fold_rev (Thm.implies_intr o cprop_of) ags |
|
650 |
|> fold_rev Thm.forall_intr cqs |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
651 |
in |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
652 |
(res, step) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
653 |
end |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
654 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
655 |
val (cases, steps) = split_list (map prove_case clauses) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
656 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
657 |
val istep = complete_thm |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
658 |
|> Thm.forall_elim_vars 0 |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
659 |
|> fold (curry op COMP) cases (* P x *) |
36945 | 660 |
|> Thm.implies_intr ihyp |
661 |
|> Thm.implies_intr (cprop_of x_D) |
|
662 |
|> Thm.forall_intr (cterm_of thy x) |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
663 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
664 |
val subset_induct_rule = |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
665 |
acc_subset_induct |
36945 | 666 |
|> (curry op COMP) (Thm.assume D_subset) |
667 |
|> (curry op COMP) (Thm.assume D_dcl) |
|
668 |
|> (curry op COMP) (Thm.assume a_D) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
669 |
|> (curry op COMP) istep |
36945 | 670 |
|> fold_rev Thm.implies_intr steps |
671 |
|> Thm.implies_intr a_D |
|
672 |
|> Thm.implies_intr D_dcl |
|
673 |
|> Thm.implies_intr D_subset |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
674 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
675 |
val simple_induct_rule = |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
676 |
subset_induct_rule |
36945 | 677 |
|> Thm.forall_intr (cterm_of thy D) |
678 |
|> Thm.forall_elim (cterm_of thy acc_R) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
679 |
|> assume_tac 1 |> Seq.hd |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
680 |
|> (curry op COMP) (acc_downward |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
681 |
|> (instantiate' [SOME (ctyp_of thy domT)] |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
682 |
(map (SOME o cterm_of thy) [R, x, z])) |
36945 | 683 |
|> Thm.forall_intr (cterm_of thy z) |
684 |
|> Thm.forall_intr (cterm_of thy x)) |
|
685 |
|> Thm.forall_intr (cterm_of thy a) |
|
686 |
|> Thm.forall_intr (cterm_of thy P) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
687 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
688 |
simple_induct_rule |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
689 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
690 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
691 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
692 |
(* FIXME: broken by design *) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
693 |
fun mk_domain_intro ctxt (Globals {domT, ...}) R R_cases clause = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
694 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
695 |
val thy = ProofContext.theory_of ctxt |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
696 |
val ClauseInfo {cdata = ClauseContext {gs, lhs, cqs, ...}, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
697 |
qglr = (oqs, _, _, _), ...} = clause |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
698 |
val goal = HOLogic.mk_Trueprop (mk_acc domT R $ lhs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
699 |
|> fold_rev (curry Logic.mk_implies) gs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
700 |
|> cterm_of thy |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
701 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
702 |
Goal.init goal |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
703 |
|> (SINGLE (resolve_tac [accI] 1)) |> the |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
704 |
|> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
705 |
|> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
706 |
|> Goal.conclude |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
707 |
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
708 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
709 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
710 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
711 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
712 |
(** Termination rule **) |
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
713 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
714 |
val wf_induct_rule = @{thm Wellfounded.wfP_induct_rule} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
715 |
val wf_in_rel = @{thm FunDef.wf_in_rel} |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
716 |
val in_rel_def = @{thm FunDef.in_rel_def} |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
717 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
718 |
fun mk_nest_term_case thy globals R' ihyp clause = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
719 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
720 |
val Globals {z, ...} = globals |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
721 |
val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, lhs, case_hyp, ...}, tree, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
722 |
qglr=(oqs, _, _, _), ...} = clause |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
723 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
724 |
val ih_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ihyp |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
725 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
726 |
fun step (fixes, assumes) (_ $ arg) u (sub,(hyps,thms)) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
727 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
728 |
val used = (u @ sub) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
729 |
|> map (fn (ctx,thm) => Function_Ctx_Tree.export_thm thy ctx thm) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
730 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
731 |
val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
732 |
|> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
733 |
|> Function_Ctx_Tree.export_term (fixes, assumes) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
734 |
|> fold_rev (curry Logic.mk_implies o prop_of) ags |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
735 |
|> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
736 |
|> cterm_of thy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
737 |
|
36945 | 738 |
val thm = Thm.assume hyp |
739 |
|> fold Thm.forall_elim cqs |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
740 |
|> fold Thm.elim_implies ags |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
741 |
|> Function_Ctx_Tree.import_thm thy (fixes, assumes) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
742 |
|> fold Thm.elim_implies used (* "(arg, lhs) : R'" *) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
743 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
744 |
val z_eq_arg = HOLogic.mk_Trueprop (mk_eq (z, arg)) |
36945 | 745 |
|> cterm_of thy |> Thm.assume |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
746 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
747 |
val acc = thm COMP ih_case |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
748 |
val z_acc_local = acc |
36945 | 749 |
|> Conv.fconv_rule |
750 |
(Conv.arg_conv (Conv.arg_conv (K (Thm.symmetric (z_eq_arg RS eq_reflection))))) |
|
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
751 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
752 |
val ethm = z_acc_local |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
753 |
|> Function_Ctx_Tree.export_thm thy (fixes, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
754 |
z_eq_arg :: case_hyp :: ags @ assumes) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
755 |
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
756 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
757 |
val sub' = sub @ [(([],[]), acc)] |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
758 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
759 |
(sub', (hyp :: hyps, ethm :: thms)) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
760 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
761 |
| step _ _ _ _ = raise Match |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
762 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
763 |
Function_Ctx_Tree.traverse_tree step tree |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
764 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
765 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
766 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
767 |
fun mk_nest_term_rule thy globals R R_cases clauses = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
768 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
769 |
val Globals { domT, x, z, ... } = globals |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
770 |
val acc_R = mk_acc domT R |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
771 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
772 |
val R' = Free ("R", fastype_of R) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
773 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
774 |
val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT))) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
775 |
val inrel_R = Const (@{const_name FunDef.in_rel}, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
776 |
HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
777 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
778 |
val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP}, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
779 |
(domT --> domT --> boolT) --> boolT) $ R') |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
780 |
|> cterm_of thy (* "wf R'" *) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
781 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
782 |
(* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
783 |
val ihyp = Term.all domT $ Abs ("z", domT, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
784 |
Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x), |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
785 |
HOLogic.mk_Trueprop (acc_R $ Bound 0))) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
786 |
|> cterm_of thy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
787 |
|
36945 | 788 |
val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0 |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
789 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
790 |
val R_z_x = cterm_of thy (HOLogic.mk_Trueprop (R $ z $ x)) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
791 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
792 |
val (hyps, cases) = fold (mk_nest_term_case thy globals R' ihyp_a) clauses ([], []) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
793 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
794 |
R_cases |
36945 | 795 |
|> Thm.forall_elim (cterm_of thy z) |
796 |
|> Thm.forall_elim (cterm_of thy x) |
|
797 |
|> Thm.forall_elim (cterm_of thy (acc_R $ z)) |
|
798 |
|> curry op COMP (Thm.assume R_z_x) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
799 |
|> fold_rev (curry op COMP) cases |
36945 | 800 |
|> Thm.implies_intr R_z_x |
801 |
|> Thm.forall_intr (cterm_of thy z) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
802 |
|> (fn it => it COMP accI) |
36945 | 803 |
|> Thm.implies_intr ihyp |
804 |
|> Thm.forall_intr (cterm_of thy x) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
805 |
|> (fn it => Drule.compose_single(it,2,wf_induct_rule)) |
36945 | 806 |
|> curry op RS (Thm.assume wfR') |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
807 |
|> forall_intr_vars |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
808 |
|> (fn it => it COMP allI) |
36945 | 809 |
|> fold Thm.implies_intr hyps |
810 |
|> Thm.implies_intr wfR' |
|
811 |
|> Thm.forall_intr (cterm_of thy R') |
|
812 |
|> Thm.forall_elim (cterm_of thy (inrel_R)) |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
813 |
|> curry op RS wf_in_rel |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
814 |
|> full_simplify (HOL_basic_ss addsimps [in_rel_def]) |
36945 | 815 |
|> Thm.forall_intr (cterm_of thy Rrel) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
816 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
817 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
818 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
819 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
820 |
fun prepare_function config defname [((fname, fT), mixfix)] abstract_qglrs lthy = |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
821 |
let |
41846
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
822 |
val FunctionConfig {domintros, default=default_opt, ...} = config |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
823 |
|
41417 | 824 |
val default_str = the_default "%x. undefined" default_opt (*FIXME dynamic scoping*) |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
825 |
val fvar = Free (fname, fT) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
826 |
val domT = domain_type fT |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
827 |
val ranT = range_type fT |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
828 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
829 |
val default = Syntax.parse_term lthy default_str |
39288 | 830 |
|> Type.constraint fT |> Syntax.check_term lthy |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
831 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
832 |
val (globals, ctxt') = fix_globals domT ranT fvar lthy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
833 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
834 |
val Globals { x, h, ... } = globals |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
835 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
836 |
val clauses = map (mk_clause_context x ctxt') abstract_qglrs |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
837 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
838 |
val n = length abstract_qglrs |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
839 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
840 |
fun build_tree (ClauseContext { ctxt, rhs, ...}) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
841 |
Function_Ctx_Tree.mk_tree (fname, fT) h ctxt rhs |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
842 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
843 |
val trees = map build_tree clauses |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
844 |
val RCss = map find_calls trees |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
845 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
846 |
val ((G, GIntro_thms, G_elim, G_induct), lthy) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
847 |
PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
848 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
849 |
val ((f, (_, f_defthm)), lthy) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
850 |
PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
851 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
852 |
val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
853 |
val trees = map (Function_Ctx_Tree.inst_tree (ProofContext.theory_of lthy) fvar f) trees |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
854 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
855 |
val ((R, RIntro_thmss, R_elim), lthy) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
856 |
PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
857 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
858 |
val (_, lthy) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
859 |
Local_Theory.abbrev Syntax.mode_default ((Binding.name (dom_name defname), NoSyn), mk_acc domT R) lthy |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
860 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
861 |
val newthy = ProofContext.theory_of lthy |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
862 |
val clauses = map (transfer_clause_ctx newthy) clauses |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
863 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
864 |
val cert = cterm_of (ProofContext.theory_of lthy) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
865 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
866 |
val xclauses = PROFILE "xclauses" |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
867 |
(map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
868 |
RCss GIntro_thms) RIntro_thmss |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
869 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
870 |
val complete = |
36945 | 871 |
mk_completeness globals clauses abstract_qglrs |> cert |> Thm.assume |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
872 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
873 |
val compat = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
874 |
mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |
36945 | 875 |
|> map (cert #> Thm.assume) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
876 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
877 |
val compat_store = store_compat_thms n compat |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
878 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
879 |
val (goalstate, values) = PROFILE "prove_stuff" |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
880 |
(prove_stuff lthy globals G f R xclauses complete compat |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
881 |
compat_store G_elim) f_defthm |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
882 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
883 |
fun mk_partial_rules provedgoal = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
884 |
let |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
885 |
val newthy = theory_of_thm provedgoal (*FIXME*) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
886 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
887 |
val (graph_is_function, complete_thm) = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
888 |
provedgoal |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
889 |
|> Conjunction.elim |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
890 |
|> apfst (Thm.forall_elim_vars 0) |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
891 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
892 |
val f_iff = graph_is_function RS (f_defthm RS ex1_implies_iff) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
893 |
|
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
894 |
val psimps = PROFILE "Proving simplification rules" |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
895 |
(mk_psimps newthy globals R xclauses values f_iff) graph_is_function |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
896 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
897 |
val simple_pinduct = PROFILE "Proving partial induction rule" |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
898 |
(mk_partial_induct_rule newthy globals R complete_thm) xclauses |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
899 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
900 |
val total_intro = PROFILE "Proving nested termination rule" |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
901 |
(mk_nest_term_rule newthy globals R R_elim) xclauses |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
902 |
|
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
903 |
val dom_intros = |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
904 |
if domintros then SOME (PROFILE "Proving domain introduction rules" |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
905 |
(map (mk_domain_intro lthy globals R R_elim)) xclauses) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
906 |
else NONE |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
907 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
908 |
FunctionResult {fs=[f], G=G, R=R, cases=complete_thm, |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
909 |
psimps=psimps, simple_pinducts=[simple_pinduct], |
41846
b368a7aee46a
removed support for tail-recursion from function package (now implemented by partial_function)
krauss
parents:
41417
diff
changeset
|
910 |
termination=total_intro, domintros=dom_intros} |
34232
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
911 |
end |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
912 |
in |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
913 |
((f, goalstate, mk_partial_rules), lthy) |
36a2a3029fd3
new year's resolution: reindented code in function package
krauss
parents:
34065
diff
changeset
|
914 |
end |
33099
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
915 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
916 |
|
b8cdd3d73022
function package: more standard names for structures and files
krauss
parents:
diff
changeset
|
917 |
end |