src/HOL/Tools/Lifting/lifting_term.ML
changeset 60222 78fc1b798c61
parent 60217 40c63ffce97f
child 60239 755e11e2e15d
     1.1 --- a/src/HOL/Tools/Lifting/lifting_term.ML	Tue Nov 18 16:19:57 2014 +0100
     1.2 +++ b/src/HOL/Tools/Lifting/lifting_term.ML	Tue Nov 18 16:19:57 2014 +0100
     1.3 @@ -14,9 +14,12 @@
     1.4    type 'a fold_quot_thm = { constr: typ -> thm * 'a -> thm * 'a, lift: typ -> thm * 'a -> thm * 'a, 
     1.5    comp_lift: typ -> thm * 'a -> thm * 'a }
     1.6  
     1.7 +  type quotients = Lifting_Info.quotient Symtab.table
     1.8 +  
     1.9    val force_qty_type: Proof.context -> typ -> thm -> thm
    1.10  
    1.11 -  val prove_schematic_quot_thm: 'a fold_quot_thm -> Proof.context -> typ * typ -> 'a -> thm * 'a
    1.12 +  val prove_schematic_quot_thm: 'a fold_quot_thm -> quotients -> Proof.context -> 
    1.13 +    typ * typ -> 'a -> thm * 'a
    1.14  
    1.15    val instantiate_rtys: Proof.context -> typ * typ -> typ * typ
    1.16  
    1.17 @@ -47,6 +50,8 @@
    1.18  exception MERGE_TRANSFER_REL of Pretty.T
    1.19  exception CHECK_RTY of typ * typ
    1.20  
    1.21 +type quotients = Lifting_Info.quotient Symtab.table
    1.22 +
    1.23  fun match ctxt err ty_pat ty =
    1.24    let
    1.25      val thy = Proof_Context.theory_of ctxt
    1.26 @@ -68,43 +73,43 @@
    1.27         Pretty.str "don't match."])
    1.28    end
    1.29  
    1.30 -fun get_quot_data ctxt s =
    1.31 -  case Lifting_Info.lookup_quotients ctxt s of
    1.32 +fun get_quot_data quotients s =
    1.33 +  case Symtab.lookup quotients s of
    1.34      SOME qdata => qdata
    1.35    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    1.36      [Pretty.str ("No quotient type " ^ quote s), 
    1.37       Pretty.brk 1, 
    1.38       Pretty.str "found."])
    1.39  
    1.40 -fun get_quot_thm ctxt s =
    1.41 +fun get_quot_thm quotients ctxt s =
    1.42    let
    1.43      val thy = Proof_Context.theory_of ctxt
    1.44    in
    1.45 -    Thm.transfer thy (#quot_thm (get_quot_data ctxt s))
    1.46 +    Thm.transfer thy (#quot_thm (get_quot_data quotients s))
    1.47    end
    1.48  
    1.49 -fun has_pcrel_info ctxt s = is_some (#pcr_info (get_quot_data ctxt s))
    1.50 +fun has_pcrel_info quotients s = is_some (#pcr_info (get_quot_data quotients s))
    1.51  
    1.52 -fun get_pcrel_info ctxt s =
    1.53 -  case #pcr_info (get_quot_data ctxt s) of
    1.54 +fun get_pcrel_info quotients s =
    1.55 +  case #pcr_info (get_quot_data quotients s) of
    1.56      SOME pcr_info => pcr_info
    1.57    | NONE => raise QUOT_THM_INTERNAL (Pretty.block 
    1.58      [Pretty.str ("No parametrized correspondce relation for " ^ quote s), 
    1.59       Pretty.brk 1, 
    1.60       Pretty.str "found."])
    1.61  
    1.62 -fun get_pcrel_def ctxt s =
    1.63 +fun get_pcrel_def quotients ctxt s =
    1.64    let
    1.65      val thy = Proof_Context.theory_of ctxt
    1.66    in
    1.67 -    Thm.transfer thy (#pcrel_def (get_pcrel_info ctxt s))
    1.68 +    Thm.transfer thy (#pcrel_def (get_pcrel_info quotients s))
    1.69    end
    1.70  
    1.71 -fun get_pcr_cr_eq ctxt s =
    1.72 +fun get_pcr_cr_eq quotients ctxt s =
    1.73    let
    1.74      val thy = Proof_Context.theory_of ctxt
    1.75    in
    1.76 -    Thm.transfer thy (#pcr_cr_eq (get_pcrel_info ctxt s))
    1.77 +    Thm.transfer thy (#pcr_cr_eq (get_pcrel_info quotients s))
    1.78    end
    1.79  
    1.80  fun get_rel_quot_thm ctxt s =
    1.81 @@ -195,11 +200,12 @@
    1.82            rel_quot_thm_prems
    1.83        end
    1.84  
    1.85 -fun rty_is_TVar ctxt qty = (is_TVar o fst o quot_thm_rty_qty o get_quot_thm ctxt o Tname) qty
    1.86 +fun gen_rty_is_TVar quotients ctxt qty = qty |> Tname |> get_quot_thm quotients ctxt |> 
    1.87 +  quot_thm_rty_qty |> fst |> is_TVar
    1.88  
    1.89 -fun instantiate_rtys ctxt (rty, (qty as Type (qty_name, _))) =
    1.90 +fun gen_instantiate_rtys quotients ctxt (rty, (qty as Type (qty_name, _))) =
    1.91    let
    1.92 -    val quot_thm = get_quot_thm ctxt qty_name
    1.93 +    val quot_thm = get_quot_thm quotients ctxt qty_name
    1.94      val (rty_pat, qty_pat) = quot_thm_rty_qty quot_thm
    1.95  
    1.96      fun inst_rty (Type (s, tys), Type (s', tys')) = 
    1.97 @@ -223,32 +229,35 @@
    1.98    in
    1.99      (inst_rty (rty_pat, rty), Envir.subst_type qtyenv rty_pat)
   1.100    end
   1.101 -  | instantiate_rtys _ _ = error "instantiate_rtys: not Type"
   1.102 +  | gen_instantiate_rtys _ _ _ = error "gen_instantiate_rtys: not Type"
   1.103 +
   1.104 +fun instantiate_rtys ctxt (rty, qty) = 
   1.105 +  gen_instantiate_rtys (Lifting_Info.get_quotients ctxt) ctxt (rty, qty)
   1.106  
   1.107  type 'a fold_quot_thm = { constr: typ -> thm * 'a -> thm * 'a, lift: typ -> thm * 'a -> thm * 'a, 
   1.108    comp_lift: typ -> thm * 'a -> thm * 'a }
   1.109  
   1.110 -fun prove_schematic_quot_thm actions ctxt (rty, qty) fold_val =
   1.111 +fun prove_schematic_quot_thm actions quotients ctxt (rty, qty) fold_val =
   1.112    let
   1.113      fun lifting_step (rty, qty) =
   1.114        let
   1.115 -        val (rty', rtyq) = instantiate_rtys ctxt (rty, qty)
   1.116 -        val (rty's, rtyqs) = if rty_is_TVar ctxt qty then ([rty'],[rtyq]) 
   1.117 +        val (rty', rtyq) = gen_instantiate_rtys quotients ctxt (rty, qty)
   1.118 +        val (rty's, rtyqs) = if gen_rty_is_TVar quotients ctxt qty then ([rty'],[rtyq]) 
   1.119            else (Targs rty', Targs rtyq) 
   1.120          val (args, fold_val) = 
   1.121 -          fold_map (prove_schematic_quot_thm actions ctxt) (rty's ~~ rtyqs) fold_val
   1.122 +          fold_map (prove_schematic_quot_thm actions quotients ctxt) (rty's ~~ rtyqs) fold_val
   1.123        in
   1.124          if forall is_id_quot args
   1.125          then
   1.126            let
   1.127 -            val quot_thm = get_quot_thm ctxt (Tname qty)
   1.128 +            val quot_thm = get_quot_thm quotients ctxt (Tname qty)
   1.129            in
   1.130              #lift actions qty (quot_thm, fold_val)
   1.131            end
   1.132          else
   1.133            let
   1.134 -            val quot_thm = get_quot_thm ctxt (Tname qty)
   1.135 -            val rel_quot_thm = if rty_is_TVar ctxt qty then the_single args else
   1.136 +            val quot_thm = get_quot_thm quotients ctxt (Tname qty)
   1.137 +            val rel_quot_thm = if gen_rty_is_TVar quotients ctxt qty then the_single args else
   1.138                args MRSL (get_rel_quot_thm ctxt (Tname rty))
   1.139              val comp_quot_thm = [rel_quot_thm, quot_thm] MRSL @{thm Quotient_compose}
   1.140            in
   1.141 @@ -262,7 +271,8 @@
   1.142          then
   1.143            let
   1.144              val (args, fold_val) = 
   1.145 -              fold_map (prove_schematic_quot_thm actions ctxt) (zip_Tvars ctxt s tys tys') fold_val
   1.146 +              fold_map (prove_schematic_quot_thm actions quotients ctxt) 
   1.147 +                (zip_Tvars ctxt s tys tys') fold_val
   1.148            in
   1.149              if forall is_id_quot args
   1.150              then
   1.151 @@ -277,7 +287,7 @@
   1.152          else
   1.153            lifting_step (rty, qty)
   1.154        | (_, Type (s', tys')) => 
   1.155 -        (case try (get_quot_thm ctxt) s' of
   1.156 +        (case try (get_quot_thm quotients ctxt) s' of
   1.157            SOME quot_thm => 
   1.158              let
   1.159                val rty_pat = (fst o quot_thm_rty_qty) quot_thm
   1.160 @@ -288,7 +298,7 @@
   1.161              let                                               
   1.162                val rty_pat = Type (s', map (fn _ => TFree ("a",[])) tys')
   1.163              in
   1.164 -              prove_schematic_quot_thm actions ctxt (rty_pat, qty) fold_val
   1.165 +              prove_schematic_quot_thm actions quotients ctxt (rty_pat, qty) fold_val
   1.166              end)
   1.167        | _ => (@{thm identity_quotient}, fold_val)
   1.168        )
   1.169 @@ -330,8 +340,9 @@
   1.170  in
   1.171    fun prove_quot_thm ctxt (rty, qty) =
   1.172      let
   1.173 -      val (schematic_quot_thm, _) = prove_schematic_quot_thm id_actions ctxt (rty, qty) ()
   1.174 -    val quot_thm = force_qty_type ctxt qty schematic_quot_thm
   1.175 +      val quotients = Lifting_Info.get_quotients ctxt
   1.176 +      val (schematic_quot_thm, _) = prove_schematic_quot_thm id_actions quotients ctxt (rty, qty) ()
   1.177 +      val quot_thm = force_qty_type ctxt qty schematic_quot_thm
   1.178        val _ = check_rty_type ctxt rty quot_thm
   1.179      in
   1.180        quot_thm
   1.181 @@ -476,17 +487,7 @@
   1.182    fun rewrs_imp rules = first_imp (map rewr_imp rules)
   1.183  in
   1.184  
   1.185 -  (*
   1.186 -    ctm - of the form "[POS|NEG] (par_R OO T) t f) ?X", where par_R is a parametricity transfer 
   1.187 -    relation for t and T is a transfer relation between t and f, which consists only from
   1.188 -    parametrized transfer relations (i.e., pcr_?) and equalities op=. POS or NEG encodes
   1.189 -    co-variance or contra-variance.
   1.190 -    
   1.191 -    The function merges par_R OO T using definitions of parametrized correspondence relations
   1.192 -    (e.g., (rel_S R) OO (pcr_T op=) --> pcr_T R using the definition pcr_T R = (rel_S R) OO cr_T).
   1.193 -  *)
   1.194 -
   1.195 -  fun merge_transfer_relations ctxt ctm =
   1.196 +  fun gen_merge_transfer_relations quotients ctxt ctm =
   1.197      let
   1.198        val ctm = Thm.dest_arg ctm
   1.199        val tm = Thm.term_of ctm
   1.200 @@ -534,19 +535,21 @@
   1.201                  in
   1.202                    case distr_rule of
   1.203                      NONE => raise MERGE_TRANSFER_REL (cannot_merge_error_msg ())
   1.204 -                    | SOME distr_rule =>  (map (merge_transfer_relations ctxt) (cprems_of distr_rule)) 
   1.205 +                    | SOME distr_rule =>  (map (gen_merge_transfer_relations quotients ctxt) 
   1.206 +                                            (cprems_of distr_rule)) 
   1.207                        MRSL distr_rule
   1.208                  end
   1.209                else
   1.210                  let 
   1.211 -                  val pcrel_def = get_pcrel_def ctxt ((fst o dest_Type) qty)
   1.212 +                  val pcrel_def = get_pcrel_def quotients ctxt ((fst o dest_Type) qty)
   1.213                    val pcrel_const = (head_of o fst o Logic.dest_equals o Thm.prop_of) pcrel_def
   1.214                  in
   1.215                    if same_constants pcrel_const (head_of trans_rel) then
   1.216                      let
   1.217                        val unfolded_ctm = Thm.rhs_of (Conv.arg1_conv (Conv.arg_conv (Conv.rewr_conv pcrel_def)) ctm)
   1.218                        val distr_rule = rewrs_imp @{thms POS_pcr_rule NEG_pcr_rule} unfolded_ctm
   1.219 -                      val result = (map (merge_transfer_relations ctxt) (cprems_of distr_rule)) MRSL distr_rule
   1.220 +                      val result = (map (gen_merge_transfer_relations quotients ctxt) 
   1.221 +                        (cprems_of distr_rule)) MRSL distr_rule
   1.222                        val fold_pcr_rel = Conv.rewr_conv (Thm.symmetric pcrel_def)
   1.223                      in  
   1.224                        Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.combination_conv 
   1.225 @@ -558,17 +561,22 @@
   1.226              end
   1.227      end
   1.228      handle QUOT_THM_INTERNAL pretty_msg => raise MERGE_TRANSFER_REL pretty_msg
   1.229 +
   1.230 +  (*
   1.231 +    ctm - of the form "[POS|NEG] (par_R OO T) t f) ?X", where par_R is a parametricity transfer 
   1.232 +    relation for t and T is a transfer relation between t and f, which consists only from
   1.233 +    parametrized transfer relations (i.e., pcr_?) and equalities op=. POS or NEG encodes
   1.234 +    co-variance or contra-variance.
   1.235 +    
   1.236 +    The function merges par_R OO T using definitions of parametrized correspondence relations
   1.237 +    (e.g., (rel_S R) OO (pcr_T op=) --> pcr_T R using the definition pcr_T R = (rel_S R) OO cr_T).
   1.238 +  *)
   1.239 +
   1.240 +  fun merge_transfer_relations ctxt ctm = gen_merge_transfer_relations 
   1.241 +    (Lifting_Info.get_quotients ctxt) ctxt ctm
   1.242  end
   1.243  
   1.244 -(*
   1.245 -  It replaces cr_T by pcr_T op= in the transfer relation. For composed
   1.246 -  abstract types, it replaces T_rel R OO cr_T by pcr_T R. If the parametrized
   1.247 -  correspondce relation does not exist, the original relation is kept.
   1.248 -
   1.249 -  thm - a transfer rule
   1.250 -*)
   1.251 -
   1.252 -fun parametrize_transfer_rule ctxt thm =
   1.253 +fun gen_parametrize_transfer_rule quotients ctxt thm =
   1.254    let
   1.255      fun parametrize_relation_conv ctm =
   1.256        let
   1.257 @@ -585,21 +593,21 @@
   1.258                val q = (fst o dest_Type) qty
   1.259              in
   1.260                let
   1.261 -                val (rty', rtyq) = instantiate_rtys ctxt (rty, qty)
   1.262 -                val (rty's, rtyqs) = if rty_is_TVar ctxt qty then ([rty'],[rtyq]) 
   1.263 +                val (rty', rtyq) = gen_instantiate_rtys quotients ctxt (rty, qty)
   1.264 +                val (rty's, rtyqs) = if gen_rty_is_TVar quotients ctxt qty then ([rty'],[rtyq]) 
   1.265                    else (Targs rty', Targs rtyq)
   1.266                in
   1.267                  if forall op= (rty's ~~ rtyqs) then
   1.268                    let
   1.269 -                    val pcr_cr_eq = (Thm.symmetric o mk_meta_eq) (get_pcr_cr_eq ctxt q)
   1.270 +                    val pcr_cr_eq = (Thm.symmetric o mk_meta_eq) (get_pcr_cr_eq quotients ctxt q)
   1.271                    in      
   1.272                      Conv.rewr_conv pcr_cr_eq ctm
   1.273                    end
   1.274                    handle QUOT_THM_INTERNAL _ => Conv.all_conv ctm
   1.275                  else
   1.276 -                  if has_pcrel_info ctxt q then
   1.277 +                  if has_pcrel_info quotients q then
   1.278                      let 
   1.279 -                      val pcrel_def = Thm.symmetric (get_pcrel_def ctxt q)
   1.280 +                      val pcrel_def = Thm.symmetric (get_pcrel_def quotients ctxt q)
   1.281                      in
   1.282                        (Conv.rewr_conv pcrel_def then_conv all_args_conv parametrize_relation_conv) ctm
   1.283                      end
   1.284 @@ -611,4 +619,16 @@
   1.285      in
   1.286        Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.fun2_conv parametrize_relation_conv)) thm
   1.287      end
   1.288 +
   1.289 +(*
   1.290 +  It replaces cr_T by pcr_T op= in the transfer relation. For composed
   1.291 +  abstract types, it replaces T_rel R OO cr_T by pcr_T R. If the parametrized
   1.292 +  correspondce relation does not exist, the original relation is kept.
   1.293 +
   1.294 +  thm - a transfer rule
   1.295 +*)
   1.296 +
   1.297 +fun parametrize_transfer_rule ctxt thm = 
   1.298 +  gen_parametrize_transfer_rule (Lifting_Info.get_quotients ctxt) ctxt thm
   1.299 +
   1.300  end