src/HOL/BNF_Wellorder_Constructions.thy
 changeset 61943 7fba644ed827 parent 61799 4cf66f21b764 child 63040 eb4ddd18d635
```     1.1 --- a/src/HOL/BNF_Wellorder_Constructions.thy	Sun Dec 27 21:46:36 2015 +0100
1.2 +++ b/src/HOL/BNF_Wellorder_Constructions.thy	Sun Dec 27 22:07:17 2015 +0100
1.3 @@ -1515,19 +1515,19 @@
1.4  "curr A f \<equiv> \<lambda> a. if a \<in> A then \<lambda>b. f (a,b) else undefined"
1.5
1.6  lemma curr_in:
1.7 -assumes f: "f \<in> Func (A <*> B) C"
1.8 +assumes f: "f \<in> Func (A \<times> B) C"
1.9  shows "curr A f \<in> Func A (Func B C)"
1.10  using assms unfolding curr_def Func_def by auto
1.11
1.12  lemma curr_inj:
1.13 -assumes "f1 \<in> Func (A <*> B) C" and "f2 \<in> Func (A <*> B) C"
1.14 +assumes "f1 \<in> Func (A \<times> B) C" and "f2 \<in> Func (A \<times> B) C"
1.15  shows "curr A f1 = curr A f2 \<longleftrightarrow> f1 = f2"
1.16  proof safe
1.17    assume c: "curr A f1 = curr A f2"
1.18    show "f1 = f2"
1.19    proof (rule ext, clarify)
1.20      fix a b show "f1 (a, b) = f2 (a, b)"
1.21 -    proof (cases "(a,b) \<in> A <*> B")
1.22 +    proof (cases "(a,b) \<in> A \<times> B")
1.23        case False
1.24        thus ?thesis using assms unfolding Func_def by auto
1.25      next
1.26 @@ -1540,7 +1540,7 @@
1.27
1.28  lemma curr_surj:
1.29  assumes "g \<in> Func A (Func B C)"
1.30 -shows "\<exists> f \<in> Func (A <*> B) C. curr A f = g"
1.31 +shows "\<exists> f \<in> Func (A \<times> B) C. curr A f = g"
1.32  proof
1.33    let ?f = "\<lambda> ab. if fst ab \<in> A \<and> snd ab \<in> B then g (fst ab) (snd ab) else undefined"
1.34    show "curr A ?f = g"
1.35 @@ -1557,11 +1557,11 @@
1.36        thus ?thesis using True unfolding Func_def curr_def by auto
1.37      qed
1.38    qed
1.39 -  show "?f \<in> Func (A <*> B) C" using assms unfolding Func_def mem_Collect_eq by auto
1.40 +  show "?f \<in> Func (A \<times> B) C" using assms unfolding Func_def mem_Collect_eq by auto
1.41  qed
1.42
1.43  lemma bij_betw_curr:
1.44 -"bij_betw (curr A) (Func (A <*> B) C) (Func A (Func B C))"
1.45 +"bij_betw (curr A) (Func (A \<times> B) C) (Func A (Func B C))"
1.46  unfolding bij_betw_def inj_on_def image_def
1.47  apply (intro impI conjI ballI)
1.48  apply (erule curr_inj[THEN iffD1], assumption+)
```