IntEx.thy
changeset 194 03c03e88efa9
parent 192 a296bf1a3b09
child 195 72165b83b9d6
equal deleted inserted replaced
192:a296bf1a3b09 194:03c03e88efa9
   140   val t_t2 =
   140   val t_t2 =
   141   Toplevel.program (fn () =>
   141   Toplevel.program (fn () =>
   142     repabs_eq2 @{context} (g, thm, othm)
   142     repabs_eq2 @{context} (g, thm, othm)
   143   )
   143   )
   144 *}
   144 *}
   145 ML {*
       
   146  val lpi = Drule.instantiate'
       
   147    [SOME @{ctyp "nat \<times> nat"}, NONE, SOME @{ctyp "bool"}, NONE] [] @{thm LAMBDA_PRS};
       
   148 *}
       
   149 prove lambda_prs_mn_b : {* concl_of lpi *}
       
   150 apply (tactic {* compose_tac (false, @{thm LAMBDA_PRS}, 2) 1 *})
       
   151 apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
       
   152 apply (tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
       
   153 done
       
   154 
   145 
   155 ML {*
   146 ML {*
   156 fun make_simp_lam_prs_thm lthy quot_thm typ =
   147 fun make_simp_lam_prs_thm lthy quot_thm typ =
   157   let
   148   let
   158     val (_, [lty, rty]) = dest_Type typ;
   149     val (_, [lty, rty]) = dest_Type typ;
   164       (compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW
   155       (compose_tac (false, @{thm LAMBDA_PRS}, 2)) THEN_ALL_NEW
   165       (quotient_tac quot_thm);
   156       (quotient_tac quot_thm);
   166     val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1);
   157     val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1);
   167     val ts = @{thm HOL.sym} OF [t]
   158     val ts = @{thm HOL.sym} OF [t]
   168   in
   159   in
   169     MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_def}] ts
   160     MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] ts
   170   end
   161   end
   171 *}
   162 *}
   172 
   163 
   173 
   164 
   174 
   165 thm id_apply
   175 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
   166 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
   176 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
   167 ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *}
   177 thm HOL.sym[OF lambda_prs_mn_b,simplified]
   168 thm HOL.sym[OF lambda_prs_mn_b,simplified]
   178 
   169 
   179 ML {*
   170 ML {*
   180   fun simp_lam_prs lthy thm =
   171   fun simp_lam_prs lthy thm =
   181     simp_lam_prs lthy (eqsubst_thm lthy
   172     simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm)
   182       @{thms HOL.sym[OF lambda_prs_mn_b,simplified]}
       
   183     thm)
       
   184     handle _ => thm
   173     handle _ => thm
   185 *}
   174 *}
   186 ML {* t_t2 *}
   175 ML {* t_t2 *}
   187 ML {* val t_l = simp_lam_prs @{context} t_t2 *}
   176 ML {* val t_l = simp_lam_prs @{context} t_t2 *}
   188 ML {* findabs rty (prop_of (atomize_thm @{thm plus_sym_pre})) *}
       
   189 
   177 
   190 ML {*
   178 ML {*
   191   fun simp_allex_prs lthy thm =
   179   fun simp_allex_prs lthy thm =
   192     let
   180     let
   193       val rwf = @{thm FORALL_PRS[OF QUOTIENT_my_int]};
   181       val rwf = @{thm FORALL_PRS[OF QUOTIENT_my_int]};