equivalence in code_dt data structure must respect both rty and qty
authorkuncar
Sat May 02 13:58:06 2015 +0200 (2015-05-02)
changeset 6023229ac1c6a1fbb
parent 60231 0daab758e087
child 60233 89d500d7e3eb
equivalence in code_dt data structure must respect both rty and qty
src/HOL/Tools/Lifting/lifting_def_code_dt.ML
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat May 02 13:58:06 2015 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat May 02 13:58:06 2015 +0200
     1.3 @@ -67,14 +67,15 @@
     1.4  fun wit_of_code_dt (CODE_DT code_dt) = #wit code_dt;
     1.5  fun wit_thm_of_code_dt (CODE_DT code_dt) = #wit_thm code_dt;
     1.6  fun rep_isom_data_of_code_dt (CODE_DT code_dt) = #rep_isom_data code_dt;
     1.7 -fun rty_equiv (T, U) = Type.raw_instance (T, U) andalso Type.raw_instance (U, T);
     1.8 -val code_dt_eq = rty_equiv o apply2 rty_of_code_dt;
     1.9 +fun ty_alpha_equiv (T, U) = Type.raw_instance (T, U) andalso Type.raw_instance (U, T);
    1.10 +fun code_dt_eq c = (ty_alpha_equiv o apply2 rty_of_code_dt) c 
    1.11 +  andalso (ty_alpha_equiv o apply2 qty_of_code_dt) c;
    1.12  fun term_of_code_dt code_dt = code_dt |> `rty_of_code_dt ||> qty_of_code_dt |> HOLogic.mk_prodT
    1.13    |> Net.encode_type |> single;
    1.14  
    1.15  (* modulo renaming, typ must contain TVars *)
    1.16  fun is_code_dt_of_type (rty, qty) code_dt = code_dt |> `rty_of_code_dt ||> qty_of_code_dt
    1.17 -  |> HOLogic.mk_prodT |> curry rty_equiv (HOLogic.mk_prodT (rty, qty));
    1.18 +  |> HOLogic.mk_prodT |> curry ty_alpha_equiv (HOLogic.mk_prodT (rty, qty));
    1.19  
    1.20  fun mk_rep_isom_data isom transfer bundle_name pointer =
    1.21    REP_ISOM { isom = isom, transfer = transfer, bundle_name = bundle_name, pointer = pointer}