equal
deleted
inserted
replaced
323 ML {* |
323 ML {* |
324 cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context}) |
324 cterm_of @{theory} (tyRel @{typ "trm \<Rightarrow> bool"} @{typ "trm"} @{term "RR"} @{context}) |
325 *} |
325 *} |
326 |
326 |
327 definition |
327 definition |
328 "(x : p) \<Longrightarrow> (Babs p m x = m x)" |
328 Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" |
|
329 where |
|
330 "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)" |
|
331 |
|
332 (* Babs p m = \<lambda>x. if x \<in> p then m x else undefined *) |
329 |
333 |
330 (*definition BAll :: "('a \<Rightarrow> prop) \<Rightarrow> ('a \<Rightarrow> prop) \<Rightarrow> prop" where |
334 (*definition BAll :: "('a \<Rightarrow> prop) \<Rightarrow> ('a \<Rightarrow> prop) \<Rightarrow> prop" where |
331 "BAll (R :: 'a \<Rightarrow> prop) (P :: 'a \<Rightarrow> prop) \<equiv> (\<And>x. (PROP R x \<Longrightarrow> PROP P x))"*) |
335 "BAll (R :: 'a \<Rightarrow> prop) (P :: 'a \<Rightarrow> prop) \<equiv> (\<And>x. (PROP R x \<Longrightarrow> PROP P x))"*) |
332 |
336 |
333 |
337 |
1139 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1143 apply (tactic {* LocalDefs.unfold_tac @{context} fset_defs *} ) |
1140 apply (atomize(full)) |
1144 apply (atomize(full)) |
1141 apply (tactic {* foo_tac' @{context} 1 *}) |
1145 apply (tactic {* foo_tac' @{context} 1 *}) |
1142 done |
1146 done |
1143 |
1147 |
1144 thm list.induct |
1148 ML {* val li = Thm.freezeT (atomize_thm @{thm list.induct}) *} |
1145 lemma list_induct2: |
|
1146 shows "(P []) \<Longrightarrow> (\<forall> a list. ((P list) \<longrightarrow> (P (a # list)))) \<Longrightarrow> \<forall>l :: 'a list. (P l)" |
|
1147 apply (rule allI) |
|
1148 apply (rule list.induct) |
|
1149 apply (assumption) |
|
1150 apply (auto) |
|
1151 done |
|
1152 |
|
1153 ML {* ObjectLogic.atomize (cprop_of @{thm list_induct2}) *} |
|
1154 ML {* (atomize_thm @{thm list_induct2}) *} |
|
1155 |
|
1156 ML {* val li = Thm.freezeT (atomize_thm @{thm list_induct2}) *} |
|
1157 |
1149 |
1158 (* TODO: the following 2 lemmas should go to quotscript.thy after all are done *) |
1150 (* TODO: the following 2 lemmas should go to quotscript.thy after all are done *) |
1159 lemma RIGHT_RES_FORALL_REGULAR: |
1151 lemma RIGHT_RES_FORALL_REGULAR: |
1160 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
1152 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
1161 shows "All P ==> Ball R Q" |
1153 shows "All P ==> Ball R Q" |
1337 (REP_fset (ABS_fset l))))))))) |
1329 (REP_fset (ABS_fset l))))))))) |
1338 |
1330 |
1339 = Ball (Respects ((op \<approx>) ===> (op =))) |
1331 = Ball (Respects ((op \<approx>) ===> (op =))) |
1340 (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow> |
1332 (\<lambda>P. ((P []) \<and> (Ball (Respects (op \<approx>)) (\<lambda>t. P t \<longrightarrow> (\<forall>h. (P (h # t)))))) \<longrightarrow> |
1341 (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))" |
1333 (Ball (Respects (op \<approx>)) (\<lambda>l. P l)))" |
|
1334 thm APPLY_RSP |
|
1335 thm APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op =" "id" "id"] |
|
1336 apply (rule APPLY_RSP[of "op \<approx> ===> (op = ===> op =)" _ _ "op ="]) |
1342 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))" |
1337 term "(\<forall>P. (((P []) \<and> (\<forall>t. (P t \<longrightarrow> (\<forall>h. P (h # t))))) \<longrightarrow> (\<forall>l. (P l))))" |
1343 thm LAMBDA_PRS1[symmetric] |
1338 thm LAMBDA_PRS1[symmetric] |
1344 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*) |
1339 (*apply (simp only:LAMBDA_PRS1[symmetric] FUN_QUOTIENT IDENTITY_QUOTIENT QUOT_TYPE_I_fset.QUOTIENT)*) |
1345 apply (unfold Ball_def) |
1340 apply (unfold Ball_def) |
1346 apply (simp only: IN_RESPECTS) |
1341 apply (simp only: IN_RESPECTS) |