# HG changeset patch
# User wenzelm
# Date 1393795492 -3600
# Node ID b56fda32bf24dac75fe69e13b10ec934281d1b06
# Parent  a05413276a0db1acd328fa5d97448e6272f4e6c2
tuned whitespace;

diff -r a05413276a0d -r b56fda32bf24 src/HOL/Decision_Procs/langford.ML
--- 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