Quot/QuotList.thy
changeset 922 a2589b4bc442
parent 913 b1f55dd64481
child 924 5455b19ef138
equal deleted inserted replaced
921:dae038c8cd69 922:a2589b4bc442
   159 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *)
   159 (* induct_tac doesn't accept 'arbitrary', so we manually 'spec' *)
   160 lemma foldl_rsp[quot_respect]:
   160 lemma foldl_rsp[quot_respect]:
   161   assumes q1: "Quotient R1 Abs1 Rep1"
   161   assumes q1: "Quotient R1 Abs1 Rep1"
   162   and     q2: "Quotient R2 Abs2 Rep2"
   162   and     q2: "Quotient R2 Abs2 Rep2"
   163   shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"
   163   shows "((R1 ===> R2 ===> R1) ===> R1 ===> list_rel R2 ===> R1) foldl foldl"
   164 apply auto
   164 apply(auto)
   165 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)")
   165 apply (subgoal_tac "R1 xa ya \<longrightarrow> list_rel R2 xb yb \<longrightarrow> R1 (foldl x xa xb) (foldl y ya yb)")
   166 apply simp
   166 apply simp
   167 apply (rule_tac x="xa" in spec)
   167 apply (rule_tac x="xa" in spec)
   168 apply (rule_tac x="ya" in spec)
   168 apply (rule_tac x="ya" in spec)
   169 apply (rule_tac xs="xb" and ys="yb" in list_induct2)
   169 apply (rule_tac xs="xb" and ys="yb" in list_induct2)
   190 apply(rule allI)+
   190 apply(rule allI)+
   191 apply(induct_tac x xa rule: list_induct2')
   191 apply(induct_tac x xa rule: list_induct2')
   192 apply(simp_all)
   192 apply(simp_all)
   193 done
   193 done
   194 
   194 
       
   195 
   195 (* Rest are unused *)
   196 (* Rest are unused *)
   196 
   197 text {*
   197 lemma list_rel_refl:
   198 lemma list_rel_refl:
   198   assumes a: "\<And>x y. R x y = (R x = R y)"
   199   assumes a: "\<And>x y. R x y = (R x = R y)"
   199   shows "list_rel R x x"
   200   shows "list_rel R x x"
   200 by (induct x) (auto simp add: a)
   201 by (induct x) (auto simp add: a)
       
   202 *}
   201 
   203 
   202 end
   204 end