48 |
48 |
49 perm_noption \<equiv> "perm :: 'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" (unchecked) |
49 perm_noption \<equiv> "perm :: 'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" (unchecked) |
50 perm_nprod \<equiv> "perm :: 'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" (unchecked) |
50 perm_nprod \<equiv> "perm :: 'x prm \<Rightarrow> ('a, 'b) nprod \<Rightarrow> ('a, 'b) nprod" (unchecked) |
51 begin |
51 begin |
52 |
52 |
53 definition |
53 definition perm_fun :: "'x prm \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" where |
54 perm_fun_def: "perm_fun pi (f::'a\<Rightarrow>'b) = (\<lambda>x. pi\<bullet>f((rev pi)\<bullet>x))" |
54 "perm_fun pi f = (\<lambda>x. pi \<bullet> f (rev pi \<bullet> x))" |
55 |
55 |
56 definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where |
56 definition perm_bool :: "'x prm \<Rightarrow> bool \<Rightarrow> bool" where |
57 perm_bool_def: "perm_bool pi b = b" |
57 "perm_bool pi b = b" |
58 |
58 |
59 primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit" where |
59 primrec perm_unit :: "'x prm \<Rightarrow> unit \<Rightarrow> unit" where |
60 "perm_unit pi () = ()" |
60 "perm_unit pi () = ()" |
61 |
61 |
62 primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where |
62 primrec perm_prod :: "'x prm \<Rightarrow> ('a\<times>'b) \<Rightarrow> ('a\<times>'b)" where |
63 "perm_prod pi (x,y) = (pi\<bullet>x,pi\<bullet>y)" |
63 "perm_prod pi (x, y) = (pi\<bullet>x, pi\<bullet>y)" |
64 |
64 |
65 primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
65 primrec perm_list :: "'x prm \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
66 nil_eqvt: "perm_list pi [] = []" |
66 nil_eqvt: "perm_list pi [] = []" |
67 | cons_eqvt: "perm_list pi (x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)" |
67 | cons_eqvt: "perm_list pi (x#xs) = (pi\<bullet>x)#(pi\<bullet>xs)" |
68 |
68 |
69 primrec perm_option :: "'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" where |
69 primrec perm_option :: "'x prm \<Rightarrow> 'a option \<Rightarrow> 'a option" where |
70 some_eqvt: "perm_option pi (Some x) = Some (pi\<bullet>x)" |
70 some_eqvt: "perm_option pi (Some x) = Some (pi\<bullet>x)" |
71 | none_eqvt: "perm_option pi None = None" |
71 | none_eqvt: "perm_option pi None = None" |
72 |
72 |
73 definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where |
73 definition perm_char :: "'x prm \<Rightarrow> char \<Rightarrow> char" where |
74 perm_char_def: "perm_char pi c = c" |
74 "perm_char pi c = c" |
75 |
75 |
76 definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where |
76 definition perm_nat :: "'x prm \<Rightarrow> nat \<Rightarrow> nat" where |
77 perm_nat_def: "perm_nat pi i = i" |
77 "perm_nat pi i = i" |
78 |
78 |
79 definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where |
79 definition perm_int :: "'x prm \<Rightarrow> int \<Rightarrow> int" where |
80 perm_int_def: "perm_int pi i = i" |
80 "perm_int pi i = i" |
81 |
81 |
82 primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where |
82 primrec perm_noption :: "'x prm \<Rightarrow> 'a noption \<Rightarrow> 'a noption" where |
83 nsome_eqvt: "perm_noption pi (nSome x) = nSome (pi\<bullet>x)" |
83 nsome_eqvt: "perm_noption pi (nSome x) = nSome (pi\<bullet>x)" |
84 | nnone_eqvt: "perm_noption pi nNone = nNone" |
84 | nnone_eqvt: "perm_noption pi nNone = nNone" |
85 |
85 |
1026 have "pt TYPE('a \<Rightarrow> bool) TYPE('x)" by (rule pt_fun_inst) |
1026 have "pt TYPE('a \<Rightarrow> bool) TYPE('x)" by (rule pt_fun_inst) |
1027 then show ?thesis by (simp add: pt_def perm_set_def) |
1027 then show ?thesis by (simp add: pt_def perm_set_def) |
1028 qed |
1028 qed |
1029 |
1029 |
1030 lemma pt_unit_inst: |
1030 lemma pt_unit_inst: |
1031 shows "pt TYPE(unit) TYPE('x)" |
1031 shows "pt TYPE(unit) TYPE('x)" |
1032 by (simp add: pt_def) |
1032 by (simp add: pt_def) |
1033 |
1033 |
1034 lemma pt_prod_inst: |
1034 lemma pt_prod_inst: |
1035 assumes pta: "pt TYPE('a) TYPE('x)" |
1035 assumes pta: "pt TYPE('a) TYPE('x)" |
1036 and ptb: "pt TYPE('b) TYPE('x)" |
1036 and ptb: "pt TYPE('b) TYPE('x)" |