author | krauss |
Thu, 21 Sep 2006 12:22:05 +0200 | |
changeset 20654 | d80502f0d701 |
parent 20536 | f088edff8af8 |
child 20797 | c1f0bc7e7d80 |
permissions | -rw-r--r-- |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
1 |
(* Title: HOL/Tools/function_package/fundef_prep.ML |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
2 |
ID: $Id$ |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
3 |
Author: Alexander Krauss, TU Muenchen |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
4 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
5 |
A package for general recursive function definitions. |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
6 |
Preparation step: makes auxiliary definitions and generates |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
7 |
proof obligations. |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
8 |
*) |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
9 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
10 |
signature FUNDEF_PREP = |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
11 |
sig |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
12 |
val prepare_fundef : string (* defname *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
13 |
-> (string * typ * mixfix) (* defined symbol *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
14 |
-> ((string * typ) list * term list * term * term) list (* specification *) |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
15 |
-> string (* default_value, not parsed yet *) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
16 |
-> local_theory |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
17 |
-> FundefCommon.prep_result * term * local_theory |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19583
diff
changeset
|
18 |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
19 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
20 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
21 |
structure FundefPrep : FUNDEF_PREP = |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
22 |
struct |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
23 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
24 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
25 |
open FundefCommon |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
26 |
open FundefAbbrev |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
27 |
|
19922 | 28 |
(* Theory dependencies. *) |
29 |
val Pair_inject = thm "Product_Type.Pair_inject"; |
|
30 |
||
31 |
val acc_induct_rule = thm "Accessible_Part.acc_induct_rule" |
|
32 |
||
33 |
val ex1_implies_ex = thm "FunDef.fundef_ex1_existence" |
|
34 |
val ex1_implies_un = thm "FunDef.fundef_ex1_uniqueness" |
|
35 |
val ex1_implies_iff = thm "FunDef.fundef_ex1_iff" |
|
36 |
||
37 |
val conjunctionI = thm "conjunctionI"; |
|
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
38 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
39 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
40 |
|
19922 | 41 |
fun find_calls tree = |
42 |
let |
|
43 |
fun add_Ri (fixes,assumes) (_ $ arg) _ (_, xs) = ([], (fixes, assumes, arg) :: xs) |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
44 |
| add_Ri _ _ _ _ = raise Match |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
45 |
in |
19922 | 46 |
rev (FundefCtxTree.traverse_tree add_Ri tree []) |
47 |
end |
|
48 |
||
49 |
||
50 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
51 |
(* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
52 |
(* Takes bound form of qglrs tuples *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
53 |
fun mk_compat_impl domT ranT fvar f ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) = |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
54 |
let |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
55 |
val shift = incr_boundvars (length qs') |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
56 |
in |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
57 |
(implies $ Trueprop (eq_const domT $ shift lhs $ lhs') |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
58 |
$ Trueprop (eq_const ranT $ shift rhs $ rhs')) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
59 |
|> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
60 |
|> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs') |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
61 |
|> curry abstract_over fvar |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
62 |
|> curry subst_bound f |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
63 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
64 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
65 |
fun mk_compat_proof_obligations domT ranT fvar f glrs = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
66 |
map (mk_compat_impl domT ranT fvar f) (unordered_pairs glrs) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
67 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
68 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
69 |
fun mk_completeness globals clauses qglrs = |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
70 |
let |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
71 |
val Globals {x, Pbool, ...} = globals |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
72 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
73 |
fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = Trueprop Pbool |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
74 |
|> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs))) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
75 |
|> fold_rev (curry Logic.mk_implies) gs |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
76 |
|> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
77 |
in |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
78 |
Trueprop Pbool |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
79 |
|> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
80 |
|> mk_forall_rename ("x", x) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
81 |
|> mk_forall_rename ("P", Pbool) |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
82 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
83 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
84 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
85 |
fun mk_clause_context x ctxt (pre_qs,pre_gs,pre_lhs,pre_rhs) = |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
86 |
let |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
87 |
val (qs, ctxt') = Variable.invent_fixes (map fst pre_qs) ctxt |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
88 |
|>> map2 (fn (_, T) => fn n => Free (n, T)) pre_qs |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
89 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
90 |
val thy = ProofContext.theory_of ctxt' |
19922 | 91 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
92 |
fun inst t = subst_bounds (rev qs, t) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
93 |
val gs = map inst pre_gs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
94 |
val lhs = inst pre_lhs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
95 |
val rhs = inst pre_rhs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
96 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
97 |
val cqs = map (cterm_of thy) qs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
98 |
val ags = map (assume o cterm_of thy) gs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
99 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
100 |
val case_hyp = assume (cterm_of thy (Trueprop (mk_eq (x, lhs)))) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
101 |
in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
102 |
ClauseContext { ctxt = ctxt', qs = qs, gs = gs, lhs = lhs, rhs = rhs, |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
103 |
cqs = cqs, ags = ags, case_hyp = case_hyp } |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
104 |
end |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
105 |
|
19922 | 106 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
107 |
(* lowlevel term function *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
108 |
fun abstract_over_list vs body = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
109 |
let |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
110 |
exception SAME; |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
111 |
fun abs lev v tm = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
112 |
if v aconv tm then Bound lev |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
113 |
else |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
114 |
(case tm of |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
115 |
Abs (a, T, t) => Abs (a, T, abs (lev + 1) v t) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
116 |
| t $ u => (abs lev v t $ (abs lev v u handle SAME => u) handle SAME => t $ abs lev v u) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
117 |
| _ => raise SAME); |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
118 |
in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
119 |
fold_index (fn (i,v) => fn t => abs i v t handle SAME => t) vs body |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
120 |
end |
19922 | 121 |
|
122 |
||
123 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
124 |
fun mk_clause_info globals G f no cdata qglr tree RCs GIntro_thm RIntro_thms = |
19922 | 125 |
let |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
126 |
val Globals {h, fvar, x, ...} = globals |
19922 | 127 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
128 |
val ClauseContext { ctxt, qs, cqs, ags, ... } = cdata |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
129 |
val cert = Thm.cterm_of (ProofContext.theory_of ctxt) |
19922 | 130 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
131 |
(* Instantiate the GIntro thm with "f" and import into the clause context. *) |
19922 | 132 |
val lGI = GIntro_thm |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
133 |
|> forall_elim (cert f) |
19922 | 134 |
|> fold forall_elim cqs |
135 |
|> fold implies_elim_swp ags |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
136 |
|
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
137 |
fun mk_call_info (rcfix, rcassm, rcarg) RI = |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
138 |
let |
19922 | 139 |
val llRI = RI |
140 |
|> fold forall_elim cqs |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
141 |
|> fold (forall_elim o cert o Free) rcfix |
19922 | 142 |
|> fold implies_elim_swp ags |
143 |
|> fold implies_elim_swp rcassm |
|
144 |
||
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
145 |
val h_assum = |
19922 | 146 |
mk_relmem (rcarg, h $ rcarg) G |
147 |
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm |
|
148 |
|> fold_rev (mk_forall o Free) rcfix |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
149 |
|> Pattern.rewrite_term (ProofContext.theory_of ctxt) [(f, h)] [] |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
150 |
|> abstract_over_list (rev qs) |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
151 |
in |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
152 |
RCInfo {RIvs=rcfix, rcarg=rcarg, CCas=rcassm, llRI=llRI, h_assum=h_assum} |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
153 |
end |
19922 | 154 |
|
155 |
val RC_infos = map2 mk_call_info RCs RIntro_thms |
|
156 |
in |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
157 |
ClauseInfo |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
158 |
{ |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
159 |
no=no, |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
160 |
cdata=cdata, |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
161 |
qglr=qglr, |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
162 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
163 |
lGI=lGI, |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
164 |
RCs=RC_infos, |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
165 |
tree=tree |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
166 |
} |
19922 | 167 |
end |
168 |
||
169 |
||
170 |
||
171 |
||
172 |
||
173 |
||
174 |
||
175 |
(* replace this by a table later*) |
|
176 |
fun store_compat_thms 0 thms = [] |
|
177 |
| store_compat_thms n thms = |
|
178 |
let |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
179 |
val (thms1, thms2) = chop n thms |
19922 | 180 |
in |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
181 |
(thms1 :: store_compat_thms (n - 1) thms2) |
19922 | 182 |
end |
183 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
184 |
(* expects i <= j *) |
19922 | 185 |
fun lookup_compat_thm i j cts = |
186 |
nth (nth cts (i - 1)) (j - i) |
|
187 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
188 |
(* Returns "Gsi, Gsj, lhs_i = lhs_j |-- rhs_j_f = rhs_i_f" *) |
19922 | 189 |
(* if j < i, then turn around *) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
190 |
fun get_compat_thm thy cts i j ctxi ctxj = |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
191 |
let |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
192 |
val ClauseContext {cqs=cqsi,ags=agsi,lhs=lhsi,...} = ctxi |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
193 |
val ClauseContext {cqs=cqsj,ags=agsj,lhs=lhsj,...} = ctxj |
19922 | 194 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
195 |
val lhsi_eq_lhsj = cterm_of thy (Trueprop (mk_eq (lhsi, lhsj))) |
19922 | 196 |
in if j < i then |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
197 |
let |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
198 |
val compat = lookup_compat_thm j i cts |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
199 |
in |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
200 |
compat (* "!!qj qi. Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
201 |
|> fold forall_elim (cqsj @ cqsi) (* "Gsj => Gsi => lhsj = lhsi ==> rhsj = rhsi" *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
202 |
|> fold implies_elim_swp agsj |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
203 |
|> fold implies_elim_swp agsi |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
204 |
|> implies_elim_swp ((assume lhsi_eq_lhsj) RS sym) (* "Gsj, Gsi, lhsi = lhsj |-- rhsj = rhsi" *) |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
205 |
end |
19922 | 206 |
else |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
207 |
let |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
208 |
val compat = lookup_compat_thm i j cts |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
209 |
in |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
210 |
compat (* "!!qi qj. Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
211 |
|> fold forall_elim (cqsi @ cqsj) (* "Gsi => Gsj => lhsi = lhsj ==> rhsi = rhsj" *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
212 |
|> fold implies_elim_swp agsi |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
213 |
|> fold implies_elim_swp agsj |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
214 |
|> implies_elim_swp (assume lhsi_eq_lhsj) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
215 |
|> (fn thm => thm RS sym) (* "Gsi, Gsj, lhsi = lhsj |-- rhsj = rhsi" *) |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
216 |
end |
19564
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
217 |
end |
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
218 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
219 |
|
d3e2f532459a
First usable version of the new function definition package (HOL/function_packake/...).
krauss
parents:
diff
changeset
|
220 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
221 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
222 |
(* Generates the replacement lemma in fully quantified form. *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
223 |
fun mk_replacement_lemma thy h ih_elim clause = |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
224 |
let |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
225 |
val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause |
19922 | 226 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
227 |
val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim |
19922 | 228 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
229 |
val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
230 |
val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs |
19922 | 231 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
232 |
val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *) |
19922 | 233 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
234 |
val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case_inst (Ris ~~ h_assums) tree |
19922 | 235 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
236 |
val replace_lemma = (eql RS meta_eq_to_obj_eq) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
237 |
|> implies_intr (cprop_of case_hyp) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
238 |
|> fold_rev (implies_intr o cprop_of) h_assums |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
239 |
|> fold_rev (implies_intr o cprop_of) ags |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
240 |
|> fold_rev forall_intr cqs |
19922 | 241 |
in |
242 |
replace_lemma |
|
243 |
end |
|
244 |
||
245 |
||
246 |
||
247 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
248 |
fun pr (s:string) x = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
249 |
let val _ = print s |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
250 |
in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
251 |
x |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
252 |
end |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
253 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
254 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
255 |
fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj = |
19922 | 256 |
let |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
257 |
val Globals {h, y, x, fvar, ...} = globals |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
258 |
val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
259 |
val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
260 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
261 |
val cctxj as ClauseContext {ags = agsj', lhs = lhsj', rhs = rhsj', qs = qsj', cqs = cqsj', ...} |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
262 |
= mk_clause_context x ctxti cdescj |
19922 | 263 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
264 |
val rhsj'h = Pattern.rewrite_term thy [(fvar,h)] [] rhsj' |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
265 |
val compat = get_compat_thm thy compat_store i j cctxi cctxj |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
266 |
val Ghsj' = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qsj', h_assum)))) RCsj |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
267 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
268 |
val RLj_import = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
269 |
RLj |> fold forall_elim cqsj' |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
270 |
|> fold implies_elim_swp agsj' |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
271 |
|> fold implies_elim_swp Ghsj' |
19922 | 272 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
273 |
val y_eq_rhsj'h = assume (cterm_of thy (Trueprop (mk_eq (y, rhsj'h)))) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
274 |
val lhsi_eq_lhsj' = assume (cterm_of thy (Trueprop (mk_eq (lhsi, lhsj')))) (* lhs_i = lhs_j' |-- lhs_i = lhs_j' *) |
19922 | 275 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
276 |
val eq_pairs = assume (cterm_of thy (Trueprop (mk_eq (mk_prod (lhsi, y), mk_prod (lhsj',rhsj'h))))) |
19922 | 277 |
in |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
278 |
(trans OF [case_hyp, lhsi_eq_lhsj']) (* lhs_i = lhs_j' |-- x = lhs_j' *) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
279 |
|> implies_elim RLj_import (* Rj1' ... Rjk', lhs_i = lhs_j' |-- rhs_j'_h = rhs_j'_f *) |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
280 |
|> (fn it => trans OF [it, compat]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk' |-- rhs_j'_h = rhs_i_f *) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
281 |
|> (fn it => trans OF [y_eq_rhsj'h, it]) (* lhs_i = lhs_j', Gj', Rj1' ... Rjk', y = rhs_j_h' |-- y = rhs_i_f *) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
282 |
|> implies_intr (cprop_of y_eq_rhsj'h) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
283 |
|> implies_intr (cprop_of lhsi_eq_lhsj') (* Gj', Rj1' ... Rjk' |-- [| lhs_i = lhs_j', y = rhs_j_h' |] ==> y = rhs_i_f *) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
284 |
|> (fn it => Drule.compose_single(it, 2, Pair_inject)) (* Gj', Rj1' ... Rjk' |-- (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
285 |
|> implies_elim_swp eq_pairs |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
286 |
|> fold_rev (implies_intr o cprop_of) Ghsj' |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
287 |
|> fold_rev (implies_intr o cprop_of) agsj' (* Gj', Rj1', ..., Rjk' ==> (lhs_i, y) = (lhs_j', rhs_j_h') ==> y = rhs_i_f *) |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
288 |
|> implies_intr (cprop_of eq_pairs) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
289 |
|> fold_rev forall_intr (cterm_of thy h :: cqsj') |
19922 | 290 |
end |
291 |
||
292 |
||
293 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
294 |
fun mk_uniqueness_case thy globals G f ihyp ih_intro G_cases compat_store clauses rep_lemmas clausei = |
19922 | 295 |
let |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
296 |
val Globals {x, y, ranT, fvar, ...} = globals |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
297 |
val ClauseInfo {cdata = ClauseContext {lhs, rhs, qs, cqs, ags, case_hyp, ...}, lGI, RCs, ...} = clausei |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
298 |
val rhsC = Pattern.rewrite_term thy [(fvar, f)] [] rhs |
19922 | 299 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
300 |
val ih_intro_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_intro |
19922 | 301 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
302 |
fun prep_RC (RCInfo {llRI, RIvs, CCas, ...}) = (llRI RS ih_intro_case) |
19922 | 303 |
|> fold_rev (implies_intr o cprop_of) CCas |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
304 |
|> fold_rev (forall_intr o cterm_of thy o Free) RIvs |
19922 | 305 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
306 |
val existence = fold (curry op COMP o prep_RC) RCs lGI |
19922 | 307 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
308 |
val a = cterm_of thy (mk_prod (lhs, y)) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
309 |
val P = cterm_of thy (mk_eq (y, rhsC)) |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
310 |
val a_in_G = assume (cterm_of thy (Trueprop (mk_mem (term_of a, G)))) |
19922 | 311 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
312 |
val unique_clauses = map2 (mk_uniqueness_clause thy globals f compat_store clausei) clauses rep_lemmas |
19922 | 313 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
314 |
val uniqueness = G_cases |
19922 | 315 |
|> forall_elim a |
316 |
|> forall_elim P |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
317 |
|> implies_elim_swp a_in_G |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
318 |
|> fold implies_elim_swp unique_clauses |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
319 |
|> implies_intr (cprop_of a_in_G) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
320 |
|> forall_intr (cterm_of thy y) |
19922 | 321 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
322 |
val P2 = cterm_of thy (lambda y (mk_mem (mk_prod (lhs, y), G))) (* P2 y := (lhs, y): G *) |
19922 | 323 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
324 |
val exactly_one = |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
325 |
ex1I |> instantiate' [SOME (ctyp_of thy ranT)] [SOME P2, SOME (cterm_of thy rhsC)] |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
326 |
|> curry (op COMP) existence |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
327 |
|> curry (op COMP) uniqueness |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
328 |
|> simplify (HOL_basic_ss addsimps [case_hyp RS sym]) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
329 |
|> implies_intr (cprop_of case_hyp) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
330 |
|> fold_rev (implies_intr o cprop_of) ags |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
331 |
|> fold_rev forall_intr cqs |
19922 | 332 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
333 |
val function_value = |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
334 |
existence |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
335 |
|> implies_intr ihyp |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
336 |
|> implies_intr (cprop_of case_hyp) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
337 |
|> forall_intr (cterm_of thy x) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
338 |
|> forall_elim (cterm_of thy lhs) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
339 |
|> curry (op RS) refl |
19922 | 340 |
in |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
341 |
(exactly_one, function_value) |
19922 | 342 |
end |
343 |
||
344 |
||
345 |
||
346 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
347 |
fun prove_stuff thy congs globals G f R clauses complete compat compat_store G_elim f_def = |
19922 | 348 |
let |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
349 |
val Globals {h, domT, ranT, x, ...} = globals |
19922 | 350 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
351 |
val inst_ex1_ex = f_def RS ex1_implies_ex |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
352 |
val inst_ex1_un = f_def RS ex1_implies_un |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
353 |
val inst_ex1_iff = f_def RS ex1_implies_iff |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
354 |
|
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
355 |
(* Inductive Hypothesis: !!z. (z,x):R ==> EX!y. (z,y):G *) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
356 |
val ihyp = all domT $ Abs ("z", domT, |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
357 |
implies $ Trueprop (mk_relmemT domT domT (Bound 0, x) R) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
358 |
$ Trueprop (Const ("Ex1", (ranT --> boolT) --> boolT) $ |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
359 |
Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G))) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
360 |
|> cterm_of thy |
19922 | 361 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
362 |
val ihyp_thm = assume ihyp |> forall_elim_vars 0 |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
363 |
val ih_intro = ihyp_thm RS inst_ex1_ex |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
364 |
val ih_elim = ihyp_thm RS inst_ex1_un |
19922 | 365 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
366 |
val _ = Output.debug "Proving Replacement lemmas..." |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
367 |
val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
368 |
|
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
369 |
val _ = Output.debug "Proving cases for unique existence..." |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
370 |
val (ex1s, values) = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
371 |
split_list (map (mk_uniqueness_case thy globals G f ihyp ih_intro G_elim compat_store clauses repLemmas) clauses) |
19922 | 372 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
373 |
val _ = Output.debug "Proving: Graph is a function" (* FIXME: Rewrite this proof. *) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
374 |
val graph_is_function = complete |
19922 | 375 |
|> forall_elim_vars 0 |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
376 |
|> fold (curry op COMP) ex1s |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
377 |
|> implies_intr (ihyp) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
378 |
|> implies_intr (cterm_of thy (Trueprop (mk_mem (x, mk_acc domT R)))) |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
379 |
|> forall_intr (cterm_of thy x) |
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
380 |
|> (fn it => Drule.compose_single (it, 2, acc_induct_rule)) (* "EX! y. (?x,y):G" *) |
19922 | 381 |
|> (fn it => fold (forall_intr o cterm_of thy) (term_vars (prop_of it)) it) |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
382 |
|> Drule.close_derivation |
19922 | 383 |
|
384 |
val goal = complete COMP (graph_is_function COMP conjunctionI) |
|
385 |
|> Drule.close_derivation |
|
386 |
||
387 |
val goalI = Goal.protect goal |
|
388 |
|> fold_rev (implies_intr o cprop_of) compat |
|
389 |
|> implies_intr (cprop_of complete) |
|
390 |
in |
|
391 |
(prop_of goal, goalI, inst_ex1_iff, values) |
|
392 |
end |
|
393 |
||
394 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
395 |
fun define_graph Gname fvar domT ranT clauses RCss lthy = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
396 |
let |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
397 |
val GT = mk_relT (domT, ranT) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
398 |
val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)])) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
399 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
400 |
fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
401 |
let |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
402 |
fun mk_h_assm (rcfix, rcassm, rcarg) = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
403 |
mk_relmem (rcarg, fvar $ rcarg) Gvar |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
404 |
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
405 |
|> fold_rev (mk_forall o Free) rcfix |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
406 |
in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
407 |
mk_relmem (lhs, rhs) Gvar |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
408 |
|> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
409 |
|> fold_rev (curry Logic.mk_implies) gs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
410 |
|> fold_rev mk_forall (fvar :: qs) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
411 |
end |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
412 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
413 |
val G_intros = map2 mk_GIntro clauses RCss |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
414 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
415 |
val (GIntro_thms, (G, G_elim, lthy)) = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
416 |
FundefInductiveWrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
417 |
in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
418 |
((G, GIntro_thms, G_elim), lthy) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
419 |
end |
19922 | 420 |
|
421 |
||
422 |
||
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
423 |
fun define_function fdefname (fname, mixfix) domT ranT G default lthy = |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
424 |
let |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
425 |
val f_def = |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
426 |
Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $ |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
427 |
Abs ("y", ranT, mk_relmemT domT ranT (Bound 1, Bound 0) G)) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
428 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
429 |
val ((f, (_, f_defthm)), lthy) = LocalTheory.def ((fname ^ "C", mixfix), ((fdefname, []), f_def)) lthy |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
430 |
in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
431 |
((f, f_defthm), lthy) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
432 |
end |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
433 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
434 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
435 |
fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy = |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19583
diff
changeset
|
436 |
let |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
437 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
438 |
val RT = mk_relT (domT, domT) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
439 |
val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)])) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
440 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
441 |
fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
442 |
mk_relmem (rcarg, lhs) Rvar |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
443 |
|> fold_rev (curry Logic.mk_implies o prop_of) rcassm |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
444 |
|> fold_rev (curry Logic.mk_implies) gs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
445 |
|> fold_rev (mk_forall o Free) rcfix |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
446 |
|> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
447 |
(* "!!qs xs. CS ==> G => (r, lhs) : R" *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
448 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
449 |
val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
450 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
451 |
val (RIntro_thmss, (R, R_elim, lthy)) = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
452 |
fold_burrow FundefInductiveWrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
453 |
in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
454 |
((R, RIntro_thmss, R_elim), lthy) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
455 |
end |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19583
diff
changeset
|
456 |
|
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
457 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
458 |
fun fix_globals domT ranT fvar ctxt = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
459 |
let |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
460 |
val ([h, y, x, z, a, D, P, Pbool],ctxt') = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
461 |
Variable.invent_fixes ["h_fd", "y_fd", "x_fd", "z_fd", "a_fd", "D_fd", "P_fd", "Pb_fd"] ctxt |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
462 |
in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
463 |
(Globals {h = Free (h, domT --> ranT), |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
464 |
y = Free (y, ranT), |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
465 |
x = Free (x, domT), |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
466 |
z = Free (z, domT), |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
467 |
a = Free (a, domT), |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
468 |
D = Free (D, HOLogic.mk_setT domT), |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
469 |
P = Free (P, domT --> boolT), |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
470 |
Pbool = Free (Pbool, boolT), |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
471 |
fvar = fvar, |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
472 |
domT = domT, |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
473 |
ranT = ranT |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
474 |
}, |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
475 |
ctxt') |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
476 |
end |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
477 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
478 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
479 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
480 |
fun inst_RC thy fvar f (rcfix, rcassm, rcarg) = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
481 |
let |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
482 |
fun inst_term t = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
483 |
subst_bound(f, abstract_over (fvar, t)) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
484 |
in |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
485 |
(rcfix, map (assume o cterm_of thy o inst_term o prop_of) rcassm, inst_term rcarg) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
486 |
end |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
487 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
488 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
489 |
|
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
490 |
fun prepare_fundef defname (fname, fT, mixfix) abstract_qglrs default_str lthy = |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
491 |
let |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
492 |
val fvar = Free (fname, fT) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
493 |
val domT = domain_type fT |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
494 |
val ranT = range_type fT |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
495 |
|
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
496 |
val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *) |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
497 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
498 |
val congs = get_fundef_congs (Context.Proof lthy) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
499 |
val (globals, ctxt') = fix_globals domT ranT fvar lthy |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
500 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
501 |
val Globals { x, ... } = globals |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
502 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
503 |
val clauses = map (mk_clause_context x ctxt') abstract_qglrs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
504 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
505 |
val n = length abstract_qglrs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
506 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
507 |
val congs_deps = map (fn c => (c, FundefCtxTree.cong_deps c)) (congs @ FundefCtxTree.add_congs) (* FIXME: Save in theory *) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
508 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
509 |
fun build_tree (ClauseContext { ctxt, rhs, ...}) = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
510 |
FundefCtxTree.mk_tree congs_deps (fname, fT) ctxt rhs |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
511 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
512 |
val trees = map build_tree clauses |
19922 | 513 |
val RCss = map find_calls trees |
514 |
||
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
515 |
val ((G, GIntro_thms, G_elim), lthy) = define_graph (defname ^ "_graph") fvar domT ranT clauses RCss lthy |
20654
d80502f0d701
1. Function package accepts a parameter (default "some_term"), which specifies the functions
krauss
parents:
20536
diff
changeset
|
516 |
val ((f, f_defthm), lthy) = define_function (defname ^ "_sum_def") (fname, mixfix) domT ranT G default lthy |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
517 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
518 |
val RCss = map (map (inst_RC (ProofContext.theory_of lthy) fvar f)) RCss |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
519 |
val trees = map (FundefCtxTree.inst_tree (ProofContext.theory_of lthy) fvar f) trees |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19583
diff
changeset
|
520 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
521 |
val ((R, RIntro_thmss, R_elim), lthy) = |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
522 |
define_recursion_relation (defname ^ "_rel") domT ranT fvar f abstract_qglrs clauses RCss lthy |
19922 | 523 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
524 |
val dom_abbrev = Logic.mk_equals (Free (defname ^ "_dom", fastype_of (mk_acc domT R)), mk_acc domT R) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
525 |
val lthy = Specification.abbreviation_i ("", false) [(NONE, dom_abbrev)] lthy |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19583
diff
changeset
|
526 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
527 |
val newthy = ProofContext.theory_of lthy |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
528 |
val clauses = map (transfer_clause_ctx newthy) clauses |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
529 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
530 |
val cert = cterm_of (ProofContext.theory_of lthy) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
531 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
532 |
val xclauses = map7 (mk_clause_info globals G f) (1 upto n) clauses abstract_qglrs trees RCss GIntro_thms RIntro_thmss |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
533 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
534 |
val complete = mk_completeness globals clauses abstract_qglrs |> cert |> assume |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
535 |
val compat = mk_compat_proof_obligations domT ranT fvar f abstract_qglrs |> map (cert #> assume) |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
536 |
|
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
537 |
val compat_store = store_compat_thms n compat |
20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19922
diff
changeset
|
538 |
|
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
539 |
val (goal, goalI, ex1_iff, values) = prove_stuff newthy congs globals G f R xclauses complete compat compat_store G_elim f_defthm |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19583
diff
changeset
|
540 |
in |
20523
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
541 |
(Prep {globals = globals, f = f, G = G, R = R, goal = goal, goalI = goalI, values = values, clauses = xclauses, ex1_iff = ex1_iff, R_cases = R_elim}, f, |
36a59e5d0039
Major update to function package, including new syntax and the (only theoretical)
krauss
parents:
20071
diff
changeset
|
542 |
lthy) |
19770
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19583
diff
changeset
|
543 |
end |
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19583
diff
changeset
|
544 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19583
diff
changeset
|
545 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19583
diff
changeset
|
546 |
|
be5c23ebe1eb
HOL/Tools/function_package: Added support for mutual recursive definitions.
krauss
parents:
19583
diff
changeset
|
547 |
|
19876 | 548 |
end |