equal
deleted
inserted
replaced
99 by (simp add: same_fst_def) |
99 by (simp add: same_fst_def) |
100 |
100 |
101 lemma wf_same_fst: |
101 lemma wf_same_fst: |
102 assumes "\<And>x. P x \<Longrightarrow> wf (R x)" |
102 assumes "\<And>x. P x \<Longrightarrow> wf (R x)" |
103 shows "wf (same_fst P R)" |
103 shows "wf (same_fst P R)" |
104 proof (clarsimp simp add: wf_def same_fst_def) |
104 proof - |
105 fix Q a b |
105 have "\<And>a b Q. \<forall>a b. (\<forall>x. P a \<and> (x, b) \<in> R a \<longrightarrow> Q (a, x)) \<longrightarrow> Q (a, b) \<Longrightarrow> Q (a, b)" |
106 assume *: "\<forall>a b. (\<forall>x. P a \<and> (x,b) \<in> R a \<longrightarrow> Q (a,x)) \<longrightarrow> Q (a,b)" |
106 proof - |
107 show "Q(a,b)" |
107 fix Q a b |
108 proof (cases "wf (R a)") |
108 assume *: "\<forall>a b. (\<forall>x. P a \<and> (x,b) \<in> R a \<longrightarrow> Q (a,x)) \<longrightarrow> Q (a,b)" |
109 case True |
109 show "Q(a,b)" |
110 then show ?thesis |
110 proof (cases "wf (R a)") |
111 by (induction b rule: wf_induct_rule) (use * in blast) |
111 case True |
112 qed (use * assms in blast) |
112 then show ?thesis |
|
113 by (induction b rule: wf_induct_rule) (use * in blast) |
|
114 qed (use * assms in blast) |
|
115 qed |
|
116 then show ?thesis |
|
117 by (clarsimp simp add: wf_def same_fst_def) |
113 qed |
118 qed |
114 |
119 |
115 end |
120 end |