# HG changeset patch # User Cezary Kaliszyk # Date 1255100745 -7200 # Node ID fdaf1466daf0ccf9d3990470d33a6ec1723e2af0 # Parent 4efc9e6661a416ebc9609ad990169001837a25ef Further experiments with proving induction manually diff -r 4efc9e6661a4 -r fdaf1466daf0 QuotMain.thy --- a/QuotMain.thy Fri Oct 09 15:03:43 2009 +0200 +++ b/QuotMain.thy Fri Oct 09 17:05:45 2009 +0200 @@ -1102,25 +1102,28 @@ term "f ===> g" definition - "rfall p m = (\x. (p x \ m x))" + "res_forall p m = (\x. (x \ p \ m x))" + +definition + "res_exists p m = (\x. (x \ p \ m x))" -term "ABS_fset" -term "I" +(* The definition is total??? *) +definition + "x IN p ==> (res_abstract p m x = m x)" -term "(REP_fset ---> I) ---> I" -lemma "rfall (Respects ((op \) ===> (op =))) +lemma "(res_forall (Respects ((op \) ===> (op =))) (((REP_fset ---> id) ---> id) (((ABS_fset ---> id) ---> id) (\P. (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset [])) \ - rfall (Respects (op \)) + res_forall (Respects (op \)) ((ABS_fset ---> id) ((REP_fset ---> id) (\t. ((ABS_fset ---> id) ((REP_fset ---> id) P) - (REP_fset (ABS_fset t))) --> + (REP_fset (ABS_fset t))) \ (!h. (ABS_fset ---> id) ((REP_fset ---> id) P) @@ -1128,20 +1131,34 @@ (ABS_fset (h # REP_fset - (ABS_fset t)))))))) --> - rfall (Respects (op \)) + (ABS_fset t)))))))) \ + res_forall (Respects (op \)) ((ABS_fset ---> id) ((REP_fset ---> id) (\l. (ABS_fset ---> id) ((REP_fset ---> id) P) - (REP_fset (ABS_fset l))))))))" - -apply (unfold rfall_def) + (REP_fset (ABS_fset l)))))))))" +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 res_forall_def) apply (unfold id_def) apply (simp add: FUN_MAP_I) +apply (simp add:IN_RESPECTS) apply (simp add: QUOT_TYPE_I_fset.thm10) -. +apply (simp add:list_eq_refl) + + + +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) *} apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} )