# HG changeset patch # User Cezary Kaliszyk # Date 1256128229 -7200 # Node ID ec772b461e26f4bbaf32331c17efc1a15803f9c9 # Parent 0ffc37761e537888f86449423a3be79f7f5f3c6e Cleaning the code diff -r 0ffc37761e53 -r ec772b461e26 QuotMain.thy --- 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 \"} @{context} *} apply (simp only: equiv_res_forall[OF equiv_list_eq]) @@ -1431,177 +1429,6 @@ ) *} -lemma "(Ball (Respects ((op \) ===> (op =))) - (((REP_fset ---> id) ---> id) - (((ABS_fset ---> id) ---> id) - (\P. - (ABS_fset ---> id) ((REP_fset ---> id) P) - (REP_fset (ABS_fset [])) \ - Ball (Respects (op \)) - ((ABS_fset ---> id) - ((REP_fset ---> id) - (\t. - ((ABS_fset ---> id) - ((REP_fset ---> id) P) - (REP_fset (ABS_fset t))) \ - (!h. - (ABS_fset ---> id) - ((REP_fset ---> id) P) - (REP_fset - (ABS_fset - (h # - REP_fset - (ABS_fset t)))))))) \ - Ball (Respects (op \)) - ((ABS_fset ---> id) - ((REP_fset ---> id) - (\l. - (ABS_fset ---> id) - ((REP_fset ---> id) P) - (REP_fset (ABS_fset l))))))))) - - = Ball (Respects ((op \) ===> (op =))) - (\P. ((P []) \ (Ball (Respects (op \)) (\t. P t \ (\h. (P (h # t)))))) \ - (Ball (Respects (op \)) (\l. P l)))" - -thm APPLY_RSP[of "op \ ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"] -proof - -note APPLY_RSP_I = APPLY_RSP[of "op \ ===> (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 \ ===> (op = ===> op =)"] -term "(op \ ===> op =) ===> op =" -proof - -note APPLY_RSP_I2 = APPLY_RSP[of "(op \ ===> op =) ===> op =" "(ABS_fset ---> id) ---> id" "(REP_fset ---> id) ---> id" "op =" "id" "id" "Ball (Respects op \ ===> op =)" "Ball (Respects op \ ===> op =)"] -show ?thesis apply - - -thm APPLY_RSP_I2[of _ "\P. (P [] \ (\t\'b list\Respects op \. P t \ (\h\'b. P (h # t))) \ - (\l\'b list\Respects op \. P l))"] -proof - -note APPLY_RSP_I3=APPLY_RSP_I2[of _ "\P. (P [] \ (\t\'b list\Respects op \. P t \ (\h\'b. P (h # t))) \ - (\l\'b list\Respects op \. P l))"] -show ?thesis apply - -term "(REP_fset ---> id ---> id - (ABS_fset ---> id ---> id - (\P\'a list \ bool. - ABS_fset ---> id (REP_fset ---> id P) - (REP_fset (ABS_fset [])) \ - Ball (Respects op \) - (ABS_fset ---> id - (REP_fset ---> id - (\t\'a list. - ABS_fset ---> id (REP_fset ---> id P) - (REP_fset (ABS_fset t)) \ - (\h\'a. - ABS_fset ---> id (REP_fset ---> id P) - (REP_fset - (ABS_fset - (h # REP_fset (ABS_fset t)))))))) \ - Ball (Respects op \) - (ABS_fset ---> id - (REP_fset ---> id - (\l\'a list. - ABS_fset ---> id (REP_fset ---> id P) - (REP_fset (ABS_fset l))))))))" - -apply (rule APPLY_RSP_I3) -term "Ball (Respects op \ ===> op =)" -thm APPLY_RSP_I [of _ "Ball (Respects op \ ===> 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 \ ===> (op = ===> op =)" "REP_fset ---> (id ---> id)" "ABS_fset ---> (id ---> id)" "op =" "id" "id"]) -apply (rule APPLY_RSP[of "op \ ===> (op = ===> op =)" _ _ "op ="]) -term "(\P. (((P []) \ (\t. (P t \ (\h. P (h # t))))) \ (\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) *}