isabelle: src/HOL/Nominal/Examples/Class.thy@72e149c9caeb (annotated)

18425 bcf13dbaa339 I think the earlier version was completely broken urbanc parents: 18395 diff changeset	1
18661 dde117622dac updated to new induction principle urbanc parents: 18425 diff changeset	2	theory Class
18425 bcf13dbaa339 I think the earlier version was completely broken urbanc parents: 18395 diff changeset	3	imports "../nominal"
bcf13dbaa339 I think the earlier version was completely broken urbanc parents: 18395 diff changeset	4	begin
18395 87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	5
18881 c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	6	section {* Term-Calculus from Urban's PhD *}
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	7
18395 87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	8	atom_decl name coname
87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	9
18881 c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	10	nominal_datatype trm =
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	11	Ax "name" "coname"
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	12	\| Cut "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" ("Cut <_>._ [_]._" [100,100,100,100] 100)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	13	\| NotR "\<guillemotleft>name\<guillemotright>trm" "coname" ("NotR [_]._ _" [100,100,100] 100)
18881 c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	14	\| NotL "\<guillemotleft>coname\<guillemotright>trm" "name" ("NotL <_>._ _" [100,100,100] 100)
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	15	\| AndR "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>coname\<guillemotright>trm" "coname" ("AndR <_>._ <_>._ _" [100,100,100,100,100] 100)
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	16	\| AndL1 "\<guillemotleft>name\<guillemotright>trm" "name" ("AndL1 [_]._ _" [100,100,100] 100)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	17	\| AndL2 "\<guillemotleft>name\<guillemotright>trm" "name" ("AndL2 [_]._ _" [100,100,100] 100)
18881 c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	18	\| OrR1 "\<guillemotleft>coname\<guillemotright>trm" "coname" ("OrR1 <_>._ _" [100,100,100] 100)
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	19	\| OrR2 "\<guillemotleft>coname\<guillemotright>trm" "coname" ("OrR2 <_>._ _" [100,100,100] 100)
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	20	\| OrL "\<guillemotleft>name\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name" ("OrL [_]._ [_]._ _" [100,100,100,100,100] 100)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	21	\| ImpR "\<guillemotleft>name\<guillemotright>(\<guillemotleft>coname\<guillemotright>trm)" "coname" ("ImpR [_].<_>._ _" [100,100,100,100] 100)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	22	\| ImpL "\<guillemotleft>coname\<guillemotright>trm" "\<guillemotleft>name\<guillemotright>trm" "name" ("ImpL <_>._ [_]._ _" [100,100,100,100,100] 100)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	23
19326 72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	24	thm trm_rec_set.intros[no_vars]
18881 c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	25
19326 72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	26	lemma rec_total:
72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	27	shows "\<exists>r. (t,r) \<in> trm_rec_set f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12"
72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	28	by (induct t rule: trm.induct_weak, auto intro: trm_rec_set.intros)
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	29
19326 72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	30	lemma rec_prm_eq:
72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	31	assumes a: "(t,y) \<in> trm_rec_set f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12"
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	32	and b: "pi1 \<triangleq> pi2"
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	33	and c: "pi3 \<triangleq> pi4"
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	34	shows "y pi1 pi3 = y pi2 pi4"
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	35	using a b c
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	36	apply(induct fixing: pi1 pi2 pi3 pi4)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	37	(* axiom *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	38	apply(simp add: pt3[OF pt_name_inst] pt3[OF pt_coname_inst])
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	39	(* Cut *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	40	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	41	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	42	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	43	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	44	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	45	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	46	apply(tactic {* DatatypeAux.cong_tac 1 *})+
19326 72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	47	apply(simp_all add: pt2[OF pt_name_inst] pt2[OF pt_coname_inst]
72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	48	pt3[OF pt_name_inst] pt3[OF pt_coname_inst])
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	49	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	50	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	51	apply(rule at_prm_eq_append'[OF at_coname_inst], assumption, assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	52	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	53	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	54	apply(assumption, rule at_prm_eq_append'[OF at_name_inst], assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	55	(* NotR *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	56	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	57	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	58	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	59	apply(tactic {* DatatypeAux.cong_tac 1 *})+
19326 72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	60	apply(simp_all add: pt2[OF pt_name_inst] pt2[OF pt_coname_inst]
72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	61	pt3[OF pt_name_inst] pt3[OF pt_coname_inst])
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	62	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	63	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	64	apply(assumption, rule at_prm_eq_append'[OF at_name_inst], assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	65	(* NotL *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	66	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	67	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	68	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	69	apply(tactic {* DatatypeAux.cong_tac 1 *})+
19326 72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	70	apply(simp_all add: pt2[OF pt_name_inst] pt2[OF pt_coname_inst]
72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	71	pt3[OF pt_name_inst] pt3[OF pt_coname_inst])
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	72	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	73	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	74	apply(rule at_prm_eq_append'[OF at_coname_inst], assumption, assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	75	(* AndR *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	76	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	77	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	78	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	79	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	80	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	81	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	82	apply(tactic {* DatatypeAux.cong_tac 1 *})+
19326 72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	83	apply(simp_all add: pt2[OF pt_name_inst] pt2[OF pt_coname_inst]
72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	84	pt3[OF pt_name_inst] pt3[OF pt_coname_inst])
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	85	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	86	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	87	apply(rule at_prm_eq_append'[OF at_coname_inst], assumption, assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	88	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	89	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	90	apply(rule at_prm_eq_append'[OF at_coname_inst], assumption, assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	91	(* AndL1 *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	92	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	93	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	94	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	95	apply(tactic {* DatatypeAux.cong_tac 1 *})+
19326 72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	96	apply(simp_all add: pt2[OF pt_name_inst] pt2[OF pt_coname_inst]
72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	97	pt3[OF pt_name_inst] pt3[OF pt_coname_inst])
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	98	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	99	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	100	apply(assumption, rule at_prm_eq_append'[OF at_name_inst], assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	101	(* AndL1 *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	102	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	103	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	104	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	105	apply(tactic {* DatatypeAux.cong_tac 1 *})+
19326 72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	106	apply(simp_all add: pt2[OF pt_name_inst] pt2[OF pt_coname_inst]
72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	107	pt3[OF pt_name_inst] pt3[OF pt_coname_inst])
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	108	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	109	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	110	apply(assumption, rule at_prm_eq_append'[OF at_name_inst], assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	111	(* OrR1 *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	112	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	113	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	114	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	115	apply(tactic {* DatatypeAux.cong_tac 1 *})+
19326 72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	116	apply(simp_all add: pt2[OF pt_name_inst] pt2[OF pt_coname_inst]
72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	117	pt3[OF pt_name_inst] pt3[OF pt_coname_inst])
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	118	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	119	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	120	apply(rule at_prm_eq_append'[OF at_coname_inst], assumption, assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	121	(* OrR2 *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	122	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	123	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	124	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	125	apply(tactic {* DatatypeAux.cong_tac 1 *})+
19326 72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	126	apply(simp_all add: pt2[OF pt_name_inst] pt2[OF pt_coname_inst]
72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	127	pt3[OF pt_name_inst] pt3[OF pt_coname_inst])
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	128	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	129	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	130	apply(rule at_prm_eq_append'[OF at_coname_inst], assumption, assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	131	(* OrL *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	132	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	133	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	134	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	135	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	136	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	137	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	138	apply(tactic {* DatatypeAux.cong_tac 1 *})+
19326 72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	139	apply(simp_all add: pt2[OF pt_name_inst] pt2[OF pt_coname_inst]
72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	140	pt3[OF pt_name_inst] pt3[OF pt_coname_inst])
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	141	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	142	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	143	apply(assumption, rule at_prm_eq_append'[OF at_name_inst], assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	144	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	145	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	146	apply(assumption, rule at_prm_eq_append'[OF at_name_inst], assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	147	(* ImpR *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	148	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	149	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	150	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	151	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	152	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	153	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	154	apply(tactic {* DatatypeAux.cong_tac 1 *})+
19326 72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	155	apply(simp_all add: pt2[OF pt_name_inst] pt2[OF pt_coname_inst]
72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	156	pt3[OF pt_name_inst] pt3[OF pt_coname_inst])
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	157	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	158	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	159	apply(rule at_prm_eq_append'[OF at_coname_inst], assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	160	apply(rule at_prm_eq_append'[OF at_name_inst], assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	161	(* ImpL *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	162	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	163	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	164	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	165	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	166	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	167	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	168	apply(tactic {* DatatypeAux.cong_tac 1 *})+
19326 72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	169	apply(simp_all add: pt2[OF pt_name_inst] pt2[OF pt_coname_inst]
72e149c9caeb changed the it_prm proof to work for recursion urbanc parents: 19319 diff changeset	170	pt3[OF pt_name_inst] pt3[OF pt_coname_inst])
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	171	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	172	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	173	apply(rule at_prm_eq_append'[OF at_coname_inst], assumption, assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	174	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	175	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	176	apply(assumption, rule at_prm_eq_append'[OF at_name_inst], assumption)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	177	done
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	178
18881 c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	179	text {* Induction principles *}
18395 87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	180
18881 c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	181	thm trm.induct_weak --"weak"
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	182	thm trm.induct --"strong"
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	183	thm trm.induct' --"strong with explicit context (rarely needed)"
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	184
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	185	text {* named terms *}
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	186
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	187	nominal_datatype ntrm = N "\<guillemotleft>name\<guillemotright>trm" ("N (_)._" [100,100] 100)
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	188
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	189	text {* conamed terms *}
18395 87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	190
18881 c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	191	nominal_datatype ctrm = C "\<guillemotleft>coname\<guillemotright>trm" ("C <_>._" [100,100] 100)
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	192
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	193	text {* We should now define the two forms of substitition :o( *}
18395 87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	194
18881 c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	195	consts
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	196	substn :: "trm \<Rightarrow> name \<Rightarrow> ctrm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100)
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	197	substc :: "trm \<Rightarrow> coname \<Rightarrow> ntrm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100)
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	198
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	199	text {* does not work yet *}

author	urbanc
	Fri, 24 Mar 2006 15:59:16 +0100
changeset 19326	72e149c9caeb
parent 19319	7e1f85ceb1a2
child 19477	a95176d0f0dd
permissions	-rw-r--r--