wneuper/isa: src/HOL/Tools/Transfer/transfer.ML@f4ba736040fa

     1 (*  Title:      HOL/Tools/Transfer/transfer.ML

     2     Author:     Brian Huffman, TU Muenchen

     3     Author:     Ondrej Kuncar, TU Muenchen

     5 Generic theorem transfer method.

     6 *)

     8 signature TRANSFER =

     9 sig

    10   type pred_data

    11   val rel_eq_onp: pred_data -> thm

    13   val bottom_rewr_conv: thm list -> conv

    14   val top_rewr_conv: thm list -> conv

    16   val prep_conv: conv

    17   val get_transfer_raw: Proof.context -> thm list

    18   val get_relator_eq_item_net: Proof.context -> thm Item_Net.T

    19   val get_relator_eq: Proof.context -> thm list

    20   val get_sym_relator_eq: Proof.context -> thm list

    21   val get_relator_eq_raw: Proof.context -> thm list

    22   val get_relator_domain: Proof.context -> thm list

    23   val morph_pred_data: morphism -> pred_data -> pred_data

    24   val lookup_pred_data: Proof.context -> string -> pred_data option

    25   val update_pred_data: string -> pred_data -> Context.generic -> Context.generic

    26   val get_compound_lhs: Proof.context -> (term * thm) Item_Net.T

    27   val get_compound_rhs: Proof.context -> (term * thm) Item_Net.T

    28   val transfer_add: attribute

    29   val transfer_del: attribute

    30   val transfer_raw_add: thm -> Context.generic -> Context.generic

    31   val transfer_raw_del: thm -> Context.generic -> Context.generic

    32   val transferred_attribute: thm list -> attribute

    33   val untransferred_attribute: thm list -> attribute

    34   val prep_transfer_domain_thm: Proof.context -> thm -> thm

    35   val transfer_domain_add: attribute

    36   val transfer_domain_del: attribute

    37   val transfer_rule_of_term: Proof.context -> bool -> term -> thm

    38   val transfer_rule_of_lhs: Proof.context -> term -> thm

    39   val eq_tac: Proof.context -> int -> tactic

    40   val transfer_step_tac: Proof.context -> int -> tactic

    41   val transfer_tac: bool -> Proof.context -> int -> tactic

    42   val transfer_prover_tac: Proof.context -> int -> tactic

    43   val gen_frees_tac: (string * typ) list -> Proof.context -> int -> tactic

    44   val setup: theory -> theory

    45 end

    47 structure Transfer : TRANSFER =

    48 struct

    50 (** Theory Data **)

    52 val compound_xhs_empty_net = Item_Net.init (Thm.eq_thm_prop o pairself snd) (single o fst);

    53 val rewr_rules = Item_Net.init Thm.eq_thm_prop (single o fst o HOLogic.dest_eq

    54   o HOLogic.dest_Trueprop o Thm.concl_of);

    56 type pred_data = {rel_eq_onp: thm}

    58 val rel_eq_onp = #rel_eq_onp

    60 structure Data = Generic_Data

    61 (

    62   type T =

    63     { transfer_raw : thm Item_Net.T,

    64       known_frees : (string * typ) list,

    65       compound_lhs : (term * thm) Item_Net.T,

    66       compound_rhs : (term * thm) Item_Net.T,

    67       relator_eq : thm Item_Net.T,

    68       relator_eq_raw : thm Item_Net.T,

    69       relator_domain : thm Item_Net.T,

    70       pred_data : pred_data Symtab.table }

    71   val empty =

    72     { transfer_raw = Thm.intro_rules,

    73       known_frees = [],

    74       compound_lhs = compound_xhs_empty_net,

    75       compound_rhs = compound_xhs_empty_net,

    76       relator_eq = rewr_rules,

    77       relator_eq_raw = Thm.full_rules,

    78       relator_domain = Thm.full_rules,

    79       pred_data = Symtab.empty }

    80   val extend = I

    81   fun merge

    82     ( { transfer_raw = t1, known_frees = k1,

    83         compound_lhs = l1,

    84         compound_rhs = c1, relator_eq = r1,

    85         relator_eq_raw = rw1, relator_domain = rd1,

    86         pred_data = pd1 },

    87       { transfer_raw = t2, known_frees = k2,

    88         compound_lhs = l2,

    89         compound_rhs = c2, relator_eq = r2,

    90         relator_eq_raw = rw2, relator_domain = rd2,

    91         pred_data = pd2 } ) =

    92     { transfer_raw = Item_Net.merge (t1, t2),

    93       known_frees = Library.merge (op =) (k1, k2),

    94       compound_lhs = Item_Net.merge (l1, l2),

    95       compound_rhs = Item_Net.merge (c1, c2),

    96       relator_eq = Item_Net.merge (r1, r2),

    97       relator_eq_raw = Item_Net.merge (rw1, rw2),

    98       relator_domain = Item_Net.merge (rd1, rd2),

    99       pred_data = Symtab.merge (K true) (pd1, pd2) }

   100 )

   102 fun get_transfer_raw ctxt = ctxt

   103   |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)

   105 fun get_known_frees ctxt = ctxt

   106   |> (#known_frees o Data.get o Context.Proof)

   108 fun get_compound_lhs ctxt = ctxt

   109   |> (#compound_lhs o Data.get o Context.Proof)

   111 fun get_compound_rhs ctxt = ctxt

   112   |> (#compound_rhs o Data.get o Context.Proof)

   114 fun get_relator_eq_item_net ctxt = (#relator_eq o Data.get o Context.Proof) ctxt

   116 fun get_relator_eq ctxt = ctxt

   117   |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)

   118   |> map safe_mk_meta_eq

   120 fun get_sym_relator_eq ctxt = ctxt

   121   |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)

   122   |> map (Thm.symmetric o safe_mk_meta_eq)

   124 fun get_relator_eq_raw ctxt = ctxt

   125   |> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof)

   127 fun get_relator_domain ctxt = ctxt

   128   |> (Item_Net.content o #relator_domain o Data.get o Context.Proof)

   130 fun get_pred_data ctxt = ctxt

   131   |> (#pred_data o Data.get o Context.Proof)

   133 fun map_data f1 f2 f3 f4 f5 f6 f7 f8

   134   { transfer_raw, known_frees, compound_lhs, compound_rhs,

   135     relator_eq, relator_eq_raw, relator_domain, pred_data } =

   136   { transfer_raw = f1 transfer_raw,

   137     known_frees = f2 known_frees,

   138     compound_lhs = f3 compound_lhs,

   139     compound_rhs = f4 compound_rhs,

   140     relator_eq = f5 relator_eq,

   141     relator_eq_raw = f6 relator_eq_raw,

   142     relator_domain = f7 relator_domain,

   143     pred_data = f8 pred_data }

   145 fun map_transfer_raw   f = map_data f I I I I I I I

   146 fun map_known_frees    f = map_data I f I I I I I I

   147 fun map_compound_lhs   f = map_data I I f I I I I I

   148 fun map_compound_rhs   f = map_data I I I f I I I I

   149 fun map_relator_eq     f = map_data I I I I f I I I

   150 fun map_relator_eq_raw f = map_data I I I I I f I I

   151 fun map_relator_domain f = map_data I I I I I I f I

   152 fun map_pred_data      f = map_data I I I I I I I f

   154 fun add_transfer_thm thm = Data.map

   155   (map_transfer_raw (Item_Net.update thm) o

   156    map_compound_lhs

   157      (case HOLogic.dest_Trueprop (Thm.concl_of thm) of

   158         Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>

   159           Item_Net.update (lhs, thm)

   160       | _ => I) o

   161    map_compound_rhs

   162      (case HOLogic.dest_Trueprop (Thm.concl_of thm) of

   163         Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>

   164           Item_Net.update (rhs, thm)

   165       | _ => I) o

   166    map_known_frees (Term.add_frees (Thm.concl_of thm)))

   168 fun del_transfer_thm thm = Data.map

   169   (map_transfer_raw (Item_Net.remove thm) o

   170    map_compound_lhs

   171      (case HOLogic.dest_Trueprop (Thm.concl_of thm) of

   172         Const (@{const_name Rel}, _) $ _ $ (lhs as (_ $ _)) $ _ =>

   173           Item_Net.remove (lhs, thm)

   174       | _ => I) o

   175    map_compound_rhs

   176      (case HOLogic.dest_Trueprop (Thm.concl_of thm) of

   177         Const (@{const_name Rel}, _) $ _ $ _ $ (rhs as (_ $ _)) =>

   178           Item_Net.remove (rhs, thm)

   179       | _ => I))

   181 fun transfer_raw_add thm ctxt = add_transfer_thm thm ctxt

   182 fun transfer_raw_del thm ctxt = del_transfer_thm thm ctxt

   184 (** Conversions **)

   186 fun bottom_rewr_conv rewrs = Conv.bottom_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}

   187 fun top_rewr_conv rewrs = Conv.top_conv (K (Conv.try_conv (Conv.rewrs_conv rewrs))) @{context}

   189 fun transfer_rel_conv conv =

   190   Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.fun2_conv (Conv.arg_conv conv)))

   192 val Rel_rule = Thm.symmetric @{thm Rel_def}

   194 fun dest_funcT cT =

   195   (case Thm.dest_ctyp cT of [T, U] => (T, U)

   196     | _ => raise TYPE ("dest_funcT", [Thm.typ_of cT], []))

   198 fun Rel_conv ct =

   199   let val (cT, cT') = dest_funcT (Thm.ctyp_of_term ct)

   200       val (cU, _) = dest_funcT cT'

   201   in Drule.instantiate' [SOME cT, SOME cU] [SOME ct] Rel_rule end

   203 (* Conversion to preprocess a transfer rule *)

   204 fun safe_Rel_conv ct =

   205   Conv.try_conv (HOLogic.Trueprop_conv (Conv.fun_conv (Conv.fun_conv Rel_conv))) ct

   207 fun prep_conv ct = (

   208       Conv.implies_conv safe_Rel_conv prep_conv

   209       else_conv

   210       safe_Rel_conv

   211       else_conv

   212       Conv.all_conv) ct

   214 (** Replacing explicit equalities with is_equality premises **)

   216 fun mk_is_equality t =

   217   Const (@{const_name is_equality}, Term.fastype_of t --> HOLogic.boolT) $ t

   219 val is_equality_lemma =

   220   @{lemma "(!!R. is_equality R ==> PROP (P R)) == PROP (P (op =))"

   221     by (unfold is_equality_def, rule, drule meta_spec,

   222       erule meta_mp, rule refl, simp)}

   224 fun gen_abstract_equalities ctxt (dest : term -> term * (term -> term)) thm =

   225   let

   226     val thy = Thm.theory_of_thm thm

   227     val prop = Thm.prop_of thm

   228     val (t, mk_prop') = dest prop

   229     (* Only consider "op =" at non-base types *)

   230     fun is_eq (Const (@{const_name HOL.eq}, Type ("fun", [T, _]))) =

   231         (case T of Type (_, []) => false | _ => true)

   232       | is_eq _ = false

   233     val add_eqs = Term.fold_aterms (fn t => if is_eq t then insert (op =) t else I)

   234     val eq_consts = rev (add_eqs t [])

   235     val eqTs = map (snd o dest_Const) eq_consts

   236     val used = Term.add_free_names prop []

   237     val names = map (K "") eqTs |> Name.variant_list used

   238     val frees = map Free (names ~~ eqTs)

   239     val prems = map (HOLogic.mk_Trueprop o mk_is_equality) frees

   240     val prop1 = mk_prop' (Term.subst_atomic (eq_consts ~~ frees) t)

   241     val prop2 = fold Logic.all frees (Logic.list_implies (prems, prop1))

   242     val cprop = Thm.cterm_of thy prop2

   243     val equal_thm = Raw_Simplifier.rewrite ctxt false [is_equality_lemma] cprop

   244     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm

   245   in

   246     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))

   247   end

   248     handle TERM _ => thm

   250 fun abstract_equalities_transfer ctxt thm =

   251   let

   252     fun dest prop =

   253       let

   254         val prems = Logic.strip_imp_prems prop

   255         val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)

   256         val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)

   257       in

   258         (rel, fn rel' =>

   259           Logic.list_implies (prems, HOLogic.mk_Trueprop (rel' $ x $ y)))

   260       end

   261     val contracted_eq_thm =

   262       Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm

   263       handle CTERM _ => thm

   264   in

   265     gen_abstract_equalities ctxt dest contracted_eq_thm

   266   end

   268 fun abstract_equalities_relator_eq ctxt rel_eq_thm =

   269   gen_abstract_equalities ctxt (fn x => (x, I))

   270     (rel_eq_thm RS @{thm is_equality_def [THEN iffD2]})

   272 fun abstract_equalities_domain ctxt thm =

   273   let

   274     fun dest prop =

   275       let

   276         val prems = Logic.strip_imp_prems prop

   277         val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)

   278         val ((eq, dom), y) = apfst Term.dest_comb (Term.dest_comb concl)

   279       in

   280         (dom, fn dom' => Logic.list_implies (prems, HOLogic.mk_Trueprop (eq $ dom' $ y)))

   281       end

   282     fun transfer_rel_conv conv =

   283       Conv.concl_conv ~1 (HOLogic.Trueprop_conv (Conv.arg1_conv (Conv.arg_conv conv)))

   284     val contracted_eq_thm =

   285       Conv.fconv_rule (transfer_rel_conv (bottom_rewr_conv (get_relator_eq ctxt))) thm

   286   in

   287     gen_abstract_equalities ctxt dest contracted_eq_thm

   288   end

   291 (** Replacing explicit Domainp predicates with Domainp assumptions **)

   293 fun mk_Domainp_assm (T, R) =

   294   HOLogic.mk_eq ((Const (@{const_name Domainp}, Term.fastype_of T --> Term.fastype_of R) $ T), R)

   296 val Domainp_lemma =

   297   @{lemma "(!!R. Domainp T = R ==> PROP (P R)) == PROP (P (Domainp T))"

   298     by (rule, drule meta_spec,

   299       erule meta_mp, rule refl, simp)}

   301 fun fold_Domainp f (t as Const (@{const_name Domainp},_) $ (Var (_,_))) = f t

   302   | fold_Domainp f (t $ u) = fold_Domainp f t #> fold_Domainp f u

   303   | fold_Domainp f (Abs (_, _, t)) = fold_Domainp f t

   304   | fold_Domainp _ _ = I

   306 fun subst_terms tab t =

   307   let

   308     val t' = Termtab.lookup tab t

   309   in

   310     case t' of

   311       SOME t' => t'

   312       | NONE =>

   313         (case t of

   314           u $ v => (subst_terms tab u) $ (subst_terms tab v)

   315           | Abs (a, T, t) => Abs (a, T, subst_terms tab t)

   316           | t => t)

   317   end

   319 fun gen_abstract_domains ctxt (dest : term -> term * (term -> term)) thm =

   320   let

   321     val thy = Thm.theory_of_thm thm

   322     val prop = Thm.prop_of thm

   323     val (t, mk_prop') = dest prop

   324     val Domainp_tms = rev (fold_Domainp (fn t => insert op= t) t [])

   325     val Domainp_Ts = map (snd o dest_funT o snd o dest_Const o fst o dest_comb) Domainp_tms

   326     val used = Term.add_free_names t []

   327     val rels = map (snd o dest_comb) Domainp_tms

   328     val rel_names = map (fst o fst o dest_Var) rels

   329     val names = map (fn name => ("D" ^ name)) rel_names |> Name.variant_list used

   330     val frees = map Free (names ~~ Domainp_Ts)

   331     val prems = map (HOLogic.mk_Trueprop o mk_Domainp_assm) (rels ~~ frees);

   332     val t' = subst_terms (fold Termtab.update (Domainp_tms ~~ frees) Termtab.empty) t

   333     val prop1 = fold Logic.all frees (Logic.list_implies (prems, mk_prop' t'))

   334     val prop2 = Logic.list_rename_params (rev names) prop1

   335     val cprop = Thm.cterm_of thy prop2

   336     val equal_thm = Raw_Simplifier.rewrite ctxt false [Domainp_lemma] cprop

   337     fun forall_elim thm = Thm.forall_elim_vars (Thm.maxidx_of thm + 1) thm;

   338   in

   339     forall_elim (thm COMP (equal_thm COMP @{thm equal_elim_rule2}))

   340   end

   341     handle TERM _ => thm

   343 fun abstract_domains_transfer ctxt thm =

   344   let

   345     fun dest prop =

   346       let

   347         val prems = Logic.strip_imp_prems prop

   348         val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)

   349         val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)

   350       in

   351         (x, fn x' =>

   352           Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x' $ y)))

   353       end

   354   in

   355     gen_abstract_domains ctxt dest thm

   356   end

   358 fun abstract_domains_relator_domain ctxt thm =

   359   let

   360     fun dest prop =

   361       let

   362         val prems = Logic.strip_imp_prems prop

   363         val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop)

   364         val ((rel, x), y) = apfst Term.dest_comb (Term.dest_comb concl)

   365       in

   366         (y, fn y' =>

   367           Logic.list_implies (prems, HOLogic.mk_Trueprop (rel $ x $ y')))

   368       end

   369   in

   370     gen_abstract_domains ctxt dest thm

   371   end

   373 fun detect_transfer_rules thm =

   374   let

   375     fun is_transfer_rule tm = case (HOLogic.dest_Trueprop tm) of

   376       (Const (@{const_name HOL.eq}, _)) $ ((Const (@{const_name Domainp}, _)) $ _) $ _ => false

   377       | _ $ _ $ _ => true

   378       | _ => false

   379     fun safe_transfer_rule_conv ctm =

   380       if is_transfer_rule (term_of ctm) then safe_Rel_conv ctm else Conv.all_conv ctm

   381   in

   382     Conv.fconv_rule (Conv.prems_conv ~1 safe_transfer_rule_conv) thm

   383   end

   385 (** Adding transfer domain rules **)

   387 fun prep_transfer_domain_thm ctxt thm =

   388   (abstract_equalities_domain ctxt o detect_transfer_rules) thm

   390 fun add_transfer_domain_thm thm ctxt = (add_transfer_thm o

   391   prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt

   393 fun del_transfer_domain_thm thm ctxt = (del_transfer_thm o

   394   prep_transfer_domain_thm (Context.proof_of ctxt)) thm ctxt

   396 (** Transfer proof method **)

   398 val post_simps =

   399   @{thms transfer_forall_eq [symmetric]

   400     transfer_implies_eq [symmetric] transfer_bforall_unfold}

   402 fun gen_frees_tac keepers ctxt = SUBGOAL (fn (t, i) =>

   403   let

   404     val keepers = keepers @ get_known_frees ctxt

   405     val vs = rev (Term.add_frees t [])

   406     val vs' = filter_out (member (op =) keepers) vs

   407   in

   408     Induct.arbitrary_tac ctxt 0 vs' i

   409   end)

   411 fun mk_relT (T, U) = T --> U --> HOLogic.boolT

   413 fun mk_Rel t =

   414   let val T = fastype_of t

   415   in Const (@{const_name Transfer.Rel}, T --> T) $ t end

   417 fun transfer_rule_of_terms (prj : typ * typ -> typ) ctxt tab t u =

   418   let

   419     val thy = Proof_Context.theory_of ctxt

   420     (* precondition: prj(T,U) must consist of only TFrees and type "fun" *)

   421     fun rel (T as Type ("fun", [T1, T2])) (U as Type ("fun", [U1, U2])) =

   422         let

   423           val r1 = rel T1 U1

   424           val r2 = rel T2 U2

   425           val rT = fastype_of r1 --> fastype_of r2 --> mk_relT (T, U)

   426         in

   427           Const (@{const_name rel_fun}, rT) $ r1 $ r2

   428         end

   429       | rel T U =

   430         let

   431           val (a, _) = dest_TFree (prj (T, U))

   432         in

   433           Free (the (AList.lookup (op =) tab a), mk_relT (T, U))

   434         end

   435     fun zip _ thms (Bound i) (Bound _) = (nth thms i, [])

   436       | zip ctxt thms (Abs (x, T, t)) (Abs (y, U, u)) =

   437         let

   438           val ([x', y'], ctxt') = Variable.variant_fixes [x, y] ctxt

   439           val prop = mk_Rel (rel T U) $ Free (x', T) $ Free (y', U)

   440           val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)

   441           val thm0 = Thm.assume cprop

   442           val (thm1, hyps) = zip ctxt' (thm0 :: thms) t u

   443           val ((r1, x), y) = apfst Thm.dest_comb (Thm.dest_comb (Thm.dest_arg cprop))

   444           val r2 = Thm.dest_fun2 (Thm.dest_arg (cprop_of thm1))

   445           val (a1, (b1, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r1))

   446           val (a2, (b2, _)) = apsnd dest_funcT (dest_funcT (ctyp_of_term r2))

   447           val tinsts = [SOME a1, SOME b1, SOME a2, SOME b2]

   448           val insts = [SOME (Thm.dest_arg r1), SOME (Thm.dest_arg r2)]

   449           val rule = Drule.instantiate' tinsts insts @{thm Rel_abs}

   450           val thm2 = Thm.forall_intr x (Thm.forall_intr y (Thm.implies_intr cprop thm1))

   451         in

   452           (thm2 COMP rule, hyps)

   453         end

   454       | zip ctxt thms (f $ t) (g $ u) =

   455         let

   456           val (thm1, hyps1) = zip ctxt thms f g

   457           val (thm2, hyps2) = zip ctxt thms t u

   458         in

   459           (thm2 RS (thm1 RS @{thm Rel_app}), hyps1 @ hyps2)

   460         end

   461       | zip _ _ t u =

   462         let

   463           val T = fastype_of t

   464           val U = fastype_of u

   465           val prop = mk_Rel (rel T U) $ t $ u

   466           val cprop = Thm.cterm_of thy (HOLogic.mk_Trueprop prop)

   467         in

   468           (Thm.assume cprop, [cprop])

   469         end

   470     val r = mk_Rel (rel (fastype_of t) (fastype_of u))

   471     val goal = HOLogic.mk_Trueprop (r $ t $ u)

   472     val rename = Thm.trivial (cterm_of thy goal)

   473     val (thm, hyps) = zip ctxt [] t u

   474   in

   475     Drule.implies_intr_list hyps (thm RS rename)

   476   end

   478 (* create a lambda term of the same shape as the given term *)

   479 fun skeleton (is_atom : term -> bool) ctxt t =

   480   let

   481     fun dummy ctxt =

   482       let

   483         val (c, ctxt) = yield_singleton Variable.variant_fixes "a" ctxt

   484       in

   485         (Free (c, dummyT), ctxt)

   486       end

   487     fun go (Bound i) ctxt = (Bound i, ctxt)

   488       | go (Abs (x, _, t)) ctxt =

   489         let

   490           val (t', ctxt) = go t ctxt

   491         in

   492           (Abs (x, dummyT, t'), ctxt)

   493         end

   494       | go (tu as (t $ u)) ctxt =

   495         if is_atom tu andalso not (Term.is_open tu) then dummy ctxt else

   496         let

   497           val (t', ctxt) = go t ctxt

   498           val (u', ctxt) = go u ctxt

   499         in

   500           (t' $ u', ctxt)

   501         end

   502       | go _ ctxt = dummy ctxt

   503   in

   504     go t ctxt |> fst |> Syntax.check_term ctxt |>

   505       map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type})))

   506   end

   508 (** Monotonicity analysis **)

   510 (* TODO: Put extensible table in theory data *)

   511 val monotab =

   512   Symtab.make

   513     [(@{const_name transfer_implies}, [~1, 1]),

   514      (@{const_name transfer_forall}, [1])(*,

   515      (@{const_name implies}, [~1, 1]),

   516      (@{const_name All}, [1])*)]

   518 (*

   519 Function bool_insts determines the set of boolean-relation variables

   520 that can be instantiated to implies, rev_implies, or iff.

   522 Invariants: bool_insts p (t, u) requires that

   523   u :: _ => _ => ... => bool, and

   524   t is a skeleton of u

   525 *)

   526 fun bool_insts p (t, u) =

   527   let

   528     fun strip2 (t1 $ t2, u1 $ u2, tus) =

   529         strip2 (t1, u1, (t2, u2) :: tus)

   530       | strip2 x = x

   531     fun or3 ((a, b, c), (x, y, z)) = (a orelse x, b orelse y, c orelse z)

   532     fun go Ts p (Abs (_, T, t), Abs (_, _, u)) tab = go (T :: Ts) p (t, u) tab

   533       | go Ts p (t, u) tab =

   534         let

   535           val (a, _) = dest_TFree (Term.body_type (Term.fastype_of1 (Ts, t)))

   536           val (_, tf, tus) = strip2 (t, u, [])

   537           val ps_opt = case tf of Const (c, _) => Symtab.lookup monotab c | _ => NONE

   538           val tab1 =

   539             case ps_opt of

   540               SOME ps =>

   541               let

   542                 val ps' = map (fn x => p * x) (take (length tus) ps)

   543               in

   544                 fold I (map2 (go Ts) ps' tus) tab

   545               end

   546             | NONE => tab

   547           val tab2 = Symtab.make [(a, (p >= 0, p <= 0, is_none ps_opt))]

   548         in

   549           Symtab.join (K or3) (tab1, tab2)

   550         end

   551     val tab = go [] p (t, u) Symtab.empty

   552     fun f (a, (true, false, false)) = SOME (a, @{const implies})

   553       | f (a, (false, true, false)) = SOME (a, @{const rev_implies})

   554       | f (a, (true, true, _))      = SOME (a, HOLogic.eq_const HOLogic.boolT)

   555       | f _                         = NONE

   556   in

   557     map_filter f (Symtab.dest tab)

   558   end

   560 fun retrieve_terms t net = map fst (Item_Net.retrieve net t)

   562 fun matches_list ctxt term =

   563   is_some o find_first (fn pat => Pattern.matches (Proof_Context.theory_of ctxt) (pat, term))

   565 fun transfer_rule_of_term ctxt equiv t : thm =

   566   let

   567     val compound_rhs = get_compound_rhs ctxt

   568     fun is_rhs t = compound_rhs |> retrieve_terms t |> matches_list ctxt t

   569     val s = skeleton is_rhs ctxt t

   570     val frees = map fst (Term.add_frees s [])

   571     val tfrees = map fst (Term.add_tfrees s [])

   572     fun prep a = "R" ^ Library.unprefix "'" a

   573     val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt

   574     val tab = tfrees ~~ rnames

   575     fun prep a = the (AList.lookup (op =) tab a)

   576     val thm = transfer_rule_of_terms fst ctxt' tab s t

   577     val binsts = bool_insts (if equiv then 0 else 1) (s, t)

   578     val cbool = @{ctyp bool}

   579     val relT = @{typ "bool => bool => bool"}

   580     val idx = Thm.maxidx_of thm + 1

   581     val thy = Proof_Context.theory_of ctxt

   582     fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)

   583     fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)

   584   in

   585     thm

   586       |> Thm.generalize (tfrees, rnames @ frees) idx

   587       |> Thm.instantiate (map tinst binsts, map inst binsts)

   588   end

   590 fun transfer_rule_of_lhs ctxt t : thm =

   591   let

   592     val compound_lhs = get_compound_lhs ctxt

   593     fun is_lhs t = compound_lhs |> retrieve_terms t |> matches_list ctxt t

   594     val s = skeleton is_lhs ctxt t

   595     val frees = map fst (Term.add_frees s [])

   596     val tfrees = map fst (Term.add_tfrees s [])

   597     fun prep a = "R" ^ Library.unprefix "'" a

   598     val (rnames, ctxt') = Variable.variant_fixes (map prep tfrees) ctxt

   599     val tab = tfrees ~~ rnames

   600     fun prep a = the (AList.lookup (op =) tab a)

   601     val thm = transfer_rule_of_terms snd ctxt' tab t s

   602     val binsts = bool_insts 1 (s, t)

   603     val cbool = @{ctyp bool}

   604     val relT = @{typ "bool => bool => bool"}

   605     val idx = Thm.maxidx_of thm + 1

   606     val thy = Proof_Context.theory_of ctxt

   607     fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)

   608     fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)

   609   in

   610     thm

   611       |> Thm.generalize (tfrees, rnames @ frees) idx

   612       |> Thm.instantiate (map tinst binsts, map inst binsts)

   613   end

   615 fun eq_rules_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules)

   616   THEN_ALL_NEW rtac @{thm is_equality_eq}

   618 fun eq_tac ctxt = eq_rules_tac (get_relator_eq_raw ctxt)

   620 fun transfer_step_tac ctxt = (REPEAT_ALL_NEW (resolve_tac (get_transfer_raw ctxt))

   621   THEN_ALL_NEW (DETERM o eq_rules_tac (get_relator_eq_raw ctxt)))

   623 fun transfer_tac equiv ctxt i =

   624   let

   625     val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}

   626     val start_rule =

   627       if equiv then @{thm transfer_start} else @{thm transfer_start'}

   628     val rules = get_transfer_raw ctxt

   629     val eq_rules = get_relator_eq_raw ctxt

   630     (* allow unsolved subgoals only for standard transfer method, not for transfer' *)

   631     val end_tac = if equiv then K all_tac else K no_tac

   632     val err_msg = "Transfer failed to convert goal to an object-logic formula"

   633     fun main_tac (t, i) =

   634       rtac start_rule i THEN

   635       (rtac (transfer_rule_of_term ctxt equiv (HOLogic.dest_Trueprop t))

   636         THEN_ALL_NEW

   637           (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))

   638             ORELSE' end_tac)) (i + 1)

   639         handle TERM (_, ts) => raise TERM (err_msg, ts)

   640   in

   641     EVERY

   642       [rewrite_goal_tac ctxt pre_simps i THEN

   643        SUBGOAL main_tac i,

   644        (* FIXME: rewrite_goal_tac does unwanted eta-contraction *)

   645        rewrite_goal_tac ctxt post_simps i,

   646        Goal.norm_hhf_tac ctxt i]

   647   end

   649 fun transfer_prover_tac ctxt = SUBGOAL (fn (t, i) =>

   650   let

   651     val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t

   652     val rule1 = transfer_rule_of_term ctxt false rhs

   653     val rules = get_transfer_raw ctxt

   654     val eq_rules = get_relator_eq_raw ctxt

   655     val expand_eq_in_rel = transfer_rel_conv (top_rewr_conv [@{thm rel_fun_eq[symmetric,THEN eq_reflection]}])

   656   in

   657     EVERY

   658       [CONVERSION prep_conv i,

   659        rtac @{thm transfer_prover_start} i,

   660        ((rtac rule1 ORELSE' (CONVERSION expand_eq_in_rel THEN' rtac rule1))

   661         THEN_ALL_NEW

   662          (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules))) (i+1),

   663        rtac @{thm refl} i]

   664   end)

   666 (** Transfer attribute **)

   668 fun transferred ctxt extra_rules thm =

   669   let

   670     val start_rule = @{thm transfer_start}

   671     val start_rule' = @{thm transfer_start'}

   672     val rules = extra_rules @ get_transfer_raw ctxt

   673     val eq_rules = get_relator_eq_raw ctxt

   674     val err_msg = "Transfer failed to convert goal to an object-logic formula"

   675     val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}

   676     val thm1 = Drule.forall_intr_vars thm

   677     val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])

   678                 |> map (fn v as ((a, _), S) => (v, TFree (a, S)))

   679     val thm2 = thm1

   680       |> Thm.certify_instantiate (instT, [])

   681       |> Raw_Simplifier.rewrite_rule ctxt pre_simps

   682     val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt

   683     val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)

   684     val rule = transfer_rule_of_lhs ctxt' t

   685     val tac =

   686       resolve_tac [thm2 RS start_rule', thm2 RS start_rule] 1 THEN

   687       (rtac rule

   688         THEN_ALL_NEW

   689           (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)

   690             THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1

   691         handle TERM (_, ts) => raise TERM (err_msg, ts)

   692     val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)

   693     val tnames = map (fst o dest_TFree o snd) instT

   694   in

   695     thm3

   696       |> Raw_Simplifier.rewrite_rule ctxt' post_simps

   697       |> Simplifier.norm_hhf ctxt'

   698       |> Drule.generalize (tnames, [])

   699       |> Drule.zero_var_indexes

   700   end

   701 (*

   702     handle THM _ => thm

   703 *)

   705 fun untransferred ctxt extra_rules thm =

   706   let

   707     val start_rule = @{thm untransfer_start}

   708     val rules = extra_rules @ get_transfer_raw ctxt

   709     val eq_rules = get_relator_eq_raw ctxt

   710     val err_msg = "Transfer failed to convert goal to an object-logic formula"

   711     val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}

   712     val thm1 = Drule.forall_intr_vars thm

   713     val instT = rev (Term.add_tvars (Thm.full_prop_of thm1) [])

   714                 |> map (fn v as ((a, _), S) => (v, TFree (a, S)))

   715     val thm2 = thm1

   716       |> Thm.certify_instantiate (instT, [])

   717       |> Raw_Simplifier.rewrite_rule ctxt pre_simps

   718     val ctxt' = Variable.declare_names (Thm.full_prop_of thm2) ctxt

   719     val t = HOLogic.dest_Trueprop (Thm.concl_of thm2)

   720     val rule = transfer_rule_of_term ctxt' true t

   721     val tac =

   722       rtac (thm2 RS start_rule) 1 THEN

   723       (rtac rule

   724         THEN_ALL_NEW

   725           (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules)

   726             THEN_ALL_NEW (DETERM o eq_rules_tac eq_rules)))) 1

   727         handle TERM (_, ts) => raise TERM (err_msg, ts)

   728     val thm3 = Goal.prove_internal ctxt' [] @{cpat "Trueprop ?P"} (K tac)

   729     val tnames = map (fst o dest_TFree o snd) instT

   730   in

   731     thm3

   732       |> Raw_Simplifier.rewrite_rule ctxt' post_simps

   733       |> Simplifier.norm_hhf ctxt'

   734       |> Drule.generalize (tnames, [])

   735       |> Drule.zero_var_indexes

   736   end

   738 (** Methods and attributes **)

   740 val free = Args.context -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>

   741   error ("Bad free variable: " ^ Syntax.string_of_term ctxt t))

   743 val fixing = Scan.optional (Scan.lift (Args.$$$ "fixing" -- Args.colon)

   744   |-- Scan.repeat free) []

   746 fun transfer_method equiv : (Proof.context -> Proof.method) context_parser =

   747   fixing >> (fn vs => fn ctxt =>

   748     SIMPLE_METHOD' (gen_frees_tac vs ctxt THEN' transfer_tac equiv ctxt))

   750 val transfer_prover_method : (Proof.context -> Proof.method) context_parser =

   751   Scan.succeed (fn ctxt => SIMPLE_METHOD' (transfer_prover_tac ctxt))

   753 (* Attribute for transfer rules *)

   755 fun prep_rule ctxt =

   756   abstract_domains_transfer ctxt o abstract_equalities_transfer ctxt o Conv.fconv_rule prep_conv

   758 val transfer_add =

   759   Thm.declaration_attribute (fn thm => fn ctxt =>

   760     (add_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)

   762 val transfer_del =

   763   Thm.declaration_attribute (fn thm => fn ctxt =>

   764     (del_transfer_thm o prep_rule (Context.proof_of ctxt)) thm ctxt)

   766 val transfer_attribute =

   767   Attrib.add_del transfer_add transfer_del

   769 (* Attributes for transfer domain rules *)

   771 val transfer_domain_add = Thm.declaration_attribute add_transfer_domain_thm

   773 val transfer_domain_del = Thm.declaration_attribute del_transfer_domain_thm

   775 val transfer_domain_attribute =

   776   Attrib.add_del transfer_domain_add transfer_domain_del

   778 (* Attributes for transferred rules *)

   780 fun transferred_attribute thms = Thm.rule_attribute

   781   (fn context => transferred (Context.proof_of context) thms)

   783 fun untransferred_attribute thms = Thm.rule_attribute

   784   (fn context => untransferred (Context.proof_of context) thms)

   786 val transferred_attribute_parser =

   787   Attrib.thms >> transferred_attribute

   789 val untransferred_attribute_parser =

   790   Attrib.thms >> untransferred_attribute

   792 fun morph_pred_data phi {rel_eq_onp} = {rel_eq_onp = Morphism.thm phi rel_eq_onp}

   794 fun lookup_pred_data ctxt type_name = Symtab.lookup (get_pred_data ctxt) type_name

   795   |> Option.map (morph_pred_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)))

   797 fun update_pred_data type_name qinfo ctxt =

   798   Data.map (map_pred_data (Symtab.update (type_name, qinfo))) ctxt

   800 (* Theory setup *)

   802 val relator_eq_setup =

   803   let

   804     val name = @{binding relator_eq}

   805     fun add_thm thm context = context

   806       |> Data.map (map_relator_eq (Item_Net.update thm))

   807       |> Data.map (map_relator_eq_raw

   808           (Item_Net.update (abstract_equalities_relator_eq (Context.proof_of context) thm)))

   809     fun del_thm thm context = context

   810       |> Data.map (map_relator_eq (Item_Net.remove thm))

   811       |> Data.map (map_relator_eq_raw

   812           (Item_Net.remove (abstract_equalities_relator_eq (Context.proof_of context) thm)))

   813     val add = Thm.declaration_attribute add_thm

   814     val del = Thm.declaration_attribute del_thm

   815     val text = "declaration of relator equality rule (used by transfer method)"

   816     val content = Item_Net.content o #relator_eq o Data.get

   817   in

   818     Attrib.setup name (Attrib.add_del add del) text

   819     #> Global_Theory.add_thms_dynamic (name, content)

   820   end

   822 val relator_domain_setup =

   823   let

   824     val name = @{binding relator_domain}

   825     fun add_thm thm context =

   826       let

   827         val thm = abstract_domains_relator_domain (Context.proof_of context) thm

   828       in

   829         context |> Data.map (map_relator_domain (Item_Net.update thm)) |> add_transfer_domain_thm thm

   830       end

   831     fun del_thm thm context =

   832       let

   833         val thm = abstract_domains_relator_domain (Context.proof_of context) thm

   834       in

   835         context |> Data.map (map_relator_domain (Item_Net.remove thm)) |> del_transfer_domain_thm thm

   836       end

   837     val add = Thm.declaration_attribute add_thm

   838     val del = Thm.declaration_attribute del_thm

   839     val text = "declaration of relator domain rule (used by transfer method)"

   840     val content = Item_Net.content o #relator_domain o Data.get

   841   in

   842     Attrib.setup name (Attrib.add_del add del) text

   843     #> Global_Theory.add_thms_dynamic (name, content)

   844   end

   846 val setup =

   847   relator_eq_setup

   848   #> relator_domain_setup

   849   #> Attrib.setup @{binding transfer_rule} transfer_attribute

   850      "transfer rule for transfer method"

   851   #> Global_Theory.add_thms_dynamic

   852      (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)

   853   #> Attrib.setup @{binding transfer_domain_rule} transfer_domain_attribute

   854      "transfer domain rule for transfer method"

   855   #> Attrib.setup @{binding transferred} transferred_attribute_parser

   856      "raw theorem transferred to abstract theorem using transfer rules"

   857   #> Attrib.setup @{binding untransferred} untransferred_attribute_parser

   858      "abstract theorem transferred to raw theorem using transfer rules"

   859   #> Global_Theory.add_thms_dynamic

   860      (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get)

   861   #> Method.setup @{binding transfer} (transfer_method true)

   862      "generic theorem transfer method"

   863   #> Method.setup @{binding transfer'} (transfer_method false)

   864      "generic theorem transfer method"

   865   #> Method.setup @{binding transfer_prover} transfer_prover_method

   866      "for proving transfer rules"

   868 end

author	kuncar
	Thu, 10 Apr 2014 17:48:18 +0200
changeset 57866	f4ba736040fa
parent 57862	src/HOL/Tools/transfer.ML@3373f5d1e074
child 58064	ba1ac087b3a7
permissions	-rw-r--r--