540 lemma fs1_strong_cases: |
540 lemma fs1_strong_cases: |
541 fixes X :: "'a list" |
541 fixes X :: "'a list" |
542 shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))" |
542 shows "(X = []) \<or> (\<exists>a. \<exists> Y. (~(a memb Y) \<and> (X \<approx> a # Y)))" |
543 apply (induct X) |
543 apply (induct X) |
544 apply (simp) |
544 apply (simp) |
545 apply (erule disjE) |
545 apply (metis QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons QuotMain.m1) |
546 apply (metis QuotMain.m1 list_eq_refl) |
|
547 apply (metis QUOT_TYPE_I_fset.R_sym QUOT_TYPE_I_fset.thm11 list_eq_refl mem_cons) |
|
548 done |
546 done |
|
547 |
549 |
548 |
550 text {* |
549 text {* |
551 Unabs_def converts a definition given as |
550 Unabs_def converts a definition given as |
552 |
551 |
553 c \<equiv> %x. %y. f x y |
552 c \<equiv> %x. %y. f x y |
1096 cterm_of @{theory} goal |
1095 cterm_of @{theory} goal |
1097 ); |
1096 ); |
1098 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1097 val cgoal2 = Thm.rhs_of (MetaSimplifier.rewrite true fset_defs_sym cgoal) |
1099 *} |
1098 *} |
1100 ML {* @{term "\<exists>x. P x"} *} |
1099 ML {* @{term "\<exists>x. P x"} *} |
1101 ML {* Thm.bicompose *} |
1100 |
1102 prove aaa: {* (Thm.term_of cgoal2) *} |
1101 term "f ---> g" |
|
1102 term "f ===> g" |
|
1103 |
|
1104 definition |
|
1105 "rfall p m = (\<forall>x. (p x \<longrightarrow> m x))" |
|
1106 |
|
1107 term "ABS_fset" |
|
1108 term "I" |
|
1109 |
|
1110 term "(REP_fset ---> I) ---> I" |
|
1111 lemma "rfall (Respects ((op \<approx>) ===> (op =))) |
|
1112 (((REP_fset ---> id) ---> id) |
|
1113 (((ABS_fset ---> id) ---> id) |
|
1114 (\<lambda>P. |
|
1115 (ABS_fset ---> id) ((REP_fset ---> id) P) |
|
1116 (REP_fset (ABS_fset [])) \<and> |
|
1117 rfall (Respects (op \<approx>)) |
|
1118 ((ABS_fset ---> id) |
|
1119 ((REP_fset ---> id) |
|
1120 (\<lambda>t. |
|
1121 ((ABS_fset ---> id) |
|
1122 ((REP_fset ---> id) P) |
|
1123 (REP_fset (ABS_fset t))) --> |
|
1124 (!h. |
|
1125 (ABS_fset ---> id) |
|
1126 ((REP_fset ---> id) P) |
|
1127 (REP_fset |
|
1128 (ABS_fset |
|
1129 (h # |
|
1130 REP_fset |
|
1131 (ABS_fset t)))))))) --> |
|
1132 rfall (Respects (op \<approx>)) |
|
1133 ((ABS_fset ---> id) |
|
1134 ((REP_fset ---> id) |
|
1135 (\<lambda>l. |
|
1136 (ABS_fset ---> id) |
|
1137 ((REP_fset ---> id) P) |
|
1138 (REP_fset (ABS_fset l))))))))" |
|
1139 |
|
1140 apply (unfold rfall_def) |
|
1141 apply (unfold id_def) |
|
1142 apply (simp add: FUN_MAP_I) |
|
1143 apply (simp add: QUOT_TYPE_I_fset.thm10) |
|
1144 . |
|
1145 |
|
1146 (*prove aaa: {* (Thm.term_of cgoal2) *} |
1103 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1147 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1104 apply (atomize(full)) |
1148 apply (atomize(full)) |
1105 apply (tactic {* foo_tac' @{context} 1 *}) |
1149 apply (tactic {* foo_tac' @{context} 1 *}) |
1106 done |
1150 done*) |
1107 |
1151 |
1108 (* |
1152 (* |
1109 datatype obj1 = |
1153 datatype obj1 = |
1110 OVAR1 "string" |
1154 OVAR1 "string" |
1111 | OBJ1 "(string * (string \<Rightarrow> obj1)) list" |
1155 | OBJ1 "(string * (string \<Rightarrow> obj1)) list" |