1271 

  1272 section {* Infrastructure for concrete atom types *}

  1272 section {* library functions for the nominal infrastructure *}

  1273 

  1274 

  1275 section {* A swapping operation for concrete atoms *}

  1276   

  1277 definition

  1278   flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')")

  1279 where

  1280   "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"

  1281 

  1282 lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"

  1283   unfolding flip_def by (rule swap_self)

  1284 

  1285 lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)"

  1286   unfolding flip_def by (rule swap_commute)

  1287 

  1288 lemma minus_flip [simp]: "- (a \<leftrightarrow> b) = (a \<leftrightarrow> b)"

  1289   unfolding flip_def by (rule minus_swap)

  1290 

  1291 lemma add_flip_cancel: "(a \<leftrightarrow> b) + (a \<leftrightarrow> b) = 0"

  1292   unfolding flip_def by (rule swap_cancel)

  1293 

  1294 lemma permute_flip_cancel [simp]: "(a \<leftrightarrow> b) \<bullet> (a \<leftrightarrow> b) \<bullet> x = x"

  1295   unfolding permute_plus [symmetric] add_flip_cancel by simp

  1296 

  1297 lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x"

  1298   by (simp add: flip_commute)

  1299 

  1300 lemma flip_eqvt: 

  1301   fixes a b c::"'a::at_base"

  1302   shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)"

  1303   unfolding flip_def

  1304   by (simp add: swap_eqvt atom_eqvt)

  1305 

  1306 lemma flip_at_base_simps [simp]:

  1307   shows "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> a = b"

  1308   and   "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> b = a"

  1309   and   "\<lbrakk>a \<noteq> c; b \<noteq> c\<rbrakk> \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> c = c"

  1310   and   "sort_of (atom a) \<noteq> sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> x = x"

  1311   unfolding flip_def

  1312   unfolding atom_eq_iff [symmetric]

  1313   unfolding atom_eqvt [symmetric]

  1314   by simp_all

  1315 

  1316 text {* the following two lemmas do not hold for at_base, 

  1317   only for single sort atoms from at *}

  1318 

  1319 lemma permute_flip_at:

  1320   fixes a b c::"'a::at"

  1321   shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)"

  1322   unfolding flip_def

  1323   apply (rule atom_eq_iff [THEN iffD1])

  1324   apply (subst atom_eqvt [symmetric])

  1325   apply (simp add: swap_atom)

  1326   done

  1327 

  1328 lemma flip_at_simps [simp]:

  1329   fixes a b::"'a::at"

  1330   shows "(a \<leftrightarrow> b) \<bullet> a = b" 

  1331   and   "(a \<leftrightarrow> b) \<bullet> b = a"

  1332   unfolding permute_flip_at by simp_all

  1333 

  1334 lemma flip_fresh_fresh:

  1335   fixes a b::"'a::at_base"

  1336   assumes "atom a \<sharp> x" "atom b \<sharp> x"

  1337   shows "(a \<leftrightarrow> b) \<bullet> x = x"

  1338 using assms

  1339 by (simp add: flip_def swap_fresh_fresh)

  1340 

  1341 subsection {* Syntax for coercing at-elements to the atom-type *}

  1342 

  1343 syntax

  1344   "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3)

  1345 

  1346 translations

  1347   "_atom_constrain a t" => "CONST atom (_constrain a t)"

  1348 

  1349 

  1350 subsection {* A lemma for proving instances of class @{text at}. *}

  1351 

  1352 setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *}

  1353 setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *}

  1354 

  1355 text {*

  1356   New atom types are defined as subtypes of @{typ atom}.

  1357 *}

  1358 

  1359 lemma exists_eq_simple_sort: 

  1360   shows "\<exists>a. a \<in> {a. sort_of a = s}"

  1361   by (rule_tac x="Atom s 0" in exI, simp)

  1362 

  1363 lemma exists_eq_sort: 

  1364   shows "\<exists>a. a \<in> {a. sort_of a \<in> range sort_fun}"

  1365   by (rule_tac x="Atom (sort_fun x) y" in exI, simp)

  1366 

  1367 lemma at_base_class:

  1368   fixes sort_fun :: "'b \<Rightarrow>atom_sort"

  1369   fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"

  1370   assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}"

  1371   assumes atom_def: "\<And>a. atom a = Rep a"

  1372   assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"

  1373   shows "OFCLASS('a, at_base_class)"

  1374 proof

  1375   interpret type_definition Rep Abs "{a. sort_of a \<in> range sort_fun}" by (rule type)

  1376   have sort_of_Rep: "\<And>a. sort_of (Rep a) \<in> range sort_fun" using Rep by simp

  1377   fix a b :: 'a and p p1 p2 :: perm

  1378   show "0 \<bullet> a = a"

  1379     unfolding permute_def by (simp add: Rep_inverse)

  1380   show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"

  1381     unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)

  1382   show "atom a = atom b \<longleftrightarrow> a = b"

  1383     unfolding atom_def by (simp add: Rep_inject)

  1384   show "p \<bullet> atom a = atom (p \<bullet> a)"

  1385     unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)

  1386 qed

  1387 

  1388 (*

  1389 lemma at_class:

  1390   fixes s :: atom_sort

  1391   fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"

  1392   assumes type: "type_definition Rep Abs {a. sort_of a \<in> range (\<lambda>x::unit. s)}"

  1393   assumes atom_def: "\<And>a. atom a = Rep a"

  1394   assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"

  1395   shows "OFCLASS('a, at_class)"

  1396 proof

  1397   interpret type_definition Rep Abs "{a. sort_of a \<in> range (\<lambda>x::unit. s)}" by (rule type)

  1398   have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)

  1399   fix a b :: 'a and p p1 p2 :: perm

  1400   show "0 \<bullet> a = a"

  1401     unfolding permute_def by (simp add: Rep_inverse)

  1402   show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"

  1403     unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)

  1404   show "sort_of (atom a) = sort_of (atom b)"

  1405     unfolding atom_def by (simp add: sort_of_Rep)

  1406   show "atom a = atom b \<longleftrightarrow> a = b"

  1407     unfolding atom_def by (simp add: Rep_inject)

  1408   show "p \<bullet> atom a = atom (p \<bullet> a)"

  1409     unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)

  1410 qed

  1411 *)

  1412 

  1413 lemma at_class:

  1414   fixes s :: atom_sort

  1415   fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"

  1416   assumes type: "type_definition Rep Abs {a. sort_of a = s}"

  1417   assumes atom_def: "\<And>a. atom a = Rep a"

  1418   assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"

  1419   shows "OFCLASS('a, at_class)"

  1420 proof

  1421   interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type)

  1422   have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)

  1423   fix a b :: 'a and p p1 p2 :: perm

  1424   show "0 \<bullet> a = a"

  1425     unfolding permute_def by (simp add: Rep_inverse)

  1426   show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"

  1427     unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)

  1428   show "sort_of (atom a) = sort_of (atom b)"

  1429     unfolding atom_def by (simp add: sort_of_Rep)

  1430   show "atom a = atom b \<longleftrightarrow> a = b"

  1431     unfolding atom_def by (simp add: Rep_inject)

  1432   show "p \<bullet> atom a = atom (p \<bullet> a)"

  1433     unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)

  1434 qed

  1435 

  1436 setup {* Sign.add_const_constraint

  1437   (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *}

  1438 setup {* Sign.add_const_constraint

  1439   (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *}

  1440 

  1441 

  1442 section {* Library functions for the nominal infrastructure *}

  1443 

  1276 

  1447 section {* Automation for creating concrete atom types *}

  1277 end

  1448 

  1449 text {* at the moment only single-sort concrete atoms are supported *}

  1450 

  1451 use "nominal_atoms.ML"

  1452 

  1453 

  1454 

  1455 end