theory Subtyping imports "../Nominal" XQuery Equivalence begin (* Move to XQuery *) lemma val_list_sng: "val_list_map SngV Vs = Vs" apply(nominal_induct Vs rule:val_val_list.strong_inducts(2)) apply(simp,auto) done (* All types nonempty. Move to XQuery *) lemma nonempty_types: "\ V. V : (\::ty)" "\ Vs. Vs :* \" apply(nominal_induct \ and \ rule:ty_regex_ty.strong_inducts) apply(auto intro: val_ty_val_list_ty.intros) done lemma sub_ty_elim: "\AtomTy \ \ AtomTy \'; V : \\ \ V : \'" "\\ \ \'; Vs :* \\ \ Vs :* \'" apply(erule sub_ty.cases,auto) apply(subgoal_tac "SngV V :* AtomTy \") prefer 2 apply(erule val_ty_val_list_ty.intros) apply(subgoal_tac "SngV V :* AtomTy \'") prefer 2 apply(blast) apply(erule val_ty_cases, simp add:val_list.inject regex_ty.inject)+ apply(erule sub_ty.cases,auto) done lemma equiv_ty_coerce: "\ \ \' \ \ \ \'" apply(auto simp add: equiv_ty_sub) done (* Congruences *) lemma sub_ty_alt_cong: "\\1 \ \1'; \2 \ \2'\ \ AltTy \1 \2 \ AltTy \1' \2'" apply(rule sub_ty_intro) apply(erule val_ty_cases) apply(simp add:regex_ty.inject,clarify) apply(rule st4, blast intro:sub_ty_elim) apply(simp add:regex_ty.inject,clarify) apply(rule st5, blast intro:sub_ty_elim) done lemma sub_ty_seq_cong: "\\1 \ \1'; \2 \ \2'\ \ SeqTy \1 \2 \ SeqTy \1' \2'" apply(rule sub_ty_intro) apply(erule val_ty_cases) apply(simp add:regex_ty.inject,clarify) apply(rule st3, auto intro:sub_ty_elim) done lemma sub_ty_elem_cong: "\\1 \ \2\ \ AtomTy (ElemTy l \1) \ AtomTy (ElemTy l \2)" apply(rule sub_ty_intro) apply(erule val_ty_cases) apply(simp add:regex_ty.inject,clarify) apply(rule st2[simplified]) apply(erule val_ty_cases) apply(simp add:ty.inject,clarify) apply(rule vt2) apply(blast intro:sub_ty_elim) done lemma sub_ty_star_cong: "\\1 \ \2\ \ StarTy \1 \ StarTy \2" apply(rule sub_ty_intro) apply(drule_tac F="SngV" and ty'=\2 in star_map) apply(simp_all add:val_list_sng sub_ty_elim) done (* Equivalence congruences *) lemma equiv_ty_seq_cong: "\\1 \ \1'; \2 \ \2'\ \ SeqTy \1 \2 \ SeqTy \1' \2' " by (auto simp add:equiv_ty_sub intro: sub_ty_seq_cong) lemma equiv_ty_alt_cong: "\\1 \ \1'; \2 \ \2'\ \ AltTy \1 \2 \ AltTy \1' \2' " by (auto simp add:equiv_ty_sub intro: sub_ty_alt_cong) lemma equiv_ty_star_cong: "\\1 \ \1'\ \ StarTy \1 \ StarTy \1'" by (auto simp add:equiv_ty_sub intro: sub_ty_star_cong) (* KLeene algebra laws *) (* Sequencing *) lemma sub_seq_assoc: "SeqTy(SeqTy \1 \2) \3 \ SeqTy \1 (SeqTy \2 \3)" apply(auto simp add: equiv_ty_sub) apply(rule sub_ty_intro) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(blast intro:val_ty_val_list_ty.intros) apply(rule sub_ty_intro) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) back apply(subgoal_tac "SeqV (SeqV V1 V1a) V2a :* SeqTy (SeqTy \1 \2) \3") prefer 2 apply(blast intro:val_ty_val_list_ty.intros) apply(simp) done lemma seq_unit_1: "SeqTy EmptyTy \ \ \" apply(auto simp add: equiv_ty_sub) apply(rule sub_ty_intro) apply(erule val_list_ty.cases, simp_all add:regex_ty.inject, clarify) apply(erule val_ty_cases,clarsimp) apply(rule sub_ty_intro) apply(subgoal_tac "SeqV NilV Vs :* SeqTy EmptyTy \") apply(simp) apply( blast intro: val_ty_val_list_ty.intros) done lemma seq_unit_2: "SeqTy \ EmptyTy \ \" apply(auto simp add: equiv_ty_sub) apply(rule sub_ty_intro) apply(erule val_list_ty.cases, simp_all add:regex_ty.inject, clarify) apply(erule val_ty_cases,clarsimp) apply(rule sub_ty_intro) apply(subgoal_tac "SeqV Vs NilV:* SeqTy \ EmptyTy") apply(simp) apply( blast intro: val_ty_val_list_ty.intros) done (* Alternative *) lemma sub_alt_comm: "AltTy \1 \2 \ AltTy \2 \1" apply(subgoal_tac "!!\1 \2 . AltTy \1 \2 \ AltTy \2 \1") apply(auto simp add: equiv_ty_sub) apply(rule sub_ty_intro) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(blast intro:val_ty_val_list_ty.intros) + done lemma sub_alt_assoc: "AltTy(AltTy \1 \2) \3 \ AltTy \1 (AltTy \2 \3)" apply(auto simp add: equiv_ty_sub) apply(rule sub_ty_intro) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(blast intro:val_ty_val_list_ty.intros)+ apply(rule sub_ty_intro) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(blast intro:val_ty_val_list_ty.intros) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(blast intro:val_ty_val_list_ty.intros) + done lemma alt_ub1: "\1 \ AltTy \1 \2" apply(rule sub_ty_intro) apply(erule val_ty_val_list_ty.intros) done lemma alt_ub2: "\2 \ AltTy \1 \2" apply(rule sub_ty_intro) apply(erule val_ty_val_list_ty.intros) done lemma alt_lub: "AltTy \1 \2 \ \ \ (\1 \ \ \ \2 \ \) " apply(auto) apply(rule sub_ty_intro) apply(erule sub_ty_elim) apply(erule val_ty_val_list_ty.intros) apply(rule sub_ty_intro) apply(erule sub_ty_elim) apply(erule val_ty_val_list_ty.intros) done lemma alt_idem: "AltTy \ \ \ \" apply(simp add:equiv_ty_sub) apply(auto) apply(rule sub_ty_intro) apply(erule val_ty_cases) apply(simp_all add:regex_ty.inject,clarsimp) apply(rule alt_ub1) done (* Distributivity *) lemma dist1: "SeqTy \1 (AltTy \2 \3) \ AltTy (SeqTy \1 \2 ) (SeqTy \1 \3)" apply(auto simp add: equiv_ty_sub) apply(rule sub_ty_intro) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) back apply(blast intro:val_ty_val_list_ty.intros) apply(blast intro:val_ty_val_list_ty.intros) apply(rule sub_ty_intro) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(blast intro:val_ty_val_list_ty.intros) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(blast intro:val_ty_val_list_ty.intros) done lemma dist2: "SeqTy (AltTy \1 \2) \3 \ AltTy (SeqTy \1 \3 ) (SeqTy \2 \3)" apply(auto simp add: equiv_ty_sub) apply(rule sub_ty_intro) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(blast intro:val_ty_val_list_ty.intros) apply(blast intro:val_ty_val_list_ty.intros) apply(rule sub_ty_intro) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(blast intro:val_ty_val_list_ty.intros) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(blast intro:val_ty_val_list_ty.intros) done lemma alt_elem: "AtomTy (ElemTy l (AltTy \1 \2)) \ AltTy (AtomTy (ElemTy l \1)) (AtomTy (ElemTy l \2))" apply(auto simp add: equiv_ty_sub) apply(rule sub_ty_intro) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(erule val_ty.cases,simp_all add:ty.inject,clarsimp) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(blast intro:val_ty_val_list_ty.intros[simplified]) + apply(rule sub_ty_intro) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(erule val_ty.cases,simp_all add:ty.inject,clarsimp) apply(blast intro:val_ty_val_list_ty.intros[simplified]) + apply(erule val_list_ty.cases,simp_all add:regex_ty.inject,clarsimp) apply(erule val_ty.cases,simp_all add:ty.inject,clarsimp) apply(blast intro:val_ty_val_list_ty.intros[simplified]) + done (* Star *) lemma unit_sub_star: "EmptyTy \ StarTy \" apply(rule sub_ty_intro) apply(erule val_ty_cases,blast intro: val_ty_val_list_ty.intros) done lemma self_sub_star: "\ \ StarTy \" apply(rule sub_ty_intro) apply(erule val_ty_val_list_ty.intros) done lemma seq_sub_star: "SeqTy (StarTy \) (StarTy \) \ StarTy \" apply(rule sub_ty_intro) apply(erule val_ty_cases,simp_all add:regex_ty.inject,clarsimp) apply(blast intro: val_ty_val_list_ty.intros) done lemma star_induction_helper: "\V :* StarTy \1;EmptyTy \ \2; \1 \ \2; SeqTy \2 \2 \ \2 \ \ V :* \2" apply(nominal_induct V \\"StarTy \1" rule: val_ty_val_list_ty.strong_inducts(2)) apply(simp,simp_all add:regex_ty.inject) apply(erule sub_ty_elim) apply(blast intro:val_ty_val_list_ty.intros) (* case 2 *) apply(clarsimp) apply(rule sub_ty_elim,simp_all) (* case 3 *) apply(clarsimp) apply(erule sub_ty_elim) back back apply(blast intro: val_ty_val_list_ty.intros) done lemma star_induction: "\EmptyTy \ \2; \1 \ \2; SeqTy \2 \2 \ \2 \ \ StarTy \1 \ \2" apply(rule sub_ty_intro) apply(blast intro:star_induction_helper) done (* Additional derived laws *) lemma sub_ty_star_seq: "\\1 \ StarTy \; \2 \ StarTy \\ \ SeqTy \1 \2 \ StarTy \" apply(rule sub_ty_trans) apply(rule sub_ty_seq_cong) apply(simp_all) apply(rule seq_sub_star) done lemma empty_not_sub_atom: " EmptyTy \ AtomTy \ \ False" apply(drule sub_ty_elim) apply(rule st1) apply(erule val_list_ty.cases) apply(auto) done lemma atom_not_sub_empty: "AtomTy \ \ EmptyTy \ False" "(\::regex_ty) = \ \ True" apply(nominal_induct \ and \ rule:ty_regex_ty.strong_inducts) apply(auto) apply(insert nonempty_types(2)) apply(drule_tac x=" regex_ty" in meta_spec,clarsimp) apply(drule sub_ty_elim) apply(rule val_ty_val_list_ty.intros)+ apply(blast) apply(erule val_list_ty.cases,simp_all) back apply(drule sub_ty_elim) apply(rule val_ty_val_list_ty.intros)+ apply(erule val_list_ty.cases,simp_all) apply(drule sub_ty_elim) apply(rule val_ty_val_list_ty.intros)+ apply(erule val_list_ty.cases,simp_all) done lemma star_sub_atom: "StarTy \ \ AtomTy \ \ \ \ AtomTy \ " apply(rule sub_ty_trans) apply(rule self_sub_star) apply(assumption) done (* Lemmas needed to prove that Empty is the only subtype of Empty up to equivalence *) lemma empty_in_sub_empty: "\ V :* \; \ \ EmptyTy\ \ V = NilV" apply(drule sub_ty_elim) apply(assumption) apply(erule val_ty_cases,simp) done lemma seq_sub_empty: "SeqTy \1 \2 \ EmptyTy \ (\1 \ EmptyTy \ \2 \ EmptyTy )" apply(auto) apply(rule sub_ty_intro) apply(subgoal_tac "\ Vs'. Vs' :* \2") prefer 2 apply(rule nonempty_types) apply(clarify) apply(subgoal_tac "SeqV Vs Vs' = NilV") prefer 2 apply(rule empty_in_sub_empty) apply(blast intro: val_ty_val_list_ty.intros) apply(simp) apply(frule seqv_nil_inv1) apply(blast intro: val_ty_val_list_ty.intros) apply(rule sub_ty_intro) apply(subgoal_tac "\ Vs'. Vs' :* \1") prefer 2 apply(rule nonempty_types) apply(clarify) apply(subgoal_tac "SeqV Vs' Vs = NilV") prefer 2 apply(rule empty_in_sub_empty) apply(blast intro: val_ty_val_list_ty.intros) apply(simp) apply(frule seqv_nil_inv2) apply(blast intro: val_ty_val_list_ty.intros) done lemma alt_sub_empty: "AltTy \1 \2 \ EmptyTy \ (\1 \ EmptyTy \ \2 \ EmptyTy )" apply(auto) apply(rule sub_ty_intro) apply(erule sub_ty_elim) apply(blast intro:val_ty_val_list_ty.intros) apply(rule sub_ty_intro) apply(erule sub_ty_elim) apply(blast intro:val_ty_val_list_ty.intros) done lemma star_sub_empty: "StarTy \1 \ EmptyTy \ (\1 \ EmptyTy )" apply(rule sub_ty_intro) apply(erule sub_ty_elim) apply(blast intro:val_ty_val_list_ty.intros) done lemma equiv_ty_star_empty: "StarTy EmptyTy \ EmptyTy" apply(simp add: equiv_ty_sub, auto) apply(rule star_induction,auto intro: sub_ty_refl equiv_ty_coerce seq_unit_1) apply(rule unit_sub_star) done theorem sub_ty_empty_inv: "\ \ EmptyTy \ \ \ EmptyTy" apply(nominal_induct \ rule:ty_regex_ty.strong_inducts(2)) apply(simp, auto) apply(rule equiv_ty_refl) (* Atom *) apply(blast dest:atom_not_sub_empty) (* Seq *) apply(drule seq_sub_empty) apply(clarsimp) apply(rule equiv_ty_trans) apply(erule equiv_ty_seq_cong,assumption) apply(rule seq_unit_1) (* Alt *) apply(drule alt_sub_empty) apply(clarsimp) apply(rule equiv_ty_trans) apply(rule equiv_ty_alt_cong) apply(assumption+) apply(rule alt_idem) (* Star *) apply(drule star_sub_empty) apply(clarsimp) apply(rule equiv_ty_trans) apply(erule equiv_ty_star_cong) apply(rule equiv_ty_star_empty) done (* Type-based optimizations. E.g., if the target of a conditional or for loop has type <: EmptyTy then we can simplify. *) lemma empty_ty_equiv_empty: "\\ \ E \; \ \ E : EmptyTy\ \ \ \ E \ Empty" apply(rule op_equiv_intro) apply(auto) apply(drule soundness,simp_all) apply(erule val_ty_cases,simp) apply(blast intro: ctx_wf_valid_sub eval_evals.intros) (* \ *) apply(drule converges_elim) apply(simp) apply(clarsimp) apply(drule soundness,simp_all) apply(erule val_ty_cases,simp) apply(erule eval.cases,simp_all) done lemma equiv_empty_ty: "\\ \ E \ ; \ \ E : \; \ \ EmptyTy\ \ \ \ E \ Empty" apply(frule empty_ty_equiv_empty) apply(erule wf_sub) apply(simp_all) done lemma cond_empty_ty: "\\ \ E \ ; \ \ E : \; \ \ EmptyTy\ \ \ \ Cond E E1 E2 \ E2" apply(rule op_equiv_trans) apply(rule cond_congr) apply(rule equiv_empty_ty) apply(simp_all) apply(rule op_equiv_refl)+ apply(rule cond_empty) done lemma for_empty_ty: "\\ \ E1 \; \ \ E1 : \; \ \ EmptyTy; x\ (\,E1)\ \ \ \ For E1 x E2 \ Empty" apply(rule op_equiv_trans) apply(rule for_congr) apply(rule equiv_empty_ty) apply(simp_all) apply(rule op_equiv_refl)+ apply(rule for_empty) apply(simp) done end