54 |
53 |
55 fun strip_trueprop (Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ P) = P |
54 fun strip_trueprop (Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ P) = P |
56 | strip_trueprop _ = raise TRUEPROP("not a prop!"); |
55 | strip_trueprop _ = raise TRUEPROP("not a prop!"); |
57 |
56 |
58 |
57 |
|
58 fun neg P = Const ("Not", Type("fun",[Type("bool",[]),Type("bool",[])])) $ P; |
|
59 |
|
60 |
|
61 fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_))= (p = q) |
|
62 | is_neg _ _ = false; |
|
63 |
59 |
64 |
60 exception STRIP_CONCL; |
65 exception STRIP_CONCL; |
61 |
66 |
62 |
67 |
63 fun strip_concl prems bvs (Const ("all", _) $ Abs (x,xtp,body)) = strip_concl prems ((x,xtp)::bvs) body |
68 fun strip_concl' prems bvs (Const ("==>",_) $ P $ Q) = |
64 | strip_concl prems bvs (Const ("==>",_) $ P $ Q) = |
|
65 let val P' = strip_trueprop P |
69 let val P' = strip_trueprop P |
66 val prems' = P'::prems |
70 val prems' = P'::prems |
67 in |
71 in |
68 strip_concl prems' bvs Q |
72 strip_concl' prems' bvs Q |
69 end |
73 end |
70 | strip_concl prems bvs _ = add_EX (make_conjs prems) bvs; |
74 | strip_concl' prems bvs P = |
|
75 let val P' = neg (strip_trueprop P) |
|
76 in |
|
77 add_EX (make_conjs (P'::prems)) bvs |
|
78 end; |
|
79 |
|
80 |
|
81 fun strip_concl prems bvs concl (Const ("all", _) $ Abs (x,xtp,body)) = strip_concl prems ((x,xtp)::bvs) concl body |
|
82 | strip_concl prems bvs concl (Const ("==>",_) $ P $ Q) = |
|
83 if (is_neg P concl) then (strip_concl' prems bvs Q) |
|
84 else |
|
85 (let val P' = strip_trueprop P |
|
86 val prems' = P'::prems |
|
87 in |
|
88 strip_concl prems' bvs concl Q |
|
89 end) |
|
90 | strip_concl prems bvs concl _ = add_EX (make_conjs prems) bvs; |
71 |
91 |
72 |
92 |
73 |
93 |
74 fun trans_elim (main,others) = |
94 fun trans_elim (main,others,concl) = |
75 let val others' = map (strip_concl [] []) others |
95 let val others' = map (strip_concl [] [] concl) others |
76 val disjs = make_disjs others' |
96 val disjs = make_disjs others' |
77 in |
97 in |
78 make_imp(strip_trueprop main,disjs) |
98 make_imp(strip_trueprop main,disjs) |
79 end; |
99 end; |
80 |
100 |
81 |
101 |
82 fun neg P = Const ("Not", Type("fun",[Type("bool",[]),Type("bool",[])])) $ P; |
102 fun elimR2Fol_aux prems concl = |
83 |
|
84 |
|
85 fun elimR2Fol_aux prems = |
|
86 let val nprems = length prems |
103 let val nprems = length prems |
87 val main = hd prems |
104 val main = hd prems |
88 in |
105 in |
89 if (nprems = 1) then neg (strip_trueprop main) |
106 if (nprems = 1) then neg (strip_trueprop main) |
90 else trans_elim (main, tl prems) |
107 else trans_elim (main, tl prems, concl) |
91 end; |
108 end; |
92 |
109 |
93 |
110 |
94 fun trueprop term = Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ term; |
111 fun trueprop term = Const ("Trueprop", Type("fun",[Type("bool",[]),Type("prop",[])])) $ term; |
95 |
112 |
97 fun elimR2Fol elimR = |
114 fun elimR2Fol elimR = |
98 let val elimR' = Drule.freeze_all elimR |
115 let val elimR' = Drule.freeze_all elimR |
99 val (prems,concl) = (prems_of elimR', concl_of elimR') |
116 val (prems,concl) = (prems_of elimR', concl_of elimR') |
100 in |
117 in |
101 case concl of Const("Trueprop",_) $ Free(_,Type("bool",[])) |
118 case concl of Const("Trueprop",_) $ Free(_,Type("bool",[])) |
102 => trueprop (elimR2Fol_aux prems) |
119 => trueprop (elimR2Fol_aux prems concl) |
103 | Free(x,Type("prop",[])) => trueprop(elimR2Fol_aux prems) |
120 | Free(x,Type("prop",[])) => trueprop(elimR2Fol_aux prems concl) |
104 | _ => raise ELIMR2FOL("Not an elimination rule!") |
121 | _ => raise ELIMR2FOL("Not an elimination rule!") |
105 end; |
122 end; |
106 |
|
107 |
123 |
108 |
124 |
109 |
125 |
110 (**** use prove_goalw_cterm to prove ****) |
126 (**** use prove_goalw_cterm to prove ****) |
111 |
127 |