theory Spi_LDI_DC imports Spi_DI_DC begin (* to do with the earlier rules for deducibility constraint system reduction, independent of the deduction system involved *) (* conditions for a deducibility constraint system *) consts lhs_ord :: "'n ldc list => bool" ldcrC45 :: "'n mlred" ldcrC45p :: "'n msg => 'n msg => 'n mlred" ldcrC45e :: "'n mlred" ldcrC345e :: "'n mlred" recdef "lhs_ord" "measure size" "lhs_ord [] = True" "lhs_ord ((flag, S, M) # Cs) = (lhs_ord Cs & (flag | (ALL (flag', S', M') : set Cs. S' <= S)))" primrec "adjreg exa exb (flag, con) = (if flag then (True, con) else (False, case con of (S, M) => (insert exa (insert exb S), M)))" inductive "ldcrC45p Mx My" intros plI : "Mpair Mx My : S ==> Not ({Mx, My} <= S) ==> (map (adjreg Mx My) A @ (False, insert Mx (insert My S), U) # Cs, A @ (False, S, U) # Cs) : ldcrC45p Mx My" elI : "Enc Mx My : S ==> Not ({Mx, My} <= S) ==> (map (adjreg Mx My) A @ (False, insert Mx (insert My S), U) # (True, S, My) # Cs, A @ (False, S, U) # Cs) : ldcrC45p Mx My" inductive "ldcrC45" intros plI : "Mpair Ma Mb : S ==> Not ({Ma, Mb} <= S) ==> (map (adjreg Ma Mb) A @ (False, insert Ma (insert Mb S), U) # Cs, A @ (False, S, U) # Cs) : ldcrC45" elI : "Enc Mp Mk : S ==> Not ({Mp, Mk} <= S) ==> (map (adjreg Mp Mk) A @ (False, insert Mp (insert Mk S), U) # (True, S, Mk) # Cs, A @ (False, S, U) # Cs) : ldcrC45" defs ldcrC45e_def : "ldcrC45e == ldcrC2 Un snd ` ldcrC1i Un ldcrC45" ldcrC345e_def : "ldcrC345e == ldcrC45e Un ldcrC3" inductive "ldcr" intros cI : "fcons : cdcr ==> fcons : ldcr" C45 : "cons : ldcrC45 ==> (Name, cons) : ldcr" end