140 |
140 |
141 val not_refl_disj_D = thm"meson_not_refl_disj_D"; |
141 val not_refl_disj_D = thm"meson_not_refl_disj_D"; |
142 |
142 |
143 fun refl_clause_aux 0 th = th |
143 fun refl_clause_aux 0 th = th |
144 | refl_clause_aux n th = |
144 | refl_clause_aux n th = |
145 (Output.debug ("refl_clause_aux " ^ Int.toString n ^ " " ^ string_of_thm th); |
|
146 case HOLogic.dest_Trueprop (concl_of th) of |
145 case HOLogic.dest_Trueprop (concl_of th) of |
147 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) => |
146 (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _) => |
148 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) |
147 refl_clause_aux n (th RS disj_assoc) (*isolate an atom as first disjunct*) |
149 | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => |
148 | (Const ("op |", _) $ (Const("Not",_) $ (Const("op =",_) $ t $ u)) $ _) => |
150 if is_Var t orelse is_Var u then (*Var inequation: delete or ignore*) |
149 if is_Var t orelse is_Var u then (*Var inequation: delete or ignore*) |
151 (refl_clause_aux (n-1) (th RS not_refl_disj_D) (*delete*) |
150 (refl_clause_aux (n-1) (th RS not_refl_disj_D) (*delete*) |
152 handle THM _ => refl_clause_aux (n-1) (th RS disj_comm)) (*ignore*) |
151 handle THM _ => refl_clause_aux (n-1) (th RS disj_comm)) (*ignore*) |
153 else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*) |
152 else refl_clause_aux (n-1) (th RS disj_comm) (*not between Vars: ignore*) |
154 | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm) |
153 | (Const ("op |", _) $ _ $ _) => refl_clause_aux n (th RS disj_comm) |
155 | _ => (*not a disjunction*) th); |
154 | _ => (*not a disjunction*) th; |
156 |
155 |
157 fun notequal_lits_count (Const ("op |", _) $ P $ Q) = |
156 fun notequal_lits_count (Const ("op |", _) $ P $ Q) = |
158 notequal_lits_count P + notequal_lits_count Q |
157 notequal_lits_count P + notequal_lits_count Q |
159 | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1 |
158 | notequal_lits_count (Const("Not",_) $ (Const("op =",_) $ _ $ _)) = 1 |
160 | notequal_lits_count _ = 0; |
159 | notequal_lits_count _ = 0; |
391 val tag_False = thm "tag_False"; |
390 val tag_False = thm "tag_False"; |
392 val nnf_simps = [Ex1_def,Ball_def,Bex_def,tag_True,tag_False] |
391 val nnf_simps = [Ex1_def,Ball_def,Bex_def,tag_True,tag_False] |
393 |
392 |
394 val nnf_ss = |
393 val nnf_ss = |
395 HOL_basic_ss addsimps |
394 HOL_basic_ss addsimps |
396 (nnf_simps @ [if_True, if_False, if_cancel, if_eq_cancel, cases_simp] |
395 (nnf_simps @ [if_True, if_False, if_cancel, if_eq_cancel, cases_simp] @ |
397 @ ex_simps @ all_simps @ simp_thms) |
396 thms"split_ifs" @ ex_simps @ all_simps @ simp_thms) |
398 addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc] |
397 addsimprocs [defALL_regroup,defEX_regroup,neq_simproc,let_simproc]; |
399 addsplits [split_if]; |
|
400 |
398 |
401 fun make_nnf th = th |> simplify nnf_ss |
399 fun make_nnf th = th |> simplify nnf_ss |
402 |> make_nnf1 |
400 |> make_nnf1 |
403 |
401 |
404 (*Pull existential quantifiers to front. This accomplishes Skolemization for |
402 (*Pull existential quantifiers to front. This accomplishes Skolemization for |