merged

--- a/src/HOL/Complex.thy	Thu Sep 08 11:31:23 2011 +0200
+++ b/src/HOL/Complex.thy	Thu Sep 08 11:31:53 2011 +0200
@@ -253,6 +253,10 @@
   shows "complex_of_real r * Complex x y = Complex (r*x) (r*y)"
   by (simp add: complex_of_real_def)
 
+lemma complex_split_polar:
+     "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
+  by (simp add: complex_eq_iff polar_Ex)
+
 
 subsection {* Vector Norm *}
 
@@ -379,7 +383,7 @@
 qed
 
 
-subsection {* The Complex Number @{term "\<i>"} *}
+subsection {* The Complex Number $i$ *}
 
 definition "ii" :: complex  ("\<i>")
   where i_def: "ii \<equiv> Complex 0 1"
@@ -423,6 +427,9 @@
 lemma inverse_i [simp]: "inverse ii = - ii"
   by (rule inverse_unique, simp)
 
+lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
+  by (simp add: mult_assoc [symmetric])
+
 
 subsection {* Complex Conjugation *}
 
@@ -507,6 +514,12 @@
 lemma complex_mod_mult_cnj: "cmod (z * cnj z) = (cmod z)\<twosuperior>"
   by (simp add: norm_mult power2_eq_square)
 
+lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
+  by (simp add: cmod_def power2_eq_square)
+
+lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
+  by simp
+
 lemma bounded_linear_cnj: "bounded_linear cnj"
   using complex_cnj_add complex_cnj_scaleR
   by (rule bounded_linear_intro [where K=1], simp)
@@ -518,9 +531,7 @@
   bounded_linear.isCont [OF bounded_linear_cnj]
 
 
-subsection{*The Functions @{term sgn} and @{term arg}*}
-
-text {*------------ Argand -------------*}
+subsection {* Complex Signum and Argument *}
 
 definition arg :: "complex => real" where
   "arg z = (SOME a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi)"
@@ -570,16 +581,90 @@
 
 subsection{*Finally! Polar Form for Complex Numbers*}
 
-text {* An abbreviation for @{text "cos a + i sin a"}. *}
+subsubsection {* $\cos \theta + i \sin \theta$ *}
 
 definition cis :: "real \<Rightarrow> complex" where
   "cis a = Complex (cos a) (sin a)"
 
-text {* An abbreviation for @{text "r(cos a + i sin a)"}. *}
+lemma Re_cis [simp]: "Re (cis a) = cos a"
+  by (simp add: cis_def)
+
+lemma Im_cis [simp]: "Im (cis a) = sin a"
+  by (simp add: cis_def)
+
+lemma cis_zero [simp]: "cis 0 = 1"
+  by (simp add: cis_def)
+
+lemma norm_cis [simp]: "norm (cis a) = 1"
+  by (simp add: cis_def)
+
+lemma sgn_cis [simp]: "sgn (cis a) = cis a"
+  by (simp add: sgn_div_norm)
+
+lemma cis_neq_zero [simp]: "cis a \<noteq> 0"
+  by (metis norm_cis norm_zero zero_neq_one)
+
+lemma cis_mult: "cis a * cis b = cis (a + b)"
+  by (simp add: cis_def cos_add sin_add)
+
+lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
+  by (induct n, simp_all add: real_of_nat_Suc algebra_simps cis_mult)
+
+lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
+  by (simp add: cis_def)
+
+lemma cis_divide: "cis a / cis b = cis (a - b)"
+  by (simp add: complex_divide_def cis_mult diff_minus)
+
+lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
+  by (auto simp add: DeMoivre)
+
+lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
+  by (auto simp add: DeMoivre)
+
+subsubsection {* $r(\cos \theta + i \sin \theta)$ *}
 
 definition rcis :: "[real, real] \<Rightarrow> complex" where
   "rcis r a = complex_of_real r * cis a"
 
+lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
+  by (simp add: rcis_def)
+
+lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
+  by (simp add: rcis_def)
+
+lemma rcis_Ex: "\<exists>r a. z = rcis r a"
+  by (simp add: complex_eq_iff polar_Ex)
+
+lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
+  by (simp add: rcis_def norm_mult)
+
+lemma cis_rcis_eq: "cis a = rcis 1 a"
+  by (simp add: rcis_def)
+
+lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
+  by (simp add: rcis_def cis_mult)
+
+lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
+  by (simp add: rcis_def)
+
+lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
+  by (simp add: rcis_def)
+
+lemma rcis_eq_zero_iff [simp]: "rcis r a = 0 \<longleftrightarrow> r = 0"
+  by (simp add: rcis_def)
+
+lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
+  by (simp add: rcis_def power_mult_distrib DeMoivre)
+
+lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
+  by (simp add: divide_inverse rcis_def)
+
+lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
+  by (simp add: rcis_def cis_divide [symmetric])
+
+subsubsection {* Complex exponential *}
+
 abbreviation expi :: "complex \<Rightarrow> complex"
   where "expi \<equiv> exp"
 
@@ -604,86 +689,11 @@
 lemma expi_def: "expi z = complex_of_real (exp (Re z)) * cis (Im z)"
   unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by simp
 
-lemma complex_split_polar:
-     "\<exists>r a. z = complex_of_real r * (Complex (cos a) (sin a))"
-apply (induct z)
-apply (auto simp add: polar_Ex complex_of_real_mult_Complex)
-done
-
-lemma rcis_Ex: "\<exists>r a. z = rcis r a"
-apply (induct z)
-apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex)
-done
-
-lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a"
-  by (simp add: rcis_def cis_def)
-
-lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
-  by (simp add: rcis_def cis_def)
-
-lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
-  by (simp add: rcis_def cis_def norm_mult)
-
-lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
-  by (simp add: cmod_def power2_eq_square)
-
-lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0"
-  by simp
-
-lemma cis_rcis_eq: "cis a = rcis 1 a"
-  by (simp add: rcis_def)
-
-lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)"
-  by (simp add: rcis_def cis_def cos_add sin_add right_distrib
-    right_diff_distrib complex_of_real_def)
-
-lemma cis_mult: "cis a * cis b = cis (a + b)"
-  by (simp add: cis_rcis_eq rcis_mult)
-
-lemma cis_zero [simp]: "cis 0 = 1"
-  by (simp add: cis_def complex_one_def)
+lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)"
+  unfolding expi_def by simp
 
-lemma rcis_zero_mod [simp]: "rcis 0 a = 0"
-  by (simp add: rcis_def)
-
-lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r"
-  by (simp add: rcis_def)
-
-lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x"
-  by (simp add: mult_assoc [symmetric])
-
-lemma DeMoivre: "(cis a) ^ n = cis (real n * a)"
-  by (induct n, simp_all add: real_of_nat_Suc algebra_simps cis_mult)
-
-lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)"
-  by (simp add: rcis_def power_mult_distrib DeMoivre)
-
-lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)"
-  by (simp add: cis_def complex_inverse_complex_split diff_minus)
-
-lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)"
-  by (simp add: divide_inverse rcis_def)
-
-lemma cis_divide: "cis a / cis b = cis (a - b)"
-  by (simp add: complex_divide_def cis_mult diff_minus)
-
-lemma rcis_divide: "rcis r1 a / rcis r2 b = rcis (r1/r2) (a - b)"
-apply (simp add: complex_divide_def)
-apply (case_tac "r2=0", simp)
-apply (simp add: rcis_inverse rcis_mult diff_minus)
-done
-
-lemma Re_cis [simp]: "Re(cis a) = cos a"
-  by (simp add: cis_def)
-
-lemma Im_cis [simp]: "Im(cis a) = sin a"
-  by (simp add: cis_def)
-
-lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)"
-  by (auto simp add: DeMoivre)
-
-lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)"
-  by (auto simp add: DeMoivre)
+lemma Im_exp: "Im (exp z) = exp (Re z) * sin (Im z)"
+  unfolding expi_def by simp
 
 lemma complex_expi_Ex: "\<exists>a r. z = complex_of_real r * expi a"
 apply (insert rcis_Ex [of z])

--- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Sep 08 11:31:23 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Sep 08 11:31:53 2011 +0200
@@ -1312,9 +1312,25 @@
 (** predicators and application operators **)
 
 type sym_info =
-  {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
+  {pred_sym : bool, min_ary : int, max_ary : int, types : typ list,
+   in_conj : bool}
 
-fun add_iterm_syms_to_table ctxt explicit_apply =
+fun default_sym_tab_entries type_enc =
+  (make_fixed_const NONE @{const_name undefined},
+       {pred_sym = false, min_ary = 0, max_ary = 0, types = [],
+        in_conj = false}) ::
+  ([tptp_false, tptp_true]
+   |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [],
+                  in_conj = false})) @
+  ([tptp_equal, tptp_old_equal]
+   |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [],
+                  in_conj = false}))
+  |> not (is_type_enc_higher_order type_enc)
+     ? cons (prefixed_predicator_name,
+             {pred_sym = true, min_ary = 1, max_ary = 1, types = [],
+              in_conj = false})
+
+fun sym_table_for_facts ctxt type_enc explicit_apply conjs facts =
   let
     fun consider_var_ary const_T var_T max_ary =
       let
@@ -1330,10 +1346,10 @@
          (can dest_funT T orelse T = @{typ bool}) then
         let
           val bool_vars' = bool_vars orelse body_type T = @{typ bool}
-          fun repair_min_ary {pred_sym, min_ary, max_ary, types} =
+          fun repair_min_ary {pred_sym, min_ary, max_ary, types, in_conj} =
             {pred_sym = pred_sym andalso not bool_vars',
              min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
-             max_ary = max_ary, types = types}
+             max_ary = max_ary, types = types, in_conj = in_conj}
           val fun_var_Ts' =
             fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
         in
@@ -1345,77 +1361,70 @@
         end
       else
         accum
-    fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
-      let val (head, args) = strip_iterm_comb tm in
-        (case head of
-           IConst ((s, _), T, _) =>
-           if String.isPrefix bound_var_prefix s orelse
-              String.isPrefix all_bound_var_prefix s then
-             add_universal_var T accum
-           else if String.isPrefix exist_bound_var_prefix s then
-             accum
-           else
-             let val ary = length args in
-               ((bool_vars, fun_var_Ts),
-                case Symtab.lookup sym_tab s of
-                  SOME {pred_sym, min_ary, max_ary, types} =>
-                  let
-                    val pred_sym =
-                      pred_sym andalso top_level andalso not bool_vars
-                    val types' = types |> insert_type ctxt I T
-                    val min_ary =
-                      if is_some explicit_apply orelse
-                         pointer_eq (types', types) then
-                        min_ary
-                      else
-                        fold (consider_var_ary T) fun_var_Ts min_ary
-                  in
-                    Symtab.update (s, {pred_sym = pred_sym,
-                                       min_ary = Int.min (ary, min_ary),
-                                       max_ary = Int.max (ary, max_ary),
-                                       types = types'})
-                                  sym_tab
-                  end
-                | NONE =>
-                  let
-                    val pred_sym = top_level andalso not bool_vars
-                    val min_ary =
-                      case explicit_apply of
-                        SOME true => 0
-                      | SOME false => ary
-                      | NONE => fold (consider_var_ary T) fun_var_Ts ary
-                  in
-                    Symtab.update_new (s, {pred_sym = pred_sym,
-                                           min_ary = min_ary, max_ary = ary,
-                                           types = [T]})
+    fun add_fact_syms conj_fact =
+      let
+        fun add_iterm_syms top_level tm
+                           (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
+          let val (head, args) = strip_iterm_comb tm in
+            (case head of
+               IConst ((s, _), T, _) =>
+               if String.isPrefix bound_var_prefix s orelse
+                  String.isPrefix all_bound_var_prefix s then
+                 add_universal_var T accum
+               else if String.isPrefix exist_bound_var_prefix s then
+                 accum
+               else
+                 let val ary = length args in
+                   ((bool_vars, fun_var_Ts),
+                    case Symtab.lookup sym_tab s of
+                      SOME {pred_sym, min_ary, max_ary, types, in_conj} =>
+                      let
+                        val pred_sym =
+                          pred_sym andalso top_level andalso not bool_vars
+                        val types' = types |> insert_type ctxt I T
+                        val in_conj = in_conj orelse conj_fact
+                        val min_ary =
+                          if is_some explicit_apply orelse
+                             pointer_eq (types', types) then
+                            min_ary
+                          else
+                            fold (consider_var_ary T) fun_var_Ts min_ary
+                      in
+                        Symtab.update (s, {pred_sym = pred_sym,
+                                           min_ary = Int.min (ary, min_ary),
+                                           max_ary = Int.max (ary, max_ary),
+                                           types = types', in_conj = in_conj})
                                       sym_tab
-                  end)
-             end
-         | IVar (_, T) => add_universal_var T accum
-         | IAbs ((_, T), tm) => accum |> add_universal_var T |> add false tm
-         | _ => accum)
-        |> fold (add false) args
-      end
-  in add true end
-fun add_fact_syms_to_table ctxt explicit_apply =
-  K (add_iterm_syms_to_table ctxt explicit_apply)
-  |> formula_fold NONE |> fact_lift
-
-fun default_sym_tab_entries type_enc =
-  (make_fixed_const NONE @{const_name undefined},
-                   {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
-  ([tptp_false, tptp_true]
-   |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
-  ([tptp_equal, tptp_old_equal]
-   |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
-  |> not (is_type_enc_higher_order type_enc)
-     ? cons (prefixed_predicator_name,
-             {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
-
-fun sym_table_for_facts ctxt type_enc explicit_apply facts =
-  ((false, []), Symtab.empty)
-  |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
-  |> fold Symtab.update (default_sym_tab_entries type_enc)
+                      end
+                    | NONE =>
+                      let
+                        val pred_sym = top_level andalso not bool_vars
+                        val min_ary =
+                          case explicit_apply of
+                            SOME true => 0
+                          | SOME false => ary
+                          | NONE => fold (consider_var_ary T) fun_var_Ts ary
+                      in
+                        Symtab.update_new (s,
+                            {pred_sym = pred_sym, min_ary = min_ary,
+                             max_ary = ary, types = [T], in_conj = conj_fact})
+                            sym_tab
+                      end)
+                 end
+             | IVar (_, T) => add_universal_var T accum
+             | IAbs ((_, T), tm) =>
+               accum |> add_universal_var T |> add_iterm_syms false tm
+             | _ => accum)
+            |> fold (add_iterm_syms false) args
+          end
+      in K (add_iterm_syms true) |> formula_fold NONE |> fact_lift end
+  in
+    ((false, []), Symtab.empty)
+    |> fold (add_fact_syms true) conjs
+    |> fold (add_fact_syms false) facts
+    |> snd
+    |> fold Symtab.update (default_sym_tab_entries type_enc)
+  end
 
 fun min_ary_of sym_tab s =
   case Symtab.lookup sym_tab s of
@@ -1883,12 +1892,15 @@
 
 fun sym_decl_table_for_facts ctxt format type_enc sym_tab (conjs, facts) =
   let
-    fun add_iterm_syms in_conj tm =
+    fun add_iterm_syms tm =
       let val (head, args) = strip_iterm_comb tm in
         (case head of
            IConst ((s, s'), T, T_args) =>
            let
-             val pred_sym = is_pred_sym sym_tab s
+             val (pred_sym, in_conj) =
+               case Symtab.lookup sym_tab s of
+                 SOME {pred_sym, in_conj, ...} => (pred_sym, in_conj)
+               | NONE => (false, false)
              val decl_sym =
                (case type_enc of
                   Guards _ => not pred_sym
@@ -1902,12 +1914,11 @@
              else
                I
            end
-         | IAbs (_, tm) => add_iterm_syms in_conj tm
+         | IAbs (_, tm) => add_iterm_syms tm
          | _ => I)
-        #> fold (add_iterm_syms in_conj) args
+        #> fold add_iterm_syms args
       end
-    fun add_fact_syms in_conj =
-      K (add_iterm_syms in_conj) |> formula_fold NONE |> fact_lift
+    val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> fact_lift
     fun add_formula_var_types (AQuant (_, xs, phi)) =
         fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
         #> add_formula_var_types phi
@@ -1937,8 +1948,7 @@
   in
     Symtab.empty
     |> is_type_enc_fairly_sound type_enc
-       ? (fold (add_fact_syms true) conjs
-          #> fold (add_fact_syms false) facts
+       ? (fold (fold add_fact_syms) [conjs, facts]
           #> (case type_enc of
                 Simple_Types (First_Order, Polymorphic, _) => add_TYPE_const ()
               | Simple_Types _ => I
@@ -2305,12 +2315,11 @@
       translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
                          hyp_ts concl_t facts
     val sym_tab =
-      conjs @ facts |> sym_table_for_facts ctxt type_enc explicit_apply
+      sym_table_for_facts ctxt type_enc explicit_apply conjs facts
     val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
     val firstorderize = firstorderize_fact thy format type_enc sym_tab
     val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
-    val sym_tab =
-      conjs @ facts |> sym_table_for_facts ctxt type_enc (SOME false)
+    val sym_tab = sym_table_for_facts ctxt type_enc (SOME false) conjs facts
     val helpers =
       sym_tab |> helper_facts_for_sym_table ctxt format type_enc
               |> map firstorderize