theory simp_pair_singleton_switch_alphabet_dependent

imports Complex_Main
begin
typedecl sT
consts paS :: "sT => sT => sT"

syntax "_paS" :: "sT => sT => sT" ("(\<lbrace>(_,_)\<rbrace>)")
  translations
  "\<lbrace>r,s\<rbrace>" == "CONST paS r s"
    
theorem lrbrace_notation [simp]:
  "\<lbrace>\<lbrace>r,s\<rbrace>,\<lbrace>p,p\<rbrace>\<rbrace> = \<lbrace>\<lbrace>p,p\<rbrace>,\<lbrace>r,s\<rbrace>\<rbrace>"
  sorry
    
theorem "\<lbrace>\<lbrace>f,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
  apply simp
  --"Output: \<lbrace>\<lbrace>e,e\<rbrace>,\<lbrace>f,d\<rbrace>\<rbrace> = z"
  oops    
 
theorem "\<lbrace>\<lbrace>a,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
  apply simp
  oops
theorem "\<lbrace>\<lbrace>b,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
  apply simp
  oops
theorem "\<lbrace>\<lbrace>c,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
  apply simp
  oops
theorem "\<lbrace>\<lbrace>d,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
  apply simp
  oops
theorem "\<lbrace>\<lbrace>e,d\<rbrace>,\<lbrace>e,e\<rbrace>\<rbrace> = z"
  apply simp
  oops
  
theorem regular_braces [simp]:
  "{{r,s},{p}} = {{p},{r,s}}"  
  sorry
theorem "{{c,d},{e,e}} = z"
  apply simp
  --"Output: {{e}, {a, d}} = z"
  oops
end