theory Codatatype_Witnesses
imports
"../code/BNF_Nonuniform_Fixpoint"
"~~/src/HOL/Library/BNF_Axiomatization"
begin
declare [[bnf_internals,typedef_overloaded]]
bnf_axiomatization ('a0,'a1,'T0,'T1) GG
[wits: "'a0 ⇒ 'T1 ⇒ ('a0,'a1,'T0,'T1) GG"
"'a1 ⇒ 'T0 ⇒ ('a0,'a1,'T0,'T1) GG"
"'a0 ⇒ 'a1 ⇒ 'T0 ⇒ 'T1 ⇒ ('a0,'a1,'T0,'T1) GG"
]
bnf_axiomatization ('a0,'a1) FF1_1
[wits: "'a0 ⇒ ('a0,'a1) FF1_1" "'a1 ⇒ ('a0,'a1) FF1_1"]
bnf_axiomatization ('a0,'a1) FF1_2
[wits: "'a0 ⇒ 'a1 ⇒ ('a0,'a1) FF1_2"]
bnf_axiomatization ('a0,'a1) FF2_1
[wits: "'a0 ⇒ ('a0,'a1) FF2_1"]
bnf_axiomatization ('a0,'a1) FF2_2
[wits: "'a0 ⇒ ('a0,'a1) FF2_2"]
nonuniform_codatatype
('a0, 'a1) T = C "('a0, 'a1, (('a0, 'a1) FF1_1, ('a0, 'a1) FF1_2) T, (('a0, 'a1) FF2_1, ('a0, 'a1) FF2_2) T) GG"
type_synonym depth = "label_T list"
abbreviation "L1 ≡ T.L_2_T"
abbreviation "L2 ≡ T.L_1_T"
datatype witposFs = A0 | A1
datatype witposG = AA0 | AA1 | T0 | T1
definition "nwitsG ≡ 3"
definition "nwitsF1_1 ≡ 2" definition "nwitsF1_2 ≡ 1"
definition "nwitsF2_1 ≡ 1" definition "nwitsF2_2 ≡ 1"
declare numeral_2_eq_2[simp]
lemmas nwits_defs = nwitsG_def
nwitsF1_1_def nwitsF1_2_def
nwitsF2_1_def nwitsF2_2_def
fun wp_G where
"wp_G 0 = {AA0,T1}"
| "wp_G (Suc 0) = {AA1,T0}"
| "wp_G (Suc (Suc 0)) = {AA0,AA1,T0,T1}"
fun wp_F1_1 where
"wp_F1_1 0 = {A0}"
| "wp_F1_1 (Suc 0) = {A1}"
fun wp_F1_2 where
"wp_F1_2 (0 :: nat) = {A0,A1}"
fun wp_F2_1 where "wp_F2_1 (0 :: nat) = {A0}"
fun wp_F2_2 where "wp_F2_2 (0 :: nat) = {A0}"
fun trans :: "witposFs set ⇒ label_T × nat × nat × nat ⇒
witposFs set ⇒ bool"
where
"trans S (L1,i,i_1,i_2) S' ⟷
i < nwitsG ∧ i_1 < nwitsF1_1 ∧ i_2 < nwitsF1_2 ∧
(AA0 ∈ wp_G i ⟶ A0 ∈ S) ∧
(AA1 ∈ wp_G i ⟶ A1 ∈ S) ∧
S' = {x . x = A0 ∧ wp_F1_1 i_1 ⊆ S} ∪
{x . x = A1 ∧ wp_F1_2 i_2 ⊆ S}"
|"trans S (L2,i,i_1,i_2) S' ⟷
i < nwitsG ∧ i_1 < nwitsF2_1 ∧ i_2 < nwitsF2_2 ∧
(AA0 ∈ wp_G i ⟶ A0 ∈ S) ∧
(AA1 ∈ wp_G i ⟶ A1 ∈ S) ∧
S' = {x . x = A0 ∧ wp_F2_1 i_1 ⊆ S} ∪
{x . x = A1 ∧ wp_F2_2 i_2 ⊆ S}"
definition "S1 ≡ {A1}"
definition "S0 ≡ {A0}"
definition "S01 ≡ {A0,A1}"
lemmas S_defs = S1_def S0_def S01_def
lemma
"trans S1 (L1,1,1,0) S0"
"trans S0 (L2,0,0,0) S01"
"trans S01 (L1,2,0,0) S01"
"trans S01 (L2,1,0,0) S01"
by (auto simp: nwits_defs S_defs)
inductive
is_S1 :: "depth ⇒ bool" and
is_S0 :: "depth ⇒ bool" and
is_S01 :: "depth ⇒ bool"
where
"is_S1 []"
| "is_S1 u ⟹ is_S0 (L1 # u)"
| "is_S0 u ⟹ is_S01 (L2 # u)"
| "is_S01 u ⟹ is_S01 (L1 # u)"
| "is_S01 u ⟹ is_S01 (L2 # u)"
definition "is_S u = (is_S1 u ∨ is_S0 u ∨ is_S01 u)"
lemmas is_S_Nil = is_S_def[of "[]", unfolded is_S1.simps simp_thms]
context
fixes dummy :: "'a0 × 'a1"
and a1 :: 'a1
begin
definition pred1 :: "depth ⇒ ('a0, 'a1) shape_1_T ⇒ bool" where
"pred1 u sh1 = (T.invar_shape_1_T u sh1 ∧ pred_shape_1_T (λ_. False) (λx. x = a1) sh1)"
definition pred2 :: "depth ⇒ ('a0, 'a1) shape_2_T ⇒ bool" where
"pred2 u sh2 = (T.invar_shape_2_T u sh2 ∧ pred_shape_2_T (λ_. False) (λx. x = a1) sh2)"
abbreviation "spred u g ≡
pred_pre_T (pred1 u) (pred2 u) (λu'. u' = L2 # u ∧ is_S u') (λu'. u' = L1 # u ∧ is_S u') g"
definition "wcoalg u = Eps (spred u)"
primcorec wit :: "depth ⇒ ('a0,'a1) raw_T" where
"wit u = T.raw_T.Ctor_T (map_pre_T id id wit wit (wcoalg u))"
lemma is_pred_S:
"(is_S1 u ⟶(∃sh2::('a0,'a1) shape_2_T. pred2 u sh2)) ∧
(is_S0 u ⟶ (∃sh1::('a0,'a1) shape_1_T. pred1 u sh1)) ∧
(is_S01 u ⟶ (∃sh1::('a0,'a1) shape_1_T. pred1 u sh1) ∧ (∃sh2::('a0,'a1) shape_2_T. pred2 u sh2))"
apply (rule is_S1_is_S0_is_S01.induct; unfold pred1_def[abs_def] pred2_def[abs_def];
((erule exE conjE)+)?; (rule conjI)?)
apply (rule
exI[of _ "T.shape_1_T.leaf_T _"]
exI[of _ "T.shape_2_T.leaf_T _"]
exI[of _ "T.shape_1_T.node_1_T (arg.wit1_pre_T_1_0 _)"]
exI[of _ "T.shape_1_T.node_1_T (arg.wit2_pre_T_1_0 _)"]
exI[of _ "T.shape_2_T.node_1_T (arg.wit_pre_T_1_1 _ _)"]
exI[of _ "T.shape_1_T.node_0_T (arg.wit_pre_T_0_0 _)"]
exI[of _ "T.shape_2_T.node_0_T (arg.wit_pre_T_0_1 _)"],
((hypsubst | assumption | drule
arg.arg.pre_T_0_0.wit
arg.arg.pre_T_0_1.wit
arg.arg.pre_T_1_0.wit1
arg.arg.pre_T_1_0.wit2
arg.arg.pre_T_1_1.wit | (rule conjI ballI)+ | simp only:
list.case simp_thms if_True if_False label_T.distinct
T.invar_shape_1_T.simps T.invar_shape_2_T.simps
shape_1_T.pred_inject shape_2_T.pred_inject
arg.arg.pre_T_0_0.pred_set
arg.arg.pre_T_0_1.pred_set
arg.arg.pre_T_1_0.pred_set
arg.arg.pre_T_1_1.pred_set)+; fail) [])+
done
lemmas is_pred_S1 = is_pred_S[THEN conjunct1, rule_format]
lemmas is_pred_S0 = is_pred_S[THEN conjunct2, THEN conjunct1, rule_format]
lemmas is_pred_S01 = is_pred_S[THEN conjunct2, THEN conjunct2, rule_format]
lemma is_S_closed:
"is_S u ⟹ spred u (wcoalg u)"
unfolding is_S_def wcoalg_def
apply (rule someI_ex)
apply (elim disjE; frule is_pred_S1 is_pred_S0 is_pred_S01; unfold pre_T.pred_set; (erule conjE exE)+)
apply (rule exI[of _ "wit1_pre_T _ _"] exI[of _ "wit2_pre_T _ _"] exI[of _ "wit3_pre_T _ _"],
((hypsubst | assumption | drule pre_T.wit1 pre_T.wit2 pre_T.wit3 | rule conjI ballI |
simp only: is_S1_is_S0_is_S01.intros list.simps simp_thms)+; fail))+
done
lemma pred_raw_T_wit: "is_S u ⟹ pred_raw_T (λ_. False) (λx. x = a1) (wit u)"
apply (rule raw_T.rel_coinduct[THEN iffD2[OF raw_T.pred_rel],
of "eq_onp (λx. ∃u. x = wit u ∧ is_S u)"])
apply (unfold eq_onp_def simp_thms)
apply (rule exI conjI refl)+
apply assumption
apply (erule thin_rl)
apply (erule exE conjE)+
apply hypsubst_thin
apply (drule is_S_closed)
apply (unfold pre_T.pred_rel shape_1_T.pred_rel shape_2_T.pred_rel wit.sel pre_T.rel_map
id_apply eq_onp_def pred1_def pred2_def)
apply (erule pre_T.rel_mono_strong)
apply (erule conjE)+
apply hypsubst_thin
apply (erule shape_1_T.rel_mono_strong; (erule conjunct1 | assumption))
apply (erule conjE)+
apply hypsubst_thin
apply (erule shape_2_T.rel_mono_strong; (erule conjunct1 | assumption))
apply (erule exE conjE)+
apply hypsubst_thin
apply ((rule exI conjI refl | assumption)+) []
apply (erule exE conjE)+
apply hypsubst_thin
apply ((rule exI conjI refl | assumption)+) []
done
lemma invar_wit: "is_S u ⟹ T.invar_raw_T u (wit u)"
apply (rule invar_raw_T.coinduct[of "λu' w. ∃u. u' = u ∧ w = wit u ∧ is_S u"])
apply (rule exI conjI refl)+
apply assumption
apply (erule thin_rl)
apply (erule exE conjE)+
apply hypsubst_thin
apply (rule exI conjI refl)+
apply (rule wit.ctr)
apply (drule is_S_closed)
apply (unfold pre_T.pred_map)
apply (erule pre_T.pred_mono_strong)
apply (unfold id_apply o_apply pred1_def)
apply (erule conjunct1)
apply (unfold id_apply o_apply pred2_def)
apply (erule conjunct1)
apply (erule conjE)
apply hypsubst_thin
apply (rule disjI1)
apply (rule exI conjI refl)+
apply assumption
apply (erule conjE)
apply hypsubst_thin
apply (rule disjI1)
apply (rule exI conjI refl)+
apply assumption
done
lemmas invar_wit_Nil = invar_wit[OF is_S_Nil]
lemmas T_wit_Nil =
pred_raw_T_wit[OF is_S_Nil, unfolded raw_T.pred_set, THEN conjunct1, THEN bspec]
pred_raw_T_wit[OF is_S_Nil, unfolded raw_T.pred_set, THEN conjunct2, THEN bspec]
end
end