reorder some steps in the construction to support mutual datatypes
authorkuncar
Sat May 02 13:58:06 2015 +0200 (2015-05-02)
changeset 602353cab6f891c2f
parent 60234 17ff843807cb
child 60236 865741686926
reorder some steps in the construction to support mutual datatypes
src/HOL/Tools/Lifting/lifting_def_code_dt.ML
src/HOL/Tools/Lifting/lifting_info.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 @@ -266,9 +266,13 @@
     1.4              val code_dt = the code_dt
     1.5              val rhs = dest_comb (rhs_of_lift_def lift_def) |> snd
     1.6              val rep_isom_data = code_dt |> rep_isom_data_of_code_dt |> the
     1.7 +            val pointer = pointer_of_rep_isom_data rep_isom_data
     1.8 +            val quot_active = 
     1.9 +              Lifting_Info.lookup_restore_data lthy pointer |> the |> #quotient |> #quot_thm
    1.10 +              |> Lifting_Info.lookup_quot_thm_quotients lthy |> is_some
    1.11              val qty_code_dt_bundle_name = bundle_name_of_rep_isom_data rep_isom_data
    1.12              val rep_isom = mk_rep_isom_of_code_dt qty_ret code_dt |> the
    1.13 -            val lthy = Bundle.includes [qty_code_dt_bundle_name] lthy
    1.14 +            val lthy = if quot_active then lthy else Bundle.includes [qty_code_dt_bundle_name] lthy
    1.15              fun qty_isom_of_rep_isom rep = rep |> dest_Const |> snd |> domain_type
    1.16              val qty_isom = qty_isom_of_rep_isom rep_isom
    1.17              val f'_var = (Binding.suffix_name "_aux" (fst var), NoSyn);
    1.18 @@ -303,7 +307,9 @@
    1.19              val lthy =  lthy
    1.20                |> Local_Theory.note ((Binding.empty, @{attributes [code]}), [f_alt_def])
    1.21                |> snd
    1.22 -              |> Lifting_Setup.lifting_forget (pointer_of_rep_isom_data rep_isom_data)
    1.23 +              (* if processing a mutual datatype (there is a cycle!) the corresponding quotient 
    1.24 +                 will be needed later and will be forgotten later *)
    1.25 +              |> (if quot_active then I else Lifting_Setup.lifting_forget pointer)
    1.26            in
    1.27              (ret_lift_def, lthy)
    1.28            end
    1.29 @@ -311,6 +317,32 @@
    1.30      end
    1.31  and mk_rep_isom qty_isom_bundle (rty, qty, qty_isom) lthy =
    1.32    let
    1.33 +    (* logical definition of qty qty_isom isomorphism *) 
    1.34 +    val uTname = unique_Tname (rty, qty)
    1.35 +    fun eq_onp_to_top_tac ctxt = SELECT_GOAL (Local_Defs.unfold_tac ctxt 
    1.36 +      (@{thm eq_onp_top_eq_eq[symmetric]} :: Lifting_Info.get_relator_eq_onp_rules ctxt))
    1.37 +    fun lift_isom_tac ctxt = HEADGOAL (eq_onp_to_top_tac ctxt
    1.38 +      THEN' (rtac @{thm id_transfer}));
    1.39 +
    1.40 +    val (rep_isom_lift_def, lthy) = lift_def ld_no_notes (Binding.qualified true "Rep_isom" uTname, NoSyn)
    1.41 +      (qty_isom --> qty) (HOLogic.id_const rty) lift_isom_tac [] lthy
    1.42 +      |> apfst (inst_of_lift_def lthy (qty_isom --> qty));
    1.43 +    val (abs_isom, lthy) = lift_def ld_no_notes (Binding.qualified true "Abs_isom" uTname, NoSyn)
    1.44 +      (qty --> qty_isom) (HOLogic.id_const rty) lift_isom_tac [] lthy
    1.45 +      |> apfst (mk_lift_const_of_lift_def (qty --> qty_isom));
    1.46 +    val rep_isom = lift_const_of_lift_def rep_isom_lift_def
    1.47 +
    1.48 +    val pointer = Lifting_Setup.pointer_of_bundle_binding lthy qty_isom_bundle
    1.49 +    fun code_dt phi context = code_dt_of lthy (rty, qty) |> the |>
    1.50 +      update_rep_isom rep_isom (transfer_rules_of_lift_def rep_isom_lift_def |> hd)
    1.51 +       (bundle_name_of_bundle_binding qty_isom_bundle phi context) pointer;
    1.52 +    val lthy = lthy  
    1.53 +      |> Local_Theory.declaration {syntax = false, pervasive = true}
    1.54 +        (fn phi => fn context => Data.map (Item_Net.update (morph_code_dt phi (code_dt phi context))) context)
    1.55 +      |> Local_Theory.restore
    1.56 +
    1.57 +    (* in order to make the qty qty_isom isomorphism executable we have to define discriminators 
    1.58 +      and selectors for qty_isom *)
    1.59      val (rty_name, typs) = dest_Type rty
    1.60      val (_, qty_typs) = dest_Type qty
    1.61      val fp = BNF_FP_Def_Sugar.fp_sugar_of lthy rty_name
    1.62 @@ -364,16 +396,12 @@
    1.63      val sel_rhs = map (map mk_sel_rhs) sel_argss
    1.64      val dis_rhs = map (fn k => list_comb (dis_casex, mk_dis_case_args (ks ~~ xss) k)) ks
    1.65      val dis_qty = qty_isom --> HOLogic.boolT;
    1.66 -    val uTname = unique_Tname (rty, qty)
    1.67      val dis_names = map (fn k => Binding.qualified true ("dis" ^ string_of_int k) uTname) ks;
    1.68  
    1.69      val (diss, lthy) = @{fold_map 2} (fn b => fn rhs => fn lthy =>
    1.70        lift_def ld_no_notes (b, NoSyn) dis_qty rhs (K all_tac) [] lthy
    1.71        |> apfst (mk_lift_const_of_lift_def dis_qty)) dis_names dis_rhs lthy
    1.72  
    1.73 -    fun eq_onp_to_top_tac ctxt = SELECT_GOAL (Local_Defs.unfold_tac ctxt 
    1.74 -      (@{thm eq_onp_top_eq_eq[symmetric]} :: Lifting_Info.get_relator_eq_onp_rules ctxt))
    1.75 -
    1.76      val unfold_lift_sel_rsp = @{lemma "(\<And>x. P1 x \<Longrightarrow> P2 (f x)) \<Longrightarrow> (rel_fun (eq_onp P1) (eq_onp P2)) f f"
    1.77        by (simp add: eq_onp_same_args rel_fun_eq_onp_rel)}
    1.78  
    1.79 @@ -394,23 +422,13 @@
    1.80          (b, NoSyn) (qty_isom --> qty_ret) rhs (HEADGOAL o sel_tac wits) [] lthy
    1.81        |> apfst (mk_lift_const_of_lift_def (qty_isom --> qty_ret)))) sel_names sel_rhs lthy
    1.82  
    1.83 -    fun lift_isom_tac ctxt = HEADGOAL (eq_onp_to_top_tac ctxt
    1.84 -      THEN' (rtac @{thm id_transfer}));
    1.85 -
    1.86 -    val (rep_isom_lift_def, lthy) = lift_def ld_no_notes (Binding.qualified true "Rep_isom" uTname, NoSyn)
    1.87 -      (qty_isom --> qty) (HOLogic.id_const rty) lift_isom_tac [] lthy
    1.88 -      |> apfst (inst_of_lift_def lthy (qty_isom --> qty));
    1.89 -    val (abs_isom, lthy) = lift_def ld_no_notes (Binding.qualified true "Abs_isom" uTname, NoSyn)
    1.90 -      (qty --> qty_isom) (HOLogic.id_const rty) lift_isom_tac [] lthy
    1.91 -      |> apfst (mk_lift_const_of_lift_def (qty --> qty_isom));
    1.92 +    (* now we can execute the qty qty_isom isomorphism *)
    1.93      fun mk_type_definition newT oldT RepC AbsC A =
    1.94        let
    1.95          val typedefC =
    1.96            Const (@{const_name type_definition},
    1.97              (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
    1.98        in typedefC $ RepC $ AbsC $ A end;
    1.99 -
   1.100 -    val rep_isom = lift_const_of_lift_def rep_isom_lift_def
   1.101      val typedef_goal = mk_type_definition qty_isom qty rep_isom abs_isom (HOLogic.mk_UNIV qty) |>
   1.102        HOLogic.mk_Trueprop;
   1.103      fun typ_isom_tac ctxt i =
   1.104 @@ -431,7 +449,6 @@
   1.105        |> singleton (Variable.export transfer_lthy lthy)
   1.106        |> (fn thm => @{thm UNIV_typedef_to_Quotient} OF [thm, @{thm reflexive}])
   1.107      val qty_isom_name = Tname qty_isom;
   1.108 -    
   1.109      val quot_isom_rep =
   1.110        let
   1.111          val (quotients : Lifting_Term.quotients) = Symtab.insert (Lifting_Info.quotient_eq) (qty_isom_name,
   1.112 @@ -442,7 +459,6 @@
   1.113            ctxt (rty, qty) () |> fst |> Lifting_Term.force_qty_type ctxt qty
   1.114            |> quot_thm_rep
   1.115        end;
   1.116 -
   1.117      val x_lthy = lthy
   1.118      val (x, lthy) = yield_singleton (mk_Frees "x") qty_isom lthy;
   1.119  
   1.120 @@ -513,16 +529,9 @@
   1.121        |> Thm.close_derivation
   1.122        |> singleton(Variable.export lthy x_lthy)
   1.123      val lthy = x_lthy
   1.124 -    val pointer = Lifting_Setup.pointer_of_bundle_binding lthy qty_isom_bundle
   1.125 -    fun code_dt phi context = code_dt_of lthy (rty, qty) |> the |>
   1.126 -      update_rep_isom rep_isom (transfer_rules_of_lift_def rep_isom_lift_def |> hd)
   1.127 -       (bundle_name_of_bundle_binding qty_isom_bundle phi context) pointer;
   1.128      val lthy =
   1.129        lthy
   1.130        |> snd o Local_Theory.note ((Binding.empty, @{attributes [code]}), [rep_isom_code])
   1.131 -      |> Local_Theory.declaration {syntax = false, pervasive = true}
   1.132 -        (fn phi => fn context => Data.map (Item_Net.update (morph_code_dt phi (code_dt phi context))) context)
   1.133 -      |> Local_Theory.restore
   1.134        |> Lifting_Setup.lifting_forget pointer
   1.135    in
   1.136      ((selss, diss, rep_isom_code), lthy)
   1.137 @@ -710,6 +719,21 @@
   1.138      rename term new_names
   1.139    end
   1.140  
   1.141 +fun quot_thm_err ctxt (rty, qty) pretty_msg =
   1.142 +  let
   1.143 +    val error_msg = cat_lines
   1.144 +       ["Lifting failed for the following types:",
   1.145 +        Pretty.string_of (Pretty.block
   1.146 +         [Pretty.str "Raw type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty]),
   1.147 +        Pretty.string_of (Pretty.block
   1.148 +         [Pretty.str "Abstract type:", Pretty.brk 2, Syntax.pretty_typ ctxt qty]),
   1.149 +        "",
   1.150 +        (Pretty.string_of (Pretty.block
   1.151 +         [Pretty.str "Reason:", Pretty.brk 2, pretty_msg]))]
   1.152 +  in
   1.153 +    error error_msg
   1.154 +  end
   1.155 +
   1.156  fun lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy =
   1.157    let
   1.158      val config = evaluate_params params
   1.159 @@ -742,21 +766,6 @@
   1.160      Proof.theorem NONE (snd oo after_qed) [map (rpair []) (the_list goal)] lthy
   1.161    end
   1.162  
   1.163 -fun quot_thm_err ctxt (rty, qty) pretty_msg =
   1.164 -  let
   1.165 -    val error_msg = cat_lines
   1.166 -       ["Lifting failed for the following types:",
   1.167 -        Pretty.string_of (Pretty.block
   1.168 -         [Pretty.str "Raw type:", Pretty.brk 2, Syntax.pretty_typ ctxt rty]),
   1.169 -        Pretty.string_of (Pretty.block
   1.170 -         [Pretty.str "Abstract type:", Pretty.brk 2, Syntax.pretty_typ ctxt qty]),
   1.171 -        "",
   1.172 -        (Pretty.string_of (Pretty.block
   1.173 -         [Pretty.str "Reason:", Pretty.brk 2, pretty_msg]))]
   1.174 -  in
   1.175 -    error error_msg
   1.176 -  end
   1.177 -
   1.178  fun check_rty_err ctxt (rty_schematic, rty_forced) (raw_var, rhs_raw) =
   1.179    let
   1.180      val (_, ctxt') = yield_singleton Proof_Context.read_vars raw_var ctxt
     2.1 --- a/src/HOL/Tools/Lifting/lifting_info.ML	Sat May 02 13:58:06 2015 +0200
     2.2 +++ b/src/HOL/Tools/Lifting/lifting_info.ML	Sat May 02 13:58:06 2015 +0200
     2.3 @@ -16,6 +16,7 @@
     2.4    val quotient_eq: quotient * quotient -> bool
     2.5    val transform_quotient: morphism -> quotient -> quotient
     2.6    val lookup_quotients: Proof.context -> string -> quotient option
     2.7 +  val lookup_quot_thm_quotients: Proof.context -> thm -> quotient option
     2.8    val update_quotients: string -> quotient -> Context.generic -> Context.generic
     2.9    val delete_quotients: thm -> Context.generic -> Context.generic
    2.10    val print_quotients: Proof.context -> unit
    2.11 @@ -221,6 +222,17 @@
    2.12  
    2.13  fun lookup_quotients ctxt type_name = Symtab.lookup (get_quotients ctxt) type_name
    2.14  
    2.15 +fun lookup_quot_thm_quotients ctxt quot_thm =
    2.16 +  let
    2.17 +    val (_, qtyp) = quot_thm_rty_qty quot_thm
    2.18 +    val qty_full_name = (fst o dest_Type) qtyp
    2.19 +    fun compare_data (data:quotient) = Thm.eq_thm_prop (#quot_thm data, quot_thm)
    2.20 +  in
    2.21 +    case lookup_quotients ctxt qty_full_name of
    2.22 +      SOME quotient => if compare_data quotient then SOME quotient else NONE
    2.23 +      | NONE => NONE
    2.24 +  end
    2.25 +
    2.26  fun update_quotients type_name qinfo ctxt = 
    2.27    Data.map (map_quotients (Symtab.update (type_name, qinfo))) ctxt
    2.28  
    2.29 @@ -228,10 +240,8 @@
    2.30    let
    2.31      val (_, qtyp) = quot_thm_rty_qty quot_thm
    2.32      val qty_full_name = (fst o dest_Type) qtyp
    2.33 -    val symtab = get_quotients' ctxt
    2.34 -    fun compare_data (_, data:quotient) = Thm.eq_thm_prop (#quot_thm data, quot_thm)
    2.35    in
    2.36 -    if Symtab.member compare_data symtab (qty_full_name, quot_thm)
    2.37 +    if is_some (lookup_quot_thm_quotients (Context.proof_of ctxt) quot_thm)
    2.38        then Data.map (map_quotients (Symtab.delete qty_full_name)) ctxt
    2.39        else ctxt
    2.40    end