src/HOL/Tools/Lifting/lifting_def_code_dt.ML
changeset 60231 0daab758e087
parent 60230 4857d553c52c
child 60232 29ac1c6a1fbb
     1.1 --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Mon Apr 13 15:27:34 2015 +0200
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Sat May 02 13:58:06 2015 +0200
     1.3 @@ -46,8 +46,10 @@
     1.4  
     1.5  structure Lifting_Def_Code_Dt: LIFTING_DEF_CODE_DT =
     1.6  struct
     1.7 +                                                                       
     1.8 +open Ctr_Sugar_Util BNF_Util BNF_FP_Util BNF_FP_Def_Sugar Lifting_Def Lifting_Util
     1.9  
    1.10 -open Ctr_Sugar_Util BNF_Util BNF_FP_Util BNF_FP_Def_Sugar Lifting_Def Lifting_Util
    1.11 +infix 0 MRSL
    1.12  
    1.13  (** data structures **)
    1.14  
    1.15 @@ -272,7 +274,7 @@
    1.16              val f'_qty = strip_type qty |> fst |> rpair qty_isom |> op --->
    1.17              val f'_rsp_rel = Lifting_Term.equiv_relation lthy (rty, f'_qty);
    1.18              val rsp = rsp_thm_of_lift_def lift_def
    1.19 -            val rel_eq_onps_conv = HOLogic.Trueprop_conv (ret_rel_conv (R_conv rel_eq_onps))
    1.20 +            val rel_eq_onps_conv = HOLogic.Trueprop_conv (Conv.fun2_conv (ret_rel_conv (R_conv rel_eq_onps)))
    1.21              val rsp_norm = Conv.fconv_rule rel_eq_onps_conv rsp
    1.22              val f'_rsp_goal = HOLogic.mk_Trueprop (f'_rsp_rel $ rhs $ rhs);
    1.23              val f'_rsp = Goal.prove_sorry lthy [] [] f'_rsp_goal
    1.24 @@ -366,20 +368,31 @@
    1.25        lift_def ld_no_notes (b, NoSyn) dis_qty rhs (K all_tac) [] lthy
    1.26        |> apfst (mk_lift_const_of_lift_def dis_qty)) dis_names dis_rhs lthy
    1.27  
    1.28 +    fun eq_onp_to_top_tac ctxt = SELECT_GOAL (Local_Defs.unfold_tac ctxt 
    1.29 +      (@{thm eq_onp_top_eq_eq[symmetric]} :: Lifting_Info.get_relator_eq_onp_rules ctxt))
    1.30 +
    1.31 +    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.32 +      by (simp add: eq_onp_same_args rel_fun_eq_onp_rel)}
    1.33 +
    1.34      fun lift_sel_tac exhaust_rule dt_rules wits ctxt i =
    1.35 -      (Method.insert_tac wits THEN' case_tac exhaust_rule ctxt THEN_ALL_NEW (
    1.36 -      EVERY' [hyp_subst_tac ctxt, Raw_Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules),
    1.37 +        (Method.insert_tac wits THEN' 
    1.38 +         eq_onp_to_top_tac ctxt THEN' (* normalize *)
    1.39 +         rtac unfold_lift_sel_rsp THEN'
    1.40 +         case_tac exhaust_rule ctxt THEN_ALL_NEW (
    1.41 +        EVERY' [hyp_subst_tac ctxt, (* does not kill wits because = was rewritten to eq_onp top *)
    1.42 +        Raw_Simplifier.rewrite_goal_tac ctxt (map safe_mk_meta_eq dt_rules), 
    1.43          REPEAT_DETERM o etac conjE, atac])) i
    1.44      val pred_simps = Transfer.lookup_pred_data lthy (Tname rty) |> the |> Transfer.pred_simps
    1.45      val sel_tac = lift_sel_tac (#exhaust ctr_sugar) (#case_thms ctr_sugar @ pred_simps)
    1.46      val sel_names = map (fn (k, xs) => map (fn k' => Binding.qualified true
    1.47        ("sel" ^ string_of_int k ^ string_of_int k') uTname) (1 upto length xs)) (ks ~~ ctr_Tss);
    1.48      val (selss, lthy) = @{fold_map 2} (@{fold_map 2} (fn b => fn ((_, qty_ret), wits, rhs) => fn lthy =>
    1.49 -      lift_def_code_dt { code_dt = true, lift_config = ld_no_notes }
    1.50 +        lift_def_code_dt { code_dt = true, lift_config = ld_no_notes }
    1.51          (b, NoSyn) (qty_isom --> qty_ret) rhs (HEADGOAL o sel_tac wits) [] lthy
    1.52        |> apfst (mk_lift_const_of_lift_def (qty_isom --> qty_ret)))) sel_names sel_rhs lthy
    1.53  
    1.54 -    fun lift_isom_tac ctxt = Local_Defs.unfold_tac ctxt [id_apply] THEN HEADGOAL atac;
    1.55 +    fun lift_isom_tac ctxt = HEADGOAL (eq_onp_to_top_tac ctxt
    1.56 +      THEN' (rtac @{thm id_transfer}));
    1.57  
    1.58      val (rep_isom_lift_def, lthy) = lift_def ld_no_notes (Binding.qualified true "Rep_isom" uTname, NoSyn)
    1.59        (qty_isom --> qty) (HOLogic.id_const rty) lift_isom_tac [] lthy
    1.60 @@ -387,7 +400,6 @@
    1.61      val (abs_isom, lthy) = lift_def ld_no_notes (Binding.qualified true "Abs_isom" uTname, NoSyn)
    1.62        (qty --> qty_isom) (HOLogic.id_const rty) lift_isom_tac [] lthy
    1.63        |> apfst (mk_lift_const_of_lift_def (qty --> qty_isom));
    1.64 -
    1.65      fun mk_type_definition newT oldT RepC AbsC A =
    1.66        let
    1.67          val typedefC =
    1.68 @@ -398,12 +410,13 @@
    1.69      val rep_isom = lift_const_of_lift_def rep_isom_lift_def
    1.70      val typedef_goal = mk_type_definition qty_isom qty rep_isom abs_isom (HOLogic.mk_UNIV qty) |>
    1.71        HOLogic.mk_Trueprop;
    1.72 -
    1.73 -      fun typ_isom_tac ctxt i =
    1.74 -        EVERY' [ SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms type_definition_def}),
    1.75 -          DETERM o Transfer.transfer_tac true ctxt, Raw_Simplifier.rewrite_goal_tac ctxt
    1.76 -            (map safe_mk_meta_eq @{thms id_apply simp_thms Ball_def}),
    1.77 -           rtac TrueI] i;
    1.78 +    fun typ_isom_tac ctxt i =
    1.79 +      EVERY' [ SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms type_definition_def}),
    1.80 +        DETERM o Transfer.transfer_tac true ctxt,
    1.81 +          SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms eq_onp_top_eq_eq}) (* normalize *), 
    1.82 +          Raw_Simplifier.rewrite_goal_tac ctxt 
    1.83 +          (map safe_mk_meta_eq @{thms id_apply simp_thms Ball_def}),
    1.84 +         rtac TrueI] i;
    1.85  
    1.86      val (_, transfer_lthy) = Proof_Context.note_thmss "" [((Binding.empty, []),
    1.87        [(@{thms right_total_UNIV_transfer},[Transfer.transfer_add]),
    1.88 @@ -414,9 +427,8 @@
    1.89        |> Thm.close_derivation
    1.90        |> singleton (Variable.export transfer_lthy lthy)
    1.91        |> (fn thm => @{thm UNIV_typedef_to_Quotient} OF [thm, @{thm reflexive}])
    1.92 -
    1.93      val qty_isom_name = Tname qty_isom;
    1.94 -
    1.95 +    
    1.96      val quot_isom_rep =
    1.97        let
    1.98          val (quotients : Lifting_Term.quotients) = Symtab.insert (Lifting_Info.quotient_eq) (qty_isom_name,
    1.99 @@ -485,7 +497,6 @@
   1.100        (fn {context = ctxt, prems = _} => rep_isom_code_tac ctr_sugar ctxt 1)
   1.101        |> Thm.close_derivation
   1.102        |> singleton(Variable.export lthy x_lthy)
   1.103 -
   1.104      val lthy = x_lthy
   1.105      val pointer = Lifting_Setup.pointer_of_bundle_binding lthy qty_isom_bundle
   1.106      fun code_dt phi context = code_dt_of lthy (rty, qty) |> the |>
   1.107 @@ -510,6 +521,7 @@
   1.108      val pred_data = if is_some pred_data then the pred_data
   1.109        else error ("code_dt: " ^ quote rty_name ^ " is not a datatype.")
   1.110      val rel_eq_onp = safe_mk_meta_eq (Transfer.rel_eq_onp pred_data);
   1.111 +    val rel_eq_onps = insert Thm.eq_thm rel_eq_onp rel_eq_onps
   1.112      val R_conv = Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}
   1.113        then_conv Conv.rewr_conv rel_eq_onp
   1.114      val quot_thm = Conv.fconv_rule(HOLogic.Trueprop_conv (Quotient_R_conv R_conv)) quot_thm;
   1.115 @@ -522,12 +534,12 @@
   1.116          val TFrees = Term.add_tfreesT qty []
   1.117  
   1.118          fun non_empty_typedef_tac non_empty_pred ctxt i =
   1.119 -          (SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' rtac non_empty_pred) i
   1.120 -
   1.121 +          (Method.insert_tac [non_empty_pred] THEN' 
   1.122 +            SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' atac) i
   1.123          val uTname = unique_Tname (rty, qty)
   1.124          val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty));
   1.125          val ((_, tcode_dt), lthy) = conceal_naming_result (typedef (Binding.concealed uTname, TFrees, NoSyn)
   1.126 -          Tdef_set NONE (fn lthy => non_empty_typedef_tac non_empty_pred lthy 1)) lthy;
   1.127 +          Tdef_set NONE (fn lthy => HEADGOAL (non_empty_typedef_tac non_empty_pred lthy))) lthy;
   1.128          val type_definition_thm = tcode_dt |> snd |> #type_definition;
   1.129          val qty_isom = tcode_dt |> fst |> #abs_type;
   1.130  
   1.131 @@ -542,10 +554,10 @@
   1.132            |> Local_Theory.restore
   1.133            |> mk_rep_isom binding (rty, qty, qty_isom) |> snd
   1.134        in
   1.135 -        (quot_thm, (lthy, rel_eq_onp :: rel_eq_onps))
   1.136 +        (quot_thm, (lthy, rel_eq_onps))
   1.137        end
   1.138      else
   1.139 -      (quot_thm, (lthy, rel_eq_onp :: rel_eq_onps))
   1.140 +      (quot_thm, (lthy, rel_eq_onps))
   1.141    end
   1.142  and lift_def_code_dt config var qty rhs tac par_thms lthy = gen_lift_def (add_lift_def_code_dt config)
   1.143    var qty rhs tac par_thms lthy
   1.144 @@ -577,6 +589,112 @@
   1.145  
   1.146  **)
   1.147  
   1.148 +local
   1.149 +  val eq_onp_assms_tac_fixed_rules = map (Transfer.prep_transfer_domain_thm @{context})
   1.150 +    [@{thm pcr_Domainp_total}, @{thm pcr_Domainp_par_left_total}, @{thm pcr_Domainp_par}, 
   1.151 +      @{thm pcr_Domainp}]
   1.152 +in
   1.153 +fun mk_readable_rsp_thm_eq tm lthy =
   1.154 +  let
   1.155 +    val ctm = Thm.cterm_of lthy tm
   1.156 +    
   1.157 +    fun assms_rewr_conv tactic rule ct =
   1.158 +      let
   1.159 +        fun prove_extra_assms thm =
   1.160 +          let
   1.161 +            val assms = cprems_of thm
   1.162 +            fun finish thm = if Thm.no_prems thm then SOME (Goal.conclude thm) else NONE
   1.163 +            fun prove ctm = Option.mapPartial finish (SINGLE tactic (Goal.init ctm))
   1.164 +          in
   1.165 +            map_interrupt prove assms
   1.166 +          end
   1.167 +    
   1.168 +        fun cconl_of thm = Drule.strip_imp_concl (Thm.cprop_of thm)
   1.169 +        fun lhs_of thm = fst (Thm.dest_equals (cconl_of thm))
   1.170 +        fun rhs_of thm = snd (Thm.dest_equals (cconl_of thm))
   1.171 +        val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule;
   1.172 +        val lhs = lhs_of rule1;
   1.173 +        val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1;
   1.174 +        val rule3 =
   1.175 +          Thm.instantiate (Thm.match (lhs, ct)) rule2
   1.176 +            handle Pattern.MATCH => raise CTERM ("assms_rewr_conv", [lhs, ct]);
   1.177 +        val proved_assms = prove_extra_assms rule3
   1.178 +      in
   1.179 +        case proved_assms of
   1.180 +          SOME proved_assms =>
   1.181 +            let
   1.182 +              val rule3 = proved_assms MRSL rule3
   1.183 +              val rule4 =
   1.184 +                if lhs_of rule3 aconvc ct then rule3
   1.185 +                else
   1.186 +                  let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
   1.187 +                  in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (rhs_of rule3)) end
   1.188 +            in Thm.transitive rule4 (Thm.beta_conversion true (rhs_of rule4)) end
   1.189 +          | NONE => Conv.no_conv ct
   1.190 +      end
   1.191 +
   1.192 +    fun assms_rewrs_conv tactic rules = Conv.first_conv (map (assms_rewr_conv tactic) rules)
   1.193 +
   1.194 +    fun simp_arrows_conv ctm =
   1.195 +      let
   1.196 +        val unfold_conv = Conv.rewrs_conv 
   1.197 +          [@{thm rel_fun_eq_eq_onp[THEN eq_reflection]}, 
   1.198 +            @{thm rel_fun_eq_onp_rel[THEN eq_reflection]},
   1.199 +            @{thm rel_fun_eq[THEN eq_reflection]},
   1.200 +            @{thm rel_fun_eq_rel[THEN eq_reflection]}, 
   1.201 +            @{thm rel_fun_def[THEN eq_reflection]}]
   1.202 +        fun binop_conv2 cv1 cv2 = Conv.combination_conv (Conv.arg_conv cv1) cv2
   1.203 +        val eq_onp_assms_tac_rules = @{thm left_unique_OO} :: 
   1.204 +            eq_onp_assms_tac_fixed_rules @ (Transfer.get_transfer_raw lthy)
   1.205 +        val intro_top_rule = @{thm eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}
   1.206 +        val kill_tops = Transfer.top_sweep_rewr_conv [@{thm eq_onp_top_eq_eq[THEN eq_reflection]}]
   1.207 +        val eq_onp_assms_tac = (CONVERSION kill_tops THEN' 
   1.208 +          TRY o REPEAT_ALL_NEW (resolve_tac lthy eq_onp_assms_tac_rules) 
   1.209 +          THEN_ALL_NEW (DETERM o Transfer.eq_tac lthy)) 1
   1.210 +        val relator_eq_onp_conv = Conv.bottom_conv
   1.211 +          (K (Conv.try_conv (assms_rewrs_conv eq_onp_assms_tac
   1.212 +            (intro_top_rule :: Lifting_Info.get_relator_eq_onp_rules lthy)))) lthy
   1.213 +          then_conv kill_tops
   1.214 +        val relator_eq_conv = Conv.bottom_conv
   1.215 +          (K (Conv.try_conv (Conv.rewrs_conv (Transfer.get_relator_eq lthy)))) lthy
   1.216 +      in
   1.217 +        case (Thm.term_of ctm) of
   1.218 +          Const (@{const_name "rel_fun"}, _) $ _ $ _ => 
   1.219 +            (binop_conv2 simp_arrows_conv simp_arrows_conv then_conv unfold_conv) ctm
   1.220 +          | _ => (relator_eq_onp_conv then_conv relator_eq_conv) ctm
   1.221 +      end
   1.222 +    
   1.223 +    val unfold_ret_val_invs = Conv.bottom_conv 
   1.224 +      (K (Conv.try_conv (Conv.rewr_conv @{thm eq_onp_same_args[THEN eq_reflection]}))) lthy
   1.225 +    val unfold_inv_conv = 
   1.226 +      Conv.top_sweep_conv (K (Conv.rewr_conv @{thm eq_onp_def[THEN eq_reflection]})) lthy
   1.227 +    val simp_conv = HOLogic.Trueprop_conv (Conv.fun2_conv simp_arrows_conv)
   1.228 +    val univq_conv = Conv.rewr_conv @{thm HOL.all_simps(6)[symmetric, THEN eq_reflection]}
   1.229 +    val univq_prenex_conv = Conv.top_conv (K (Conv.try_conv univq_conv)) lthy
   1.230 +    val beta_conv = Thm.beta_conversion true
   1.231 +    val eq_thm = 
   1.232 +      (simp_conv then_conv univq_prenex_conv then_conv beta_conv then_conv unfold_ret_val_invs
   1.233 +         then_conv unfold_inv_conv) ctm
   1.234 +  in
   1.235 +    Object_Logic.rulify lthy (eq_thm RS Drule.equal_elim_rule2)
   1.236 +  end
   1.237 +end
   1.238 +
   1.239 +fun rename_to_tnames ctxt term =
   1.240 +  let
   1.241 +    fun all_typs (Const (@{const_name Pure.all}, _) $ Abs (_, T, t)) = T :: all_typs t
   1.242 +      | all_typs _ = []
   1.243 +
   1.244 +    fun rename (Const (@{const_name Pure.all}, T1) $ Abs (_, T2, t)) (new_name :: names) = 
   1.245 +        (Const (@{const_name Pure.all}, T1) $ Abs (new_name, T2, rename t names)) 
   1.246 +      | rename t _ = t
   1.247 +
   1.248 +    val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
   1.249 +    val new_names = Old_Datatype_Prop.make_tnames (all_typs fixed_def_t)
   1.250 +  in
   1.251 +    rename term new_names
   1.252 +  end
   1.253 +
   1.254  fun lift_def_cmd (params, raw_var, rhs_raw, par_xthms) lthy =
   1.255    let
   1.256      val config = evaluate_params params
   1.257 @@ -585,6 +703,26 @@
   1.258      val rhs = (Syntax.check_term lthy o Syntax.parse_term lthy) rhs_raw
   1.259      val par_thms = Attrib.eval_thms lthy par_xthms
   1.260      val (goal, after_qed) = prepare_lift_def (add_lift_def_code_dt config) var qty rhs par_thms lthy
   1.261 +    val (goal, after_qed) =
   1.262 +      case goal of
   1.263 +        NONE => (goal, K (after_qed Drule.dummy_thm))
   1.264 +        | SOME prsp_tm =>
   1.265 +          let
   1.266 +            val readable_rsp_thm_eq = mk_readable_rsp_thm_eq prsp_tm lthy
   1.267 +            val (readable_rsp_tm, _) = Logic.dest_implies (Thm.prop_of readable_rsp_thm_eq)
   1.268 +            val readable_rsp_tm_tnames = rename_to_tnames lthy readable_rsp_tm
   1.269 +        
   1.270 +            fun after_qed' [[thm]] lthy = 
   1.271 +              let
   1.272 +                val internal_rsp_thm = Goal.prove lthy [] [] prsp_tm 
   1.273 +                    (fn {context = ctxt, ...} =>
   1.274 +                      rtac readable_rsp_thm_eq 1 THEN Proof_Context.fact_tac ctxt [thm] 1)
   1.275 +              in
   1.276 +                after_qed internal_rsp_thm lthy
   1.277 +              end
   1.278 +          in
   1.279 +            (SOME readable_rsp_tm_tnames, after_qed')
   1.280 +          end 
   1.281    in
   1.282      Proof.theorem NONE (snd oo after_qed) [map (rpair []) (the_list goal)] lthy
   1.283    end