46 in |
46 in |
47 rev (FundefCtxTree.traverse_tree add_Ri tree []) |
47 rev (FundefCtxTree.traverse_tree add_Ri tree []) |
48 end |
48 end |
49 |
49 |
50 |
50 |
51 |
|
52 (* !!qs' qs. Gs ==> Gs' ==> lhs = lhs' ==> rhs = rhs' *) |
|
53 (* Takes bound form of qglrs tuples *) |
|
54 fun mk_compat_impl domT ranT fvar f ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) = |
|
55 let |
|
56 val shift = incr_boundvars (length qs') |
|
57 in |
|
58 (implies $ Trueprop (eq_const domT $ shift lhs $ lhs') |
|
59 $ Trueprop (eq_const ranT $ shift rhs $ rhs')) |
|
60 |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |
|
61 |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs') |
|
62 |> curry abstract_over fvar |
|
63 |> curry subst_bound f |
|
64 end |
|
65 |
|
66 fun mk_compat_proof_obligations domT ranT fvar f glrs = |
51 fun mk_compat_proof_obligations domT ranT fvar f glrs = |
67 map (mk_compat_impl domT ranT fvar f) (unordered_pairs glrs) |
52 let |
68 |
53 fun mk_impl ((qs, gs, lhs, rhs),(qs', gs', lhs', rhs')) = |
69 |
54 let |
70 fun mk_completeness globals clauses qglrs = |
55 val shift = incr_boundvars (length qs') |
71 let |
56 in |
72 val Globals {x, Pbool, ...} = globals |
57 (implies $ Trueprop (eq_const domT $ shift lhs $ lhs') |
73 |
58 $ Trueprop (eq_const ranT $ shift rhs $ rhs')) |
74 fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = Trueprop Pbool |
59 |> fold_rev (curry Logic.mk_implies) (map shift gs @ gs') |
75 |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs))) |
60 |> fold_rev (fn (n,T) => fn b => all T $ Abs(n,T,b)) (qs @ qs') |
76 |> fold_rev (curry Logic.mk_implies) gs |
61 |> curry abstract_over fvar |
77 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
62 |> curry subst_bound f |
|
63 end |
|
64 in |
|
65 map mk_impl (unordered_pairs glrs) |
|
66 end |
|
67 |
|
68 |
|
69 fun mk_completeness (Globals {x, Pbool, ...}) clauses qglrs = |
|
70 let |
|
71 fun mk_case (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) = |
|
72 Trueprop Pbool |
|
73 |> curry Logic.mk_implies (Trueprop (mk_eq (x, lhs))) |
|
74 |> fold_rev (curry Logic.mk_implies) gs |
|
75 |> fold_rev mk_forall_rename (map fst oqs ~~ qs) |
78 in |
76 in |
79 Trueprop Pbool |
77 Trueprop Pbool |
80 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs) |
78 |> fold_rev (curry Logic.mk_implies o mk_case) (clauses ~~ qglrs) |
81 |> mk_forall_rename ("x", x) |
79 |> mk_forall_rename ("x", x) |
82 |> mk_forall_rename ("P", Pbool) |
80 |> mk_forall_rename ("P", Pbool) |
242 in |
240 in |
243 replace_lemma |
241 replace_lemma |
244 end |
242 end |
245 |
243 |
246 |
244 |
247 |
|
248 |
|
249 fun pr (s:string) x = |
|
250 let val _ = print s |
|
251 in |
|
252 x |
|
253 end |
|
254 |
|
255 |
|
256 fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj = |
245 fun mk_uniqueness_clause thy globals f compat_store clausei clausej RLj = |
257 let |
246 let |
258 val Globals {h, y, x, fvar, ...} = globals |
247 val Globals {h, y, x, fvar, ...} = globals |
259 val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei |
248 val ClauseInfo {no=i, cdata=cctxi as ClauseContext {ctxt=ctxti, lhs=lhsi, case_hyp, ...}, ...} = clausei |
260 val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej |
249 val ClauseInfo {no=j, qglr=cdescj, RCs=RCsj, ...} = clausej |