equal
deleted
inserted
replaced
1359 apply(rule subst[OF permute_fun_app_eq]) |
1359 apply(rule subst[OF permute_fun_app_eq]) |
1360 apply(simp) |
1360 apply(simp) |
1361 apply(rule THE_defaultI'[OF unique]) |
1361 apply(rule THE_defaultI'[OF unique]) |
1362 done |
1362 done |
1363 |
1363 |
|
1364 lemma fundef_ex1_eqvt2: |
|
1365 fixes x::"'a::pt" |
|
1366 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
|
1367 assumes eqvt: "eqvt_at G x" |
|
1368 assumes ex1: "\<exists>!y. G x y" |
|
1369 shows "(p \<bullet> (f x)) = f (p \<bullet> x)" |
|
1370 apply(simp only: f_def) |
|
1371 apply(subst the_default_eqvt) |
|
1372 apply(rule ex1) |
|
1373 using eqvt |
|
1374 unfolding eqvt_at_def |
|
1375 apply(simp) |
|
1376 done |
|
1377 |
1364 lemma fundef_ex1_eqvt: |
1378 lemma fundef_ex1_eqvt: |
1365 fixes x::"'a::pt" |
1379 fixes x::"'a::pt" |
1366 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
1380 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
1367 assumes eqvt: "eqvt G" |
1381 assumes eqvt: "eqvt G" |
1368 assumes ex1: "\<exists>!y. G x y" |
1382 assumes ex1: "\<exists>!y. G x y" |
1373 using eqvt |
1387 using eqvt |
1374 unfolding eqvt_def |
1388 unfolding eqvt_def |
1375 apply(simp add: permute_fun_app_eq) |
1389 apply(simp add: permute_fun_app_eq) |
1376 done |
1390 done |
1377 |
1391 |
|
1392 lemma fundef_ex1_eqvt_at2: |
|
1393 fixes x::"'a::pt" |
|
1394 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
|
1395 assumes eqvt: "eqvt_at G x" |
|
1396 assumes ex1: "\<exists>!y. G x y" |
|
1397 shows "eqvt_at f x" |
|
1398 unfolding eqvt_at_def |
|
1399 using assms |
|
1400 by (auto intro: fundef_ex1_eqvt2) |
|
1401 |
1378 lemma fundef_ex1_eqvt_at: |
1402 lemma fundef_ex1_eqvt_at: |
1379 fixes x::"'a::pt" |
1403 fixes x::"'a::pt" |
1380 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
1404 assumes f_def: "f == (\<lambda>x::'a. THE_default d (G x))" |
1381 assumes eqvt: "eqvt G" |
1405 assumes eqvt: "eqvt G" |
1382 assumes ex1: "\<exists>!y. G x y" |
1406 assumes ex1: "\<exists>!y. G x y" |
1383 shows "eqvt_at f x" |
1407 shows "eqvt_at f x" |
1384 unfolding eqvt_at_def |
1408 unfolding eqvt_at_def |
1385 using assms |
1409 using assms |
1386 by (auto intro: fundef_ex1_eqvt) |
1410 by (auto intro: fundef_ex1_eqvt) |
1387 |
|
1388 |
1411 |
1389 section {* Support of Finite Sets of Finitely Supported Elements *} |
1412 section {* Support of Finite Sets of Finitely Supported Elements *} |
1390 |
1413 |
1391 text {* support and freshness for atom sets *} |
1414 text {* support and freshness for atom sets *} |
1392 |
1415 |