src/HOL/Tools/ATP/atp_translate.ML
changeset 44625 4a1132815a70
parent 44624 b82085db501f
child 44626 a40b713232c8
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 31 11:23:16 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Aug 31 11:52:03 2011 +0200
     1.3 @@ -367,17 +367,17 @@
     1.4  
     1.5  (** Isabelle arities **)
     1.6  
     1.7 -type arity_literal = name * name * name list
     1.8 +type arity_atom = name * name * name list
     1.9  
    1.10  val type_class = the_single @{sort type}
    1.11  
    1.12 -fun add_packed_sort tvar =
    1.13 -  fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
    1.14 -
    1.15  type arity_clause =
    1.16    {name : string,
    1.17 -   prem_lits : arity_literal list,
    1.18 -   concl_lit : arity_literal}
    1.19 +   prem_atoms : arity_atom list,
    1.20 +   concl_atom : arity_atom}
    1.21 +
    1.22 +fun add_prem_atom tvar =
    1.23 +  fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
    1.24  
    1.25  (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
    1.26  fun make_axiom_arity_clause (tcons, name, (cls, args)) =
    1.27 @@ -386,9 +386,9 @@
    1.28      val tvars_srts = ListPair.zip (tvars, args)
    1.29    in
    1.30      {name = name,
    1.31 -     prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts,
    1.32 -     concl_lit = (`make_type_class cls, `make_fixed_type_const tcons,
    1.33 -                  tvars ~~ tvars)}
    1.34 +     prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
    1.35 +     concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
    1.36 +                   tvars ~~ tvars)}
    1.37    end
    1.38  
    1.39  fun arity_clause _ _ (_, []) = []
    1.40 @@ -715,7 +715,7 @@
    1.41                Explicit_Type_Args)
    1.42      end
    1.43  
    1.44 -(* Make literals for sorted type variables. *)
    1.45 +(* Make atoms for sorted type variables. *)
    1.46  fun generic_add_sorts_on_type (_, []) = I
    1.47    | generic_add_sorts_on_type ((x, i), s :: ss) =
    1.48      generic_add_sorts_on_type ((x, i), ss)
    1.49 @@ -731,8 +731,24 @@
    1.50  fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
    1.51    | add_sorts_on_tvar _ = I
    1.52  
    1.53 -fun type_literals_for_types type_enc add_sorts_on_typ Ts =
    1.54 +val tvar_a_str = "'a"
    1.55 +val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
    1.56 +val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
    1.57 +val itself_name = `make_fixed_type_const @{type_name itself}
    1.58 +val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
    1.59 +val tvar_a_atype = AType (tvar_a_name, [])
    1.60 +val a_itself_atype = AType (itself_name, [tvar_a_atype])
    1.61 +
    1.62 +fun type_class_formula type_enc class arg =
    1.63 +  AAtom (ATerm (class, arg ::
    1.64 +      (case type_enc of
    1.65 +         Simple_Types (_, Polymorphic, _) =>
    1.66 +         if exploit_tff1_dummy_type_vars then [] else [ATerm (TYPE_name, [arg])]
    1.67 +       | _ => [])))
    1.68 +fun formulas_for_types type_enc add_sorts_on_typ Ts =
    1.69    [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
    1.70 +     |> map (fn (class, name) =>
    1.71 +                type_class_formula type_enc class (ATerm (name, [])))
    1.72  
    1.73  fun mk_aconns c phis =
    1.74    let val (phis', phi') = split_last phis in
    1.75 @@ -1273,14 +1289,6 @@
    1.76    K (add_iterm_syms_to_table ctxt explicit_apply)
    1.77    |> formula_fold NONE |> fact_lift
    1.78  
    1.79 -val tvar_a_str = "'a"
    1.80 -val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
    1.81 -val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
    1.82 -val itself_name = `make_fixed_type_const @{type_name itself}
    1.83 -val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
    1.84 -val tvar_a_atype = AType (tvar_a_name, [])
    1.85 -val a_itself_atype = AType (itself_name, [tvar_a_atype])
    1.86 -
    1.87  val default_sym_tab_entries : (string * sym_info) list =
    1.88    (prefixed_predicator_name,
    1.89     {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
    1.90 @@ -1453,22 +1461,8 @@
    1.91     (("If", true), @{thms if_True if_False True_or_False})]
    1.92    |> map (apsnd (map zero_var_indexes))
    1.93  
    1.94 -fun type_class_aterm type_enc class arg =
    1.95 -  case type_enc of
    1.96 -    Simple_Types (_, Polymorphic, _) =>
    1.97 -    if exploit_tff1_dummy_type_vars then ATerm (class, [arg])
    1.98 -    else ATerm (class, [arg, ATerm (TYPE_name, [arg])])
    1.99 -  | _ => ATerm (class, [arg])
   1.100 -
   1.101 -fun fo_literal_from_type_literal type_enc (class, name) =
   1.102 -  (true, type_class_aterm type_enc class (ATerm (name, [])))
   1.103 -
   1.104 -fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
   1.105 -
   1.106 -fun bound_tvars type_enc Ts =
   1.107 -  mk_ahorn (map (formula_from_fo_literal
   1.108 -                 o fo_literal_from_type_literal type_enc)
   1.109 -                (type_literals_for_types type_enc add_sorts_on_tvar Ts))
   1.110 +fun bound_tvars type_enc =
   1.111 +  mk_ahorn o formulas_for_types type_enc add_sorts_on_tvar
   1.112  
   1.113  fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
   1.114    (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
   1.115 @@ -1750,22 +1744,20 @@
   1.116    let val ty_arg = ATerm (tvar_a_name, []) in
   1.117      Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
   1.118               AConn (AImplies,
   1.119 -                    [AAtom (type_class_aterm type_enc subclass ty_arg),
   1.120 -                     AAtom (type_class_aterm type_enc superclass ty_arg)])
   1.121 +                    [type_class_formula type_enc subclass ty_arg,
   1.122 +                     type_class_formula type_enc superclass ty_arg])
   1.123               |> close_formula_universally type_enc, isabelle_info introN, NONE)
   1.124    end
   1.125  
   1.126 -fun fo_literal_from_arity_literal type_enc (class, t, args) =
   1.127 -  (true, type_class_aterm type_enc class
   1.128 -                          (ATerm (t, map (fn arg => ATerm (arg, [])) args)))
   1.129 +fun formula_from_arity_atom type_enc (class, t, args) =
   1.130 +  ATerm (t, map (fn arg => ATerm (arg, [])) args)
   1.131 +  |> type_class_formula type_enc class
   1.132  
   1.133  fun formula_line_for_arity_clause type_enc
   1.134 -        ({name, prem_lits, concl_lit, ...} : arity_clause) =
   1.135 +        ({name, prem_atoms, concl_atom, ...} : arity_clause) =
   1.136    Formula (arity_clause_prefix ^ name, Axiom,
   1.137 -           mk_ahorn (map (formula_from_fo_literal
   1.138 -                          o fo_literal_from_arity_literal type_enc) prem_lits)
   1.139 -                    (formula_from_fo_literal
   1.140 -                         (fo_literal_from_arity_literal type_enc concl_lit))
   1.141 +           mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
   1.142 +                    (formula_from_arity_atom type_enc concl_atom)
   1.143             |> close_formula_universally type_enc, isabelle_info introN, NONE)
   1.144  
   1.145  fun formula_line_for_conjecture ctxt format mono type_enc
   1.146 @@ -1777,18 +1769,14 @@
   1.147             |> bound_tvars type_enc atomic_types
   1.148             |> close_formula_universally type_enc, NONE, NONE)
   1.149  
   1.150 -fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
   1.151 -  atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
   1.152 -               |> map (fo_literal_from_type_literal type_enc)
   1.153 -
   1.154 -fun formula_line_for_free_type j lit =
   1.155 -  Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
   1.156 -           formula_from_fo_literal lit, NONE, NONE)
   1.157 +fun formula_line_for_free_type j phi =
   1.158 +  Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE)
   1.159  fun formula_lines_for_free_types type_enc facts =
   1.160    let
   1.161 -    val litss = map (free_type_literals type_enc) facts
   1.162 -    val lits = fold (union (op =)) litss []
   1.163 -  in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
   1.164 +    val phis =
   1.165 +      fold (union (op =)) (map #atomic_types facts) []
   1.166 +      |> formulas_for_types type_enc add_sorts_on_tfree
   1.167 +  in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
   1.168  
   1.169  (** Symbol declarations **)
   1.170