src/HOL/Tools/Transfer/transfer_bnf.ML
author blanchet
Mon, 08 Sep 2014 19:21:07 +0200
changeset 58234 265aea1e9985
parent 58230 61e4c96bf2b6
child 58356 2f04f1fd28aa
permissions -rw-r--r--
honour sorts in N2M
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
     1
(*  Title:      HOL/Tools/Transfer/transfer_bnf.ML
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
     2
    Author:     Ondrej Kuncar, TU Muenchen
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
     3
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
     4
Setup for Transfer for types that are BNF.
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
     5
*)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
     6
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
     7
signature TRANSFER_BNF =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
     8
sig
58191
b3c71d630777 pretend code generation is a ctr_sugar plugin
blanchet
parents: 58186
diff changeset
     9
  val transfer_plugin: string
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    10
  val base_name_of_bnf: BNF_Def.bnf -> binding
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    11
  val type_name_of_bnf: BNF_Def.bnf -> string
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    12
  val lookup_defined_pred_data: Proof.context -> string -> Transfer.pred_data
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    13
  val bnf_only_type_ctr: (BNF_Def.bnf -> 'a -> 'a) -> BNF_Def.bnf -> 'a -> 'a
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    14
end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    15
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    16
structure Transfer_BNF : TRANSFER_BNF =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    17
struct
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    18
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    19
open BNF_Util
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    20
open BNF_Def
56651
fc105315822a localize new size function generation code
blanchet
parents: 56648
diff changeset
    21
open BNF_FP_Util
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    22
open BNF_FP_Def_Sugar
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    23
58191
b3c71d630777 pretend code generation is a ctr_sugar plugin
blanchet
parents: 58186
diff changeset
    24
val transfer_plugin = "transfer"
58186
a6c3962ea907 named interpretations
blanchet
parents: 58179
diff changeset
    25
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    26
(* util functions *)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    27
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    28
fun base_name_of_bnf bnf = Binding.name (Binding.name_of (name_of_bnf bnf))
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    29
fun mk_Frees_free x Ts ctxt = Variable.variant_frees ctxt [] (mk_names (length Ts) x ~~ Ts) |> map Free
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    30
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    31
fun mk_Domainp P =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    32
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    33
    val PT = fastype_of P
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    34
    val argT = hd (binder_types PT)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    35
  in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    36
    Const (@{const_name Domainp}, PT --> argT --> HOLogic.boolT) $ P
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    37
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    38
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    39
fun mk_pred pred_def args T =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    40
  let
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
    41
    val pred_name = pred_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    42
      |> head_of |> fst o dest_Const
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    43
    val argsT = map fastype_of args
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    44
  in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    45
    list_comb (Const (pred_name, argsT ---> (T --> HOLogic.boolT)), args)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    46
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    47
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
    48
fun mk_eq_onp arg =
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    49
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    50
    val argT = domain_type (fastype_of arg)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    51
  in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    52
    Const (@{const_name eq_onp}, (argT --> HOLogic.boolT) --> argT --> argT --> HOLogic.boolT)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    53
      $ arg
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    54
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    55
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    56
fun subst_conv thm =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    57
  Conv.top_sweep_conv (K (Conv.rewr_conv (safe_mk_meta_eq thm))) @{context}
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    58
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    59
fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    60
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    61
fun is_Type (Type _) = true
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    62
  | is_Type _ = false
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    63
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    64
fun bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    65
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    66
fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    67
56648
2ffa440b3074 manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents: 56538
diff changeset
    68
fun fp_sugar_only_type_ctr f fp_sugars =
2ffa440b3074 manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents: 56538
diff changeset
    69
  (case filter (is_Type o T_of_bnf o bnf_of_fp_sugar) fp_sugars of
2ffa440b3074 manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents: 56538
diff changeset
    70
    [] => I
2ffa440b3074 manual merge + added 'rel_distincts' field to record for symmetry
blanchet
parents: 56538
diff changeset
    71
  | fp_sugars' => f fp_sugars')
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    72
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    73
(* relation constraints - bi_total & co. *)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    74
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    75
fun mk_relation_constraint name arg =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    76
  (Const (name, fastype_of arg --> HOLogic.boolT)) $ arg
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    77
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
    78
fun side_constraint_tac bnf constr_defs ctxt i =
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    79
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    80
    val thms = constr_defs @ map mk_sym [rel_eq_of_bnf bnf, rel_conversep_of_bnf bnf,
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    81
      rel_OO_of_bnf bnf]
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
    82
  in
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    83
    (SELECT_GOAL (Local_Defs.unfold_tac ctxt thms) THEN' rtac (rel_mono_of_bnf bnf)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    84
      THEN_ALL_NEW atac) i
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    85
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    86
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
    87
fun bi_constraint_tac constr_iff sided_constr_intros ctxt i =
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
    88
  (SELECT_GOAL (Local_Defs.unfold_tac ctxt [constr_iff]) THEN'
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    89
    CONJ_WRAP' (fn thm => rtac thm THEN_ALL_NEW (REPEAT_DETERM o etac conjE THEN' atac)) sided_constr_intros) i
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    90
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    91
fun generate_relation_constraint_goal ctxt bnf constraint_def =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    92
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    93
    val constr_name = constraint_def |> prop_of |> HOLogic.dest_Trueprop |> fst o HOLogic.dest_eq
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    94
      |> head_of |> fst o dest_Const
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    95
    val live = live_of_bnf bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    96
    val (((As, Bs), Ds), ctxt) = ctxt
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    97
      |> mk_TFrees live
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    98
      ||>> mk_TFrees live
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
    99
      ||>> mk_TFrees (dead_of_bnf bnf)
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   100
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   101
    val relator = mk_rel_of_bnf Ds As Bs bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   102
    val relsT = map2 mk_pred2T As Bs
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   103
    val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   104
    val concl = HOLogic.mk_Trueprop (mk_relation_constraint constr_name (list_comb (relator, args)))
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   105
    val assms = map (HOLogic.mk_Trueprop o (mk_relation_constraint constr_name)) args
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   106
    val goal = Logic.list_implies (assms, concl)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   107
  in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   108
    (goal, ctxt)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   109
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   110
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   111
fun prove_relation_side_constraint ctxt bnf constraint_def =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   112
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   113
    val old_ctxt = ctxt
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   114
    val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
57890
1e13f63fb452 use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
traytel
parents: 57399
diff changeset
   115
    val thm = Goal.prove_sorry ctxt [] [] goal
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   116
      (fn {context = ctxt, prems = _} => side_constraint_tac bnf [constraint_def] ctxt 1)
57890
1e13f63fb452 use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
traytel
parents: 57399
diff changeset
   117
      |> Thm.close_derivation
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   118
  in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   119
    Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   120
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   121
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   122
fun prove_relation_bi_constraint ctxt bnf constraint_def side_constraints =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   123
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   124
    val old_ctxt = ctxt
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   125
    val (goal, ctxt) = generate_relation_constraint_goal ctxt bnf constraint_def
57890
1e13f63fb452 use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
traytel
parents: 57399
diff changeset
   126
    val thm = Goal.prove_sorry ctxt [] [] goal
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   127
      (fn {context = ctxt, prems = _} => bi_constraint_tac constraint_def side_constraints ctxt 1)
57890
1e13f63fb452 use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
traytel
parents: 57399
diff changeset
   128
      |> Thm.close_derivation
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   129
  in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   130
    Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   131
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   132
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   133
val defs = [("left_total_rel", @{thm left_total_alt_def}), ("right_total_rel", @{thm right_total_alt_def}),
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   134
  ("left_unique_rel", @{thm left_unique_alt_def}), ("right_unique_rel", @{thm right_unique_alt_def})]
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   135
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   136
fun prove_relation_constraints bnf lthy =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   137
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   138
    val transfer_attr = @{attributes [transfer_rule]}
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   139
    val Tname = base_name_of_bnf bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   140
    fun qualify suffix = Binding.qualified true suffix Tname
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   141
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   142
    val defs = map (apsnd (prove_relation_side_constraint lthy bnf)) defs
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   143
    val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def}
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   144
      [snd (nth defs 0), snd (nth defs 1)]
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   145
    val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def}
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   146
      [snd (nth defs 2), snd (nth defs 3)]
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   147
    val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   148
    val notes = maps (fn (name, thm) => [((qualify name, []), [([thm], transfer_attr)])]) defs
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   149
  in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   150
    notes
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   151
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   152
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   153
(* relator_eq *)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   154
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   155
fun relator_eq bnf =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   156
  [((Binding.empty, []), [([rel_eq_of_bnf bnf], @{attributes [relator_eq]})])]
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   157
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   158
(* predicator definition and Domainp and eq_onp theorem *)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   159
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   160
fun define_pred bnf lthy =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   161
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   162
    fun mk_pred_name c = Binding.prefix_name "pred_" c
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   163
    val live = live_of_bnf bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   164
    val Tname = base_name_of_bnf bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   165
    val ((As, Ds), lthy) = lthy
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   166
      |> mk_TFrees live
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   167
      ||>> mk_TFrees (dead_of_bnf bnf)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   168
    val T = mk_T_of_bnf Ds As bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   169
    val sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   170
    val argTs = map mk_pred1T As
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   171
    val args = mk_Frees_free "P" argTs lthy
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   172
    val conjs = map (fn (set, arg) => mk_Ball (set $ Bound 0) arg) (sets ~~ args)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   173
    val rhs = Abs ("x", T, foldr1 HOLogic.mk_conj conjs)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   174
    val pred_name = mk_pred_name Tname
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   175
    val headT = argTs ---> (T --> HOLogic.boolT)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   176
    val head = Free (Binding.name_of pred_name, headT)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   177
    val lhs = list_comb (head, args)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   178
    val def = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   179
    val ((_, (_, pred_def)), lthy) = Specification.definition ((SOME (pred_name, SOME headT, NoSyn)),
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   180
      ((Binding.empty, []), def)) lthy
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   181
  in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   182
    (pred_def, lthy)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   183
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   184
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   185
fun Domainp_tac bnf pred_def ctxt i =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   186
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   187
    val n = live_of_bnf bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   188
    val set_map's = set_map_of_bnf bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   189
  in
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   190
    EVERY' [rtac ext, SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm Domainp.simps},
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   191
        in_rel_of_bnf bnf, pred_def]), rtac iffI,
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   192
        REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE], hyp_subst_tac ctxt,
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   193
        CONJ_WRAP' (fn set_map => EVERY' [rtac ballI, dtac (set_map RS equalityD1 RS set_mp),
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   194
          etac imageE, dtac set_rev_mp, atac, REPEAT_DETERM o eresolve_tac [CollectE, @{thm case_prodE}],
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   195
          hyp_subst_tac ctxt, rtac @{thm iffD2[OF arg_cong2[of _ _ _ _ Domainp, OF refl fst_conv]]},
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   196
          etac @{thm DomainPI}]) set_map's,
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   197
        REPEAT_DETERM o etac conjE, REPEAT_DETERM o resolve_tac [exI, (refl RS conjI), rotate_prems 1 conjI],
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   198
        rtac refl, rtac (box_equals OF [map_cong0_of_bnf bnf, map_comp_of_bnf bnf RS sym,
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   199
          map_id_of_bnf bnf]),
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   200
        REPEAT_DETERM_N n o (EVERY' [rtac @{thm box_equals[OF _ sym[OF o_apply] sym[OF id_apply]]},
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   201
          rtac @{thm fst_conv}]), rtac CollectI,
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   202
        CONJ_WRAP' (fn set_map => EVERY' [rtac (set_map RS @{thm ord_eq_le_trans}),
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   203
          REPEAT_DETERM o resolve_tac [@{thm image_subsetI}, CollectI, @{thm case_prodI}],
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   204
          dtac (rotate_prems 1 bspec), atac, etac @{thm DomainpE}, etac @{thm someI}]) set_map's
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   205
      ] i
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   206
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   207
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   208
fun prove_Domainp_rel ctxt bnf pred_def =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   209
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   210
    val live = live_of_bnf bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   211
    val old_ctxt = ctxt
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   212
    val (((As, Bs), Ds), ctxt) = ctxt
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   213
      |> mk_TFrees live
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   214
      ||>> mk_TFrees live
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   215
      ||>> mk_TFrees (dead_of_bnf bnf)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   216
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   217
    val relator = mk_rel_of_bnf Ds As Bs bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   218
    val relsT = map2 mk_pred2T As Bs
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   219
    val T = mk_T_of_bnf Ds As bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   220
    val (args, ctxt) = Ctr_Sugar_Util.mk_Frees "R" relsT ctxt
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   221
    val lhs = mk_Domainp (list_comb (relator, args))
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   222
    val rhs = mk_pred pred_def (map mk_Domainp args) T
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   223
    val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
57890
1e13f63fb452 use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
traytel
parents: 57399
diff changeset
   224
    val thm = Goal.prove_sorry ctxt [] [] goal
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   225
      (fn {context = ctxt, prems = _} => Domainp_tac bnf pred_def ctxt 1)
57890
1e13f63fb452 use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
traytel
parents: 57399
diff changeset
   226
      |> Thm.close_derivation
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   227
  in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   228
    Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   229
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   230
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   231
fun pred_eq_onp_tac bnf pred_def ctxt i =
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   232
  (SELECT_GOAL (Local_Defs.unfold_tac ctxt [@{thm eq_onp_Grp},
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   233
    @{thm Ball_Collect}, pred_def]) THEN' CONVERSION (subst_conv (map_id0_of_bnf bnf RS sym))
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   234
  THEN' rtac (rel_Grp_of_bnf bnf)) i
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   235
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   236
fun prove_rel_eq_onp ctxt bnf pred_def =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   237
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   238
    val live = live_of_bnf bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   239
    val old_ctxt = ctxt
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   240
    val ((As, Ds), ctxt) = ctxt
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   241
      |> mk_TFrees live
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   242
      ||>> mk_TFrees (dead_of_bnf bnf)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   243
    val T = mk_T_of_bnf Ds As bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   244
    val argTs = map mk_pred1T As
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   245
    val (args, ctxt) = mk_Frees "P" argTs ctxt
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   246
    val relator = mk_rel_of_bnf Ds As As bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   247
    val lhs = list_comb (relator, map mk_eq_onp args)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   248
    val rhs = mk_eq_onp (mk_pred pred_def args T)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   249
    val goal = HOLogic.mk_eq (lhs, rhs) |> HOLogic.mk_Trueprop
57890
1e13f63fb452 use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
traytel
parents: 57399
diff changeset
   250
    val thm = Goal.prove_sorry ctxt [] [] goal
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   251
      (fn {context = ctxt, prems = _} => pred_eq_onp_tac bnf pred_def ctxt 1)
57890
1e13f63fb452 use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
traytel
parents: 57399
diff changeset
   252
      |> Thm.close_derivation
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   253
  in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   254
    Drule.zero_var_indexes (singleton (Variable.export ctxt old_ctxt) thm)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   255
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   256
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   257
fun predicator bnf lthy =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   258
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   259
    val (pred_def, lthy) = define_pred bnf lthy
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   260
    val pred_def = Morphism.thm (Local_Theory.target_morphism lthy) pred_def
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   261
    val Domainp_rel = prove_Domainp_rel lthy bnf pred_def
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   262
    val rel_eq_onp = prove_rel_eq_onp lthy bnf pred_def
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   263
    fun qualify defname suffix = Binding.qualified true suffix defname
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   264
    val Domainp_rel_thm_name = qualify (base_name_of_bnf bnf) "Domainp_rel"
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   265
    val rel_eq_onp_thm_name = qualify (base_name_of_bnf bnf) "rel_eq_onp"
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   266
    val rel_eq_onp_internal = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
56677
660ffb526069 predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents: 56651
diff changeset
   267
      (Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
660ffb526069 predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents: 56651
diff changeset
   268
        rel_eq_onp
660ffb526069 predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents: 56651
diff changeset
   269
    val pred_data = {rel_eq_onp = rel_eq_onp_internal}
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   270
    val type_name = type_name_of_bnf bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   271
    val relator_domain_attr = @{attributes [relator_domain]}
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   272
    val notes = [((Domainp_rel_thm_name, []), [([Domainp_rel], relator_domain_attr)]),
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   273
      ((rel_eq_onp_thm_name, []), [([rel_eq_onp], [])])]
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   274
    val lthy = Local_Theory.declaration {syntax = false, pervasive = true}
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   275
      (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data)) lthy
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   276
  in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   277
    (notes, lthy)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   278
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   279
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   280
(* BNF interpretation *)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   281
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   282
fun transfer_bnf_interpretation bnf lthy =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   283
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   284
    val constr_notes = if dead_of_bnf bnf > 0 then []
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   285
      else prove_relation_constraints bnf lthy
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   286
    val relator_eq_notes = if dead_of_bnf bnf > 0 then []
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   287
      else relator_eq bnf
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   288
    val (pred_notes, lthy) = predicator bnf lthy
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   289
  in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   290
    snd (Local_Theory.notes (constr_notes @ relator_eq_notes @ pred_notes) lthy)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   291
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   292
58191
b3c71d630777 pretend code generation is a ctr_sugar plugin
blanchet
parents: 58186
diff changeset
   293
val _ = Theory.setup (bnf_interpretation transfer_plugin
58186
a6c3962ea907 named interpretations
blanchet
parents: 58179
diff changeset
   294
  (bnf_only_type_ctr (BNF_Util.map_local_theory o transfer_bnf_interpretation))
58179
2de7b0313de3 tuned size function generation
blanchet
parents: 58177
diff changeset
   295
  (bnf_only_type_ctr (transfer_bnf_interpretation)))
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   296
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   297
(* simplification rules for the predicator *)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   298
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   299
fun lookup_defined_pred_data lthy name =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   300
  case (Transfer.lookup_pred_data lthy name) of
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   301
    SOME data => data
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   302
    | NONE => (error "lookup_pred_data: something went utterly wrong")
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   303
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   304
fun prove_pred_inject lthy (fp_sugar:fp_sugar) =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   305
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   306
    val involved_types = distinct op= (
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   307
        map type_name_of_bnf (#fp_nesting_bnfs fp_sugar)
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   308
      @ map type_name_of_bnf (#live_nesting_bnfs fp_sugar)
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   309
      @ map type_name_of_bnf (#bnfs (#fp_res fp_sugar)))
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   310
    val eq_onps = map (Transfer.rel_eq_onp o lookup_defined_pred_data lthy) involved_types
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   311
    val live = live_of_bnf (bnf_of_fp_sugar fp_sugar)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   312
    val old_lthy = lthy
58227
d91f7a80f412 use right sort constraints
blanchet
parents: 58191
diff changeset
   313
    val old_As = snd (dest_Type (#T fp_sugar))
58230
61e4c96bf2b6 made code work also in the presence of deads
blanchet
parents: 58227
diff changeset
   314
    val liveness =
61e4c96bf2b6 made code work also in the presence of deads
blanchet
parents: 58227
diff changeset
   315
      BNF_FP_Def_Sugar.liveness_of_fp_bnf (length old_As) (hd (#bnfs (#fp_res fp_sugar)));
58227
d91f7a80f412 use right sort constraints
blanchet
parents: 58191
diff changeset
   316
    val (unsorted_As, lthy) = mk_TFrees live lthy
58234
265aea1e9985 honour sorts in N2M
blanchet
parents: 58230
diff changeset
   317
    val As = map2 (Ctr_Sugar_Util.resort_tfree_or_tvar o snd o Ctr_Sugar_Util.dest_TFree_or_TVar)
58230
61e4c96bf2b6 made code work also in the presence of deads
blanchet
parents: 58227
diff changeset
   318
      (map_filter (uncurry (fn true => SOME | false => K NONE)) (liveness ~~ old_As)) unsorted_As
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   319
    val predTs = map mk_pred1T As
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   320
    val (preds, lthy) = mk_Frees "P" predTs lthy
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   321
    val args = map mk_eq_onp preds
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   322
    val cTs = map (SOME o certifyT lthy) (maps (replicate 2) As)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   323
    val cts = map (SOME o certify lthy) args
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   324
    fun get_rhs thm = thm |> concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   325
    fun is_eqn thm = can get_rhs thm
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   326
    fun rel2pred_massage thm =
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   327
      let
56677
660ffb526069 predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents: 56651
diff changeset
   328
        val live_step = @{lemma "x = y \<Longrightarrow> (eq_onp P a a \<and> x) = (P a \<and> y)" by (simp only: eq_onp_same_args)}
660ffb526069 predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents: 56651
diff changeset
   329
        val kill_top1 = @{lemma "(top x \<and> P) = P" by blast}
660ffb526069 predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents: 56651
diff changeset
   330
        val kill_top2 = @{lemma "(P \<and> top x) = P" by blast}
660ffb526069 predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents: 56651
diff changeset
   331
        fun pred_eq_onp_conj conjs = List.foldr (fn (_, thm) => thm RS live_step)
660ffb526069 predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents: 56651
diff changeset
   332
          @{thm refl[of True]} conjs
56538
7c3b6b799b94 observe also DEADID BNFs and associate the conjunction in rel_inject to the right
kuncar
parents: 56524
diff changeset
   333
        val conjuncts = if is_eqn thm then thm |> get_rhs |> HOLogic.dest_conj else []
56677
660ffb526069 predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents: 56651
diff changeset
   334
        val kill_top = Local_Defs.unfold lthy [kill_top2] #> Local_Defs.unfold lthy [kill_top1]
56538
7c3b6b799b94 observe also DEADID BNFs and associate the conjunction in rel_inject to the right
kuncar
parents: 56524
diff changeset
   335
        val kill_True = Local_Defs.unfold lthy [@{thm HOL.simp_thms(21)}]
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   336
      in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   337
        thm
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   338
        |> Drule.instantiate' cTs cts
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   339
        |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
56677
660ffb526069 predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents: 56651
diff changeset
   340
          (Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   341
        |> Local_Defs.unfold lthy eq_onps
57399
cfc19f0a6261 compile
blanchet
parents: 56677
diff changeset
   342
        |> (fn thm => if conjuncts <> [] then @{thm box_equals}
56538
7c3b6b799b94 observe also DEADID BNFs and associate the conjunction in rel_inject to the right
kuncar
parents: 56524
diff changeset
   343
              OF [thm, @{thm eq_onp_same_args}, pred_eq_onp_conj conjuncts |> kill_True]
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   344
            else thm RS (@{thm eq_onp_same_args} RS iffD1))
56677
660ffb526069 predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents: 56651
diff changeset
   345
        |> kill_top
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   346
      end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   347
    val rel_injects = #rel_injects fp_sugar
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   348
  in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   349
    rel_injects
56538
7c3b6b799b94 observe also DEADID BNFs and associate the conjunction in rel_inject to the right
kuncar
parents: 56524
diff changeset
   350
    |> map (Local_Defs.unfold lthy [@{thm conj_assoc}])
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   351
    |> map rel2pred_massage
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   352
    |> Variable.export lthy old_lthy
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   353
    |> map Drule.zero_var_indexes
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   354
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   355
56677
660ffb526069 predicator simplification rules: support also partially specialized types e.g. 'a * nat
kuncar
parents: 56651
diff changeset
   356
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   357
(* fp_sugar interpretation *)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   358
58186
a6c3962ea907 named interpretations
blanchet
parents: 58179
diff changeset
   359
fun transfer_fp_sugars_interpretation fp_sugar lthy =
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   360
  let
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   361
    val pred_injects = prove_pred_inject lthy fp_sugar
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   362
    fun qualify defname suffix = Binding.qualified true suffix defname
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   363
    val pred_inject_thm_name = qualify (base_name_of_bnf (bnf_of_fp_sugar fp_sugar)) "pred_inject"
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   364
    val simp_attrs = @{attributes [simp]}
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   365
  in
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   366
    snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   367
  end
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   368
58191
b3c71d630777 pretend code generation is a ctr_sugar plugin
blanchet
parents: 58186
diff changeset
   369
val _ = Theory.setup (fp_sugars_interpretation transfer_plugin
58186
a6c3962ea907 named interpretations
blanchet
parents: 58179
diff changeset
   370
  (fp_sugar_only_type_ctr (map_local_theory o fold transfer_fp_sugars_interpretation))
a6c3962ea907 named interpretations
blanchet
parents: 58179
diff changeset
   371
  (fp_sugar_only_type_ctr (fold transfer_fp_sugars_interpretation)))
56524
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   372
f4ba736040fa setup for Transfer and Lifting from BNF; tuned thm names
kuncar
parents:
diff changeset
   373
end