For the Isar version of the ZF logics manual

--- a/doc-src/ZF/FOL-eg.txt	Fri Aug 15 13:45:39 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,245 +0,0 @@
-(**** FOL examples ****)
-
-Pretty.setmargin 72;  (*existing macros just allow this margin*)
-print_depth 0;
-
-(*** Intuitionistic examples ***)
-
-context IFOL.thy;
-
-(*Quantifier example from Logic&Computation*)
-Goal "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
-by (resolve_tac [impI] 1);
-by (resolve_tac [allI] 1);
-by (resolve_tac [exI] 1);
-by (eresolve_tac [exE] 1);
-choplev 2;
-by (eresolve_tac [exE] 1);
-by (resolve_tac [exI] 1);
-by (eresolve_tac [allE] 1);
-by (assume_tac 1);
-
-
-(*Example of Dyckhoff's method*)
-Goalw [not_def] "~ ~ ((P-->Q) | (Q-->P))";
-by (resolve_tac [impI] 1);
-by (eresolve_tac [disj_impE] 1);
-by (eresolve_tac [imp_impE] 1);
-by (eresolve_tac [imp_impE] 1);
-by (REPEAT (eresolve_tac [FalseE] 2));
-by (assume_tac 1);
-
-
-
-
-
-(*** Classical examples ***)
-
-context FOL.thy;
-
-Goal "EX y. ALL x. P(y)-->P(x)";
-by (resolve_tac [exCI] 1);
-by (resolve_tac [allI] 1);
-by (resolve_tac [impI] 1);
-by (eresolve_tac [allE] 1);
-prth (allI RSN (2,swap));
-by (eresolve_tac [it] 1);
-by (resolve_tac [impI] 1);
-by (eresolve_tac [notE] 1);
-by (assume_tac 1);
-Goal "EX y. ALL x. P(y)-->P(x)";
-by (Blast_tac 1);
-
-
-
-- Goal "EX y. ALL x. P(y)-->P(x)";
-Level 0
-EX y. ALL x. P(y) --> P(x)
- 1. EX y. ALL x. P(y) --> P(x)
-- by (resolve_tac [exCI] 1);
-Level 1
-EX y. ALL x. P(y) --> P(x)
- 1. ALL y. ~(ALL x. P(y) --> P(x)) ==> ALL x. P(?a) --> P(x)
-- by (resolve_tac [allI] 1);
-Level 2
-EX y. ALL x. P(y) --> P(x)
- 1. !!x. ALL y. ~(ALL x. P(y) --> P(x)) ==> P(?a) --> P(x)
-- by (resolve_tac [impI] 1);
-Level 3
-EX y. ALL x. P(y) --> P(x)
- 1. !!x. [| ALL y. ~(ALL x. P(y) --> P(x)); P(?a) |] ==> P(x)
-- by (eresolve_tac [allE] 1);
-Level 4
-EX y. ALL x. P(y) --> P(x)
- 1. !!x. [| P(?a); ~(ALL xa. P(?y3(x)) --> P(xa)) |] ==> P(x)
-- prth (allI RSN (2,swap));
-[| ~(ALL x. ?P1(x)); !!x. ~?Q ==> ?P1(x) |] ==> ?Q
-- by (eresolve_tac [it] 1);
-Level 5
-EX y. ALL x. P(y) --> P(x)
- 1. !!x xa. [| P(?a); ~P(x) |] ==> P(?y3(x)) --> P(xa)
-- by (resolve_tac [impI] 1);
-Level 6
-EX y. ALL x. P(y) --> P(x)
- 1. !!x xa. [| P(?a); ~P(x); P(?y3(x)) |] ==> P(xa)
-- by (eresolve_tac [notE] 1);
-Level 7
-EX y. ALL x. P(y) --> P(x)
- 1. !!x xa. [| P(?a); P(?y3(x)) |] ==> P(x)
-- by (assume_tac 1);
-Level 8
-EX y. ALL x. P(y) --> P(x)
-No subgoals!
-- Goal "EX y. ALL x. P(y)-->P(x)";
-Level 0
-EX y. ALL x. P(y) --> P(x)
- 1. EX y. ALL x. P(y) --> P(x)
-- by (best_tac FOL_dup_cs 1);
-Level 1
-EX y. ALL x. P(y) --> P(x)
-No subgoals!
-
-
-(**** finally, the example FOL/ex/if.ML ****)
-
-> val prems = goalw if_thy [if_def]
-#    "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
-Level 0
-if(P,Q,R)
- 1. P & Q | ~P & R
-> by (Classical.fast_tac (FOL_cs addIs prems) 1);
-Level 1
-if(P,Q,R)
-No subgoals!
-> val ifI = result();
-
-
-> val major::prems = goalw if_thy [if_def]
-#    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
-Level 0
-S
- 1. S
-> by (cut_facts_tac [major] 1);
-Level 1
-S
- 1. P & Q | ~P & R ==> S
-> by (Classical.fast_tac (FOL_cs addIs prems) 1);
-Level 2
-S
-No subgoals!
-> val ifE = result();
-
-> goal if_thy "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
-Level 0
-if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
- 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
-> by (resolve_tac [iffI] 1);
-Level 1
-if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
- 1. if(P,if(Q,A,B),if(Q,C,D)) ==> if(Q,if(P,A,C),if(P,B,D))
- 2. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
-> by (eresolve_tac [ifE] 1);
-Level 2
-if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
- 1. [| P; if(Q,A,B) |] ==> if(Q,if(P,A,C),if(P,B,D))
- 2. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
- 3. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
-> by (eresolve_tac [ifE] 1);
-Level 3
-if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
- 1. [| P; Q; A |] ==> if(Q,if(P,A,C),if(P,B,D))
- 2. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
- 3. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
- 4. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
-> by (resolve_tac [ifI] 1);
-Level 4
-if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
- 1. [| P; Q; A; Q |] ==> if(P,A,C)
- 2. [| P; Q; A; ~Q |] ==> if(P,B,D)
- 3. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
- 4. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
- 5. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
-> by (resolve_tac [ifI] 1);
-Level 5
-if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
- 1. [| P; Q; A; Q; P |] ==> A
- 2. [| P; Q; A; Q; ~P |] ==> C
- 3. [| P; Q; A; ~Q |] ==> if(P,B,D)
- 4. [| P; ~Q; B |] ==> if(Q,if(P,A,C),if(P,B,D))
- 5. [| ~P; if(Q,C,D) |] ==> if(Q,if(P,A,C),if(P,B,D))
- 6. if(Q,if(P,A,C),if(P,B,D)) ==> if(P,if(Q,A,B),if(Q,C,D))
-
-> choplev 0;
-Level 0
-if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
- 1. if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
-> val if_cs = FOL_cs addSIs [ifI] addSEs[ifE];
-> by (Classical.fast_tac if_cs 1);
-Level 1
-if(P,if(Q,A,B),if(Q,C,D)) <-> if(Q,if(P,A,C),if(P,B,D))
-No subgoals!
-> val if_commute = result();
-
-> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
-Level 0
-if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
- 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
-> by (Classical.fast_tac if_cs 1);
-Level 1
-if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
-No subgoals!
-> val nested_ifs = result();
-
-
-> choplev 0;
-Level 0
-if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
- 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
-> by (rewrite_goals_tac [if_def]);
-Level 1
-if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
- 1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <->
-    P & (Q & A | ~Q & B) | ~P & (R & A | ~R & B)
-> by (Classical.fast_tac FOL_cs 1);
-Level 2
-if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,A,B))
-No subgoals!
-
-
-> goal if_thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
-Level 0
-if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
- 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
-> by (REPEAT (Classical.step_tac if_cs 1));
-Level 1
-if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
- 1. [| A; ~P; R; ~P; R |] ==> B
- 2. [| B; ~P; ~R; ~P; ~R |] ==> A
- 3. [| ~P; R; B; ~P; R |] ==> A
- 4. [| ~P; ~R; A; ~B; ~P |] ==> R
-
-> choplev 0;
-Level 0
-if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
- 1. if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
-> by (rewrite_goals_tac [if_def]);
-Level 1
-if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
- 1. (P & Q | ~P & R) & A | ~(P & Q | ~P & R) & B <->
-    P & (Q & A | ~Q & B) | ~P & (R & B | ~R & A)
-> by (Classical.fast_tac FOL_cs 1);
-by: tactic failed
-Exception- ERROR raised
-Exception failure raised
-
-> by (REPEAT (Classical.step_tac FOL_cs 1));
-Level 2
-if(if(P,Q,R),A,B) <-> if(P,if(Q,A,B),if(R,B,A))
- 1. [| A; ~P; R; ~P; R; ~False |] ==> B
- 2. [| A; ~P; R; R; ~False; ~B; ~B |] ==> Q
- 3. [| B; ~P; ~R; ~P; ~A |] ==> R
- 4. [| B; ~P; ~R; ~Q; ~A |] ==> R
- 5. [| B; ~R; ~P; ~A; ~R; Q; ~False |] ==> A
- 6. [| ~P; R; B; ~P; R; ~False |] ==> A
- 7. [| ~P; ~R; A; ~B; ~R |] ==> P
- 8. [| ~P; ~R; A; ~B; ~R |] ==> Q

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ZF/FOL_examples.thy	Tue Aug 19 13:53:58 2003 +0200
@@ -0,0 +1,34 @@
+header{*Examples of Classical Reasoning*}
+
+theory FOL_examples = FOL:
+
+lemma "EX y. ALL x. P(y)-->P(x)"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule exCI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule allI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule impI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule allE)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+txt{*see below for @{text allI} combined with @{text swap}*}
+apply (erule allI [THEN [2] swap])
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule impI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule notE)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply assumption
+done
+
+text {*
+@{thm[display] allI [THEN [2] swap]}
+*}
+
+lemma "EX y. ALL x. P(y)-->P(x)"
+by blast
+
+end
+
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ZF/IFOL_examples.thy	Tue Aug 19 13:53:58 2003 +0200
@@ -0,0 +1,58 @@
+header{*Examples of Intuitionistic Reasoning*}
+
+theory IFOL_examples = IFOL:
+
+text{*Quantifier example from the book Logic and Computation*}
+lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule impI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule allI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule exI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule exE)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule allE)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+txt{*Now @{text "apply assumption"} fails*}
+oops
+
+text{*Trying again, with the same first two steps*}
+lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule impI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule allI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule exE)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule exI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule allE)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply assumption
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+done
+
+lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
+by (tactic {*IntPr.fast_tac 1*})
+
+text{*Example of Dyckhoff's method*}
+lemma "~ ~ ((P-->Q) | (Q-->P))"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (unfold not_def)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule impI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule disj_impE)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule imp_impE)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+ apply (erule imp_impE)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply assumption 
+apply (erule FalseE)+
+done
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ZF/IsaMakefile	Tue Aug 19 13:53:58 2003 +0200
@@ -0,0 +1,50 @@
+#
+# IsaMakefile to build the examples for the FOL and ZF manual
+#
+
+## targets
+
+default: ZF-examples styles
+images:
+test:
+all: default
+
+
+## global settings
+
+SRC = $(ISABELLE_HOME)/src
+OUT = $(ISABELLE_OUTPUT)
+LOG = $(OUT)/log
+OPTIONS = -m brackets -i true -d "" -D document
+USEDIR = @$(ISATOOL) usedir $(OPTIONS) $(OUT)/ZF
+
+
+## ZF
+
+ZF:
+	@cd $(SRC)/ZF; $(ISATOOL) make ZF
+
+styles:
+	@rm -f isabelle.sty
+	@rm -f isabellesym.sty
+	@rm -f pdfsetup.sty
+	@$(ISATOOL) latex -o sty >/dev/null
+	@rm -f pdfsetup.sty
+	@rm -f document/isabelle.sty
+	@rm -f document/isabellesym.sty
+	@rm -f document/pdfsetup.sty
+	@rm -f document/session.tex
+
+
+## ZF-examples
+
+ZF-examples: ZF $(LOG)/ZF-examples.gz
+
+$(LOG)/ZF-examples.gz: $(OUT)/ZF \
+	FOL_examples.thy  IFOL_examples.thy ZF_examples.thy If.thy ROOT.ML 
+	@$(USEDIR) .
+
+## clean
+
+clean:
+	@rm -f $(LOG)/ZF-examples.gz document/*.tex 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ZF/ROOT.ML	Tue Aug 19 13:53:58 2003 +0200
@@ -0,0 +1,5 @@
+(* ID:         $Id$ *)
+use_thy "IFOL_examples";
+use_thy "FOL_examples";
+use_thy "ZF_examples";
+use_thy "If";

--- a/doc-src/ZF/ZF-eg.txt	Fri Aug 15 13:45:39 2003 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,230 +0,0 @@
-(**** ZF examples ****)
-
-Pretty.setmargin 72;  (*existing macros just allow this margin*)
-print_depth 0;
-
-(*** Powerset example ***)
-
-val [prem] = goal ZF.thy "A<=B  ==>  Pow(A) <= Pow(B)";
-by (resolve_tac [subsetI] 1);
-by (resolve_tac [PowI] 1);
-by (dresolve_tac [PowD] 1);
-by (eresolve_tac [subset_trans] 1);
-by (resolve_tac [prem] 1);
-val Pow_mono = result();
-
-goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
-by (resolve_tac [equalityI] 1);
-by (resolve_tac [Int_greatest] 1);
-by (resolve_tac [Int_lower1 RS Pow_mono] 1);
-by (resolve_tac [Int_lower2 RS Pow_mono] 1);
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [IntE] 1);
-by (resolve_tac [PowI] 1);
-by (REPEAT (dresolve_tac [PowD] 1));
-by (resolve_tac [Int_greatest] 1);
-by (REPEAT (assume_tac 1));
-choplev 0;
-by (fast_tac (ZF_cs addIs [equalityI]) 1);
-
-Goal "C<=D ==> Union(C) <= Union(D)";
-by (resolve_tac [subsetI] 1);
-by (eresolve_tac [UnionE] 1);
-by (resolve_tac [UnionI] 1);
-by (eresolve_tac [subsetD] 1);
-by (assume_tac 1);
-by (assume_tac 1);
-choplev 0;
-by (resolve_tac [Union_least] 1);
-by (resolve_tac [Union_upper] 1);
-by (eresolve_tac [subsetD] 1);
-
-
-val prems = goal ZF.thy
-    "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
-\    (f Un g)`a = f`a";
-by (resolve_tac [apply_equality] 1);
-by (resolve_tac [UnI1] 1);
-by (resolve_tac [apply_Pair] 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
-by (resolve_tac [fun_disjoint_Un] 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
-by (resolve_tac prems 1);
-
-
-Goal "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
-\     (f Un g)`a = f`a";
-by (resolve_tac [apply_equality] 1);
-by (resolve_tac [UnI1] 1);
-by (resolve_tac [apply_Pair] 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (resolve_tac [fun_disjoint_Un] 1);
-by (assume_tac 1);
-by (assume_tac 1);
-by (assume_tac 1);
-
-
-
-
-goal ZF.thy "f``(UN x:A. B(x)) = (UN x:A. f``B(x))";
-by (resolve_tac [equalityI] 1);
-by (resolve_tac [subsetI] 1);
-fe imageE;
-
-
-goal ZF.thy "(UN x:C. A(x) Int B) = (UN x:C. A(x))  Int  B";
-by (resolve_tac [equalityI] 1);
-by (resolve_tac [Int_greatest] 1);
-fr UN_mono;
-by (resolve_tac [Int_lower1] 1);
-fr UN_least;
-????
-
-
-> goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
-Level 0
-Pow(A Int B) = Pow(A) Int Pow(B)
- 1. Pow(A Int B) = Pow(A) Int Pow(B)
-> by (resolve_tac [equalityI] 1);
-Level 1
-Pow(A Int B) = Pow(A) Int Pow(B)
- 1. Pow(A Int B) <= Pow(A) Int Pow(B)
- 2. Pow(A) Int Pow(B) <= Pow(A Int B)
-> by (resolve_tac [Int_greatest] 1);
-Level 2
-Pow(A Int B) = Pow(A) Int Pow(B)
- 1. Pow(A Int B) <= Pow(A)
- 2. Pow(A Int B) <= Pow(B)
- 3. Pow(A) Int Pow(B) <= Pow(A Int B)
-> by (resolve_tac [Int_lower1 RS Pow_mono] 1);
-Level 3
-Pow(A Int B) = Pow(A) Int Pow(B)
- 1. Pow(A Int B) <= Pow(B)
- 2. Pow(A) Int Pow(B) <= Pow(A Int B)
-> by (resolve_tac [Int_lower2 RS Pow_mono] 1);
-Level 4
-Pow(A Int B) = Pow(A) Int Pow(B)
- 1. Pow(A) Int Pow(B) <= Pow(A Int B)
-> by (resolve_tac [subsetI] 1);
-Level 5
-Pow(A Int B) = Pow(A) Int Pow(B)
- 1. !!x. x : Pow(A) Int Pow(B) ==> x : Pow(A Int B)
-> by (eresolve_tac [IntE] 1);
-Level 6
-Pow(A Int B) = Pow(A) Int Pow(B)
- 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x : Pow(A Int B)
-> by (resolve_tac [PowI] 1);
-Level 7
-Pow(A Int B) = Pow(A) Int Pow(B)
- 1. !!x. [| x : Pow(A); x : Pow(B) |] ==> x <= A Int B
-> by (REPEAT (dresolve_tac [PowD] 1));
-Level 8
-Pow(A Int B) = Pow(A) Int Pow(B)
- 1. !!x. [| x <= A; x <= B |] ==> x <= A Int B
-> by (resolve_tac [Int_greatest] 1);
-Level 9
-Pow(A Int B) = Pow(A) Int Pow(B)
- 1. !!x. [| x <= A; x <= B |] ==> x <= A
- 2. !!x. [| x <= A; x <= B |] ==> x <= B
-> by (REPEAT (assume_tac 1));
-Level 10
-Pow(A Int B) = Pow(A) Int Pow(B)
-No subgoals!
-> choplev 0;
-Level 0
-Pow(A Int B) = Pow(A) Int Pow(B)
- 1. Pow(A Int B) = Pow(A) Int Pow(B)
-> by (fast_tac (ZF_cs addIs [equalityI]) 1);
-Level 1
-Pow(A Int B) = Pow(A) Int Pow(B)
-No subgoals!
-
-
-
-
-> val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)";
-Level 0
-Union(C) <= Union(D)
- 1. Union(C) <= Union(D)
-> by (resolve_tac [subsetI] 1);
-Level 1
-Union(C) <= Union(D)
- 1. !!x. x : Union(C) ==> x : Union(D)
-> by (eresolve_tac [UnionE] 1);
-Level 2
-Union(C) <= Union(D)
- 1. !!x B. [| x : B; B : C |] ==> x : Union(D)
-> by (resolve_tac [UnionI] 1);
-Level 3
-Union(C) <= Union(D)
- 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : D
- 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)
-> by (resolve_tac [prem RS subsetD] 1);
-Level 4
-Union(C) <= Union(D)
- 1. !!x B. [| x : B; B : C |] ==> ?B2(x,B) : C
- 2. !!x B. [| x : B; B : C |] ==> x : ?B2(x,B)
-> by (assume_tac 1);
-Level 5
-Union(C) <= Union(D)
- 1. !!x B. [| x : B; B : C |] ==> x : B
-> by (assume_tac 1);
-Level 6
-Union(C) <= Union(D)
-No subgoals!
-
-
-
-> val prems = goal ZF.thy
-#     "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==>  \
-# \    (f Un g)`a = f`a";
-Level 0
-(f Un g) ` a = f ` a
- 1. (f Un g) ` a = f ` a
-> by (resolve_tac [apply_equality] 1);
-Level 1
-(f Un g) ` a = f ` a
- 1. <a,f ` a> : f Un g
- 2. f Un g : (PROD x:?A. ?B(x))
-> by (resolve_tac [UnI1] 1);
-Level 2
-(f Un g) ` a = f ` a
- 1. <a,f ` a> : f
- 2. f Un g : (PROD x:?A. ?B(x))
-> by (resolve_tac [apply_Pair] 1);
-Level 3
-(f Un g) ` a = f ` a
- 1. f : (PROD x:?A2. ?B2(x))
- 2. a : ?A2
- 3. f Un g : (PROD x:?A. ?B(x))
-> by (resolve_tac prems 1);
-Level 4
-(f Un g) ` a = f ` a
- 1. a : A
- 2. f Un g : (PROD x:?A. ?B(x))
-> by (resolve_tac prems 1);
-Level 5
-(f Un g) ` a = f ` a
- 1. f Un g : (PROD x:?A. ?B(x))
-> by (resolve_tac [fun_disjoint_Un] 1);
-Level 6
-(f Un g) ` a = f ` a
- 1. f : ?A3 -> ?B3
- 2. g : ?C3 -> ?D3
- 3. ?A3 Int ?C3 = 0
-> by (resolve_tac prems 1);
-Level 7
-(f Un g) ` a = f ` a
- 1. g : ?C3 -> ?D3
- 2. A Int ?C3 = 0
-> by (resolve_tac prems 1);
-Level 8
-(f Un g) ` a = f ` a
- 1. A Int C = 0
-> by (resolve_tac prems 1);
-Level 9
-(f Un g) ` a = f ` a
-No subgoals!

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ZF/ZF_examples.thy	Tue Aug 19 13:53:58 2003 +0200
@@ -0,0 +1,121 @@
+header{*Examples of Reasoning in ZF Set Theory*}
+
+theory ZF_examples = Main_ZFC:
+
+subsection {* Binary Trees *}
+
+consts
+  bt :: "i => i"
+
+datatype "bt(A)" =
+  Lf | Br ("a \<in> A", "t1 \<in> bt(A)", "t2 \<in> bt(A)")
+
+declare bt.intros [simp]
+
+text{*Induction via tactic emulation*}
+lemma Br_neq_left [rule_format]: "l \<in> bt(A) ==> \<forall>x r. Br(x, l, r) \<noteq> l"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+  apply (induct_tac l)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+  apply auto
+  done
+
+(*
+  apply (Inductive.case_tac l)
+  apply (tactic {*exhaust_tac "l" 1*})
+*)
+
+text{*The new induction method, which I don't understand*}
+lemma Br_neq_left': "l \<in> bt(A) ==> (!!x r. Br(x, l, r) \<noteq> l)"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+  apply (induct set: bt)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+  apply auto
+  done
+
+lemma Br_iff: "Br(a, l, r) = Br(a', l', r') <-> a = a' & l = l' & r = r'"
+  -- "Proving a freeness theorem."
+  by (blast elim!: bt.free_elims)
+
+inductive_cases BrE: "Br(a, l, r) \<in> bt(A)"
+  -- "An elimination rule, for type-checking."
+
+text {*
+@{thm[display] BrE[no_vars]}
+\rulename{BrE}
+*};
+
+subsection{*Powerset example*}
+
+lemma Pow_mono: "A<=B  ==>  Pow(A) <= Pow(B)"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule subsetI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule PowI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (drule PowD)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule subset_trans, assumption)
+done
+
+lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule equalityI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule Int_greatest)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule Int_lower1 [THEN Pow_mono])
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule Int_lower2 [THEN Pow_mono])
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule subsetI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule IntE)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule PowI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (drule PowD)+
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule Int_greatest, assumption+)
+done
+
+text{*Trying again from the beginning in order to use @{text blast}*}
+lemma "Pow(A Int B) = Pow(A) Int Pow(B)"
+by blast
+
+
+lemma "C<=D ==> Union(C) <= Union(D)"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule subsetI)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule UnionE)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule UnionI)
+apply (erule subsetD, assumption, assumption)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+done
+
+text{*Trying again from the beginning in order to prove from the definitions*}
+
+lemma "C<=D ==> Union(C) <= Union(D)"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule Union_least)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule Union_upper)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (erule subsetD, assumption)
+done
+
+
+lemma "[| a:A;  f: A->B;  g: C->D;  A Int C = 0 |] ==> (f Un g)`a = f`a"
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule apply_equality)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule UnI1)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule apply_Pair, assumption+)
+  --{* @{subgoals[display,indent=0,margin=65]} *}
+apply (rule fun_disjoint_Un, assumption+)
+done
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ZF/isabelle.sty	Tue Aug 19 13:53:58 2003 +0200
@@ -0,0 +1,157 @@
+%%
+%% Author: Markus Wenzel, TU Muenchen
+%% License: GPL (GNU GENERAL PUBLIC LICENSE)
+%%
+%% macros for Isabelle generated LaTeX output
+%%
+
+%%% Simple document preparation (based on theory token language and symbols)
+
+% isabelle environments
+
+\newcommand{\isabellecontext}{UNKNOWN}
+
+\newcommand{\isastyle}{\small\tt\slshape}
+\newcommand{\isastyleminor}{\small\tt\slshape}
+\newcommand{\isastylescript}{\footnotesize\tt\slshape}
+\newcommand{\isastyletext}{\normalsize\rm}
+\newcommand{\isastyletxt}{\rm}
+\newcommand{\isastylecmt}{\rm}
+
+%symbol markup -- \emph achieves decent spacing via italic corrections
+\newcommand{\isamath}[1]{\emph{$#1$}}
+\newcommand{\isatext}[1]{\emph{#1}}
+\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
+
+\newdimen\isa@parindent\newdimen\isa@parskip
+
+\newenvironment{isabellebody}{%
+\isamarkuptrue\par%
+\isa@parindent\parindent\parindent0pt%
+\isa@parskip\parskip\parskip0pt%
+\isastyle}{\par}
+
+\newenvironment{isabelle}
+{\begin{trivlist}\begin{isabellebody}\item\relax}
+{\end{isabellebody}\end{trivlist}}
+
+\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
+
+\newcommand{\isaindent}[1]{\hphantom{#1}}
+\newcommand{\isanewline}{\mbox{}\par\mbox{}}
+\newcommand{\isadigit}[1]{#1}
+
+\chardef\isacharbang=`\!
+\chardef\isachardoublequote=`\"
+\chardef\isacharhash=`\#
+\chardef\isachardollar=`\$
+\chardef\isacharpercent=`\%
+\chardef\isacharampersand=`\&
+\chardef\isacharprime=`\'
+\chardef\isacharparenleft=`\(
+\chardef\isacharparenright=`\)
+\chardef\isacharasterisk=`\*
+\chardef\isacharplus=`\+
+\chardef\isacharcomma=`\,
+\chardef\isacharminus=`\-
+\chardef\isachardot=`\.
+\chardef\isacharslash=`\/
+\chardef\isacharcolon=`\:
+\chardef\isacharsemicolon=`\;
+\chardef\isacharless=`\<
+\chardef\isacharequal=`\=
+\chardef\isachargreater=`\>
+\chardef\isacharquery=`\?
+\chardef\isacharat=`\@
+\chardef\isacharbrackleft=`\[
+\chardef\isacharbackslash=`\\
+\chardef\isacharbrackright=`\]
+\chardef\isacharcircum=`\^
+\chardef\isacharunderscore=`\_
+\chardef\isacharbackquote=`\`
+\chardef\isacharbraceleft=`\{
+\chardef\isacharbar=`\|
+\chardef\isacharbraceright=`\}
+\chardef\isachartilde=`\~
+
+
+% keyword and section markup
+
+\newcommand{\isakeywordcharunderscore}{\_}
+\newcommand{\isakeyword}[1]
+{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
+\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
+\newcommand{\isacommand}[1]{\isakeyword{#1}}
+
+\newcommand{\isamarkupheader}[1]{\section{#1}}
+\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
+\newcommand{\isamarkupsection}[1]{\section{#1}}
+\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
+\newcommand{\isamarkupsect}[1]{\section{#1}}
+\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
+
+\newif\ifisamarkup
+\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
+\newcommand{\isaendpar}{\par\medskip}
+\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
+\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
+\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
+
+
+% alternative styles
+
+\newcommand{\isabellestyle}{}
+\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
+
+\newcommand{\isabellestylett}{%
+\renewcommand{\isastyle}{\small\tt}%
+\renewcommand{\isastyleminor}{\small\tt}%
+\renewcommand{\isastylescript}{\footnotesize\tt}%
+}
+\newcommand{\isabellestyleit}{%
+\renewcommand{\isastyle}{\small\it}%
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastylescript}{\footnotesize\it}%
+\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
+\renewcommand{\isacharbang}{\isamath{!}}%
+\renewcommand{\isachardoublequote}{}%
+\renewcommand{\isacharhash}{\isamath{\#}}%
+\renewcommand{\isachardollar}{\isamath{\$}}%
+\renewcommand{\isacharpercent}{\isamath{\%}}%
+\renewcommand{\isacharampersand}{\isamath{\&}}%
+\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
+\renewcommand{\isacharparenleft}{\isamath{(}}%
+\renewcommand{\isacharparenright}{\isamath{)}}%
+\renewcommand{\isacharasterisk}{\isamath{*}}%
+\renewcommand{\isacharplus}{\isamath{+}}%
+\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
+\renewcommand{\isacharminus}{\isamath{-}}%
+\renewcommand{\isachardot}{\isamath{\mathord.}}%
+\renewcommand{\isacharslash}{\isamath{/}}%
+\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
+\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
+\renewcommand{\isacharless}{\isamath{<}}%
+\renewcommand{\isacharequal}{\isamath{=}}%
+\renewcommand{\isachargreater}{\isamath{>}}%
+\renewcommand{\isacharat}{\isamath{@}}%
+\renewcommand{\isacharbrackleft}{\isamath{[}}%
+\renewcommand{\isacharbrackright}{\isamath{]}}%
+\renewcommand{\isacharunderscore}{\mbox{-}}%
+\renewcommand{\isacharbraceleft}{\isamath{\{}}%
+\renewcommand{\isacharbar}{\isamath{\mid}}%
+\renewcommand{\isacharbraceright}{\isamath{\}}}%
+\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
+}
+
+\newcommand{\isabellestylesl}{%
+\isabellestyleit%
+\renewcommand{\isastyle}{\small\sl}%
+\renewcommand{\isastyleminor}{\sl}%
+\renewcommand{\isastylescript}{\footnotesize\sl}%
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/ZF/isabellesym.sty	Tue Aug 19 13:53:58 2003 +0200
@@ -0,0 +1,354 @@
+%%
+%% Author: Markus Wenzel, TU Muenchen
+%% License: GPL (GNU GENERAL PUBLIC LICENSE)
+%%
+%% definitions of standard Isabelle symbols
+%%
+
+% symbol definitions
+
+\newcommand{\isasymzero}{\isamath{\mathbf{0}}}  %requires amssym
+\newcommand{\isasymone}{\isamath{\mathbf{1}}}   %requires amssym
+\newcommand{\isasymtwo}{\isamath{\mathbf{2}}}   %requires amssym
+\newcommand{\isasymthree}{\isamath{\mathbf{3}}} %requires amssym
+\newcommand{\isasymfour}{\isamath{\mathbf{4}}}  %requires amssym
+\newcommand{\isasymfive}{\isamath{\mathbf{5}}}  %requires amssym
+\newcommand{\isasymsix}{\isamath{\mathbf{6}}}   %requires amssym
+\newcommand{\isasymseven}{\isamath{\mathbf{7}}} %requires amssym
+\newcommand{\isasymeight}{\isamath{\mathbf{8}}} %requires amssym
+\newcommand{\isasymnine}{\isamath{\mathbf{9}}}  %requires amssym
+\newcommand{\isasymA}{\isamath{\mathcal{A}}}
+\newcommand{\isasymB}{\isamath{\mathcal{B}}}
+\newcommand{\isasymC}{\isamath{\mathcal{C}}}
+\newcommand{\isasymD}{\isamath{\mathcal{D}}}
+\newcommand{\isasymE}{\isamath{\mathcal{E}}}
+\newcommand{\isasymF}{\isamath{\mathcal{F}}}
+\newcommand{\isasymG}{\isamath{\mathcal{G}}}
+\newcommand{\isasymH}{\isamath{\mathcal{H}}}
+\newcommand{\isasymI}{\isamath{\mathcal{I}}}
+\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
+\newcommand{\isasymK}{\isamath{\mathcal{K}}}
+\newcommand{\isasymL}{\isamath{\mathcal{L}}}
+\newcommand{\isasymM}{\isamath{\mathcal{M}}}
+\newcommand{\isasymN}{\isamath{\mathcal{N}}}
+\newcommand{\isasymO}{\isamath{\mathcal{O}}}
+\newcommand{\isasymP}{\isamath{\mathcal{P}}}
+\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
+\newcommand{\isasymR}{\isamath{\mathcal{R}}}
+\newcommand{\isasymS}{\isamath{\mathcal{S}}}
+\newcommand{\isasymT}{\isamath{\mathcal{T}}}
+\newcommand{\isasymU}{\isamath{\mathcal{U}}}
+\newcommand{\isasymV}{\isamath{\mathcal{V}}}
+\newcommand{\isasymW}{\isamath{\mathcal{W}}}
+\newcommand{\isasymX}{\isamath{\mathcal{X}}}
+\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
+\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
+\newcommand{\isasyma}{\isamath{\mathrm{a}}}
+\newcommand{\isasymb}{\isamath{\mathrm{b}}}
+\newcommand{\isasymc}{\isamath{\mathrm{c}}}
+\newcommand{\isasymd}{\isamath{\mathrm{d}}}
+\newcommand{\isasyme}{\isamath{\mathrm{e}}}
+\newcommand{\isasymf}{\isamath{\mathrm{f}}}
+\newcommand{\isasymg}{\isamath{\mathrm{g}}}
+\newcommand{\isasymh}{\isamath{\mathrm{h}}}
+\newcommand{\isasymi}{\isamath{\mathrm{i}}}
+\newcommand{\isasymj}{\isamath{\mathrm{j}}}
+\newcommand{\isasymk}{\isamath{\mathrm{k}}}
+\newcommand{\isasyml}{\isamath{\mathrm{l}}}
+\newcommand{\isasymm}{\isamath{\mathrm{m}}}
+\newcommand{\isasymn}{\isamath{\mathrm{n}}}
+\newcommand{\isasymo}{\isamath{\mathrm{o}}}
+\newcommand{\isasymp}{\isamath{\mathrm{p}}}
+\newcommand{\isasymq}{\isamath{\mathrm{q}}}
+\newcommand{\isasymr}{\isamath{\mathrm{r}}}
+\newcommand{\isasyms}{\isamath{\mathrm{s}}}
+\newcommand{\isasymt}{\isamath{\mathrm{t}}}
+\newcommand{\isasymu}{\isamath{\mathrm{u}}}
+\newcommand{\isasymv}{\isamath{\mathrm{v}}}
+\newcommand{\isasymw}{\isamath{\mathrm{w}}}
+\newcommand{\isasymx}{\isamath{\mathrm{x}}}
+\newcommand{\isasymy}{\isamath{\mathrm{y}}}
+\newcommand{\isasymz}{\isamath{\mathrm{z}}}
+\newcommand{\isasymAA}{\isamath{\mathfrak{A}}}  %requires eufrak
+\newcommand{\isasymBB}{\isamath{\mathfrak{B}}}  %requires eufrak
+\newcommand{\isasymCC}{\isamath{\mathfrak{C}}}  %requires eufrak
+\newcommand{\isasymDD}{\isamath{\mathfrak{D}}}  %requires eufrak
+\newcommand{\isasymEE}{\isamath{\mathfrak{E}}}  %requires eufrak
+\newcommand{\isasymFF}{\isamath{\mathfrak{F}}}  %requires eufrak
+\newcommand{\isasymGG}{\isamath{\mathfrak{G}}}  %requires eufrak
+\newcommand{\isasymHH}{\isamath{\mathfrak{H}}}  %requires eufrak
+\newcommand{\isasymII}{\isamath{\mathfrak{I}}}  %requires eufrak
+\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}}  %requires eufrak
+\newcommand{\isasymKK}{\isamath{\mathfrak{K}}}  %requires eufrak
+\newcommand{\isasymLL}{\isamath{\mathfrak{L}}}  %requires eufrak
+\newcommand{\isasymMM}{\isamath{\mathfrak{M}}}  %requires eufrak
+\newcommand{\isasymNN}{\isamath{\mathfrak{N}}}  %requires eufrak
+\newcommand{\isasymOO}{\isamath{\mathfrak{O}}}  %requires eufrak
+\newcommand{\isasymPP}{\isamath{\mathfrak{P}}}  %requires eufrak
+\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}}  %requires eufrak
+\newcommand{\isasymRR}{\isamath{\mathfrak{R}}}  %requires eufrak
+\newcommand{\isasymSS}{\isamath{\mathfrak{S}}}  %requires eufrak
+\newcommand{\isasymTT}{\isamath{\mathfrak{T}}}  %requires eufrak
+\newcommand{\isasymUU}{\isamath{\mathfrak{U}}}  %requires eufrak
+\newcommand{\isasymVV}{\isamath{\mathfrak{V}}}  %requires eufrak
+\newcommand{\isasymWW}{\isamath{\mathfrak{W}}}  %requires eufrak
+\newcommand{\isasymXX}{\isamath{\mathfrak{X}}}  %requires eufrak
+\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}}  %requires eufrak
+\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}}  %requires eufrak
+\newcommand{\isasymaa}{\isamath{\mathfrak{a}}}  %requires eufrak
+\newcommand{\isasymbb}{\isamath{\mathfrak{b}}}  %requires eufrak
+\newcommand{\isasymcc}{\isamath{\mathfrak{c}}}  %requires eufrak
+\newcommand{\isasymdd}{\isamath{\mathfrak{d}}}  %requires eufrak
+\newcommand{\isasymee}{\isamath{\mathfrak{e}}}  %requires eufrak
+\newcommand{\isasymff}{\isamath{\mathfrak{f}}}  %requires eufrak
+\newcommand{\isasymgg}{\isamath{\mathfrak{g}}}  %requires eufrak
+\newcommand{\isasymhh}{\isamath{\mathfrak{h}}}  %requires eufrak
+\newcommand{\isasymii}{\isamath{\mathfrak{i}}}  %requires eufrak
+\newcommand{\isasymjj}{\isamath{\mathfrak{j}}}  %requires eufrak
+\newcommand{\isasymkk}{\isamath{\mathfrak{k}}}  %requires eufrak
+\newcommand{\isasymll}{\isamath{\mathfrak{l}}}  %requires eufrak
+\newcommand{\isasymmm}{\isamath{\mathfrak{m}}}  %requires eufrak
+\newcommand{\isasymnn}{\isamath{\mathfrak{n}}}  %requires eufrak
+\newcommand{\isasymoo}{\isamath{\mathfrak{o}}}  %requires eufrak
+\newcommand{\isasympp}{\isamath{\mathfrak{p}}}  %requires eufrak
+\newcommand{\isasymqq}{\isamath{\mathfrak{q}}}  %requires eufrak
+\newcommand{\isasymrr}{\isamath{\mathfrak{r}}}  %requires eufrak
+\newcommand{\isasymss}{\isamath{\mathfrak{s}}}  %requires eufrak
+\newcommand{\isasymtt}{\isamath{\mathfrak{t}}}  %requires eufrak
+\newcommand{\isasymuu}{\isamath{\mathfrak{u}}}  %requires eufrak
+\newcommand{\isasymvv}{\isamath{\mathfrak{v}}}  %requires eufrak
+\newcommand{\isasymww}{\isamath{\mathfrak{w}}}  %requires eufrak
+\newcommand{\isasymxx}{\isamath{\mathfrak{x}}}  %requires eufrak
+\newcommand{\isasymyy}{\isamath{\mathfrak{y}}}  %requires eufrak
+\newcommand{\isasymzz}{\isamath{\mathfrak{z}}}  %requires eufrak
+\newcommand{\isasymalpha}{\isamath{\alpha}}
+\newcommand{\isasymbeta}{\isamath{\beta}}
+\newcommand{\isasymgamma}{\isamath{\gamma}}
+\newcommand{\isasymdelta}{\isamath{\delta}}
+\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
+\newcommand{\isasymzeta}{\isamath{\zeta}}
+\newcommand{\isasymeta}{\isamath{\eta}}
+\newcommand{\isasymtheta}{\isamath{\vartheta}}
+\newcommand{\isasymiota}{\isamath{\iota}}
+\newcommand{\isasymkappa}{\isamath{\kappa}}
+\newcommand{\isasymlambda}{\isamath{\lambda}}
+\newcommand{\isasymmu}{\isamath{\mu}}
+\newcommand{\isasymnu}{\isamath{\nu}}
+\newcommand{\isasymxi}{\isamath{\xi}}
+\newcommand{\isasympi}{\isamath{\pi}}
+\newcommand{\isasymrho}{\isamath{\varrho}}
+\newcommand{\isasymsigma}{\isamath{\sigma}}
+\newcommand{\isasymtau}{\isamath{\tau}}
+\newcommand{\isasymupsilon}{\isamath{\upsilon}}
+\newcommand{\isasymphi}{\isamath{\varphi}}
+\newcommand{\isasymchi}{\isamath{\chi}}
+\newcommand{\isasympsi}{\isamath{\psi}}
+\newcommand{\isasymomega}{\isamath{\omega}}
+\newcommand{\isasymGamma}{\isamath{\Gamma}}
+\newcommand{\isasymDelta}{\isamath{\Delta}}
+\newcommand{\isasymTheta}{\isamath{\Theta}}
+\newcommand{\isasymLambda}{\isamath{\Lambda}}
+\newcommand{\isasymXi}{\isamath{\Xi}}
+\newcommand{\isasymPi}{\isamath{\Pi}}
+\newcommand{\isasymSigma}{\isamath{\Sigma}}
+\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
+\newcommand{\isasymPhi}{\isamath{\Phi}}
+\newcommand{\isasymPsi}{\isamath{\Psi}}
+\newcommand{\isasymOmega}{\isamath{\Omega}}
+\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
+\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
+\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
+\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
+\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
+\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
+\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
+\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
+\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
+\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
+\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
+\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
+\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
+\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
+\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
+\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
+\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
+\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
+\newcommand{\isasymmapsto}{\isamath{\mapsto}}
+\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
+\newcommand{\isasymmidarrow}{\isamath{\relbar}}
+\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
+\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
+\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
+\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
+\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
+\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
+\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
+\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
+\newcommand{\isasymleadsto}{\isamath{\leadsto}}  %requires amssym
+\newcommand{\isasymup}{\isamath{\uparrow}}
+\newcommand{\isasymUp}{\isamath{\Uparrow}}
+\newcommand{\isasymdown}{\isamath{\downarrow}}
+\newcommand{\isasymDown}{\isamath{\Downarrow}}
+\newcommand{\isasymupdown}{\isamath{\updownarrow}}
+\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
+\newcommand{\isasymlangle}{\isamath{\langle}}
+\newcommand{\isasymrangle}{\isamath{\rangle}}
+\newcommand{\isasymlceil}{\isamath{\lceil}}
+\newcommand{\isasymrceil}{\isamath{\rceil}}
+\newcommand{\isasymlfloor}{\isamath{\lfloor}}
+\newcommand{\isasymrfloor}{\isamath{\rfloor}}
+\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
+\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
+\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
+\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
+\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
+\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
+\newcommand{\isasymguillemotleft}{\isatext{\flqq}}  %requires babel 
+\newcommand{\isasymguillemotright}{\isatext{\frqq}}  %requires babel 
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
+\newcommand{\isasymnot}{\isamath{\neg}}
+\newcommand{\isasymbottom}{\isamath{\bot}}
+\newcommand{\isasymtop}{\isamath{\top}}
+\newcommand{\isasymand}{\isamath{\wedge}}
+\newcommand{\isasymAnd}{\isamath{\bigwedge}}
+\newcommand{\isasymor}{\isamath{\vee}}
+\newcommand{\isasymOr}{\isamath{\bigvee}}
+\newcommand{\isasymforall}{\isamath{\forall\,}}
+\newcommand{\isasymexists}{\isamath{\exists\,}}
+\newcommand{\isasymbox}{\isamath{\Box}}  %requires amssym
+\newcommand{\isasymdiamond}{\isamath{\Diamond}}  %requires amssym
+\newcommand{\isasymturnstile}{\isamath{\vdash}}
+\newcommand{\isasymTurnstile}{\isamath{\models}}
+\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
+\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
+\newcommand{\isasymstileturn}{\isamath{\dashv}}
+\newcommand{\isasymsurd}{\isamath{\surd}}
+\newcommand{\isasymle}{\isamath{\le}}
+\newcommand{\isasymge}{\isamath{\ge}}
+\newcommand{\isasymlless}{\isamath{\ll}}
+\newcommand{\isasymggreater}{\isamath{\gg}}
+\newcommand{\isasymlesssim}{\isamath{\lesssim}}  %requires amssymb
+\newcommand{\isasymgreatersim}{\isamath{\gtrsim}}  %requires amssymb
+\newcommand{\isasymlessapprox}{\isamath{\lessapprox}}  %requires amssymb
+\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}}  %requires amssymb
+\newcommand{\isasymin}{\isamath{\in}}
+\newcommand{\isasymnotin}{\isamath{\notin}}
+\newcommand{\isasymsubset}{\isamath{\subset}}
+\newcommand{\isasymsupset}{\isamath{\supset}}
+\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
+\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
+\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}
+\newcommand{\isasymsqsupset}{\isamath{\sqsupset}}  %requires amssym
+\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
+\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
+\newcommand{\isasyminter}{\isamath{\cap}}
+\newcommand{\isasymInter}{\isamath{\bigcap\,}}
+\newcommand{\isasymunion}{\isamath{\cup}}
+\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
+\newcommand{\isasymsqunion}{\isamath{\sqcup}}
+\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
+\newcommand{\isasymsqinter}{\isamath{\sqcap}}
+\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}}  %requires masmath
+\newcommand{\isasymuplus}{\isamath{\uplus}}
+\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
+\newcommand{\isasymnoteq}{\isamath{\not=}}
+\newcommand{\isasymsim}{\isamath{\sim}}
+\newcommand{\isasymdoteq}{\isamath{\doteq}}
+\newcommand{\isasymsimeq}{\isamath{\simeq}}
+\newcommand{\isasymapprox}{\isamath{\approx}}
+\newcommand{\isasymasymp}{\isamath{\asymp}}
+\newcommand{\isasymcong}{\isamath{\cong}}
+\newcommand{\isasymsmile}{\isamath{\smile}}
+\newcommand{\isasymequiv}{\isamath{\equiv}}
+\newcommand{\isasymfrown}{\isamath{\frown}}
+\newcommand{\isasympropto}{\isamath{\propto}}
+\newcommand{\isasymbowtie}{\isamath{\bowtie}}
+\newcommand{\isasymprec}{\isamath{\prec}}
+\newcommand{\isasymsucc}{\isamath{\succ}}
+\newcommand{\isasympreceq}{\isamath{\preceq}}
+\newcommand{\isasymsucceq}{\isamath{\succeq}}
+\newcommand{\isasymparallel}{\isamath{\parallel}}
+\newcommand{\isasymbar}{\isamath{\mid}}
+\newcommand{\isasymplusminus}{\isamath{\pm}}
+\newcommand{\isasymminusplus}{\isamath{\mp}}
+\newcommand{\isasymtimes}{\isamath{\times}}
+\newcommand{\isasymdiv}{\isamath{\div}}
+\newcommand{\isasymcdot}{\isamath{\cdot}}
+\newcommand{\isasymstar}{\isamath{\star}}
+\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
+\newcommand{\isasymcirc}{\isamath{\circ}}
+\newcommand{\isasymdagger}{\isamath{\dagger}}
+\newcommand{\isasymddagger}{\isamath{\ddagger}}
+\newcommand{\isasymlhd}{\isamath{\lhd}}
+\newcommand{\isasymrhd}{\isamath{\rhd}}
+\newcommand{\isasymunlhd}{\isamath{\unlhd}}
+\newcommand{\isasymunrhd}{\isamath{\unrhd}}
+\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
+\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
+\newcommand{\isasymtriangle}{\isamath{\triangle}}
+\newcommand{\isasymtriangleq}{\isamath{\triangleq}}  %requires amssymb
+\newcommand{\isasymoplus}{\isamath{\oplus}}
+\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
+\newcommand{\isasymotimes}{\isamath{\otimes}}
+\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
+\newcommand{\isasymodot}{\isamath{\odot}}
+\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
+\newcommand{\isasymominus}{\isamath{\ominus}}
+\newcommand{\isasymoslash}{\isamath{\oslash}}
+\newcommand{\isasymdots}{\isamath{\dots}}
+\newcommand{\isasymcdots}{\isamath{\cdots}}
+\newcommand{\isasymSum}{\isamath{\sum\,}}
+\newcommand{\isasymProd}{\isamath{\prod\,}}
+\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
+\newcommand{\isasyminfinity}{\isamath{\infty}}
+\newcommand{\isasymintegral}{\isamath{\int\,}}
+\newcommand{\isasymointegral}{\isamath{\oint\,}}
+\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
+\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
+\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
+\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
+\newcommand{\isasymaleph}{\isamath{\aleph}}
+\newcommand{\isasymemptyset}{\isamath{\emptyset}}
+\newcommand{\isasymnabla}{\isamath{\nabla}}
+\newcommand{\isasympartial}{\isamath{\partial}}
+\newcommand{\isasymRe}{\isamath{\Re}}
+\newcommand{\isasymIm}{\isamath{\Im}}
+\newcommand{\isasymflat}{\isamath{\flat}}
+\newcommand{\isasymnatural}{\isamath{\natural}}
+\newcommand{\isasymsharp}{\isamath{\sharp}}
+\newcommand{\isasymangle}{\isamath{\angle}}
+\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
+\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
+\newcommand{\isasymhyphen}{\isatext{\rm-}}
+\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
+\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}}  %requires latin1
+\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}}  %requires latin1
+\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}}  %requires latin1
+\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}}  %requires latin1
+\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}}  %requires latin1
+\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}}  %requires latin1
+\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
+\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
+\newcommand{\isasymsection}{\isatext{\rm\S}}
+\newcommand{\isasymparagraph}{\isatext{\rm\P}}
+\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
+\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
+\newcommand{\isasymeuro}{\isatext{\textgreek{\euro}}}  %requires greek babel
+\newcommand{\isasympounds}{\isamath{\pounds}}
+\newcommand{\isasymyen}{\isatext{\yen}}  %requires amssymb
+\newcommand{\isasymcent}{\isatext{\textcent}}  %requires textcomp
+\newcommand{\isasymcurrency}{\isatext{\textcurrency}} %requires textcomp
+\newcommand{\isasymdegree}{\isatext{\rm\textdegree}}  %requires latin1
+\newcommand{\isasymamalg}{\isamath{\amalg}}
+\newcommand{\isasymmho}{\isamath{\mho}}  %requires amssym
+\newcommand{\isasymlozenge}{\isamath{\lozenge}}  %requires amssym
+\newcommand{\isasymJoin}{\isamath{\Join}}  %requires amssym
+\newcommand{\isasymwp}{\isamath{\wp}}
+\newcommand{\isasymwrong}{\isamath{\wr}}
+\newcommand{\isasymstruct}{\isamath{\diamond}}
+\newcommand{\isasymacute}{\isatext{\'\relax}}
+\newcommand{\isasymindex}{\isatext{\i}}
+\newcommand{\isasymdieresis}{\isatext{\"\relax}}
+\newcommand{\isasymcedilla}{\isatext{\c\relax}}
+\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
+\newcommand{\isasymspacespace}{\isamath{~~}}