src/HOL/ZF/LProd.thy

 (*  Title:      HOL/ZF/LProd.thy
-    ID:         $Id$
     Author:     Steven Obua
 
     Introduces the lprod relation.
     See "Partizan Games in Isabelle/HOLZF", available from http://www4.in.tum.de/~obua/partizan
 *)

     OF wf_mult[OF wf_trancl[OF wf_R]]], OF subset]
   note lprod = wf_subset[OF lprodtrancl, where p="lprod R", OF lprod_subset, simplified]
   show ?thesis by (auto intro: lprod)
 qed
 
-constdefs
-  gprod_2_2 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set"
+definition gprod_2_2 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set" where
   "gprod_2_2 R \<equiv> { ((a,b), (c,d)) . (a = c \<and> (b,d) \<in> R) \<or> (b = d \<and> (a,c) \<in> R) }"
-  gprod_2_1 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set"
+
+definition gprod_2_1 :: "('a * 'a) set \<Rightarrow> (('a * 'a) * ('a * 'a)) set" where
   "gprod_2_1 R \<equiv>  { ((a,b), (c,d)) . (a = d \<and> (b,c) \<in> R) \<or> (b = c \<and> (a,d) \<in> R) }"
 
 lemma lprod_2_3: "(a, b) \<in> R \<Longrightarrow> ([a, c], [b, c]) \<in> lprod R"
   by (auto intro: lprod_list[where a=c and b=c and 
     ah = "[a]" and at = "[]" and bh="[b]" and bt="[]", simplified]) 

 lemma lprod_3_7: assumes z': "(z',z) \<in> R" shows "([x, z', y], [x, y, z]) \<in> lprod R"
   apply (rule lprod_list[where a="y" and b="y" and ah="[x, z']" and at="[]" and bh="[x]" and bt="[z]", simplified])
   apply (simp add: z' lprod_2_4)
   done
 
-constdefs
-   perm :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> bool"
+definition perm :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> bool" where
    "perm f A \<equiv> inj_on f A \<and> f ` A = A"
 
 lemma "((as,bs) \<in> lprod R) = 
   (\<exists> f. perm f {0 ..< (length as)} \<and> 
   (\<forall> j. j < length as \<longrightarrow> ((nth as j, nth bs (f j)) \<in> R \<or> (nth as j = nth bs (f j)))) \<and> 

 oops
 
 lemma "trans R \<Longrightarrow> (ah@a#at, bh@b#bt) \<in> lprod R \<Longrightarrow> (b, a) \<in> R \<or> a = b \<Longrightarrow> (ah@at, bh@bt) \<in> lprod R" 
 oops
 
-
-
 end