89 |
89 |
90 val Trueprop = Const("Trueprop",oT-->propT); |
90 val Trueprop = Const("Trueprop",oT-->propT); |
91 fun mk_tprop P = Trueprop $ P; |
91 fun mk_tprop P = Trueprop $ P; |
92 fun dest_tprop (Const("Trueprop",_) $ P) = P; |
92 fun dest_tprop (Const("Trueprop",_) $ P) = P; |
93 |
93 |
94 (*** Tactic for folding constructor definitions ***) |
|
95 |
|
96 (*The depth of injections in a constructor function*) |
|
97 fun inject_depth (Const _ $ t) = 1 + inject_depth t |
|
98 | inject_depth t = 0; |
|
99 |
|
100 val rhs_of_thm = #2 o Logic.dest_equals o #prop o rep_thm; |
|
101 |
|
102 (*There are critical pairs! E.g. K == Inl(0), S == Inr(Inl(0)) |
|
103 Folds longest definitions first to avoid folding subexpressions of an rhs.*) |
|
104 fun fold_con_tac defs = |
|
105 let val keylist = make_keylist (inject_depth o rhs_of_thm) defs; |
|
106 val keys = distinct (sort op> (map #2 keylist)); |
|
107 val deflists = map (keyfilter keylist) keys |
|
108 in EVERY (map fold_tac deflists) end; |
|
109 |
|
110 (*Prove a goal stated as a term, with exception handling*) |
94 (*Prove a goal stated as a term, with exception handling*) |
111 fun prove_term sign defs (P,tacsf) = |
95 fun prove_term sign defs (P,tacsf) = |
112 let val ct = Sign.cterm_of sign P |
96 let val ct = Sign.cterm_of sign P |
113 in prove_goalw_cterm defs ct tacsf |
97 in prove_goalw_cterm defs ct tacsf |
114 handle e => (writeln ("Exception in proof of\n" ^ |
98 handle e => (writeln ("Exception in proof of\n" ^ |