isabelle: src/HOL/Nominal/Examples/Class.thy@7e1f85ceb1a2 (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
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	24	thm trm_iter_set.intros[no_vars]
18881 c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	25
19319 7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	26	lemma it_total:
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	27	shows "\<exists>r. (t,r) \<in> trm_iter_set f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12"
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	28	by (induct t rule: trm.induct_weak, auto intro: trm_iter_set.intros)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	29
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	30	lemma it_prm_eq:
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	31	assumes a: "(t,y) \<in> trm_iter_set f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12"
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 *})+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	47	apply(simp_all)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	48	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	49	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	50	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	51	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	52	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	53	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	54	(* NotR *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	55	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	56	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	57	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	58	apply(tactic {* DatatypeAux.cong_tac 1 *})+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	59	apply(simp_all)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	60	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	61	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	62	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	63	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	64	(* NotL *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	65	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	66	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	67	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	68	apply(tactic {* DatatypeAux.cong_tac 1 *})+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	69	apply(simp_all)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	70	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	71	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	72	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	73	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	74	(* AndR *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	75	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	76	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	77	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	78	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	79	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	80	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	81	apply(tactic {* DatatypeAux.cong_tac 1 *})+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	82	apply(simp_all)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	83	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	84	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	85	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	86	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	87	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	88	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	89	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	90	(* AndL1 *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	91	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	92	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	93	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	94	apply(tactic {* DatatypeAux.cong_tac 1 *})+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	95	apply(simp_all)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	96	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	97	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	98	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	99	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	100	(* AndL1 *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	101	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	102	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	103	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	104	apply(tactic {* DatatypeAux.cong_tac 1 *})+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	105	apply(simp_all)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	106	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	107	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	108	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	109	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	110	(* OrR1 *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	111	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	112	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	113	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	114	apply(tactic {* DatatypeAux.cong_tac 1 *})+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	115	apply(simp_all)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	116	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	117	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	118	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	119	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	120	(* OrR2 *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	121	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	122	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	123	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	124	apply(tactic {* DatatypeAux.cong_tac 1 *})+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	125	apply(simp_all)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	126	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	127	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	128	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	129	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	130	(* OrL *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	131	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	132	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	133	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	134	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	135	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	136	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	137	apply(tactic {* DatatypeAux.cong_tac 1 *})+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	138	apply(simp_all)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	139	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	140	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	141	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	142	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	143	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	144	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	145	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	146	(* ImpR *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	147	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	148	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	149	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	150	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	151	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	152	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	153	apply(tactic {* DatatypeAux.cong_tac 1 *})+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	154	apply(simp_all)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	155	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	156	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	157	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	158	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	159	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	160	(* ImpL *)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	161	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	162	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	163	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	164	apply(rule_tac f="fresh_fun" in arg_cong)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	165	apply(simp add: expand_fun_eq)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	166	apply(rule allI)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	167	apply(tactic {* DatatypeAux.cong_tac 1 *})+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	168	apply(simp_all)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	169	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	170	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	171	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	172	apply(drule meta_spec)+
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	173	apply(drule meta_mp, erule_tac [2] meta_mp)
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	174	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	175	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	176	done
7e1f85ceb1a2 added the first two simple proofs of the recursion urbanc parents: 18881 diff changeset	177
18881 c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	178	text {* Induction principles *}
18395 87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	179
18881 c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	180	thm trm.induct_weak --"weak"
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	181	thm trm.induct --"strong"
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	182	thm trm.induct' --"strong with explicit context (rarely needed)"
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	183
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	184	text {* named terms *}
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	185
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	186	nominal_datatype ntrm = N "\<guillemotleft>name\<guillemotright>trm" ("N (_)._" [100,100] 100)
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	187
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	188	text {* conamed terms *}
18395 87217764cec2 initial commit (not to be seen by the public) urbanc parents: diff changeset	189
18881 c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	190	nominal_datatype ctrm = C "\<guillemotleft>coname\<guillemotright>trm" ("C <_>._" [100,100] 100)
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	191
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	192	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	193
18881 c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	194	consts
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	195	substn :: "trm \<Rightarrow> name \<Rightarrow> ctrm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100)
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	196	substc :: "trm \<Rightarrow> coname \<Rightarrow> ntrm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100)
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	197
c5f7cba2a675 added all constructors from PhD urbanc parents: 18661 diff changeset	198	text {* does not work yet *}

author	urbanc
	Wed, 22 Mar 2006 18:09:35 +0100
changeset 19319	7e1f85ceb1a2
parent 18881	c5f7cba2a675
child 19326	72e149c9caeb
permissions	-rw-r--r--