fixing transfer tactic - unfold fully identity relation by using relator_eq
authorkuncar
Sat Mar 16 20:51:23 2013 +0100 (2013-03-16)
changeset 514378739f8abbecb
parent 51436 790310525e97
child 51438 a614e456870b
fixing transfer tactic - unfold fully identity relation by using relator_eq
src/HOL/Tools/transfer.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/Tools/transfer.ML	Sat Mar 16 17:22:05 2013 +0100
     1.2 +++ b/src/HOL/Tools/transfer.ML	Sat Mar 16 20:51:23 2013 +0100
     1.3 @@ -29,22 +29,27 @@
     1.4      { transfer_raw : thm Item_Net.T,
     1.5        known_frees : (string * typ) list,
     1.6        compound_rhs : unit Net.net,
     1.7 -      relator_eq : thm Item_Net.T }
     1.8 +      relator_eq : thm Item_Net.T,
     1.9 +      relator_eq_raw : thm Item_Net.T }
    1.10    val empty =
    1.11      { transfer_raw = Thm.full_rules,
    1.12        known_frees = [],
    1.13        compound_rhs = Net.empty,
    1.14 -      relator_eq = Thm.full_rules }
    1.15 +      relator_eq = Thm.full_rules,
    1.16 +      relator_eq_raw = Thm.full_rules }
    1.17    val extend = I
    1.18    fun merge
    1.19      ( { transfer_raw = t1, known_frees = k1,
    1.20 -        compound_rhs = c1, relator_eq = r1},
    1.21 +        compound_rhs = c1, relator_eq = r1,
    1.22 +        relator_eq_raw = rw1 },
    1.23        { transfer_raw = t2, known_frees = k2,
    1.24 -        compound_rhs = c2, relator_eq = r2}) =
    1.25 +        compound_rhs = c2, relator_eq = r2,
    1.26 +        relator_eq_raw = rw2 } ) =
    1.27      { transfer_raw = Item_Net.merge (t1, t2),
    1.28        known_frees = Library.merge (op =) (k1, k2),
    1.29        compound_rhs = Net.merge (K true) (c1, c2),
    1.30 -      relator_eq = Item_Net.merge (r1, r2) }
    1.31 +      relator_eq = Item_Net.merge (r1, r2),
    1.32 +      relator_eq_raw = Item_Net.merge (rw1, rw2) }
    1.33  )
    1.34  
    1.35  fun get_relator_eq ctxt = ctxt
    1.36 @@ -55,6 +60,9 @@
    1.37    |> (Item_Net.content o #relator_eq o Data.get o Context.Proof)
    1.38    |> map (Thm.symmetric o safe_mk_meta_eq)
    1.39  
    1.40 +fun get_relator_eq_raw ctxt = ctxt
    1.41 +  |> (Item_Net.content o #relator_eq_raw o Data.get o Context.Proof)
    1.42 +
    1.43  fun get_transfer_raw ctxt = ctxt
    1.44    |> (Item_Net.content o #transfer_raw o Data.get o Context.Proof)
    1.45  
    1.46 @@ -64,17 +72,19 @@
    1.47  fun get_compound_rhs ctxt = ctxt
    1.48    |> (#compound_rhs o Data.get o Context.Proof)
    1.49  
    1.50 -fun map_data f1 f2 f3 f4
    1.51 -  { transfer_raw, known_frees, compound_rhs, relator_eq } =
    1.52 +fun map_data f1 f2 f3 f4 f5
    1.53 +  { transfer_raw, known_frees, compound_rhs, relator_eq, relator_eq_raw } =
    1.54    { transfer_raw = f1 transfer_raw,
    1.55      known_frees = f2 known_frees,
    1.56      compound_rhs = f3 compound_rhs,
    1.57 -    relator_eq = f4 relator_eq }
    1.58 +    relator_eq = f4 relator_eq,
    1.59 +    relator_eq_raw = f5 relator_eq_raw }
    1.60  
    1.61 -fun map_transfer_raw f = map_data f I I I
    1.62 -fun map_known_frees f = map_data I f I I
    1.63 -fun map_compound_rhs f = map_data I I f I
    1.64 -fun map_relator_eq f = map_data I I I f
    1.65 +fun map_transfer_raw f = map_data f I I I I
    1.66 +fun map_known_frees f = map_data I f I I I
    1.67 +fun map_compound_rhs f = map_data I I f I I
    1.68 +fun map_relator_eq f = map_data I I I f I
    1.69 +fun map_relator_eq_raw f = map_data I I I I f
    1.70  
    1.71  fun add_transfer_thm thm = Data.map
    1.72    (map_transfer_raw (Item_Net.update thm) o
    1.73 @@ -277,12 +287,15 @@
    1.74      Thm.generalize (tfrees, rnames @ frees) (Thm.maxidx_of thm + 1) thm
    1.75    end
    1.76  
    1.77 +fun eq_tac eq_rules = TRY o REPEAT_ALL_NEW (resolve_tac eq_rules) THEN_ALL_NEW rtac @{thm is_equality_eq}
    1.78 +
    1.79  fun transfer_tac equiv ctxt i =
    1.80    let
    1.81      val pre_simps = @{thms transfer_forall_eq transfer_implies_eq}
    1.82      val start_rule = 
    1.83        if equiv then @{thm transfer_start} else @{thm transfer_start'}
    1.84      val rules = get_transfer_raw ctxt
    1.85 +    val eq_rules = get_relator_eq_raw ctxt
    1.86      (* allow unsolved subgoals only for standard transfer method, not for transfer' *)
    1.87      val end_tac = if equiv then K all_tac else K no_tac
    1.88      val err_msg = "Transfer failed to convert goal to an object-logic formula"
    1.89 @@ -290,7 +303,7 @@
    1.90        rtac start_rule i THEN
    1.91        (rtac (transfer_rule_of_term ctxt (HOLogic.dest_Trueprop t))
    1.92          THEN_ALL_NEW
    1.93 -          (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules))
    1.94 +          (SOLVED' (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))
    1.95              ORELSE' end_tac)) (i + 1)
    1.96          handle TERM (_, ts) => raise TERM (err_msg, ts)
    1.97    in
    1.98 @@ -307,12 +320,13 @@
    1.99      val rhs = (snd o Term.dest_comb o HOLogic.dest_Trueprop) t
   1.100      val rule1 = transfer_rule_of_term ctxt rhs
   1.101      val rules = get_transfer_raw ctxt
   1.102 +    val eq_rules = get_relator_eq_raw ctxt
   1.103    in
   1.104      EVERY
   1.105        [CONVERSION prep_conv i,
   1.106         rtac @{thm transfer_prover_start} i,
   1.107         (rtac rule1 THEN_ALL_NEW
   1.108 -         REPEAT_ALL_NEW (resolve_tac rules)) (i+1),
   1.109 +         (REPEAT_ALL_NEW (resolve_tac rules) THEN_ALL_NEW (DETERM o eq_tac eq_rules))) (i+1),
   1.110         rtac @{thm refl} i]
   1.111    end)
   1.112  
   1.113 @@ -350,9 +364,9 @@
   1.114    let
   1.115      val name = @{binding relator_eq}
   1.116      fun add_thm thm = Data.map (map_relator_eq (Item_Net.update thm))
   1.117 -      #> add_transfer_thm (abstract_equalities_relator_eq thm)
   1.118 +      #> Data.map (map_relator_eq_raw (Item_Net.update (abstract_equalities_relator_eq thm)))
   1.119      fun del_thm thm = Data.map (map_relator_eq (Item_Net.remove thm))
   1.120 -      #> del_transfer_thm (abstract_equalities_relator_eq thm)
   1.121 +      #> Data.map (map_relator_eq_raw (Item_Net.remove (abstract_equalities_relator_eq thm)))
   1.122      val add = Thm.declaration_attribute add_thm
   1.123      val del = Thm.declaration_attribute del_thm
   1.124      val text = "declaration of relator equality rule (used by transfer method)"
   1.125 @@ -368,6 +382,8 @@
   1.126       "transfer rule for transfer method"
   1.127    #> Global_Theory.add_thms_dynamic
   1.128       (@{binding transfer_raw}, Item_Net.content o #transfer_raw o Data.get)
   1.129 +  #> Global_Theory.add_thms_dynamic
   1.130 +     (@{binding relator_eq_raw}, Item_Net.content o #relator_eq_raw o Data.get)
   1.131    #> Method.setup @{binding transfer} (transfer_method true)
   1.132       "generic theorem transfer method"
   1.133    #> Method.setup @{binding transfer'} (transfer_method false)
     2.1 --- a/src/HOL/Transfer.thy	Sat Mar 16 17:22:05 2013 +0100
     2.2 +++ b/src/HOL/Transfer.thy	Sat Mar 16 20:51:23 2013 +0100
     2.3 @@ -57,6 +57,9 @@
     2.4  definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
     2.5    where "is_equality R \<longleftrightarrow> R = (op =)"
     2.6  
     2.7 +lemma is_equality_eq: "is_equality (op =)"
     2.8 +  unfolding is_equality_def by simp
     2.9 +
    2.10  text {* Handling of meta-logic connectives *}
    2.11  
    2.12  definition transfer_forall where
    2.13 @@ -179,9 +182,6 @@
    2.14  
    2.15  subsection {* Properties of relators *}
    2.16  
    2.17 -lemma is_equality_eq [transfer_rule]: "is_equality (op =)"
    2.18 -  unfolding is_equality_def by simp
    2.19 -
    2.20  lemma right_total_eq [transfer_rule]: "right_total (op =)"
    2.21    unfolding right_total_def by simp
    2.22