Quelle  Relations.thy

theory Relations imports Main begin

(*Id is only used in UNITY*)
(*refl, antisym,trans,univalent,\<dots> ho hum*)

text‹
 @{thm[display] Id_def[no_vars]}
 \rulename{Id_def}
 ›

text‹
 @{thm[display] relcomp_unfold[no_vars]}
 \rulename{relcomp_unfold}
 ›

text‹
 @{thm[display] R_O_Id[no_vars]}
 \rulename{R_O_Id}
 ›

text‹
 @{thm[display] relcomp_mono[no_vars]}
 \rulename{relcomp_mono}
 ›

text‹
 @{thm[display] converse_iff[no_vars]}
 \rulename{converse_iff}
 ›

text‹
 @{thm[display] converse_relcomp[no_vars]}
 \rulename{converse_relcomp}
 ›

text‹
 @{thm[display] Image_iff[no_vars]}
 \rulename{Image_iff}
 ›

text‹
 @{thm[display] Image_UN[no_vars]}
 \rulename{Image_UN}
 ›

text‹
 @{thm[display] Domain_iff[no_vars]}
 \rulename{Domain_iff}
 ›

text‹
 @{thm[display] Range_iff[no_vars]}
 \rulename{Range_iff}
 ›

text‹
 @{thm[display] relpow.simps[no_vars]}
 \rulename{relpow.simps}
 
 @{thm[display] rtrancl_refl[no_vars]}
 \rulename{rtrancl_refl}
 
 @{thm[display] r_into_rtrancl[no_vars]}
 \rulename{r_into_rtrancl}
 
 @{thm[display] rtrancl_trans[no_vars]}
 \rulename{rtrancl_trans}
 
 @{thm[display] rtrancl_induct[no_vars]}
 \rulename{rtrancl_induct}
 
 @{thm[display] rtrancl_idemp[no_vars]}
 \rulename{rtrancl_idemp}
 
 @{thm[display] r_into_trancl[no_vars]}
 \rulename{r_into_trancl}
 
 @{thm[display] trancl_trans[no_vars]}
 \rulename{trancl_trans}
 
 @{thm[display] trancl_into_rtrancl[no_vars]}
 \rulename{trancl_into_rtrancl}
 
 @{thm[display] trancl_converse[no_vars]}
 \rulename{trancl_converse}
 ›

text‹Relations. transitive closure›

lemma rtrancl_converseD: "(x,y) ∈ (r^-1)🪙* ==> (y,x) ∈ r🪙*"
apply (erule rtrancl_induct)
txt‹
 @{subgoals[display,indent=0,margin=65]}
 ›
 apply (rule rtrancl_refl)
apply (blast intro: rtrancl_trans)
done


lemma rtrancl_converseI: "(y,x) ∈ r🪙* ==> (x,y) ∈ (r^-1)🪙*"
apply (erule rtrancl_induct)
 apply (rule rtrancl_refl)
apply (blast intro: rtrancl_trans)
done

lemma rtrancl_converse: "(r^-1)🪙* = (r🪙*)^-1"
by (auto intro: rtrancl_converseI dest: rtrancl_converseD)

lemma rtrancl_converse: "(r^-1)🪙* = (r🪙*)^-1"
apply (intro equalityI subsetI)
txt‹
 after intro rules
 
 @{subgoals[display,indent=0,margin=65]}
 ›
apply clarify
txt‹
 after splitting
 @{subgoals[display,indent=0,margin=65]}
 ›
oops


lemma "(∀u v. (u,v) ∈ A ⟶ u=v) ==> A ⊆ Id"
apply (rule subsetI)
txt‹
 @{subgoals[display,indent=0,margin=65]}
 
 after subsetI
 ›
apply clarify
txt‹
 @{subgoals[display,indent=0,margin=65]}
 
 subgoals after clarify
 ›
by blast




text‹rejects›

lemma "(a ∈ {z. P z} ∪ {y. Q y}) = P a ∨ Q a"
apply (blast)
done

text‹Pow, Inter too little used›

lemma "(A ⊂ B) = (A ⊆ B ∧ A ≠ B)"
apply (simp add: psubset_eq)
done

end