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+)