improved Nitpick's support for quotient types
authorblanchet
Tue Feb 23 11:05:32 2010 +0100 (2010-02-23)
changeset 353118f9a66fc9f80
parent 35309 997aa3a3e4bb
child 35312 99cd1f96b400
improved Nitpick's support for quotient types
src/HOL/Nitpick.thy
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/src/HOL/Nitpick.thy	Tue Feb 23 10:02:14 2010 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Tue Feb 23 11:05:32 2010 +0100
     1.3 @@ -36,7 +36,6 @@
     1.4             and bisim :: "bisim_iterator \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
     1.5             and bisim_iterator_max :: bisim_iterator
     1.6             and Quot :: "'a \<Rightarrow> 'b"
     1.7 -           and quot_normal :: "'a \<Rightarrow> 'a"
     1.8             and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
     1.9  
    1.10  datatype ('a, 'b) pair_box = PairBox 'a 'b
    1.11 @@ -237,11 +236,10 @@
    1.12  setup {* Nitpick_Isar.setup *}
    1.13  
    1.14  hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim 
    1.15 -    bisim_iterator_max Quot quot_normal Tha PairBox FunBox Word refl' wf'
    1.16 -    wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd
    1.17 -    int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac
    1.18 -    plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac
    1.19 -    of_frac
    1.20 +    bisim_iterator_max Quot Tha PairBox FunBox Word refl' wf' wf_wfrec wf_wfrec'
    1.21 +    wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac
    1.22 +    Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac plus_frac
    1.23 +    times_frac uminus_frac number_of_frac inverse_frac less_eq_frac of_frac
    1.24  hide (open) type bisim_iterator pair_box fun_box unsigned_bit signed_bit word
    1.25  hide (open) fact If_def Ex1_def rtrancl_def rtranclp_def tranclp_def refl'_def
    1.26      wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Feb 23 10:02:14 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Feb 23 11:05:32 2010 +0100
     2.3 @@ -54,6 +54,7 @@
     2.4    val numeral_prefix : string
     2.5    val ubfp_prefix : string
     2.6    val lbfp_prefix : string
     2.7 +  val quot_normal_prefix : string
     2.8    val skolem_prefix : string
     2.9    val special_prefix : string
    2.10    val uncurry_prefix : string
    2.11 @@ -173,7 +174,7 @@
    2.12    val inverse_axioms_for_rep_fun : theory -> styp -> term list
    2.13    val optimized_typedef_axioms : theory -> string * typ list -> term list
    2.14    val optimized_quot_type_axioms :
    2.15 -    theory -> (typ option * bool) list -> string * typ list -> term list
    2.16 +    Proof.context -> (typ option * bool) list -> string * typ list -> term list
    2.17    val def_of_const : theory -> const_table -> styp -> term option
    2.18    val fixpoint_kind_of_const :
    2.19      theory -> const_table -> string * typ -> fixpoint_kind
    2.20 @@ -268,6 +269,7 @@
    2.21  val step_prefix = nitpick_prefix ^ "step" ^ name_sep
    2.22  val ubfp_prefix = nitpick_prefix ^ "ubfp" ^ name_sep
    2.23  val lbfp_prefix = nitpick_prefix ^ "lbfp" ^ name_sep
    2.24 +val quot_normal_prefix = nitpick_prefix ^ "qn" ^ name_sep
    2.25  val skolem_prefix = nitpick_prefix ^ "sk"
    2.26  val special_prefix = nitpick_prefix ^ "sp"
    2.27  val uncurry_prefix = nitpick_prefix ^ "unc"
    2.28 @@ -277,6 +279,9 @@
    2.29  
    2.30  (* int -> string *)
    2.31  fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep
    2.32 +(* Proof.context -> typ -> string *)
    2.33 +fun quot_normal_name_for_type ctxt T =
    2.34 +  quot_normal_prefix ^ unyxml (Syntax.string_of_typ ctxt T)
    2.35  
    2.36  (* string -> string * string *)
    2.37  val strip_first_name_sep =
    2.38 @@ -559,14 +564,15 @@
    2.39  (* theory -> typ -> typ -> typ -> typ *)
    2.40  fun instantiate_type thy T1 T1' T2 =
    2.41    Same.commit (Envir.subst_type_same
    2.42 -                   (Sign.typ_match thy (Logic.varifyT T1, T1') Vartab.empty))
    2.43 -              (Logic.varifyT T2)
    2.44 +                   (Sign.typ_match thy (T1, T1') Vartab.empty)) T2
    2.45    handle Type.TYPE_MATCH =>
    2.46           raise TYPE ("Nitpick_HOL.instantiate_type", [T1, T1'], [])
    2.47 +fun varify_and_instantiate_type thy T1 T1' T2 =
    2.48 +  instantiate_type thy (Logic.varifyT T1) T1' (Logic.varifyT T2)
    2.49  
    2.50  (* theory -> typ -> typ -> styp *)
    2.51  fun repair_constr_type thy body_T' T =
    2.52 -  instantiate_type thy (body_type T) body_T' T
    2.53 +  varify_and_instantiate_type thy (body_type T) body_T' T
    2.54  
    2.55  (* string -> (string * string) list -> theory -> theory *)
    2.56  fun register_frac_type frac_s ersaetze thy =
    2.57 @@ -889,7 +895,8 @@
    2.58               [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
    2.59             else case typedef_info thy s of
    2.60               SOME {abs_type, rep_type, Abs_name, ...} =>
    2.61 -             [(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
    2.62 +             [(Abs_name,
    2.63 +               varify_and_instantiate_type thy abs_type T rep_type --> T)]
    2.64             | NONE =>
    2.65               if T = @{typ ind} then
    2.66                 [dest_Const @{const Zero_Rep}, dest_Const @{const Suc_Rep}]
    2.67 @@ -1385,7 +1392,7 @@
    2.68      else case typedef_info thy abs_s of
    2.69        SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} =>
    2.70        let
    2.71 -        val rep_T = instantiate_type thy abs_type abs_T rep_type
    2.72 +        val rep_T = varify_and_instantiate_type thy abs_type abs_T rep_type
    2.73          val rep_t = Const (Rep_name, abs_T --> rep_T)
    2.74          val set_t = Const (set_name, rep_T --> bool_T)
    2.75          val set_t' =
    2.76 @@ -1400,8 +1407,10 @@
    2.77        end
    2.78      | NONE => []
    2.79    end
    2.80 -fun optimized_quot_type_axioms thy stds abs_z =
    2.81 +(* Proof.context -> string * typ list -> term list *)
    2.82 +fun optimized_quot_type_axioms ctxt stds abs_z =
    2.83    let
    2.84 +    val thy = ProofContext.theory_of ctxt
    2.85      val abs_T = Type abs_z
    2.86      val rep_T = rep_type_for_quot_type thy abs_T
    2.87      val equiv_rel = equiv_relation_for_quot_type thy abs_T
    2.88 @@ -1410,7 +1419,7 @@
    2.89      val y_var = Var (("y", 0), rep_T)
    2.90      val x = (@{const_name Quot}, rep_T --> abs_T)
    2.91      val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T
    2.92 -    val normal_t = Const (@{const_name quot_normal}, rep_T --> rep_T)
    2.93 +    val normal_t = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T)
    2.94      val normal_x = normal_t $ x_var
    2.95      val normal_y = normal_t $ y_var
    2.96      val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T)
    2.97 @@ -1639,7 +1648,7 @@
    2.98                  in
    2.99                    (Abs (Name.uu, rep_T,
   2.100                          Const (@{const_name Quot}, rep_T --> abs_T)
   2.101 -                               $ (Const (@{const_name quot_normal},
   2.102 +                               $ (Const (quot_normal_name_for_type ctxt abs_T,
   2.103                                           rep_T --> rep_T) $ Bound 0)), ts)
   2.104                  end
   2.105                else if is_quot_rep_fun ctxt x then
   2.106 @@ -2230,6 +2239,10 @@
   2.107         else if String.isPrefix step_prefix s then
   2.108           (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T),
   2.109            format_type default_format default_format T)
   2.110 +       else if String.isPrefix quot_normal_prefix s then
   2.111 +         let val t = Const (nitpick_prefix ^ "normalize quotient type", T) in
   2.112 +           (t, format_term_type thy def_table formats t)
   2.113 +         end
   2.114         else if String.isPrefix skolem_prefix s then
   2.115           let
   2.116             val ss = the (AList.lookup (op =) (!skolems) s)
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Feb 23 10:02:14 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Feb 23 11:05:32 2010 +0100
     3.3 @@ -293,15 +293,15 @@
     3.4          $ do_term new_Ts old_Ts polar t2
     3.5        | Const (s as @{const_name The}, T) => do_description_operator s T
     3.6        | Const (s as @{const_name Eps}, T) => do_description_operator s T
     3.7 -      | Const (@{const_name quot_normal}, Type ("fun", [T, _])) =>
     3.8 -        let val T' = box_type hol_ctxt InFunLHS T in
     3.9 -          Const (@{const_name quot_normal}, T' --> T')
    3.10 -        end
    3.11        | Const (s as @{const_name Tha}, T) => do_description_operator s T
    3.12        | Const (x as (s, T)) =>
    3.13          Const (s, if s = @{const_name converse} orelse
    3.14                       s = @{const_name trancl} then
    3.15                      box_relational_operator_type T
    3.16 +                  else if String.isPrefix quot_normal_prefix s then
    3.17 +                    let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
    3.18 +                      T' --> T'
    3.19 +                    end
    3.20                    else if is_built_in_const thy stds fast_descrs x orelse
    3.21                            s = @{const_name Sigma} then
    3.22                      T
    3.23 @@ -1022,8 +1022,9 @@
    3.24  
    3.25  (* hol_context -> term -> (term list * term list) * (bool * bool) *)
    3.26  fun axioms_for_term
    3.27 -        (hol_ctxt as {thy, max_bisim_depth, stds, user_axioms, fast_descrs,
    3.28 -                      evals, def_table, nondef_table, user_nondefs, ...}) t =
    3.29 +        (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
    3.30 +                      fast_descrs, evals, def_table, nondef_table, user_nondefs,
    3.31 +                      ...}) t =
    3.32    let
    3.33      type accumulator = styp list * (term list * term list)
    3.34      (* (term list * term list -> term list)
    3.35 @@ -1134,7 +1135,8 @@
    3.36          #> (if is_pure_typedef thy T then
    3.37                fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
    3.38              else if is_quot_type thy T then
    3.39 -              fold (add_def_axiom depth) (optimized_quot_type_axioms thy stds z)
    3.40 +              fold (add_def_axiom depth)
    3.41 +                   (optimized_quot_type_axioms ctxt stds z)
    3.42              else if max_bisim_depth >= 0 andalso is_codatatype thy T then
    3.43                fold (add_maybe_def_axiom depth)
    3.44                     (codatatype_bisim_axioms hol_ctxt T)