--- a/src/HOL/Induct/ABexp.thy Sat Jun 20 15:43:36 2015 +0200
+++ b/src/HOL/Induct/ABexp.thy Sat Jun 20 15:45:02 2015 +0200
@@ -2,7 +2,7 @@
Author: Stefan Berghofer, TU Muenchen
*)
-section {* Arithmetic and boolean expressions *}
+section \<open>Arithmetic and boolean expressions\<close>
theory ABexp
imports Main
@@ -20,7 +20,7 @@
| Neg "'a bexp"
-text {* \medskip Evaluation of arithmetic and boolean expressions *}
+text \<open>\medskip Evaluation of arithmetic and boolean expressions\<close>
primrec evala :: "('a => nat) => 'a aexp => nat"
and evalb :: "('a => nat) => 'a bexp => bool"
@@ -36,7 +36,7 @@
| "evalb env (Neg b) = (\<not> evalb env b)"
-text {* \medskip Substitution on arithmetic and boolean expressions *}
+text \<open>\medskip Substitution on arithmetic and boolean expressions\<close>
primrec substa :: "('a => 'b aexp) => 'a aexp => 'b aexp"
and substb :: "('a => 'b aexp) => 'a bexp => 'b bexp"
@@ -55,7 +55,7 @@
"evala env (substa (Var (v := a')) a) = evala (env (v := evala env a')) a"
and subst1_bexp:
"evalb env (substb (Var (v := a')) b) = evalb (env (v := evala env a')) b"
- -- {* one variable *}
+ -- \<open>one variable\<close>
by (induct a and b) simp_all
lemma subst_all_aexp:
--- a/src/HOL/Induct/Com.thy Sat Jun 20 15:43:36 2015 +0200
+++ b/src/HOL/Induct/Com.thy Sat Jun 20 15:45:02 2015 +0200
@@ -5,7 +5,7 @@
Example of Mutual Induction via Iteratived Inductive Definitions: Commands
*)
-section{*Mutual Induction via Iteratived Inductive Definitions*}
+section\<open>Mutual Induction via Iteratived Inductive Definitions\<close>
theory Com imports Main begin
@@ -25,15 +25,15 @@
| While exp com ("WHILE _ DO _" 60)
-subsection {* Commands *}
+subsection \<open>Commands\<close>
-text{* Execution of commands *}
+text\<open>Execution of commands\<close>
abbreviation (input)
generic_rel ("_/ -|[_]-> _" [50,0,50] 50) where
"esig -|[eval]-> ns == (esig,ns) \<in> eval"
-text{*Command execution. Natural numbers represent Booleans: 0=True, 1=False*}
+text\<open>Command execution. Natural numbers represent Booleans: 0=True, 1=False\<close>
inductive_set
exec :: "((exp*state) * (nat*state)) set => ((com*state)*state)set"
@@ -74,7 +74,7 @@
and exec_WHILE_case: "(WHILE b DO c,s) -[eval]-> t"
-text{*Justifies using "exec" in the inductive definition of "eval"*}
+text\<open>Justifies using "exec" in the inductive definition of "eval"\<close>
lemma exec_mono: "A<=B ==> exec(A) <= exec(B)"
apply (rule subsetI)
apply (simp add: split_paired_all)
@@ -92,7 +92,7 @@
unfolding subset_eq
by (auto simp add: le_fun_def)
-text{*Command execution is functional (deterministic) provided evaluation is*}
+text\<open>Command execution is functional (deterministic) provided evaluation is\<close>
theorem single_valued_exec: "single_valued ev ==> single_valued(exec ev)"
apply (simp add: single_valued_def)
apply (intro allI)
@@ -102,9 +102,9 @@
done
-subsection {* Expressions *}
+subsection \<open>Expressions\<close>
-text{* Evaluation of arithmetic expressions *}
+text\<open>Evaluation of arithmetic expressions\<close>
inductive_set
eval :: "((exp*state) * (nat*state)) set"
@@ -136,13 +136,13 @@
by (rule fun_upd_same [THEN subst]) fast
-text{* Make the induction rule look nicer -- though @{text eta_contract} makes the new
- version look worse than it is...*}
+text\<open>Make the induction rule look nicer -- though @{text eta_contract} makes the new
+ version look worse than it is...\<close>
lemma split_lemma: "{((e,s),(n,s')). P e s n s'} = Collect (split (%v. split (split P v)))"
by auto
-text{*New induction rule. Note the form of the VALOF induction hypothesis*}
+text\<open>New induction rule. Note the form of the VALOF induction hypothesis\<close>
lemma eval_induct
[case_names N X Op valOf, consumes 1, induct set: eval]:
"[| (e,s) -|-> (n,s');
@@ -167,12 +167,12 @@
done
-text{*Lemma for @{text Function_eval}. The major premise is that @{text "(c,s)"} executes to @{text "s1"}
+text\<open>Lemma for @{text Function_eval}. The major premise is that @{text "(c,s)"} executes to @{text "s1"}
using eval restricted to its functional part. Note that the execution
@{text "(c,s) -[eval]-> s2"} can use unrestricted @{text eval}! The reason is that
the execution @{text "(c,s) -[eval Int {...}]-> s1"} assures us that execution is
functional on the argument @{text "(c,s)"}.
-*}
+\<close>
lemma com_Unique:
"(c,s) -[eval Int {((e,s),(n,t)). \<forall>nt'. (e,s) -|-> nt' --> (n,t)=nt'}]-> s1
==> \<forall>s2. (c,s) -[eval]-> s2 --> s2=s1"
@@ -190,7 +190,7 @@
done
-text{*Expression evaluation is functional, or deterministic*}
+text\<open>Expression evaluation is functional, or deterministic\<close>
theorem single_valued_eval: "single_valued eval"
apply (unfold single_valued_def)
apply (intro allI, rule impI)
@@ -204,14 +204,14 @@
lemma eval_N_E [dest!]: "(N n, s) -|-> (v, s') ==> (v = n & s' = s)"
by (induct e == "N n" s v s' set: eval) simp_all
-text{*This theorem says that "WHILE TRUE DO c" cannot terminate*}
+text\<open>This theorem says that "WHILE TRUE DO c" cannot terminate\<close>
lemma while_true_E:
"(c', s) -[eval]-> t ==> c' = WHILE (N 0) DO c ==> False"
by (induct set: exec) auto
-subsection{* Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and
- WHILE e DO c *}
+subsection\<open>Equivalence of IF e THEN c;;(WHILE e DO c) ELSE SKIP and
+ WHILE e DO c\<close>
lemma while_if1:
"(c',s) -[eval]-> t
@@ -233,8 +233,8 @@
-subsection{* Equivalence of (IF e THEN c1 ELSE c2);;c
- and IF e THEN (c1;;c) ELSE (c2;;c) *}
+subsection\<open>Equivalence of (IF e THEN c1 ELSE c2);;c
+ and IF e THEN (c1;;c) ELSE (c2;;c)\<close>
lemma if_semi1:
"(c',s) -[eval]-> t
@@ -254,9 +254,9 @@
-subsection{* Equivalence of VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
+subsection\<open>Equivalence of VALOF c1 RESULTIS (VALOF c2 RESULTIS e)
and VALOF c1;;c2 RESULTIS e
- *}
+\<close>
lemma valof_valof1:
"(e',s) -|-> (v,s')
@@ -276,7 +276,7 @@
by (blast intro: valof_valof1 valof_valof2)
-subsection{* Equivalence of VALOF SKIP RESULTIS e and e *}
+subsection\<open>Equivalence of VALOF SKIP RESULTIS e and e\<close>
lemma valof_skip1:
"(e',s) -|-> (v,s')
@@ -293,7 +293,7 @@
by (blast intro: valof_skip1 valof_skip2)
-subsection{* Equivalence of VALOF x:=e RESULTIS x and e *}
+subsection\<open>Equivalence of VALOF x:=e RESULTIS x and e\<close>
lemma valof_assign1:
"(e',s) -|-> (v,s'')
--- a/src/HOL/Induct/Comb.thy Sat Jun 20 15:43:36 2015 +0200
+++ b/src/HOL/Induct/Comb.thy Sat Jun 20 15:45:02 2015 +0200
@@ -3,22 +3,22 @@
Copyright 1996 University of Cambridge
*)
-section {* Combinatory Logic example: the Church-Rosser Theorem *}
+section \<open>Combinatory Logic example: the Church-Rosser Theorem\<close>
theory Comb imports Main begin
-text {*
+text \<open>
Curiously, combinators do not include free variables.
Example taken from @{cite camilleri92}.
HOL system proofs may be found in the HOL distribution at
.../contrib/rule-induction/cl.ml
-*}
+\<close>
-subsection {* Definitions *}
+subsection \<open>Definitions\<close>
-text {* Datatype definition of combinators @{text S} and @{text K}. *}
+text \<open>Datatype definition of combinators @{text S} and @{text K}.\<close>
datatype comb = K
| S
@@ -28,10 +28,10 @@
Ap (infixl "\<bullet>" 90)
-text {*
+text \<open>
Inductive definition of contractions, @{text "-1->"} and
(multi-step) reductions, @{text "--->"}.
-*}
+\<close>
inductive_set
contract :: "(comb*comb) set"
@@ -47,10 +47,10 @@
contract_rel :: "[comb,comb] => bool" (infixl "--->" 50) where
"x ---> y == (x,y) \<in> contract^*"
-text {*
+text \<open>
Inductive definition of parallel contractions, @{text "=1=>"} and
(multi-step) parallel reductions, @{text "===>"}.
-*}
+\<close>
inductive_set
parcontract :: "(comb*comb) set"
@@ -66,9 +66,9 @@
parcontract_rel :: "[comb,comb] => bool" (infixl "===>" 50) where
"x ===> y == (x,y) \<in> parcontract^*"
-text {*
+text \<open>
Misc definitions.
-*}
+\<close>
definition
I :: comb where
@@ -76,18 +76,18 @@
definition
diamond :: "('a * 'a)set => bool" where
- --{*confluence; Lambda/Commutation treats this more abstractly*}
+ --\<open>confluence; Lambda/Commutation treats this more abstractly\<close>
"diamond(r) = (\<forall>x y. (x,y) \<in> r -->
(\<forall>y'. (x,y') \<in> r -->
(\<exists>z. (y,z) \<in> r & (y',z) \<in> r)))"
-subsection {*Reflexive/Transitive closure preserves Church-Rosser property*}
+subsection \<open>Reflexive/Transitive closure preserves Church-Rosser property\<close>
-text{*So does the Transitive closure, with a similar proof*}
+text\<open>So does the Transitive closure, with a similar proof\<close>
-text{*Strip lemma.
- The induction hypothesis covers all but the last diamond of the strip.*}
+text\<open>Strip lemma.
+ The induction hypothesis covers all but the last diamond of the strip.\<close>
lemma diamond_strip_lemmaE [rule_format]:
"[| diamond(r); (x,y) \<in> r^* |] ==>
\<forall>y'. (x,y') \<in> r --> (\<exists>z. (y',z) \<in> r^* & (y,z) \<in> r)"
@@ -105,9 +105,9 @@
done
-subsection {* Non-contraction results *}
+subsection \<open>Non-contraction results\<close>
-text {* Derive a case for each combinator constructor. *}
+text \<open>Derive a case for each combinator constructor.\<close>
inductive_cases
K_contractE [elim!]: "K -1-> r"
@@ -133,15 +133,15 @@
apply (blast intro: rtrancl_trans)+
done
-text {*Counterexample to the diamond property for @{term "x -1-> y"}*}
+text \<open>Counterexample to the diamond property for @{term "x -1-> y"}\<close>
lemma not_diamond_contract: "~ diamond(contract)"
by (unfold diamond_def, metis S_contractE contract.K)
-subsection {* Results about Parallel Contraction *}
+subsection \<open>Results about Parallel Contraction\<close>
-text {* Derive a case for each combinator constructor. *}
+text \<open>Derive a case for each combinator constructor.\<close>
inductive_cases
K_parcontractE [elim!]: "K =1=> r"
@@ -152,7 +152,7 @@
(*** Basic properties of parallel contraction ***)
-subsection {* Basic properties of parallel contraction *}
+subsection \<open>Basic properties of parallel contraction\<close>
lemma K1_parcontractD [dest!]: "K##x =1=> z ==> (\<exists>x'. z = K##x' & x =1=> x')"
by blast
@@ -164,24 +164,24 @@
"S##x##y =1=> z ==> (\<exists>x' y'. z = S##x'##y' & x =1=> x' & y =1=> y')"
by blast
-text{*The rules above are not essential but make proofs much faster*}
+text\<open>The rules above are not essential but make proofs much faster\<close>
-text{*Church-Rosser property for parallel contraction*}
+text\<open>Church-Rosser property for parallel contraction\<close>
lemma diamond_parcontract: "diamond parcontract"
apply (unfold diamond_def)
apply (rule impI [THEN allI, THEN allI])
apply (erule parcontract.induct, fast+)
done
-text {*
+text \<open>
\medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}.
-*}
+\<close>
lemma contract_subset_parcontract: "contract <= parcontract"
by (auto, erule contract.induct, blast+)
-text{*Reductions: simply throw together reflexivity, transitivity and
- the one-step reductions*}
+text\<open>Reductions: simply throw together reflexivity, transitivity and
+ the one-step reductions\<close>
declare r_into_rtrancl [intro] rtrancl_trans [intro]
--- a/src/HOL/Induct/Common_Patterns.thy Sat Jun 20 15:43:36 2015 +0200
+++ b/src/HOL/Induct/Common_Patterns.thy Sat Jun 20 15:45:02 2015 +0200
@@ -2,13 +2,13 @@
Author: Makarius
*)
-section {* Common patterns of induction *}
+section \<open>Common patterns of induction\<close>
theory Common_Patterns
imports Main
begin
-text {*
+text \<open>
The subsequent Isar proof schemes illustrate common proof patterns
supported by the generic @{text "induct"} method.
@@ -19,80 +19,80 @@
several rules. Working with inductive predicates is similar, but
involves explicit facts about membership, instead of implicit
syntactic typing.
-*}
+\<close>
-subsection {* Variations on statement structure *}
+subsection \<open>Variations on statement structure\<close>
-subsubsection {* Local facts and parameters *}
+subsubsection \<open>Local facts and parameters\<close>
-text {*
+text \<open>
Augmenting a problem by additional facts and locally fixed variables
is a bread-and-butter method in many applications. This is where
unwieldy object-level @{text "\<forall>"} and @{text "\<longrightarrow>"} used to occur in
the past. The @{text "induct"} method works with primary means of
the proof language instead.
-*}
+\<close>
lemma
fixes n :: nat
and x :: 'a
assumes "A n x"
- shows "P n x" using `A n x`
+ shows "P n x" using \<open>A n x\<close>
proof (induct n arbitrary: x)
case 0
- note prem = `A 0 x`
+ note prem = \<open>A 0 x\<close>
show "P 0 x" sorry
next
case (Suc n)
- note hyp = `\<And>x. A n x \<Longrightarrow> P n x`
- and prem = `A (Suc n) x`
+ note hyp = \<open>\<And>x. A n x \<Longrightarrow> P n x\<close>
+ and prem = \<open>A (Suc n) x\<close>
show "P (Suc n) x" sorry
qed
-subsubsection {* Local definitions *}
+subsubsection \<open>Local definitions\<close>
-text {*
+text \<open>
Here the idea is to turn sub-expressions of the problem into a
defined induction variable. This is often accompanied with fixing
of auxiliary parameters in the original expression, otherwise the
induction step would refer invariably to particular entities. This
combination essentially expresses a partially abstracted
representation of inductive expressions.
-*}
+\<close>
lemma
fixes a :: "'a \<Rightarrow> nat"
assumes "A (a x)"
- shows "P (a x)" using `A (a x)`
+ shows "P (a x)" using \<open>A (a x)\<close>
proof (induct n \<equiv> "a x" arbitrary: x)
case 0
- note prem = `A (a x)`
- and defn = `0 = a x`
+ note prem = \<open>A (a x)\<close>
+ and defn = \<open>0 = a x\<close>
show "P (a x)" sorry
next
case (Suc n)
- note hyp = `\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)`
- and prem = `A (a x)`
- and defn = `Suc n = a x`
+ note hyp = \<open>\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)\<close>
+ and prem = \<open>A (a x)\<close>
+ and defn = \<open>Suc n = a x\<close>
show "P (a x)" sorry
qed
-text {*
+text \<open>
Observe how the local definition @{text "n = a x"} recurs in the
inductive cases as @{text "0 = a x"} and @{text "Suc n = a x"},
according to underlying induction rule.
-*}
+\<close>
-subsubsection {* Simple simultaneous goals *}
+subsubsection \<open>Simple simultaneous goals\<close>
-text {*
+text \<open>
The most basic simultaneous induction operates on several goals
one-by-one, where each case refers to induction hypotheses that are
duplicated according to the number of conclusions.
-*}
+\<close>
lemma
fixes n :: nat
@@ -105,18 +105,18 @@
show "Q 0" sorry
next
case (Suc n) case 1
- note hyps = `P n` `Q n`
+ note hyps = \<open>P n\<close> \<open>Q n\<close>
show "P (Suc n)" sorry
next
case (Suc n) case 2
- note hyps = `P n` `Q n`
+ note hyps = \<open>P n\<close> \<open>Q n\<close>
show "Q (Suc n)" sorry
qed
-text {*
+text \<open>
The split into subcases may be deferred as follows -- this is
particularly relevant for goal statements with local premises.
-*}
+\<close>
lemma
fixes n :: nat
@@ -126,32 +126,32 @@
case 0
{
case 1
- note `A 0`
+ note \<open>A 0\<close>
show "P 0" sorry
next
case 2
- note `B 0`
+ note \<open>B 0\<close>
show "Q 0" sorry
}
next
case (Suc n)
- note `A n \<Longrightarrow> P n`
- and `B n \<Longrightarrow> Q n`
+ note \<open>A n \<Longrightarrow> P n\<close>
+ and \<open>B n \<Longrightarrow> Q n\<close>
{
case 1
- note `A (Suc n)`
+ note \<open>A (Suc n)\<close>
show "P (Suc n)" sorry
next
case 2
- note `B (Suc n)`
+ note \<open>B (Suc n)\<close>
show "Q (Suc n)" sorry
}
qed
-subsubsection {* Compound simultaneous goals *}
+subsubsection \<open>Compound simultaneous goals\<close>
-text {*
+text \<open>
The following pattern illustrates the slightly more complex
situation of simultaneous goals with individual local assumptions.
In compound simultaneous statements like this, local assumptions
@@ -159,7 +159,7 @@
framework. In contrast, local parameters do not require separate
@{text "\<And>"} prefixes here, but may be moved into the common context
of the whole statement.
-*}
+\<close>
lemma
fixes n :: nat
@@ -171,42 +171,42 @@
case 0
{
case 1
- note prem = `A 0 x`
+ note prem = \<open>A 0 x\<close>
show "P 0 x" sorry
}
{
case 2
- note prem = `B 0 y`
+ note prem = \<open>B 0 y\<close>
show "Q 0 y" sorry
}
next
case (Suc n)
- note hyps = `\<And>x. A n x \<Longrightarrow> P n x` `\<And>y. B n y \<Longrightarrow> Q n y`
+ note hyps = \<open>\<And>x. A n x \<Longrightarrow> P n x\<close> \<open>\<And>y. B n y \<Longrightarrow> Q n y\<close>
then have some_intermediate_result sorry
{
case 1
- note prem = `A (Suc n) x`
+ note prem = \<open>A (Suc n) x\<close>
show "P (Suc n) x" sorry
}
{
case 2
- note prem = `B (Suc n) y`
+ note prem = \<open>B (Suc n) y\<close>
show "Q (Suc n) y" sorry
}
qed
-text {*
+text \<open>
Here @{text "induct"} provides again nested cases with numbered
sub-cases, which allows to share common parts of the body context.
In typical applications, there could be a long intermediate proof of
general consequences of the induction hypotheses, before finishing
each conclusion separately.
-*}
+\<close>
-subsection {* Multiple rules *}
+subsection \<open>Multiple rules\<close>
-text {*
+text \<open>
Multiple induction rules emerge from mutual definitions of
datatypes, inductive predicates, functions etc. The @{text
"induct"} method accepts replicated arguments (with @{text "and"}
@@ -216,18 +216,18 @@
The goal statement essentially follows the same arrangement,
although it might be subdivided into simultaneous sub-problems as
before!
-*}
+\<close>
datatype foo = Foo1 nat | Foo2 bar
and bar = Bar1 bool | Bar2 bazar
and bazar = Bazar foo
-text {*
+text \<open>
The pack of induction rules for this datatype is: @{thm [display]
foo.induct [no_vars] bar.induct [no_vars] bazar.induct [no_vars]}
This corresponds to the following basic proof pattern:
-*}
+\<close>
lemma
fixes foo :: foo
@@ -241,25 +241,25 @@
show "P (Foo1 n)" sorry
next
case (Foo2 bar)
- note `Q bar`
+ note \<open>Q bar\<close>
show "P (Foo2 bar)" sorry
next
case (Bar1 b)
show "Q (Bar1 b)" sorry
next
case (Bar2 bazar)
- note `R bazar`
+ note \<open>R bazar\<close>
show "Q (Bar2 bazar)" sorry
next
case (Bazar foo)
- note `P foo`
+ note \<open>P foo\<close>
show "R (Bazar foo)" sorry
qed
-text {*
+text \<open>
This can be combined with the previous techniques for compound
statements, e.g.\ like this.
-*}
+\<close>
lemma
fixes x :: 'a and y :: 'b and z :: 'c
@@ -279,12 +279,12 @@
oops
-subsection {* Inductive predicates *}
+subsection \<open>Inductive predicates\<close>
-text {*
+text \<open>
The most basic form of induction involving predicates (or sets)
essentially eliminates a given membership fact.
-*}
+\<close>
inductive Even :: "nat \<Rightarrow> bool" where
zero: "Even 0"
@@ -299,22 +299,22 @@
show "P 0" sorry
next
case (double n)
- note `Even n` and `P n`
+ note \<open>Even n\<close> and \<open>P n\<close>
show "P (2 * n)" sorry
qed
-text {*
+text \<open>
Alternatively, an initial rule statement may be proven as follows,
performing ``in-situ'' elimination with explicit rule specification.
-*}
+\<close>
lemma "Even n \<Longrightarrow> P n"
proof (induct rule: Even.induct)
oops
-text {*
+text \<open>
Simultaneous goals do not introduce anything new.
-*}
+\<close>
lemma
assumes "Even n"
@@ -331,7 +331,7 @@
}
next
case (double n)
- note `Even n` and `P1 n` and `P2 n`
+ note \<open>Even n\<close> and \<open>P1 n\<close> and \<open>P2 n\<close>
{
case 1
show "P1 (2 * n)" sorry
@@ -341,11 +341,11 @@
}
qed
-text {*
+text \<open>
Working with mutual rules requires special care in composing the
statement as a two-level conjunction, using lists of propositions
separated by @{text "and"}. For example:
-*}
+\<close>
inductive Evn :: "nat \<Rightarrow> bool" and Odd :: "nat \<Rightarrow> bool"
where
@@ -367,28 +367,28 @@
{ case 3 show "P3 0" sorry }
next
case (succ_Evn n)
- note `Evn n` and `P1 n` `P2 n` `P3 n`
+ note \<open>Evn n\<close> and \<open>P1 n\<close> \<open>P2 n\<close> \<open>P3 n\<close>
{ case 1 show "Q1 (Suc n)" sorry }
{ case 2 show "Q2 (Suc n)" sorry }
next
case (succ_Odd n)
- note `Odd n` and `Q1 n` `Q2 n`
+ note \<open>Odd n\<close> and \<open>Q1 n\<close> \<open>Q2 n\<close>
{ case 1 show "P1 (Suc n)" sorry }
{ case 2 show "P2 (Suc n)" sorry }
{ case 3 show "P3 (Suc n)" sorry }
qed
-text {*
+text \<open>
Cases and hypotheses in each case can be named explicitly.
-*}
+\<close>
inductive star :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" for r
where
refl: "star r x x"
| step: "r x y \<Longrightarrow> star r y z \<Longrightarrow> star r x z"
-text {* Underscores are replaced by the default name hyps: *}
+text \<open>Underscores are replaced by the default name hyps:\<close>
lemmas star_induct = star.induct [case_names base step[r _ IH]]
--- a/src/HOL/Induct/Ordinals.thy Sat Jun 20 15:43:36 2015 +0200
+++ b/src/HOL/Induct/Ordinals.thy Sat Jun 20 15:45:02 2015 +0200
@@ -2,17 +2,17 @@
Author: Stefan Berghofer and Markus Wenzel, TU Muenchen
*)
-section {* Ordinals *}
+section \<open>Ordinals\<close>
theory Ordinals
imports Main
begin
-text {*
+text \<open>
Some basic definitions of ordinal numbers. Draws an Agda
development (in Martin-L\"of type theory) by Peter Hancock (see
@{url "http://www.dcs.ed.ac.uk/home/pgh/chat.html"}).
-*}
+\<close>
datatype ordinal =
Zero
--- a/src/HOL/Induct/PropLog.thy Sat Jun 20 15:43:36 2015 +0200
+++ b/src/HOL/Induct/PropLog.thy Sat Jun 20 15:45:02 2015 +0200
@@ -3,11 +3,11 @@
Copyright 1994 TU Muenchen & University of Cambridge
*)
-section {* Meta-theory of propositional logic *}
+section \<open>Meta-theory of propositional logic\<close>
theory PropLog imports Main begin
-text {*
+text \<open>
Datatype definition of propositional logic formulae and inductive
definition of the propositional tautologies.
@@ -16,9 +16,9 @@
Prove: If @{text "H |= p"} then @{text "G |= p"} where @{text "G \<in>
Fin(H)"}
-*}
+\<close>
-subsection {* The datatype of propositions *}
+subsection \<open>The datatype of propositions\<close>
datatype 'a pl =
false |
@@ -26,7 +26,7 @@
imp "'a pl" "'a pl" (infixr "->" 90)
-subsection {* The proof system *}
+subsection \<open>The proof system\<close>
inductive thms :: "['a pl set, 'a pl] => bool" (infixl "|-" 50)
for H :: "'a pl set"
@@ -38,9 +38,9 @@
| MP: "[| H |- p->q; H |- p |] ==> H |- q"
-subsection {* The semantics *}
+subsection \<open>The semantics\<close>
-subsubsection {* Semantics of propositional logic. *}
+subsubsection \<open>Semantics of propositional logic.\<close>
primrec eval :: "['a set, 'a pl] => bool" ("_[[_]]" [100,0] 100)
where
@@ -48,10 +48,10 @@
| "tt[[#v]] = (v \<in> tt)"
| eval_imp: "tt[[p->q]] = (tt[[p]] --> tt[[q]])"
-text {*
+text \<open>
A finite set of hypotheses from @{text t} and the @{text Var}s in
@{text p}.
-*}
+\<close>
primrec hyps :: "['a pl, 'a set] => 'a pl set"
where
@@ -60,18 +60,18 @@
| "hyps (p->q) tt = hyps p tt Un hyps q tt"
-subsubsection {* Logical consequence *}
+subsubsection \<open>Logical consequence\<close>
-text {*
+text \<open>
For every valuation, if all elements of @{text H} are true then so
is @{text p}.
-*}
+\<close>
definition sat :: "['a pl set, 'a pl] => bool" (infixl "|=" 50)
where "H |= p = (\<forall>tt. (\<forall>q\<in>H. tt[[q]]) --> tt[[p]])"
-subsection {* Proof theory of propositional logic *}
+subsection \<open>Proof theory of propositional logic\<close>
lemma thms_mono: "G<=H ==> thms(G) <= thms(H)"
apply (rule predicate1I)
@@ -80,14 +80,14 @@
done
lemma thms_I: "H |- p->p"
- -- {*Called @{text I} for Identity Combinator, not for Introduction. *}
+ -- \<open>Called @{text I} for Identity Combinator, not for Introduction.\<close>
by (best intro: thms.K thms.S thms.MP)
-subsubsection {* Weakening, left and right *}
+subsubsection \<open>Weakening, left and right\<close>
lemma weaken_left: "[| G \<subseteq> H; G|-p |] ==> H|-p"
- -- {* Order of premises is convenient with @{text THEN} *}
+ -- \<open>Order of premises is convenient with @{text THEN}\<close>
by (erule thms_mono [THEN predicate1D])
lemma weaken_left_insert: "G |- p \<Longrightarrow> insert a G |- p"
@@ -103,7 +103,7 @@
by (fast intro: thms.K thms.MP)
-subsubsection {* The deduction theorem *}
+subsubsection \<open>The deduction theorem\<close>
theorem deduction: "insert p H |- q ==> H |- p->q"
apply (induct set: thms)
@@ -112,7 +112,7 @@
done
-subsubsection {* The cut rule *}
+subsubsection \<open>The cut rule\<close>
lemma cut: "insert p H |- q \<Longrightarrow> H |- p \<Longrightarrow> H |- q"
by (rule thms.MP) (rule deduction)
@@ -124,15 +124,15 @@
by (rule thms_falseE) (rule thms.MP)
-subsubsection {* Soundness of the rules wrt truth-table semantics *}
+subsubsection \<open>Soundness of the rules wrt truth-table semantics\<close>
theorem soundness: "H |- p ==> H |= p"
by (induct set: thms) (auto simp: sat_def)
-subsection {* Completeness *}
+subsection \<open>Completeness\<close>
-subsubsection {* Towards the completeness proof *}
+subsubsection \<open>Towards the completeness proof\<close>
lemma false_imp: "H |- p->false ==> H |- p->q"
apply (rule deduction)
@@ -146,7 +146,7 @@
done
lemma hyps_thms_if: "hyps p tt |- (if tt[[p]] then p else p->false)"
- -- {* Typical example of strengthening the induction statement. *}
+ -- \<open>Typical example of strengthening the induction statement.\<close>
apply simp
apply (induct p)
apply (simp_all add: thms_I thms.H)
@@ -155,21 +155,21 @@
done
lemma sat_thms_p: "{} |= p ==> hyps p tt |- p"
- -- {* Key lemma for completeness; yields a set of assumptions
- satisfying @{text p} *}
+ -- \<open>Key lemma for completeness; yields a set of assumptions
+ satisfying @{text p}\<close>
unfolding sat_def
by (metis (full_types) empty_iff hyps_thms_if)
-text {*
+text \<open>
For proving certain theorems in our new propositional logic.
-*}
+\<close>
declare deduction [intro!]
declare thms.H [THEN thms.MP, intro]
-text {*
+text \<open>
The excluded middle in the form of an elimination rule.
-*}
+\<close>
lemma thms_excluded_middle: "H |- (p->q) -> ((p->false)->q) -> q"
apply (rule deduction [THEN deduction])
@@ -178,29 +178,29 @@
lemma thms_excluded_middle_rule:
"[| insert p H |- q; insert (p->false) H |- q |] ==> H |- q"
- -- {* Hard to prove directly because it requires cuts *}
+ -- \<open>Hard to prove directly because it requires cuts\<close>
by (rule thms_excluded_middle [THEN thms.MP, THEN thms.MP], auto)
-subsection{* Completeness -- lemmas for reducing the set of assumptions*}
+subsection\<open>Completeness -- lemmas for reducing the set of assumptions\<close>
-text {*
+text \<open>
For the case @{prop "hyps p t - insert #v Y |- p"} we also have @{prop
"hyps p t - {#v} \<subseteq> hyps p (t-{v})"}.
-*}
+\<close>
lemma hyps_Diff: "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})"
by (induct p) auto
-text {*
+text \<open>
For the case @{prop "hyps p t - insert (#v -> Fls) Y |- p"} we also have
@{prop "hyps p t-{#v->Fls} \<subseteq> hyps p (insert v t)"}.
-*}
+\<close>
lemma hyps_insert: "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})"
by (induct p) auto
-text {* Two lemmas for use with @{text weaken_left} *}
+text \<open>Two lemmas for use with @{text weaken_left}\<close>
lemma insert_Diff_same: "B-C <= insert a (B-insert a C)"
by fast
@@ -208,10 +208,10 @@
lemma insert_Diff_subset2: "insert a (B-{c}) - D <= insert a (B-insert c D)"
by fast
-text {*
+text \<open>
The set @{term "hyps p t"} is finite, and elements have the form
@{term "#v"} or @{term "#v->Fls"}.
-*}
+\<close>
lemma hyps_finite: "finite(hyps p t)"
by (induct p) auto
@@ -223,34 +223,34 @@
by (rule Diff_mono [OF _ subset_refl, THEN weaken_left])
-subsubsection {* Completeness theorem *}
+subsubsection \<open>Completeness theorem\<close>
-text {*
+text \<open>
Induction on the finite set of assumptions @{term "hyps p t0"}. We
may repeatedly subtract assumptions until none are left!
-*}
+\<close>
lemma completeness_0_lemma:
"{} |= p ==> \<forall>t. hyps p t - hyps p t0 |- p"
apply (rule hyps_subset [THEN hyps_finite [THEN finite_subset_induct]])
apply (simp add: sat_thms_p, safe)
- txt{*Case @{text"hyps p t-insert(#v,Y) |- p"} *}
+ txt\<open>Case @{text"hyps p t-insert(#v,Y) |- p"}\<close>
apply (iprover intro: thms_excluded_middle_rule
insert_Diff_same [THEN weaken_left]
insert_Diff_subset2 [THEN weaken_left]
hyps_Diff [THEN Diff_weaken_left])
-txt{*Case @{text"hyps p t-insert(#v -> false,Y) |- p"} *}
+txt\<open>Case @{text"hyps p t-insert(#v -> false,Y) |- p"}\<close>
apply (iprover intro: thms_excluded_middle_rule
insert_Diff_same [THEN weaken_left]
insert_Diff_subset2 [THEN weaken_left]
hyps_insert [THEN Diff_weaken_left])
done
-text{*The base case for completeness*}
+text\<open>The base case for completeness\<close>
lemma completeness_0: "{} |= p ==> {} |- p"
by (metis Diff_cancel completeness_0_lemma)
-text{*A semantic analogue of the Deduction Theorem*}
+text\<open>A semantic analogue of the Deduction Theorem\<close>
lemma sat_imp: "insert p H |= q ==> H |= p->q"
by (auto simp: sat_def)
--- a/src/HOL/Induct/QuoDataType.thy Sat Jun 20 15:43:36 2015 +0200
+++ b/src/HOL/Induct/QuoDataType.thy Sat Jun 20 15:45:02 2015 +0200
@@ -3,25 +3,25 @@
Copyright 2004 University of Cambridge
*)
-section{*Defining an Initial Algebra by Quotienting a Free Algebra*}
+section\<open>Defining an Initial Algebra by Quotienting a Free Algebra\<close>
theory QuoDataType imports Main begin
-subsection{*Defining the Free Algebra*}
+subsection\<open>Defining the Free Algebra\<close>
-text{*Messages with encryption and decryption as free constructors.*}
+text\<open>Messages with encryption and decryption as free constructors.\<close>
datatype
freemsg = NONCE nat
| MPAIR freemsg freemsg
| CRYPT nat freemsg
| DECRYPT nat freemsg
-text{*The equivalence relation, which makes encryption and decryption inverses
+text\<open>The equivalence relation, which makes encryption and decryption inverses
provided the keys are the same.
The first two rules are the desired equations. The next four rules
make the equations applicable to subterms. The last two rules are symmetry
-and transitivity.*}
+and transitivity.\<close>
inductive_set
msgrel :: "(freemsg * freemsg) set"
@@ -38,7 +38,7 @@
| TRANS: "\<lbrakk>X \<sim> Y; Y \<sim> Z\<rbrakk> \<Longrightarrow> X \<sim> Z"
-text{*Proving that it is an equivalence relation*}
+text\<open>Proving that it is an equivalence relation\<close>
lemma msgrel_refl: "X \<sim> X"
by (induct X) (blast intro: msgrel.intros)+
@@ -52,76 +52,76 @@
qed
-subsection{*Some Functions on the Free Algebra*}
+subsection\<open>Some Functions on the Free Algebra\<close>
-subsubsection{*The Set of Nonces*}
+subsubsection\<open>The Set of Nonces\<close>
-text{*A function to return the set of nonces present in a message. It will
-be lifted to the initial algebra, to serve as an example of that process.*}
+text\<open>A function to return the set of nonces present in a message. It will
+be lifted to the initial algebra, to serve as an example of that process.\<close>
primrec freenonces :: "freemsg \<Rightarrow> nat set" where
"freenonces (NONCE N) = {N}"
| "freenonces (MPAIR X Y) = freenonces X \<union> freenonces Y"
| "freenonces (CRYPT K X) = freenonces X"
| "freenonces (DECRYPT K X) = freenonces X"
-text{*This theorem lets us prove that the nonces function respects the
+text\<open>This theorem lets us prove that the nonces function respects the
equivalence relation. It also helps us prove that Nonce
- (the abstract constructor) is injective*}
+ (the abstract constructor) is injective\<close>
theorem msgrel_imp_eq_freenonces: "U \<sim> V \<Longrightarrow> freenonces U = freenonces V"
by (induct set: msgrel) auto
-subsubsection{*The Left Projection*}
+subsubsection\<open>The Left Projection\<close>
-text{*A function to return the left part of the top pair in a message. It will
-be lifted to the initial algebra, to serve as an example of that process.*}
+text\<open>A function to return the left part of the top pair in a message. It will
+be lifted to the initial algebra, to serve as an example of that process.\<close>
primrec freeleft :: "freemsg \<Rightarrow> freemsg" where
"freeleft (NONCE N) = NONCE N"
| "freeleft (MPAIR X Y) = X"
| "freeleft (CRYPT K X) = freeleft X"
| "freeleft (DECRYPT K X) = freeleft X"
-text{*This theorem lets us prove that the left function respects the
+text\<open>This theorem lets us prove that the left function respects the
equivalence relation. It also helps us prove that MPair
- (the abstract constructor) is injective*}
+ (the abstract constructor) is injective\<close>
theorem msgrel_imp_eqv_freeleft:
"U \<sim> V \<Longrightarrow> freeleft U \<sim> freeleft V"
by (induct set: msgrel) (auto intro: msgrel.intros)
-subsubsection{*The Right Projection*}
+subsubsection\<open>The Right Projection\<close>
-text{*A function to return the right part of the top pair in a message.*}
+text\<open>A function to return the right part of the top pair in a message.\<close>
primrec freeright :: "freemsg \<Rightarrow> freemsg" where
"freeright (NONCE N) = NONCE N"
| "freeright (MPAIR X Y) = Y"
| "freeright (CRYPT K X) = freeright X"
| "freeright (DECRYPT K X) = freeright X"
-text{*This theorem lets us prove that the right function respects the
+text\<open>This theorem lets us prove that the right function respects the
equivalence relation. It also helps us prove that MPair
- (the abstract constructor) is injective*}
+ (the abstract constructor) is injective\<close>
theorem msgrel_imp_eqv_freeright:
"U \<sim> V \<Longrightarrow> freeright U \<sim> freeright V"
by (induct set: msgrel) (auto intro: msgrel.intros)
-subsubsection{*The Discriminator for Constructors*}
+subsubsection\<open>The Discriminator for Constructors\<close>
-text{*A function to distinguish nonces, mpairs and encryptions*}
+text\<open>A function to distinguish nonces, mpairs and encryptions\<close>
primrec freediscrim :: "freemsg \<Rightarrow> int" where
"freediscrim (NONCE N) = 0"
| "freediscrim (MPAIR X Y) = 1"
| "freediscrim (CRYPT K X) = freediscrim X + 2"
| "freediscrim (DECRYPT K X) = freediscrim X - 2"
-text{*This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}*}
+text\<open>This theorem helps us prove @{term "Nonce N \<noteq> MPair X Y"}\<close>
theorem msgrel_imp_eq_freediscrim:
"U \<sim> V \<Longrightarrow> freediscrim U = freediscrim V"
by (induct set: msgrel) auto
-subsection{*The Initial Algebra: A Quotiented Message Type*}
+subsection\<open>The Initial Algebra: A Quotiented Message Type\<close>
definition "Msg = UNIV//msgrel"
@@ -130,7 +130,7 @@
unfolding Msg_def by (auto simp add: quotient_def)
-text{*The abstract message constructors*}
+text\<open>The abstract message constructors\<close>
definition
Nonce :: "nat \<Rightarrow> msg" where
"Nonce N = Abs_Msg(msgrel``{NONCE N})"
@@ -151,14 +151,14 @@
Abs_Msg (\<Union>U \<in> Rep_Msg X. msgrel``{DECRYPT K U})"
-text{*Reduces equality of equivalence classes to the @{term msgrel} relation:
- @{term "(msgrel `` {x} = msgrel `` {y}) = ((x,y) \<in> msgrel)"} *}
+text\<open>Reduces equality of equivalence classes to the @{term msgrel} relation:
+ @{term "(msgrel `` {x} = msgrel `` {y}) = ((x,y) \<in> msgrel)"}\<close>
lemmas equiv_msgrel_iff = eq_equiv_class_iff [OF equiv_msgrel UNIV_I UNIV_I]
declare equiv_msgrel_iff [simp]
-text{*All equivalence classes belong to set of representatives*}
+text\<open>All equivalence classes belong to set of representatives\<close>
lemma [simp]: "msgrel``{U} \<in> Msg"
by (auto simp add: Msg_def quotient_def intro: msgrel_refl)
@@ -167,13 +167,13 @@
apply (erule Abs_Msg_inverse)
done
-text{*Reduces equality on abstractions to equality on representatives*}
+text\<open>Reduces equality on abstractions to equality on representatives\<close>
declare inj_on_Abs_Msg [THEN inj_on_iff, simp]
declare Abs_Msg_inverse [simp]
-subsubsection{*Characteristic Equations for the Abstract Constructors*}
+subsubsection\<open>Characteristic Equations for the Abstract Constructors\<close>
lemma MPair: "MPair (Abs_Msg(msgrel``{U})) (Abs_Msg(msgrel``{V})) =
Abs_Msg (msgrel``{MPAIR U V})"
@@ -201,7 +201,7 @@
by (simp add: Decrypt_def UN_equiv_class [OF equiv_msgrel])
qed
-text{*Case analysis on the representation of a msg as an equivalence class.*}
+text\<open>Case analysis on the representation of a msg as an equivalence class.\<close>
lemma eq_Abs_Msg [case_names Abs_Msg, cases type: msg]:
"(!!U. z = Abs_Msg(msgrel``{U}) ==> P) ==> P"
apply (rule Rep_Msg [of z, unfolded Msg_def, THEN quotientE])
@@ -209,7 +209,7 @@
apply (auto simp add: Rep_Msg_inverse intro: msgrel_refl)
done
-text{*Establishing these two equations is the point of the whole exercise*}
+text\<open>Establishing these two equations is the point of the whole exercise\<close>
theorem CD_eq [simp]: "Crypt K (Decrypt K X) = X"
by (cases X, simp add: Crypt Decrypt CD)
@@ -217,7 +217,7 @@
by (cases X, simp add: Crypt Decrypt DC)
-subsection{*The Abstract Function to Return the Set of Nonces*}
+subsection\<open>The Abstract Function to Return the Set of Nonces\<close>
definition
nonces :: "msg \<Rightarrow> nat set" where
@@ -227,7 +227,7 @@
by (auto simp add: congruent_def msgrel_imp_eq_freenonces)
-text{*Now prove the four equations for @{term nonces}*}
+text\<open>Now prove the four equations for @{term nonces}\<close>
lemma nonces_Nonce [simp]: "nonces (Nonce N) = {N}"
by (simp add: nonces_def Nonce_def
@@ -252,7 +252,7 @@
done
-subsection{*The Abstract Function to Return the Left Part*}
+subsection\<open>The Abstract Function to Return the Left Part\<close>
definition
left :: "msg \<Rightarrow> msg" where
@@ -261,7 +261,7 @@
lemma left_congruent: "(\<lambda>U. msgrel `` {freeleft U}) respects msgrel"
by (auto simp add: congruent_def msgrel_imp_eqv_freeleft)
-text{*Now prove the four equations for @{term left}*}
+text\<open>Now prove the four equations for @{term left}\<close>
lemma left_Nonce [simp]: "left (Nonce N) = Nonce N"
by (simp add: left_def Nonce_def
@@ -286,7 +286,7 @@
done
-subsection{*The Abstract Function to Return the Right Part*}
+subsection\<open>The Abstract Function to Return the Right Part\<close>
definition
right :: "msg \<Rightarrow> msg" where
@@ -295,7 +295,7 @@
lemma right_congruent: "(\<lambda>U. msgrel `` {freeright U}) respects msgrel"
by (auto simp add: congruent_def msgrel_imp_eqv_freeright)
-text{*Now prove the four equations for @{term right}*}
+text\<open>Now prove the four equations for @{term right}\<close>
lemma right_Nonce [simp]: "right (Nonce N) = Nonce N"
by (simp add: right_def Nonce_def
@@ -320,12 +320,12 @@
done
-subsection{*Injectivity Properties of Some Constructors*}
+subsection\<open>Injectivity Properties of Some Constructors\<close>
lemma NONCE_imp_eq: "NONCE m \<sim> NONCE n \<Longrightarrow> m = n"
by (drule msgrel_imp_eq_freenonces, simp)
-text{*Can also be proved using the function @{term nonces}*}
+text\<open>Can also be proved using the function @{term nonces}\<close>
lemma Nonce_Nonce_eq [iff]: "(Nonce m = Nonce n) = (m = n)"
by (auto simp add: Nonce_def msgrel_refl dest: NONCE_imp_eq)
@@ -361,11 +361,11 @@
apply (blast dest: NONCE_neqv_MPAIR)
done
-text{*Example suggested by a referee*}
+text\<open>Example suggested by a referee\<close>
theorem Crypt_Nonce_neq_Nonce: "Crypt K (Nonce M) \<noteq> Nonce N"
by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)
-text{*...and many similar results*}
+text\<open>...and many similar results\<close>
theorem Crypt2_Nonce_neq_Nonce: "Crypt K (Crypt K' (Nonce M)) \<noteq> Nonce N"
by (auto simp add: Nonce_def Crypt dest: msgrel_imp_eq_freediscrim)
@@ -418,10 +418,10 @@
qed
-subsection{*The Abstract Discriminator*}
+subsection\<open>The Abstract Discriminator\<close>
-text{*However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
-need this function in order to prove discrimination theorems.*}
+text\<open>However, as @{text Crypt_Nonce_neq_Nonce} above illustrates, we don't
+need this function in order to prove discrimination theorems.\<close>
definition
discrim :: "msg \<Rightarrow> int" where
@@ -430,7 +430,7 @@
lemma discrim_congruent: "(\<lambda>U. {freediscrim U}) respects msgrel"
by (auto simp add: congruent_def msgrel_imp_eq_freediscrim)
-text{*Now prove the four equations for @{term discrim}*}
+text\<open>Now prove the four equations for @{term discrim}\<close>
lemma discrim_Nonce [simp]: "discrim (Nonce N) = 0"
by (simp add: discrim_def Nonce_def
--- a/src/HOL/Induct/QuoNestedDataType.thy Sat Jun 20 15:43:36 2015 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy Sat Jun 20 15:45:02 2015 +0200
@@ -3,13 +3,13 @@
Copyright 2004 University of Cambridge
*)
-section{*Quotienting a Free Algebra Involving Nested Recursion*}
+section\<open>Quotienting a Free Algebra Involving Nested Recursion\<close>
theory QuoNestedDataType imports Main begin
-subsection{*Defining the Free Algebra*}
+subsection\<open>Defining the Free Algebra\<close>
-text{*Messages with encryption and decryption as free constructors.*}
+text\<open>Messages with encryption and decryption as free constructors.\<close>
datatype
freeExp = VAR nat
| PLUS freeExp freeExp
@@ -17,11 +17,11 @@
datatype_compat freeExp
-text{*The equivalence relation, which makes PLUS associative.*}
+text\<open>The equivalence relation, which makes PLUS associative.\<close>
-text{*The first rule is the desired equation. The next three rules
+text\<open>The first rule is the desired equation. The next three rules
make the equations applicable to subterms. The last two rules are symmetry
-and transitivity.*}
+and transitivity.\<close>
inductive_set
exprel :: "(freeExp * freeExp) set"
and exp_rel :: "[freeExp, freeExp] => bool" (infixl "\<sim>" 50)
@@ -36,7 +36,7 @@
monos listrel_mono
-text{*Proving that it is an equivalence relation*}
+text\<open>Proving that it is an equivalence relation\<close>
lemma exprel_refl: "X \<sim> X"
and list_exprel_refl: "(Xs,Xs) \<in> listrel(exprel)"
@@ -67,14 +67,14 @@
-subsection{*Some Functions on the Free Algebra*}
+subsection\<open>Some Functions on the Free Algebra\<close>
-subsubsection{*The Set of Variables*}
+subsubsection\<open>The Set of Variables\<close>
-text{*A function to return the set of variables present in a message. It will
+text\<open>A function to return the set of variables present in a message. It will
be lifted to the initial algebra, to serve as an example of that process.
Note that the "free" refers to the free datatype rather than to the concept
-of a free variable.*}
+of a free variable.\<close>
primrec freevars :: "freeExp \<Rightarrow> nat set"
and freevars_list :: "freeExp list \<Rightarrow> nat set" where
"freevars (VAR N) = {N}"
@@ -84,9 +84,9 @@
| "freevars_list [] = {}"
| "freevars_list (X # Xs) = freevars X \<union> freevars_list Xs"
-text{*This theorem lets us prove that the vars function respects the
+text\<open>This theorem lets us prove that the vars function respects the
equivalence relation. It also helps us prove that Variable
- (the abstract constructor) is injective*}
+ (the abstract constructor) is injective\<close>
theorem exprel_imp_eq_freevars: "U \<sim> V \<Longrightarrow> freevars U = freevars V"
apply (induct set: exprel)
apply (erule_tac [4] listrel.induct)
@@ -95,9 +95,9 @@
-subsubsection{*Functions for Freeness*}
+subsubsection\<open>Functions for Freeness\<close>
-text{*A discriminator function to distinguish vars, sums and function calls*}
+text\<open>A discriminator function to distinguish vars, sums and function calls\<close>
primrec freediscrim :: "freeExp \<Rightarrow> int" where
"freediscrim (VAR N) = 0"
| "freediscrim (PLUS X Y) = 1"
@@ -108,8 +108,8 @@
by (induct set: exprel) auto
-text{*This function, which returns the function name, is used to
-prove part of the injectivity property for FnCall.*}
+text\<open>This function, which returns the function name, is used to
+prove part of the injectivity property for FnCall.\<close>
primrec freefun :: "freeExp \<Rightarrow> nat" where
"freefun (VAR N) = 0"
| "freefun (PLUS X Y) = 0"
@@ -120,8 +120,8 @@
by (induct set: exprel) (simp_all add: listrel.intros)
-text{*This function, which returns the list of function arguments, is used to
-prove part of the injectivity property for FnCall.*}
+text\<open>This function, which returns the list of function arguments, is used to
+prove part of the injectivity property for FnCall.\<close>
primrec freeargs :: "freeExp \<Rightarrow> freeExp list" where
"freeargs (VAR N) = []"
| "freeargs (PLUS X Y) = []"
@@ -143,7 +143,7 @@
qed
-subsection{*The Initial Algebra: A Quotiented Message Type*}
+subsection\<open>The Initial Algebra: A Quotiented Message Type\<close>
definition "Exp = UNIV//exprel"
@@ -151,7 +151,7 @@
morphisms Rep_Exp Abs_Exp
unfolding Exp_def by (auto simp add: quotient_def)
-text{*The abstract message constructors*}
+text\<open>The abstract message constructors\<close>
definition
Var :: "nat \<Rightarrow> exp" where
@@ -168,14 +168,14 @@
Abs_Exp (\<Union>Us \<in> listset (map Rep_Exp Xs). exprel `` {FNCALL F Us})"
-text{*Reduces equality of equivalence classes to the @{term exprel} relation:
- @{term "(exprel `` {x} = exprel `` {y}) = ((x,y) \<in> exprel)"} *}
+text\<open>Reduces equality of equivalence classes to the @{term exprel} relation:
+ @{term "(exprel `` {x} = exprel `` {y}) = ((x,y) \<in> exprel)"}\<close>
lemmas equiv_exprel_iff = eq_equiv_class_iff [OF equiv_exprel UNIV_I UNIV_I]
declare equiv_exprel_iff [simp]
-text{*All equivalence classes belong to set of representatives*}
+text\<open>All equivalence classes belong to set of representatives\<close>
lemma [simp]: "exprel``{U} \<in> Exp"
by (auto simp add: Exp_def quotient_def intro: exprel_refl)
@@ -184,13 +184,13 @@
apply (erule Abs_Exp_inverse)
done
-text{*Reduces equality on abstractions to equality on representatives*}
+text\<open>Reduces equality on abstractions to equality on representatives\<close>
declare inj_on_Abs_Exp [THEN inj_on_iff, simp]
declare Abs_Exp_inverse [simp]
-text{*Case analysis on the representation of a exp as an equivalence class.*}
+text\<open>Case analysis on the representation of a exp as an equivalence class.\<close>
lemma eq_Abs_Exp [case_names Abs_Exp, cases type: exp]:
"(!!U. z = Abs_Exp(exprel``{U}) ==> P) ==> P"
apply (rule Rep_Exp [of z, unfolded Exp_def, THEN quotientE])
@@ -199,8 +199,8 @@
done
-subsection{*Every list of abstract expressions can be expressed in terms of a
- list of concrete expressions*}
+subsection\<open>Every list of abstract expressions can be expressed in terms of a
+ list of concrete expressions\<close>
definition
Abs_ExpList :: "freeExp list => exp list" where
@@ -225,7 +225,7 @@
by (rule exE [OF ExpList_rep], blast)
-subsubsection{*Characteristic Equations for the Abstract Constructors*}
+subsubsection\<open>Characteristic Equations for the Abstract Constructors\<close>
lemma Plus: "Plus (Abs_Exp(exprel``{U})) (Abs_Exp(exprel``{V})) =
Abs_Exp (exprel``{PLUS U V})"
@@ -236,12 +236,12 @@
by (simp add: Plus_def UN_equiv_class2 [OF equiv_exprel equiv_exprel])
qed
-text{*It is not clear what to do with FnCall: it's argument is an abstraction
+text\<open>It is not clear what to do with FnCall: it's argument is an abstraction
of an @{typ "exp list"}. Is it just Nil or Cons? What seems to work best is to
-regard an @{typ "exp list"} as a @{term "listrel exprel"} equivalence class*}
+regard an @{typ "exp list"} as a @{term "listrel exprel"} equivalence class\<close>
-text{*This theorem is easily proved but never used. There's no obvious way
-even to state the analogous result, @{text FnCall_Cons}.*}
+text\<open>This theorem is easily proved but never used. There's no obvious way
+even to state the analogous result, @{text FnCall_Cons}.\<close>
lemma FnCall_Nil: "FnCall F [] = Abs_Exp (exprel``{FNCALL F []})"
by (simp add: FnCall_def)
@@ -273,13 +273,13 @@
qed
-text{*Establishing this equation is the point of the whole exercise*}
+text\<open>Establishing this equation is the point of the whole exercise\<close>
theorem Plus_assoc: "Plus X (Plus Y Z) = Plus (Plus X Y) Z"
by (cases X, cases Y, cases Z, simp add: Plus exprel.ASSOC)
-subsection{*The Abstract Function to Return the Set of Variables*}
+subsection\<open>The Abstract Function to Return the Set of Variables\<close>
definition
vars :: "exp \<Rightarrow> nat set" where
@@ -288,13 +288,13 @@
lemma vars_respects: "freevars respects exprel"
by (auto simp add: congruent_def exprel_imp_eq_freevars)
-text{*The extension of the function @{term vars} to lists*}
+text\<open>The extension of the function @{term vars} to lists\<close>
primrec vars_list :: "exp list \<Rightarrow> nat set" where
"vars_list [] = {}"
| "vars_list(E#Es) = vars E \<union> vars_list Es"
-text{*Now prove the three equations for @{term vars}*}
+text\<open>Now prove the three equations for @{term vars}\<close>
lemma vars_Variable [simp]: "vars (Var N) = {N}"
by (simp add: vars_def Var_def
@@ -320,12 +320,12 @@
by simp
-subsection{*Injectivity Properties of Some Constructors*}
+subsection\<open>Injectivity Properties of Some Constructors\<close>
lemma VAR_imp_eq: "VAR m \<sim> VAR n \<Longrightarrow> m = n"
by (drule exprel_imp_eq_freevars, simp)
-text{*Can also be proved using the function @{term vars}*}
+text\<open>Can also be proved using the function @{term vars}\<close>
lemma Var_Var_eq [iff]: "(Var m = Var n) = (m = n)"
by (auto simp add: Var_def exprel_refl dest: VAR_imp_eq)
@@ -344,7 +344,7 @@
apply (drule exprel_imp_eq_freediscrim, simp)
done
-subsection{*Injectivity of @{term FnCall}*}
+subsection\<open>Injectivity of @{term FnCall}\<close>
definition
"fun" :: "exp \<Rightarrow> nat" where
@@ -362,8 +362,8 @@
args :: "exp \<Rightarrow> exp list" where
"args X = the_elem (\<Union>U \<in> Rep_Exp X. {Abs_ExpList (freeargs U)})"
-text{*This result can probably be generalized to arbitrary equivalence
-relations, but with little benefit here.*}
+text\<open>This result can probably be generalized to arbitrary equivalence
+relations, but with little benefit here.\<close>
lemma Abs_ExpList_eq:
"(y, z) \<in> listrel exprel \<Longrightarrow> Abs_ExpList (y) = Abs_ExpList (z)"
by (induct set: listrel) simp_all
@@ -389,9 +389,9 @@
qed
-subsection{*The Abstract Discriminator*}
-text{*However, as @{text FnCall_Var_neq_Var} illustrates, we don't need this
-function in order to prove discrimination theorems.*}
+subsection\<open>The Abstract Discriminator\<close>
+text\<open>However, as @{text FnCall_Var_neq_Var} illustrates, we don't need this
+function in order to prove discrimination theorems.\<close>
definition
discrim :: "exp \<Rightarrow> int" where
@@ -400,7 +400,7 @@
lemma discrim_respects: "(\<lambda>U. {freediscrim U}) respects exprel"
by (auto simp add: congruent_def exprel_imp_eq_freediscrim)
-text{*Now prove the four equations for @{term discrim}*}
+text\<open>Now prove the four equations for @{term discrim}\<close>
lemma discrim_Var [simp]: "discrim (Var N) = 0"
by (simp add: discrim_def Var_def
@@ -419,7 +419,7 @@
done
-text{*The structural induction rule for the abstract type*}
+text\<open>The structural induction rule for the abstract type\<close>
theorem exp_inducts:
assumes V: "\<And>nat. P1 (Var nat)"
and P: "\<And>exp1 exp2. \<lbrakk>P1 exp1; P1 exp2\<rbrakk> \<Longrightarrow> P1 (Plus exp1 exp2)"
--- a/src/HOL/Induct/SList.thy Sat Jun 20 15:43:36 2015 +0200
+++ b/src/HOL/Induct/SList.thy Sat Jun 20 15:45:02 2015 +0200
@@ -21,7 +21,7 @@
datatype 'a m = Node 'a * 'a m list
*)
-section {* Extended List Theory (old) *}
+section \<open>Extended List Theory (old)\<close>
theory SList
imports Sexp
@@ -377,7 +377,7 @@
(* setting up rewrite sets *)
-text{*Better to have a single theorem with a conjunctive conclusion.*}
+text\<open>Better to have a single theorem with a conjunctive conclusion.\<close>
declare def_list_rec_NilCons [OF list_case_def, simp]
(** list_case **)
--- a/src/HOL/Induct/Sigma_Algebra.thy Sat Jun 20 15:43:36 2015 +0200
+++ b/src/HOL/Induct/Sigma_Algebra.thy Sat Jun 20 15:45:02 2015 +0200
@@ -2,17 +2,17 @@
Author: Markus Wenzel, TU Muenchen
*)
-section {* Sigma algebras *}
+section \<open>Sigma algebras\<close>
theory Sigma_Algebra
imports Main
begin
-text {*
+text \<open>
This is just a tiny example demonstrating the use of inductive
definitions in classical mathematics. We define the least @{text
\<sigma>}-algebra over a given set of sets.
-*}
+\<close>
inductive_set \<sigma>_algebra :: "'a set set => 'a set set" for A :: "'a set set"
where
@@ -21,11 +21,11 @@
| complement: "a \<in> \<sigma>_algebra A ==> -a \<in> \<sigma>_algebra A"
| Union: "(!!i::nat. a i \<in> \<sigma>_algebra A) ==> (\<Union>i. a i) \<in> \<sigma>_algebra A"
-text {*
+text \<open>
The following basic facts are consequences of the closure properties
of any @{text \<sigma>}-algebra, merely using the introduction rules, but
no induction nor cases.
-*}
+\<close>
theorem sigma_algebra_empty: "{} \<in> \<sigma>_algebra A"
proof -
--- a/src/HOL/Induct/Term.thy Sat Jun 20 15:43:36 2015 +0200
+++ b/src/HOL/Induct/Term.thy Sat Jun 20 15:45:02 2015 +0200
@@ -2,7 +2,7 @@
Author: Stefan Berghofer, TU Muenchen
*)
-section {* Terms over a given alphabet *}
+section \<open>Terms over a given alphabet\<close>
theory Term
imports Main
@@ -13,7 +13,7 @@
| App 'b "('a, 'b) term list"
-text {* \medskip Substitution function on terms *}
+text \<open>\medskip Substitution function on terms\<close>
primrec subst_term :: "('a => ('a, 'b) term) => ('a, 'b) term => ('a, 'b) term"
and subst_term_list :: "('a => ('a, 'b) term) => ('a, 'b) term list => ('a, 'b) term list"
@@ -24,7 +24,7 @@
| "subst_term_list f (t # ts) = subst_term f t # subst_term_list f ts"
-text {* \medskip A simple theorem about composition of substitutions *}
+text \<open>\medskip A simple theorem about composition of substitutions\<close>
lemma subst_comp:
"subst_term (subst_term f1 \<circ> f2) t =
@@ -34,7 +34,7 @@
by (induct t and ts rule: subst_term.induct subst_term_list.induct) simp_all
-text {* \medskip Alternative induction rule *}
+text \<open>\medskip Alternative induction rule\<close>
lemma
assumes var: "!!v. P (Var v)"
--- a/src/HOL/Induct/Tree.thy Sat Jun 20 15:43:36 2015 +0200
+++ b/src/HOL/Induct/Tree.thy Sat Jun 20 15:45:02 2015 +0200
@@ -3,7 +3,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
*)
-section {* Infinitely branching trees *}
+section \<open>Infinitely branching trees\<close>
theory Tree
imports Main
@@ -32,11 +32,11 @@
by (induct ts) auto
-subsection{*The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.*}
+subsection\<open>The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.\<close>
datatype brouwer = Zero | Succ "brouwer" | Lim "nat => brouwer"
-text{*Addition of ordinals*}
+text\<open>Addition of ordinals\<close>
primrec add :: "[brouwer,brouwer] => brouwer"
where
"add i Zero = i"
@@ -46,7 +46,7 @@
lemma add_assoc: "add (add i j) k = add i (add j k)"
by (induct k) auto
-text{*Multiplication of ordinals*}
+text\<open>Multiplication of ordinals\<close>
primrec mult :: "[brouwer,brouwer] => brouwer"
where
"mult i Zero = Zero"
@@ -59,14 +59,14 @@
lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
by (induct k) (auto simp add: add_mult_distrib)
-text{*We could probably instantiate some axiomatic type classes and use
-the standard infix operators.*}
+text\<open>We could probably instantiate some axiomatic type classes and use
+the standard infix operators.\<close>
-subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*}
+subsection\<open>A WF Ordering for The Brouwer ordinals (Michael Compton)\<close>
-text{*To use the function package we need an ordering on the Brouwer
+text\<open>To use the function package we need an ordering on the Brouwer
ordinals. Start with a predecessor relation and form its transitive
- closure. *}
+ closure.\<close>
definition brouwer_pred :: "(brouwer * brouwer) set"
where "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
@@ -86,7 +86,7 @@
lemma [simp]: "(f n, Lim f) : brouwer_order"
by(auto simp add: brouwer_order_def brouwer_pred_def)
-text{*Example of a general function*}
+text\<open>Example of a general function\<close>
function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
where