--- a/src/HOL/Decision_Procs/langford.ML Sun Mar 02 22:03:27 2014 +0100
+++ b/src/HOL/Decision_Procs/langford.ML Sun Mar 02 22:24:52 2014 +0100
@@ -21,7 +21,7 @@
fun prove_finite cT u =
let
- val [th0, th1] = map (instantiate' [SOME cT] []) @{thms "finite.intros"}
+ val [th0, th1] = map (instantiate' [SOME cT] []) @{thms finite.intros}
fun ins x th =
Thm.implies_elim
(instantiate' [] [(SOME o Thm.dest_arg o Thm.dest_arg) (Thm.cprop_of th), SOME x] th1) th
@@ -33,176 +33,193 @@
(Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms ball_simps simp_thms})));
fun basic_dloqe ctxt stupid dlo_qeth dlo_qeth_nolb dlo_qeth_noub gather ep =
- case term_of ep of
- Const(@{const_name Ex},_)$_ =>
- let
- val p = Thm.dest_arg ep
- val ths =
- simplify (put_simpset HOL_basic_ss ctxt addsimps gather) (instantiate' [] [SOME p] stupid)
- val (L,U) =
- let
- val (_, q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
- in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1)
- end
- fun proveneF S =
- let val (a,A) = Thm.dest_comb S |>> Thm.dest_arg
- val cT = ctyp_of_term a
- val ne = instantiate' [SOME cT] [SOME a, SOME A]
- @{thm insert_not_empty}
- val f = prove_finite cT (dest_set S)
- in (ne, f) end
+ (case term_of ep of
+ Const (@{const_name Ex}, _) $ _ =>
+ let
+ val p = Thm.dest_arg ep
+ val ths =
+ simplify (put_simpset HOL_basic_ss ctxt addsimps gather)
+ (instantiate' [] [SOME p] stupid)
+ val (L, U) =
+ let val (_, q) = Thm.dest_abs NONE (Thm.dest_arg (Thm.rhs_of ths))
+ in (Thm.dest_arg1 q |> Thm.dest_arg1, Thm.dest_arg q |> Thm.dest_arg1) end
+ fun proveneF S =
+ let
+ val (a, A) = Thm.dest_comb S |>> Thm.dest_arg
+ val cT = ctyp_of_term a
+ val ne = instantiate' [SOME cT] [SOME a, SOME A] @{thm insert_not_empty}
+ val f = prove_finite cT (dest_set S)
+ in (ne, f) end
- val qe = case (term_of L, term_of U) of
- (Const (@{const_name Orderings.bot}, _),_) =>
- let
- val (neU,fU) = proveneF U
- in simp_rule ctxt (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
- | (_,Const (@{const_name Orderings.bot}, _)) =>
- let
- val (neL,fL) = proveneF L
- in simp_rule ctxt (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
-
- | (_,_) =>
- let
- val (neL,fL) = proveneF L
- val (neU,fU) = proveneF U
- in simp_rule ctxt (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU]))
- end
- in qe end
- | _ => error "dlo_qe : Not an existential formula";
+ val qe =
+ (case (term_of L, term_of U) of
+ (Const (@{const_name Orderings.bot}, _),_) =>
+ let val (neU, fU) = proveneF U
+ in simp_rule ctxt (Thm.transitive ths (dlo_qeth_nolb OF [neU, fU])) end
+ | (_, Const (@{const_name Orderings.bot}, _)) =>
+ let val (neL,fL) = proveneF L
+ in simp_rule ctxt (Thm.transitive ths (dlo_qeth_noub OF [neL, fL])) end
+ | _ =>
+ let
+ val (neL, fL) = proveneF L
+ val (neU, fU) = proveneF U
+ in simp_rule ctxt (Thm.transitive ths (dlo_qeth OF [neL, neU, fL, fU])) end)
+ in qe end
+ | _ => error "dlo_qe : Not an existential formula");
val all_conjuncts =
- let fun h acc ct =
- case term_of ct of
- @{term HOL.conj}$_$_ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
- | _ => ct::acc
-in h [] end;
+ let
+ fun h acc ct =
+ (case term_of ct of
+ @{term HOL.conj} $ _ $ _ => h (h acc (Thm.dest_arg ct)) (Thm.dest_arg1 ct)
+ | _ => ct :: acc)
+ in h [] end;
fun conjuncts ct =
- case term_of ct of
- @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
-| _ => [ct];
+ (case term_of ct of
+ @{term HOL.conj} $ _ $ _ => Thm.dest_arg1 ct :: conjuncts (Thm.dest_arg ct)
+ | _ => [ct]);
-fun fold1 f = foldr1 (uncurry f);
+fun fold1 f = foldr1 (uncurry f); (* FIXME !? *)
-val list_conj = fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c') ;
+val list_conj =
+ fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c');
fun mk_conj_tab th =
- let fun h acc th =
- case prop_of th of
- @{term "Trueprop"}$(@{term HOL.conj}$p$q) =>
- h (h acc (th RS conjunct2)) (th RS conjunct1)
- | @{term "Trueprop"}$p => (p,th)::acc
-in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
+ let
+ fun h acc th =
+ (case prop_of th of
+ @{term "Trueprop"} $ (@{term HOL.conj} $ p $ q) =>
+ h (h acc (th RS conjunct2)) (th RS conjunct1)
+ | @{term "Trueprop"} $ p => (p, th) :: acc)
+ in fold (Termtab.insert Thm.eq_thm) (h [] th) Termtab.empty end;
fun is_conj (@{term HOL.conj}$_$_) = true
| is_conj _ = false;
fun prove_conj tab cjs =
- case cjs of
- [c] => if is_conj (term_of c) then prove_conj tab (conjuncts c) else tab c
- | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs];
+ (case cjs of
+ [c] =>
+ if is_conj (term_of c)
+ then prove_conj tab (conjuncts c)
+ else tab c
+ | c :: cs => conjI OF [prove_conj tab [c], prove_conj tab cs]);
fun conj_aci_rule eq =
- let
- val (l,r) = Thm.dest_equals eq
- fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c))
- fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c))
- val ll = Thm.dest_arg l
- val rr = Thm.dest_arg r
+ let
+ val (l, r) = Thm.dest_equals eq
+ fun tabl c = the (Termtab.lookup (mk_conj_tab (Thm.assume l)) (term_of c))
+ fun tabr c = the (Termtab.lookup (mk_conj_tab (Thm.assume r)) (term_of c))
+ val ll = Thm.dest_arg l
+ val rr = Thm.dest_arg r
+ val thl = prove_conj tabl (conjuncts rr) |> Drule.implies_intr_hyps
+ val thr = prove_conj tabr (conjuncts ll) |> Drule.implies_intr_hyps
+ val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
+ in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
- val thl = prove_conj tabl (conjuncts rr)
- |> Drule.implies_intr_hyps
- val thr = prove_conj tabr (conjuncts ll)
- |> Drule.implies_intr_hyps
- val eqI = instantiate' [] [SOME ll, SOME rr] @{thm iffI}
- in Thm.implies_elim (Thm.implies_elim eqI thl) thr |> mk_meta_eq end;
+fun contains x ct =
+ member (op aconv) (Misc_Legacy.term_frees (term_of ct)) (term_of x);
-fun contains x ct = member (op aconv) (Misc_Legacy.term_frees (term_of ct)) (term_of x);
-
-fun is_eqx x eq = case term_of eq of
- Const(@{const_name HOL.eq},_)$l$r => l aconv term_of x orelse r aconv term_of x
- | _ => false ;
+fun is_eqx x eq =
+ (case term_of eq of
+ Const (@{const_name HOL.eq}, _) $ l $ r =>
+ l aconv term_of x orelse r aconv term_of x
+ | _ => false);
local
+
fun proc ctxt ct =
- case term_of ct of
- Const(@{const_name Ex},_)$Abs (xn,_,_) =>
- let
- val e = Thm.dest_fun ct
- val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
- val Pp = Thm.apply @{cterm "Trueprop"} p
- val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
- in case eqs of
- [] =>
- let
- val (dx,ndx) = List.partition (contains x) neqs
- in case ndx of [] => NONE
- | _ =>
- conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
- (Thm.apply @{cterm Trueprop} (list_conj (ndx @dx))))
- |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
- |> Conv.fconv_rule (Conv.arg_conv
- (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
- |> SOME
- end
- | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp
- (Thm.apply @{cterm Trueprop} (list_conj (eqs@neqs))))
- |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
- |> Conv.fconv_rule (Conv.arg_conv
- (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
- |> SOME
- end
- | _ => NONE;
-in val reduce_ex_simproc =
+ (case term_of ct of
+ Const (@{const_name Ex}, _) $ Abs (xn, _, _) =>
+ let
+ val e = Thm.dest_fun ct
+ val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
+ val Pp = Thm.apply @{cterm Trueprop} p
+ val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
+ in
+ (case eqs of
+ [] =>
+ let
+ val (dx, ndx) = List.partition (contains x) neqs
+ in
+ case ndx of
+ [] => NONE
+ | _ =>
+ conj_aci_rule (Thm.mk_binop @{cterm "op \<equiv> :: prop => _"} Pp
+ (Thm.apply @{cterm Trueprop} (list_conj (ndx @ dx))))
+ |> Thm.abstract_rule xn x
+ |> Drule.arg_cong_rule e
+ |> Conv.fconv_rule
+ (Conv.arg_conv
+ (Simplifier.rewrite
+ (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
+ |> SOME
+ end
+ | _ =>
+ conj_aci_rule (Thm.mk_binop @{cterm "op \<equiv> :: prop => _"} Pp
+ (Thm.apply @{cterm Trueprop} (list_conj (eqs @ neqs))))
+ |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e
+ |> Conv.fconv_rule
+ (Conv.arg_conv
+ (Simplifier.rewrite
+ (put_simpset HOL_basic_ss ctxt addsimps @{thms simp_thms ex_simps})))
+ |> SOME)
+ end
+ | _ => NONE);
+
+in
+
+val reduce_ex_simproc =
Simplifier.make_simproc
- {lhss = [@{cpat "EX x. ?P x"}] , name = "reduce_ex_simproc",
- proc = K proc, identifier = []}
+ {lhss = [@{cpat "\<exists>x. ?P x"}],
+ name = "reduce_ex_simproc",
+ proc = K proc,
+ identifier = []};
+
end;
fun raw_dlo_conv ctxt dlo_ss ({qe_bnds, qe_nolb, qe_noub, gst, gs, ...}: Langford_Data.entry) =
- let
- val ctxt' = put_simpset dlo_ss ctxt addsimps @{thms "dnf_simps"} addsimprocs [reduce_ex_simproc]
- val dnfex_conv = Simplifier.rewrite ctxt'
- val pcv =
- Simplifier.rewrite
- (put_simpset dlo_ss ctxt
- addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
- in fn p =>
- Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
- (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive)
- (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
- end;
-
+ let
+ val ctxt' = put_simpset dlo_ss ctxt addsimps @{thms dnf_simps} addsimprocs [reduce_ex_simproc]
+ val dnfex_conv = Simplifier.rewrite ctxt'
+ val pcv =
+ Simplifier.rewrite
+ (put_simpset dlo_ss ctxt
+ addsimps @{thms simp_thms ex_simps all_simps all_not_ex not_all ex_disj_distrib})
+ in
+ fn p =>
+ Qelim.gen_qelim_conv pcv pcv dnfex_conv cons
+ (Thm.add_cterm_frees p []) (K Thm.reflexive) (K Thm.reflexive)
+ (K (basic_dloqe ctxt gst qe_bnds qe_nolb qe_noub gs)) p
+ end;
val grab_atom_bop =
- let
- fun h bounds tm =
- (case term_of tm of
- Const (@{const_name HOL.eq}, T) $ _ $ _ =>
- if domain_type T = HOLogic.boolT then find_args bounds tm
- else Thm.dest_fun2 tm
- | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
- | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
- | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
- | Const ("==>", _) $ _ $ _ => find_args bounds tm
- | Const ("==", _) $ _ $ _ => find_args bounds tm
- | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
- | _ => Thm.dest_fun2 tm)
- and find_args bounds tm =
- (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
- and find_body bounds b =
- let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
- in h (bounds + 1) b' end;
-in h end;
+ let
+ fun h bounds tm =
+ (case term_of tm of
+ Const (@{const_name HOL.eq}, T) $ _ $ _ =>
+ if domain_type T = HOLogic.boolT then find_args bounds tm
+ else Thm.dest_fun2 tm
+ | Const (@{const_name Not}, _) $ _ => h bounds (Thm.dest_arg tm)
+ | Const (@{const_name All}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const ("all", _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name Ex}, _) $ _ => find_body bounds (Thm.dest_arg tm)
+ | Const (@{const_name HOL.conj}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.disj}, _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name HOL.implies}, _) $ _ $ _ => find_args bounds tm
+ | Const ("==>", _) $ _ $ _ => find_args bounds tm
+ | Const ("==", _) $ _ $ _ => find_args bounds tm
+ | Const (@{const_name Trueprop}, _) $ _ => h bounds (Thm.dest_arg tm)
+ | _ => Thm.dest_fun2 tm)
+ and find_args bounds tm =
+ (h bounds (Thm.dest_arg tm) handle CTERM _ => h bounds (Thm.dest_arg1 tm))
+ and find_body bounds b =
+ let val (_, b') = Thm.dest_abs (SOME (Name.bound bounds)) b
+ in h (bounds + 1) b' end;
+ in h end;
fun dlo_instance ctxt tm =
- (fst (Langford_Data.get ctxt),
- Langford_Data.match ctxt (grab_atom_bop 0 tm));
+ (fst (Langford_Data.get ctxt), Langford_Data.match ctxt (grab_atom_bop 0 tm));
fun dlo_conv ctxt tm =
(case dlo_instance ctxt tm of
@@ -210,28 +227,28 @@
| (ss, SOME instance) => raw_dlo_conv ctxt ss instance tm);
fun generalize_tac f = CSUBGOAL (fn (p, _) => PRIMITIVE (fn st =>
- let
- fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
- fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
- val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
- val p' = fold_rev gen ts p
- in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
-
+ let
+ fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
+ fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
+ val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
+ val p' = fold_rev gen ts p
+ in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
fun cfrees ats ct =
- let
- val ins = insert (op aconvc)
- fun h acc t =
- case (term_of t) of
- _$_$_ => if member (op aconvc) ats (Thm.dest_fun2 t)
- then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc)
- else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
- | _$_ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
- | Abs(_,_,_) => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
- | Free _ => if member (op aconvc) ats t then acc else ins t acc
- | Var _ => if member (op aconvc) ats t then acc else ins t acc
- | _ => acc
- in h [] ct end
+ let
+ val ins = insert (op aconvc)
+ fun h acc t =
+ (case (term_of t) of
+ _ $ _ $ _ =>
+ if member (op aconvc) ats (Thm.dest_fun2 t)
+ then ins (Thm.dest_arg t) (ins (Thm.dest_arg1 t) acc)
+ else h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
+ | _ $ _ => h (h acc (Thm.dest_arg t)) (Thm.dest_fun t)
+ | Abs _ => Thm.dest_abs NONE t ||> h acc |> uncurry (remove (op aconvc))
+ | Free _ => if member (op aconvc) ats t then acc else ins t acc
+ | Var _ => if member (op aconvc) ats t then acc else ins t acc
+ | _ => acc)
+ in h [] ct end
fun dlo_tac ctxt = CSUBGOAL (fn (p, i) =>
(case dlo_instance ctxt p of