# HG changeset patch
# User berghofe
# Date 1170868221 -3600
# Node ID 71b4aefad2274c58e9af903da0848fc484cd13a8
# Parent  23e0fde84cb705cc99f7870bf2ef366c0fba622f
- Adapted to new inductive definition package
- Adapted to changes in Multiset theory

diff -r 23e0fde84cb7 -r 71b4aefad227 src/HOL/ZF/Games.thy
--- a/src/HOL/ZF/Games.thy	Wed Feb 07 18:07:10 2007 +0100
+++ b/src/HOL/ZF/Games.thy	Wed Feb 07 18:10:21 2007 +0100
@@ -366,7 +366,7 @@
 consts
   ge_game :: "(game * game) \<Rightarrow> bool" 
 
-recdef ge_game "(gprod_2_1 option_of)"
+recdef ge_game "Collect2 (gprod_2_1 (member2 option_of))"
   "ge_game (G, H) = (\<forall> x. if zin x (right_options G) then (
                           if zin x (left_options H) then \<not> (ge_game (H, x) \<or> (ge_game (x, G))) 
                                                     else \<not> (ge_game (H, x)))
@@ -448,8 +448,8 @@
 lemma eq_game_refl: "eq_game G G"
   by (simp add: ge_game_refl eq_game_def)
 
-lemma induct_game: "(\<And>x. \<forall>y. (y, x) \<in> lprod option_of \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
-  by (erule wf_induct[OF wf_lprod[OF wf_option_of]])
+lemma induct_game: "(\<And>x. \<forall>y. lprod (member2 option_of) y x \<longrightarrow> P y \<Longrightarrow> P x) \<Longrightarrow> P a"
+  by (erule wfP_induct[OF wf_lprod[to_set, OF wf_option_of]])
 
 lemma ge_game_trans:
   assumes "ge_game (x, y)" "ge_game (y, z)" 
@@ -509,7 +509,7 @@
 consts 
   plus_game :: "game * game \<Rightarrow> game"
 
-recdef plus_game "gprod_2_2 option_of"
+recdef plus_game "Collect2 (gprod_2_2 (member2 option_of))"
   "plus_game (G, H) = Game (zunion (zimage (\<lambda> g. plus_game (g, H)) (left_options G))
                                    (zimage (\<lambda> h. plus_game (G, h)) (left_options H)))
                            (zunion (zimage (\<lambda> g. plus_game (g, H)) (right_options G))
diff -r 23e0fde84cb7 -r 71b4aefad227 src/HOL/ZF/LProd.thy
--- a/src/HOL/ZF/LProd.thy	Wed Feb 07 18:07:10 2007 +0100
+++ b/src/HOL/ZF/LProd.thy	Wed Feb 07 18:10:21 2007 +0100
@@ -10,58 +10,57 @@
 imports Multiset
 begin
 
-consts
-  lprod :: "('a * 'a) set \<Rightarrow> ('a list * 'a list) set"
+inductive2
+  lprod :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
+  for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  lprod_single[intro!]: "R a b \<Longrightarrow> lprod R [a] [b]"
+| lprod_list[intro!]: "lprod R (ah@at) (bh@bt) \<Longrightarrow> R a b \<or> a = b \<Longrightarrow> lprod R (ah@a#at) (bh@b#bt)"
 
-inductive "lprod R"
-intros
-  lprod_single[intro!]: "(a, b) \<in> R \<Longrightarrow> ([a], [b]) \<in> lprod R"
-  lprod_list[intro!]: "(ah@at, bh@bt) \<in> lprod R \<Longrightarrow> (a,b) \<in> R \<or> a = b \<Longrightarrow> (ah@a#at, bh@b#bt) \<in> lprod R"
-
-lemma "(as,bs) \<in> lprod R \<Longrightarrow> length as = length bs"
+lemma "lprod R as bs \<Longrightarrow> length as = length bs"
   apply (induct as bs rule: lprod.induct)
   apply auto
   done
 
-lemma "(as, bs) \<in> lprod R \<Longrightarrow> 1 \<le> length as \<and> 1 \<le> length bs"
+lemma "lprod R as bs \<Longrightarrow> 1 \<le> length as \<and> 1 \<le> length bs"
   apply (induct as bs rule: lprod.induct)
   apply auto
   done
 
-lemma lprod_subset_elem: "(as, bs) \<in> lprod S \<Longrightarrow> S \<subseteq> R \<Longrightarrow> (as, bs) \<in> lprod R"
+lemma lprod_subset_elem: "lprod S as bs \<Longrightarrow> S \<le> R \<Longrightarrow> lprod R as bs"
   apply (induct as bs rule: lprod.induct)
   apply (auto)
   done
 
-lemma lprod_subset: "S \<subseteq> R \<Longrightarrow> lprod S \<subseteq> lprod R"
+lemma lprod_subset: "S \<le> R \<Longrightarrow> lprod S \<le> lprod R"
   by (auto intro: lprod_subset_elem)
 
-lemma lprod_implies_mult: "(as, bs) \<in> lprod R \<Longrightarrow> trans R \<Longrightarrow> (multiset_of as, multiset_of bs) \<in> mult R"
+lemma lprod_implies_mult: "lprod R as bs \<Longrightarrow> transP R \<Longrightarrow> mult R (multiset_of as) (multiset_of bs)"
 proof (induct as bs rule: lprod.induct)
   case (lprod_single a b)
   note step = one_step_implies_mult[
     where r=R and I="{#}" and K="{#a#}" and J="{#b#}", simplified]    
   show ?case by (auto intro: lprod_single step)
 next
-  case (lprod_list a ah at b bh bt) 
-  from prems have transR: "trans R" by auto
+  case (lprod_list ah at bh bt a b) 
+  from prems have transR: "transP R" by auto
   have as: "multiset_of (ah @ a # at) = multiset_of (ah @ at) + {#a#}" (is "_ = ?ma + _")
     by (simp add: ring_eq_simps)
   have bs: "multiset_of (bh @ b # bt) = multiset_of (bh @ bt) + {#b#}" (is "_ = ?mb + _")
     by (simp add: ring_eq_simps)
-  from prems have "(?ma, ?mb) \<in> mult R"
+  from prems have "mult R ?ma ?mb"
     by auto
   with mult_implies_one_step[OF transR] have 
-    "\<exists>I J K. ?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> R)"
+    "\<exists>I J K. ?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. R k j)"
     by blast
   then obtain I J K where 
-    decomposed: "?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. (k, j) \<in> R)"
+    decomposed: "?mb = I + J \<and> ?ma = I + K \<and> J \<noteq> {#} \<and> (\<forall>k\<in>set_of K. \<exists>j\<in>set_of J. R k j)"
     by blast   
   show ?case
   proof (cases "a = b")
     case True    
-    have "((I + {#b#}) + K, (I + {#b#}) + J) \<in> mult R"
-      apply (rule one_step_implies_mult[OF transR])
+    have "mult R ((I + {#b#}) + K) ((I + {#b#}) + J)"
+      apply (rule one_step_implies_mult)
       apply (auto simp add: decomposed)
       done
     then show ?thesis
@@ -71,9 +70,9 @@
       done
   next
     case False
-    from False lprod_list have False: "(a, b) \<in> R" by blast
-    have "(I + (K + {#a#}), I + (J + {#b#})) \<in> mult R"
-      apply (rule one_step_implies_mult[OF transR])
+    from False lprod_list have False: "R a b" by blast
+    have "mult R (I + (K + {#a#})) (I + (J + {#b#}))"
+      apply (rule one_step_implies_mult)
       apply (auto simp add: False decomposed)
       done
     then show ?thesis
@@ -85,88 +84,88 @@
 qed
 
 lemma wf_lprod[recdef_wf,simp,intro]:
-  assumes wf_R: "wf R"
-  shows "wf (lprod R)"
+  assumes wf_R: "wfP R"
+  shows "wfP (lprod R)"
 proof -
-  have subset: "lprod (R^+) \<subseteq> inv_image (mult (R^+)) multiset_of"
-    by (auto simp add: lprod_implies_mult trans_trancl)
-  note lprodtrancl = wf_subset[OF wf_inv_image[where r="mult (R^+)" and f="multiset_of", 
-    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]
+  have subset: "lprod (R^++) \<le> inv_imagep (mult (R^++)) multiset_of"
+    by (auto simp add: lprod_implies_mult trans_trancl[to_pred])
+  note lprodtrancl = wfP_subset[OF wf_inv_image[to_pred, where r="mult (R^++)" and f="multiset_of", 
+    OF wf_mult[OF wfP_trancl[OF wf_R]]], OF subset]
+  note lprod = wfP_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"
-  "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"
-  "gprod_2_1 R \<equiv>  { ((a,b), (c,d)) . (a = d \<and> (b,c) \<in> R) \<or> (b = c \<and> (a,d) \<in> R) }"
+  gprod_2_2 :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a * 'a) \<Rightarrow> ('a * 'a) \<Rightarrow> bool"
+  "gprod_2_2 R \<equiv> \<lambda>(a,b) (c,d). (a = c \<and> R b d) \<or> (b = d \<and> R a c)"
+  gprod_2_1 :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a * 'a) \<Rightarrow> ('a * 'a) \<Rightarrow> bool"
+  "gprod_2_1 R \<equiv> \<lambda>(a,b) (c,d). (a = d \<and> R b c) \<or> (b = c \<and> R a d)"
 
-lemma lprod_2_3: "(a, b) \<in> R \<Longrightarrow> ([a, c], [b, c]) \<in> lprod R"
+lemma lprod_2_3: "R a b \<Longrightarrow> lprod R [a, c] [b, c]"
   by (auto intro: lprod_list[where a=c and b=c and 
     ah = "[a]" and at = "[]" and bh="[b]" and bt="[]", simplified]) 
 
-lemma lprod_2_4: "(a, b) \<in> R \<Longrightarrow> ([c, a], [c, b]) \<in> lprod R"
+lemma lprod_2_4: "R a b \<Longrightarrow> lprod R [c, a] [c, b]"
   by (auto intro: lprod_list[where a=c and b=c and 
     ah = "[]" and at = "[a]" and bh="[]" and bt="[b]", simplified])
 
-lemma lprod_2_1: "(a, b) \<in> R \<Longrightarrow> ([c, a], [b, c]) \<in> lprod R"
+lemma lprod_2_1: "R a b \<Longrightarrow> lprod R [c, a] [b, c]"
   by (auto intro: lprod_list[where a=c and b=c and 
     ah = "[]" and at = "[a]" and bh="[b]" and bt="[]", simplified]) 
 
-lemma lprod_2_2: "(a, b) \<in> R \<Longrightarrow> ([a, c], [c, b]) \<in> lprod R"
+lemma lprod_2_2: "R a b \<Longrightarrow> lprod R [a, c] [c, b]"
   by (auto intro: lprod_list[where a=c and b=c and 
     ah = "[a]" and at = "[]" and bh="[]" and bt="[b]", simplified])
 
 lemma [recdef_wf, simp, intro]: 
-  assumes wfR: "wf R" shows "wf (gprod_2_1 R)"
+  assumes wfR: "wfP R" shows "wfP (gprod_2_1 R)"
 proof -
-  have "gprod_2_1 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
+  have "gprod_2_1 R \<le> inv_imagep (lprod R) (\<lambda> (a,b). [a,b])"
     by (auto simp add: gprod_2_1_def lprod_2_1 lprod_2_2)
   with wfR show ?thesis
-    by (rule_tac wf_subset, auto)
+    by (rule_tac wfP_subset, auto intro!: wf_inv_image[to_pred])
 qed
 
 lemma [recdef_wf, simp, intro]: 
-  assumes wfR: "wf R" shows "wf (gprod_2_2 R)"
+  assumes wfR: "wfP R" shows "wfP (gprod_2_2 R)"
 proof -
-  have "gprod_2_2 R \<subseteq> inv_image (lprod R) (\<lambda> (a,b). [a,b])"
+  have "gprod_2_2 R \<le> inv_imagep (lprod R) (\<lambda> (a,b). [a,b])"
     by (auto simp add: gprod_2_2_def lprod_2_3 lprod_2_4)
   with wfR show ?thesis
-    by (rule_tac wf_subset, auto)
+    by (rule_tac wfP_subset, auto intro!: wf_inv_image[to_pred])
 qed
 
-lemma lprod_3_1: assumes "(x', x) \<in> R" shows "([y, z, x'], [x, y, z]) \<in> lprod R"
+lemma lprod_3_1: assumes "R x' x" shows "lprod R [y, z, x'] [x, y, z]"
   apply (rule lprod_list[where a="y" and b="y" and ah="[]" and at="[z,x']" and bh="[x]" and bt="[z]", simplified])
   apply (auto simp add: lprod_2_1 prems)
   done
 
-lemma lprod_3_2: assumes "(z',z) \<in> R" shows "([z', x, y], [x,y,z]) \<in> lprod R"
+lemma lprod_3_2: assumes "R z' z" shows "lprod R [z', x, y] [x,y,z]"
   apply (rule lprod_list[where a="y" and b="y" and ah="[z',x]" and at="[]" and bh="[x]" and bt="[z]", simplified])
   apply (auto simp add: lprod_2_2 prems)
   done
 
-lemma lprod_3_3: assumes xr: "(xr, x) \<in> R" shows "([xr, y, z], [x, y, z]) \<in> lprod R"
+lemma lprod_3_3: assumes xr: "R xr x" shows "lprod R [xr, y, z] [x, y, z]"
   apply (rule lprod_list[where a="y" and b="y" and ah="[xr]" and at="[z]" and bh="[x]" and bt="[z]", simplified])
   apply (simp add: xr lprod_2_3)
   done
 
-lemma lprod_3_4: assumes yr: "(yr, y) \<in> R" shows "([x, yr, z], [x, y, z]) \<in> lprod R"
+lemma lprod_3_4: assumes yr: "R yr y" shows "lprod R [x, yr, z] [x, y, z]"
   apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[yr,z]" and bh="[]" and bt="[y,z]", simplified])
   apply (simp add: yr lprod_2_3)
   done
 
-lemma lprod_3_5: assumes zr: "(zr, z) \<in> R" shows "([x, y, zr], [x, y, z]) \<in> lprod R"
+lemma lprod_3_5: assumes zr: "R zr z" shows "lprod R [x, y, zr] [x, y, z]"
   apply (rule lprod_list[where a="x" and b="x" and ah="[]" and at="[y,zr]" and bh="[]" and bt="[y,z]", simplified])
   apply (simp add: zr lprod_2_4)
   done
 
-lemma lprod_3_6: assumes y': "(y', y) \<in> R" shows "([x, z, y'], [x, y, z]) \<in> lprod R"
+lemma lprod_3_6: assumes y': "R y' y" shows "lprod R [x, z, y'] [x, y, z]"
   apply (rule lprod_list[where a="z" and b="z" and ah="[x]" and at="[y']" and bh="[x,y]" and bt="[]", simplified])
   apply (simp add: y' lprod_2_4)
   done
 
-lemma lprod_3_7: assumes z': "(z',z) \<in> R" shows "([x, z', y], [x, y, z]) \<in> lprod R"
+lemma lprod_3_7: assumes z': "R z' z" shows "lprod R [x, z', y] [x, y, z]"
   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
@@ -175,13 +174,13 @@
    perm :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> bool"
    "perm f A \<equiv> inj_on f A \<and> f ` A = A"
 
-lemma "((as,bs) \<in> lprod R) = 
+lemma "lprod R as bs = 
   (\<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> 
-  (\<exists> i. i < length as \<and> (nth as i, nth bs (f i)) \<in> R))"
+  (\<forall> j. j < length as \<longrightarrow> (R (nth as j) (nth bs (f j)) \<or> (nth as j = nth bs (f j)))) \<and> 
+  (\<exists> i. i < length as \<and> R (nth as i) (nth bs (f i))))"
 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" 
+lemma "transP R \<Longrightarrow> lprod R (ah@a#at) (bh@b#bt) \<Longrightarrow> R b a \<or> a = b \<Longrightarrow> lprod R (ah@at) (bh@bt)" 
 oops