src/HOL/Inductive.thy
changeset 45899 df887263a379
parent 45897 65cef0298158
child 45907 4b41967bd77e
     1.1 --- a/src/HOL/Inductive.thy	Fri Dec 16 11:02:55 2011 +0100
     1.2 +++ b/src/HOL/Inductive.thy	Fri Dec 16 12:03:33 2011 +0100
     1.3 @@ -116,7 +116,7 @@
     1.4      to control unfolding*}
     1.5  
     1.6  lemma def_lfp_unfold: "[| h==lfp(f);  mono(f) |] ==> h = f(h)"
     1.7 -by (auto intro!: lfp_unfold)
     1.8 +  by (auto intro!: lfp_unfold)
     1.9  
    1.10  lemma def_lfp_induct: 
    1.11      "[| A == lfp(f); mono(f);
    1.12 @@ -160,12 +160,12 @@
    1.13  
    1.14  text{*weak version*}
    1.15  lemma weak_coinduct: "[| a: X;  X \<subseteq> f(X) |] ==> a : gfp(f)"
    1.16 -by (rule gfp_upperbound [THEN subsetD], auto)
    1.17 +  by (rule gfp_upperbound [THEN subsetD]) auto
    1.18  
    1.19  lemma weak_coinduct_image: "!!X. [| a : X; g`X \<subseteq> f (g`X) |] ==> g a : gfp f"
    1.20 -apply (erule gfp_upperbound [THEN subsetD])
    1.21 -apply (erule imageI)
    1.22 -done
    1.23 +  apply (erule gfp_upperbound [THEN subsetD])
    1.24 +  apply (erule imageI)
    1.25 +  done
    1.26  
    1.27  lemma coinduct_lemma:
    1.28       "[| X \<le> f (sup X (gfp f));  mono f |] ==> sup X (gfp f) \<le> f (sup X (gfp f))"
    1.29 @@ -182,7 +182,7 @@
    1.30  
    1.31  text{*strong version, thanks to Coen and Frost*}
    1.32  lemma coinduct_set: "[| mono(f);  a: X;  X \<subseteq> f(X Un gfp(f)) |] ==> a : gfp(f)"
    1.33 -by (blast intro: weak_coinduct [OF _ coinduct_lemma])
    1.34 +  by (blast intro: weak_coinduct [OF _ coinduct_lemma])
    1.35  
    1.36  lemma coinduct: "[| mono(f); X \<le> f (sup X (gfp f)) |] ==> X \<le> gfp(f)"
    1.37    apply (rule order_trans)
    1.38 @@ -192,7 +192,7 @@
    1.39    done
    1.40  
    1.41  lemma gfp_fun_UnI2: "[| mono(f);  a: gfp(f) |] ==> a: f(X Un gfp(f))"
    1.42 -by (blast dest: gfp_lemma2 mono_Un)
    1.43 +  by (blast dest: gfp_lemma2 mono_Un)
    1.44  
    1.45  
    1.46  subsection {* Even Stronger Coinduction Rule, by Martin Coen *}
    1.47 @@ -227,27 +227,26 @@
    1.48      to control unfolding*}
    1.49  
    1.50  lemma def_gfp_unfold: "[| A==gfp(f);  mono(f) |] ==> A = f(A)"
    1.51 -by (auto intro!: gfp_unfold)
    1.52 +  by (auto intro!: gfp_unfold)
    1.53  
    1.54  lemma def_coinduct:
    1.55       "[| A==gfp(f);  mono(f);  X \<le> f(sup X A) |] ==> X \<le> A"
    1.56 -by (iprover intro!: coinduct)
    1.57 +  by (iprover intro!: coinduct)
    1.58  
    1.59  lemma def_coinduct_set:
    1.60       "[| A==gfp(f);  mono(f);  a:X;  X \<subseteq> f(X Un A) |] ==> a: A"
    1.61 -by (auto intro!: coinduct_set)
    1.62 +  by (auto intro!: coinduct_set)
    1.63  
    1.64  (*The version used in the induction/coinduction package*)
    1.65  lemma def_Collect_coinduct:
    1.66      "[| A == gfp(%w. Collect(P(w)));  mono(%w. Collect(P(w)));   
    1.67          a: X;  !!z. z: X ==> P (X Un A) z |] ==>  
    1.68       a : A"
    1.69 -apply (erule def_coinduct_set, auto) 
    1.70 -done
    1.71 +  by (erule def_coinduct_set) auto
    1.72  
    1.73  lemma def_coinduct3:
    1.74      "[| A==gfp(f); mono(f);  a:X;  X \<subseteq> f(lfp(%x. f(x) Un X Un A)) |] ==> a: A"
    1.75 -by (auto intro!: coinduct3)
    1.76 +  by (auto intro!: coinduct3)
    1.77  
    1.78  text{*Monotonicity of @{term gfp}!*}
    1.79  lemma gfp_mono: "(!!Z. f Z \<le> g Z) ==> gfp f \<le> gfp g"
    1.80 @@ -296,8 +295,7 @@
    1.81  let
    1.82    fun fun_tr ctxt [cs] =
    1.83      let
    1.84 -      (* FIXME proper name context!? *)
    1.85 -      val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
    1.86 +      val x = Syntax.free (fst (Name.variant "x" (Term.declare_term_frees cs Name.context)));
    1.87        val ft = Datatype_Case.case_tr true ctxt [x, cs];
    1.88      in lambda x ft end
    1.89  in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end