--- a/QuotMain.thy Wed Oct 21 14:15:22 2009 +0200
+++ b/QuotMain.thy Wed Oct 21 14:30:29 2009 +0200
@@ -1133,6 +1133,7 @@
*)
thm list_eq.intros(5)
+(* prove {* build_repabs_goal @{context} (atomize_thm @{thm list_eq.intros(5)}) consts @{typ "'a list"} @{typ "'a fset"} *} *)
ML {*
val m1_novars = snd(no_vars ((Context.Theory @{theory}), @{thm list_eq.intros(5)}))
val goal = build_repabs_goal @{context} m1_novars consts @{typ "'a list"} @{typ "'a fset"}
@@ -1153,9 +1154,6 @@
ML {* atomize_thm @{thm list_induct_hol4} *}
-
-ML {* val li = atomize_thm @{thm list_induct_hol4} *}
-
prove list_induct_r: {*
build_regularize_goal (atomize_thm @{thm list_induct_hol4}) @{typ "'a List.list"} @{term "op \<approx>"} @{context} *}
apply (simp only: equiv_res_forall[OF equiv_list_eq])
@@ -1431,177 +1429,6 @@
)
*}
-lemma "(Ball (Respects ((op \<approx>) ===> (op =)))
- (((REP_fset ---> id) ---> id)
- (((ABS_fset ---> id) ---> id)
- (\<lambda>P.
- (ABS_fset ---> id) ((REP_fset ---> id) P)
- (REP_fset (ABS_fset [])) \<and>
- Ball (Respects (op \<approx>))
- ((ABS_fset ---> id)
- ((REP_fset ---> id)
- (\<lambda>t.
- ((ABS_fset ---> id)
- ((REP_fset ---> id) P)
- (REP_fset (ABS_fset t))) \<longrightarrow>
- (!h.
- (ABS_fset ---> id)
- ((REP_fset ---> id) P)
- (REP_fset
- (ABS_fset
- (h #
- REP_fset
- (ABS_fset t)))))))) \<longrightarrow>
- Ball (Respects (op \<approx>))
- ((ABS_fset ---> id)
- ((REP_fset ---> id)
- (\<lambda>l.
- (ABS_fset ---> id)
- ((REP_fset ---> id) P)
- (REP_fset (ABS_fset l)))))))))
-
- = Ball (Respects ((op \<approx>) ===> (op =)))
- (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow>
- (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))"
-
-thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"]
-proof -
-note APPLY_RSP_I = APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"]
-show ?thesis apply -
-
-
-ML_prf {*
- val gc = Subgoal.focus @{context} 1 (Isar.goal ())
- |> fst
- |> #concl
- val tc = cterm_of @{theory} (concl_of ( @{thm "APPLY_RSP" }))
- val (_, tc') = Thm.dest_comb tc
- val (_, gc') = Thm.dest_comb gc
- *}
-
-
-
-
-ML_prf {*
- (gc', tc')
-*}
-ML_prf {* Pattern.first_order_match *}
-ML_prf {* Thm.match (@{cpat "?P::?'a"}, @{cterm "1::nat"}) *}
-ML_prf {* Pattern.match @{theory} (term_of @{cpat "?P::nat"}, term_of @{cterm "1::nat"}) (Vartab.empty, Vartab.empty) *}
-
-ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *}
-ML_prf {* val (op2, (l2, r2)) = dest_cbinop gc' *}
-
-ML_prf {* val mo = Thm.match (op1, op2) *}
-ML_prf {* val t1 = Drule.instantiate mo @{thm "APPLY_RSP" } *}
-ML_prf {* val tc = cterm_of @{theory} (concl_of t1) *}
-ML_prf {* val (_, tc') = Thm.dest_comb tc *}
-ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *}
-ML_prf {* val (mlty, mlt) = Thm.match (l1, l2) *}
-ML_prf {* val t2 = Drule.instantiate (mlty, []) t1 *}
-ML_prf {* val tc = cterm_of @{theory} (concl_of t2) *}
-ML_prf {* val (_, tc') = Thm.dest_comb tc *}
-ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *}
-ML_prf {* val mr = Thm.match (r1, r2) *}
-
-ML_prf {* val t3 = Drule.instantiate ml t2 *}
-ML_prf {* val tc = cterm_of @{theory} (concl_of t3) *}
-ML_prf {* val (_, tc') = Thm.dest_comb tc *}
-
-
-
-ML_prf {* mtyl; mtyr *}
-
-ML_prf {* val ol1 = Thm.capply op1 l1 *}
-ML_prf {* val ol2 = Thm.capply op2 l2 *}
-ML_prf {* (ol1, ol2); Thm.match (ol1, ol2) *}
-ML_prf {* val w1 = Thm.capply ol1 r1 *}
-ML_prf {* val w2 = Thm.capply ol2 r2 *}
-
-
-.
-(*ML_prf {* (w1, w2); Thm.match (w1, w2) *}*)
-
-
-
-ML_prf {*
- (tc', gc')
-*}
-
-thm APPLY_RSP
-thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)"]
-term "(op \<approx> ===> op =) ===> op ="
-proof -
-note APPLY_RSP_I2 = APPLY_RSP[of "(op \<approx> ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id" "Ball (Respects op \<approx> ===> op =)" "Ball (Respects op \<approx> ===> op =)"]
-show ?thesis apply -
-
-thm APPLY_RSP_I2[of _ "\<lambda>P. (P [] \<and> (\<forall>t\<Colon>'b list\<in>Respects op \<approx>. P t \<longrightarrow> (\<forall>h\<Colon>'b. P (h # t))) \<longrightarrow>
- (\<forall>l\<Colon>'b list\<in>Respects op \<approx>. P l))"]
-proof -
-note APPLY_RSP_I3=APPLY_RSP_I2[of _ "\<lambda>P. (P [] \<and> (\<forall>t\<Colon>'b list\<in>Respects op \<approx>. P t \<longrightarrow> (\<forall>h\<Colon>'b. P (h # t))) \<longrightarrow>
- (\<forall>l\<Colon>'b list\<in>Respects op \<approx>. P l))"]
-show ?thesis apply -
-term "(REP_fset ---> id ---> id
- (ABS_fset ---> id ---> id
- (\<lambda>P\<Colon>'a list \<Rightarrow> bool.
- ABS_fset ---> id (REP_fset ---> id P)
- (REP_fset (ABS_fset [])) \<and>
- Ball (Respects op \<approx>)
- (ABS_fset ---> id
- (REP_fset ---> id
- (\<lambda>t\<Colon>'a list.
- ABS_fset ---> id (REP_fset ---> id P)
- (REP_fset (ABS_fset t)) \<longrightarrow>
- (\<forall>h\<Colon>'a.
- ABS_fset ---> id (REP_fset ---> id P)
- (REP_fset
- (ABS_fset
- (h # REP_fset (ABS_fset t)))))))) \<longrightarrow>
- Ball (Respects op \<approx>)
- (ABS_fset ---> id
- (REP_fset ---> id
- (\<lambda>l\<Colon>'a list.
- ABS_fset ---> id (REP_fset ---> id P)
- (REP_fset (ABS_fset l))))))))"
-
-apply (rule APPLY_RSP_I3)
-term "Ball (Respects op \<approx> ===> op =)"
-thm APPLY_RSP_I [of _ "Ball (Respects op \<approx> ===> op =)"]
-
-thm APPLY_RSP
-
-.
-
-apply (tactic {* Cong_Tac.cong_tac @{thm APPLY_RSP_I} 1 *} )
-
-apply (tactic {* match_tac @{thms APPLY_RSP_I} 1 *})
- .
-
-apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"])
-apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op ="])
-term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))"
-thm LAMBDA_PRS1[symmetric]
-(*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*)
-apply (unfold Ball_def)
-apply (simp only: IN_RESPECTS)
-apply (simp only:list_eq_refl)
-apply (unfold id_def)
-(*apply (simp only: FUN_MAP_I)*)
-apply (simp)
-apply (simp only: QUOT_TYPE_I_fset.thm10)
-..
-apply (simp add:IN_RESPECTS)
-
-
-
-
-apply (simp add: QUOT_TYPE_I_fset.R_trans2)
-
-apply (rule ext)
-apply (simp add:QUOT_TYPE_I_fset.REP_ABS_rsp)
-apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *} )
-apply (simp add:cons_preserves)
-
(*prove aaa: {* (Thm.term_of cgoal2) *}