Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
QuotMain.thy
changeset 381 991db758a72d
parent 379 57bde65f6eb2
child 382 7ccbf4e2eb18
equal deleted inserted replaced
379:57bde65f6eb2 381:991db758a72d 
   156 
   156 
   157 
   157 
   158 (* lifting of constants *)
 
   158 (* lifting of constants *)
 
   159 use "quotient_def.ML"
 
   159 use "quotient_def.ML"
 
   160 
   160 
       
   161 (* TODO: Consider defining it with an "if"; sth like:
 
       
   162    Babs p m = \<lambda>x. if x \<in> p then m x else undefined
 
       
   163 *)
 
       
   164 definition
 
       
   165   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 
       
   166 where
 
       
   167   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
   161 
   168 
   162 
   169 
   163 section {* ATOMIZE *}
 
   170 section {* ATOMIZE *}
 
   164 
   171 
   165 lemma atomize_eqv[atomize]: 
   172 lemma atomize_eqv[atomize]:
 
   166   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)" 
   173   shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
 
   167 proof
 
   174 proof
 
   168   assume "A \<equiv> B" 
   175   assume "A \<equiv> B"
 
   169   then show "Trueprop A \<equiv> Trueprop B" by unfold
 
   176   then show "Trueprop A \<equiv> Trueprop B" by unfold
 
   170 next
 
   177 next
 
   171   assume *: "Trueprop A \<equiv> Trueprop B"
 
   178   assume *: "Trueprop A \<equiv> Trueprop B"
 
   172   have "A = B"
 
   179   have "A = B"
 
   173   proof (cases A)
 
   180   proof (cases A)
 
   192 end
 
   199 end
 
   193 *}
 
   200 *}
 
   194 
   201 
   195 ML {* atomize_thm @{thm list.induct} *}
 
   202 ML {* atomize_thm @{thm list.induct} *}
 
   196 
   203 
   197 section {* REGULARIZE *}
 
       
   198 (*
 
       
   199 
       
   200 Regularizing a theorem means:
 
       
   201  - Quantifiers over a type that needs lifting are replaced by
 
       
   202    bounded quantifiers, for example:
 
       
   203       \<forall>x. P     \<Longrightarrow>     \<forall>x\<in>(Respects R). P
 
       
   204  - Abstractions over a type that needs lifting are replaced
 
       
   205    by bounded abstractions:
 
       
   206       \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)
 
       
   207 
       
   208  - Equalities over the type being lifted are replaced by
 
       
   209    appropriate relations:
 
       
   210       A = B     \<Longrightarrow>     A \<approx> B
 
       
   211    Example with more complicated types of A, B:
 
       
   212       A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B
 
       
   213 
       
   214 Regularizing is done in 3 phases:
 
       
   215  - First a regularized term is created
 
       
   216  - Next we prove that the original theorem implies the new one
 
       
   217  - Finally using MP we get the new theorem.
 
       
   218 
       
   219 To prove that the old theorem implies the new one, we first
 
       
   220 atomize it and then try:
 
       
   221  - Reflexivity of the relation
 
       
   222  - Assumption
 
       
   223  - Elimnating quantifiers on both sides of toplevel implication
 
       
   224  - Simplifying implications on both sides of toplevel implication
 
       
   225  - Ball (Respects ?E) ?P = All ?P
 
       
   226  - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
 
       
   227 
       
   228 *)
 
       
   229 
       
   230 definition
 
       
   231   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 
       
   232 where
 
       
   233   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
       
   234 (* TODO: Consider defining it with an "if"; sth like:
 
       
   235    Babs p m = \<lambda>x. if x \<in> p then m x else undefined
 
       
   236 *)
 
       
   237 
       
   238 ML {*
 
       
   239 fun needs_lift (rty as Type (rty_s, _)) ty =
 
       
   240   case ty of
 
       
   241     Type (s, tys) =>
 
       
   242       (s = rty_s) orelse (exists (needs_lift rty) tys)
 
       
   243   | _ => false
 
       
   244 
       
   245 *}
 
       
   246 
       
   247 
       
   248 lemma universal_twice:
 
       
   249   assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
 
       
   250   shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
 
       
   251 using * by auto
 
       
   252 
       
   253 lemma implication_twice:
 
       
   254   assumes a: "c \<longrightarrow> a"
 
       
   255   assumes b: "a \<Longrightarrow> b \<longrightarrow> d"
 
       
   256   shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
 
       
   257 using a b by auto
 
       
   258 
       
   259 section {* RepAbs injection *}
 
   204 section {* RepAbs injection *}
 
   260 (*
 
   205 (*
 
   261 
       
   262 RepAbs injection is done in the following phases:
 
       
   263  1) build_repabs_term inserts rep-abs pairs in the term
 
       
   264  2) we prove the equality between the original theorem and this one
 
       
   265  3) we use Pure.equal_elim_rule1 to get the new theorem.
 
       
   266 
       
   267 build_repabs_term does:
 
       
   268 
       
   269   For abstractions:
 
       
   270   * If the type of the abstraction doesn't need lifting we recurse.
 
       
   271   * If it does we add RepAbs around the whole term and check if the
 
       
   272     variable needs lifting.
 
       
   273     * If it doesn't then we recurse
 
       
   274     * If it does we recurse and put 'RepAbs' around all occurences
 
       
   275       of the variable in the obtained subterm. This in combination
 
       
   276       with the RepAbs above will let us change the type of the
 
       
   277       abstraction with rewriting.
 
       
   278   For applications:
 
       
   279   * If the term is 'Respects' applied to anything we leave it unchanged
 
       
   280   * If the term needs lifting and the head is a constant that we know
 
       
   281     how to lift, we put a RepAbs and recurse
 
       
   282   * If the term needs lifting and the head is a free applied to subterms
 
       
   283     (if it is not applied we treated it in Abs branch) then we
 
       
   284     put RepAbs and recurse
 
       
   285   * Otherwise just recurse.
 
       
   286 
       
   287 
   206 
   288 To prove that the old theorem implies the new one, we first
 
   207 To prove that the old theorem implies the new one, we first
 
   289 atomize it and then try:
 
   208 atomize it and then try:
 
   290 
   209 
   291  1) theorems 'trans2' from the appropriate QUOT_TYPE
 
   210  1) theorems 'trans2' from the appropriate QUOT_TYPE
 
   306 14) simplifying (= ===> =) for simpler respectfullness
 
   225 14) simplifying (= ===> =) for simpler respectfullness
 
   307 
   226 
   308 *)
 
   227 *)
 
   309 
   228 
   310 
   229 
   311 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
 
   230 
   312 ML {*
 
   231 (* Need to have a meta-equality *)
 
   313 fun exchange_ty lthy rty qty ty =
 
       
   314   let
 
       
   315     val thy = ProofContext.theory_of lthy
 
       
   316   in
 
       
   317     if Sign.typ_instance thy (ty, rty) then
 
       
   318       let
 
       
   319         val inst = Sign.typ_match thy (rty, ty) Vartab.empty
 
       
   320       in
 
       
   321         Envir.subst_type inst qty
 
       
   322       end
 
       
   323     else
 
       
   324       let
 
       
   325         val (s, tys) = dest_Type ty
 
       
   326       in
 
       
   327         Type (s, map (exchange_ty lthy rty qty) tys)
 
       
   328       end
 
       
   329   end
 
       
   330   handle TYPE _ => ty (* for dest_Type *)
 
       
   331 *}
 
       
   332 
       
   333 
       
   334 ML {*
 
       
   335 fun find_matching_types rty ty =
 
       
   336   if Type.raw_instance (Logic.varifyT ty, rty)
 
       
   337   then [ty]
 
       
   338   else
 
       
   339     let val (s, tys) = dest_Type ty in
 
       
   340     flat (map (find_matching_types rty) tys)
 
       
   341     end
 
       
   342     handle TYPE _ => []
 
       
   343 *}
 
       
   344 
       
   345 ML {*
 
       
   346 fun negF absF = repF
 
       
   347   | negF repF = absF
 
       
   348 
       
   349 fun get_fun flag qenv lthy ty =
 
       
   350 let
 
       
   351   
       
   352   fun get_fun_aux s fs =
 
       
   353    (case (maps_lookup (ProofContext.theory_of lthy) s) of
 
       
   354       SOME info => list_comb (Const (#mapfun info, dummyT), fs)
 
       
   355     | NONE      => error ("no map association for type " ^ s))
 
       
   356 
       
   357   fun get_const flag qty =
 
       
   358   let 
       
   359     val thy = ProofContext.theory_of lthy
 
       
   360     val qty_name = Long_Name.base_name (fst (dest_Type qty))
 
       
   361   in
 
       
   362     case flag of
 
       
   363       absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)
 
       
   364     | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
 
       
   365   end
 
       
   366 
       
   367   fun mk_identity ty = Abs ("", ty, Bound 0)
 
       
   368 
       
   369 in
 
       
   370   if (AList.defined (op=) qenv ty)
 
       
   371   then (get_const flag ty)
 
       
   372   else (case ty of
 
       
   373           TFree _ => mk_identity ty
 
       
   374         | Type (_, []) => mk_identity ty 
       
   375         | Type ("fun" , [ty1, ty2]) => 
       
   376             let
 
       
   377               val fs_ty1 = get_fun (negF flag) qenv lthy ty1
 
       
   378               val fs_ty2 = get_fun flag qenv lthy ty2
 
       
   379             in  
       
   380               get_fun_aux "fun" [fs_ty1, fs_ty2]
 
       
   381             end 
       
   382         | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
 
       
   383         | _ => error ("no type variables allowed"))
 
       
   384 end
 
       
   385 *}
 
       
   386 
       
   387 ML {*
 
       
   388 fun get_fun_OLD flag (rty, qty) lthy ty =
 
       
   389   let
 
       
   390     val tys = find_matching_types rty ty;
 
       
   391     val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
 
       
   392     val xchg_ty = exchange_ty lthy rty qty ty
 
       
   393   in
 
       
   394     get_fun flag qenv lthy xchg_ty
 
       
   395   end
 
       
   396 *}
 
       
   397 
       
   398 text {* Does the same as 'subst' in a given prop or theorem *}
 
       
   399 ML {*
 
       
   400 fun eqsubst_prop ctxt thms t =
 
       
   401   let
 
       
   402     val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t)
 
       
   403     val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
 
       
   404       NONE => error "eqsubst_prop"
 
       
   405     | SOME th => cprem_of th 1
 
       
   406   in term_of a' end
 
       
   407 *}
 
       
   408 
       
   409 ML {*
 
       
   410   fun repeat_eqsubst_prop ctxt thms t =
 
       
   411     repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t)
 
       
   412     handle _ => t
 
       
   413 *}
 
       
   414 
       
   415 
       
   416 ML {*
 
       
   417 fun eqsubst_thm ctxt thms thm =
 
       
   418   let
 
       
   419     val goalstate = Goal.init (Thm.cprop_of thm)
 
       
   420     val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
 
       
   421       NONE => error "eqsubst_thm"
 
       
   422     | SOME th => cprem_of th 1
 
       
   423     val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
 
       
   424     val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');
 
       
   425     val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
 
       
   426     val rt = Goal.prove_internal [] cgoal (fn _ => tac);
 
       
   427   in
 
       
   428     @{thm Pure.equal_elim_rule1} OF [rt, thm]
 
       
   429   end
 
       
   430 *}
 
       
   431 
       
   432 ML {*
 
       
   433   fun repeat_eqsubst_thm ctxt thms thm =
 
       
   434     repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm)
 
       
   435     handle _ => thm
 
       
   436 *}
 
       
   437 
       
   438 (* Needed to have a meta-equality *)
 
       
   439 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
 
   232 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id"
 
   440 by (simp add: id_def)
 
   233 by (simp add: id_def)
 
   441 
       
   442 (* TODO: can be also obtained with: *)
 
   234 (* TODO: can be also obtained with: *)
 
   443 ML {* symmetric (eq_reflection OF @{thms id_def}) *}
 
   235 ML {* symmetric (eq_reflection OF @{thms id_def}) *}
 
   444 
   236 
   445 ML {*
 
   237 ML {*
 
   446 fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
 
   238 fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
 
   497       (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
 
   289       (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
 
   498   | (_ $ (_ $ (Abs(_, _, _)) $ _)) =>
 
   290   | (_ $ (_ $ (Abs(_, _, _)) $ _)) =>
 
   499       (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
 
   291       (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
 
   500       (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
 
   292       (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
 
   501   | _ => fn _ => no_tac) i st
 
   293   | _ => fn _ => no_tac) i st
 
       
   294 *}
 
       
   295 
       
   296 ML {* (* Legacy *)
 
       
   297 fun needs_lift (rty as Type (rty_s, _)) ty =
 
       
   298   case ty of
 
       
   299     Type (s, tys) =>
 
       
   300       (s = rty_s) orelse (exists (needs_lift rty) tys)
 
       
   301   | _ => false
 
       
   302 
   502 *}
 
   303 *}
 
   503 
   304 
   504 ML {*
 
   305 ML {*
 
   505 fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
 
   306 fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
 
   506   let
 
   307   let
 
   574 ML {*
 
   375 ML {*
 
   575 fun simp_ids lthy thm =
 
   376 fun simp_ids lthy thm =
 
   576   MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm
 
   377   MetaSimplifier.rewrite_rule @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} thm
 
   577 *}
 
   378 *}
 
   578 
   379 
   579 ML {*
 
   380 text {* Does the same as 'subst' in a given prop or theorem *}
 
   580 fun simp_ids_trm trm =
 
   381 
   581   trm |>
 
   382 ML {*
 
   582   MetaSimplifier.rewrite false @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
 
   383 fun eqsubst_thm ctxt thms thm =
 
   583   |> cprop_of |> Thm.dest_equals |> snd
 
   384   let
 
   584 
   385     val goalstate = Goal.init (Thm.cprop_of thm)
 
       
   386     val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of
 
       
   387       NONE => error "eqsubst_thm"
 
       
   388     | SOME th => cprem_of th 1
 
       
   389     val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1
 
       
   390     val goal = Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a');
 
       
   391     val cgoal = cterm_of (ProofContext.theory_of ctxt) goal
 
       
   392     val rt = Goal.prove_internal [] cgoal (fn _ => tac);
 
       
   393   in
 
       
   394     @{thm Pure.equal_elim_rule1} OF [rt, thm]
 
       
   395   end
 
   585 *}
 
   396 *}
 
   586 
   397 
   587 text {* expects atomized definition *}
 
   398 text {* expects atomized definition *}
 
   588 ML {*
 
   399 ML {*
 
   589 fun add_lower_defs_aux lthy thm =
 
   400 fun add_lower_defs_aux lthy thm =
 
   618       (if needs_lift rty T then [T] else [])
 
   429       (if needs_lift rty T then [T] else [])
 
   619   | _ => [];
 
   430   | _ => [];
 
   620 fun findaps rty tm = distinct (op =) (findaps_all rty tm)
 
   431 fun findaps rty tm = distinct (op =) (findaps_all rty tm)
 
   621 *}
 
   432 *}
 
   622 
   433 
       
   434 
       
   435 
       
   436 (* changes (?'a ?'b raw) (?'a ?'b quo) (int 'b raw \<Rightarrow> bool) to (int 'b quo \<Rightarrow> bool) *)
 
       
   437 ML {*
 
       
   438 fun exchange_ty lthy rty qty ty =
 
       
   439   let
 
       
   440     val thy = ProofContext.theory_of lthy
 
       
   441   in
 
       
   442     if Sign.typ_instance thy (ty, rty) then
 
       
   443       let
 
       
   444         val inst = Sign.typ_match thy (rty, ty) Vartab.empty
 
       
   445       in
 
       
   446         Envir.subst_type inst qty
 
       
   447       end
 
       
   448     else
 
       
   449       let
 
       
   450         val (s, tys) = dest_Type ty
 
       
   451       in
 
       
   452         Type (s, map (exchange_ty lthy rty qty) tys)
 
       
   453       end
 
       
   454   end
 
       
   455   handle TYPE _ => ty (* for dest_Type *)
 
       
   456 *}
 
       
   457 
       
   458 
       
   459 ML {*
 
       
   460 fun find_matching_types rty ty =
 
       
   461   if Type.raw_instance (Logic.varifyT ty, rty)
 
       
   462   then [ty]
 
       
   463   else
 
       
   464     let val (s, tys) = dest_Type ty in
 
       
   465     flat (map (find_matching_types rty) tys)
 
       
   466     end
 
       
   467     handle TYPE _ => []
 
       
   468 *}
 
       
   469 
       
   470 ML {*
 
       
   471 fun negF absF = repF
 
       
   472   | negF repF = absF
 
       
   473 
       
   474 fun get_fun flag qenv lthy ty =
 
       
   475 let
 
       
   476   
       
   477   fun get_fun_aux s fs =
 
       
   478    (case (maps_lookup (ProofContext.theory_of lthy) s) of
 
       
   479       SOME info => list_comb (Const (#mapfun info, dummyT), fs)
 
       
   480     | NONE      => error ("no map association for type " ^ s))
 
       
   481 
       
   482   fun get_const flag qty =
 
       
   483   let 
       
   484     val thy = ProofContext.theory_of lthy
 
       
   485     val qty_name = Long_Name.base_name (fst (dest_Type qty))
 
       
   486   in
 
       
   487     case flag of
 
       
   488       absF => Const (Sign.full_bname thy ("ABS_" ^ qty_name), dummyT)
 
       
   489     | repF => Const (Sign.full_bname thy ("REP_" ^ qty_name), dummyT)
 
       
   490   end
 
       
   491 
       
   492   fun mk_identity ty = Abs ("", ty, Bound 0)
 
       
   493 
       
   494 in
 
       
   495   if (AList.defined (op=) qenv ty)
 
       
   496   then (get_const flag ty)
 
       
   497   else (case ty of
 
       
   498           TFree _ => mk_identity ty
 
       
   499         | Type (_, []) => mk_identity ty 
       
   500         | Type ("fun" , [ty1, ty2]) => 
       
   501             let
 
       
   502               val fs_ty1 = get_fun (negF flag) qenv lthy ty1
 
       
   503               val fs_ty2 = get_fun flag qenv lthy ty2
 
       
   504             in  
       
   505               get_fun_aux "fun" [fs_ty1, fs_ty2]
 
       
   506             end 
       
   507         | Type (s, tys) => get_fun_aux s (map (get_fun flag qenv lthy) tys)
 
       
   508         | _ => error ("no type variables allowed"))
 
       
   509 end
 
       
   510 *}
 
       
   511 
       
   512 ML {*
 
       
   513 fun get_fun_OLD flag (rty, qty) lthy ty =
 
       
   514   let
 
       
   515     val tys = find_matching_types rty ty;
 
       
   516     val qenv = map (fn t => (exchange_ty lthy rty qty t, t)) tys;
 
       
   517     val xchg_ty = exchange_ty lthy rty qty ty
 
       
   518   in
 
       
   519     get_fun flag qenv lthy xchg_ty
 
       
   520   end
 
       
   521 *}
 
   623 
   522 
   624 ML {*
 
   523 ML {*
 
   625 fun applic_prs lthy rty qty absrep ty =
 
   524 fun applic_prs lthy rty qty absrep ty =
 
   626   let
 
   525   let
 
   627     val rty = Logic.varifyT rty;
 
   526     val rty = Logic.varifyT rty;
 
   700 (******************************************)
 
   599 (******************************************)
 
   701 (******************************************)
 
   600 (******************************************)
 
   702 (* version with explicit qtrm             *)
 
   601 (* version with explicit qtrm             *)
 
   703 (******************************************)
 
   602 (******************************************)
 
   704 (******************************************)
 
   603 (******************************************)
 
   705 
       
   706 ML {*
 
       
   707 fun atomize_goal thy gl =
 
       
   708   let
 
       
   709     val vars = map Free (Term.add_frees gl []);
 
       
   710     val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all;
 
       
   711     fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm;
 
       
   712     val glv = fold lambda_all vars gl
 
       
   713     val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv))
 
       
   714     val glf = Type.legacy_freeze gla
 
       
   715   in
 
       
   716     if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf
 
       
   717   end
 
       
   718 *}
 
       
   719 
       
   720 
       
   721 ML {* atomize_goal @{theory} @{term "x memb [] = False"} *}
 
       
   722 ML {* atomize_goal @{theory} @{term "x = xa \<Longrightarrow> a # x = a # xa"} *}
 
       
   723 
   604 
   724 
   605 
   725 ML {*
 
   606 ML {*
 
   726 (* builds the relation for respects *)
 
   607 (* builds the relation for respects *)
 
   727  
   608  
   899 apply(subst equiv_res_exists)
 
   780 apply(subst equiv_res_exists)
 
   900 apply(rule a)
 
   781 apply(rule a)
 
   901 apply(rule b)
 
   782 apply(rule b)
 
   902 done
 
   783 done
 
   903 
   784 
       
   785 lemma universal_twice:
 
       
   786   assumes *: "\<And>x. (P x \<longrightarrow> Q x)"
 
       
   787   shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)"
 
       
   788 using * by auto
 
       
   789 
       
   790 lemma implication_twice:
 
       
   791   assumes a: "c \<longrightarrow> a"
 
       
   792   assumes b: "a \<Longrightarrow> b \<longrightarrow> d"
 
       
   793   shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
 
       
   794 using a b by auto
 
       
   795 
   904 ML {*
 
   796 ML {*
 
   905 (* FIXME: get_rid of rel_refl rel_eqv *)
 
   797 (* FIXME: get_rid of rel_refl rel_eqv *)
 
   906 fun REGULARIZE_tac lthy rel_refl rel_eqv =
 
   798 fun REGULARIZE_tac lthy rel_refl rel_eqv =
 
   907    (REPEAT1 o FIRST1) 
   799    (REPEAT1 o FIRST1) 
   908      [rtac rel_refl,
 
   800      [rtac rel_refl,
 
   955   in
 
   847   in
 
   956     Goal.prove lthy [] [] goal 
   848     Goal.prove lthy [] [] goal 
   957       (fn {context, ...} => REGULARIZE_tac' context rel_refl rel_eqv)
 
   849       (fn {context, ...} => REGULARIZE_tac' context rel_refl rel_eqv)
 
   958   end
 
   850   end
 
   959 *}
 
   851 *}
 
       
   852 
       
   853 (*
 
       
   854 Injecting REPABS means:
 
       
   855 
       
   856   For abstractions:
 
       
   857   * If the type of the abstraction doesn't need lifting we recurse.
 
       
   858   * If it does we add RepAbs around the whole term and check if the
 
       
   859     variable needs lifting.
 
       
   860     * If it doesn't then we recurse
 
       
   861     * If it does we recurse and put 'RepAbs' around all occurences
 
       
   862       of the variable in the obtained subterm. This in combination
 
       
   863       with the RepAbs above will let us change the type of the
 
       
   864       abstraction with rewriting.
 
       
   865   For applications:
 
       
   866   * If the term is 'Respects' applied to anything we leave it unchanged
 
       
   867   * If the term needs lifting and the head is a constant that we know
 
       
   868     how to lift, we put a RepAbs and recurse
 
       
   869   * If the term needs lifting and the head is a free applied to subterms
 
       
   870     (if it is not applied we treated it in Abs branch) then we
 
       
   871     put RepAbs and recurse
 
       
   872   * Otherwise just recurse.
 
       
   873 *)
 
   960 
   874 
   961 (* rep-abs injection *)
 
   875 (* rep-abs injection *)
 
   962 
   876 
   963 ML {*
 
   877 ML {*
 
   964 fun mk_repabs lthy (T, T') trm = 
   878 fun mk_repabs lthy (T, T') trm = 
  1029 ML {*
 
   943 ML {*
 
  1030 fun mk_inj_REPABS_goal lthy (rtrm, qtrm) =
 
   944 fun mk_inj_REPABS_goal lthy (rtrm, qtrm) =
 
  1031   Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))
 
   945   Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))
 
  1032 *}
 
   946 *}
 
  1033 
   947 
  1034 (* Final wrappers *)
 
   948 
       
   949 
       
   950 (*
 
       
   951 To prove that the old theorem implies the new one, we first
 
       
   952 atomize it and then try:
 
       
   953  - Reflexivity of the relation
 
       
   954  - Assumption
 
       
   955  - Elimnating quantifiers on both sides of toplevel implication
 
       
   956  - Simplifying implications on both sides of toplevel implication
 
       
   957  - Ball (Respects ?E) ?P = All ?P
 
       
   958  - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
 
       
   959 *)
 
  1035 
   960 
  1036 ML {*
 
   961 ML {*
 
  1037 fun regularize_tac ctxt rel_eqv rel_refl =
 
   962 fun regularize_tac ctxt rel_eqv rel_refl =
 
  1038   (ObjectLogic.full_atomize_tac) THEN'
 
   963   (ObjectLogic.full_atomize_tac) THEN'
 
  1039   REPEAT_ALL_NEW (FIRST' [
 
   964   REPEAT_ALL_NEW (FIRST' [
nominal2