isabelle: src/HOL/Lambda/ParRed.ML@10af4886b33f (annotated)

1288 6eb89a693e05 Improved a few proofs. nipkow parents: 1269 diff changeset	1	(* Title: HOL/Lambda/ParRed.ML
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	2	ID: $Id$
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	3	Author: Tobias Nipkow
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	4	Copyright 1995 TU Muenchen
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	5
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	6	Properties of => and cd, in particular the diamond property of => and
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	7	confluence of beta.
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	8	*)
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	9
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	10	open ParRed;
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	11
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1172 diff changeset	12	Addsimps par_beta.intrs;
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	13
2159 e650a3f6f600 Used nat_trans_tac. New Eta. various smaller changes. nipkow parents: 2057 diff changeset	14	val par_beta_cases = map (par_beta.mk_cases dB.simps)
e650a3f6f600 Used nat_trans_tac. New Eta. various smaller changes. nipkow parents: 2057 diff changeset	15	["Var n => t", "Abs s => Abs t",
e650a3f6f600 Used nat_trans_tac. New Eta. various smaller changes. nipkow parents: 2057 diff changeset	16	"(Abs s) @ t => u", "s @ t => u", "Abs s => t"];
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	17
1974 b50f96543dec Removed refs to clasets like rel_cs etc. Used implicit claset. nipkow parents: 1730 diff changeset	18	AddSIs par_beta.intrs;
b50f96543dec Removed refs to clasets like rel_cs etc. Used implicit claset. nipkow parents: 1730 diff changeset	19	AddSEs par_beta_cases;
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	20
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	21	(*** beta <= par_beta <= beta^* ***)
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	22
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	23	goal ParRed.thy "(Var n => t) = (t = Var n)";
2891 d8f254ad1ab9 Calls Blast_tac paulson parents: 2637 diff changeset	24	by (Blast_tac 1);
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	25	qed "par_beta_varL";
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1172 diff changeset	26	Addsimps [par_beta_varL];
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	27
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	28	goal ParRed.thy "t => t";
2159 e650a3f6f600 Used nat_trans_tac. New Eta. various smaller changes. nipkow parents: 2057 diff changeset	29	by (dB.induct_tac "t" 1);
2031 03a843f0f447 Ran expandshort paulson parents: 1974 diff changeset	30	by (ALLGOALS Asm_simp_tac);
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	31	qed"par_beta_refl";
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1172 diff changeset	32	Addsimps [par_beta_refl];
1974 b50f96543dec Removed refs to clasets like rel_cs etc. Used implicit claset. nipkow parents: 1730 diff changeset	33	(* AddSIs [par_beta_refl]; causes search to blow up *)
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	34
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	35	goal ParRed.thy "beta <= par_beta";
1465 5d7a7e439cec expanded tabs clasohm parents: 1431 diff changeset	36	by (rtac subsetI 1);
1431 be7c6d77e19c Polished proofs. nipkow parents: 1288 diff changeset	37	by (split_all_tac 1);
1730 1c7f793fc374 Updated for new form of induction rules paulson parents: 1486 diff changeset	38	by (etac beta.induct 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3207 diff changeset	39	by (ALLGOALS(blast_tac (claset() addSIs [par_beta_refl])));
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	40	qed "beta_subset_par_beta";
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	41
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	42	goal ParRed.thy "par_beta <= beta^*";
1465 5d7a7e439cec expanded tabs clasohm parents: 1431 diff changeset	43	by (rtac subsetI 1);
1431 be7c6d77e19c Polished proofs. nipkow parents: 1288 diff changeset	44	by (split_all_tac 1);
1730 1c7f793fc374 Updated for new form of induction rules paulson parents: 1486 diff changeset	45	by (etac par_beta.induct 1);
2922 580647a879cf Using Blast_tac paulson parents: 2891 diff changeset	46	by (Blast_tac 1);
580647a879cf Using Blast_tac paulson parents: 2891 diff changeset	47	(* rtrancl_refl complicates the proof by increasing the branching factor*)
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3207 diff changeset	48	by (ALLGOALS (blast_tac (claset() delrules [rtrancl_refl]
2922 580647a879cf Using Blast_tac paulson parents: 2891 diff changeset	49	addIs [rtrancl_into_rtrancl])));
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	50	qed "par_beta_subset_beta";
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	51
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	52	(* => *)
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	53
1172 ab725b698cb2 Renamed some vars. nipkow parents: 1156 diff changeset	54	goal ParRed.thy "!t' n. t => t' --> lift t n => lift t' n";
2159 e650a3f6f600 Used nat_trans_tac. New Eta. various smaller changes. nipkow parents: 2057 diff changeset	55	by (dB.induct_tac "t" 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3207 diff changeset	56	by (ALLGOALS(fast_tac (claset() addss (simpset()))));
1486 7b95d7b49f7a Introduced qed_spec_mp. nipkow parents: 1465 diff changeset	57	qed_spec_mp "par_beta_lift";
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1172 diff changeset	58	Addsimps [par_beta_lift];
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	59
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	60	goal ParRed.thy
1124 a6233ea105a4 Polished the presentation making it completely definitional. nipkow parents: 1120 diff changeset	61	"!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
2159 e650a3f6f600 Used nat_trans_tac. New Eta. various smaller changes. nipkow parents: 2057 diff changeset	62	by (dB.induct_tac "t" 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3207 diff changeset	63	by (asm_simp_tac (addsplit(simpset())) 1);
2057 4d7a4b25a11f Ran expandshort paulson parents: 2031 diff changeset	64	by (strip_tac 1);
4d7a4b25a11f Ran expandshort paulson parents: 2031 diff changeset	65	by (eresolve_tac par_beta_cases 1);
4d7a4b25a11f Ran expandshort paulson parents: 2031 diff changeset	66	by (Asm_simp_tac 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3207 diff changeset	67	by (asm_simp_tac (simpset() addsimps [subst_subst RS sym]) 1);
96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3207 diff changeset	68	by (fast_tac (claset() addSIs [par_beta_lift] addss (simpset())) 1);
96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3207 diff changeset	69	by (fast_tac (claset() addss (simpset())) 1);
1486 7b95d7b49f7a Introduced qed_spec_mp. nipkow parents: 1465 diff changeset	70	qed_spec_mp "par_beta_subst";
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	71
1156 b373cb33352f Put in direct proof of C-R w/o detour via cd. nipkow parents: 1124 diff changeset	72	(* Confluence (directly) *)
b373cb33352f Put in direct proof of C-R w/o detour via cd. nipkow parents: 1124 diff changeset	73
1269 ee011b365770 New version with eta reduction. nipkow parents: 1266 diff changeset	74	goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
1730 1c7f793fc374 Updated for new form of induction rules paulson parents: 1486 diff changeset	75	by (rtac (impI RS allI RS allI) 1);
1c7f793fc374 Updated for new form of induction rules paulson parents: 1486 diff changeset	76	by (etac par_beta.induct 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3207 diff changeset	77	by (ALLGOALS(blast_tac (claset() addSIs [par_beta_subst])));
1156 b373cb33352f Put in direct proof of C-R w/o detour via cd. nipkow parents: 1124 diff changeset	78	qed "diamond_par_beta";
b373cb33352f Put in direct proof of C-R w/o detour via cd. nipkow parents: 1124 diff changeset	79
b373cb33352f Put in direct proof of C-R w/o detour via cd. nipkow parents: 1124 diff changeset	80
b373cb33352f Put in direct proof of C-R w/o detour via cd. nipkow parents: 1124 diff changeset	81	(* cd *)
b373cb33352f Put in direct proof of C-R w/o detour via cd. nipkow parents: 1124 diff changeset	82
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	83	goal ParRed.thy "!t. s => t --> t => cd s";
2159 e650a3f6f600 Used nat_trans_tac. New Eta. various smaller changes. nipkow parents: 2057 diff changeset	84	by (dB.induct_tac "s" 1);
2057 4d7a4b25a11f Ran expandshort paulson parents: 2031 diff changeset	85	by (Simp_tac 1);
4d7a4b25a11f Ran expandshort paulson parents: 2031 diff changeset	86	by (etac rev_mp 1);
2159 e650a3f6f600 Used nat_trans_tac. New Eta. various smaller changes. nipkow parents: 2057 diff changeset	87	by (dB.induct_tac "dB1" 1);
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3207 diff changeset	88	by (ALLGOALS(fast_tac (claset() addSIs [par_beta_subst]
96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3207 diff changeset	89	addss (simpset()))));
1486 7b95d7b49f7a Introduced qed_spec_mp. nipkow parents: 1465 diff changeset	90	qed_spec_mp "par_beta_cd";
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	91
1156 b373cb33352f Put in direct proof of C-R w/o detour via cd. nipkow parents: 1124 diff changeset	92	(* Confluence (via cd) *)
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	93
1269 ee011b365770 New version with eta reduction. nipkow parents: 1266 diff changeset	94	goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
4089 96fba19bcbe2 isatool fixclasimp; wenzelm parents: 3207 diff changeset	95	by (blast_tac (claset() addIs [par_beta_cd]) 1);
1266 3ae9fe3c0f68 added local simpsets clasohm parents: 1172 diff changeset	96	qed "diamond_par_beta2";
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	97
ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	98	goal ParRed.thy "confluent(beta)";
2891 d8f254ad1ab9 Calls Blast_tac paulson parents: 2637 diff changeset	99	by (blast_tac (HOL_cs addIs [diamond_par_beta2, diamond_to_confluence,
d8f254ad1ab9 Calls Blast_tac paulson parents: 2637 diff changeset	100	par_beta_subset_beta, beta_subset_par_beta]) 1);
1120 ff7dd80513e6 Lambda calculus in de Bruijn notation. nipkow parents: diff changeset	101	qed"beta_confluent";

author	paulson
	Wed, 11 Mar 1998 11:03:43 +0100
changeset 4732	10af4886b33f
parent 4089	96fba19bcbe2
child 5069	3ea049f7979d
permissions	-rw-r--r--