src/HOL/Nominal/Examples/Lam_substs.thy
changeset 18758 e8a11e84864c
parent 18659 2ff0ae57431d
child 19166 fd8f152cfc76
equal deleted inserted replaced
18757:f0d901bc0686 18758:e8a11e84864c
   565   and   f2::"('a::pt_name) f2_ty"
   565   and   f2::"('a::pt_name) f2_ty"
   566   and   f3::"('a::pt_name) f3_ty"
   566   and   f3::"('a::pt_name) f3_ty"
   567   assumes f: "finite ((supp (f1,f2,f3))::name set)"
   567   assumes f: "finite ((supp (f1,f2,f3))::name set)"
   568   and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
   568   and     c: "\<exists>(a::name). a\<sharp>f3 \<and> (\<forall>(y::'a::pt_name). a\<sharp>f3 a y)"
   569   shows "\<exists>!y. (t,y)\<in>rec f1 f2 f3"
   569   shows "\<exists>!y. (t,y)\<in>rec f1 f2 f3"
   570 proof 
   570 proof (rule ex_ex1I)
   571   case goal1
   571   case goal1
   572   show ?case by (rule rec_total[OF f, OF c])
   572   show ?case by (rule rec_total[OF f, OF c])
   573 next
   573 next
   574   case (goal2 y1 y2)
   574   case (goal2 y1 y2)
   575   assume a1: "(t,y1)\<in>rec f1 f2 f3" and a2: "(t,y2)\<in>rec f1 f2 f3"
   575   assume a1: "(t,y1)\<in>rec f1 f2 f3" and a2: "(t,y2)\<in>rec f1 f2 f3"