diff -r cd6ce3322b8f -r 123877af04ed IntEx.thy --- a/IntEx.thy Sat Nov 28 04:37:30 2009 +0100 +++ b/IntEx.thy Sat Nov 28 04:46:03 2009 +0100 @@ -147,11 +147,9 @@ ML {* fun all_r_mk_comb_tac_intex lthy = all_r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *} -lemma cheat: "P" sorry - lemma "PLUS a b = PLUS b a" apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) +apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *}) prefer 2 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} @@ -161,12 +159,6 @@ apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) -apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) (***) -apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) -apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) -apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) -apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) -apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) @@ -178,7 +170,13 @@ apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) -apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) +apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) +apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) +apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) +apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) +apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) +apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) +apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) done lemma plus_assoc_pre: @@ -191,7 +189,7 @@ lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)" apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) +apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *}) apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} @@ -228,7 +226,7 @@ lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)" apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *}) -apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *}) +apply(tactic {* regularize_tac @{context} rel_eqv [rel_refl] 1 *}) apply(tactic {* all_r_mk_comb_tac_intex @{context} 1*}) ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *}