# HG changeset patch
# User paulson
# Date 1077554018 -3600
# Node ID 91181ee5860cd5da7d96bd7761c9ed3865aa4fa4
# Parent  0cc42bb96330e95c221bc32da6ea886b928bdb59
converted HOL/Complex/NSInduct to Isar script

diff -r 0cc42bb96330 -r 91181ee5860c src/HOL/Complex/NSInduct.ML
--- a/src/HOL/Complex/NSInduct.ML	Mon Feb 23 16:35:46 2004 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,116 +0,0 @@
-(*  Title:       NSInduct.ML
-    Author:      Jacques D. Fleuriot
-    Copyright:   2001  University of Edinburgh
-    Description: Nonstandard characterization of induction etc.
-*)
-
-Goalw [starPNat_def]
-"(( *pNat* P) (Abs_hypnat(hypnatrel``{%n. X n}))) = \
-\     ({n. P (X n)} : FreeUltrafilterNat)";
-by (Auto_tac);
-by (Ultra_tac 1);
-qed "starPNat";
-
-Goal "( *pNat* P) (hypnat_of_nat n) = P n";
-by (auto_tac (claset(),simpset() addsimps [starPNat, hypnat_of_nat_eq]));
-qed "starPNat_hypnat_of_nat";
-Addsimps [starPNat_hypnat_of_nat];
-
-Goalw [hypnat_zero_def,hypnat_one_def]
-    "!!P. (( *pNat* P) 0 &   \
-\           (ALL n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1))) \
-\      --> ( *pNat* P)(n)";
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starPNat]));
-by (Ultra_tac 1);
-by (etac nat_induct 1);
-by (dres_inst_tac [("x","hypnat_of_nat n")] spec 1);
-by (rtac ccontr 1);
-by (auto_tac (claset(),simpset() addsimps [starPNat,
-    hypnat_of_nat_eq,hypnat_add]));
-qed "hypnat_induct_obj";
-
-Goal
-  "!!P. [| ( *pNat* P) 0;   \
-\        !!n. ( *pNat* P)(n) ==> ( *pNat* P)(n + 1)|] \
-\    ==> ( *pNat* P)(n)";
-by (cut_inst_tac [("P","P"),("n","n")] hypnat_induct_obj 1);
-by (Auto_tac);
-qed "hypnat_induct";
-
-fun hypnat_ind_tac a i = 
-  res_inst_tac [("n",a)] hypnat_induct i  THEN  rename_last_tac a [""] (i+1);
-
-Goalw [starPNat2_def]
-"(( *pNat2* P) (Abs_hypnat(hypnatrel``{%n. X n})) \
-\            (Abs_hypnat(hypnatrel``{%n. Y n}))) = \
-\     ({n. P (X n) (Y n)} : FreeUltrafilterNat)";
-by (Auto_tac);
-by (Ultra_tac 1);
-qed "starPNat2";
-
-Goalw [starPNat2_def] "( *pNat2* (op =)) = (op =)";
-by (rtac ext 1);
-by (rtac ext 1);
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
-by (Auto_tac THEN Ultra_tac 1);
-qed "starPNat2_eq_iff";
-
-Goal "( *pNat2* (%x y. x = y)) X Y = (X = Y)";
-by (simp_tac (simpset() addsimps [starPNat2_eq_iff]) 1);
-qed "starPNat2_eq_iff2";
-
-Goal "(EX h. P(h::hypnat)) = (EX x. P(Abs_hypnat(hypnatrel `` {x})))";
-by (Auto_tac);
-by (res_inst_tac [("z","h")] eq_Abs_hypnat 1);
-by (Auto_tac);
-val lemma_hyp = result();
-
-Goalw [hSuc_def] "hSuc m ~= 0";
-by Auto_tac;
-qed "hSuc_not_zero";
-
-bind_thm ("zero_not_hSuc", hSuc_not_zero RS not_sym);
-
-Goalw [hSuc_def,hypnat_one_def] 
-      "(hSuc m = hSuc n) = (m = n)";
-by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
-by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [hypnat_add]));
-qed "hSuc_hSuc_eq";
-
-AddIffs [hSuc_not_zero,zero_not_hSuc,hSuc_hSuc_eq];
-
-Goal "c : (S :: nat set) ==> (LEAST n. n : S) : S";
-by (etac LeastI 1);
-qed "nonempty_nat_set_Least_mem";
-
-Goalw [InternalNatSets_def,starsetNat_n_def]
-    "[| S : InternalNatSets; S ~= {} |] ==> EX n: S. ALL m: S. n <= m";
-by (auto_tac (claset(),simpset() addsimps [lemma_hyp]));
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset() addSDs [bspec],simpset() addsimps [hypnat_le]));
-by (dres_inst_tac [("x","%m. LEAST n. n : As m")] spec 1);
-by Auto_tac;
-by (ultra_tac (claset() addDs [nonempty_nat_set_Least_mem],simpset()) 1);
-by (dres_inst_tac [("x","x")] bspec 1 THEN Auto_tac);
-by (ultra_tac (claset() addIs [Least_le],simpset()) 1);
-qed "nonempty_InternalNatSet_has_least";
-
-(* Goldblatt p 129 Thm 11.3.2 *)
-Goal "[| X : InternalNatSets; 0 : X; ALL n. n : X --> n + 1 : X |] \
-\     ==> X = (UNIV:: hypnat set)";
-by (rtac ccontr 1);
-by (ftac InternalNatSets_Compl 1);
-by (dres_inst_tac [("S","- X")] nonempty_InternalNatSet_has_least 1);
-by Auto_tac;
-by (subgoal_tac "1 <= n" 1);
-by (dres_inst_tac [("x","n - 1")] bspec 1);
-by (Step_tac 1);
-by (dres_inst_tac [("x","n - 1")] spec 1);
-by (dres_inst_tac [("c","1"),("a","n")] add_right_mono 2); 
-by (auto_tac ((claset(),simpset() addsimps [linorder_not_less RS sym])
-        delIffs [hypnat_neq0_conv]));
-qed "internal_induct";
-
diff -r 0cc42bb96330 -r 91181ee5860c src/HOL/Complex/NSInduct.thy
--- a/src/HOL/Complex/NSInduct.thy	Mon Feb 23 16:35:46 2004 +0100
+++ b/src/HOL/Complex/NSInduct.thy	Mon Feb 23 17:33:38 2004 +0100
@@ -1,23 +1,127 @@
 (*  Title:       NSInduct.thy
     Author:      Jacques D. Fleuriot
     Copyright:   2001  University of Edinburgh
-    Description: Nonstandard characterization of induction etc.
 *)
 
-NSInduct =  Complex + 
+header{*Nonstandard Characterization of Induction*}
+
+theory NSInduct =  Complex:
 
 constdefs
 
-  starPNat :: (nat => bool) => hypnat => bool  ("*pNat* _" [80] 80)
-  "*pNat* P == (%x. EX X. (X: Rep_hypnat(x) & 
-                      {n. P(X n)} : FreeUltrafilterNat))" 
+  starPNat :: "(nat => bool) => hypnat => bool"  ("*pNat* _" [80] 80)
+  "*pNat* P == (%x. \<exists>X. (X \<in> Rep_hypnat(x) &
+                      {n. P(X n)} \<in> FreeUltrafilterNat))"
+
+
+  starPNat2 :: "(nat => nat => bool) => hypnat =>hypnat => bool"
+               ("*pNat2* _" [80] 80)
+  "*pNat2* P == (%x y. \<exists>X. \<exists>Y. (X \<in> Rep_hypnat(x) & Y \<in> Rep_hypnat(y) &
+                      {n. P(X n) (Y n)} \<in> FreeUltrafilterNat))"
+
+  hSuc :: "hypnat => hypnat"
+  "hSuc n == n + 1"
 
 
-  starPNat2 :: (nat => nat => bool) => hypnat =>hypnat => bool  ("*pNat2* _" [80] 80)
-  "*pNat2* P == (%x y. EX X. EX Y. (X: Rep_hypnat(x) & Y: Rep_hypnat(y) & 
-                      {n. P(X n) (Y n)} : FreeUltrafilterNat))" 
+lemma starPNat:
+     "(( *pNat* P) (Abs_hypnat(hypnatrel``{%n. X n}))) =
+      ({n. P (X n)} \<in> FreeUltrafilterNat)"
+by (auto simp add: starPNat_def, ultra)
+
+lemma starPNat_hypnat_of_nat [simp]: "( *pNat* P) (hypnat_of_nat n) = P n"
+by (auto simp add: starPNat hypnat_of_nat_eq)
+
+lemma hypnat_induct_obj:
+    "(( *pNat* P) 0 &
+            (\<forall>n. ( *pNat* P)(n) --> ( *pNat* P)(n + 1)))
+       --> ( *pNat* P)(n)"
+apply (rule eq_Abs_hypnat [of n])
+apply (auto simp add: hypnat_zero_def hypnat_one_def starPNat, ultra)
+apply (erule nat_induct)
+apply (drule_tac x = "hypnat_of_nat n" in spec)
+apply (rule ccontr)
+apply (auto simp add: starPNat hypnat_of_nat_eq hypnat_add)
+done
+
+lemma hypnat_induct:
+  "[| ( *pNat* P) 0;
+      !!n. ( *pNat* P)(n) ==> ( *pNat* P)(n + 1)|]
+     ==> ( *pNat* P)(n)"
+by (insert hypnat_induct_obj [of P n], auto)
+
+lemma starPNat2:
+"(( *pNat2* P) (Abs_hypnat(hypnatrel``{%n. X n}))
+             (Abs_hypnat(hypnatrel``{%n. Y n}))) =
+      ({n. P (X n) (Y n)} \<in> FreeUltrafilterNat)"
+by (auto simp add: starPNat2_def, ultra)
+
+lemma starPNat2_eq_iff: "( *pNat2* (op =)) = (op =)"
+apply (simp add: starPNat2_def)
+apply (rule ext)
+apply (rule ext)
+apply (rule_tac z = x in eq_Abs_hypnat)
+apply (rule_tac z = y in eq_Abs_hypnat)
+apply (auto, ultra)
+done
+
+lemma starPNat2_eq_iff2: "( *pNat2* (%x y. x = y)) X Y = (X = Y)"
+by (simp add: starPNat2_eq_iff)
+
+lemma lemma_hyp: "(\<exists>h. P(h::hypnat)) = (\<exists>x. P(Abs_hypnat(hypnatrel `` {x})))"
+apply auto
+apply (rule_tac z = h in eq_Abs_hypnat, auto)
+done
 
-  hSuc :: hypnat => hypnat
-  "hSuc n == n + 1"
-    
-end
\ No newline at end of file
+lemma hSuc_not_zero [iff]: "hSuc m \<noteq> 0"
+by (simp add: hSuc_def)
+
+lemmas zero_not_hSuc = hSuc_not_zero [THEN not_sym, standard, iff]
+
+lemma hSuc_hSuc_eq [iff]: "(hSuc m = hSuc n) = (m = n)"
+by (simp add: hSuc_def hypnat_one_def)
+
+lemma nonempty_nat_set_Least_mem: "c \<in> (S :: nat set) ==> (LEAST n. n  \<in> S)  \<in> S"
+by (erule LeastI)
+
+lemma nonempty_InternalNatSet_has_least:
+    "[| S \<in> InternalNatSets; S \<noteq> {} |] ==> \<exists>n \<in> S. \<forall>m \<in> S. n \<le> m"
+apply (auto simp add: InternalNatSets_def starsetNat_n_def lemma_hyp)
+apply (rule_tac z = x in eq_Abs_hypnat)
+apply (auto dest!: bspec simp add: hypnat_le)
+apply (drule_tac x = "%m. LEAST n. n \<in> As m" in spec, auto)
+apply (ultra, force dest: nonempty_nat_set_Least_mem)
+apply (drule_tac x = x in bspec, auto)
+apply (ultra, auto intro: Least_le)
+done
+
+text{* Goldblatt page 129 Thm 11.3.2*}
+lemma internal_induct:
+     "[| X \<in> InternalNatSets; 0 \<in> X; \<forall>n. n \<in> X --> n + 1 \<in> X |]
+      ==> X = (UNIV:: hypnat set)"
+apply (rule ccontr)
+apply (frule InternalNatSets_Compl)
+apply (drule_tac S = "- X" in nonempty_InternalNatSet_has_least, auto)
+apply (subgoal_tac "1 \<le> n")
+apply (drule_tac x = "n - 1" in bspec, safe)
+apply (drule_tac x = "n - 1" in spec)
+apply (drule_tac [2] c = 1 and a = n in add_right_mono)
+apply (auto simp add: linorder_not_less [symmetric] iff del: hypnat_neq0_conv)
+done
+
+ML
+{*
+val starPNat = thm "starPNat";
+val starPNat_hypnat_of_nat = thm "starPNat_hypnat_of_nat";
+val hypnat_induct = thm "hypnat_induct";
+val starPNat2 = thm "starPNat2";
+val starPNat2_eq_iff = thm "starPNat2_eq_iff";
+val starPNat2_eq_iff2 = thm "starPNat2_eq_iff2";
+val hSuc_not_zero = thm "hSuc_not_zero";
+val zero_not_hSuc = thms "zero_not_hSuc";
+val hSuc_hSuc_eq = thm "hSuc_hSuc_eq";
+val nonempty_nat_set_Least_mem = thm "nonempty_nat_set_Least_mem";
+val nonempty_InternalNatSet_has_least = thm "nonempty_InternalNatSet_has_least";
+val internal_induct = thm "internal_induct";
+*}
+
+end
diff -r 0cc42bb96330 -r 91181ee5860c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Feb 23 16:35:46 2004 +0100
+++ b/src/HOL/IsaMakefile	Mon Feb 23 17:33:38 2004 +0100
@@ -160,7 +160,7 @@
   Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
   Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy\
   Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy\
-  Complex/NSCA.thy Complex/NSComplex.thy
+  Complex/NSCA.thy Complex/NSComplex.thy Complex/NSInduct.thy
 	@cd Complex; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Complex