--- a/FSet.thy Fri Nov 27 18:38:44 2009 +0100
+++ b/FSet.thy Sat Nov 28 02:54:24 2009 +0100
@@ -341,20 +341,64 @@
apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *})
done
+ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+
lemma cheat: "P" sorry
lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l"
apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *})
apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
prefer 2
-apply (tactic {* clean_tac @{context} [quot] defs
- [(@{typ "('a list \<Rightarrow> bool)"},@{typ "('a fset \<Rightarrow> bool)"})] 1 *})
-apply(tactic {* r_mk_comb_tac' @{context} rty [quot] rel_refl trans2 rsp_thms 1*})
+apply(rule cheat)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* D *) (* reflexivity of basic relations *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* C *) (* = and extensionality *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* B *) (* Cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 7 *) (* respectfulness *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *)
+apply(tactic {* r_mk_comb_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *)
done
-
-
quotient_def
fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a"
where
@@ -400,12 +444,8 @@
apply (assumption)
done
-
ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
-
-
-
(* Construction site starts here *)
lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *})
--- a/IntEx.thy Fri Nov 27 18:38:44 2009 +0100
+++ b/IntEx.thy Sat Nov 28 02:54:24 2009 +0100
@@ -140,13 +140,46 @@
ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
ML {* val consts = lookup_quot_consts defs *}
-ML {*
-fun lift_tac_fset lthy t =
- lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs
-*}
+ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
+
+
+ML {* fun r_mk_comb_tac_intex lthy = r_mk_comb_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+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"
-by (tactic {* lift_tac_fset @{context} @{thm plus_sym_pre} 1 *})
+apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 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) *}
+apply(tactic {* clean_tac @{context} [quot] defs aps 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*})
+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 {* all_r_mk_comb_tac_intex @{context} 1*})
+done
lemma plus_assoc_pre:
shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
@@ -157,8 +190,13 @@
done
lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
-by (tactic {* lift_tac_fset @{context} @{thm plus_assoc_pre} 1 *})
-
+apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 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) *}
+apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+done
lemma ho_tst: "foldl my_plus x [] = x"
apply simp
@@ -171,7 +209,7 @@
sorry
lemma "foldl PLUS x [] = x"
-apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *})
+apply (tactic {* lift_tac_intex @{context} @{thm ho_tst} 1 *})
apply (simp_all only: map_prs foldl_prs)
sorry
@@ -191,8 +229,11 @@
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 {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty [quot] [rel_refl] [trans2] rsp_thms) 1 *})
-oops
+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) *}
+apply(tactic {* clean_tac @{context} [quot] defs aps 1 *})
+done
(*
--- a/QuotMain.thy Fri Nov 27 18:38:44 2009 +0100
+++ b/QuotMain.thy Sat Nov 28 02:54:24 2009 +0100
@@ -717,7 +717,8 @@
*)
ML {*
-fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} =>
+fun instantiate_tac thm =
+ Subgoal.FOCUS (fn {concl, ...} =>
let
val pat = Drule.strip_imp_concl (cprop_of thm)
val insts = Thm.match (pat, concl)
@@ -739,13 +740,17 @@
CHANGED o (simp_tac (HOL_ss addsimps @{thms id_simps}))])
*}
+lemma FUN_REL_I:
+ assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
+ shows "(R1 ===> R2) f g"
+using a by (simp add: FUN_REL.simps)
+
ML {*
-fun LAMBDA_RES_TAC ctxt i st =
- (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
- (_ $ (_ $ (Abs(_, _, _)) $ (Abs(_, _, _)))) =>
- (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
- (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
- | _ => fn _ => no_tac) i st
+val LAMBDA_RES_TAC =
+ SUBGOAL (fn (goal, i) =>
+ case goal of
+ (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} i
+ | _ => no_tac)
*}
ML {*
@@ -815,7 +820,7 @@
fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
(FIRST' [
resolve_tac trans2,
- LAMBDA_RES_TAC ctxt,
+ LAMBDA_RES_TAC,
rtac @{thm RES_FORALL_RSP},
ball_rsp_tac ctxt,
rtac @{thm RES_EXISTS_RSP},
@@ -834,6 +839,9 @@
WEAK_LAMBDA_RES_TAC ctxt,
CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))
])
+
+fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
+ REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms)
*}
(*
@@ -841,7 +849,7 @@
we try:
1) theorems 'trans2' from the appropriate QUOT_TYPE
- 2) remove lambdas from both sides (LAMBDA_RES_TAC)
+ 2) remove lambdas from both sides: LAMBDA_RES_TAC
3) remove Ball/Bex from the right hand side
4) use user-supplied RSP theorems
5) remove rep_abs from the right side
@@ -849,44 +857,96 @@
7) split applications of lifted type (apply_rsp)
8) split applications of non-lifted type (cong_tac)
9) apply extentionality
-10) reflexivity of the relation
-11) assumption
+ A) reflexivity of the relation
+ B) assumption
(Lambdas under respects may have left us some assumptions)
-12) proving obvious higher order equalities by simplifying fun_rel
+ C) proving obvious higher order equalities by simplifying fun_rel
(not sure if it is still needed?)
-13) unfolding lambda on one side
-14) simplifying (= ===> =) for simpler respectfulness
+ D) unfolding lambda on one side
+ E) simplifying (= ===> =) for simpler respectfulness
*)
ML {*
fun r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
- REPEAT_ALL_NEW (FIRST' [
+ (FIRST' [
(K (print_tac "start")) THEN' (K no_tac),
+
+ (* "cong" rule of the of the relation *)
+ (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> (a \<approx> b) = (c \<approx> d) *)
DT ctxt "1" (resolve_tac trans2),
- DT ctxt "2" (LAMBDA_RES_TAC ctxt),
+
+ (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
+ DT ctxt "2" (LAMBDA_RES_TAC),
+
+ (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *)
DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
+
DT ctxt "4" (ball_rsp_tac ctxt),
DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
DT ctxt "6" (bex_rsp_tac ctxt),
+
+ (* respectfulness of ops *)
DT ctxt "7" (resolve_tac rsp_thms),
+
+ (* reflexivity of operators arising from Cong_tac *)
DT ctxt "8" (rtac @{thm refl}),
+
+ (* R (\<dots>) (Rep (Abs \<dots>)) \<Longrightarrow> R (\<dots>) (\<dots>) *)
+ (* observe ---> *)
DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt
THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
+
+ (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP provided type of t needs lifting *)
DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN'
(RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
+
+ (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *)
DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
+
+ (* = (\<lambda>x\<dots>) (\<lambda>x\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *)
DT ctxt "C" (rtac @{thm ext}),
+
+ (* reflexivity of the basic relations *)
DT ctxt "D" (resolve_tac rel_refl),
+
+ (* resolving with R x y assumptions *)
DT ctxt "E" (atac),
+
DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))
])
+
+fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
+ REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)
*}
+ML {*
+fun get_inj_repabs_tac ctxt rel lhs rhs =
+let
+ val _ = tracing "input"
+ val _ = tracing ("rel: " ^ Syntax.string_of_term ctxt rel)
+ val _ = tracing ("lhs: " ^ Syntax.string_of_term ctxt lhs)
+ val _ = tracing ("rhs: " ^ Syntax.string_of_term ctxt rhs)
+in
+ case (rel, lhs, rhs) of
+ (_, l, Const _ $ (Const _ $ r)) (* FIXME: not right_match *)
+ => rtac @{thm REP_ABS_RSP(1)}
+ | (_, Const (@{const_name "Ball"}, _) $ _,
+ Const (@{const_name "Ball"}, _) $ _)
+ => rtac @{thm RES_FORALL_RSP}
+ | _ => K no_tac
+end
+*}
-
+ML {*
+fun inj_repabs_tac ctxt =
+ SUBGOAL (fn (goal, i) =>
+ (case (HOLogic.dest_Trueprop goal) of
+ (rel $ lhs $ rhs) => get_inj_repabs_tac ctxt rel lhs rhs
+ | _ => K no_tac) i)
+*}
section {* Cleaning of the theorem *}