author | wenzelm |
Sun, 16 Sep 2007 14:55:48 +0200 | |
changeset 24600 | 5877b88f262c |
parent 21887 | b1137bd73012 |
child 25601 | 24567e50ebcc |
permissions | -rw-r--r-- |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
1 |
(* Title : HOL/Hyperreal/StarDef.thy |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
2 |
ID : $Id$ |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
3 |
Author : Jacques D. Fleuriot and Brian Huffman |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
4 |
*) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
5 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
6 |
header {* Construction of Star Types Using Ultrafilters *} |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
7 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
8 |
theory StarDef |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
9 |
imports Filter |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
10 |
uses ("transfer.ML") |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
11 |
begin |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
12 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
13 |
subsection {* A Free Ultrafilter over the Naturals *} |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
14 |
|
19765 | 15 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
16 |
FreeUltrafilterNat :: "nat set set" ("\<U>") where |
19765 | 17 |
"\<U> = (SOME U. freeultrafilter U)" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
18 |
|
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
19 |
lemma freeultrafilter_FreeUltrafilterNat: "freeultrafilter \<U>" |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
20 |
apply (unfold FreeUltrafilterNat_def) |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
21 |
apply (rule someI_ex) |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
22 |
apply (rule freeultrafilter_Ex) |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
23 |
apply (rule nat_infinite) |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
24 |
done |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
25 |
|
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
26 |
interpretation FreeUltrafilterNat: freeultrafilter [FreeUltrafilterNat] |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
27 |
by (rule freeultrafilter_FreeUltrafilterNat) |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
28 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
29 |
text {* This rule takes the place of the old ultra tactic *} |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
30 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
31 |
lemma ultra: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
32 |
"\<lbrakk>{n. P n} \<in> \<U>; {n. P n \<longrightarrow> Q n} \<in> \<U>\<rbrakk> \<Longrightarrow> {n. Q n} \<in> \<U>" |
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
33 |
by (simp add: Collect_imp_eq |
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
34 |
FreeUltrafilterNat.Un_iff FreeUltrafilterNat.Compl_iff) |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
35 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
36 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
37 |
subsection {* Definition of @{text star} type constructor *} |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
38 |
|
19765 | 39 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
40 |
starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set" where |
19765 | 41 |
"starrel = {(X,Y). {n. X n = Y n} \<in> \<U>}" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
42 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
43 |
typedef 'a star = "(UNIV :: (nat \<Rightarrow> 'a) set) // starrel" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
44 |
by (auto intro: quotientI) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
45 |
|
19765 | 46 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
47 |
star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star" where |
19765 | 48 |
"star_n X = Abs_star (starrel `` {X})" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
49 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
50 |
theorem star_cases [case_names star_n, cases type: star]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
51 |
"(\<And>X. x = star_n X \<Longrightarrow> P) \<Longrightarrow> P" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
52 |
by (cases x, unfold star_n_def star_def, erule quotientE, fast) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
53 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
54 |
lemma all_star_eq: "(\<forall>x. P x) = (\<forall>X. P (star_n X))" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
55 |
by (auto, rule_tac x=x in star_cases, simp) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
56 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
57 |
lemma ex_star_eq: "(\<exists>x. P x) = (\<exists>X. P (star_n X))" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
58 |
by (auto, rule_tac x=x in star_cases, auto) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
59 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
60 |
text {* Proving that @{term starrel} is an equivalence relation *} |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
61 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
62 |
lemma starrel_iff [iff]: "((X,Y) \<in> starrel) = ({n. X n = Y n} \<in> \<U>)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
63 |
by (simp add: starrel_def) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
64 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
65 |
lemma equiv_starrel: "equiv UNIV starrel" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
66 |
proof (rule equiv.intro) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
67 |
show "reflexive starrel" by (simp add: refl_def) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
68 |
show "sym starrel" by (simp add: sym_def eq_commute) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
69 |
show "trans starrel" by (auto intro: transI elim!: ultra) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
70 |
qed |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
71 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
72 |
lemmas equiv_starrel_iff = |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
73 |
eq_equiv_class_iff [OF equiv_starrel UNIV_I UNIV_I] |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
74 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
75 |
lemma starrel_in_star: "starrel``{x} \<in> star" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
76 |
by (simp add: star_def quotientI) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
77 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
78 |
lemma star_n_eq_iff: "(star_n X = star_n Y) = ({n. X n = Y n} \<in> \<U>)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
79 |
by (simp add: star_n_def Abs_star_inject starrel_in_star equiv_starrel_iff) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
80 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
81 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
82 |
subsection {* Transfer principle *} |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
83 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
84 |
text {* This introduction rule starts each transfer proof. *} |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
85 |
lemma transfer_start: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
86 |
"P \<equiv> {n. Q} \<in> \<U> \<Longrightarrow> Trueprop P \<equiv> Trueprop Q" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
87 |
by (subgoal_tac "P \<equiv> Q", simp, simp add: atomize_eq) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
88 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
89 |
text {*Initialize transfer tactic.*} |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
90 |
use "transfer.ML" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
91 |
setup Transfer.setup |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
92 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
93 |
text {* Transfer introduction rules. *} |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
94 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
95 |
lemma transfer_ex [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
96 |
"\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk> |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
97 |
\<Longrightarrow> \<exists>x::'a star. p x \<equiv> {n. \<exists>x. P n x} \<in> \<U>" |
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
98 |
by (simp only: ex_star_eq FreeUltrafilterNat.Collect_ex) |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
99 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
100 |
lemma transfer_all [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
101 |
"\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk> |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
102 |
\<Longrightarrow> \<forall>x::'a star. p x \<equiv> {n. \<forall>x. P n x} \<in> \<U>" |
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
103 |
by (simp only: all_star_eq FreeUltrafilterNat.Collect_all) |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
104 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
105 |
lemma transfer_not [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
106 |
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>\<rbrakk> \<Longrightarrow> \<not> p \<equiv> {n. \<not> P n} \<in> \<U>" |
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
107 |
by (simp only: FreeUltrafilterNat.Collect_not) |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
108 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
109 |
lemma transfer_conj [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
110 |
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk> |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
111 |
\<Longrightarrow> p \<and> q \<equiv> {n. P n \<and> Q n} \<in> \<U>" |
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
112 |
by (simp only: FreeUltrafilterNat.Collect_conj) |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
113 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
114 |
lemma transfer_disj [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
115 |
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk> |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
116 |
\<Longrightarrow> p \<or> q \<equiv> {n. P n \<or> Q n} \<in> \<U>" |
21787
9edd495b6330
consistent naming for FreeUltrafilterNat lemmas; cleaned up
huffman
parents:
21404
diff
changeset
|
117 |
by (simp only: FreeUltrafilterNat.Collect_disj) |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
118 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
119 |
lemma transfer_imp [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
120 |
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk> |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
121 |
\<Longrightarrow> p \<longrightarrow> q \<equiv> {n. P n \<longrightarrow> Q n} \<in> \<U>" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
122 |
by (simp only: imp_conv_disj transfer_disj transfer_not) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
123 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
124 |
lemma transfer_iff [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
125 |
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; q \<equiv> {n. Q n} \<in> \<U>\<rbrakk> |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
126 |
\<Longrightarrow> p = q \<equiv> {n. P n = Q n} \<in> \<U>" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
127 |
by (simp only: iff_conv_conj_imp transfer_conj transfer_imp) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
128 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
129 |
lemma transfer_if_bool [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
130 |
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> {n. X n} \<in> \<U>; y \<equiv> {n. Y n} \<in> \<U>\<rbrakk> |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
131 |
\<Longrightarrow> (if p then x else y) \<equiv> {n. if P n then X n else Y n} \<in> \<U>" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
132 |
by (simp only: if_bool_eq_conj transfer_conj transfer_imp transfer_not) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
133 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
134 |
lemma transfer_eq [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
135 |
"\<lbrakk>x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> \<Longrightarrow> x = y \<equiv> {n. X n = Y n} \<in> \<U>" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
136 |
by (simp only: star_n_eq_iff) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
137 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
138 |
lemma transfer_if [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
139 |
"\<lbrakk>p \<equiv> {n. P n} \<in> \<U>; x \<equiv> star_n X; y \<equiv> star_n Y\<rbrakk> |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
140 |
\<Longrightarrow> (if p then x else y) \<equiv> star_n (\<lambda>n. if P n then X n else Y n)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
141 |
apply (rule eq_reflection) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
142 |
apply (auto simp add: star_n_eq_iff transfer_not elim!: ultra) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
143 |
done |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
144 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
145 |
lemma transfer_fun_eq [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
146 |
"\<lbrakk>\<And>X. f (star_n X) = g (star_n X) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
147 |
\<equiv> {n. F n (X n) = G n (X n)} \<in> \<U>\<rbrakk> |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
148 |
\<Longrightarrow> f = g \<equiv> {n. F n = G n} \<in> \<U>" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
149 |
by (simp only: expand_fun_eq transfer_all) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
150 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
151 |
lemma transfer_star_n [transfer_intro]: "star_n X \<equiv> star_n (\<lambda>n. X n)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
152 |
by (rule reflexive) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
153 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
154 |
lemma transfer_bool [transfer_intro]: "p \<equiv> {n. p} \<in> \<U>" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
155 |
by (simp add: atomize_eq) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
156 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
157 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
158 |
subsection {* Standard elements *} |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
159 |
|
19765 | 160 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
161 |
star_of :: "'a \<Rightarrow> 'a star" where |
19765 | 162 |
"star_of x == star_n (\<lambda>n. x)" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
163 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
164 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
165 |
Standard :: "'a star set" where |
20719 | 166 |
"Standard = range star_of" |
167 |
||
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
168 |
text {* Transfer tactic should remove occurrences of @{term star_of} *} |
18708 | 169 |
setup {* Transfer.add_const "StarDef.star_of" *} |
20719 | 170 |
|
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
171 |
declare star_of_def [transfer_intro] |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
172 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
173 |
lemma star_of_inject: "(star_of x = star_of y) = (x = y)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
174 |
by (transfer, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
175 |
|
20719 | 176 |
lemma Standard_star_of [simp]: "star_of x \<in> Standard" |
177 |
by (simp add: Standard_def) |
|
178 |
||
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
179 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
180 |
subsection {* Internal functions *} |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
181 |
|
19765 | 182 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
183 |
Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300) where |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
184 |
"Ifun f \<equiv> \<lambda>x. Abs_star |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
185 |
(\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
186 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
187 |
lemma Ifun_congruent2: |
19980
dc17fd6c0908
replaced respects2 by congruent2 because of type problem
nipkow
parents:
19765
diff
changeset
|
188 |
"congruent2 starrel starrel (\<lambda>F X. starrel``{\<lambda>n. F n (X n)})" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
189 |
by (auto simp add: congruent2_def equiv_starrel_iff elim!: ultra) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
190 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
191 |
lemma Ifun_star_n: "star_n F \<star> star_n X = star_n (\<lambda>n. F n (X n))" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
192 |
by (simp add: Ifun_def star_n_def Abs_star_inverse starrel_in_star |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
193 |
UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2]) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
194 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
195 |
text {* Transfer tactic should remove occurrences of @{term Ifun} *} |
18708 | 196 |
setup {* Transfer.add_const "StarDef.Ifun" *} |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
197 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
198 |
lemma transfer_Ifun [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
199 |
"\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
200 |
by (simp only: Ifun_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
201 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
202 |
lemma Ifun_star_of [simp]: "star_of f \<star> star_of x = star_of (f x)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
203 |
by (transfer, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
204 |
|
20719 | 205 |
lemma Standard_Ifun [simp]: |
206 |
"\<lbrakk>f \<in> Standard; x \<in> Standard\<rbrakk> \<Longrightarrow> f \<star> x \<in> Standard" |
|
207 |
by (auto simp add: Standard_def) |
|
208 |
||
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
209 |
text {* Nonstandard extensions of functions *} |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
210 |
|
19765 | 211 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
212 |
starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a star \<Rightarrow> 'b star)" ("*f* _" [80] 80) where |
19765 | 213 |
"starfun f == \<lambda>x. star_of f \<star> x" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
214 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
215 |
definition |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
216 |
starfun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)" |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
217 |
("*f2* _" [80] 80) where |
19765 | 218 |
"starfun2 f == \<lambda>x y. star_of f \<star> x \<star> y" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
219 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
220 |
declare starfun_def [transfer_unfold] |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
221 |
declare starfun2_def [transfer_unfold] |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
222 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
223 |
lemma starfun_star_n: "( *f* f) (star_n X) = star_n (\<lambda>n. f (X n))" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
224 |
by (simp only: starfun_def star_of_def Ifun_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
225 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
226 |
lemma starfun2_star_n: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
227 |
"( *f2* f) (star_n X) (star_n Y) = star_n (\<lambda>n. f (X n) (Y n))" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
228 |
by (simp only: starfun2_def star_of_def Ifun_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
229 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
230 |
lemma starfun_star_of [simp]: "( *f* f) (star_of x) = star_of (f x)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
231 |
by (transfer, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
232 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
233 |
lemma starfun2_star_of [simp]: "( *f2* f) (star_of x) = *f* f x" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
234 |
by (transfer, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
235 |
|
20719 | 236 |
lemma Standard_starfun [simp]: "x \<in> Standard \<Longrightarrow> starfun f x \<in> Standard" |
237 |
by (simp add: starfun_def) |
|
238 |
||
239 |
lemma Standard_starfun2 [simp]: |
|
240 |
"\<lbrakk>x \<in> Standard; y \<in> Standard\<rbrakk> \<Longrightarrow> starfun2 f x y \<in> Standard" |
|
241 |
by (simp add: starfun2_def) |
|
242 |
||
21887 | 243 |
lemma Standard_starfun_iff: |
244 |
assumes inj: "\<And>x y. f x = f y \<Longrightarrow> x = y" |
|
245 |
shows "(starfun f x \<in> Standard) = (x \<in> Standard)" |
|
246 |
proof |
|
247 |
assume "x \<in> Standard" |
|
248 |
thus "starfun f x \<in> Standard" by simp |
|
249 |
next |
|
250 |
have inj': "\<And>x y. starfun f x = starfun f y \<Longrightarrow> x = y" |
|
251 |
using inj by transfer |
|
252 |
assume "starfun f x \<in> Standard" |
|
253 |
then obtain b where b: "starfun f x = star_of b" |
|
254 |
unfolding Standard_def .. |
|
255 |
hence "\<exists>x. starfun f x = star_of b" .. |
|
256 |
hence "\<exists>a. f a = b" by transfer |
|
257 |
then obtain a where "f a = b" .. |
|
258 |
hence "starfun f (star_of a) = star_of b" by transfer |
|
259 |
with b have "starfun f x = starfun f (star_of a)" by simp |
|
260 |
hence "x = star_of a" by (rule inj') |
|
261 |
thus "x \<in> Standard" |
|
262 |
unfolding Standard_def by auto |
|
263 |
qed |
|
264 |
||
265 |
lemma Standard_starfun2_iff: |
|
266 |
assumes inj: "\<And>a b a' b'. f a b = f a' b' \<Longrightarrow> a = a' \<and> b = b'" |
|
267 |
shows "(starfun2 f x y \<in> Standard) = (x \<in> Standard \<and> y \<in> Standard)" |
|
268 |
proof |
|
269 |
assume "x \<in> Standard \<and> y \<in> Standard" |
|
270 |
thus "starfun2 f x y \<in> Standard" by simp |
|
271 |
next |
|
272 |
have inj': "\<And>x y z w. starfun2 f x y = starfun2 f z w \<Longrightarrow> x = z \<and> y = w" |
|
273 |
using inj by transfer |
|
274 |
assume "starfun2 f x y \<in> Standard" |
|
275 |
then obtain c where c: "starfun2 f x y = star_of c" |
|
276 |
unfolding Standard_def .. |
|
277 |
hence "\<exists>x y. starfun2 f x y = star_of c" by auto |
|
278 |
hence "\<exists>a b. f a b = c" by transfer |
|
279 |
then obtain a b where "f a b = c" by auto |
|
280 |
hence "starfun2 f (star_of a) (star_of b) = star_of c" |
|
281 |
by transfer |
|
282 |
with c have "starfun2 f x y = starfun2 f (star_of a) (star_of b)" |
|
283 |
by simp |
|
284 |
hence "x = star_of a \<and> y = star_of b" |
|
285 |
by (rule inj') |
|
286 |
thus "x \<in> Standard \<and> y \<in> Standard" |
|
287 |
unfolding Standard_def by auto |
|
288 |
qed |
|
289 |
||
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
290 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
291 |
subsection {* Internal predicates *} |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
292 |
|
19765 | 293 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
294 |
unstar :: "bool star \<Rightarrow> bool" where |
19765 | 295 |
"unstar b = (b = star_of True)" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
296 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
297 |
lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
298 |
by (simp add: unstar_def star_of_def star_n_eq_iff) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
299 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
300 |
lemma unstar_star_of [simp]: "unstar (star_of p) = p" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
301 |
by (simp add: unstar_def star_of_inject) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
302 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
303 |
text {* Transfer tactic should remove occurrences of @{term unstar} *} |
18708 | 304 |
setup {* Transfer.add_const "StarDef.unstar" *} |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
305 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
306 |
lemma transfer_unstar [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
307 |
"p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
308 |
by (simp only: unstar_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
309 |
|
19765 | 310 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
311 |
starP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> bool" ("*p* _" [80] 80) where |
19765 | 312 |
"*p* P = (\<lambda>x. unstar (star_of P \<star> x))" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
313 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
314 |
definition |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
315 |
starP2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> bool" ("*p2* _" [80] 80) where |
19765 | 316 |
"*p2* P = (\<lambda>x y. unstar (star_of P \<star> x \<star> y))" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
317 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
318 |
declare starP_def [transfer_unfold] |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
319 |
declare starP2_def [transfer_unfold] |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
320 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
321 |
lemma starP_star_n: "( *p* P) (star_n X) = ({n. P (X n)} \<in> \<U>)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
322 |
by (simp only: starP_def star_of_def Ifun_star_n unstar_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
323 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
324 |
lemma starP2_star_n: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
325 |
"( *p2* P) (star_n X) (star_n Y) = ({n. P (X n) (Y n)} \<in> \<U>)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
326 |
by (simp only: starP2_def star_of_def Ifun_star_n unstar_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
327 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
328 |
lemma starP_star_of [simp]: "( *p* P) (star_of x) = P x" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
329 |
by (transfer, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
330 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
331 |
lemma starP2_star_of [simp]: "( *p2* P) (star_of x) = *p* P x" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
332 |
by (transfer, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
333 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
334 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
335 |
subsection {* Internal sets *} |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
336 |
|
19765 | 337 |
definition |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
338 |
Iset :: "'a set star \<Rightarrow> 'a star set" where |
19765 | 339 |
"Iset A = {x. ( *p2* op \<in>) x A}" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
340 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
341 |
lemma Iset_star_n: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
342 |
"(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
343 |
by (simp add: Iset_def starP2_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
344 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
345 |
text {* Transfer tactic should remove occurrences of @{term Iset} *} |
18708 | 346 |
setup {* Transfer.add_const "StarDef.Iset" *} |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
347 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
348 |
lemma transfer_mem [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
349 |
"\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk> |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
350 |
\<Longrightarrow> x \<in> a \<equiv> {n. X n \<in> A n} \<in> \<U>" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
351 |
by (simp only: Iset_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
352 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
353 |
lemma transfer_Collect [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
354 |
"\<lbrakk>\<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk> |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
355 |
\<Longrightarrow> Collect p \<equiv> Iset (star_n (\<lambda>n. Collect (P n)))" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
356 |
by (simp add: atomize_eq expand_set_eq all_star_eq Iset_star_n) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
357 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
358 |
lemma transfer_set_eq [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
359 |
"\<lbrakk>a \<equiv> Iset (star_n A); b \<equiv> Iset (star_n B)\<rbrakk> |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
360 |
\<Longrightarrow> a = b \<equiv> {n. A n = B n} \<in> \<U>" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
361 |
by (simp only: expand_set_eq transfer_all transfer_iff transfer_mem) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
362 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
363 |
lemma transfer_ball [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
364 |
"\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk> |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
365 |
\<Longrightarrow> \<forall>x\<in>a. p x \<equiv> {n. \<forall>x\<in>A n. P n x} \<in> \<U>" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
366 |
by (simp only: Ball_def transfer_all transfer_imp transfer_mem) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
367 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
368 |
lemma transfer_bex [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
369 |
"\<lbrakk>a \<equiv> Iset (star_n A); \<And>X. p (star_n X) \<equiv> {n. P n (X n)} \<in> \<U>\<rbrakk> |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
370 |
\<Longrightarrow> \<exists>x\<in>a. p x \<equiv> {n. \<exists>x\<in>A n. P n x} \<in> \<U>" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
371 |
by (simp only: Bex_def transfer_ex transfer_conj transfer_mem) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
372 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
373 |
lemma transfer_Iset [transfer_intro]: |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
374 |
"\<lbrakk>a \<equiv> star_n A\<rbrakk> \<Longrightarrow> Iset a \<equiv> Iset (star_n (\<lambda>n. A n))" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
375 |
by simp |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
376 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
377 |
text {* Nonstandard extensions of sets. *} |
19765 | 378 |
|
379 |
definition |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20719
diff
changeset
|
380 |
starset :: "'a set \<Rightarrow> 'a star set" ("*s* _" [80] 80) where |
19765 | 381 |
"starset A = Iset (star_of A)" |
17429
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
382 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
383 |
declare starset_def [transfer_unfold] |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
384 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
385 |
lemma starset_mem: "(star_of x \<in> *s* A) = (x \<in> A)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
386 |
by (transfer, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
387 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
388 |
lemma starset_UNIV: "*s* (UNIV::'a set) = (UNIV::'a star set)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
389 |
by (transfer UNIV_def, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
390 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
391 |
lemma starset_empty: "*s* {} = {}" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
392 |
by (transfer empty_def, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
393 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
394 |
lemma starset_insert: "*s* (insert x A) = insert (star_of x) ( *s* A)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
395 |
by (transfer insert_def Un_def, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
396 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
397 |
lemma starset_Un: "*s* (A \<union> B) = *s* A \<union> *s* B" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
398 |
by (transfer Un_def, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
399 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
400 |
lemma starset_Int: "*s* (A \<inter> B) = *s* A \<inter> *s* B" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
401 |
by (transfer Int_def, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
402 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
403 |
lemma starset_Compl: "*s* -A = -( *s* A)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
404 |
by (transfer Compl_def, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
405 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
406 |
lemma starset_diff: "*s* (A - B) = *s* A - *s* B" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
407 |
by (transfer set_diff_def, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
408 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
409 |
lemma starset_image: "*s* (f ` A) = ( *f* f) ` ( *s* A)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
410 |
by (transfer image_def, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
411 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
412 |
lemma starset_vimage: "*s* (f -` A) = ( *f* f) -` ( *s* A)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
413 |
by (transfer vimage_def, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
414 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
415 |
lemma starset_subset: "( *s* A \<subseteq> *s* B) = (A \<subseteq> B)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
416 |
by (transfer subset_def, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
417 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
418 |
lemma starset_eq: "( *s* A = *s* B) = (A = B)" |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
419 |
by (transfer, rule refl) |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
420 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
421 |
lemmas starset_simps [simp] = |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
422 |
starset_mem starset_UNIV |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
423 |
starset_empty starset_insert |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
424 |
starset_Un starset_Int |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
425 |
starset_Compl starset_diff |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
426 |
starset_image starset_vimage |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
427 |
starset_subset starset_eq |
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
428 |
|
e8d6ed3aacfe
merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
huffman
parents:
diff
changeset
|
429 |
end |