Removed the use of 'rty' from APPLY_RSP, finally LF proofs go automatically.
--- a/FSet.thy Wed Dec 02 10:56:35 2009 +0100
+++ b/FSet.thy Wed Dec 02 11:30:40 2009 +0100
@@ -371,7 +371,6 @@
apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-
apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* C *) (* = and extensionality *)
apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 3 *) (* Ball-Ball *)
apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
@@ -380,22 +379,22 @@
apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* B *) (* Cong *)
apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
-apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 7 *) (* respectfulness *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* inj_repabs_tac_fset' @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
done
quotient_def
--- a/LFex.thy Wed Dec 02 10:56:35 2009 +0100
+++ b/LFex.thy Wed Dec 02 11:30:40 2009 +0100
@@ -225,8 +225,6 @@
val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM}
val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs}
val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}
- val lower = flat (map (add_lower_defs @{context}) defs)
- val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower
val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
*}
@@ -267,198 +265,9 @@
apply -
apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1*})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1*})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1*})
+prefer 2
apply(tactic {* clean_tac @{context} quot defs 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1*})
done
(* Does not work:
@@ -487,97 +296,7 @@
\<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *})
apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ kind } quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-(* LOOP! *)
-(* apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *}) *)
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 1 *})
-apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
apply(tactic {* clean_tac @{context} quot defs 1 *})
done
--- a/QuotMain.thy Wed Dec 02 10:56:35 2009 +0100
+++ b/QuotMain.thy Wed Dec 02 11:30:40 2009 +0100
@@ -840,21 +840,36 @@
*}
-
-
+definition
+ "QUOT_TRUE x \<equiv> True"
ML {*
-fun APPLY_RSP_TAC rty =
- Subgoal.FOCUS (fn {concl, ...} =>
- case HOLogic.dest_Trueprop (term_of concl) of
- (_ $ (f $ _) $ (_ $ _)) =>
+fun find_qt_asm asms =
+ let
+ fun find_fun trm =
+ case trm of
+ (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
+ | _ => false
+ in
+ case find_first find_fun asms of
+ SOME (_ $ (_ $ (f $ a))) => (f, a)
+ | _ => error "find_qt_asm"
+ end
+*}
+
+ML {*
+fun APPLY_RSP_TAC rty =
+ Subgoal.FOCUS (fn {concl, asms, ...} =>
+ case ((HOLogic.dest_Trueprop (term_of concl))) of
+ ((_ $ (f $ _) $ (_ $ _))) =>
let
+ val (asmf, asma) = find_qt_asm (map term_of asms);
val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
val insts = Thm.match (pat, concl)
in
- if needs_lift rty (fastype_of f)
- then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
- else no_tac
+ if (fastype_of asmf) = (fastype_of f)
+ then no_tac
+ else rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
end
| _ => no_tac)
*}
@@ -886,9 +901,6 @@
*)
-definition
- "QUOT_TRUE x \<equiv> True"
-
lemma quot_true_dests:
shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
@@ -942,7 +954,7 @@
ML {* fun unlam (Abs a) = snd (Term.dest_abs a) *}
ML {*
-fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
+fun inj_repabs_tac_old ctxt rty quot_thms rel_refl trans2 =
(FIRST' [
(* "cong" rule of the of the relation / transitivity*)
(* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
@@ -998,11 +1010,11 @@
*}
ML {*
-fun inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 =
+fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
(FIRST' [
(* "cong" rule of the of the relation / transitivity*)
(* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
- DT ctxt "1" (resolve_tac trans2),
+ NDT ctxt "1" (resolve_tac trans2),
(* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam),