460 |
460 |
461 fun unarize_type @{typ "unsigned_bit word"} = nat_T |
461 fun unarize_type @{typ "unsigned_bit word"} = nat_T |
462 | unarize_type @{typ "signed_bit word"} = int_T |
462 | unarize_type @{typ "signed_bit word"} = int_T |
463 | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts) |
463 | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts) |
464 | unarize_type T = T |
464 | unarize_type T = T |
465 fun unarize_unbox_etc_type (Type (@{type_name fin_fun}, Ts)) = |
465 fun unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) = |
466 unarize_unbox_etc_type (Type (@{type_name fun}, Ts)) |
|
467 | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) = |
|
468 unarize_unbox_etc_type (Type (@{type_name fun}, Ts)) |
466 unarize_unbox_etc_type (Type (@{type_name fun}, Ts)) |
469 | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) = |
467 | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) = |
470 Type (@{type_name prod}, map unarize_unbox_etc_type Ts) |
468 Type (@{type_name prod}, map unarize_unbox_etc_type Ts) |
471 | unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T |
469 | unarize_unbox_etc_type @{typ "unsigned_bit word"} = nat_T |
472 | unarize_unbox_etc_type @{typ "signed_bit word"} = int_T |
470 | unarize_unbox_etc_type @{typ "signed_bit word"} = int_T |
802 exists (fn (s', T') => s = s' andalso repair_constr_type ctxt co_T T' = T) |
800 exists (fn (s', T') => s = s' andalso repair_constr_type ctxt co_T T' = T) |
803 (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these) |
801 (AList.lookup (op =) codatatypes co_s |> Option.map snd |> these) |
804 end |
802 end |
805 | _ => false |
803 | _ => false |
806 fun is_constr_like ctxt (s, T) = |
804 fun is_constr_like ctxt (s, T) = |
807 member (op =) [@{const_name FinFun}, @{const_name FunBox}, |
805 member (op =) [@{const_name FunBox}, @{const_name PairBox}, |
808 @{const_name PairBox}, @{const_name Quot}, |
806 @{const_name Quot}, @{const_name Zero_Rep}, |
809 @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse |
807 @{const_name Suc_Rep}] s orelse |
810 let |
808 let |
811 val thy = ProofContext.theory_of ctxt |
809 val thy = ProofContext.theory_of ctxt |
812 val (x as (_, T)) = (s, unarize_unbox_etc_type T) |
810 val (x as (_, T)) = (s, unarize_unbox_etc_type T) |
813 in |
811 in |
814 is_real_constr thy x orelse is_record_constr x orelse |
812 is_real_constr thy x orelse is_record_constr x orelse |
1093 t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1 |
1091 t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1 |
1094 |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2) |
1092 |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2) |
1095 |> Envir.eta_contract |
1093 |> Envir.eta_contract |
1096 |> new_s <> @{type_name fun} |
1094 |> new_s <> @{type_name fun} |
1097 ? construct_value ctxt stds |
1095 ? construct_value ctxt stds |
1098 (if new_s = @{type_name fin_fun} then @{const_name FinFun} |
1096 (@{const_name FunBox}, |
1099 else @{const_name FunBox}, |
|
1100 Type (@{type_name fun}, new_Ts) --> new_T) |
1097 Type (@{type_name fun}, new_Ts) --> new_T) |
1101 o single |
1098 o single |
1102 | t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])) |
1099 | t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])) |
1103 | (Type (new_s, new_Ts as [new_T1, new_T2]), |
1100 | (Type (new_s, new_Ts as [new_T1, new_T2]), |
1104 Type (old_s, old_Ts as [old_T1, old_T2])) => |
1101 Type (old_s, old_Ts as [old_T1, old_T2])) => |
1105 if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse |
1102 if old_s = @{type_name fun_box} orelse |
1106 old_s = @{type_name pair_box} orelse old_s = @{type_name prod} then |
1103 old_s = @{type_name pair_box} orelse old_s = @{type_name prod} then |
1107 case constr_expand hol_ctxt old_T t of |
1104 case constr_expand hol_ctxt old_T t of |
1108 Const (old_s, _) $ t1 => |
1105 Const (old_s, _) $ t1 => |
1109 if new_s = @{type_name fun} then |
1106 if new_s = @{type_name fun} then |
1110 coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1 |
1107 coerce_term hol_ctxt Ts new_T (Type (@{type_name fun}, old_Ts)) t1 |