Inserted some extra paragraphs in large proofs to make tex run...
authorschirmer
Fri Nov 01 13:16:28 2002 +0100 (2002-11-01)
changeset 13690ac335b2f4a39
parent 13689 3d4ad560b2ff
child 13691 a6bc3001106a
Inserted some extra paragraphs in large proofs to make tex run...
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxSound.thy
src/HOL/Bali/DefiniteAssignmentCorrect.thy
src/HOL/Bali/Evaln.thy
src/HOL/Bali/Term.thy
src/HOL/Bali/TypeSafe.thy
     1.1 --- a/src/HOL/Bali/AxCompl.thy	Fri Nov 01 10:35:50 2002 +0100
     1.2 +++ b/src/HOL/Bali/AxCompl.thy	Fri Nov 01 13:16:28 2002 +0100
     1.3 @@ -1047,15 +1047,6 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -(* To term *)
     1.8 -lemma term_cases: "
     1.9 -  \<lbrakk>\<And> v. P \<langle>v\<rangle>\<^sub>v; \<And> e. P \<langle>e\<rangle>\<^sub>e;\<And> c. P \<langle>c\<rangle>\<^sub>s;\<And> l. P \<langle>l\<rangle>\<^sub>l\<rbrakk>
    1.10 -  \<Longrightarrow> P t"
    1.11 -  apply (cases t)
    1.12 -  apply (case_tac a)
    1.13 -  apply auto
    1.14 -  done
    1.15 -
    1.16  lemma MGFn_lemma:
    1.17    assumes mgf_methds: 
    1.18             "\<And> n. \<forall> C sig. G,(A::state triple set)\<turnstile>{=:n} \<langle>Methd C sig\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
    1.19 @@ -1243,6 +1234,10 @@
    1.20        show "G,A\<turnstile>{=:n} \<langle>Methd D mn\<rangle>\<^sub>e\<succ> {G\<rightarrow>}"
    1.21  	by simp
    1.22      next
    1.23 +-- {* 
    1.24 +\par
    1.25 +*} (* dummy text command to break paragraph for latex;
    1.26 +              large paragraphs exhaust memory of debian pdflatex *)
    1.27        case (Body D c)
    1.28        have mgf_c: "G,A\<turnstile>{=:n} \<langle>c\<rangle>\<^sub>s\<succ> {G\<rightarrow>}" .
    1.29        from wf MGFn_Init [OF hyp] mgf_c
     2.1 --- a/src/HOL/Bali/AxSound.thy	Fri Nov 01 10:35:50 2002 +0100
     2.2 +++ b/src/HOL/Bali/AxSound.thy	Fri Nov 01 13:16:28 2002 +0100
     2.3 @@ -569,7 +569,11 @@
     2.4        ultimately show ?thesis using Q by simp
     2.5      qed
     2.6    qed
     2.7 -next   
     2.8 +next
     2.9 +-- {* 
    2.10 +\par
    2.11 +*} (* dummy text command to break paragraph for latex;
    2.12 +              large paragraphs exhaust memory of debian pdflatex *)   
    2.13    case (AVar A P Q R e1 e2)
    2.14    have valid_e1: "G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }" .
    2.15    have valid_e2: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} e2-\<succ> {\<lambda>Val:i:. avar G i a ..; R} }"
    2.16 @@ -879,6 +883,10 @@
    2.17      qed
    2.18    qed
    2.19  next
    2.20 +-- {* 
    2.21 +\par
    2.22 +*} (* dummy text command to break paragraph for latex;
    2.23 +              large paragraphs exhaust memory of debian pdflatex *)
    2.24    case (BinOp A P Q R binop e1 e2)
    2.25    assume valid_e1: "G,A|\<Turnstile>\<Colon>{ {Normal P} e1-\<succ> {Q} }" 
    2.26    have valid_e2: "\<And> v1.  G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 v1}
    2.27 @@ -1216,6 +1224,10 @@
    2.28      qed
    2.29    qed
    2.30  next
    2.31 +-- {* 
    2.32 +\par
    2.33 +*} (* dummy text command to break paragraph for latex;
    2.34 +              large paragraphs exhaust memory of debian pdflatex *)
    2.35    case (Call A P Q R S accC' args e mn mode pTs' statT)
    2.36    have valid_e: "G,A|\<Turnstile>\<Colon>{ {Normal P} e-\<succ> {Q} }" .
    2.37    have valid_args: "\<And> a. G,A|\<Turnstile>\<Colon>{ {Q\<leftarrow>In1 a} args\<doteq>\<succ> {R a} }"
    2.38 @@ -1799,6 +1811,10 @@
    2.39      qed
    2.40    qed
    2.41  next
    2.42 +-- {* 
    2.43 +\par
    2.44 +*} (* dummy text command to break paragraph for latex;
    2.45 +              large paragraphs exhaust memory of debian pdflatex *)
    2.46    case (Lab A P Q c l)
    2.47    have valid_c: "G,A|\<Turnstile>\<Colon>{ {Normal P} .c. {abupd (absorb l) .; Q} }".
    2.48    show "G,A|\<Turnstile>\<Colon>{ {Normal P} .l\<bullet> c. {Q} }"
    2.49 @@ -2202,6 +2218,10 @@
    2.50      qed
    2.51    qed
    2.52  next
    2.53 +-- {* 
    2.54 +\par
    2.55 +*} (* dummy text command to break paragraph for latex;
    2.56 +              large paragraphs exhaust memory of debian pdflatex *)
    2.57    case (Jmp A P j)
    2.58    show "G,A|\<Turnstile>\<Colon>{ {Normal (abupd (\<lambda>a. Some (Jump j)) .; P\<leftarrow>\<diamondsuit>)} .Jmp j. {P} }"
    2.59    proof (rule valid_stmt_NormalI)
    2.60 @@ -2473,6 +2493,10 @@
    2.61      qed
    2.62    qed
    2.63  next
    2.64 +-- {* 
    2.65 +\par
    2.66 +*} (* dummy text command to break paragraph for latex;
    2.67 +              large paragraphs exhaust memory of debian pdflatex *)
    2.68    case (Done A C P)
    2.69    show "G,A|\<Turnstile>\<Colon>{ {Normal (P\<leftarrow>\<diamondsuit> \<and>. initd C)} .Init C. {P} }" 
    2.70    proof (rule valid_stmt_NormalI)
     3.1 --- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Nov 01 10:35:50 2002 +0100
     3.2 +++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Fri Nov 01 13:16:28 2002 +0100
     3.3 @@ -2829,6 +2829,10 @@
     3.4        ultimately show ?thesis by (intro conjI)
     3.5      qed
     3.6    next
     3.7 +-- {* 
     3.8 +\par
     3.9 +*} (* dummy text command to break paragraph for latex;
    3.10 +              large paragraphs exhaust memory of debian pdflatex *)
    3.11      case (If b c1 c2 e s0 s1 s2 Env T A)
    3.12      have G: "prg Env = G" .
    3.13      with If.hyps have eval_e: "prg Env \<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" by simp
    3.14 @@ -3325,6 +3329,10 @@
    3.15        qed
    3.16      qed
    3.17    next
    3.18 +-- {* 
    3.19 +\par
    3.20 +*} (* dummy text command to break paragraph for latex;
    3.21 +              large paragraphs exhaust memory of debian pdflatex *)
    3.22      case (Fin c1 c2 s0 s1 s2 s3 x1 Env T A)
    3.23      have G: "prg Env = G" .
    3.24      from Fin.prems obtain C1 C2 where 
    3.25 @@ -3580,6 +3588,10 @@
    3.26        by simp_all      
    3.27      ultimately show ?case by (intro conjI)
    3.28    next
    3.29 +-- {* 
    3.30 +\par
    3.31 +*} (* dummy text command to break paragraph for latex;
    3.32 +              large paragraphs exhaust memory of debian pdflatex *)
    3.33      case (NewA elT a e i s0 s1 s2 s3 Env T A) 
    3.34      have G: "prg Env = G" .
    3.35      from NewA.prems obtain
    3.36 @@ -3881,6 +3893,10 @@
    3.37        by simp_all
    3.38      ultimately show ?case by (intro conjI) 
    3.39    next
    3.40 +-- {* 
    3.41 +\par
    3.42 +*} (* dummy text command to break paragraph for latex;
    3.43 +              large paragraphs exhaust memory of debian pdflatex *)
    3.44      case (Super s Env T A)
    3.45      from Super.prems
    3.46      have "nrm A = dom (locals (store ((Norm s)::state)))"
    3.47 @@ -4271,6 +4287,10 @@
    3.48        by simp_all
    3.49      ultimately show ?case by (intro conjI)
    3.50    next
    3.51 +-- {* 
    3.52 +\par
    3.53 +*} (* dummy text command to break paragraph for latex;
    3.54 +              large paragraphs exhaust memory of debian pdflatex *)
    3.55      case (LVar s vn Env T A)
    3.56      from LVar.prems
    3.57      have "nrm A = dom (locals (store ((Norm s)::state)))"
     4.1 --- a/src/HOL/Bali/Evaln.thy	Fri Nov 01 10:35:50 2002 +0100
     4.2 +++ b/src/HOL/Bali/Evaln.thy	Fri Nov 01 13:16:28 2002 +0100
     4.3 @@ -743,6 +743,10 @@
     4.4      by (rule evaln.Super)
     4.5    then show ?case ..
     4.6  next
     4.7 +-- {* 
     4.8 +\par
     4.9 +*} (* dummy text command to break paragraph for latex;
    4.10 +              large paragraphs exhaust memory of debian pdflatex *)
    4.11    case (Acc f s0 s1 v va)
    4.12    then obtain n where
    4.13      "G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v, f)\<midarrow>n\<rightarrow> s1"
     5.1 --- a/src/HOL/Bali/Term.thy	Fri Nov 01 10:35:50 2002 +0100
     5.2 +++ b/src/HOL/Bali/Term.thy	Fri Nov 01 13:16:28 2002 +0100
     5.3 @@ -383,6 +383,14 @@
     5.4  lemma elist_var_inj_term [iff]: "\<langle>t::expr list\<rangle> \<noteq> \<langle>w::var\<rangle>"
     5.5    by (simp add: inj_term_simps)
     5.6  
     5.7 +lemma term_cases: "
     5.8 +  \<lbrakk>\<And> v. P \<langle>v\<rangle>\<^sub>v; \<And> e. P \<langle>e\<rangle>\<^sub>e;\<And> c. P \<langle>c\<rangle>\<^sub>s;\<And> l. P \<langle>l\<rangle>\<^sub>l\<rbrakk>
     5.9 +  \<Longrightarrow> P t"
    5.10 +  apply (cases t)
    5.11 +  apply (case_tac a)
    5.12 +  apply auto
    5.13 +  done
    5.14 +
    5.15  section {* Evaluation of unary operations *}
    5.16  consts eval_unop :: "unop \<Rightarrow> val \<Rightarrow> val"
    5.17  primrec
     6.1 --- a/src/HOL/Bali/TypeSafe.thy	Fri Nov 01 10:35:50 2002 +0100
     6.2 +++ b/src/HOL/Bali/TypeSafe.thy	Fri Nov 01 13:16:28 2002 +0100
     6.3 @@ -1938,6 +1938,10 @@
     6.4            a boolean value is part of @{term hyp_e}. See also Loop 
     6.5         *}
     6.6    next
     6.7 +-- {* 
     6.8 +\par
     6.9 +*} (* dummy text command to break paragraph for latex;
    6.10 +              large paragraphs exhaust memory of debian pdflatex *)
    6.11      case (Loop b c e l s0 s1 s2 s3 L accC T A)
    6.12      have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1" .
    6.13      have hyp_e: "PROP ?TypeSafe (Norm s0) s1 (In1l e) (In1 b)" .
    6.14 @@ -2228,6 +2232,10 @@
    6.15        qed
    6.16      qed
    6.17    next
    6.18 +-- {* 
    6.19 +\par
    6.20 +*} (* dummy text command to break paragraph for latex;
    6.21 +              large paragraphs exhaust memory of debian pdflatex *)
    6.22      case (Fin c1 c2 s0 s1 s2 s3 x1 L accC T A)
    6.23      have eval_c1: "G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1, s1)" .
    6.24      have eval_c2: "G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2" .
    6.25 @@ -2506,6 +2514,10 @@
    6.26            (error_free (Norm s0) = error_free s3) "
    6.27        by simp
    6.28    next
    6.29 +-- {* 
    6.30 +\par
    6.31 +*} (* dummy text command to break paragraph for latex;
    6.32 +              large paragraphs exhaust memory of debian pdflatex *)
    6.33      case (Cast castT e s0 s1 s2 v L accC T A)
    6.34      have "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
    6.35      have s2:"s2 = abupd (raise_if (\<not> G,store s1\<turnstile>v fits castT) ClassCast) s1" .
    6.36 @@ -2719,6 +2731,10 @@
    6.37             (error_free (Norm s) = error_free (Norm s))"
    6.38        by simp
    6.39    next
    6.40 +-- {* 
    6.41 +\par
    6.42 +*} (* dummy text command to break paragraph for latex;
    6.43 +              large paragraphs exhaust memory of debian pdflatex *)
    6.44      case (Acc upd s0 s1 w v L accC T A) 
    6.45      have hyp: "PROP ?TypeSafe (Norm s0) s1 (In2 v) (In2 (w,upd))" .
    6.46      have conf_s0: "Norm s0\<Colon>\<preceq>(G, L)" .
    6.47 @@ -3342,6 +3358,10 @@
    6.48        qed
    6.49      qed
    6.50    next
    6.51 +-- {* 
    6.52 +\par
    6.53 +*} (* dummy text command to break paragraph for latex;
    6.54 +              large paragraphs exhaust memory of debian pdflatex *)
    6.55      case (Methd D s0 s1 sig v L accC T A)
    6.56      have "G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1" .
    6.57      have hyp:"PROP ?TypeSafe (Norm s0) s1 (In1l (body G D sig)) (In1 v)" .
    6.58 @@ -3707,6 +3727,10 @@
    6.59      then show ?case
    6.60        by (auto elim!: wt_elim_cases)
    6.61    next
    6.62 +-- {* 
    6.63 +\par
    6.64 +*} (* dummy text command to break paragraph for latex;
    6.65 +              large paragraphs exhaust memory of debian pdflatex *)
    6.66      case (Cons e es s0 s1 s2 v vs L accC T A)
    6.67      have eval_e: "G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1" .
    6.68      have eval_es: "G\<turnstile>s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2" .