31 (entr as ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, |
31 (entr as ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, |
32 ld = ld, qe = qe, atoms = atoms}, |
32 ld = ld, qe = qe, atoms = atoms}, |
33 {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) = |
33 {isolate_conv = icv, whatis = wi, simpset = simpset}):entry) = |
34 let |
34 let |
35 fun uset (vars as (x::vs)) p = case Thm.term_of p of |
35 fun uset (vars as (x::vs)) p = case Thm.term_of p of |
36 Const(\<^const_name>\<open>HOL.conj\<close>, _)$ _ $ _ => |
36 \<^Const_>\<open>HOL.conj for _ _\<close> => |
37 let |
37 let |
38 val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb |
38 val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb |
39 val (lS,lth) = uset vars l val (rS, rth) = uset vars r |
39 val (lS,lth) = uset vars l val (rS, rth) = uset vars r |
40 in (lS@rS, Drule.binop_cong_rule b lth rth) end |
40 in (lS@rS, Drule.binop_cong_rule b lth rth) end |
41 | Const(\<^const_name>\<open>HOL.disj\<close>, _)$ _ $ _ => |
41 | \<^Const_>\<open>HOL.disj for _ _\<close> => |
42 let |
42 let |
43 val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb |
43 val ((b,l),r) = Thm.dest_comb p |>> Thm.dest_comb |
44 val (lS,lth) = uset vars l val (rS, rth) = uset vars r |
44 val (lS,lth) = uset vars l val (rS, rth) = uset vars r |
45 in (lS@rS, Drule.binop_cong_rule b lth rth) end |
45 in (lS@rS, Drule.binop_cong_rule b lth rth) end |
46 | _ => |
46 | _ => |
76 end |
76 end |
77 val U_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 (Thm.cprop_of qe))))) |
77 val U_v = dest_Var (Thm.term_of (Thm.dest_arg (Thm.dest_arg (Thm.dest_arg1 (Thm.cprop_of qe))))) |
78 fun main vs p = |
78 fun main vs p = |
79 let |
79 let |
80 val ((xn,ce),(x,fm)) = (case Thm.term_of p of |
80 val ((xn,ce),(x,fm)) = (case Thm.term_of p of |
81 Const(\<^const_name>\<open>Ex\<close>,_)$Abs(xn,xT,_) => |
81 \<^Const_>\<open>Ex _ for \<open>Abs(xn,xT,_)\<close>\<close> => |
82 Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn |
82 Thm.dest_comb p ||> Thm.dest_abs (SOME xn) |>> pair xn |
83 | _ => raise CTERM ("main QE only treats existential quantifiers!", [p])) |
83 | _ => raise CTERM ("main QE only treats existential quantifiers!", [p])) |
84 val cT = Thm.ctyp_of_cterm x |
84 val cT = Thm.ctyp_of_cterm x |
85 val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc) |
85 val (u,nth) = uset (x::vs) fm |>> distinct (op aconvc) |
86 val nthx = Thm.abstract_rule xn x nth |
86 val nthx = Thm.abstract_rule xn x nth |
97 val insI1 = Thm.instantiate' [SOME cT] [] @{thm "insertI1"} |
97 val insI1 = Thm.instantiate' [SOME cT] [] @{thm "insertI1"} |
98 val insI2 = Thm.instantiate' [SOME cT] [] @{thm "insertI2"} |
98 val insI2 = Thm.instantiate' [SOME cT] [] @{thm "insertI2"} |
99 in |
99 in |
100 fun provein x S = |
100 fun provein x S = |
101 case Thm.term_of S of |
101 case Thm.term_of S of |
102 Const(\<^const_name>\<open>Orderings.bot\<close>, _) => raise CTERM ("provein : not a member!", [S]) |
102 \<^Const_>\<open>Orderings.bot _\<close> => raise CTERM ("provein : not a member!", [S]) |
103 | Const(\<^const_name>\<open>insert\<close>, _) $ y $_ => |
103 | \<^Const_>\<open>insert _ for y _\<close> => |
104 let val (cy,S') = Thm.dest_binop S |
104 let val (cy,S') = Thm.dest_binop S |
105 in if Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1 |
105 in if Thm.term_of x aconv y then Thm.instantiate' [] [SOME x, SOME S'] insI1 |
106 else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2) |
106 else Thm.implies_elim (Thm.instantiate' [] [SOME x, SOME S', SOME cy] insI2) |
107 (provein x S') |
107 (provein x S') |
108 end |
108 end |
121 val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt, |
121 val [ld_conj, ld_disj, ld_eq, ld_neq, ld_lt, |
122 ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize (TVars.empty, Vars.make [(U_v,cU)])) ld |
122 ld_le, ld_gt, ld_ge, ld_P] = map (Drule.instantiate_normalize (TVars.empty, Vars.make [(U_v,cU)])) ld |
123 |
123 |
124 fun decomp_mpinf fm = |
124 fun decomp_mpinf fm = |
125 case Thm.term_of fm of |
125 case Thm.term_of fm of |
126 Const(\<^const_name>\<open>HOL.conj\<close>,_)$_$_ => |
126 \<^Const_>\<open>HOL.conj for _ _\<close> => |
127 let val (p,q) = Thm.dest_binop fm |
127 let val (p,q) = Thm.dest_binop fm |
128 in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj) |
128 in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj) |
129 (Thm.lambda x p) (Thm.lambda x q)) |
129 (Thm.lambda x p) (Thm.lambda x q)) |
130 end |
130 end |
131 | Const(\<^const_name>\<open>HOL.disj\<close>,_)$_$_ => |
131 | \<^Const_>\<open>HOL.disj for _ _\<close> => |
132 let val (p,q) = Thm.dest_binop fm |
132 let val (p,q) = Thm.dest_binop fm |
133 in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj) |
133 in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj) |
134 (Thm.lambda x p) (Thm.lambda x q)) |
134 (Thm.lambda x p) (Thm.lambda x q)) |
135 end |
135 end |
136 | _ => |
136 | _ => |
174 |
174 |
175 val grab_atom_bop = |
175 val grab_atom_bop = |
176 let |
176 let |
177 fun h bounds tm = |
177 fun h bounds tm = |
178 (case Thm.term_of tm of |
178 (case Thm.term_of tm of |
179 Const (\<^const_name>\<open>HOL.eq\<close>, T) $ _ $ _ => |
179 \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for _ _\<close> => find_args bounds tm |
180 if domain_type T = HOLogic.boolT then find_args bounds tm |
180 | \<^Const_>\<open>Not for _\<close> => h bounds (Thm.dest_arg tm) |
181 else Thm.dest_fun2 tm |
181 | \<^Const_>\<open>All _ for _\<close> => find_body bounds (Thm.dest_arg tm) |
182 | Const (\<^const_name>\<open>Not\<close>, _) $ _ => h bounds (Thm.dest_arg tm) |
182 | \<^Const_>\<open>Ex _ for _\<close> => find_body bounds (Thm.dest_arg tm) |
183 | Const (\<^const_name>\<open>All\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm) |
183 | \<^Const_>\<open>conj for _ _\<close> => find_args bounds tm |
184 | Const (\<^const_name>\<open>Ex\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm) |
184 | \<^Const_>\<open>disj for _ _\<close> => find_args bounds tm |
185 | Const (\<^const_name>\<open>HOL.conj\<close>, _) $ _ $ _ => find_args bounds tm |
185 | \<^Const_>\<open>implies for _ _\<close> => find_args bounds tm |
186 | Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _ => find_args bounds tm |
186 | \<^Const_>\<open>Pure.imp for _ _\<close> => find_args bounds tm |
187 | Const (\<^const_name>\<open>HOL.implies\<close>, _) $ _ $ _ => find_args bounds tm |
187 | \<^Const_>\<open>Pure.eq _ for _ _\<close> => find_args bounds tm |
188 | Const (\<^const_name>\<open>Pure.imp\<close>, _) $ _ $ _ => find_args bounds tm |
188 | \<^Const_>\<open>Pure.all _ for _\<close> => find_body bounds (Thm.dest_arg tm) |
189 | Const (\<^const_name>\<open>Pure.eq\<close>, _) $ _ $ _ => find_args bounds tm |
189 | \<^Const_>\<open>Trueprop for _\<close> => h bounds (Thm.dest_arg tm) |
190 | Const (\<^const_name>\<open>Pure.all\<close>, _) $ _ => find_body bounds (Thm.dest_arg tm) |
|
191 | Const (\<^const_name>\<open>Trueprop\<close>, _) $ _ => h bounds (Thm.dest_arg tm) |
|
192 | _ => Thm.dest_fun2 tm) |
190 | _ => Thm.dest_fun2 tm) |
193 and find_args bounds tm = |
191 and find_args bounds tm = |
194 (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm) |
192 (h bounds (Thm.dest_arg tm) handle CTERM _ => Thm.dest_arg1 tm) |
195 and find_body bounds b = |
193 and find_body bounds b = |
196 let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b |
194 let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b |