# HG changeset patch # User wenzelm # Date 1451503483 -3600 # Node ID 89206877f0ee1f3cc7121989aaf25431aa4a2a3d # Parent 6d02bb8b5fe12000d4c5d7941d4bc59232f18fd4 more symbols; diff -r 6d02bb8b5fe1 -r 89206877f0ee src/HOL/Induct/Comb.thy --- a/src/HOL/Induct/Comb.thy Wed Dec 30 20:12:26 2015 +0100 +++ b/src/HOL/Induct/Comb.thy Wed Dec 30 20:24:43 2015 +0100 @@ -18,53 +18,47 @@ subsection \Definitions\ -text \Datatype definition of combinators @{text S} and @{text K}.\ +text \Datatype definition of combinators \S\ and \K\.\ datatype comb = K | S - | Ap comb comb (infixl "##" 90) - -notation (xsymbols) - Ap (infixl "\" 90) - + | Ap comb comb (infixl "\" 90) text \ - Inductive definition of contractions, @{text "-1->"} and - (multi-step) reductions, @{text "--->"}. + Inductive definition of contractions, \\\<^sup>1\ and + (multi-step) reductions, \\\. \ -inductive_set - contract :: "(comb*comb) set" - and contract_rel1 :: "[comb,comb] => bool" (infixl "-1->" 50) - where - "x -1-> y == (x,y) \ contract" - | K: "K##x##y -1-> x" - | S: "S##x##y##z -1-> (x##z)##(y##z)" - | Ap1: "x-1->y ==> x##z -1-> y##z" - | Ap2: "x-1->y ==> z##x -1-> z##y" +inductive_set contract :: "(comb*comb) set" + and contract_rel1 :: "[comb,comb] \ bool" (infixl "\\<^sup>1" 50) +where + "x \\<^sup>1 y == (x,y) \ contract" +| K: "K\x\y \\<^sup>1 x" +| S: "S\x\y\z \\<^sup>1 (x\z)\(y\z)" +| Ap1: "x\\<^sup>1y \ x\z \\<^sup>1 y\z" +| Ap2: "x\\<^sup>1y \ z\x \\<^sup>1 z\y" abbreviation - contract_rel :: "[comb,comb] => bool" (infixl "--->" 50) where - "x ---> y == (x,y) \ contract^*" + contract_rel :: "[comb,comb] \ bool" (infixl "\" 50) where + "x \ y == (x,y) \ contract\<^sup>*" text \ - Inductive definition of parallel contractions, @{text "=1=>"} and - (multi-step) parallel reductions, @{text "===>"}. + Inductive definition of parallel contractions, \\\<^sup>1\ and + (multi-step) parallel reductions, \\\. \ -inductive_set - parcontract :: "(comb*comb) set" - and parcontract_rel1 :: "[comb,comb] => bool" (infixl "=1=>" 50) - where - "x =1=> y == (x,y) \ parcontract" - | refl: "x =1=> x" - | K: "K##x##y =1=> x" - | S: "S##x##y##z =1=> (x##z)##(y##z)" - | Ap: "[| x=1=>y; z=1=>w |] ==> x##z =1=> y##w" +inductive_set parcontract :: "(comb*comb) set" + and parcontract_rel1 :: "[comb,comb] \ bool" (infixl "\\<^sup>1" 50) +where + "x \\<^sup>1 y == (x,y) \ parcontract" +| refl: "x \\<^sup>1 x" +| K: "K\x\y \\<^sup>1 x" +| S: "S\x\y\z \\<^sup>1 (x\z)\(y\z)" +| Ap: "[| x\\<^sup>1y; z\\<^sup>1w |] ==> x\z \\<^sup>1 y\w" abbreviation - parcontract_rel :: "[comb,comb] => bool" (infixl "===>" 50) where - "x ===> y == (x,y) \ parcontract^*" + parcontract_rel :: "[comb,comb] \ bool" (infixl "\" 50) where + "x \ y == (x,y) \ parcontract\<^sup>*" text \ Misc definitions. @@ -72,11 +66,11 @@ definition I :: comb where - "I = S##K##K" + "I = S\K\K" definition - diamond :: "('a * 'a)set => bool" where - --\confluence; Lambda/Commutation treats this more abstractly\ + diamond :: "('a * 'a)set \ bool" where + \\confluence; Lambda/Commutation treats this more abstractly\ "diamond(r) = (\x y. (x,y) \ r --> (\y'. (x,y') \ r --> (\z. (y,z) \ r & (y',z) \ r)))" @@ -89,15 +83,15 @@ text\Strip lemma. The induction hypothesis covers all but the last diamond of the strip.\ lemma diamond_strip_lemmaE [rule_format]: - "[| diamond(r); (x,y) \ r^* |] ==> - \y'. (x,y') \ r --> (\z. (y',z) \ r^* & (y,z) \ r)" + "[| diamond(r); (x,y) \ r\<^sup>* |] ==> + \y'. (x,y') \ r --> (\z. (y',z) \ r\<^sup>* & (y,z) \ r)" apply (unfold diamond_def) apply (erule rtrancl_induct) apply (meson rtrancl_refl) apply (meson rtrancl_trans r_into_rtrancl) done -lemma diamond_rtrancl: "diamond(r) ==> diamond(r^*)" +lemma diamond_rtrancl: "diamond(r) \ diamond(r\<^sup>*)" apply (simp (no_asm_simp) add: diamond_def) apply (rule impI [THEN allI, THEN allI]) apply (erule rtrancl_induct, blast) @@ -110,30 +104,30 @@ text \Derive a case for each combinator constructor.\ inductive_cases - K_contractE [elim!]: "K -1-> r" - and S_contractE [elim!]: "S -1-> r" - and Ap_contractE [elim!]: "p##q -1-> r" + K_contractE [elim!]: "K \\<^sup>1 r" + and S_contractE [elim!]: "S \\<^sup>1 r" + and Ap_contractE [elim!]: "p\q \\<^sup>1 r" declare contract.K [intro!] contract.S [intro!] declare contract.Ap1 [intro] contract.Ap2 [intro] -lemma I_contract_E [elim!]: "I -1-> z ==> P" +lemma I_contract_E [elim!]: "I \\<^sup>1 z \ P" by (unfold I_def, blast) -lemma K1_contractD [elim!]: "K##x -1-> z ==> (\x'. z = K##x' & x -1-> x')" +lemma K1_contractD [elim!]: "K\x \\<^sup>1 z \ (\x'. z = K\x' & x \\<^sup>1 x')" by blast -lemma Ap_reduce1 [intro]: "x ---> y ==> x##z ---> y##z" +lemma Ap_reduce1 [intro]: "x \ y \ x\z \ y\z" apply (erule rtrancl_induct) apply (blast intro: rtrancl_trans)+ done -lemma Ap_reduce2 [intro]: "x ---> y ==> z##x ---> z##y" +lemma Ap_reduce2 [intro]: "x \ y \ z\x \ z\y" apply (erule rtrancl_induct) apply (blast intro: rtrancl_trans)+ done -text \Counterexample to the diamond property for @{term "x -1-> y"}\ +text \Counterexample to the diamond property for @{term "x \\<^sup>1 y"}\ lemma not_diamond_contract: "~ diamond(contract)" by (unfold diamond_def, metis S_contractE contract.K) @@ -144,9 +138,9 @@ text \Derive a case for each combinator constructor.\ inductive_cases - K_parcontractE [elim!]: "K =1=> r" - and S_parcontractE [elim!]: "S =1=> r" - and Ap_parcontractE [elim!]: "p##q =1=> r" + K_parcontractE [elim!]: "K \\<^sup>1 r" + and S_parcontractE [elim!]: "S \\<^sup>1 r" + and Ap_parcontractE [elim!]: "p\q \\<^sup>1 r" declare parcontract.intros [intro] @@ -154,14 +148,14 @@ subsection \Basic properties of parallel contraction\ -lemma K1_parcontractD [dest!]: "K##x =1=> z ==> (\x'. z = K##x' & x =1=> x')" +lemma K1_parcontractD [dest!]: "K\x \\<^sup>1 z \ (\x'. z = K\x' & x \\<^sup>1 x')" by blast -lemma S1_parcontractD [dest!]: "S##x =1=> z ==> (\x'. z = S##x' & x =1=> x')" +lemma S1_parcontractD [dest!]: "S\x \\<^sup>1 z \ (\x'. z = S\x' & x \\<^sup>1 x')" by blast lemma S2_parcontractD [dest!]: - "S##x##y =1=> z ==> (\x' y'. z = S##x'##y' & x =1=> x' & y =1=> y')" + "S\x\y \\<^sup>1 z \ (\x' y'. z = S\x'\y' & x \\<^sup>1 x' & y \\<^sup>1 y')" by blast text\The rules above are not essential but make proofs much faster\ @@ -174,10 +168,11 @@ done text \ - \medskip Equivalence of @{prop "p ---> q"} and @{prop "p ===> q"}. + \<^medskip> + Equivalence of @{prop "p \ q"} and @{prop "p \ q"}. \ -lemma contract_subset_parcontract: "contract <= parcontract" +lemma contract_subset_parcontract: "contract \ parcontract" by (auto, erule contract.induct, blast+) text\Reductions: simply throw together reflexivity, transitivity and @@ -186,16 +181,16 @@ declare r_into_rtrancl [intro] rtrancl_trans [intro] (*Example only: not used*) -lemma reduce_I: "I##x ---> x" +lemma reduce_I: "I\x \ x" by (unfold I_def, blast) -lemma parcontract_subset_reduce: "parcontract <= contract^*" +lemma parcontract_subset_reduce: "parcontract \ contract\<^sup>*" by (auto, erule parcontract.induct, blast+) -lemma reduce_eq_parreduce: "contract^* = parcontract^*" +lemma reduce_eq_parreduce: "contract\<^sup>* = parcontract\<^sup>*" by (metis contract_subset_parcontract parcontract_subset_reduce rtrancl_subset) -theorem diamond_reduce: "diamond(contract^*)" +theorem diamond_reduce: "diamond(contract\<^sup>*)" by (simp add: reduce_eq_parreduce diamond_rtrancl diamond_parcontract) end diff -r 6d02bb8b5fe1 -r 89206877f0ee src/HOL/Induct/document/root.tex --- a/src/HOL/Induct/document/root.tex Wed Dec 30 20:12:26 2015 +0100 +++ b/src/HOL/Induct/document/root.tex Wed Dec 30 20:24:43 2015 +0100 @@ -1,5 +1,5 @@ - \documentclass[11pt,a4paper]{article} +\usepackage{amssymb} \usepackage{isabelle,isabellesym,pdfsetup} %for best-style documents ...