IntEx.thy
changeset 428 f62d59cd8e1b
parent 423 2f0ad33f0241
child 430 123877af04ed
equal deleted inserted replaced
425:12fc780ff0e8 428:f62d59cd8e1b
   159 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   159 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   160 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   160 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   161 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   161 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   162 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   162 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   163 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   163 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   164 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   164 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) (***)
   165 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   165 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   166 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   166 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   167 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   167 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   168 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   168 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   169 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   169 apply(tactic {* r_mk_comb_tac_intex @{context} 1*})
   234 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
   234 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}
   235 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
   235 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
   236 done
   236 done
   237 
   237 
   238 
   238 
   239 (*
       
   240 
       
   241 ML {*
       
   242 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
       
   243   (REPEAT1 o FIRST1) 
       
   244     [(K (print_tac "start")) THEN' (K no_tac), 
       
   245      DT ctxt "1" (rtac trans_thm),
       
   246      DT ctxt "2" (LAMBDA_RES_TAC ctxt),
       
   247      DT ctxt "3" (ball_rsp_tac ctxt),
       
   248      DT ctxt "4" (bex_rsp_tac ctxt),
       
   249      DT ctxt "5" (FIRST' (map rtac rsp_thms)),
       
   250      DT ctxt "6" (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
       
   251      DT ctxt "7" (rtac refl),
       
   252      DT ctxt "8" (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
       
   253      DT ctxt "9" (Cong_Tac.cong_tac @{thm cong}),
       
   254      DT ctxt "A" (rtac @{thm ext}),
       
   255      DT ctxt "B" (rtac reflex_thm),
       
   256      DT ctxt "C" (atac),
       
   257      DT ctxt "D" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
       
   258      DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt),
       
   259      DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]
       
   260 *}
       
   261 
       
   262 ML {* 
       
   263 inj_repabs_trm @{context} (reg_atrm, aqtrm) 
       
   264   |> Syntax.check_term @{context}
       
   265 *}
       
   266 
       
   267 
       
   268 ML {* val my_goal = cterm_of @{theory} (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)) *}
       
   269 ML {* val yr_goal = cterm_of @{theory} (build_repabs_goal @{context} (@{thm testtest} OF [arthm]) consts rty qty) *}
       
   270 
       
   271 prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *}
       
   272 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
       
   273 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
       
   274 done
       
   275 
       
   276 ML {*
       
   277 inj_repabs_trm @{context} (reg_atrm, aqtrm)  
       
   278 |> Syntax.string_of_term @{context}
       
   279 |> writeln
       
   280 *}
       
   281 
       
   282 *)
       
   283 
       
   284