src/HOL/Nonstandard_Analysis/transfer.ML
changeset 64435 c93b0e6131c3
parent 64270 bf474d719011
     1.1 --- a/src/HOL/Nonstandard_Analysis/transfer.ML	Mon Oct 31 16:26:36 2016 +0100
     1.2 +++ b/src/HOL/Nonstandard_Analysis/transfer.ML	Tue Nov 01 00:44:24 2016 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  structure Transfer_Principle: TRANSFER_PRINCIPLE =
     1.5  struct
     1.6  
     1.7 -structure TransferData = Generic_Data
     1.8 +structure Data = Generic_Data
     1.9  (
    1.10    type T = {
    1.11      intros: thm list,
    1.12 @@ -55,13 +55,13 @@
    1.13  fun transfer_star_tac ctxt =
    1.14    let
    1.15      fun thm_of (Const (@{const_name Ifun}, _) $ t $ u) = @{thm transfer_Ifun} OF [thm_of t, thm_of u]
    1.16 -    | thm_of (Const (@{const_name star_of}, _) $ _) = @{thm star_of_def}
    1.17 -    | thm_of (Const (@{const_name star_n}, _) $ _) = @{thm Pure.reflexive}
    1.18 -    | thm_of _ = raise MATCH;
    1.19 +      | thm_of (Const (@{const_name star_of}, _) $ _) = @{thm star_of_def}
    1.20 +      | thm_of (Const (@{const_name star_n}, _) $ _) = @{thm Pure.reflexive}
    1.21 +      | thm_of _ = raise MATCH;
    1.22  
    1.23      fun thm_of_goal (Const (@{const_name Pure.eq}, _) $ t $ (Const (@{const_name star_n}, _) $ _)) =
    1.24 -      thm_of t
    1.25 -    | thm_of_goal _ = raise MATCH;
    1.26 +          thm_of t
    1.27 +      | thm_of_goal _ = raise MATCH;
    1.28    in
    1.29      SUBGOAL (fn (t, i) =>
    1.30        resolve_tac ctxt [thm_of_goal (strip_all_body t |> Logic.strip_imp_concl)] i
    1.31 @@ -71,44 +71,43 @@
    1.32  
    1.33  fun transfer_thm_of ctxt ths t =
    1.34    let
    1.35 -    val {intros,unfolds,refolds,consts} = TransferData.get (Context.Proof ctxt);
    1.36 +    val {intros,unfolds,refolds,consts} = Data.get (Context.Proof ctxt);
    1.37      val meta = Local_Defs.meta_rewrite_rule ctxt;
    1.38      val ths' = map meta ths;
    1.39      val unfolds' = map meta unfolds and refolds' = map meta refolds;
    1.40      val (_$_$t') = Thm.concl_of (Raw_Simplifier.rewrite ctxt true unfolds' (Thm.cterm_of ctxt t))
    1.41      val u = unstar_term consts t'
    1.42 -   val tac =
    1.43 +    val tac =
    1.44        rewrite_goals_tac ctxt (ths' @ refolds' @ unfolds') THEN
    1.45        ALLGOALS (Object_Logic.full_atomize_tac ctxt) THEN
    1.46        match_tac ctxt [transitive_thm] 1 THEN
    1.47        resolve_tac ctxt [@{thm transfer_start}] 1 THEN
    1.48        REPEAT_ALL_NEW (resolve_tac ctxt intros ORELSE' transfer_star_tac ctxt) 1 THEN
    1.49        match_tac ctxt [reflexive_thm] 1
    1.50 -  in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end
    1.51 +  in Goal.prove ctxt [] [] (Logic.mk_equals (t,u)) (K tac) end;
    1.52  
    1.53 -fun transfer_tac ctxt ths =
    1.54 -    SUBGOAL (fn (t, _) =>
    1.55 -        (fn th =>
    1.56 -            let
    1.57 -              val tr = transfer_thm_of ctxt ths t
    1.58 -              val (_$l$r) = Thm.concl_of tr;
    1.59 -              val trs = if l aconv r then [] else [tr];
    1.60 -            in rewrite_goals_tac ctxt trs th end))
    1.61 +fun transfer_tac ctxt ths = SUBGOAL (fn (t, _) => (fn th =>
    1.62 +  let
    1.63 +    val tr = transfer_thm_of ctxt ths t
    1.64 +    val (_$ l $ r) = Thm.concl_of tr;
    1.65 +    val trs = if l aconv r then [] else [tr];
    1.66 +  in rewrite_goals_tac ctxt trs th end));
    1.67  
    1.68  local
    1.69  
    1.70 -fun map_intros f = TransferData.map
    1.71 +fun map_intros f = Data.map
    1.72    (fn {intros,unfolds,refolds,consts} =>
    1.73      {intros=f intros, unfolds=unfolds, refolds=refolds, consts=consts})
    1.74  
    1.75 -fun map_unfolds f = TransferData.map
    1.76 +fun map_unfolds f = Data.map
    1.77    (fn {intros,unfolds,refolds,consts} =>
    1.78      {intros=intros, unfolds=f unfolds, refolds=refolds, consts=consts})
    1.79  
    1.80 -fun map_refolds f = TransferData.map
    1.81 +fun map_refolds f = Data.map
    1.82    (fn {intros,unfolds,refolds,consts} =>
    1.83      {intros=intros, unfolds=unfolds, refolds=f refolds, consts=consts})
    1.84  in
    1.85 +
    1.86  val intro_add = Thm.declaration_attribute (map_intros o Thm.add_thm);
    1.87  val intro_del = Thm.declaration_attribute (map_intros o Thm.del_thm);
    1.88  
    1.89 @@ -117,9 +116,10 @@
    1.90  
    1.91  val refold_add = Thm.declaration_attribute (map_refolds o Thm.add_thm);
    1.92  val refold_del = Thm.declaration_attribute (map_refolds o Thm.del_thm);
    1.93 +
    1.94  end
    1.95  
    1.96 -fun add_const c = Context.theory_map (TransferData.map
    1.97 +fun add_const c = Context.theory_map (Data.map
    1.98    (fn {intros,unfolds,refolds,consts} =>
    1.99      {intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
   1.100