87 val Collect_const = Const("Collect", [iT,iT-->oT]--->iT); |
87 val Collect_const = Const("Collect", [iT,iT-->oT]--->iT); |
88 fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t); |
88 fun mk_Collect (a,D,t) = Collect_const $ D $ absfree(a, iT, t); |
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; |
|
93 |
92 |
94 (*Prove a goal stated as a term, with exception handling*) |
93 (*Prove a goal stated as a term, with exception handling*) |
95 fun prove_term sign defs (P,tacsf) = |
94 fun prove_term sign defs (P,tacsf) = |
96 let val ct = cterm_of sign P |
95 let val ct = cterm_of sign P |
97 in prove_goalw_cterm defs ct tacsf |
96 in prove_goalw_cterm defs ct tacsf |
111 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, |
110 val basic_monos = [subset_refl, imp_refl, disj_mono, conj_mono, |
112 ex_mono, Collect_mono, Part_mono, in_mono]; |
111 ex_mono, Collect_mono, Part_mono, in_mono]; |
113 |
112 |
114 (*Return the conclusion of a rule, of the form t:X*) |
113 (*Return the conclusion of a rule, of the form t:X*) |
115 fun rule_concl rl = |
114 fun rule_concl rl = |
116 case dest_tprop (Logic.strip_imp_concl rl) of |
115 let val Const("Trueprop",_) $ (Const("op :",_) $ t $ X) = |
117 Const("op :",_) $ t $ X => (t,X) |
116 Logic.strip_imp_concl rl |
118 | _ => error "Conclusion of rule should be a set membership"; |
117 in (t,X) end; |
|
118 |
|
119 (*As above, but return error message if bad*) |
|
120 fun rule_concl_msg sign rl = rule_concl rl |
|
121 handle Bind => error ("Ill-formed conclusion of introduction rule: " ^ |
|
122 Sign.string_of_term sign rl); |
119 |
123 |
120 (*For deriving cases rules. CollectD2 discards the domain, which is redundant; |
124 (*For deriving cases rules. CollectD2 discards the domain, which is redundant; |
121 read_instantiate replaces a propositional variable by a formula variable*) |
125 read_instantiate replaces a propositional variable by a formula variable*) |
122 val equals_CollectD = |
126 val equals_CollectD = |
123 read_instantiate [("W","?Q")] |
127 read_instantiate [("W","?Q")] |